check type invariant of type_with_subtypet

This commit does two things:

1) The type invariant of type_with_subtypet (that there is one subtype) is
now checked when casting to it.

2) The check in .subtype() that there is a subtype is removed.

Author: kroening

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);
 }