Add wellformedness checks to bitvector types in std_types

Author: danpoe

src/util/std_types.h

@@ -1149,14 +1149,34 @@ class bv_typet:public bitvector_typet
 inline const bv_typet &to_bv_type(const typet &type)
 {
   PRECONDITION(type.id()==ID_bv);
-  return static_cast<const bv_typet &>(type);
+  const bv_typet &ret = static_cast<const bv_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 /// \copydoc to_bv_type(const typet &)
 inline bv_typet &to_bv_type(typet &type)
 {
   PRECONDITION(type.id()==ID_bv);
-  return static_cast<bv_typet &>(type);
+  bv_typet &ret = static_cast<bv_typet &>(type);
+  validate_type(ret);
+  return ret;
+}
+
+/// Check whether a reference to a typet is a \ref bv_typet.
+/// \param type Source type.
+/// \return True if \param type is a \ref bv_typet.
+template <>
+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");
+  DATA_INVARIANT(
+    type.get_width() > 0, "bitvector type must have non-zero width");
 }
 
 /// Fixed-width bit-vector with unsigned binary interpretation
@@ -1186,14 +1206,35 @@ class unsignedbv_typet:public bitvector_typet
 inline const unsignedbv_typet &to_unsignedbv_type(const typet &type)
 {
   PRECONDITION(type.id()==ID_unsignedbv);
-  return static_cast<const unsignedbv_typet &>(type);
+  const unsignedbv_typet &ret = static_cast<const unsignedbv_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 /// \copydoc to_unsignedbv_type(const typet &)
 inline unsignedbv_typet &to_unsignedbv_type(typet &type)
 {
   PRECONDITION(type.id()==ID_unsignedbv);
-  return static_cast<unsignedbv_typet &>(type);
+  unsignedbv_typet &ret = static_cast<unsignedbv_typet &>(type);
+  validate_type(ret);
+  return ret;
+}
+
+/// Check whether a reference to a typet is a \ref unsignedbv_typet.
+/// \param type Source type.
+/// \return True if \param type is a \ref unsignedbv_typet.
+template <>
+inline bool can_cast_type<unsignedbv_typet>(const typet &type)
+{
+  return type.id() == ID_unsignedbv;
+}
+
+inline void validate_type(const unsignedbv_typet &type)
+{
+  DATA_INVARIANT(
+    !type.get(ID_width).empty(), "unsigned bitvector type must have width");
+  DATA_INVARIANT(
+    type.get_width() > 0, "unsigned bitvector type must have non-zero width");
 }
 
 /// Fixed-width bit-vector with two's complement interpretation
@@ -1223,14 +1264,35 @@ class signedbv_typet:public bitvector_typet
 inline const signedbv_typet &to_signedbv_type(const typet &type)
 {
   PRECONDITION(type.id()==ID_signedbv);
-  return static_cast<const signedbv_typet &>(type);
+  const signedbv_typet &ret = static_cast<const signedbv_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 /// \copydoc to_signedbv_type(const typet &)
 inline signedbv_typet &to_signedbv_type(typet &type)
 {
   PRECONDITION(type.id()==ID_signedbv);
-  return static_cast<signedbv_typet &>(type);
+  signedbv_typet &ret = static_cast<signedbv_typet &>(type);
+  validate_type(ret);
+  return ret;
+}
+
+/// Check whether a reference to a typet is a \ref signedbv_typet.
+/// \param type Source type.
+/// \return True if \param type is a \ref signedbv_typet.
+template <>
+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");
+  DATA_INVARIANT(
+    type.get_width() > 0, "signed bitvector type must have non-zero width");
 }
 
 /// Fixed-width bit-vector with signed fixed-point interpretation
@@ -1268,7 +1330,35 @@ class fixedbv_typet:public bitvector_typet
 inline const fixedbv_typet &to_fixedbv_type(const typet &type)
 {
   PRECONDITION(type.id()==ID_fixedbv);
-  return static_cast<const fixedbv_typet &>(type);
+  const fixedbv_typet &ret = static_cast<const fixedbv_typet &>(type);
+  validate_type(ret);
+  return ret;
+}
+
+/// \copydoc to_fixedbv_type(const typet &)
+inline fixedbv_typet &to_fixedbv_type(typet &type)
+{
+  PRECONDITION(type.id() == ID_fixedbv);
+  fixedbv_typet &ret = static_cast<fixedbv_typet &>(type);
+  validate_type(ret);
+  return ret;
+}
+
+/// Check whether a reference to a typet is a \ref fixedbv_typet.
+/// \param type Source type.
+/// \return True if \param type is a \ref fixedbv_typet.
+template <>
+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");
+  DATA_INVARIANT(
+    type.get_width() > 0, "fixed bitvector type must have non-zero width");
 }
 
 /// Fixed-width bit-vector with IEEE floating-point interpretation
@@ -1304,7 +1394,35 @@ class floatbv_typet:public bitvector_typet
 inline const floatbv_typet &to_floatbv_type(const typet &type)
 {
   PRECONDITION(type.id()==ID_floatbv);
-  return static_cast<const floatbv_typet &>(type);
+  const floatbv_typet &ret = static_cast<const floatbv_typet &>(type);
+  validate_type(ret);
+  return ret;
+}
+
+/// \copydoc to_floatbv_type(const typet &)
+inline floatbv_typet &to_floatbv_type(typet &type)
+{
+  PRECONDITION(type.id() == ID_floatbv);
+  floatbv_typet &ret = static_cast<floatbv_typet &>(type);
+  validate_type(ret);
+  return ret;
+}
+
+/// Check whether a reference to a typet is a \ref floatbv_typet.
+/// \param type Source type.
+/// \return True if \param type is a \ref floatbv_typet.
+template <>
+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");
+  DATA_INVARIANT(
+    type.get_width() > 0, "float bitvector type must have non-zero width");
 }
 
 /// Type for C bit fields
@@ -1471,6 +1589,21 @@ inline c_bool_typet &to_c_bool_type(typet &type)
   return static_cast<c_bool_typet &>(type);
 }
 
+/// Check whether a reference to a typet is a \ref c_bool_typet.
+/// \param type Source type.
+/// \return True if \param type is a \ref c_bool_typet.
+template <>
+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");
+  DATA_INVARIANT(type.get_width() > 0, "C bool type must have non-zero width");
+}
+
 /// String type
 ///
 /// Represents string constants, such as `@class_identifier`.