From de8a8d00c60961c22da65ba38eac138a492421cc Mon Sep 17 00:00:00 2001
From: Nathan Phillips <nathan.phillips@diffblue.com>
Date: Wed, 23 Aug 2017 11:05:57 +0100
Subject: [PATCH 1/8] Implementation of expr_dynamic_cast

---
 src/util/expr_cast.h                         | 140 ++++
 src/util/std_expr.h                          | 639 +++++++++++++++++++
 unit/Makefile                                |   1 +
 unit/util/expr_cast/expr_cast.cpp            |  86 +++
 unit/util/expr_cast/expr_undefined_casts.cpp |  49 ++
 5 files changed, 915 insertions(+)
 create mode 100644 src/util/expr_cast.h
 create mode 100644 unit/util/expr_cast/expr_cast.cpp
 create mode 100644 unit/util/expr_cast/expr_undefined_casts.cpp

diff --git a/src/util/expr_cast.h b/src/util/expr_cast.h
new file mode 100644
index 00000000000..d76361e01fd
--- /dev/null
+++ b/src/util/expr_cast.h
@@ -0,0 +1,140 @@
+/*
+  Author: Nathan Phillips <Nathan.Phillips@diffblue.com>
+*/
+
+#ifndef CPROVER_UTIL_EXPR_CAST_H
+#define CPROVER_UTIL_EXPR_CAST_H
+
+/// \file util/expr_cast.h
+/// \brief Templated functions to cast to specific exprt-derived classes
+
+#include <typeinfo>
+#include "invariant.h"
+#include "expr.h"
+
+
+/// \brief Check whether a reference to a generic \ref exprt is of a specific derived class
+///   Implement template specializations of this function to enable casting
+/// \tparam T The exprt-derived class to check for
+/// \param base Reference to a generic \ref exprt
+/// \return true if \a base is of type \a T
+template<typename T> bool check_expr_type(const exprt &base);
+
+/// \brief Check whether a reference to a generic \ref exprt is of a specific derived class
+///   Implement template specializations of this function to enable casting
+/// \tparam T The exprt-derived class to check for
+/// \param base Reference to a generic \ref exprt
+/// \return true if \a base is of type \a T
+template<typename T> void validate_expr(const T &value) { }
+
+template<typename T> struct remove_constt;
+template<typename T> struct remove_constt<const T> { using type=T; };
+template<typename T> struct ptr_typet;
+template<typename T> struct ptr_typet<T *> { using type=T; };
+template<typename T> struct ref_typet;
+template<typename T> struct ref_typet<T &> { using type=T; };
+
+
+/// \brief Cast a constant pointer to a generic exprt to a specific derived class
+/// \tparam T The exprt-derived class to cast to
+/// \param base Pointer to a generic \ref exprt
+/// \return Pointer to object of type \a T or null if \a base is not an instance of \a T
+template<typename T>
+T expr_dynamic_cast(const exprt *base)
+{
+  return expr_dynamic_cast<
+    T,
+    typename remove_constt<typename ptr_typet<T>::type>::type,
+    const exprt>(base);
+}
+
+/// \brief Cast a pointer to a generic exprt to a specific derived class
+/// \tparam T The exprt-derived class to cast to
+/// \param base Pointer to a generic \ref exprt
+/// \return Pointer to object of type \a T or null if \a base is not an instance of \a T
+template<typename T>
+T expr_dynamic_cast(exprt *base)
+{
+  return expr_dynamic_cast<T, typename ptr_typet<T>::type, exprt>(base);
+}
+
+/// \brief Cast a pointer to a generic exprt to a specific derived class
+/// \tparam T The pointer or const pointer type to \a TUnderlying to cast to
+/// \tparam TUnderlying An exprt-derived class type
+/// \param base Pointer to a generic \ref exprt
+/// \return Pointer to object of type \a TUnderlying
+///   or null if \a base is not an instance of \a TUnderlying
+template<typename T, typename TUnderlying, typename TExpr>
+T expr_dynamic_cast(TExpr *base)
+{
+  static_assert(
+    std::is_base_of<exprt, TUnderlying>::value,
+    "The template argument T must be derived from exprt.");
+  if(base == nullptr)
+    return nullptr;
+  if(!check_expr_type<TUnderlying>(*base))
+    return nullptr;
+  T value=static_cast<T>(base);
+  validate_expr<TUnderlying>(*value);
+  return value;
+}
+
+/// \brief Cast a constant reference to a generic exprt to a specific derived class
+/// \tparam T The exprt-derived class to cast to
+/// \param base Reference to a generic \ref exprt
+/// \return Reference to object of type \a T
+/// \throw std::bad_cast If \a base is not an instance of \a T
+template<typename T>
+T expr_dynamic_cast(const exprt &base)
+{
+  return expr_dynamic_cast<
+    T,
+    typename remove_constt<typename ref_typet<T>::type>::type,
+    const exprt>(base);
+}
+
+/// \brief Cast a reference to a generic exprt to a specific derived class
+/// \tparam T The exprt-derived class to cast to
+/// \param base Reference to a generic \ref exprt
+/// \return Reference to object of type \a T
+/// \throw std::bad_cast If \a base is not an instance of \a T
+template<typename T>
+T expr_dynamic_cast(exprt &base)
+{
+  return expr_dynamic_cast<T, typename ref_typet<T>::type, exprt>(base);
+}
+
+/// \brief Cast a reference to a generic exprt to a specific derived class
+/// \tparam T The reference or const reference type to \a TUnderlying to cast to
+/// \tparam TUnderlying An exprt-derived class type
+/// \param base Reference to a generic \ref exprt
+/// \return Reference to object of type \a T
+/// \throw std::bad_cast If \a base is not an instance of \a TUnderlying
+template<typename T, typename TUnderlying, typename TExpr>
+T expr_dynamic_cast(TExpr &base)
+{
+  static_assert(
+    std::is_base_of<exprt, TUnderlying>::value,
+    "The template argument T must be derived from exprt.");
+  if(!check_expr_type<TUnderlying>(base))
+    throw std::bad_cast();
+  T value=static_cast<T>(base);
+  validate_expr<TUnderlying>(value);
+  return value;
+}
+
+
+inline void validate_operands(
+  const exprt &value,
+  exprt::operandst::size_type number,
+  const char *message,
+  bool allowMore=false)
+{
+  DATA_INVARIANT(
+    allowMore
+      ? value.operands().size()==number
+      : value.operands().size()>=number,
+    message);
+}
+
+#endif  // CPROVER_UTIL_EXPR_CAST_H
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index 3396398e73b..5fe5df64c91 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -19,6 +19,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "invariant.h"
 #include "std_types.h"
+#include "expr_cast.h"
+
 
 /*! \defgroup gr_std_expr Conversion to specific expressions
  *  Conversion to subclasses of @ref exprt
@@ -77,6 +79,16 @@ inline transt &to_trans_expr(exprt &expr)
   return static_cast<transt &>(expr);
 }
 
+template<> inline bool check_expr_type<transt>(const exprt &base)
+{
+  return base.id()==ID_trans;
+}
+template<> inline void validate_expr<transt>(const transt &value)
+{
+  validate_operands(value, 3, "Transition systems must have three operands");
+}
+
+
 /*! \brief Expression to hold a symbol (variable)
 */
 class symbol_exprt:public exprt
@@ -216,6 +228,16 @@ inline symbol_exprt &to_symbol_expr(exprt &expr)
   return static_cast<symbol_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<symbol_exprt>(const exprt &base)
+{
+  return base.id()==ID_symbol;
+}
+template<> inline void validate_expr<symbol_exprt>(const symbol_exprt &value)
+{
+  validate_operands(value, 0, "Symbols must not have operands");
+}
+
+
 /*! \brief Generic base class for unary expressions
 */
 class unary_exprt:public exprt
@@ -295,6 +317,12 @@ inline unary_exprt &to_unary_expr(exprt &expr)
   return static_cast<unary_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<unary_exprt>(const exprt &base)
+{
+  return base.operands().size()==1;
+}
+
+
 /*! \brief absolute value
 */
 class abs_exprt:public unary_exprt
@@ -341,6 +369,16 @@ inline abs_exprt &to_abs_expr(exprt &expr)
   return static_cast<abs_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<abs_exprt>(const exprt &base)
+{
+  return base.id()==ID_abs;
+}
+template<> inline void validate_expr<abs_exprt>(const abs_exprt &value)
+{
+  validate_operands(value, 1, "Absolute value must have one operand");
+}
+
+
 /*! \brief The unary minus expression
 */
 class unary_minus_exprt:public unary_exprt
@@ -394,6 +432,17 @@ inline unary_minus_exprt &to_unary_minus_expr(exprt &expr)
   return static_cast<unary_minus_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<unary_minus_exprt>(const exprt &base)
+{
+  return base.id()==ID_unary_minus;
+}
+template<>
+inline void validate_expr<unary_minus_exprt>(const unary_minus_exprt &value)
+{
+  validate_operands(value, 1, "Unary minus must have one operand");
+}
+
+
 /*! \brief A generic base class for expressions that are predicates,
            i.e., boolean-typed.
 */
@@ -540,6 +589,12 @@ inline binary_exprt &to_binary_expr(exprt &expr)
   return static_cast<binary_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<binary_exprt>(const exprt &base)
+{
+  return base.operands().size()==2;
+}
+
+
 /*! \brief A generic base class for expressions that are predicates,
            i.e., boolean-typed, and that take exactly two arguments.
 */
@@ -635,6 +690,12 @@ inline binary_relation_exprt &to_binary_relation_expr(exprt &expr)
   return static_cast<binary_relation_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<binary_relation_exprt>(const exprt &base)
+{
+  return check_expr_type<binary_exprt>(base);
+}
+
+
 /*! \brief A generic base class for multi-ary expressions
 */
 class multi_ary_exprt:public exprt
@@ -697,6 +758,7 @@ inline multi_ary_exprt &to_multi_ary_expr(exprt &expr)
   return static_cast<multi_ary_exprt &>(expr);
 }
 
+
 /*! \brief The plus expression
 */
 class plus_exprt:public multi_ary_exprt
@@ -753,6 +815,16 @@ inline plus_exprt &to_plus_expr(exprt &expr)
   return static_cast<plus_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<plus_exprt>(const exprt &base)
+{
+  return base.id()==ID_plus;
+}
+template<> inline void validate_expr<plus_exprt>(const plus_exprt &value)
+{
+  validate_operands(value, 2, "Plus must have two or more operands", true);
+}
+
+
 /*! \brief binary minus
 */
 class minus_exprt:public binary_exprt
@@ -801,6 +873,16 @@ inline minus_exprt &to_minus_expr(exprt &expr)
   return static_cast<minus_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<minus_exprt>(const exprt &base)
+{
+  return base.id()==ID_minus;
+}
+template<> inline void validate_expr<minus_exprt>(const minus_exprt &value)
+{
+  validate_operands(value, 2, "Minus must have two or more operands", true);
+}
+
+
 /*! \brief binary multiplication
 */
 class mult_exprt:public multi_ary_exprt
@@ -849,6 +931,16 @@ inline mult_exprt &to_mult_expr(exprt &expr)
   return static_cast<mult_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<mult_exprt>(const exprt &base)
+{
+  return base.id()==ID_mult;
+}
+template<> inline void validate_expr<mult_exprt>(const mult_exprt &value)
+{
+  validate_operands(value, 2, "Multiply must have two or more operands", true);
+}
+
+
 /*! \brief division (integer and real)
 */
 class div_exprt:public binary_exprt
@@ -897,6 +989,16 @@ inline div_exprt &to_div_expr(exprt &expr)
   return static_cast<div_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<div_exprt>(const exprt &base)
+{
+  return base.id()==ID_div;
+}
+template<> inline void validate_expr<div_exprt>(const div_exprt &value)
+{
+  validate_operands(value, 2, "Divide must have two operands");
+}
+
+
 /*! \brief binary modulo
 */
 class mod_exprt:public binary_exprt
@@ -941,6 +1043,16 @@ inline mod_exprt &to_mod_expr(exprt &expr)
   return static_cast<mod_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<mod_exprt>(const exprt &base)
+{
+  return base.id()==ID_mod;
+}
+template<> inline void validate_expr<mod_exprt>(const mod_exprt &value)
+{
+  validate_operands(value, 2, "Modulo must have two operands");
+}
+
+
 /*! \brief remainder of division
 */
 class rem_exprt:public binary_exprt
@@ -985,6 +1097,16 @@ inline rem_exprt &to_rem_expr(exprt &expr)
   return static_cast<rem_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<rem_exprt>(const exprt &base)
+{
+  return base.id()==ID_rem;
+}
+template<> inline void validate_expr<rem_exprt>(const rem_exprt &value)
+{
+  validate_operands(value, 2, "Remainder must have two operands");
+}
+
+
 /*! \brief exponentiation
  */
 class power_exprt:public binary_exprt
@@ -1029,6 +1151,16 @@ inline power_exprt &to_power_expr(exprt &expr)
   return static_cast<power_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<power_exprt>(const exprt &base)
+{
+  return base.id()==ID_power;
+}
+template<> inline void validate_expr<power_exprt>(const power_exprt &value)
+{
+  validate_operands(value, 2, "Power must have two operands");
+}
+
+
 /*! \brief falling factorial power
  */
 class factorial_power_exprt:public binary_exprt
@@ -1077,6 +1209,19 @@ inline factorial_power_exprt &to_factorial_expr(exprt &expr)
   return static_cast<factorial_power_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<factorial_power_exprt>(
+  const exprt &base)
+{
+  return base.id()==ID_factorial_power;
+}
+template<>
+inline void validate_expr<factorial_power_exprt>(
+  const factorial_power_exprt &value)
+{
+  validate_operands(value, 2, "Factorial power must have two operands");
+}
+
+
 /*! \brief equality
 */
 class equal_exprt:public binary_relation_exprt
@@ -1119,6 +1264,16 @@ inline equal_exprt &to_equal_expr(exprt &expr)
   return static_cast<equal_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<equal_exprt>(const exprt &base)
+{
+  return base.id()==ID_equal;
+}
+template<> inline void validate_expr<equal_exprt>(const equal_exprt &value)
+{
+  validate_operands(value, 2, "Equality must have two operands");
+}
+
+
 /*! \brief inequality
 */
 class notequal_exprt:public binary_relation_exprt
@@ -1165,6 +1320,17 @@ inline notequal_exprt &to_notequal_expr(exprt &expr)
   return static_cast<notequal_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<notequal_exprt>(const exprt &base)
+{
+  return base.id()==ID_notequal;
+}
+template<>
+inline void validate_expr<notequal_exprt>(const notequal_exprt &value)
+{
+  validate_operands(value, 2, "Inequality must have two operands");
+}
+
+
 /*! \brief array index operator
 */
 class index_exprt:public exprt
@@ -1247,6 +1413,16 @@ inline index_exprt &to_index_expr(exprt &expr)
   return static_cast<index_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<index_exprt>(const exprt &base)
+{
+  return base.id()==ID_index;
+}
+template<> inline void validate_expr<index_exprt>(const index_exprt &value)
+{
+  validate_operands(value, 2, "Array index must have two operands");
+}
+
+
 /*! \brief array constructor from single element
 */
 class array_of_exprt:public unary_exprt
@@ -1304,6 +1480,17 @@ inline array_of_exprt &to_array_of_expr(exprt &expr)
   return static_cast<array_of_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<array_of_exprt>(const exprt &base)
+{
+  return base.id()==ID_array_of;
+}
+template<>
+inline void validate_expr<array_of_exprt>(const array_of_exprt &value)
+{
+  validate_operands(value, 1, "'Array of' must have one operand");
+}
+
+
 /*! \brief array constructor from list of elements
 */
 class array_exprt:public exprt
@@ -1344,6 +1531,12 @@ inline array_exprt &to_array_expr(exprt &expr)
   return static_cast<array_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<array_exprt>(const exprt &base)
+{
+  return base.id()==ID_array;
+}
+
+
 /*! \brief vector constructor from list of elements
 */
 class vector_exprt:public exprt
@@ -1384,6 +1577,12 @@ inline vector_exprt &to_vector_expr(exprt &expr)
   return static_cast<vector_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<vector_exprt>(const exprt &base)
+{
+  return base.id()==ID_vector;
+}
+
+
 /*! \brief union constructor from single element
 */
 class union_exprt:public unary_exprt
@@ -1459,6 +1658,16 @@ inline union_exprt &to_union_expr(exprt &expr)
   return static_cast<union_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<union_exprt>(const exprt &base)
+{
+  return base.id()==ID_union;
+}
+template<> inline void validate_expr<union_exprt>(const union_exprt &value)
+{
+  validate_operands(value, 1, "Union constructor must have one operand");
+}
+
+
 /*! \brief struct constructor from list of elements
 */
 class struct_exprt:public exprt
@@ -1499,6 +1708,12 @@ inline struct_exprt &to_struct_expr(exprt &expr)
   return static_cast<struct_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<struct_exprt>(const exprt &base)
+{
+  return base.id()==ID_struct;
+}
+
+
 /*! \brief complex constructor from a pair of numbers
 */
 class complex_exprt:public binary_exprt
@@ -1571,6 +1786,16 @@ inline complex_exprt &to_complex_expr(exprt &expr)
   return static_cast<complex_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<complex_exprt>(const exprt &base)
+{
+  return base.id()==ID_complex;
+}
+template<> inline void validate_expr<complex_exprt>(const complex_exprt &value)
+{
+  validate_operands(value, 2, "Complex constructor must have two operands");
+}
+
+
 class namespacet;
 
 /*! \brief split an expression into a base object and a (byte) offset
@@ -1653,6 +1878,19 @@ inline object_descriptor_exprt &to_object_descriptor_expr(exprt &expr)
   return static_cast<object_descriptor_exprt &>(expr);
 }
 
+template<>
+inline bool check_expr_type<object_descriptor_exprt>(const exprt &base)
+{
+  return base.id()==ID_object_descriptor;
+}
+template<>
+inline void validate_expr<object_descriptor_exprt>(
+  const object_descriptor_exprt &value)
+{
+  validate_operands(value, 2, "Object descriptor must have two operands");
+}
+
+
 /*! \brief TO_BE_DOCUMENTED
 */
 class dynamic_object_exprt:public exprt
@@ -1720,6 +1958,18 @@ inline dynamic_object_exprt &to_dynamic_object_expr(exprt &expr)
   return static_cast<dynamic_object_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<dynamic_object_exprt>(const exprt &base)
+{
+  return base.id()==ID_dynamic_object;
+}
+template<>
+inline void validate_expr<dynamic_object_exprt>(
+  const dynamic_object_exprt &value)
+{
+  validate_operands(value, 2, "Dynamic object must have two operands");
+}
+
+
 /*! \brief semantic type conversion
 */
 class typecast_exprt:public exprt
@@ -1778,6 +2028,17 @@ inline typecast_exprt &to_typecast_expr(exprt &expr)
   return static_cast<typecast_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<typecast_exprt>(const exprt &base)
+{
+  return base.id()==ID_typecast;
+}
+template<>
+inline void validate_expr<typecast_exprt>(const typecast_exprt &value)
+{
+  validate_operands(value, 1, "Typecast must have one operand");
+}
+
+
 /*! \brief semantic type conversion from/to floating-point formats
 */
 class floatbv_typecast_exprt:public binary_exprt
@@ -1846,6 +2107,19 @@ inline floatbv_typecast_exprt &to_floatbv_typecast_expr(exprt &expr)
   return static_cast<floatbv_typecast_exprt &>(expr);
 }
 
+template<>
+inline bool check_expr_type<floatbv_typecast_exprt>(const exprt &base)
+{
+  return base.id()==ID_floatbv_typecast;
+}
+template<>
+inline void validate_expr<floatbv_typecast_exprt>(
+  const floatbv_typecast_exprt &value)
+{
+  validate_operands(value, 2, "Float typecast must have two operands");
+}
+
+
 /*! \brief boolean AND
 */
 class and_exprt:public multi_ary_exprt
@@ -1920,6 +2194,16 @@ inline and_exprt &to_and_expr(exprt &expr)
   return static_cast<and_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<and_exprt>(const exprt &base)
+{
+  return base.id()==ID_and;
+}
+// template<> inline void validate_expr<and_exprt>(const and_exprt &value)
+// {
+//   validate_operands(value, 2, "And must have two or more operands", true);
+// }
+
+
 /*! \brief boolean implication
 */
 class implies_exprt:public binary_exprt
@@ -1962,6 +2246,16 @@ inline implies_exprt &to_implies_expr(exprt &expr)
   return static_cast<implies_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<implies_exprt>(const exprt &base)
+{
+  return base.id()==ID_implies;
+}
+template<> inline void validate_expr<implies_exprt>(const implies_exprt &value)
+{
+  validate_operands(value, 2, "Implies must have two operands");
+}
+
+
 /*! \brief boolean OR
 */
 class or_exprt:public multi_ary_exprt
@@ -2036,6 +2330,16 @@ inline or_exprt &to_or_expr(exprt &expr)
   return static_cast<or_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<or_exprt>(const exprt &base)
+{
+  return base.id()==ID_or;
+}
+// template<> inline void validate_expr<or_exprt>(const or_exprt &value)
+// {
+//   validate_operands(value, 2, "Or must have two or more operands", true);
+// }
+
+
 /*! \brief Bit-wise negation of bit-vectors
 */
 class bitnot_exprt:public unary_exprt
@@ -2080,6 +2384,15 @@ inline bitnot_exprt &to_bitnot_expr(exprt &expr)
   return static_cast<bitnot_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<bitnot_exprt>(const exprt &base)
+{
+  return base.id()==ID_bitnot;
+}
+// template<> inline void validate_expr<bitnot_exprt>(const bitnot_exprt &value)
+// {
+//   validate_operands(value, 1, "Bit-wise not must have one operand");
+// }
+
 
 /*! \brief Bit-wise OR
 */
@@ -2128,6 +2441,20 @@ inline bitor_exprt &to_bitor_expr(exprt &expr)
   return static_cast<bitor_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<bitor_exprt>(const exprt &base)
+{
+  return base.id()==ID_bitor;
+}
+// template<> inline void validate_expr<bitor_exprt>(const bitor_exprt &value)
+// {
+//   validate_operands(
+//     value,
+//     2,
+//     "Bit-wise or must have two or more operands",
+//     true);
+// }
+
+
 /*! \brief Bit-wise XOR
 */
 class bitxor_exprt:public multi_ary_exprt
@@ -2174,6 +2501,20 @@ inline bitxor_exprt &to_bitxor_expr(exprt &expr)
   return static_cast<bitxor_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<bitxor_exprt>(const exprt &base)
+{
+  return base.id()==ID_bitxor;
+}
+// template<> inline void validate_expr<bitxor_exprt>(const bitxor_exprt &value)
+// {
+//   validate_operands(
+//     value,
+//     2,
+//     "Bit-wise xor must have two or more operands",
+//     true);
+// }
+
+
 /*! \brief Bit-wise AND
 */
 class bitand_exprt:public multi_ary_exprt
@@ -2221,6 +2562,20 @@ inline bitand_exprt &to_bitand_expr(exprt &expr)
   return static_cast<bitand_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<bitand_exprt>(const exprt &base)
+{
+  return base.id()==ID_bitand;
+}
+// template<> inline void validate_expr<bitand_exprt>(const bitand_exprt &value)
+// {
+//   validate_operands(
+//     value,
+//     2,
+//     "Bit-wise and must have two or more operands",
+//     true);
+// }
+
+
 /*! \brief A base class for shift operators
 */
 class shift_exprt:public binary_exprt
@@ -2295,6 +2650,16 @@ inline shift_exprt &to_shift_expr(exprt &expr)
   return static_cast<shift_exprt &>(expr);
 }
 
+// template<> inline bool check_expr_type<shift_exprt>(const exprt &base)
+// {
+//   return true;
+// }
+// template<> inline void validate_expr<shift_exprt>(const shift_exprt &value)
+// {
+//   validate_operands(value, 2, "Shifts must have two operands");
+// }
+
+
 /*! \brief Left shift
 */
 class shl_exprt:public shift_exprt
@@ -2428,6 +2793,17 @@ inline replication_exprt &to_replication_expr(exprt &expr)
   return static_cast<replication_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<replication_exprt>(const exprt &base)
+{
+  return base.id()==ID_replication;
+}
+template<>
+inline void validate_expr<replication_exprt>(const replication_exprt &value)
+{
+  validate_operands(value, 2, "Bit-wise replication must have two operands");
+}
+
+
 /*! \brief Extracts a single bit of a bit-vector operand
 */
 class extractbit_exprt:public binary_predicate_exprt
@@ -2499,6 +2875,17 @@ inline extractbit_exprt &to_extractbit_expr(exprt &expr)
   return static_cast<extractbit_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<extractbit_exprt>(const exprt &base)
+{
+  return base.id()==ID_extractbit;
+}
+template<>
+inline void validate_expr<extractbit_exprt>(const extractbit_exprt &value)
+{
+  validate_operands(value, 2, "Extract bit must have two operands");
+}
+
+
 /*! \brief Extracts a sub-range of a bit-vector operand
 */
 class extractbits_exprt:public exprt
@@ -2587,6 +2974,17 @@ inline extractbits_exprt &to_extractbits_expr(exprt &expr)
   return static_cast<extractbits_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<extractbits_exprt>(const exprt &base)
+{
+  return base.id()==ID_extractbits;
+}
+template<>
+inline void validate_expr<extractbits_exprt>(const extractbits_exprt &value)
+{
+  validate_operands(value, 3, "Extract bits must have three operands");
+}
+
+
 /*! \brief Operator to return the address of an object
 */
 class address_of_exprt:public unary_exprt
@@ -2637,6 +3035,17 @@ inline address_of_exprt &to_address_of_expr(exprt &expr)
   return static_cast<address_of_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<address_of_exprt>(const exprt &base)
+{
+  return base.id()==ID_address_of;
+}
+template<>
+inline void validate_expr<address_of_exprt>(const address_of_exprt &value)
+{
+  validate_operands(value, 1, "Address of must have one operand");
+}
+
+
 /*! \brief Boolean negation
 */
 class not_exprt:public exprt
@@ -2690,6 +3099,16 @@ inline not_exprt &to_not_expr(exprt &expr)
   return static_cast<not_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<not_exprt>(const exprt &base)
+{
+  return base.id()==ID_not;
+}
+template<> inline void validate_expr<not_exprt>(const not_exprt &value)
+{
+  validate_operands(value, 1, "Not must have one operand");
+}
+
+
 /*! \brief Operator to dereference a pointer
 */
 class dereference_exprt:public exprt
@@ -2760,6 +3179,17 @@ inline dereference_exprt &to_dereference_expr(exprt &expr)
   return static_cast<dereference_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<dereference_exprt>(const exprt &base)
+{
+  return base.id()==ID_dereference;
+}
+template<>
+inline void validate_expr<dereference_exprt>(const dereference_exprt &value)
+{
+  validate_operands(value, 1, "Dereference must have one operand");
+}
+
+
 /*! \brief The trinary if-then-else operator
 */
 class if_exprt:public exprt
@@ -2848,6 +3278,16 @@ inline if_exprt &to_if_expr(exprt &expr)
   return static_cast<if_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<if_exprt>(const exprt &base)
+{
+  return base.id()==ID_if;
+}
+template<> inline void validate_expr<if_exprt>(const if_exprt &value)
+{
+  validate_operands(value, 3, "If-then-else must have three operands");
+}
+
+
 /*! \brief Operator to update elements in structs and arrays
     \remark This expression will eventually be replaced by separate
             array and struct update operators.
@@ -2931,6 +3371,19 @@ inline with_exprt &to_with_expr(exprt &expr)
   return static_cast<with_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<with_exprt>(const exprt &base)
+{
+  return base.id()==ID_with;
+}
+template<> inline void validate_expr<with_exprt>(const with_exprt &value)
+{
+  validate_operands(
+    value,
+    3,
+    "Array/structure update must have three operands");
+}
+
+
 class index_designatort:public exprt
 {
 public:
@@ -2982,6 +3435,17 @@ inline index_designatort &to_index_designator(exprt &expr)
   return static_cast<index_designatort &>(expr);
 }
 
+template<> inline bool check_expr_type<index_designatort>(const exprt &base)
+{
+  return base.id()==ID_index_designator;
+}
+template<>
+inline void validate_expr<index_designatort>(const index_designatort &value)
+{
+  validate_operands(value, 1, "Index designator must have one operand");
+}
+
+
 class member_designatort:public exprt
 {
 public:
@@ -3028,6 +3492,17 @@ inline member_designatort &to_member_designator(exprt &expr)
   return static_cast<member_designatort &>(expr);
 }
 
+template<> inline bool check_expr_type<member_designatort>(const exprt &base)
+{
+  return base.id()==ID_member_designator;
+}
+template<>
+inline void validate_expr<member_designatort>(const member_designatort &value)
+{
+  validate_operands(value, 0, "Member designator must not have operands");
+}
+
+
 /*! \brief Operator to update elements in structs and arrays
 */
 class update_exprt:public exprt
@@ -3120,6 +3595,19 @@ inline update_exprt &to_update_expr(exprt &expr)
   return static_cast<update_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<update_exprt>(const exprt &base)
+{
+  return base.id()==ID_update;
+}
+template<> inline void validate_expr<update_exprt>(const update_exprt &value)
+{
+  validate_operands(
+    value,
+    3,
+    "Array/structure update must have three operands");
+}
+
+
 #if 0
 /*! \brief update of one element of an array
 */
@@ -3201,8 +3689,20 @@ inline array_update_exprt &to_array_update_expr(exprt &expr)
     "Array update must have three operands");
   return static_cast<array_update_exprt &>(expr);
 }
+
+template<> inline bool check_expr_type<array_update_exprt>(const exprt &base)
+{
+  return base.id()==ID_array_update;
+}
+template<>
+inline void validate_expr<array_update_exprt>(const array_update_exprt &value)
+{
+  validate_operands(value, 3, "Array update must have three operands");
+}
+
 #endif
 
+
 /*! \brief Extract member of struct or union
 */
 class member_exprt:public exprt
@@ -3325,6 +3825,16 @@ inline member_exprt &to_member_expr(exprt &expr)
   return static_cast<member_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<member_exprt>(const exprt &base)
+{
+  return base.id()==ID_member;
+}
+template<> inline void validate_expr<member_exprt>(const member_exprt &value)
+{
+  validate_operands(value, 1, "Extract member must have one operand");
+}
+
+
 /*! \brief Evaluates to true if the operand is NaN
 */
 class isnan_exprt:public unary_predicate_exprt
@@ -3367,6 +3877,16 @@ inline isnan_exprt &to_isnan_expr(exprt &expr)
   return static_cast<isnan_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<isnan_exprt>(const exprt &base)
+{
+  return base.id()==ID_isnan;
+}
+template<> inline void validate_expr<isnan_exprt>(const isnan_exprt &value)
+{
+  validate_operands(value, 1, "Is NaN must have one operand");
+}
+
+
 /*! \brief Evaluates to true if the operand is infinite
 */
 class isinf_exprt:public unary_predicate_exprt
@@ -3413,6 +3933,16 @@ inline isinf_exprt &to_isinf_expr(exprt &expr)
   return static_cast<isinf_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<isinf_exprt>(const exprt &base)
+{
+  return base.id()==ID_isinf;
+}
+template<> inline void validate_expr<isinf_exprt>(const isinf_exprt &value)
+{
+  validate_operands(value, 1, "Is infinite must have one operand");
+}
+
+
 /*! \brief Evaluates to true if the operand is finite
 */
 class isfinite_exprt:public unary_predicate_exprt
@@ -3455,6 +3985,17 @@ inline isfinite_exprt &to_isfinite_expr(exprt &expr)
   return static_cast<isfinite_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<isfinite_exprt>(const exprt &base)
+{
+  return base.id()==ID_isfinite;
+}
+template<>
+inline void validate_expr<isfinite_exprt>(const isfinite_exprt &value)
+{
+  validate_operands(value, 1, "Is finite must have one operand");
+}
+
+
 /*! \brief Evaluates to true if the operand is a normal number
 */
 class isnormal_exprt:public unary_predicate_exprt
@@ -3497,6 +4038,17 @@ inline isnormal_exprt &to_isnormal_expr(exprt &expr)
   return static_cast<isnormal_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<isnormal_exprt>(const exprt &base)
+{
+  return base.id()==ID_isnormal;
+}
+template<>
+inline void validate_expr<isnormal_exprt>(const isnormal_exprt &value)
+{
+  validate_operands(value, 1, "Is normal must have one operand");
+}
+
+
 /*! \brief IEEE-floating-point equality
 */
 class ieee_float_equal_exprt:public binary_relation_exprt
@@ -3543,6 +4095,19 @@ inline ieee_float_equal_exprt &to_ieee_float_equal_expr(exprt &expr)
   return static_cast<ieee_float_equal_exprt &>(expr);
 }
 
+template<>
+inline bool check_expr_type<ieee_float_equal_exprt>(const exprt &base)
+{
+  return base.id()==ID_ieee_float_equal;
+}
+template<>
+inline void validate_expr<ieee_float_equal_exprt>(
+  const ieee_float_equal_exprt &value)
+{
+  validate_operands(value, 2, "IEEE equality must have two operands");
+}
+
+
 /*! \brief IEEE floating-point disequality
 */
 class ieee_float_notequal_exprt:public binary_relation_exprt
@@ -3591,6 +4156,19 @@ inline ieee_float_notequal_exprt &to_ieee_float_notequal_expr(exprt &expr)
   return static_cast<ieee_float_notequal_exprt &>(expr);
 }
 
+template<>
+inline bool check_expr_type<ieee_float_notequal_exprt>(const exprt &base)
+{
+  return base.id()==ID_ieee_float_notequal;
+}
+template<>
+inline void validate_expr<ieee_float_notequal_exprt>(
+  const ieee_float_notequal_exprt &value)
+{
+  validate_operands(value, 2, "IEEE inequality must have two operands");
+}
+
+
 /*! \brief IEEE floating-point operations
 */
 class ieee_float_op_exprt:public exprt
@@ -3671,6 +4249,22 @@ inline ieee_float_op_exprt &to_ieee_float_op_expr(exprt &expr)
   return static_cast<ieee_float_op_exprt &>(expr);
 }
 
+// template<>
+// inline bool check_expr_type<ieee_float_op_exprt>(const exprt &base)
+// {
+//   return true;
+// }
+// template<>
+// inline void validate_expr<ieee_float_op_exprt>(
+//   const ieee_float_op_exprt &value)
+// {
+//   validate_operands(
+//     value,
+//     3,
+//     "IEEE float operations must have three arguments");
+// }
+
+
 /*! \brief An expression denoting a type
 */
 class type_exprt:public exprt
@@ -3743,6 +4337,12 @@ inline constant_exprt &to_constant_expr(exprt &expr)
   return static_cast<constant_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<constant_exprt>(const exprt &base)
+{
+  return base.id()==ID_constant;
+}
+
+
 /*! \brief The boolean constant true
 */
 class true_exprt:public constant_exprt
@@ -3864,6 +4464,19 @@ inline function_application_exprt &to_function_application_expr(exprt &expr)
   return static_cast<function_application_exprt &>(expr);
 }
 
+template<>
+inline bool check_expr_type<function_application_exprt>(const exprt &base)
+{
+  return base.id()==ID_function_application;
+}
+template<>
+inline void validate_expr<function_application_exprt>(
+  const function_application_exprt &value)
+{
+  validate_operands(value, 2, "Function application must have two operands");
+}
+
+
 /*! \brief Concatenation of bit-vector operands
  *
  * This expression takes any number of operands
@@ -3922,6 +4535,22 @@ inline concatenation_exprt &to_concatenation_expr(exprt &expr)
   return static_cast<concatenation_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<concatenation_exprt>(const exprt &base)
+{
+  return base.id()==ID_concatenation;
+}
+// template<>
+// inline void validate_expr<concatenation_exprt>(
+//   const concatenation_exprt &value)
+// {
+//   validate_operands(
+//     value,
+//     2,
+//     "Concatenation must have two or more operands",
+//     true);
+// }
+
+
 /*! \brief An expression denoting infinity
 */
 class infinity_exprt:public exprt
@@ -4002,6 +4631,16 @@ inline let_exprt &to_let_expr(exprt &expr)
   return static_cast<let_exprt &>(expr);
 }
 
+template<> inline bool check_expr_type<let_exprt>(const exprt &base)
+{
+  return base.id()==ID_let;
+}
+template<> inline void validate_expr<let_exprt>(const let_exprt &value)
+{
+  validate_operands(value, 3, "Let must have three operands");
+}
+
+
 /*! \brief A forall expression
 */
 class forall_exprt:public exprt
diff --git a/unit/Makefile b/unit/Makefile
index 52c60febfda..0f81813e67e 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -26,6 +26,7 @@ SRC += unit_tests.cpp \
        solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp \
        solvers/refinement/string_refinement/concretize_array.cpp \
        solvers/refinement/string_refinement/substitute_array_list.cpp \
+       util/expr_cast/expr_cast.cpp \
        util/expr_iterator.cpp \
        util/simplify_expr.cpp \
        catch_example.cpp \
diff --git a/unit/util/expr_cast/expr_cast.cpp b/unit/util/expr_cast/expr_cast.cpp
new file mode 100644
index 00000000000..728a831b8bc
--- /dev/null
+++ b/unit/util/expr_cast/expr_cast.cpp
@@ -0,0 +1,86 @@
+/*
+  Author: Nathan Phillips <Nathan.Phillips@diffblue.com>
+*/
+
+/// \file
+/// expr_dynamic_cast Unit Tests
+
+#include <catch.hpp>
+#include <util/std_expr.h>
+#include <util/std_code.h>
+#include <util/std_types.h>
+
+
+SCENARIO("expr_dynamic_cast",
+  "[core][utils][expr_cast][expr_dynamic_cast]")
+{
+  symbol_exprt symbol_expr;
+
+  GIVEN("A const exprt pointer to a symbolt")
+  {
+    const exprt *expr_ptr=&symbol_expr;
+
+    THEN("Casting from exprt pointer to symbol_exprt pointer returns non-null")
+    {
+      REQUIRE(expr_dynamic_cast<const symbol_exprt *>(expr_ptr)!=nullptr);
+    }
+
+    THEN("Casting from exprt pointer to transt pointer returns null")
+    {
+      REQUIRE(expr_dynamic_cast<const transt *>(expr_ptr)==nullptr);
+    }
+  }
+  GIVEN("A exprt pointer to a symbolt")
+  {
+    exprt *expr_ptr=&symbol_expr;
+
+    THEN("Casting from exprt pointer to symbol_exprt pointer returns non-null")
+    {
+      REQUIRE(expr_dynamic_cast<symbol_exprt *>(expr_ptr)!=nullptr);
+    }
+
+    THEN("Casting from exprt pointer to transt pointer returns null")
+    {
+      REQUIRE(expr_dynamic_cast<transt *>(expr_ptr)==nullptr);
+    }
+  }
+  GIVEN("A const exprt reference to a symbolt")
+  {
+    const exprt &expr_ref=symbol_expr;
+
+    THEN(
+      "Casting from exprt reference to symbol_exprt reference should not throw")
+    {
+      REQUIRE_NOTHROW(expr_dynamic_cast<const symbol_exprt &>(expr_ref));
+    }
+
+    THEN("Casting from exprt reference to transt reference should throw")
+    {
+      REQUIRE_THROWS_AS(
+        expr_dynamic_cast<const transt &>(expr_ref),
+        std::bad_cast);
+    }
+  }
+  GIVEN("A exprt reference to a symbolt")
+  {
+    exprt &expr_ref=symbol_expr;
+
+    THEN(
+      "Casting from exprt reference to symbol_exprt reference should not throw")
+    {
+      REQUIRE_NOTHROW(expr_dynamic_cast<symbol_exprt &>(expr_ref));
+    }
+
+    THEN("Casting from exprt reference to transt reference should throw")
+    {
+      REQUIRE_THROWS_AS(expr_dynamic_cast<transt &>(expr_ref), std::bad_cast);
+    }
+
+    THEN(
+      "Casting from non-const exprt reference to const symbol_exprt reference "
+      "should be fine")
+    {
+      REQUIRE_NOTHROW(expr_dynamic_cast<const symbol_exprt &>(expr_ref));
+    }
+  }
+}
diff --git a/unit/util/expr_cast/expr_undefined_casts.cpp b/unit/util/expr_cast/expr_undefined_casts.cpp
new file mode 100644
index 00000000000..50e3ea25a25
--- /dev/null
+++ b/unit/util/expr_cast/expr_undefined_casts.cpp
@@ -0,0 +1,49 @@
+/*
+  Author: Nathan Phillips <Nathan.Phillips@diffblue.com>
+*/
+
+/// \file
+/// expr_dynamic_cast for types that don't have a cast
+
+// This could have a unit test that consisted of trying to compile the file
+// and checking that the compiler gave the right error messages.
+
+#include <catch.hpp>
+#include <util/std_expr.h>
+#include <util/std_code.h>
+#include <util/std_types.h>
+
+
+SCENARIO("expr_dynamic_cast",
+  "[core][utils][expr_cast][expr_dynamic_cast]")
+{
+  symbol_exprt symbol_expr;
+
+  GIVEN("A const exprt pointer to a symbolt")
+  {
+    const exprt *expr_ptr=&symbol_expr;
+
+    THEN("Casting from exprt pointer to ieee_float_op_exprt should not compile")
+    {
+      // This shouldn't compile
+      expr_dynamic_cast<const ieee_float_op_exprt *>(expr_ptr);
+    }
+    THEN("Casting from exprt pointer to shift_exprt should not compile")
+    {
+      // This shouldn't compile
+      expr_dynamic_cast<const shift_exprt *>(expr_ptr);
+    }
+    THEN(
+      "Casting from exprt pointer to non-pointer/reference should not compile")
+    {
+      // This shouldn't compile
+      expr_dynamic_cast<symbol_exprt>(expr_ptr);
+    }
+    THEN(
+      "Casting from const exprt reference to non-const symbol_exprt reference "
+      "should not compile")
+    {
+      expr_dynamic_cast<symbol_exprt *>(expr_ptr);
+    }
+  }
+}

From d35710fcc5527e3192f3e9c60a48491287be0cf8 Mon Sep 17 00:00:00 2001
From: Nathan Phillips <nathan.phillips@diffblue.com>
Date: Wed, 23 Aug 2017 13:22:12 +0100
Subject: [PATCH 2/8] Made validate_expr non-template

---
 src/util/expr_cast.h |  28 +++++-----
 src/util/std_expr.h  | 130 +++++++++++++++++--------------------------
 2 files changed, 65 insertions(+), 93 deletions(-)

diff --git a/src/util/expr_cast.h b/src/util/expr_cast.h
index d76361e01fd..993b232739c 100644
--- a/src/util/expr_cast.h
+++ b/src/util/expr_cast.h
@@ -13,20 +13,16 @@
 #include "expr.h"
 
 
-/// \brief Check whether a reference to a generic \ref exprt is of a specific derived class
+/// \brief Check whether a reference to a generic \ref exprt is of a specific
+///   derived class.
+///
 ///   Implement template specializations of this function to enable casting
+///
 /// \tparam T The exprt-derived class to check for
 /// \param base Reference to a generic \ref exprt
 /// \return true if \a base is of type \a T
 template<typename T> bool check_expr_type(const exprt &base);
 
-/// \brief Check whether a reference to a generic \ref exprt is of a specific derived class
-///   Implement template specializations of this function to enable casting
-/// \tparam T The exprt-derived class to check for
-/// \param base Reference to a generic \ref exprt
-/// \return true if \a base is of type \a T
-template<typename T> void validate_expr(const T &value) { }
-
 template<typename T> struct remove_constt;
 template<typename T> struct remove_constt<const T> { using type=T; };
 template<typename T> struct ptr_typet;
@@ -35,10 +31,12 @@ template<typename T> struct ref_typet;
 template<typename T> struct ref_typet<T &> { using type=T; };
 
 
-/// \brief Cast a constant pointer to a generic exprt to a specific derived class
+/// \brief Cast a constant pointer to a generic exprt to a specific derived
+///   class
 /// \tparam T The exprt-derived class to cast to
 /// \param base Pointer to a generic \ref exprt
-/// \return Pointer to object of type \a T or null if \a base is not an instance of \a T
+/// \return Pointer to object of type \a T or null if \a base is not an
+///   instance of \a T
 template<typename T>
 T expr_dynamic_cast(const exprt *base)
 {
@@ -51,7 +49,8 @@ T expr_dynamic_cast(const exprt *base)
 /// \brief Cast a pointer to a generic exprt to a specific derived class
 /// \tparam T The exprt-derived class to cast to
 /// \param base Pointer to a generic \ref exprt
-/// \return Pointer to object of type \a T or null if \a base is not an instance of \a T
+/// \return Pointer to object of type \a T or null if \a base is not an
+///   instance of \a T
 template<typename T>
 T expr_dynamic_cast(exprt *base)
 {
@@ -75,11 +74,12 @@ T expr_dynamic_cast(TExpr *base)
   if(!check_expr_type<TUnderlying>(*base))
     return nullptr;
   T value=static_cast<T>(base);
-  validate_expr<TUnderlying>(*value);
+  validate_expr(*value);
   return value;
 }
 
-/// \brief Cast a constant reference to a generic exprt to a specific derived class
+/// \brief Cast a constant reference to a generic exprt to a specific derived
+///   class
 /// \tparam T The exprt-derived class to cast to
 /// \param base Reference to a generic \ref exprt
 /// \return Reference to object of type \a T
@@ -119,7 +119,7 @@ T expr_dynamic_cast(TExpr &base)
   if(!check_expr_type<TUnderlying>(base))
     throw std::bad_cast();
   T value=static_cast<T>(base);
-  validate_expr<TUnderlying>(value);
+  validate_expr(value);
   return value;
 }
 
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index 5fe5df64c91..fd68d7d4470 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -83,7 +83,7 @@ template<> inline bool check_expr_type<transt>(const exprt &base)
 {
   return base.id()==ID_trans;
 }
-template<> inline void validate_expr<transt>(const transt &value)
+inline void validate_expr(const transt &value)
 {
   validate_operands(value, 3, "Transition systems must have three operands");
 }
@@ -232,7 +232,7 @@ template<> inline bool check_expr_type<symbol_exprt>(const exprt &base)
 {
   return base.id()==ID_symbol;
 }
-template<> inline void validate_expr<symbol_exprt>(const symbol_exprt &value)
+inline void validate_expr(const symbol_exprt &value)
 {
   validate_operands(value, 0, "Symbols must not have operands");
 }
@@ -373,7 +373,7 @@ template<> inline bool check_expr_type<abs_exprt>(const exprt &base)
 {
   return base.id()==ID_abs;
 }
-template<> inline void validate_expr<abs_exprt>(const abs_exprt &value)
+inline void validate_expr(const abs_exprt &value)
 {
   validate_operands(value, 1, "Absolute value must have one operand");
 }
@@ -436,8 +436,7 @@ template<> inline bool check_expr_type<unary_minus_exprt>(const exprt &base)
 {
   return base.id()==ID_unary_minus;
 }
-template<>
-inline void validate_expr<unary_minus_exprt>(const unary_minus_exprt &value)
+inline void validate_expr(const unary_minus_exprt &value)
 {
   validate_operands(value, 1, "Unary minus must have one operand");
 }
@@ -819,7 +818,7 @@ template<> inline bool check_expr_type<plus_exprt>(const exprt &base)
 {
   return base.id()==ID_plus;
 }
-template<> inline void validate_expr<plus_exprt>(const plus_exprt &value)
+inline void validate_expr(const plus_exprt &value)
 {
   validate_operands(value, 2, "Plus must have two or more operands", true);
 }
@@ -877,7 +876,7 @@ template<> inline bool check_expr_type<minus_exprt>(const exprt &base)
 {
   return base.id()==ID_minus;
 }
-template<> inline void validate_expr<minus_exprt>(const minus_exprt &value)
+inline void validate_expr(const minus_exprt &value)
 {
   validate_operands(value, 2, "Minus must have two or more operands", true);
 }
@@ -935,7 +934,7 @@ template<> inline bool check_expr_type<mult_exprt>(const exprt &base)
 {
   return base.id()==ID_mult;
 }
-template<> inline void validate_expr<mult_exprt>(const mult_exprt &value)
+inline void validate_expr(const mult_exprt &value)
 {
   validate_operands(value, 2, "Multiply must have two or more operands", true);
 }
@@ -993,7 +992,7 @@ template<> inline bool check_expr_type<div_exprt>(const exprt &base)
 {
   return base.id()==ID_div;
 }
-template<> inline void validate_expr<div_exprt>(const div_exprt &value)
+inline void validate_expr(const div_exprt &value)
 {
   validate_operands(value, 2, "Divide must have two operands");
 }
@@ -1047,7 +1046,7 @@ template<> inline bool check_expr_type<mod_exprt>(const exprt &base)
 {
   return base.id()==ID_mod;
 }
-template<> inline void validate_expr<mod_exprt>(const mod_exprt &value)
+inline void validate_expr(const mod_exprt &value)
 {
   validate_operands(value, 2, "Modulo must have two operands");
 }
@@ -1101,7 +1100,7 @@ template<> inline bool check_expr_type<rem_exprt>(const exprt &base)
 {
   return base.id()==ID_rem;
 }
-template<> inline void validate_expr<rem_exprt>(const rem_exprt &value)
+inline void validate_expr(const rem_exprt &value)
 {
   validate_operands(value, 2, "Remainder must have two operands");
 }
@@ -1155,7 +1154,7 @@ template<> inline bool check_expr_type<power_exprt>(const exprt &base)
 {
   return base.id()==ID_power;
 }
-template<> inline void validate_expr<power_exprt>(const power_exprt &value)
+inline void validate_expr(const power_exprt &value)
 {
   validate_operands(value, 2, "Power must have two operands");
 }
@@ -1214,9 +1213,7 @@ template<> inline bool check_expr_type<factorial_power_exprt>(
 {
   return base.id()==ID_factorial_power;
 }
-template<>
-inline void validate_expr<factorial_power_exprt>(
-  const factorial_power_exprt &value)
+inline void validate_expr(const factorial_power_exprt &value)
 {
   validate_operands(value, 2, "Factorial power must have two operands");
 }
@@ -1268,7 +1265,7 @@ template<> inline bool check_expr_type<equal_exprt>(const exprt &base)
 {
   return base.id()==ID_equal;
 }
-template<> inline void validate_expr<equal_exprt>(const equal_exprt &value)
+inline void validate_expr(const equal_exprt &value)
 {
   validate_operands(value, 2, "Equality must have two operands");
 }
@@ -1324,8 +1321,7 @@ template<> inline bool check_expr_type<notequal_exprt>(const exprt &base)
 {
   return base.id()==ID_notequal;
 }
-template<>
-inline void validate_expr<notequal_exprt>(const notequal_exprt &value)
+inline void validate_expr(const notequal_exprt &value)
 {
   validate_operands(value, 2, "Inequality must have two operands");
 }
@@ -1417,7 +1413,7 @@ template<> inline bool check_expr_type<index_exprt>(const exprt &base)
 {
   return base.id()==ID_index;
 }
-template<> inline void validate_expr<index_exprt>(const index_exprt &value)
+inline void validate_expr(const index_exprt &value)
 {
   validate_operands(value, 2, "Array index must have two operands");
 }
@@ -1484,8 +1480,7 @@ template<> inline bool check_expr_type<array_of_exprt>(const exprt &base)
 {
   return base.id()==ID_array_of;
 }
-template<>
-inline void validate_expr<array_of_exprt>(const array_of_exprt &value)
+inline void validate_expr(const array_of_exprt &value)
 {
   validate_operands(value, 1, "'Array of' must have one operand");
 }
@@ -1662,7 +1657,7 @@ template<> inline bool check_expr_type<union_exprt>(const exprt &base)
 {
   return base.id()==ID_union;
 }
-template<> inline void validate_expr<union_exprt>(const union_exprt &value)
+inline void validate_expr(const union_exprt &value)
 {
   validate_operands(value, 1, "Union constructor must have one operand");
 }
@@ -1790,7 +1785,7 @@ template<> inline bool check_expr_type<complex_exprt>(const exprt &base)
 {
   return base.id()==ID_complex;
 }
-template<> inline void validate_expr<complex_exprt>(const complex_exprt &value)
+inline void validate_expr(const complex_exprt &value)
 {
   validate_operands(value, 2, "Complex constructor must have two operands");
 }
@@ -1883,9 +1878,7 @@ inline bool check_expr_type<object_descriptor_exprt>(const exprt &base)
 {
   return base.id()==ID_object_descriptor;
 }
-template<>
-inline void validate_expr<object_descriptor_exprt>(
-  const object_descriptor_exprt &value)
+inline void validate_expr(const object_descriptor_exprt &value)
 {
   validate_operands(value, 2, "Object descriptor must have two operands");
 }
@@ -1962,9 +1955,7 @@ template<> inline bool check_expr_type<dynamic_object_exprt>(const exprt &base)
 {
   return base.id()==ID_dynamic_object;
 }
-template<>
-inline void validate_expr<dynamic_object_exprt>(
-  const dynamic_object_exprt &value)
+inline void validate_expr(const dynamic_object_exprt &value)
 {
   validate_operands(value, 2, "Dynamic object must have two operands");
 }
@@ -2032,8 +2023,7 @@ template<> inline bool check_expr_type<typecast_exprt>(const exprt &base)
 {
   return base.id()==ID_typecast;
 }
-template<>
-inline void validate_expr<typecast_exprt>(const typecast_exprt &value)
+inline void validate_expr(const typecast_exprt &value)
 {
   validate_operands(value, 1, "Typecast must have one operand");
 }
@@ -2112,9 +2102,7 @@ inline bool check_expr_type<floatbv_typecast_exprt>(const exprt &base)
 {
   return base.id()==ID_floatbv_typecast;
 }
-template<>
-inline void validate_expr<floatbv_typecast_exprt>(
-  const floatbv_typecast_exprt &value)
+inline void validate_expr(const floatbv_typecast_exprt &value)
 {
   validate_operands(value, 2, "Float typecast must have two operands");
 }
@@ -2198,7 +2186,7 @@ template<> inline bool check_expr_type<and_exprt>(const exprt &base)
 {
   return base.id()==ID_and;
 }
-// template<> inline void validate_expr<and_exprt>(const and_exprt &value)
+// inline void validate_expr(const and_exprt &value)
 // {
 //   validate_operands(value, 2, "And must have two or more operands", true);
 // }
@@ -2250,7 +2238,7 @@ template<> inline bool check_expr_type<implies_exprt>(const exprt &base)
 {
   return base.id()==ID_implies;
 }
-template<> inline void validate_expr<implies_exprt>(const implies_exprt &value)
+inline void validate_expr(const implies_exprt &value)
 {
   validate_operands(value, 2, "Implies must have two operands");
 }
@@ -2334,7 +2322,7 @@ template<> inline bool check_expr_type<or_exprt>(const exprt &base)
 {
   return base.id()==ID_or;
 }
-// template<> inline void validate_expr<or_exprt>(const or_exprt &value)
+// inline void validate_expr(const or_exprt &value)
 // {
 //   validate_operands(value, 2, "Or must have two or more operands", true);
 // }
@@ -2388,7 +2376,7 @@ template<> inline bool check_expr_type<bitnot_exprt>(const exprt &base)
 {
   return base.id()==ID_bitnot;
 }
-// template<> inline void validate_expr<bitnot_exprt>(const bitnot_exprt &value)
+// inline void validate_expr(const bitnot_exprt &value)
 // {
 //   validate_operands(value, 1, "Bit-wise not must have one operand");
 // }
@@ -2445,7 +2433,7 @@ template<> inline bool check_expr_type<bitor_exprt>(const exprt &base)
 {
   return base.id()==ID_bitor;
 }
-// template<> inline void validate_expr<bitor_exprt>(const bitor_exprt &value)
+// inline void validate_expr(const bitor_exprt &value)
 // {
 //   validate_operands(
 //     value,
@@ -2505,7 +2493,7 @@ template<> inline bool check_expr_type<bitxor_exprt>(const exprt &base)
 {
   return base.id()==ID_bitxor;
 }
-// template<> inline void validate_expr<bitxor_exprt>(const bitxor_exprt &value)
+// inline void validate_expr(const bitxor_exprt &value)
 // {
 //   validate_operands(
 //     value,
@@ -2566,7 +2554,7 @@ template<> inline bool check_expr_type<bitand_exprt>(const exprt &base)
 {
   return base.id()==ID_bitand;
 }
-// template<> inline void validate_expr<bitand_exprt>(const bitand_exprt &value)
+// inline void validate_expr(const bitand_exprt &value)
 // {
 //   validate_operands(
 //     value,
@@ -2654,7 +2642,7 @@ inline shift_exprt &to_shift_expr(exprt &expr)
 // {
 //   return true;
 // }
-// template<> inline void validate_expr<shift_exprt>(const shift_exprt &value)
+// inline void validate_expr(const shift_exprt &value)
 // {
 //   validate_operands(value, 2, "Shifts must have two operands");
 // }
@@ -2797,8 +2785,7 @@ template<> inline bool check_expr_type<replication_exprt>(const exprt &base)
 {
   return base.id()==ID_replication;
 }
-template<>
-inline void validate_expr<replication_exprt>(const replication_exprt &value)
+inline void validate_expr(const replication_exprt &value)
 {
   validate_operands(value, 2, "Bit-wise replication must have two operands");
 }
@@ -2879,8 +2866,7 @@ template<> inline bool check_expr_type<extractbit_exprt>(const exprt &base)
 {
   return base.id()==ID_extractbit;
 }
-template<>
-inline void validate_expr<extractbit_exprt>(const extractbit_exprt &value)
+inline void validate_expr(const extractbit_exprt &value)
 {
   validate_operands(value, 2, "Extract bit must have two operands");
 }
@@ -2978,8 +2964,7 @@ template<> inline bool check_expr_type<extractbits_exprt>(const exprt &base)
 {
   return base.id()==ID_extractbits;
 }
-template<>
-inline void validate_expr<extractbits_exprt>(const extractbits_exprt &value)
+inline void validate_expr(const extractbits_exprt &value)
 {
   validate_operands(value, 3, "Extract bits must have three operands");
 }
@@ -3039,8 +3024,7 @@ template<> inline bool check_expr_type<address_of_exprt>(const exprt &base)
 {
   return base.id()==ID_address_of;
 }
-template<>
-inline void validate_expr<address_of_exprt>(const address_of_exprt &value)
+inline void validate_expr(const address_of_exprt &value)
 {
   validate_operands(value, 1, "Address of must have one operand");
 }
@@ -3103,7 +3087,7 @@ template<> inline bool check_expr_type<not_exprt>(const exprt &base)
 {
   return base.id()==ID_not;
 }
-template<> inline void validate_expr<not_exprt>(const not_exprt &value)
+inline void validate_expr(const not_exprt &value)
 {
   validate_operands(value, 1, "Not must have one operand");
 }
@@ -3183,8 +3167,7 @@ template<> inline bool check_expr_type<dereference_exprt>(const exprt &base)
 {
   return base.id()==ID_dereference;
 }
-template<>
-inline void validate_expr<dereference_exprt>(const dereference_exprt &value)
+inline void validate_expr(const dereference_exprt &value)
 {
   validate_operands(value, 1, "Dereference must have one operand");
 }
@@ -3282,7 +3265,7 @@ template<> inline bool check_expr_type<if_exprt>(const exprt &base)
 {
   return base.id()==ID_if;
 }
-template<> inline void validate_expr<if_exprt>(const if_exprt &value)
+inline void validate_expr(const if_exprt &value)
 {
   validate_operands(value, 3, "If-then-else must have three operands");
 }
@@ -3375,7 +3358,7 @@ template<> inline bool check_expr_type<with_exprt>(const exprt &base)
 {
   return base.id()==ID_with;
 }
-template<> inline void validate_expr<with_exprt>(const with_exprt &value)
+inline void validate_expr(const with_exprt &value)
 {
   validate_operands(
     value,
@@ -3439,8 +3422,7 @@ template<> inline bool check_expr_type<index_designatort>(const exprt &base)
 {
   return base.id()==ID_index_designator;
 }
-template<>
-inline void validate_expr<index_designatort>(const index_designatort &value)
+inline void validate_expr(const index_designatort &value)
 {
   validate_operands(value, 1, "Index designator must have one operand");
 }
@@ -3496,8 +3478,7 @@ template<> inline bool check_expr_type<member_designatort>(const exprt &base)
 {
   return base.id()==ID_member_designator;
 }
-template<>
-inline void validate_expr<member_designatort>(const member_designatort &value)
+inline void validate_expr(const member_designatort &value)
 {
   validate_operands(value, 0, "Member designator must not have operands");
 }
@@ -3599,7 +3580,7 @@ template<> inline bool check_expr_type<update_exprt>(const exprt &base)
 {
   return base.id()==ID_update;
 }
-template<> inline void validate_expr<update_exprt>(const update_exprt &value)
+inline void validate_expr(const update_exprt &value)
 {
   validate_operands(
     value,
@@ -3694,8 +3675,7 @@ template<> inline bool check_expr_type<array_update_exprt>(const exprt &base)
 {
   return base.id()==ID_array_update;
 }
-template<>
-inline void validate_expr<array_update_exprt>(const array_update_exprt &value)
+inline void validate_expr(const array_update_exprt &value)
 {
   validate_operands(value, 3, "Array update must have three operands");
 }
@@ -3829,7 +3809,7 @@ template<> inline bool check_expr_type<member_exprt>(const exprt &base)
 {
   return base.id()==ID_member;
 }
-template<> inline void validate_expr<member_exprt>(const member_exprt &value)
+inline void validate_expr(const member_exprt &value)
 {
   validate_operands(value, 1, "Extract member must have one operand");
 }
@@ -3881,7 +3861,7 @@ template<> inline bool check_expr_type<isnan_exprt>(const exprt &base)
 {
   return base.id()==ID_isnan;
 }
-template<> inline void validate_expr<isnan_exprt>(const isnan_exprt &value)
+inline void validate_expr(const isnan_exprt &value)
 {
   validate_operands(value, 1, "Is NaN must have one operand");
 }
@@ -3937,7 +3917,7 @@ template<> inline bool check_expr_type<isinf_exprt>(const exprt &base)
 {
   return base.id()==ID_isinf;
 }
-template<> inline void validate_expr<isinf_exprt>(const isinf_exprt &value)
+inline void validate_expr(const isinf_exprt &value)
 {
   validate_operands(value, 1, "Is infinite must have one operand");
 }
@@ -3989,8 +3969,7 @@ template<> inline bool check_expr_type<isfinite_exprt>(const exprt &base)
 {
   return base.id()==ID_isfinite;
 }
-template<>
-inline void validate_expr<isfinite_exprt>(const isfinite_exprt &value)
+inline void validate_expr(const isfinite_exprt &value)
 {
   validate_operands(value, 1, "Is finite must have one operand");
 }
@@ -4042,8 +4021,7 @@ template<> inline bool check_expr_type<isnormal_exprt>(const exprt &base)
 {
   return base.id()==ID_isnormal;
 }
-template<>
-inline void validate_expr<isnormal_exprt>(const isnormal_exprt &value)
+inline void validate_expr(const isnormal_exprt &value)
 {
   validate_operands(value, 1, "Is normal must have one operand");
 }
@@ -4100,9 +4078,7 @@ inline bool check_expr_type<ieee_float_equal_exprt>(const exprt &base)
 {
   return base.id()==ID_ieee_float_equal;
 }
-template<>
-inline void validate_expr<ieee_float_equal_exprt>(
-  const ieee_float_equal_exprt &value)
+inline void validate_expr(const ieee_float_equal_exprt &value)
 {
   validate_operands(value, 2, "IEEE equality must have two operands");
 }
@@ -4161,9 +4137,7 @@ inline bool check_expr_type<ieee_float_notequal_exprt>(const exprt &base)
 {
   return base.id()==ID_ieee_float_notequal;
 }
-template<>
-inline void validate_expr<ieee_float_notequal_exprt>(
-  const ieee_float_notequal_exprt &value)
+inline void validate_expr(const ieee_float_notequal_exprt &value)
 {
   validate_operands(value, 2, "IEEE inequality must have two operands");
 }
@@ -4469,9 +4443,7 @@ inline bool check_expr_type<function_application_exprt>(const exprt &base)
 {
   return base.id()==ID_function_application;
 }
-template<>
-inline void validate_expr<function_application_exprt>(
-  const function_application_exprt &value)
+inline void validate_expr(const function_application_exprt &value)
 {
   validate_operands(value, 2, "Function application must have two operands");
 }
@@ -4635,7 +4607,7 @@ template<> inline bool check_expr_type<let_exprt>(const exprt &base)
 {
   return base.id()==ID_let;
 }
-template<> inline void validate_expr<let_exprt>(const let_exprt &value)
+inline void validate_expr(const let_exprt &value)
 {
   validate_operands(value, 3, "Let must have three operands");
 }

From 95f6505a76b654cbb6fe769f9a38b18ef0c417e5 Mon Sep 17 00:00:00 2001
From: Nathan Phillips <nathan.phillips@diffblue.com>
Date: Wed, 23 Aug 2017 13:28:42 +0100
Subject: [PATCH 3/8] Comment on types for which expr_dynamic_cast is not
 implemented

---
 src/util/std_expr.h | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index fd68d7d4470..70cb9d7bd39 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -2638,10 +2638,9 @@ inline shift_exprt &to_shift_expr(exprt &expr)
   return static_cast<shift_exprt &>(expr);
 }
 
-// template<> inline bool check_expr_type<shift_exprt>(const exprt &base)
-// {
-//   return true;
-// }
+// The to_*_expr function for this type doesn't do any checks before casting,
+// therefore the implementation is essentially a static_cast.
+// Enabling expr_dynamic_cast would hide this; instead use static_cast directly.
 // inline void validate_expr(const shift_exprt &value)
 // {
 //   validate_operands(value, 2, "Shifts must have two operands");
@@ -4223,11 +4222,9 @@ inline ieee_float_op_exprt &to_ieee_float_op_expr(exprt &expr)
   return static_cast<ieee_float_op_exprt &>(expr);
 }
 
-// template<>
-// inline bool check_expr_type<ieee_float_op_exprt>(const exprt &base)
-// {
-//   return true;
-// }
+// The to_*_expr function for this type doesn't do any checks before casting,
+// therefore the implementation is essentially a static_cast.
+// Enabling expr_dynamic_cast would hide this; instead use static_cast directly.
 // template<>
 // inline void validate_expr<ieee_float_op_exprt>(
 //   const ieee_float_op_exprt &value)

From c372eb3f36cb67df3d0ec49c5f8a02072d5deee6 Mon Sep 17 00:00:00 2001
From: Nathan Phillips <nathan.phillips@diffblue.com>
Date: Wed, 23 Aug 2017 14:03:30 +0100
Subject: [PATCH 4/8] Used typeinfo functions instead of rolling own

---
 src/util/expr_cast.h | 27 ++++++++++++++++-----------
 1 file changed, 16 insertions(+), 11 deletions(-)

diff --git a/src/util/expr_cast.h b/src/util/expr_cast.h
index 993b232739c..0497d9c6e08 100644
--- a/src/util/expr_cast.h
+++ b/src/util/expr_cast.h
@@ -23,13 +23,6 @@
 /// \return true if \a base is of type \a T
 template<typename T> bool check_expr_type(const exprt &base);
 
-template<typename T> struct remove_constt;
-template<typename T> struct remove_constt<const T> { using type=T; };
-template<typename T> struct ptr_typet;
-template<typename T> struct ptr_typet<T *> { using type=T; };
-template<typename T> struct ref_typet;
-template<typename T> struct ref_typet<T &> { using type=T; };
-
 
 /// \brief Cast a constant pointer to a generic exprt to a specific derived
 ///   class
@@ -42,7 +35,7 @@ T expr_dynamic_cast(const exprt *base)
 {
   return expr_dynamic_cast<
     T,
-    typename remove_constt<typename ptr_typet<T>::type>::type,
+    typename std::remove_const<typename std::remove_pointer<T>::type>::type,
     const exprt>(base);
 }
 
@@ -54,7 +47,10 @@ T expr_dynamic_cast(const exprt *base)
 template<typename T>
 T expr_dynamic_cast(exprt *base)
 {
-  return expr_dynamic_cast<T, typename ptr_typet<T>::type, exprt>(base);
+  return expr_dynamic_cast<
+    T,
+    typename std::remove_const<typename std::remove_pointer<T>::type>::type,
+    exprt>(base);
 }
 
 /// \brief Cast a pointer to a generic exprt to a specific derived class
@@ -66,6 +62,9 @@ T expr_dynamic_cast(exprt *base)
 template<typename T, typename TUnderlying, typename TExpr>
 T expr_dynamic_cast(TExpr *base)
 {
+  static_assert(
+    std::is_pointer<T>::value,
+    "Tried to convert exprt * to non-pointer type");
   static_assert(
     std::is_base_of<exprt, TUnderlying>::value,
     "The template argument T must be derived from exprt.");
@@ -89,7 +88,7 @@ T expr_dynamic_cast(const exprt &base)
 {
   return expr_dynamic_cast<
     T,
-    typename remove_constt<typename ref_typet<T>::type>::type,
+    typename std::remove_const<typename std::remove_reference<T>::type>::type,
     const exprt>(base);
 }
 
@@ -101,7 +100,10 @@ T expr_dynamic_cast(const exprt &base)
 template<typename T>
 T expr_dynamic_cast(exprt &base)
 {
-  return expr_dynamic_cast<T, typename ref_typet<T>::type, exprt>(base);
+  return expr_dynamic_cast<
+    T,
+    typename std::remove_const<typename std::remove_reference<T>::type>::type,
+    exprt>(base);
 }
 
 /// \brief Cast a reference to a generic exprt to a specific derived class
@@ -113,6 +115,9 @@ T expr_dynamic_cast(exprt &base)
 template<typename T, typename TUnderlying, typename TExpr>
 T expr_dynamic_cast(TExpr &base)
 {
+  static_assert(
+    std::is_reference<T>::value,
+    "Tried to convert exprt & to non-reference type");
   static_assert(
     std::is_base_of<exprt, TUnderlying>::value,
     "The template argument T must be derived from exprt.");

From 775d9dd7530f0ba500921fb70ce6787d6651b4f2 Mon Sep 17 00:00:00 2001
From: Nathan Phillips <nathan.phillips@diffblue.com>
Date: Thu, 31 Aug 2017 11:57:06 +0100
Subject: [PATCH 5/8] Renamed can_cast_expr

---
 src/util/expr_cast.h |   6 +--
 src/util/std_expr.h  | 118 +++++++++++++++++++++----------------------
 2 files changed, 62 insertions(+), 62 deletions(-)

diff --git a/src/util/expr_cast.h b/src/util/expr_cast.h
index 0497d9c6e08..13734f30d5a 100644
--- a/src/util/expr_cast.h
+++ b/src/util/expr_cast.h
@@ -21,7 +21,7 @@
 /// \tparam T The exprt-derived class to check for
 /// \param base Reference to a generic \ref exprt
 /// \return true if \a base is of type \a T
-template<typename T> bool check_expr_type(const exprt &base);
+template<typename T> bool can_cast_expr(const exprt &base);
 
 
 /// \brief Cast a constant pointer to a generic exprt to a specific derived
@@ -70,7 +70,7 @@ T expr_dynamic_cast(TExpr *base)
     "The template argument T must be derived from exprt.");
   if(base == nullptr)
     return nullptr;
-  if(!check_expr_type<TUnderlying>(*base))
+  if(!can_cast_expr<TUnderlying>(*base))
     return nullptr;
   T value=static_cast<T>(base);
   validate_expr(*value);
@@ -121,7 +121,7 @@ T expr_dynamic_cast(TExpr &base)
   static_assert(
     std::is_base_of<exprt, TUnderlying>::value,
     "The template argument T must be derived from exprt.");
-  if(!check_expr_type<TUnderlying>(base))
+  if(!can_cast_expr<TUnderlying>(base))
     throw std::bad_cast();
   T value=static_cast<T>(base);
   validate_expr(value);
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index 70cb9d7bd39..e1d6e06c912 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -79,7 +79,7 @@ inline transt &to_trans_expr(exprt &expr)
   return static_cast<transt &>(expr);
 }
 
-template<> inline bool check_expr_type<transt>(const exprt &base)
+template<> inline bool can_cast_expr<transt>(const exprt &base)
 {
   return base.id()==ID_trans;
 }
@@ -228,7 +228,7 @@ inline symbol_exprt &to_symbol_expr(exprt &expr)
   return static_cast<symbol_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<symbol_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<symbol_exprt>(const exprt &base)
 {
   return base.id()==ID_symbol;
 }
@@ -317,7 +317,7 @@ inline unary_exprt &to_unary_expr(exprt &expr)
   return static_cast<unary_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<unary_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<unary_exprt>(const exprt &base)
 {
   return base.operands().size()==1;
 }
@@ -369,7 +369,7 @@ inline abs_exprt &to_abs_expr(exprt &expr)
   return static_cast<abs_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<abs_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<abs_exprt>(const exprt &base)
 {
   return base.id()==ID_abs;
 }
@@ -432,7 +432,7 @@ inline unary_minus_exprt &to_unary_minus_expr(exprt &expr)
   return static_cast<unary_minus_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<unary_minus_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<unary_minus_exprt>(const exprt &base)
 {
   return base.id()==ID_unary_minus;
 }
@@ -588,7 +588,7 @@ inline binary_exprt &to_binary_expr(exprt &expr)
   return static_cast<binary_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<binary_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<binary_exprt>(const exprt &base)
 {
   return base.operands().size()==2;
 }
@@ -689,9 +689,9 @@ inline binary_relation_exprt &to_binary_relation_expr(exprt &expr)
   return static_cast<binary_relation_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<binary_relation_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<binary_relation_exprt>(const exprt &base)
 {
-  return check_expr_type<binary_exprt>(base);
+  return can_cast_expr<binary_exprt>(base);
 }
 
 
@@ -814,7 +814,7 @@ inline plus_exprt &to_plus_expr(exprt &expr)
   return static_cast<plus_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<plus_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<plus_exprt>(const exprt &base)
 {
   return base.id()==ID_plus;
 }
@@ -872,7 +872,7 @@ inline minus_exprt &to_minus_expr(exprt &expr)
   return static_cast<minus_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<minus_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<minus_exprt>(const exprt &base)
 {
   return base.id()==ID_minus;
 }
@@ -930,7 +930,7 @@ inline mult_exprt &to_mult_expr(exprt &expr)
   return static_cast<mult_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<mult_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<mult_exprt>(const exprt &base)
 {
   return base.id()==ID_mult;
 }
@@ -988,7 +988,7 @@ inline div_exprt &to_div_expr(exprt &expr)
   return static_cast<div_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<div_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<div_exprt>(const exprt &base)
 {
   return base.id()==ID_div;
 }
@@ -1042,7 +1042,7 @@ inline mod_exprt &to_mod_expr(exprt &expr)
   return static_cast<mod_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<mod_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<mod_exprt>(const exprt &base)
 {
   return base.id()==ID_mod;
 }
@@ -1096,7 +1096,7 @@ inline rem_exprt &to_rem_expr(exprt &expr)
   return static_cast<rem_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<rem_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<rem_exprt>(const exprt &base)
 {
   return base.id()==ID_rem;
 }
@@ -1150,7 +1150,7 @@ inline power_exprt &to_power_expr(exprt &expr)
   return static_cast<power_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<power_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<power_exprt>(const exprt &base)
 {
   return base.id()==ID_power;
 }
@@ -1208,7 +1208,7 @@ inline factorial_power_exprt &to_factorial_expr(exprt &expr)
   return static_cast<factorial_power_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<factorial_power_exprt>(
+template<> inline bool can_cast_expr<factorial_power_exprt>(
   const exprt &base)
 {
   return base.id()==ID_factorial_power;
@@ -1261,7 +1261,7 @@ inline equal_exprt &to_equal_expr(exprt &expr)
   return static_cast<equal_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<equal_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<equal_exprt>(const exprt &base)
 {
   return base.id()==ID_equal;
 }
@@ -1317,7 +1317,7 @@ inline notequal_exprt &to_notequal_expr(exprt &expr)
   return static_cast<notequal_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<notequal_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<notequal_exprt>(const exprt &base)
 {
   return base.id()==ID_notequal;
 }
@@ -1409,7 +1409,7 @@ inline index_exprt &to_index_expr(exprt &expr)
   return static_cast<index_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<index_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<index_exprt>(const exprt &base)
 {
   return base.id()==ID_index;
 }
@@ -1476,7 +1476,7 @@ inline array_of_exprt &to_array_of_expr(exprt &expr)
   return static_cast<array_of_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<array_of_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<array_of_exprt>(const exprt &base)
 {
   return base.id()==ID_array_of;
 }
@@ -1526,7 +1526,7 @@ inline array_exprt &to_array_expr(exprt &expr)
   return static_cast<array_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<array_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<array_exprt>(const exprt &base)
 {
   return base.id()==ID_array;
 }
@@ -1572,7 +1572,7 @@ inline vector_exprt &to_vector_expr(exprt &expr)
   return static_cast<vector_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<vector_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<vector_exprt>(const exprt &base)
 {
   return base.id()==ID_vector;
 }
@@ -1653,7 +1653,7 @@ inline union_exprt &to_union_expr(exprt &expr)
   return static_cast<union_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<union_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<union_exprt>(const exprt &base)
 {
   return base.id()==ID_union;
 }
@@ -1703,7 +1703,7 @@ inline struct_exprt &to_struct_expr(exprt &expr)
   return static_cast<struct_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<struct_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<struct_exprt>(const exprt &base)
 {
   return base.id()==ID_struct;
 }
@@ -1781,7 +1781,7 @@ inline complex_exprt &to_complex_expr(exprt &expr)
   return static_cast<complex_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<complex_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<complex_exprt>(const exprt &base)
 {
   return base.id()==ID_complex;
 }
@@ -1874,7 +1874,7 @@ inline object_descriptor_exprt &to_object_descriptor_expr(exprt &expr)
 }
 
 template<>
-inline bool check_expr_type<object_descriptor_exprt>(const exprt &base)
+inline bool can_cast_expr<object_descriptor_exprt>(const exprt &base)
 {
   return base.id()==ID_object_descriptor;
 }
@@ -1951,7 +1951,7 @@ inline dynamic_object_exprt &to_dynamic_object_expr(exprt &expr)
   return static_cast<dynamic_object_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<dynamic_object_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<dynamic_object_exprt>(const exprt &base)
 {
   return base.id()==ID_dynamic_object;
 }
@@ -2019,7 +2019,7 @@ inline typecast_exprt &to_typecast_expr(exprt &expr)
   return static_cast<typecast_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<typecast_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<typecast_exprt>(const exprt &base)
 {
   return base.id()==ID_typecast;
 }
@@ -2098,7 +2098,7 @@ inline floatbv_typecast_exprt &to_floatbv_typecast_expr(exprt &expr)
 }
 
 template<>
-inline bool check_expr_type<floatbv_typecast_exprt>(const exprt &base)
+inline bool can_cast_expr<floatbv_typecast_exprt>(const exprt &base)
 {
   return base.id()==ID_floatbv_typecast;
 }
@@ -2182,7 +2182,7 @@ inline and_exprt &to_and_expr(exprt &expr)
   return static_cast<and_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<and_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<and_exprt>(const exprt &base)
 {
   return base.id()==ID_and;
 }
@@ -2234,7 +2234,7 @@ inline implies_exprt &to_implies_expr(exprt &expr)
   return static_cast<implies_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<implies_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<implies_exprt>(const exprt &base)
 {
   return base.id()==ID_implies;
 }
@@ -2318,7 +2318,7 @@ inline or_exprt &to_or_expr(exprt &expr)
   return static_cast<or_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<or_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<or_exprt>(const exprt &base)
 {
   return base.id()==ID_or;
 }
@@ -2372,7 +2372,7 @@ inline bitnot_exprt &to_bitnot_expr(exprt &expr)
   return static_cast<bitnot_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<bitnot_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<bitnot_exprt>(const exprt &base)
 {
   return base.id()==ID_bitnot;
 }
@@ -2429,7 +2429,7 @@ inline bitor_exprt &to_bitor_expr(exprt &expr)
   return static_cast<bitor_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<bitor_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<bitor_exprt>(const exprt &base)
 {
   return base.id()==ID_bitor;
 }
@@ -2489,7 +2489,7 @@ inline bitxor_exprt &to_bitxor_expr(exprt &expr)
   return static_cast<bitxor_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<bitxor_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<bitxor_exprt>(const exprt &base)
 {
   return base.id()==ID_bitxor;
 }
@@ -2550,7 +2550,7 @@ inline bitand_exprt &to_bitand_expr(exprt &expr)
   return static_cast<bitand_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<bitand_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<bitand_exprt>(const exprt &base)
 {
   return base.id()==ID_bitand;
 }
@@ -2780,7 +2780,7 @@ inline replication_exprt &to_replication_expr(exprt &expr)
   return static_cast<replication_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<replication_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<replication_exprt>(const exprt &base)
 {
   return base.id()==ID_replication;
 }
@@ -2861,7 +2861,7 @@ inline extractbit_exprt &to_extractbit_expr(exprt &expr)
   return static_cast<extractbit_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<extractbit_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<extractbit_exprt>(const exprt &base)
 {
   return base.id()==ID_extractbit;
 }
@@ -2959,7 +2959,7 @@ inline extractbits_exprt &to_extractbits_expr(exprt &expr)
   return static_cast<extractbits_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<extractbits_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<extractbits_exprt>(const exprt &base)
 {
   return base.id()==ID_extractbits;
 }
@@ -3019,7 +3019,7 @@ inline address_of_exprt &to_address_of_expr(exprt &expr)
   return static_cast<address_of_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<address_of_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<address_of_exprt>(const exprt &base)
 {
   return base.id()==ID_address_of;
 }
@@ -3082,7 +3082,7 @@ inline not_exprt &to_not_expr(exprt &expr)
   return static_cast<not_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<not_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<not_exprt>(const exprt &base)
 {
   return base.id()==ID_not;
 }
@@ -3162,7 +3162,7 @@ inline dereference_exprt &to_dereference_expr(exprt &expr)
   return static_cast<dereference_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<dereference_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<dereference_exprt>(const exprt &base)
 {
   return base.id()==ID_dereference;
 }
@@ -3260,7 +3260,7 @@ inline if_exprt &to_if_expr(exprt &expr)
   return static_cast<if_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<if_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<if_exprt>(const exprt &base)
 {
   return base.id()==ID_if;
 }
@@ -3353,7 +3353,7 @@ inline with_exprt &to_with_expr(exprt &expr)
   return static_cast<with_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<with_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<with_exprt>(const exprt &base)
 {
   return base.id()==ID_with;
 }
@@ -3417,7 +3417,7 @@ inline index_designatort &to_index_designator(exprt &expr)
   return static_cast<index_designatort &>(expr);
 }
 
-template<> inline bool check_expr_type<index_designatort>(const exprt &base)
+template<> inline bool can_cast_expr<index_designatort>(const exprt &base)
 {
   return base.id()==ID_index_designator;
 }
@@ -3473,7 +3473,7 @@ inline member_designatort &to_member_designator(exprt &expr)
   return static_cast<member_designatort &>(expr);
 }
 
-template<> inline bool check_expr_type<member_designatort>(const exprt &base)
+template<> inline bool can_cast_expr<member_designatort>(const exprt &base)
 {
   return base.id()==ID_member_designator;
 }
@@ -3575,7 +3575,7 @@ inline update_exprt &to_update_expr(exprt &expr)
   return static_cast<update_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<update_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<update_exprt>(const exprt &base)
 {
   return base.id()==ID_update;
 }
@@ -3670,7 +3670,7 @@ inline array_update_exprt &to_array_update_expr(exprt &expr)
   return static_cast<array_update_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<array_update_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<array_update_exprt>(const exprt &base)
 {
   return base.id()==ID_array_update;
 }
@@ -3804,7 +3804,7 @@ inline member_exprt &to_member_expr(exprt &expr)
   return static_cast<member_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<member_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<member_exprt>(const exprt &base)
 {
   return base.id()==ID_member;
 }
@@ -3856,7 +3856,7 @@ inline isnan_exprt &to_isnan_expr(exprt &expr)
   return static_cast<isnan_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<isnan_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<isnan_exprt>(const exprt &base)
 {
   return base.id()==ID_isnan;
 }
@@ -3912,7 +3912,7 @@ inline isinf_exprt &to_isinf_expr(exprt &expr)
   return static_cast<isinf_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<isinf_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<isinf_exprt>(const exprt &base)
 {
   return base.id()==ID_isinf;
 }
@@ -3964,7 +3964,7 @@ inline isfinite_exprt &to_isfinite_expr(exprt &expr)
   return static_cast<isfinite_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<isfinite_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<isfinite_exprt>(const exprt &base)
 {
   return base.id()==ID_isfinite;
 }
@@ -4016,7 +4016,7 @@ inline isnormal_exprt &to_isnormal_expr(exprt &expr)
   return static_cast<isnormal_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<isnormal_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<isnormal_exprt>(const exprt &base)
 {
   return base.id()==ID_isnormal;
 }
@@ -4073,7 +4073,7 @@ inline ieee_float_equal_exprt &to_ieee_float_equal_expr(exprt &expr)
 }
 
 template<>
-inline bool check_expr_type<ieee_float_equal_exprt>(const exprt &base)
+inline bool can_cast_expr<ieee_float_equal_exprt>(const exprt &base)
 {
   return base.id()==ID_ieee_float_equal;
 }
@@ -4132,7 +4132,7 @@ inline ieee_float_notequal_exprt &to_ieee_float_notequal_expr(exprt &expr)
 }
 
 template<>
-inline bool check_expr_type<ieee_float_notequal_exprt>(const exprt &base)
+inline bool can_cast_expr<ieee_float_notequal_exprt>(const exprt &base)
 {
   return base.id()==ID_ieee_float_notequal;
 }
@@ -4308,7 +4308,7 @@ inline constant_exprt &to_constant_expr(exprt &expr)
   return static_cast<constant_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<constant_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<constant_exprt>(const exprt &base)
 {
   return base.id()==ID_constant;
 }
@@ -4436,7 +4436,7 @@ inline function_application_exprt &to_function_application_expr(exprt &expr)
 }
 
 template<>
-inline bool check_expr_type<function_application_exprt>(const exprt &base)
+inline bool can_cast_expr<function_application_exprt>(const exprt &base)
 {
   return base.id()==ID_function_application;
 }
@@ -4504,7 +4504,7 @@ inline concatenation_exprt &to_concatenation_expr(exprt &expr)
   return static_cast<concatenation_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<concatenation_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<concatenation_exprt>(const exprt &base)
 {
   return base.id()==ID_concatenation;
 }
@@ -4600,7 +4600,7 @@ inline let_exprt &to_let_expr(exprt &expr)
   return static_cast<let_exprt &>(expr);
 }
 
-template<> inline bool check_expr_type<let_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<let_exprt>(const exprt &base)
 {
   return base.id()==ID_let;
 }

From b8ab6248ee9706ba3e02ef180ba9568f50ec4804 Mon Sep 17 00:00:00 2001
From: Nathan Phillips <nathan.phillips@diffblue.com>
Date: Thu, 31 Aug 2017 12:13:27 +0100
Subject: [PATCH 6/8] Code review fixup

Added missing documentation of type parameter
Added static assert for type of TExpr
---
 src/util/expr_cast.h | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/src/util/expr_cast.h b/src/util/expr_cast.h
index 13734f30d5a..6b0a428b9cc 100644
--- a/src/util/expr_cast.h
+++ b/src/util/expr_cast.h
@@ -9,6 +9,7 @@
 /// \brief Templated functions to cast to specific exprt-derived classes
 
 #include <typeinfo>
+#include <type_traits>
 #include "invariant.h"
 #include "expr.h"
 
@@ -56,12 +57,16 @@ T expr_dynamic_cast(exprt *base)
 /// \brief Cast a pointer to a generic exprt to a specific derived class
 /// \tparam T The pointer or const pointer type to \a TUnderlying to cast to
 /// \tparam TUnderlying An exprt-derived class type
+/// \tparam TExpr The original type to cast from, either exprt or const exprt
 /// \param base Pointer to a generic \ref exprt
 /// \return Pointer to object of type \a TUnderlying
 ///   or null if \a base is not an instance of \a TUnderlying
 template<typename T, typename TUnderlying, typename TExpr>
 T expr_dynamic_cast(TExpr *base)
 {
+  static_assert(
+    std::is_same<typename std::remove_const<TExpr>::type, exprt>::value,
+    "Tried to expr_dynamic_cast from something that wasn't an exprt");
   static_assert(
     std::is_pointer<T>::value,
     "Tried to convert exprt * to non-pointer type");
@@ -109,12 +114,16 @@ T expr_dynamic_cast(exprt &base)
 /// \brief Cast a reference to a generic exprt to a specific derived class
 /// \tparam T The reference or const reference type to \a TUnderlying to cast to
 /// \tparam TUnderlying An exprt-derived class type
+/// \tparam TExpr The original type to cast from, either exprt or const exprt
 /// \param base Reference to a generic \ref exprt
 /// \return Reference to object of type \a T
 /// \throw std::bad_cast If \a base is not an instance of \a TUnderlying
 template<typename T, typename TUnderlying, typename TExpr>
 T expr_dynamic_cast(TExpr &base)
 {
+  static_assert(
+    std::is_same<typename std::remove_const<TExpr>::type, exprt>::value,
+    "Tried to expr_dynamic_cast from something that wasn't an exprt");
   static_assert(
     std::is_reference<T>::value,
     "Tried to convert exprt & to non-reference type");
@@ -133,10 +142,10 @@ inline void validate_operands(
   const exprt &value,
   exprt::operandst::size_type number,
   const char *message,
-  bool allowMore=false)
+  bool allow_more=false)
 {
   DATA_INVARIANT(
-    allowMore
+    allow_more
       ? value.operands().size()==number
       : value.operands().size()>=number,
     message);

From 96f2d9e51a370b9e374e1785ed44627fb498ddbd Mon Sep 17 00:00:00 2001
From: Nathan Phillips <nathan.phillips@diffblue.com>
Date: Thu, 31 Aug 2017 18:05:52 +0100
Subject: [PATCH 7/8] Added a PRECONDITION assert/invariant

This better matches the existing behaviour
---
 src/util/expr_cast.h              |  7 +++++++
 unit/util/expr_cast/expr_cast.cpp | 14 ++++++++++----
 2 files changed, 17 insertions(+), 4 deletions(-)

diff --git a/src/util/expr_cast.h b/src/util/expr_cast.h
index 6b0a428b9cc..d18e3537a4e 100644
--- a/src/util/expr_cast.h
+++ b/src/util/expr_cast.h
@@ -88,6 +88,8 @@ T expr_dynamic_cast(TExpr *base)
 /// \param base Reference to a generic \ref exprt
 /// \return Reference to object of type \a T
 /// \throw std::bad_cast If \a base is not an instance of \a T
+/// \remark If CBMC assertions (PRECONDITION) are set to abort then this will
+///   abort rather than throw if \a base is not an instance of \a T
 template<typename T>
 T expr_dynamic_cast(const exprt &base)
 {
@@ -102,6 +104,8 @@ T expr_dynamic_cast(const exprt &base)
 /// \param base Reference to a generic \ref exprt
 /// \return Reference to object of type \a T
 /// \throw std::bad_cast If \a base is not an instance of \a T
+/// \remark If CBMC assertions (PRECONDITION) are set to abort then this will
+///   abort rather than throw if \a base is not an instance of \a T
 template<typename T>
 T expr_dynamic_cast(exprt &base)
 {
@@ -118,6 +122,8 @@ T expr_dynamic_cast(exprt &base)
 /// \param base Reference to a generic \ref exprt
 /// \return Reference to object of type \a T
 /// \throw std::bad_cast If \a base is not an instance of \a TUnderlying
+/// \remark If CBMC assertions (PRECONDITION) are set to abort then this will
+///   abort rather than throw if \a base is not an instance of \a TUnderlying
 template<typename T, typename TUnderlying, typename TExpr>
 T expr_dynamic_cast(TExpr &base)
 {
@@ -130,6 +136,7 @@ T expr_dynamic_cast(TExpr &base)
   static_assert(
     std::is_base_of<exprt, TUnderlying>::value,
     "The template argument T must be derived from exprt.");
+  PRECONDITION(can_cast_expr<TUnderlying>(base));
   if(!can_cast_expr<TUnderlying>(base))
     throw std::bad_cast();
   T value=static_cast<T>(base);
diff --git a/unit/util/expr_cast/expr_cast.cpp b/unit/util/expr_cast/expr_cast.cpp
index 728a831b8bc..dd8c48f5619 100644
--- a/unit/util/expr_cast/expr_cast.cpp
+++ b/unit/util/expr_cast/expr_cast.cpp
@@ -56,9 +56,11 @@ SCENARIO("expr_dynamic_cast",
 
     THEN("Casting from exprt reference to transt reference should throw")
     {
-      REQUIRE_THROWS_AS(
-        expr_dynamic_cast<const transt &>(expr_ref),
-        std::bad_cast);
+      // This no longer throws exceptions when our custom asserts are set to
+      //  abort the program
+      // REQUIRE_THROWS_AS(
+      //   expr_dynamic_cast<const transt &>(expr_ref),
+      //   std::bad_cast);
     }
   }
   GIVEN("A exprt reference to a symbolt")
@@ -73,7 +75,11 @@ SCENARIO("expr_dynamic_cast",
 
     THEN("Casting from exprt reference to transt reference should throw")
     {
-      REQUIRE_THROWS_AS(expr_dynamic_cast<transt &>(expr_ref), std::bad_cast);
+      // This no longer throws exceptions when our custom asserts are set to
+      //  abort the program
+      // REQUIRE_THROWS_AS(
+      //   expr_dynamic_cast<transt &>(expr_ref),
+      //   std::bad_cast);
     }
 
     THEN(

From da4df034ae76457182fd489ebec9f121b7832c71 Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Tue, 19 Sep 2017 17:26:52 +0100
Subject: [PATCH 8/8] Switch from pointers to optionalt

---
 src/util/expr_cast.h                         | 81 +++++++++++---------
 unit/CMakeLists.txt                          |  3 +
 unit/util/expr_cast/expr_cast.cpp            | 27 ++++---
 unit/util/expr_cast/expr_undefined_casts.cpp | 19 ++---
 4 files changed, 74 insertions(+), 56 deletions(-)

diff --git a/src/util/expr_cast.h b/src/util/expr_cast.h
index d18e3537a4e..e5cc222c49a 100644
--- a/src/util/expr_cast.h
+++ b/src/util/expr_cast.h
@@ -1,6 +1,10 @@
-/*
-  Author: Nathan Phillips <Nathan.Phillips@diffblue.com>
-*/
+/*******************************************************************\
+
+Module:
+
+Author: Nathan Phillips <Nathan.Phillips@diffblue.com>
+
+\*******************************************************************/
 
 #ifndef CPROVER_UTIL_EXPR_CAST_H
 #define CPROVER_UTIL_EXPR_CAST_H
@@ -10,9 +14,11 @@
 
 #include <typeinfo>
 #include <type_traits>
+#include <functional>
+
 #include "invariant.h"
 #include "expr.h"
-
+#include "optional.h"
 
 /// \brief Check whether a reference to a generic \ref exprt is of a specific
 ///   derived class.
@@ -25,61 +31,66 @@
 template<typename T> bool can_cast_expr(const exprt &base);
 
 
-/// \brief Cast a constant pointer to a generic exprt to a specific derived
-///   class
+/// \brief Try to cast a constant reference to a generic exprt to a specific
+///   derived class
 /// \tparam T The exprt-derived class to cast to
-/// \param base Pointer to a generic \ref exprt
-/// \return Pointer to object of type \a T or null if \a base is not an
-///   instance of \a T
+/// \param base Reference to a generic \ref exprt
+/// \return Reference to object of type \a T or valueless optional if \a base
+///   is not an instance of \a T
 template<typename T>
-T expr_dynamic_cast(const exprt *base)
+optionalt<std::reference_wrapper<typename std::remove_reference<T>::type>>
+expr_try_dynamic_cast(const exprt &base)
 {
-  return expr_dynamic_cast<
+  return expr_try_dynamic_cast<
     T,
-    typename std::remove_const<typename std::remove_pointer<T>::type>::type,
+    typename std::remove_reference<T>::type,
+    typename std::remove_const<typename std::remove_reference<T>::type>::type,
     const exprt>(base);
 }
 
-/// \brief Cast a pointer to a generic exprt to a specific derived class
+/// \brief Try to cast a reference to a generic exprt to a specific derived
+///   class
 /// \tparam T The exprt-derived class to cast to
-/// \param base Pointer to a generic \ref exprt
-/// \return Pointer to object of type \a T or null if \a base is not an
-///   instance of \a T
+/// \param base Reference to a generic \ref exprt
+/// \return Reference to object of type \a T or valueless optional if \a base is
+///   not an instance of \a T
 template<typename T>
-T expr_dynamic_cast(exprt *base)
+optionalt<std::reference_wrapper<typename std::remove_reference<T>::type>>
+expr_try_dynamic_cast(exprt &base)
 {
-  return expr_dynamic_cast<
+  return expr_try_dynamic_cast<
     T,
-    typename std::remove_const<typename std::remove_pointer<T>::type>::type,
+    typename std::remove_reference<T>::type,
+    typename std::remove_const<typename std::remove_reference<T>::type>::type,
     exprt>(base);
 }
 
-/// \brief Cast a pointer to a generic exprt to a specific derived class
-/// \tparam T The pointer or const pointer type to \a TUnderlying to cast to
+/// \brief Try to cast a reference to a generic exprt to a specific derived
+///    class
+/// \tparam T The reference or const reference type to \a TUnderlying to cast
+///    to
 /// \tparam TUnderlying An exprt-derived class type
 /// \tparam TExpr The original type to cast from, either exprt or const exprt
-/// \param base Pointer to a generic \ref exprt
-/// \return Pointer to object of type \a TUnderlying
-///   or null if \a base is not an instance of \a TUnderlying
-template<typename T, typename TUnderlying, typename TExpr>
-T expr_dynamic_cast(TExpr *base)
+/// \param base Reference to a generic \ref exprt
+/// \return Reference to object of type \a TUnderlying
+///   or valueless optional if \a base is not an instance of \a TUnderlying
+template<typename T, typename TConst, typename TUnderlying, typename TExpr>
+optionalt<std::reference_wrapper<TConst>> expr_try_dynamic_cast(TExpr &base)
 {
   static_assert(
     std::is_same<typename std::remove_const<TExpr>::type, exprt>::value,
-    "Tried to expr_dynamic_cast from something that wasn't an exprt");
+    "Tried to expr_try_dynamic_cast from something that wasn't an exprt");
   static_assert(
-    std::is_pointer<T>::value,
-    "Tried to convert exprt * to non-pointer type");
+    std::is_reference<T>::value,
+    "Tried to convert exprt & to non-reference type");
   static_assert(
     std::is_base_of<exprt, TUnderlying>::value,
     "The template argument T must be derived from exprt.");
-  if(base == nullptr)
-    return nullptr;
-  if(!can_cast_expr<TUnderlying>(*base))
-    return nullptr;
+  if(!can_cast_expr<TUnderlying>(base))
+    return optionalt<std::reference_wrapper<TConst>>();
   T value=static_cast<T>(base);
-  validate_expr(*value);
-  return value;
+  validate_expr(value);
+  return optionalt<std::reference_wrapper<TConst>>(value);
 }
 
 /// \brief Cast a constant reference to a generic exprt to a specific derived
diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt
index 623e57ecb50..010ef336546 100644
--- a/unit/CMakeLists.txt
+++ b/unit/CMakeLists.txt
@@ -21,6 +21,9 @@ list(REMOVE_ITEM sources
     ${CMAKE_CURRENT_SOURCE_DIR}/cpp_scanner.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/float_utils.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/ieee_float.cpp
+
+    # Intended to fail to compile
+    ${CMAKE_CURRENT_SOURCE_DIR}/util/expr_cast/expr_undefined_casts.cpp
 )
 
 add_executable(unit ${sources} ${headers})
diff --git a/unit/util/expr_cast/expr_cast.cpp b/unit/util/expr_cast/expr_cast.cpp
index dd8c48f5619..658e35a5057 100644
--- a/unit/util/expr_cast/expr_cast.cpp
+++ b/unit/util/expr_cast/expr_cast.cpp
@@ -16,32 +16,35 @@ SCENARIO("expr_dynamic_cast",
 {
   symbol_exprt symbol_expr;
 
-  GIVEN("A const exprt pointer to a symbolt")
+  GIVEN("A const exprt reference to a symbolt")
   {
-    const exprt *expr_ptr=&symbol_expr;
+    const exprt &expr=symbol_expr;
 
-    THEN("Casting from exprt pointer to symbol_exprt pointer returns non-null")
+    THEN("Try-casting from exprt reference to symbol_exprt pointer "
+         "returns a value")
     {
-      REQUIRE(expr_dynamic_cast<const symbol_exprt *>(expr_ptr)!=nullptr);
+      REQUIRE(expr_try_dynamic_cast<const symbol_exprt &>(expr).has_value());
     }
 
-    THEN("Casting from exprt pointer to transt pointer returns null")
+    THEN("Casting from exprt pointer to transt pointer doesn't return a value")
     {
-      REQUIRE(expr_dynamic_cast<const transt *>(expr_ptr)==nullptr);
+      REQUIRE(!expr_try_dynamic_cast<const transt &>(expr).has_value());
     }
   }
-  GIVEN("A exprt pointer to a symbolt")
+  GIVEN("A exprt reference to a symbolt")
   {
-    exprt *expr_ptr=&symbol_expr;
+    exprt &expr=symbol_expr;
 
-    THEN("Casting from exprt pointer to symbol_exprt pointer returns non-null")
+    THEN("Casting from exprt reference to symbol_exprt reference "
+         "returns a value")
     {
-      REQUIRE(expr_dynamic_cast<symbol_exprt *>(expr_ptr)!=nullptr);
+      REQUIRE(expr_try_dynamic_cast<symbol_exprt &>(expr).has_value());
     }
 
-    THEN("Casting from exprt pointer to transt pointer returns null")
+    THEN("Casting from exprt reference to transt reference "
+         "doesn't return a value")
     {
-      REQUIRE(expr_dynamic_cast<transt *>(expr_ptr)==nullptr);
+      REQUIRE(!expr_try_dynamic_cast<transt &>(expr).has_value());
     }
   }
   GIVEN("A const exprt reference to a symbolt")
diff --git a/unit/util/expr_cast/expr_undefined_casts.cpp b/unit/util/expr_cast/expr_undefined_casts.cpp
index 50e3ea25a25..4f1dc7165b8 100644
--- a/unit/util/expr_cast/expr_undefined_casts.cpp
+++ b/unit/util/expr_cast/expr_undefined_casts.cpp
@@ -19,31 +19,32 @@ SCENARIO("expr_dynamic_cast",
 {
   symbol_exprt symbol_expr;
 
-  GIVEN("A const exprt pointer to a symbolt")
+  GIVEN("A const exprt reference to a symbolt")
   {
-    const exprt *expr_ptr=&symbol_expr;
+    const exprt &expr=symbol_expr;
 
-    THEN("Casting from exprt pointer to ieee_float_op_exprt should not compile")
+    THEN("Casting from exprt reference to ieee_float_op_exprt "
+         "should not compile")
     {
       // This shouldn't compile
-      expr_dynamic_cast<const ieee_float_op_exprt *>(expr_ptr);
+      expr_dynamic_cast<const ieee_float_op_exprt &>(expr);
     }
-    THEN("Casting from exprt pointer to shift_exprt should not compile")
+    THEN("Casting from exprt reference to shift_exprt should not compile")
     {
       // This shouldn't compile
-      expr_dynamic_cast<const shift_exprt *>(expr_ptr);
+      expr_dynamic_cast<const shift_exprt &>(expr);
     }
     THEN(
-      "Casting from exprt pointer to non-pointer/reference should not compile")
+      "Casting from exprt reference to non-reference should not compile")
     {
       // This shouldn't compile
-      expr_dynamic_cast<symbol_exprt>(expr_ptr);
+      expr_dynamic_cast<symbol_exprt>(expr);
     }
     THEN(
       "Casting from const exprt reference to non-const symbol_exprt reference "
       "should not compile")
     {
-      expr_dynamic_cast<symbol_exprt *>(expr_ptr);
+      expr_dynamic_cast<symbol_exprt &>(expr);
     }
   }
 }