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

@@ -48,16 +48,6 @@ inline bool can_cast_type(const typet &base);
 /// validate objects in this way at any time.
 inline void validate_expr(const exprt &) {}
 
-/// Called after casting.  Provides a point to check data invariants on the
-/// structure of the typet. By default, this is a no-op, but you can provide an
-/// overload to validate particular types. Should always succeed unless the
-/// 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 &)
-{
-}
-
 namespace detail // NOLINT
 {
 
@@ -129,9 +119,8 @@ auto type_try_dynamic_cast(TType &base) ->
     "The template argument T must be derived from typet.");
   if(!can_cast_type<typename std::remove_const<T>::type>(base))
     return nullptr;
-  const auto ret = static_cast<returnt>(&base);
-  validate_type(*ret);
-  return ret;
+  TType::check(base);
+  return static_cast<returnt>(&base);
 }
 
 namespace detail // NOLINT

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);
 }
 
@@ -1190,6 +1188,13 @@ class bv_typet:public bitvector_typet
   {
     set_width(width);
   }
+
+  static void check(
+    const typet &type,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    DATA_CHECK(!type.get(ID_width).empty(), "bitvector type must have width");
+  }
 };
 
 /// Check whether a reference to a typet is a \ref bv_typet.
@@ -1201,11 +1206,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
@@ -1217,18 +1217,16 @@ inline void validate_type(const bv_typet &type)
 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);
-  return ret;
+  bv_typet::check(type);
+  return static_cast<const bv_typet &>(type);
 }
 
 /// \copydoc to_bv_type(const typet &)
 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);
-  return ret;
+  bv_typet::check(type);
+  return static_cast<bv_typet &>(type);
 }
 
 /// Fixed-width bit-vector with unsigned binary interpretation
@@ -1301,6 +1299,14 @@ class signedbv_typet:public bitvector_typet
   constant_exprt smallest_expr() const;
   constant_exprt zero_expr() const;
   constant_exprt largest_expr() const;
+
+  static void check(
+    const typet &type,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    DATA_CHECK(
+      !type.get(ID_width).empty(), "signed bitvector type must have width");
+  }
 };
 
 /// Check whether a reference to a typet is a \ref signedbv_typet.
@@ -1312,12 +1318,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
@@ -1329,18 +1329,16 @@ inline void validate_type(const signedbv_typet &type)
 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);
-  return ret;
+  signedbv_typet::check(type);
+  return static_cast<const signedbv_typet &>(type);
 }
 
 /// \copydoc to_signedbv_type(const typet &)
 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);
-  return ret;
+  signedbv_typet::check(type);
+  return static_cast<signedbv_typet &>(type);
 }
 
 /// Fixed-width bit-vector with signed fixed-point interpretation
@@ -1365,6 +1363,14 @@ class fixedbv_typet:public bitvector_typet
   {
     set(ID_integer_bits, b);
   }
+
+  static void check(
+    const typet &type,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    DATA_CHECK(
+      !type.get(ID_width).empty(), "fixed bitvector type must have width");
+  }
 };
 
 /// Check whether a reference to a typet is a \ref fixedbv_typet.
@@ -1376,12 +1382,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
@@ -1393,18 +1393,16 @@ inline void validate_type(const fixedbv_typet &type)
 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);
-  return ret;
+  fixedbv_typet::check(type);
+  return static_cast<const fixedbv_typet &>(type);
 }
 
 /// \copydoc to_fixedbv_type(const typet &)
 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);
-  return ret;
+  fixedbv_typet::check(type);
+  return static_cast<fixedbv_typet &>(type);
 }
 
 /// Fixed-width bit-vector with IEEE floating-point interpretation
@@ -1427,6 +1425,14 @@ class floatbv_typet:public bitvector_typet
   {
     set(ID_f, b);
   }
+
+  static void check(
+    const typet &type,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    DATA_CHECK(
+      !type.get(ID_width).empty(), "float bitvector type must have width");
+  }
 };
 
 /// Check whether a reference to a typet is a \ref floatbv_typet.
@@ -1438,12 +1444,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
@@ -1455,18 +1455,16 @@ inline void validate_type(const floatbv_typet &type)
 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);
-  return ret;
+  floatbv_typet::check(type);
+  return static_cast<const floatbv_typet &>(type);
 }
 
 /// \copydoc to_floatbv_type(const typet &)
 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);
-  return ret;
+  floatbv_typet::check(type);
+  return static_cast<floatbv_typet &>(type);
 }
 
 /// Type for C bit fields
@@ -1530,6 +1528,13 @@ class pointer_typet:public bitvector_typet
   {
     return signedbv_typet(get_width());
   }
+
+  static void check(
+    const typet &type,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    DATA_CHECK(!type.get(ID_width).empty(), "pointer must have width");
+  }
 };
 
 /// Check whether a reference to a typet is a \ref pointer_typet.
@@ -1541,11 +1546,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
@@ -1557,18 +1557,16 @@ inline void validate_type(const pointer_typet &type)
 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);
-  return ret;
+  pointer_typet::check(type);
+  return static_cast<const pointer_typet &>(type);
 }
 
 /// \copydoc to_pointer_type(const typet &)
 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);
-  return ret;
+  pointer_typet::check(type);
+  return static_cast<pointer_typet &>(type);
 }
 
 /// The reference type
@@ -1628,6 +1626,13 @@ class c_bool_typet:public bitvector_typet
     bitvector_typet(ID_c_bool, width)
   {
   }
+
+  static void check(
+    const typet &type,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    DATA_CHECK(!type.get(ID_width).empty(), "C bool type must have width");
+  }
 };
 
 /// Check whether a reference to a typet is a \ref c_bool_typet.
@@ -1639,11 +1644,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
@@ -1655,18 +1655,16 @@ inline void validate_type(const c_bool_typet &type)
 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);
-  return ret;
+  c_bool_typet::check(type);
+  return static_cast<const c_bool_typet &>(type);
 }
 
 /// \copydoc to_c_bool_type(const typet &)
 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);
-  return ret;
+  c_bool_typet::check(type);
+  return static_cast<c_bool_typet &>(type);
 }
 
 /// String type

src/util/validate_types.cpp

@@ -23,14 +23,34 @@ Author: Daniel Poetzl
 template <template <typename, 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