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

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