Merge pull request #6587 from diffblue/remove_ID_size_usage

array_typet and vector_typet APIs

Author: tautschnig

src/analyses/goto_rw.cpp

@@ -262,15 +262,15 @@ void rw_range_sett::get_objects_index(
   {
     const vector_typet &vector_type=to_vector_type(type);
 
-    auto subtype_bits = pointer_offset_bits(vector_type.subtype(), ns);
+    auto subtype_bits = pointer_offset_bits(vector_type.element_type(), ns);
 
     sub_size = subtype_bits.has_value() ? to_range_spect(*subtype_bits) : -1;
   }
   else if(type.id()==ID_array)
   {
     const array_typet &array_type=to_array_type(type);
 
-    auto subtype_bits = pointer_offset_bits(array_type.subtype(), ns);
+    auto subtype_bits = pointer_offset_bits(array_type.element_type(), ns);
 
     sub_size = subtype_bits.has_value() ? to_range_spect(*subtype_bits) : -1;
   }
@@ -301,7 +301,7 @@ void rw_range_sett::get_objects_array(
 {
   const array_typet &array_type = expr.type();
 
-  auto subtype_bits = pointer_offset_bits(array_type.subtype(), ns);
+  auto subtype_bits = pointer_offset_bits(array_type.element_type(), ns);
 
   range_spect sub_size;
 
@@ -608,7 +608,7 @@ void rw_range_sett::get_objects_rec(const typet &type)
   if(type.id()==ID_array)
   {
     const auto &array_type = to_array_type(type);
-    get_objects_rec(array_type.subtype());
+    get_objects_rec(array_type.element_type());
     get_objects_rec(get_modet::READ, array_type.size());
   }
 }

src/analyses/variable-sensitivity/abstract_aggregate_object.h

@@ -164,7 +164,7 @@ struct array_aggregate_typet
   static typet read_type(const typet &, const typet &object_type)
   {
     array_typet array_type(to_array_type(object_type));
-    return array_type.subtype();
+    return array_type.element_type();
   }
 
   static void get_statistics(

src/ansi-c/c_expr.cpp

@@ -23,8 +23,8 @@ shuffle_vector_exprt::shuffle_vector_exprt(
     op1() = std::move(*vector2);
 
   const vector_typet &vt = to_vector_type(op0().type());
-  type() =
-    vector_typet{vt.subtype(), from_integer(indices.size(), vt.size().type())};
+  type() = vector_typet{vt.element_type(),
+                        from_integer(indices.size(), vt.size().type())};
 
   op2().operands().swap(indices);
 }

src/ansi-c/c_typecast.cpp

@@ -223,8 +223,9 @@ bool check_c_implicit_typecast(
       }
     }
 
-    if(dest_type.id()==ID_array &&
-       src_type.subtype()==dest_type.subtype())
+    if(
+      dest_type.id() == ID_array &&
+      src_type.subtype() == to_array_type(dest_type).element_type())
       return false;
 
     if(dest_type.id()==ID_bool ||

src/ansi-c/c_typecheck_expr.cpp

@@ -3389,15 +3389,16 @@ bool c_typecheck_baset::gcc_vector_types_compatible(
     return false;
 
   // compare subtype
-  if((type0.subtype().id()==ID_signedbv ||
-      type0.subtype().id()==ID_unsignedbv) &&
-     (type1.subtype().id()==ID_signedbv ||
-      type1.subtype().id()==ID_unsignedbv) &&
-     to_bitvector_type(type0.subtype()).get_width()==
-     to_bitvector_type(type1.subtype()).get_width())
+  if(
+    (type0.element_type().id() == ID_signedbv ||
+     type0.element_type().id() == ID_unsignedbv) &&
+    (type1.element_type().id() == ID_signedbv ||
+     type1.element_type().id() == ID_unsignedbv) &&
+    to_bitvector_type(type0.element_type()).get_width() ==
+      to_bitvector_type(type1.element_type()).get_width())
     return true;
 
-  return type0.subtype()==type1.subtype();
+  return type0.element_type() == type1.element_type();
 }
 
 void c_typecheck_baset::typecheck_expr_binary_arithmetic(exprt &expr)

src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp

@@ -1440,7 +1440,8 @@ exprt c_typecheck_baset::typecheck_shuffle_vector(
     CHECK_RETURN(input_size.has_value());
     if(arg1.has_value())
       input_size = *input_size * 2;
-    constant_exprt size = from_integer(*input_size, indices_type.subtype());
+    constant_exprt size =
+      from_integer(*input_size, indices_type.element_type());
 
     for(std::size_t i = 0; i < indices_size; ++i)
     {

src/ansi-c/c_typecheck_initializer.cpp

@@ -318,7 +318,7 @@ void c_typecheck_baset::designator_enter(
     if(array_type.size().is_nil())
     {
       entry.size=0;
-      entry.subtype=array_type.subtype();
+      entry.subtype = array_type.element_type();
     }
     else
     {
@@ -332,7 +332,7 @@ void c_typecheck_baset::designator_enter(
       }
 
       entry.size = numeric_cast_v<std::size_t>(*array_size);
-      entry.subtype=array_type.subtype();
+      entry.subtype = array_type.element_type();
     }
   }
   else if(full_type.id()==ID_vector)
@@ -350,7 +350,7 @@ void c_typecheck_baset::designator_enter(
     }
 
     entry.size = numeric_cast_v<std::size_t>(*vector_size);
-    entry.subtype=vector_type.subtype();
+    entry.subtype = vector_type.element_type();
   }
   else
     UNREACHABLE;

src/ansi-c/c_typecheck_type.cpp

@@ -526,18 +526,18 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
   const source_locationt size_source_location = size.find_source_location();
 
   // check subtype
-  typecheck_type(type.subtype());
+  typecheck_type(type.element_type());
 
   // we don't allow void as subtype
-  if(type.subtype().id() == ID_empty)
+  if(type.element_type().id() == ID_empty)
   {
     error().source_location=type.source_location();
     error() << "array of voids" << eom;
     throw 0;
   }
 
   // we don't allow incomplete structs or unions as subtype
-  const typet &followed_subtype = follow(type.subtype());
+  const typet &followed_subtype = follow(type.element_type());
 
   if(
     (followed_subtype.id() == ID_struct || followed_subtype.id() == ID_union) &&
@@ -550,7 +550,7 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
   }
 
   // we don't allow functions as subtype
-  if(type.subtype().id() == ID_code)
+  if(type.element_type().id() == ID_code)
   {
     // ISO/IEC 9899 6.7.5.2
     error().source_location = type.source_location();

src/ansi-c/expr2c.cpp

@@ -587,7 +587,7 @@ std::string expr2ct::convert_rec(
     const mp_integer size_int = numeric_cast_v<mp_integer>(vector_type.size());
     std::string dest="__gcc_v"+integer2string(size_int);
 
-    std::string tmp=convert(vector_type.subtype());
+    std::string tmp = convert(vector_type.element_type());
 
     if(tmp=="signed char" || tmp=="char")
       dest+="qi";
@@ -603,7 +603,7 @@ std::string expr2ct::convert_rec(
       dest+="df";
     else
     {
-      const std::string subtype=convert(vector_type.subtype());
+      const std::string subtype = convert(vector_type.element_type());
       dest=subtype;
       dest+=" __attribute__((vector_size (";
       dest+=convert(vector_type.size());

src/cpp/cpp_declarator_converter.cpp

@@ -313,10 +313,11 @@ void cpp_declarator_convertert::combine_types(
   }
   else if(symbol.type==decl_type)
     return; // ok
-  else if(symbol.type.id()==ID_array &&
-          symbol.type.find(ID_size).is_nil() &&
-          decl_type.id()==ID_array &&
-          symbol.type.subtype()==decl_type.subtype())
+  else if(
+    symbol.type.id() == ID_array &&
+    to_array_type(symbol.type).size().is_nil() && decl_type.id() == ID_array &&
+    to_array_type(symbol.type).element_type() ==
+      to_array_type(decl_type).element_type())
   {
     symbol.type = decl_type;
     return; // ok

src/cpp/cpp_typecheck_compound_type.cpp

@@ -794,7 +794,7 @@ void cpp_typecheckt::check_fixed_size_array(typet &type)
     }
 
     // recursive call for multi-dimensional arrays
-    check_fixed_size_array(array_type.subtype());
+    check_fixed_size_array(array_type.element_type());
   }
 }
 

src/cpp/cpp_typecheck_initializer.cpp

@@ -244,8 +244,8 @@ void cpp_typecheckt::zero_initializer(
     for(mp_integer i=0; i<size; ++i)
     {
       index_exprt index(
-        object, from_integer(i, c_index_type()), array_type.subtype());
-      zero_initializer(index, array_type.subtype(), source_location, ops);
+        object, from_integer(i, c_index_type()), array_type.element_type());
+      zero_initializer(index, array_type.element_type(), source_location, ops);
     }
   }
   else if(final_type.id()==ID_union)

src/cpp/template_map.cpp

@@ -23,8 +23,8 @@ void template_mapt::apply(typet &type) const
 {
   if(type.id()==ID_array)
   {
-    apply(type.subtype());
-    apply(static_cast<exprt &>(type.add(ID_size)));
+    apply(to_array_type(type).element_type());
+    apply(to_array_type(type).size());
   }
   else if(type.id()==ID_pointer)
   {

src/goto-programs/graphml_witness.cpp

@@ -109,7 +109,7 @@ std::string graphml_witnesst::convert_assign_rec(
     forall_operands(it, assign.rhs())
     {
       index_exprt index(
-        assign.lhs(), from_integer(i++, c_index_type()), type.subtype());
+        assign.lhs(), from_integer(i++, c_index_type()), type.element_type());
       if(!result.empty())
         result+=' ';
       result+=convert_assign_rec(identifier, code_assignt(index, *it));

src/goto-programs/interpreter.cpp

@@ -487,7 +487,7 @@ exprt interpretert::get_value(
   {
     // Get size of array
     array_exprt result({}, to_array_type(real_type));
-    const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
+    const exprt &size_expr = to_array_type(type).size();
     mp_integer subtype_size=get_size(type.subtype());
     mp_integer count;
     if(size_expr.id()!=ID_constant)
@@ -553,7 +553,7 @@ exprt interpretert::get_value(
   else if(real_type.id()==ID_array)
   {
     array_exprt result({}, to_array_type(real_type));
-    const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
+    const exprt &size_expr = to_array_type(real_type).size();
 
     // Get size of array
     mp_integer subtype_size=get_size(type.subtype());
@@ -888,7 +888,7 @@ typet interpretert::concretize_type(const typet &type)
 {
   if(type.id()==ID_array)
   {
-    const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
+    const exprt &size_expr = to_array_type(type).size();
     mp_vectort computed_size = evaluate(size_expr);
     if(computed_size.size()==1 &&
        computed_size[0]>=0)
@@ -1006,7 +1006,7 @@ mp_integer interpretert::get_size(const typet &type)
   }
   else if(type.id()==ID_array)
   {
-    const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
+    const exprt &size_expr = to_array_type(type).size();
 
     mp_integer subtype_size=get_size(type.subtype());
 

src/goto-programs/interpreter_evaluate.cpp

@@ -136,7 +136,7 @@ bool interpretert::count_type_leaves(const typet &ty, mp_integer &result)
     if(array_size_vec.size()!=1)
       return true;
     mp_integer subtype_count;
-    if(count_type_leaves(at.subtype(), subtype_count))
+    if(count_type_leaves(at.element_type(), subtype_count))
       return true;
     result=array_size_vec[0]*subtype_count;
     return false;
@@ -205,12 +205,12 @@ bool interpretert::byte_offset_to_memory_offset(
       return true;
 
     mp_integer array_size=array_size_vec[0];
-    auto elem_size_bytes = pointer_offset_size(at.subtype(), ns);
+    auto elem_size_bytes = pointer_offset_size(at.element_type(), ns);
     if(!elem_size_bytes.has_value() || *elem_size_bytes == 0)
       return true;
 
     mp_integer elem_size_leaves;
-    if(count_type_leaves(at.subtype(), elem_size_leaves))
+    if(count_type_leaves(at.element_type(), elem_size_leaves))
       return true;
 
     mp_integer this_idx = offset / (*elem_size_bytes);
@@ -219,7 +219,7 @@ bool interpretert::byte_offset_to_memory_offset(
 
     mp_integer subtype_result;
     bool ret = byte_offset_to_memory_offset(
-      at.subtype(), offset % (*elem_size_bytes), subtype_result);
+      at.element_type(), offset % (*elem_size_bytes), subtype_result);
 
     result=subtype_result+(elem_size_leaves*this_idx);
     return ret;
@@ -280,24 +280,21 @@ bool interpretert::memory_offset_to_byte_offset(
     if(array_size_vec.size()!=1)
       return true;
 
-    auto elem_size = pointer_offset_size(at.subtype(), ns);
+    auto elem_size = pointer_offset_size(at.element_type(), ns);
     if(!elem_size.has_value())
       return true;
 
     mp_integer elem_count;
-    if(count_type_leaves(at.subtype(), elem_count))
+    if(count_type_leaves(at.element_type(), elem_count))
       return true;
 
     mp_integer this_idx=full_cell_offset/elem_count;
     if(this_idx>=array_size_vec[0])
       return true;
 
     mp_integer subtype_result;
-    bool ret=
-      memory_offset_to_byte_offset(
-        at.subtype(),
-        full_cell_offset%elem_count,
-        subtype_result);
+    bool ret = memory_offset_to_byte_offset(
+      at.element_type(), full_cell_offset % elem_count, subtype_result);
     result = subtype_result + ((*elem_size) * this_idx);
     return ret;
   }

src/goto-programs/json_expr.cpp

@@ -154,13 +154,13 @@ json_objectt json(const typet &type, const namespacet &ns, const irep_idt &mode)
   else if(type.id() == ID_array)
   {
     result["name"] = json_stringt("array");
-    result["subtype"] = json(to_array_type(type).subtype(), ns, mode);
+    result["subtype"] = json(to_array_type(type).element_type(), ns, mode);
     result["size"] = json(to_array_type(type).size(), ns, mode);
   }
   else if(type.id() == ID_vector)
   {
     result["name"] = json_stringt("vector");
-    result["subtype"] = json(to_vector_type(type).subtype(), ns, mode);
+    result["subtype"] = json(to_vector_type(type).element_type(), ns, mode);
     result["size"] = json(to_vector_type(type).size(), ns, mode);
   }
   else if(type.id() == ID_struct)

src/goto-programs/remove_vector.cpp

@@ -116,7 +116,7 @@ static void remove_vector(exprt &expr)
       const mp_integer dimension =
         numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
 
-      const typet subtype=array_type.subtype();
+      const typet subtype = array_type.element_type();
       // do component-wise:
       // x+y -> vector(x[0]+y[0],x[1]+y[1],...)
       array_exprt array_expr({}, array_type);
@@ -144,7 +144,7 @@ static void remove_vector(exprt &expr)
       const mp_integer dimension =
         numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
 
-      const typet subtype=array_type.subtype();
+      const typet subtype = array_type.element_type();
       // do component-wise:
       // -x -> vector(-x[0],-x[1],...)
       array_exprt array_expr({}, array_type);
@@ -173,7 +173,7 @@ static void remove_vector(exprt &expr)
       const vector_typet &vector_type = to_vector_type(expr.type());
       const auto dimension = numeric_cast_v<std::size_t>(vector_type.size());
 
-      const typet &subtype = vector_type.subtype();
+      const typet &subtype = vector_type.element_type();
       PRECONDITION(subtype.id() == ID_signedbv);
       exprt minus_one = from_integer(-1, subtype);
       exprt zero = from_integer(0, subtype);
@@ -237,7 +237,7 @@ static void remove_vector(exprt &expr)
         const auto dimension =
           numeric_cast_v<std::size_t>(to_constant_expr(array_type.size()));
         exprt casted_op =
-          typecast_exprt::conditional_cast(op, array_type.subtype());
+          typecast_exprt::conditional_cast(op, array_type.element_type());
         source_locationt source_location = expr.source_location();
         expr = array_exprt(exprt::operandst(dimension, casted_op), array_type);
         expr.add_source_location() = std::move(source_location);
@@ -285,10 +285,10 @@ static void remove_vector(typet &type)
   {
     vector_typet &vector_type=to_vector_type(type);
 
-    remove_vector(type.subtype());
+    remove_vector(vector_type.element_type());
 
     // Replace by an array with appropriate number of members.
-    array_typet array_type(vector_type.subtype(), vector_type.size());
+    array_typet array_type(vector_type.element_type(), vector_type.size());
     array_type.add_source_location()=type.source_location();
     type=array_type;
   }