Migrate existing type checks to new framework

This removes the validate_type() methods and moves the checks into a new method
check() of the corresponding type.

Author: danpoe

src/util/expr_cast.h

@@ -54,9 +54,9 @@ inline void validate_expr(const exprt &) {}
 /// program has entered an invalid state. We validate objects at cast time as
 /// that is when these checks have been used historically, but it would be
 /// reasonable to validate objects in this way at any time.
-inline void validate_type(const typet &)
-{
-}
+//inline void validate_type(const typet &)
+//{
+//}
 
 namespace detail // NOLINT
 {
@@ -130,7 +130,7 @@ auto type_try_dynamic_cast(TType &base) ->
   if(!can_cast_type<typename std::remove_const<T>::type>(base))
     return nullptr;
   const auto ret = static_cast<returnt>(&base);
-  validate_type(*ret);
+  ret->check();
   return ret;
 }
 

src/util/std_types.h

@@ -1002,15 +1002,13 @@ inline bool can_cast_type<code_typet>(const typet &type)
 inline const code_typet &to_code_type(const typet &type)
 {
   PRECONDITION(can_cast_type<code_typet>(type));
-  validate_type(type);
   return static_cast<const code_typet &>(type);
 }
 
 /// \copydoc to_code_type(const typet &)
 inline code_typet &to_code_type(typet &type)
 {
   PRECONDITION(can_cast_type<code_typet>(type));
-  validate_type(type);
   return static_cast<code_typet &>(type);
 }
 
@@ -1205,6 +1203,11 @@ class bv_typet:public bitvector_typet
   {
     set_width(width);
   }
+
+  void check(const validation_modet vm = validation_modet::INVARIANT) const
+  {
+    DATA_CHECK(!get(ID_width).empty(), "bitvector type must have width");
+  }
 };
 
 /// Check whether a reference to a typet is a \ref bv_typet.
@@ -1216,11 +1219,6 @@ inline bool can_cast_type<bv_typet>(const typet &type)
   return type.id() == ID_bv;
 }
 
-inline void validate_type(const bv_typet &type)
-{
-  DATA_INVARIANT(!type.get(ID_width).empty(), "bitvector type must have width");
-}
-
 /// \brief Cast a typet to a \ref bv_typet
 ///
 /// This is an unchecked conversion. \a type must be known to be \ref
@@ -1233,7 +1231,7 @@ inline const bv_typet &to_bv_type(const typet &type)
 {
   PRECONDITION(can_cast_type<bv_typet>(type));
   const bv_typet &ret = static_cast<const bv_typet &>(type);
-  validate_type(ret);
+  ret.check();
   return ret;
 }
 
@@ -1242,7 +1240,7 @@ inline bv_typet &to_bv_type(typet &type)
 {
   PRECONDITION(can_cast_type<bv_typet>(type));
   bv_typet &ret = static_cast<bv_typet &>(type);
-  validate_type(ret);
+  ret.check();
   return ret;
 }
 
@@ -1316,6 +1314,11 @@ class signedbv_typet:public bitvector_typet
   constant_exprt smallest_expr() const;
   constant_exprt zero_expr() const;
   constant_exprt largest_expr() const;
+
+  void check(const validation_modet vm = validation_modet::INVARIANT) const
+  {
+    DATA_CHECK(!get(ID_width).empty(), "signed bitvector type must have width");
+  }
 };
 
 /// Check whether a reference to a typet is a \ref signedbv_typet.
@@ -1327,12 +1330,6 @@ inline bool can_cast_type<signedbv_typet>(const typet &type)
   return type.id() == ID_signedbv;
 }
 
-inline void validate_type(const signedbv_typet &type)
-{
-  DATA_INVARIANT(
-    !type.get(ID_width).empty(), "signed bitvector type must have width");
-}
-
 /// \brief Cast a typet to a \ref signedbv_typet
 ///
 /// This is an unchecked conversion. \a type must be known to be \ref
@@ -1345,7 +1342,7 @@ inline const signedbv_typet &to_signedbv_type(const typet &type)
 {
   PRECONDITION(can_cast_type<signedbv_typet>(type));
   const signedbv_typet &ret = static_cast<const signedbv_typet &>(type);
-  validate_type(ret);
+  ret.check();
   return ret;
 }
 
@@ -1354,7 +1351,7 @@ inline signedbv_typet &to_signedbv_type(typet &type)
 {
   PRECONDITION(can_cast_type<signedbv_typet>(type));
   signedbv_typet &ret = static_cast<signedbv_typet &>(type);
-  validate_type(ret);
+  ret.check();
   return ret;
 }
 
@@ -1380,6 +1377,11 @@ class fixedbv_typet:public bitvector_typet
   {
     set(ID_integer_bits, b);
   }
+
+  void check(const validation_modet vm = validation_modet::INVARIANT) const
+  {
+    DATA_CHECK(!get(ID_width).empty(), "fixed bitvector type must have width");
+  }
 };
 
 /// Check whether a reference to a typet is a \ref fixedbv_typet.
@@ -1391,12 +1393,6 @@ inline bool can_cast_type<fixedbv_typet>(const typet &type)
   return type.id() == ID_fixedbv;
 }
 
-inline void validate_type(const fixedbv_typet &type)
-{
-  DATA_INVARIANT(
-    !type.get(ID_width).empty(), "fixed bitvector type must have width");
-}
-
 /// \brief Cast a typet to a \ref fixedbv_typet
 ///
 /// This is an unchecked conversion. \a type must be known to be \ref
@@ -1409,7 +1405,7 @@ inline const fixedbv_typet &to_fixedbv_type(const typet &type)
 {
   PRECONDITION(can_cast_type<fixedbv_typet>(type));
   const fixedbv_typet &ret = static_cast<const fixedbv_typet &>(type);
-  validate_type(ret);
+  ret.check();
   return ret;
 }
 
@@ -1418,7 +1414,7 @@ inline fixedbv_typet &to_fixedbv_type(typet &type)
 {
   PRECONDITION(can_cast_type<fixedbv_typet>(type));
   fixedbv_typet &ret = static_cast<fixedbv_typet &>(type);
-  validate_type(ret);
+  ret.check();
   return ret;
 }
 
@@ -1442,6 +1438,11 @@ class floatbv_typet:public bitvector_typet
   {
     set(ID_f, b);
   }
+
+  void check(const validation_modet vm = validation_modet::INVARIANT) const
+  {
+    DATA_CHECK(!get(ID_width).empty(), "float bitvector type must have width");
+  }
 };
 
 /// Check whether a reference to a typet is a \ref floatbv_typet.
@@ -1453,12 +1454,6 @@ inline bool can_cast_type<floatbv_typet>(const typet &type)
   return type.id() == ID_floatbv;
 }
 
-inline void validate_type(const floatbv_typet &type)
-{
-  DATA_INVARIANT(
-    !type.get(ID_width).empty(), "float bitvector type must have width");
-}
-
 /// \brief Cast a typet to a \ref floatbv_typet
 ///
 /// This is an unchecked conversion. \a type must be known to be \ref
@@ -1471,7 +1466,7 @@ inline const floatbv_typet &to_floatbv_type(const typet &type)
 {
   PRECONDITION(can_cast_type<floatbv_typet>(type));
   const floatbv_typet &ret = static_cast<const floatbv_typet &>(type);
-  validate_type(ret);
+  ret.check();
   return ret;
 }
 
@@ -1480,7 +1475,7 @@ inline floatbv_typet &to_floatbv_type(typet &type)
 {
   PRECONDITION(can_cast_type<floatbv_typet>(type));
   floatbv_typet &ret = static_cast<floatbv_typet &>(type);
-  validate_type(ret);
+  ret.check();
   return ret;
 }
 
@@ -1539,6 +1534,11 @@ class pointer_typet:public bitvector_typet
   {
     return signedbv_typet(get_width());
   }
+
+  void check(const validation_modet vm = validation_modet::INVARIANT) const
+  {
+    DATA_CHECK(!get(ID_width).empty(), "pointer must have width");
+  }
 };
 
 /// Check whether a reference to a typet is a \ref pointer_typet.
@@ -1550,11 +1550,6 @@ inline bool can_cast_type<pointer_typet>(const typet &type)
   return type.id() == ID_pointer;
 }
 
-inline void validate_type(const pointer_typet &type)
-{
-  DATA_INVARIANT(!type.get(ID_width).empty(), "pointer must have width");
-}
-
 /// \brief Cast a typet to a \ref pointer_typet
 ///
 /// This is an unchecked conversion. \a type must be known to be \ref
@@ -1567,7 +1562,7 @@ inline const pointer_typet &to_pointer_type(const typet &type)
 {
   PRECONDITION(can_cast_type<pointer_typet>(type));
   const pointer_typet &ret = static_cast<const pointer_typet &>(type);
-  validate_type(ret);
+  ret.check();
   return ret;
 }
 
@@ -1576,7 +1571,7 @@ inline pointer_typet &to_pointer_type(typet &type)
 {
   PRECONDITION(can_cast_type<pointer_typet>(type));
   pointer_typet &ret = static_cast<pointer_typet &>(type);
-  validate_type(ret);
+  ret.check();
   return ret;
 }
 
@@ -1641,6 +1636,11 @@ class c_bool_typet:public bitvector_typet
     bitvector_typet(ID_c_bool, width)
   {
   }
+
+  void check(const validation_modet vm = validation_modet::INVARIANT) const
+  {
+    DATA_CHECK(!get(ID_width).empty(), "C bool type must have width");
+  }
 };
 
 /// Check whether a reference to a typet is a \ref c_bool_typet.
@@ -1652,11 +1652,6 @@ inline bool can_cast_type<c_bool_typet>(const typet &type)
   return type.id() == ID_c_bool;
 }
 
-inline void validate_type(const c_bool_typet &type)
-{
-  DATA_INVARIANT(!type.get(ID_width).empty(), "C bool type must have width");
-}
-
 /// \brief Cast a typet to a \ref c_bool_typet
 ///
 /// This is an unchecked conversion. \a type must be known to be \ref
@@ -1669,7 +1664,7 @@ inline const c_bool_typet &to_c_bool_type(const typet &type)
 {
   PRECONDITION(can_cast_type<c_bool_typet>(type));
   const c_bool_typet &ret = static_cast<const c_bool_typet &>(type);
-  validate_type(ret);
+  ret.check();
   return ret;
 }
 
@@ -1678,7 +1673,7 @@ inline c_bool_typet &to_c_bool_type(typet &type)
 {
   PRECONDITION(can_cast_type<c_bool_typet>(type));
   c_bool_typet &ret = static_cast<c_bool_typet &>(type);
-  validate_type(ret);
+  ret.check();
   return ret;
 }
 

src/util/validate_types.cpp

@@ -23,14 +23,34 @@ Author: Daniel Poetzl
 template <template <typename> class C, typename... Args>
 void call_on_type(const typet &type, Args &&... args)
 {
-  if(type.id() == ID_signedbv)
+  if(type.id() == ID_bv)
   {
-    CALL_ON_TYPE(signedbv_typet);
+    CALL_ON_TYPE(bv_typet);
   }
   else if(type.id() == ID_unsignedbv)
   {
     CALL_ON_TYPE(unsignedbv_typet);
   }
+  else if(type.id() == ID_signedbv)
+  {
+    CALL_ON_TYPE(signedbv_typet);
+  }
+  else if(type.id() == ID_fixedbv)
+  {
+    CALL_ON_TYPE(fixedbv_typet);
+  }
+  else if(type.id() == ID_floatbv)
+  {
+    CALL_ON_TYPE(floatbv_typet);
+  }
+  else if(type.id() == ID_pointer)
+  {
+    CALL_ON_TYPE(pointer_typet);
+  }
+  else if(type.id() == ID_c_bool)
+  {
+    CALL_ON_TYPE(c_bool_typet);
+  }
   else
   {
 #ifdef REPORT_UNIMPLEMENTED_TYPE_CHECKS