vector_typet::size() is now a constant_exprt

src/ansi-c/ansi_c_convert_type.cpp

@@ -591,7 +591,8 @@ void ansi_c_convert_typet::write(typet &type)
 
   if(vector_size.is_not_nil())
   {
-    vector_typet new_type(type, vector_size);
+    type_with_subtypet new_type(ID_frontend_vector, type);
+    new_type.set(ID_size, vector_size);
     new_type.add_source_location()=vector_size.source_location();
     type=new_type;
   }

src/ansi-c/c_typecheck_base.h

@@ -213,7 +213,7 @@ class c_typecheck_baset:
   virtual void typecheck_c_bit_field_type(c_bit_field_typet &type);
   virtual void typecheck_typeof_type(typet &type);
   virtual void typecheck_array_type(array_typet &type);
-  virtual void typecheck_vector_type(vector_typet &type);
+  virtual void typecheck_vector_type(typet &type);
   virtual void typecheck_custom_type(typet &type);
   virtual void adjust_function_parameter(typet &type) const;
   virtual bool is_complete_type(const typet &type) const;

src/ansi-c/c_typecheck_type.cpp

@@ -99,7 +99,13 @@ void c_typecheck_baset::typecheck_type(typet &type)
     // nothing to do, these stay as is
   }
   else if(type.id()==ID_vector)
-    typecheck_vector_type(to_vector_type(type));
+  {
+    // already done
+  }
+  else if(type.id() == ID_frontend_vector)
+  {
+    typecheck_vector_type(type);
+  }
   else if(type.id()==ID_custom_unsignedbv ||
           type.id()==ID_custom_signedbv ||
           type.id()==ID_custom_floatbv ||
@@ -655,14 +661,17 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
   }
 }
 
-void c_typecheck_baset::typecheck_vector_type(vector_typet &type)
+void c_typecheck_baset::typecheck_vector_type(typet &type)
 {
-  exprt &size=type.size();
-  source_locationt source_location=size.find_source_location();
+  // This turns the type with ID_frontend_vector into the type
+  // with ID_vector; the difference is that the latter has
+  // a constant as size, which we establish now.
+  exprt size = static_cast<const exprt &>(type.find(ID_size));
+  const source_locationt source_location = size.find_source_location();
 
   typecheck_expr(size);
 
-  typet &subtype=type.subtype();
+  typet subtype = type.subtype();
   typecheck_type(subtype);
 
   // we are willing to combine 'vector' with various
@@ -699,25 +708,24 @@ void c_typecheck_baset::typecheck_vector_type(vector_typet &type)
   }
 
   // the subtype must have constant size
-  exprt size_expr=size_of_expr(type.subtype(), *this);
+  exprt sub_size_expr = size_of_expr(subtype, *this);
 
-  simplify(size_expr, *this);
+  simplify(sub_size_expr, *this);
 
-  const auto sub_size = numeric_cast<mp_integer>(size_expr);
+  const auto sub_size = numeric_cast<mp_integer>(sub_size_expr);
 
   if(!sub_size.has_value())
   {
     error().source_location=source_location;
     error() << "failed to determine size of vector base type `"
-            << to_string(type.subtype()) << "'" << eom;
+            << to_string(subtype) << "'" << eom;
     throw 0;
   }
 
   if(*sub_size == 0)
   {
     error().source_location=source_location;
-    error() << "type had size 0: `"
-            << to_string(type.subtype()) << "'" << eom;
+    error() << "type had size 0: `" << to_string(subtype) << "'" << eom;
     throw 0;
   }
 
@@ -733,7 +741,11 @@ void c_typecheck_baset::typecheck_vector_type(vector_typet &type)
 
   s /= *sub_size;
 
-  type.size()=from_integer(s, signed_size_type());
+  // produce the type with ID_vector
+  vector_typet new_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;
 }
 
 void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)

src/cpp/cpp_typecheck_type.cpp

@@ -142,7 +142,11 @@ void cpp_typecheckt::typecheck_type(typet &type)
   }
   else if(type.id()==ID_vector)
   {
-    typecheck_vector_type(to_vector_type(type));
+    // already done
+  }
+  else if(type.id() == ID_frontend_vector)
+  {
+    typecheck_vector_type(type);
   }
   else if(type.id()==ID_code)
   {

src/cpp/parse.cpp

@@ -2206,7 +2206,8 @@ bool Parser::rAttribute(typet &t)
       if(lex.get_token(tk3)!=')')
         return false;
 
-      vector_typet attr(uninitialized_typet{}, exp);
+      type_with_subtypet attr(ID_frontend_vector, uninitialized_typet{});
+      attr.set(ID_size, exp);
       attr.add_source_location()=exp.source_location();
       merge_types(attr, t);
       break;

src/util/irep_ids.def

@@ -470,6 +470,7 @@ IREP_ID_ONE(transparent_union)
 IREP_ID_TWO(C_transparent_union, #transparent_union)
 IREP_ID_ONE(aligned)
 IREP_ID_TWO(C_alignment, #alignment)
+IREP_ID_ONE(frontend_vector)
 IREP_ID_ONE(vector)
 IREP_ID_ONE(abstract)
 IREP_ID_ONE(function_application)

src/util/std_types.cpp

@@ -283,3 +283,19 @@ 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)
+{
+  size() = _size;
+}
+
+const constant_exprt &vector_typet::size() const
+{
+  return static_cast<const constant_exprt &>(find(ID_size));
+}
+
+constant_exprt &vector_typet::size()
+{
+  return static_cast<constant_exprt &>(add(ID_size));
+}

src/util/std_types.h

@@ -1751,28 +1751,18 @@ inline range_typet &to_range_type(typet &type)
 /// Used to represent the short vectors used by CPU instruction sets such as
 /// MMX, SSE and AVX. They all provide registers that are something like
 /// 8 x int32, for example, and corresponding operations that operate
-/// element-wise on their operand vectors. Compared to \ref array_typet
-/// that has no element-wise operators. Note that `remove_vector.h` removes
-/// this data type by compilation into arrays.
+/// element-wise on their operand vectors. Compared to \ref array_typet,
+/// vector_typet has a fixed size whereas array_typet has no element-wise
+/// operators.
+/// Note that `remove_vector.h` removes this data type by compilation into
+/// arrays.
 class vector_typet:public type_with_subtypet
 {
 public:
-  vector_typet(
-    const typet &_subtype,
-    const exprt &_size):type_with_subtypet(ID_vector, _subtype)
-  {
-    size()=_size;
-  }
+  vector_typet(const typet &_subtype, const constant_exprt &_size);
 
-  const exprt &size() const
-  {
-    return static_cast<const exprt &>(find(ID_size));
-  }
-
-  exprt &size()
-  {
-    return static_cast<exprt &>(add(ID_size));
-  }
+  const constant_exprt &size() const;
+  constant_exprt &size();
 };
 
 /// Check whether a reference to a typet is a \ref vector_typet.

unit/solvers/lowering/byte_operators.cpp

@@ -68,7 +68,7 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
     unsignedbv_typet u32(32);
     unsignedbv_typet u64(64);
 
-    exprt size = from_integer(8, size_type());
+    constant_exprt size = from_integer(8, size_type());
 
     std::vector<typet> types = {
       struct_typet({{"comp1", u32}, {"comp2", u64}}),
@@ -211,7 +211,7 @@ SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]")
     unsignedbv_typet u32(32);
     unsignedbv_typet u64(64);
 
-    exprt size = from_integer(8, size_type());
+    constant_exprt size = from_integer(8, size_type());
 
     std::vector<typet> types = {
     // TODO: only arrays and scalars