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

@@ -1003,15 +1003,15 @@ 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);
+  code_typet::check(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);
+  code_typet::check(type);
   return static_cast<code_typet &>(type);
 }
 
@@ -1198,6 +1198,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.
@@ -1209,11 +1216,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
@@ -1225,18 +1227,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
@@ -1308,6 +1308,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.
@@ -1319,12 +1327,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
@@ -1336,18 +1338,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
@@ -1372,6 +1372,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.
@@ -1383,12 +1391,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
@@ -1400,18 +1402,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
@@ -1434,6 +1434,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.
@@ -1445,12 +1453,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
@@ -1462,18 +1464,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
@@ -1537,6 +1537,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.
@@ -1548,11 +1555,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
@@ -1564,18 +1566,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
@@ -1635,6 +1635,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.
@@ -1646,11 +1653,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
@@ -1662,18 +1664,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

@@ -24,14 +24,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