Add wellformedness checks to bitvector types in std_types

Author: danpoe

src/util/std_types.h

@@ -1196,6 +1196,13 @@ 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");
+}
+
 /// \brief Cast a typet to a \ref bv_typet
 ///
 /// This is an unchecked conversion. \a type must be known to be \ref
@@ -1207,14 +1214,18 @@ inline bool can_cast_type<bv_typet>(const typet &type)
 inline const bv_typet &to_bv_type(const typet &type)
 {
   PRECONDITION(can_cast_type<bv_typet>(type));
-  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(can_cast_type<bv_typet>(type));
-  return static_cast<bv_typet &>(type);
+  bv_typet &ret = static_cast<bv_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 /// Fixed-width bit-vector with unsigned binary interpretation
@@ -1242,6 +1253,14 @@ 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");
+}
+
 /// \brief Cast a typet to an \ref unsignedbv_typet
 ///
 /// This is an unchecked conversion. \a type must be known to be \ref
@@ -1253,14 +1272,18 @@ inline bool can_cast_type<unsignedbv_typet>(const typet &type)
 inline const unsignedbv_typet &to_unsignedbv_type(const typet &type)
 {
   PRECONDITION(can_cast_type<unsignedbv_typet>(type));
-  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(can_cast_type<unsignedbv_typet>(type));
-  return static_cast<unsignedbv_typet &>(type);
+  unsignedbv_typet &ret = static_cast<unsignedbv_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 /// Fixed-width bit-vector with two's complement interpretation
@@ -1288,6 +1311,14 @@ 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");
+}
+
 /// \brief Cast a typet to a \ref signedbv_typet
 ///
 /// This is an unchecked conversion. \a type must be known to be \ref
@@ -1299,14 +1330,18 @@ inline bool can_cast_type<signedbv_typet>(const typet &type)
 inline const signedbv_typet &to_signedbv_type(const typet &type)
 {
   PRECONDITION(can_cast_type<signedbv_typet>(type));
-  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(can_cast_type<signedbv_typet>(type));
-  return static_cast<signedbv_typet &>(type);
+  signedbv_typet &ret = static_cast<signedbv_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 /// Fixed-width bit-vector with signed fixed-point interpretation
@@ -1342,6 +1377,14 @@ 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");
+}
+
 /// \brief Cast a typet to a \ref fixedbv_typet
 ///
 /// This is an unchecked conversion. \a type must be known to be \ref
@@ -1353,14 +1396,18 @@ inline bool can_cast_type<fixedbv_typet>(const typet &type)
 inline const fixedbv_typet &to_fixedbv_type(const typet &type)
 {
   PRECONDITION(can_cast_type<fixedbv_typet>(type));
-  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(can_cast_type<fixedbv_typet>(type));
-  return static_cast<fixedbv_typet &>(type);
+  fixedbv_typet &ret = static_cast<fixedbv_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 /// Fixed-width bit-vector with IEEE floating-point interpretation
@@ -1394,6 +1441,14 @@ 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");
+}
+
 /// \brief Cast a typet to a \ref floatbv_typet
 ///
 /// This is an unchecked conversion. \a type must be known to be \ref
@@ -1405,14 +1460,18 @@ inline bool can_cast_type<floatbv_typet>(const typet &type)
 inline const floatbv_typet &to_floatbv_type(const typet &type)
 {
   PRECONDITION(can_cast_type<floatbv_typet>(type));
-  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(can_cast_type<floatbv_typet>(type));
-  return static_cast<floatbv_typet &>(type);
+  floatbv_typet &ret = static_cast<floatbv_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 /// Type for C bit fields
@@ -1481,6 +1540,11 @@ 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
@@ -1506,12 +1570,6 @@ inline pointer_typet &to_pointer_type(typet &type)
   return ret;
 }
 
-inline void validate_type(const pointer_typet &type)
-{
-  DATA_INVARIANT(!type.get(ID_width).empty(), "pointer must have width");
-  DATA_INVARIANT(type.get_width() > 0, "pointer must have non-zero width");
-}
-
 /// The reference type
 ///
 /// Intends to model C++ reference. Comparing to \ref pointer_typet should
@@ -1584,6 +1642,12 @@ 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");
+}
+
 /// \brief Cast a typet to a \ref c_bool_typet
 ///
 /// This is an unchecked conversion. \a type must be known to be \ref
@@ -1595,14 +1659,18 @@ inline bool can_cast_type<c_bool_typet>(const typet &type)
 inline const c_bool_typet &to_c_bool_type(const typet &type)
 {
   PRECONDITION(can_cast_type<c_bool_typet>(type));
-  return static_cast<const c_bool_typet &>(type);
+  const c_bool_typet &ret = static_cast<const c_bool_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 /// \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));
-  return static_cast<c_bool_typet &>(type);
+  c_bool_typet &ret = static_cast<c_bool_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 /// String type