introduce index_type and element_type for arrays and vectors

src/goto-instrument/goto_program2code.cpp

@@ -405,9 +405,9 @@ 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.element_type());
       convert_assign_rec(code_assignt(index, *it), dest);
     }
   }

src/goto-symex/field_sensitivity.cpp

@@ -9,7 +9,6 @@ Author: Michael Tautschnig
 #include "field_sensitivity.h"
 
 #include <util/arith_tools.h>
-#include <util/c_types.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 
@@ -204,7 +203,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 +317,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,8 +197,8 @@ 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()));
-    rhs = address_of_exprt(index_expr, pointer_type(array_type.subtype()));
+      value_symbol.symbol_expr(), from_integer(0, array_type.index_type()));
+    rhs = address_of_exprt(index_expr, pointer_type(array_type.element_type()));
   }
   else
   {
@@ -277,10 +277,11 @@ void goto_symext::symex_va_start(
       va_list_entry(parameter, to_pointer_type(lhs.type()), ns));
   }
   const std::size_t va_arg_size = va_arg_operands.size();
-  exprt array =
-    array_exprt{std::move(va_arg_operands),
-                array_typet{pointer_type(empty_typet{}),
-                            from_integer(va_arg_size, size_type())}};
+
+  const auto array_type = array_typet{pointer_type(empty_typet{}),
+                                      from_integer(va_arg_size, size_type())};
+
+  exprt array = array_exprt{std::move(va_arg_operands), array_type};
 
   symbolt &va_array = get_fresh_aux_symbol(
     array.type(),
@@ -296,8 +297,8 @@ void goto_symext::symex_va_start(
   do_simplify(array);
   symex_assign(state, va_array.symbol_expr(), std::move(array));
 
-  exprt rhs = address_of_exprt{
-    index_exprt{va_array.symbol_expr(), from_integer(0, index_type())}};
+  exprt rhs = address_of_exprt{index_exprt{
+    va_array.symbol_expr(), from_integer(0, array_type.index_type())}};
   rhs = state.rename(std::move(rhs), ns).get();
   symex_assign(state, lhs, typecast_exprt::conditional_cast(rhs, lhs.type()));
 }
@@ -517,8 +518,9 @@ void goto_symext::symex_cpp_new(
 
   if(do_array)
   {
-    rhs.add_to_operands(
-      index_exprt(symbol.symbol_expr(), from_integer(0, index_type())));
+    rhs.add_to_operands(index_exprt(
+      symbol.symbol_expr(),
+      from_integer(0, to_array_type(symbol.type).index_type())));
   }
   else
     rhs.copy_to_operands(symbol.symbol_expr());

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,20 +159,22 @@ exprt boolbvt::bv_get_rec(
     }
     else if(type.id()==ID_vector)
     {
-      const typet &subtype = type.subtype();
-      std::size_t sub_width=boolbv_width(subtype);
+      const auto &vector_type = to_vector_type(type);
+      const typet &element_type = vector_type.element_type();
+      std::size_t element_width = boolbv_width(element_type);
 
-      if(sub_width!=0 && width%sub_width==0)
+      if(element_width != 0 && width % element_width == 0)
       {
-        std::size_t size=width/sub_width;
-        vector_exprt value({}, to_vector_type(type));
+        std::size_t size = width / element_width;
+        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));
+            bv_get_rec(index, bv, i * element_width, element_type));
         }
 
         return std::move(value);

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_expr.h

@@ -1327,6 +1327,9 @@ inline notequal_exprt &to_notequal_expr(exprt &expr)
 class index_exprt:public binary_exprt
 {
 public:
+  // When _array has array_type, the type of _index
+  // must be array_type.index_type().
+  // This will eventually be enforced using a precondition.
   index_exprt(const exprt &_array, exprt _index)
     : binary_exprt(_array, ID_index, std::move(_index), _array.type().subtype())
   {

src/util/std_types.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "std_types.h"
 
+#include "c_types.h"
 #include "namespace.h"
 #include "std_expr.h"
 
@@ -28,6 +29,12 @@ void array_typet::check(const typet &type, const validation_modet vm)
   }
 }
 
+typet array_typet::index_type() const
+{
+  // we may wish to make the index type part of the array type
+  return ::index_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 +243,12 @@ vector_typet::vector_typet(const typet &_subtype, const constant_exprt &_size)
   size() = _size;
 }
 
+typet vector_typet::index_type() const
+{
+  // we may wish to make the index type part of the vector type
+  return ::index_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,17 @@ 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.
+  typet index_type() const;
+
+  /// The type of the elements of the array.
+  /// This method is preferred over .subtype(),
+  /// which will eventually be deprecated.
+  const typet &element_type() const
+  {
+    return subtype();
+  }
+
   const exprt &size() const
   {
     return static_cast<const exprt &>(find(ID_size));
@@ -976,6 +987,17 @@ 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.
+  typet index_type() const;
+
+  /// The type of the elements of the vector.
+  /// This method is preferred over .subtype(),
+  /// which will eventually be deprecated.
+  const typet &element_type() const
+  {
+    return subtype();
+  }
+
   const constant_exprt &size() const;
   constant_exprt &size();
 };