introduce index_type and element_type for arrays and vectors

This commit introduces convenience methods for retrieving the type of the
elements and of the indices for array and vector types.  This avoids using a
global, architecture-dependent function to generate the index type.

Author: kroening

src/goto-instrument/goto_program2code.cpp

@@ -405,9 +405,7 @@ void goto_program2codet::convert_assign_rec(
     forall_operands(it, assign.rhs())
     {
       index_exprt index(
-          assign.lhs(),
-          from_integer(i++, index_type()),
-          type.subtype());
+        assign.lhs(), from_integer(i++, type.index_type()), type.subtype());
       convert_assign_rec(code_assignt(index, *it), dest);
     }
   }

src/goto-symex/field_sensitivity.cpp

@@ -204,7 +204,7 @@ exprt field_sensitivityt::get_fields(
 
     for(std::size_t i = 0; i < array_size; ++i)
     {
-      const index_exprt index(array, from_integer(i, index_type()));
+      const index_exprt index(array, from_integer(i, type.index_type()));
       ssa_exprt tmp = ssa_expr;
       bool was_l2 = !tmp.get_level_2().empty();
       tmp.remove_level_2();
@@ -318,7 +318,7 @@ void field_sensitivityt::field_assignments_rec(
     exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
     for(std::size_t i = 0; i < array_size; ++i)
     {
-      const index_exprt index_rhs(lhs, from_integer(i, index_type()));
+      const index_exprt index_rhs(lhs, from_integer(i, type->index_type()));
       const exprt &index_lhs = *fs_it;
 
       field_assignments_rec(

src/goto-symex/symex_builtin_functions.cpp

@@ -197,7 +197,7 @@ void goto_symext::symex_allocate(
   {
     const auto &array_type = to_array_type(*object_type);
     index_exprt index_expr(
-      value_symbol.symbol_expr(), from_integer(0, index_type()));
+      value_symbol.symbol_expr(), from_integer(0, array_type.index_type()));
     rhs = address_of_exprt(index_expr, pointer_type(array_type.subtype()));
   }
   else

src/solvers/flattening/boolbv_get.cpp

@@ -69,10 +69,12 @@ exprt boolbvt::bv_get_rec(
   {
     if(type.id()==ID_array)
     {
+      const auto &array_type = to_array_type(type);
+
       if(is_unbounded_array(type))
         return bv_get_unbounded_array(expr);
 
-      const typet &subtype=type.subtype();
+      const typet &subtype = array_type.element_type();
       std::size_t sub_width=boolbv_width(subtype);
 
       if(sub_width!=0)
@@ -85,7 +87,8 @@ exprt boolbvt::bv_get_rec(
             new_offset+=sub_width)
         {
           const index_exprt index{
-            expr, from_integer(new_offset / sub_width, index_type())};
+            expr,
+            from_integer(new_offset / sub_width, array_type.index_type())};
           op.push_back(bv_get_rec(index, bv, offset + new_offset, subtype));
         }
 
@@ -95,7 +98,7 @@ exprt boolbvt::bv_get_rec(
       }
       else
       {
-        return array_exprt{{}, to_array_type(type)};
+        return array_exprt{{}, array_type};
       }
     }
     else if(type.id()==ID_struct_tag)
@@ -156,18 +159,20 @@ exprt boolbvt::bv_get_rec(
     }
     else if(type.id()==ID_vector)
     {
-      const typet &subtype = type.subtype();
+      const auto &vector_type = to_vector_type(type);
+      const typet &subtype = vector_type.subtype();
       std::size_t sub_width=boolbv_width(subtype);
 
       if(sub_width!=0 && width%sub_width==0)
       {
         std::size_t size=width/sub_width;
-        vector_exprt value({}, to_vector_type(type));
+        vector_exprt value({}, vector_type);
         value.reserve_operands(size);
 
         for(std::size_t i=0; i<size; i++)
         {
-          const index_exprt index{expr, from_integer(i, index_type())};
+          const index_exprt index{expr,
+                                  from_integer(i, vector_type.index_type())};
           value.operands().push_back(
             bv_get_rec(index, bv, i * sub_width, subtype));
         }

src/util/pointer_offset_size.cpp

@@ -675,7 +675,9 @@ optionalt<exprt> get_subexpression_at_offset(
       {
         return get_subexpression_at_offset(
           index_exprt(
-            expr, from_integer(offset_bytes / elem_size_bytes, index_type())),
+            expr,
+            from_integer(
+              offset_bytes / elem_size_bytes, array_type.index_type())),
           offset_inside_elem,
           target_type_raw,
           ns);

src/util/std_types.cpp

@@ -28,6 +28,12 @@ void array_typet::check(const typet &type, const validation_modet vm)
   }
 }
 
+const typet &array_typet::index_type() const
+{
+  PRECONDITION(is_complete());
+  return size().type();
+}
+
 /// Return the sequence number of the component with given name.
 std::size_t struct_union_typet::component_number(
   const irep_idt &component_name) const
@@ -236,6 +242,11 @@ vector_typet::vector_typet(const typet &_subtype, const constant_exprt &_size)
   size() = _size;
 }
 
+const typet &vector_typet::index_type() const
+{
+  return size().type();
+}
+
 const constant_exprt &vector_typet::size() const
 {
   return static_cast<const constant_exprt &>(find(ID_size));

src/util/std_types.h

@@ -768,6 +768,15 @@ class array_typet:public type_with_subtypet
     add(ID_size, std::move(_size));
   }
 
+  /// The type of the index expressions into any instance of this type.
+  const typet &index_type() const;
+
+  /// The type of the elements of the array.
+  const typet &element_type() const
+  {
+    return subtype();
+  }
+
   const exprt &size() const
   {
     return static_cast<const exprt &>(find(ID_size));
@@ -976,6 +985,15 @@ class vector_typet:public type_with_subtypet
 public:
   vector_typet(const typet &_subtype, const constant_exprt &_size);
 
+  /// The type of any index expression into an instance of this type.
+  const typet &index_type() const;
+
+  /// The type of the elements of the vector.
+  const typet &element_type() const
+  {
+    return subtype();
+  }
+
   const constant_exprt &size() const;
   constant_exprt &size();
 };