check type invariant of type_with_subtypet

src/ansi-c/ansi_c_convert_type.cpp

@@ -45,9 +45,13 @@ void ansi_c_convert_typet::read_rec(const typet &type)
     c_qualifiers.is_volatile=true;
   else if(type.id()==ID_asm)
   {
-    if(type.has_subtype() &&
-       type.subtype().id()==ID_string_constant)
-      c_storage_spec.asm_label = to_string_constant(type.subtype()).get_value();
+    // These can have up to 5 subtypes; we only use the first one.
+    const auto &type_with_subtypes = to_type_with_subtypes(type);
+    if(
+      !type_with_subtypes.subtypes().empty() &&
+      type_with_subtypes.subtypes()[0].id() == ID_string_constant)
+      c_storage_spec.asm_label =
+        to_string_constant(type_with_subtypes.subtypes()[0]).get_value();
   }
   else if(type.id()==ID_section &&
           type.has_subtype() &&
@@ -187,8 +191,11 @@ void ansi_c_convert_typet::read_rec(const typet &type)
   {
     c_qualifiers.is_transparent_union=true;
   }
-  else if(type.id()==ID_vector)
-    vector_size=to_vector_type(type).size();
+  else if(type.id() == ID_frontend_vector)
+  {
+    // note that this is not yet a vector_typet -- this is a size only
+    vector_size = static_cast<const constant_exprt &>(type.find(ID_size));
+  }
   else if(type.id()==ID_void)
   {
     // we store 'void' as 'empty'

src/ansi-c/c_storage_spec.cpp

@@ -52,11 +52,12 @@ void c_storage_spect::read(const typet &type)
   {
     alias = to_string_constant(type.subtype()).get_value();
   }
-  else if(type.id()==ID_asm &&
-          type.has_subtype() &&
-          type.subtype().id()==ID_string_constant)
+  else if(
+    type.id() == ID_asm && !to_type_with_subtypes(type).subtypes().empty() &&
+    to_type_with_subtypes(type).subtypes()[0].id() == ID_string_constant)
   {
-    asm_label = to_string_constant(type.subtype()).get_value();
+    asm_label =
+      to_string_constant(to_type_with_subtypes(type).subtypes()[0]).get_value();
   }
   else if(type.id()==ID_section &&
           type.has_subtype() &&

src/ansi-c/parser.y

@@ -1607,7 +1607,7 @@ gcc_type_attribute:
         | TOK_GCC_ATTRIBUTE_TRANSPARENT_UNION
         { $$=$1; set($$, ID_transparent_union); }
         | TOK_GCC_ATTRIBUTE_VECTOR_SIZE '(' comma_expression ')'
-        { $$=$1; set($$, ID_vector); parser_stack($$).add(ID_size)=parser_stack($3); }
+        { $$=$1; set($$, ID_frontend_vector); parser_stack($$).add(ID_size)=parser_stack($3); }
         | TOK_GCC_ATTRIBUTE_ALIGNED
         { $$=$1; set($$, ID_aligned); }
         | TOK_GCC_ATTRIBUTE_ALIGNED '(' comma_expression ')'

src/solvers/lowering/byte_operators.cpp

@@ -56,6 +56,24 @@ static boundst map_bounds(
   return result;
 }
 
+/// changes the width of the given bitvector type
+bitvector_typet adjust_width(const typet &src, std::size_t new_width)
+{
+  if(src.id() == ID_unsignedbv)
+    return unsignedbv_typet(new_width);
+  else if(src.id() == ID_signedbv)
+    return signedbv_typet(new_width);
+  else if(src.id() == ID_bv)
+    return bv_typet(new_width);
+  else if(src.id() == ID_c_enum) // we use the underlying type
+    return adjust_width(to_c_enum_type(src).underlying_type(), new_width);
+  else if(src.id() == ID_c_bit_field)
+    return c_bit_field_typet(
+      to_c_bit_field_type(src).underlying_type(), new_width);
+  else
+    PRECONDITION(false);
+}
+
 /// Convert a bitvector-typed expression \p bitvector_expr to a struct-typed
 /// expression. See \ref bv_to_expr for an overview.
 static struct_exprt bv_to_struct_expr(
@@ -89,7 +107,7 @@ static struct_exprt bv_to_struct_expr(
       endianness_map,
       member_offset_bits,
       member_offset_bits + component_bits - 1);
-    bitvector_typet type{bitvector_expr.type().id(), component_bits};
+    bitvector_typet type = adjust_width(bitvector_expr.type(), component_bits);
     operands.push_back(bv_to_expr(
       extractbits_exprt{bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
       comp.type(),
@@ -133,7 +151,7 @@ static union_exprt bv_to_union_expr(
   }
 
   const auto bounds = map_bounds(endianness_map, 0, component_bits - 1);
-  bitvector_typet type{bitvector_expr.type().id(), component_bits};
+  bitvector_typet type = adjust_width(bitvector_expr.type(), component_bits);
   const irep_idt &component_name = widest_member.has_value()
                                      ? widest_member->first.get_name()
                                      : components.front().get_name();
@@ -185,7 +203,8 @@ static array_exprt bv_to_array_expr(
         numeric_cast_v<std::size_t>(*subtype_bits);
       const auto bounds = map_bounds(
         endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
-      bitvector_typet type{bitvector_expr.type().id(), subtype_bits_int};
+      bitvector_typet type =
+        adjust_width(bitvector_expr.type(), subtype_bits_int);
       operands.push_back(bv_to_expr(
         extractbits_exprt{
           bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
@@ -230,7 +249,8 @@ static vector_exprt bv_to_vector_expr(
         numeric_cast_v<std::size_t>(*subtype_bits);
       const auto bounds = map_bounds(
         endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
-      bitvector_typet type{bitvector_expr.type().id(), subtype_bits_int};
+      bitvector_typet type =
+        adjust_width(bitvector_expr.type(), subtype_bits_int);
       operands.push_back(bv_to_expr(
         extractbits_exprt{
           bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
@@ -274,7 +294,8 @@ static complex_exprt bv_to_complex_expr(
   const auto bounds_imag =
     map_bounds(endianness_map, subtype_bits, subtype_bits * 2 - 1);
 
-  const bitvector_typet type{bitvector_expr.type().id(), subtype_bits};
+  const bitvector_typet type =
+    adjust_width(bitvector_expr.type(), subtype_bits);
 
   return complex_exprt{
     bv_to_expr(
@@ -1293,7 +1314,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
   else // width_bytes>=2
   {
     concatenation_exprt concatenation(
-      std::move(op), bitvector_typet(subtype->id(), width_bytes * 8));
+      std::move(op), adjust_width(*subtype, width_bytes * 8));
 
     endianness_mapt map(concatenation.type(), little_endian, ns);
     return bv_to_expr(concatenation, src.type(), map, ns);
@@ -2304,12 +2325,11 @@ exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns)
       extractbits_exprt extra_bits{
         src.op(), bounds.ub, bounds.lb, bv_typet{n_extra_bits}};
 
-      update_value =
-        concatenation_exprt{typecast_exprt::conditional_cast(
-                              update_value, bv_typet{update_bits_int}),
-                            extra_bits,
-                            bitvector_typet{update_value.type().id(),
-                                            update_bits_int + n_extra_bits}};
+      update_value = concatenation_exprt{
+        typecast_exprt::conditional_cast(
+          update_value, bv_typet{update_bits_int}),
+        extra_bits,
+        adjust_width(update_value.type(), update_bits_int + n_extra_bits)};
     }
     else
     {

src/util/c_types.h

@@ -58,13 +58,15 @@ inline bool can_cast_type<c_bit_field_typet>(const typet &type)
 inline const c_bit_field_typet &to_c_bit_field_type(const typet &type)
 {
   PRECONDITION(can_cast_type<c_bit_field_typet>(type));
+  type_with_subtypet::check(type);
   return static_cast<const c_bit_field_typet &>(type);
 }
 
 /// \copydoc to_c_bit_field_type(const typet &type)
 inline c_bit_field_typet &to_c_bit_field_type(typet &type)
 {
   PRECONDITION(can_cast_type<c_bit_field_typet>(type));
+  type_with_subtypet::check(type);
   return static_cast<c_bit_field_typet &>(type);
 }
 
@@ -300,13 +302,15 @@ inline bool can_cast_type<c_enum_typet>(const typet &type)
 inline const c_enum_typet &to_c_enum_type(const typet &type)
 {
   PRECONDITION(can_cast_type<c_enum_typet>(type));
+  type_with_subtypet::check(type);
   return static_cast<const c_enum_typet &>(type);
 }
 
 /// \copydoc to_c_enum_type(const typet &)
 inline c_enum_typet &to_c_enum_type(typet &type)
 {
   PRECONDITION(can_cast_type<c_enum_typet>(type));
+  type_with_subtypet::check(type);
   return static_cast<c_enum_typet &>(type);
 }
 

src/util/pointer_expr.h

@@ -54,6 +54,7 @@ class pointer_typet : public bitvector_typet
     const typet &type,
     const validation_modet vm = validation_modet::INVARIANT)
   {
+    type_with_subtypet::check(type);
     DATA_CHECK(vm, !type.get(ID_width).empty(), "pointer must have width");
   }
 };
@@ -116,6 +117,8 @@ class reference_typet : public pointer_typet
     const validation_modet vm = validation_modet::INVARIANT)
   {
     PRECONDITION(type.id() == ID_pointer);
+    DATA_CHECK(
+      vm, type.get_sub().size() == 1, "reference must have one type parameter");
     const reference_typet &reference_type =
       static_cast<const reference_typet &>(type);
     DATA_CHECK(

src/util/std_types.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 void array_typet::check(const typet &type, const validation_modet vm)
 {
   PRECONDITION(type.id() == ID_array);
+  type_with_subtypet::check(type);
   const array_typet &array_type = static_cast<const array_typet &>(type);
   if(array_type.size().is_nil())
   {

src/util/std_types.h

@@ -832,13 +832,15 @@ inline bool can_cast_type<array_typet>(const typet &type)
 inline const array_typet &to_array_type(const typet &type)
 {
   PRECONDITION(can_cast_type<array_typet>(type));
+  array_typet::check(type);
   return static_cast<const array_typet &>(type);
 }
 
 /// \copydoc to_array_type(const typet &)
 inline array_typet &to_array_type(typet &type)
 {
   PRECONDITION(can_cast_type<array_typet>(type));
+  array_typet::check(type);
   return static_cast<array_typet &>(type);
 }
 
@@ -1038,13 +1040,15 @@ inline bool can_cast_type<vector_typet>(const typet &type)
 inline const vector_typet &to_vector_type(const typet &type)
 {
   PRECONDITION(can_cast_type<vector_typet>(type));
+  type_with_subtypet::check(type);
   return static_cast<const vector_typet &>(type);
 }
 
 /// \copydoc to_vector_type(const typet &)
 inline vector_typet &to_vector_type(typet &type)
 {
   PRECONDITION(can_cast_type<vector_typet>(type));
+  type_with_subtypet::check(type);
   return static_cast<vector_typet &>(type);
 }
 
@@ -1078,13 +1082,15 @@ inline bool can_cast_type<complex_typet>(const typet &type)
 inline const complex_typet &to_complex_type(const typet &type)
 {
   PRECONDITION(can_cast_type<complex_typet>(type));
+  type_with_subtypet::check(type);
   return static_cast<const complex_typet &>(type);
 }
 
 /// \copydoc to_complex_type(const typet &)
 inline complex_typet &to_complex_type(typet &type)
 {
   PRECONDITION(can_cast_type<complex_typet>(type));
+  type_with_subtypet::check(type);
   return static_cast<complex_typet &>(type);
 }
 

src/util/type.h

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 class namespacet;
 
 #include "source_location.h"
+#include "validate.h"
 #include "validate_types.h"
 #include "validation_mode.h"
 
@@ -63,7 +64,9 @@ class typet:public irept
   { return !get_sub().empty(); }
 
   bool has_subtype() const
-  { return !get_sub().empty(); }
+  {
+    return get_sub().size() == 1;
+  }
 
   void remove_subtype()
   { get_sub().clear(); }
@@ -149,17 +152,37 @@ class type_with_subtypet:public typet
     : typet(std::move(_id), std::move(_subtype))
   {
   }
+
+  const typet &subtype() const
+  {
+    // the existence of get_sub().front() is established by check()
+    return static_cast<const typet &>(get_sub().front());
+  }
+
+  typet &subtype()
+  {
+    // the existence of get_sub().front() is established by check()
+    return static_cast<typet &>(get_sub().front());
+  }
+
+  static void check(
+    const typet &type,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    DATA_CHECK(
+      vm, type.get_sub().size() == 1, "type must have one type parameter");
+  }
 };
 
 inline const type_with_subtypet &to_type_with_subtype(const typet &type)
 {
-  PRECONDITION(type.has_subtype());
+  type_with_subtypet::check(type);
   return static_cast<const type_with_subtypet &>(type);
 }
 
 inline type_with_subtypet &to_type_with_subtype(typet &type)
 {
-  PRECONDITION(type.has_subtype());
+  type_with_subtypet::check(type);
   return static_cast<type_with_subtypet &>(type);
 }