type_dynamic_cast (extension of expr_cast)

src/solvers/flattening/boolbv_width.cpp

@@ -194,10 +194,7 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
     // no width
   }
   else if(type_id==ID_pointer)
-  {
-    entry.total_width=to_pointer_type(type).get_width();
-    DATA_INVARIANT(entry.total_width!=0, "pointer must have width");
-  }
+    entry.total_width = type_checked_cast<pointer_typet>(type).get_width();
   else if(type_id==ID_symbol)
     entry=get_entry(ns.follow(type));
   else if(type_id==ID_struct_tag)

src/util/expr_cast.h

@@ -29,6 +29,17 @@ Author: Nathan Phillips <[email protected]>
 /// \return true if \a base is of type \a T
 template<typename T> inline bool can_cast_expr(const exprt &base);
 
+/// \brief Check whether a reference to a generic \ref typet is of a specific
+///   derived class.
+///
+///   Implement template specializations of this function to enable casting
+///
+/// \tparam T The typet-derived class to check for
+/// \param base Reference to a generic \ref typet
+/// \return true if \a base is of type \a T
+template <typename T>
+inline bool can_cast_type(const typet &base);
+
 /// Called after casting.  Provides a point to assert on the structure of the
 /// expr. By default, this is a no-op, but you can provide an overload to
 /// validate particular types.  Should always succeed unless the program has
@@ -37,6 +48,16 @@ template<typename T> inline bool can_cast_expr(const exprt &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
 {
 
@@ -86,6 +107,33 @@ auto expr_try_dynamic_cast(TExpr &base)
   return ret;
 }
 
+/// \brief Try to cast a reference to a generic typet to a specific derived
+///    class
+/// \tparam T The reference or const reference type to \a TUnderlying to cast
+///    to
+/// \tparam TType The original type to cast from, either typet or const typet
+/// \param base Reference to a generic \ref typet
+/// \return Ptr to object of type \a TUnderlying
+///   or nullptr if \a base is not an instance of \a TUnderlying
+template <typename T, typename TType>
+auto type_try_dynamic_cast(TType &base) ->
+  typename detail::expr_try_dynamic_cast_return_typet<T, TType>::type
+{
+  typedef
+    typename detail::expr_try_dynamic_cast_return_typet<T, TType>::type returnt;
+  static_assert(
+    std::is_base_of<typet, typename std::decay<TType>::type>::value,
+    "Tried to type_try_dynamic_cast from something that wasn't an typet");
+  static_assert(
+    std::is_base_of<typet, T>::value,
+    "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;
+}
+
 namespace detail // NOLINT
 {
 
@@ -140,6 +188,21 @@ auto expr_checked_cast(TExpr &base)
   return expr_dynamic_cast<T>(base);
 }
 
+/// \brief Cast a reference to a generic typet to a specific derived class and
+///   checks that the type could be converted.
+/// \tparam T The reference or const reference type to \a TUnderlying to cast to
+/// \tparam TType The original type to cast from, either typet or const typet
+/// \param base Reference to a generic \ref typet
+/// \return Reference to object of type \a T
+template <typename T, typename TType>
+auto type_checked_cast(TType &base) ->
+  typename detail::expr_dynamic_cast_return_typet<T, TType>::type
+{
+  auto result = type_try_dynamic_cast<T>(base);
+  CHECK_RETURN(result != nullptr);
+  return *result;
+}
+
 inline void validate_operands(
   const exprt &value,
   exprt::operandst::size_type number,

src/util/std_types.h

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include "expr.h"
 #include "mp_arith.h"
 #include "invariant.h"
+#include "expr_cast.h"
 
 class constant_exprt;
 
@@ -1416,8 +1417,9 @@ class pointer_typet:public bitvector_typet
 inline const pointer_typet &to_pointer_type(const typet &type)
 {
   PRECONDITION(type.id()==ID_pointer);
-  PRECONDITION(!type.get(ID_width).empty());
-  return static_cast<const pointer_typet &>(type);
+  const pointer_typet &ret = static_cast<const pointer_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 /*! \copydoc to_pointer_type(const typet &)
@@ -1426,8 +1428,21 @@ inline const pointer_typet &to_pointer_type(const typet &type)
 inline pointer_typet &to_pointer_type(typet &type)
 {
   PRECONDITION(type.id()==ID_pointer);
-  PRECONDITION(!type.get(ID_width).empty());
-  return static_cast<pointer_typet &>(type);
+  pointer_typet &ret = static_cast<pointer_typet &>(type);
+  validate_type(ret);
+  return ret;
+}
+
+template <>
+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");
+  DATA_INVARIANT(type.get_width() > 0, "pointer must have non-zero width");
 }
 
 /*! \brief The reference type