Merge pull request #3147 from danpoe/refactor/use-validation-methods-in-std-types

Move existing type validation checks to new framework

Author: tautschnig

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
 {
 
@@ -155,9 +145,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);
 }
 
 /// \brief Try to cast a generic typet to a specific derived class.

src/util/std_types.h

@@ -968,15 +968,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);
 }
 
@@ -1125,6 +1125,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.
@@ -1136,11 +1143,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
@@ -1152,18 +1154,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
@@ -1235,6 +1235,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.
@@ -1246,12 +1254,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
@@ -1263,18 +1265,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
@@ -1299,6 +1299,14 @@ class fixedbv_typet:public bitvector_typet
   {
     set(ID_integer_bits, narrow_cast<long long>(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.
@@ -1310,12 +1318,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
@@ -1327,18 +1329,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
@@ -1361,6 +1361,14 @@ class floatbv_typet:public bitvector_typet
   {
     set(ID_f, narrow_cast<long long>(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.
@@ -1372,12 +1380,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
@@ -1389,18 +1391,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
@@ -1464,6 +1464,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.
@@ -1475,11 +1482,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
@@ -1491,18 +1493,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
@@ -1562,6 +1562,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.
@@ -1573,11 +1580,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
@@ -1589,18 +1591,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