Merge pull request #7561 from diffblue/remove_typet_subtype

remove typet::subtype()

Author: kroening

src/cpp/cpp_template_type.h

@@ -34,7 +34,17 @@ class template_typet:public typet
     return (const template_parameterst &)find(ID_template_parameters).get_sub();
   }
 
-  using typet::subtype;
+  const typet &subtype() const
+  {
+    if(get_sub().empty())
+      return static_cast<const typet &>(get_nil_irep());
+    return static_cast<const typet &>(get_sub().front());
+  }
+
+  typet &subtype()
+  {
+    return add_subtype();
+  }
 };
 
 inline template_typet &to_template_type(typet &type)

src/util/c_types.h

@@ -22,7 +22,7 @@ class c_bit_field_typet : public bitvector_typet
   explicit c_bit_field_typet(typet _subtype, std::size_t width)
     : bitvector_typet(ID_c_bit_field, width)
   {
-    subtype().swap(_subtype);
+    add_subtype() = std::move(_subtype);
   }
 
   // These have a sub-type. The preferred way to access it
@@ -36,6 +36,28 @@ class c_bit_field_typet : public bitvector_typet
   {
     return subtype();
   }
+
+  // Use .underlying_type() instead -- this method will be removed
+  const typet &subtype() const
+  {
+    // The existence of get_sub() front is enforced by check(...)
+    return static_cast<const typet &>(get_sub().front());
+  }
+
+  // Use .underlying_type() instead -- this method will be removed
+  typet &subtype()
+  {
+    // The existence of get_sub() front is enforced by check(...)
+    return static_cast<typet &>(get_sub().front());
+  }
+
+  static void check(
+    const typet &type,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    bitvector_typet::check(type, vm);
+    type_with_subtypet::check(type, vm);
+  }
 };
 
 /// Check whether a reference to a typet is a \ref c_bit_field_typet.
@@ -58,7 +80,7 @@ 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);
+  c_bit_field_typet::check(type);
   return static_cast<const c_bit_field_typet &>(type);
 }
 

src/util/pointer_expr.h

@@ -26,7 +26,7 @@ class pointer_typet : public bitvector_typet
   pointer_typet(typet _base_type, std::size_t width)
     : bitvector_typet(ID_pointer, width)
   {
-    subtype().swap(_base_type);
+    add_subtype() = std::move(_base_type);
   }
 
   /// The type of the data what we point to.
@@ -45,6 +45,20 @@ class pointer_typet : public bitvector_typet
     return subtype();
   }
 
+  // Use .base_type() instead -- this method will be removed
+  const typet &subtype() const
+  {
+    // The existence of get_sub() front is enforced by check(...)
+    return static_cast<const typet &>(get_sub().front());
+  }
+
+  // Use .base_type() instead -- this method will be removed
+  typet &subtype()
+  {
+    // The existence of get_sub() front is enforced by check(...)
+    return static_cast<typet &>(get_sub().front());
+  }
+
   signedbv_typet difference_type() const
   {
     return signedbv_typet(get_width());
@@ -54,8 +68,8 @@ class pointer_typet : public bitvector_typet
     const typet &type,
     const validation_modet vm = validation_modet::INVARIANT)
   {
+    bitvector_typet::check(type, vm);
     type_with_subtypet::check(type);
-    DATA_CHECK(vm, !type.get(ID_width).empty(), "pointer must have width");
   }
 };
 

src/util/type.h

@@ -41,28 +41,10 @@ class typet:public irept
 #else
   typet(irep_idt _id, typet _subtype) : irept(std::move(_id))
   {
-    subtype() = std::move(_subtype);
+    add_subtype() = std::move(_subtype);
   }
 #endif
 
-  // Deliberately protected -- use type-specific accessor methods instead.
-protected:
-  const typet &subtype() const
-  {
-    if(get_sub().empty())
-      return static_cast<const typet &>(get_nil_irep());
-    return static_cast<const typet &>(get_sub().front());
-  }
-
-  typet &subtype()
-  {
-    subt &sub=get_sub();
-    if(sub.empty())
-      sub.resize(1);
-    return static_cast<typet &>(sub.front());
-  }
-
-public:
   // This method allows the construction of a type with a subtype by
   // starting from a type without subtype.  It avoids copying the contents
   // of the type.  The primary use-case are parsers, where a copy could be