add index type to the C vector type

This commit adds an index type to the C vector type to allow treating vector
index expressions in a similar way as array index expressions.  The C
front-end now annotates the vector type with that index type.  We will
eventually enforce that all index expressions use this type.

Author: kroening

src/ansi-c/c_expr.cpp

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

src/ansi-c/c_typecheck_expr.cpp

@@ -1442,8 +1442,10 @@ void c_typecheck_baset::typecheck_expr_rel_vector(binary_exprt &expr)
   // with the same dimension.
   auto subtype_width =
     to_bitvector_type(to_vector_type(o_type0).element_type()).get_width();
-  expr.type() =
-    vector_typet{signedbv_typet{subtype_width}, to_vector_type(o_type0).size()};
+  expr.type() = vector_typet{
+    to_vector_type(o_type0).index_type(),
+    signedbv_typet{subtype_width},
+    to_vector_type(o_type0).size()};
 
   // Replace the id as the semantics of these are point-wise application (and
   // the result is not of bool type).

src/ansi-c/c_typecheck_type.cpp

@@ -219,24 +219,28 @@ void c_typecheck_baset::typecheck_type(typet &type)
       else if(gcc_attr_mode == "__V2SI__") // vector of 2 ints, deprecated
       {
         if(is_signed)
-          result=vector_typet(
-            signed_int_type(),
-            from_integer(2, size_type()));
+        {
+          result = vector_typet(
+            c_index_type(), signed_int_type(), from_integer(2, size_type()));
+        }
         else
-          result=vector_typet(
-            unsigned_int_type(),
-            from_integer(2, size_type()));
+        {
+          result = vector_typet(
+            c_index_type(), unsigned_int_type(), from_integer(2, size_type()));
+        }
       }
       else if(gcc_attr_mode == "__V4SI__") // vector of 4 ints, deprecated
       {
         if(is_signed)
-          result=vector_typet(
-            signed_int_type(),
-            from_integer(4, size_type()));
+        {
+          result = vector_typet(
+            c_index_type(), signed_int_type(), from_integer(4, size_type()));
+        }
         else
-          result=vector_typet(
-            unsigned_int_type(),
-            from_integer(4, size_type()));
+        {
+          result = vector_typet(
+            c_index_type(), unsigned_int_type(), from_integer(4, size_type()));
+        }
       }
       else // give up, just use subtype
         result = to_type_with_subtype(type).subtype();
@@ -266,13 +270,17 @@ void c_typecheck_baset::typecheck_type(typet &type)
       else if(gcc_attr_mode == "__TF__") // 128 bits
         result=gcc_float128_type();
       else if(gcc_attr_mode == "__V2SF__") // deprecated vector of 2 floats
-        result=vector_typet(float_type(), from_integer(2, size_type()));
+        result = vector_typet(
+          c_index_type(), float_type(), from_integer(2, size_type()));
       else if(gcc_attr_mode == "__V2DF__") // deprecated vector of 2 doubles
-        result=vector_typet(double_type(), from_integer(2, size_type()));
+        result = vector_typet(
+          c_index_type(), double_type(), from_integer(2, size_type()));
       else if(gcc_attr_mode == "__V4SF__") // deprecated vector of 4 floats
-        result=vector_typet(float_type(), from_integer(4, size_type()));
+        result = vector_typet(
+          c_index_type(), float_type(), from_integer(4, size_type()));
       else if(gcc_attr_mode == "__V4DF__") // deprecated vector of 4 doubles
-        result=vector_typet(double_type(), from_integer(4, size_type()));
+        result = vector_typet(
+          c_index_type(), double_type(), from_integer(4, size_type()));
       else // give up, just use subtype
         result = to_type_with_subtype(type).subtype();
 
@@ -745,7 +753,8 @@ void c_typecheck_baset::typecheck_vector_type(typet &type)
   s /= *sub_size;
 
   // produce the type with ID_vector
-  vector_typet new_type(subtype, from_integer(s, signed_size_type()));
+  vector_typet new_type(
+    c_index_type(), subtype, from_integer(s, signed_size_type()));
   new_type.add_source_location() = source_location;
   new_type.size().add_source_location() = source_location;
   type = new_type;

src/util/std_types.cpp

@@ -244,16 +244,26 @@ bool is_constant_or_has_constant_components(
   return false;
 }
 
-vector_typet::vector_typet(const typet &_subtype, const constant_exprt &_size)
-  : type_with_subtypet(ID_vector, _subtype)
+vector_typet::vector_typet(
+  typet _index_type,
+  typet _element_type,
+  constant_exprt _size)
+  : type_with_subtypet(ID_vector, std::move(_element_type))
 {
-  size() = _size;
+  index_type_nonconst() = std::move(_index_type);
+  size() = std::move(_size);
 }
 
 typet vector_typet::index_type() const
 {
-  // we may wish to make the index type part of the vector type
-  return c_index_type();
+  // For backwards compatibility, allow the case that the array type is
+  // not annotated with an index type.
+  const auto &annotated_type =
+    static_cast<const typet &>(find(ID_C_index_type));
+  if(annotated_type.is_nil())
+    return c_index_type();
+  else
+    return annotated_type;
 }
 
 const constant_exprt &vector_typet::size() const

src/util/std_types.h

@@ -1007,11 +1007,19 @@ inline range_typet &to_range_type(typet &type)
 class vector_typet:public type_with_subtypet
 {
 public:
-  vector_typet(const typet &_subtype, const constant_exprt &_size);
+  vector_typet(typet index_type, typet element_type, constant_exprt size);
 
   /// The type of any index expression into an instance of this type.
   typet index_type() const;
 
+  /// The type of any index expression into an instance of this type.
+  /// This is added as a comment now for backwards compatibility, but will
+  /// eventually be the first subtype.
+  typet &index_type_nonconst()
+  {
+    return static_cast<typet &>(add(ID_C_index_type));
+  }
+
   /// The type of the elements of the vector.
   /// This method is preferred over .subtype(),
   /// which will eventually be deprecated.

unit/solvers/lowering/byte_operators.cpp

@@ -255,10 +255,11 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
     std::vector<typet> types = {
       struct_typet({{"comp1", u16}, {"comp2", u16}}),
       struct_typet({{"comp1", u32}, {"comp2", u64}}),
-      struct_typet({{"comp1", u32},
-                    {"compX", c_bit_field_typet(u8, 4)},
-                    {"pad", c_bit_field_typet(u8, 4)},
-                    {"comp2", u8}}),
+      struct_typet(
+        {{"comp1", u32},
+         {"compX", c_bit_field_typet(u8, 4)},
+         {"pad", c_bit_field_typet(u8, 4)},
+         {"comp2", u8}}),
       union_typet({{"compA", u32}, {"compB", u64}}),
       c_enum_typet(u16),
       c_enum_typet(unsignedbv_typet(128)),
@@ -272,8 +273,8 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
       ieee_float_spect::single_precision().to_type(),
       // generates the correct value, but remains wrapped in a typecast
       // pointer_typet(u64, 64),
-      vector_typet(u8, size),
-      vector_typet(u64, size),
+      vector_typet(size_type(), u8, size),
+      vector_typet(size_type(), u64, size),
       complex_typet(s16),
       complex_typet(u64)};
 
@@ -405,10 +406,11 @@ SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]")
     std::vector<typet> types = {
       struct_typet({{"comp1", u16}, {"comp2", u16}}),
       struct_typet({{"comp1", u32}, {"comp2", u64}}),
-      struct_typet({{"comp1", u32},
-                    {"compX", c_bit_field_typet(u8, 4)},
-                    {"pad", c_bit_field_typet(u8, 4)},
-                    {"comp2", u8}}),
+      struct_typet(
+        {{"comp1", u32},
+         {"compX", c_bit_field_typet(u8, 4)},
+         {"pad", c_bit_field_typet(u8, 4)},
+         {"comp2", u8}}),
       union_typet({{"compA", u32}, {"compB", u64}}),
       c_enum_typet(u16),
       c_enum_typet(unsignedbv_typet(128)),
@@ -422,8 +424,8 @@ SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]")
       ieee_float_spect::single_precision().to_type(),
       // generates the correct value, but remains wrapped in a typecast
       // pointer_typet(u64, 64),
-      vector_typet(u8, size),
-      vector_typet(u64, size),
+      vector_typet(size_type(), u8, size),
+      vector_typet(size_type(), u64, size),
       // complex_typet(s16),
       // complex_typet(u64)
     };