|  | 
|  | 1 | +/*******************************************************************\ | 
|  | 2 | +
 | 
|  | 3 | +Module: | 
|  | 4 | +
 | 
|  | 5 | +Author: Nathan Phillips <[email protected]> | 
|  | 6 | +
 | 
|  | 7 | +\*******************************************************************/ | 
|  | 8 | + | 
|  | 9 | +#ifndef CPROVER_UTIL_EXPR_CAST_H | 
|  | 10 | +#define CPROVER_UTIL_EXPR_CAST_H | 
|  | 11 | + | 
|  | 12 | +/// \file util/expr_cast.h | 
|  | 13 | +/// \brief Templated functions to cast to specific exprt-derived classes | 
|  | 14 | + | 
|  | 15 | +#include <typeinfo> | 
|  | 16 | +#include <type_traits> | 
|  | 17 | +#include <functional> | 
|  | 18 | + | 
|  | 19 | +#include "invariant.h" | 
|  | 20 | +#include "expr.h" | 
|  | 21 | +#include "optional.h" | 
|  | 22 | + | 
|  | 23 | +/// \brief Check whether a reference to a generic \ref exprt is of a specific | 
|  | 24 | +///   derived class. | 
|  | 25 | +/// | 
|  | 26 | +///   Implement template specializations of this function to enable casting | 
|  | 27 | +/// | 
|  | 28 | +/// \tparam T The exprt-derived class to check for | 
|  | 29 | +/// \param base Reference to a generic \ref exprt | 
|  | 30 | +/// \return true if \a base is of type \a T | 
|  | 31 | +template<typename T> bool can_cast_expr(const exprt &base); | 
|  | 32 | + | 
|  | 33 | + | 
|  | 34 | +/// \brief Try to cast a constant reference to a generic exprt to a specific | 
|  | 35 | +///   derived class | 
|  | 36 | +/// \tparam T The exprt-derived class to cast to | 
|  | 37 | +/// \param base Reference to a generic \ref exprt | 
|  | 38 | +/// \return Reference to object of type \a T or valueless optional if \a base | 
|  | 39 | +///   is not an instance of \a T | 
|  | 40 | +template<typename T> | 
|  | 41 | +optionalt<std::reference_wrapper<typename std::remove_reference<T>::type>> | 
|  | 42 | +expr_try_dynamic_cast(const exprt &base) | 
|  | 43 | +{ | 
|  | 44 | +  return expr_try_dynamic_cast< | 
|  | 45 | +    T, | 
|  | 46 | +    typename std::remove_reference<T>::type, | 
|  | 47 | +    typename std::remove_const<typename std::remove_reference<T>::type>::type, | 
|  | 48 | +    const exprt>(base); | 
|  | 49 | +} | 
|  | 50 | + | 
|  | 51 | +/// \brief Try to cast a reference to a generic exprt to a specific derived | 
|  | 52 | +///   class | 
|  | 53 | +/// \tparam T The exprt-derived class to cast to | 
|  | 54 | +/// \param base Reference to a generic \ref exprt | 
|  | 55 | +/// \return Reference to object of type \a T or valueless optional if \a base is | 
|  | 56 | +///   not an instance of \a T | 
|  | 57 | +template<typename T> | 
|  | 58 | +optionalt<std::reference_wrapper<typename std::remove_reference<T>::type>> | 
|  | 59 | +expr_try_dynamic_cast(exprt &base) | 
|  | 60 | +{ | 
|  | 61 | +  return expr_try_dynamic_cast< | 
|  | 62 | +    T, | 
|  | 63 | +    typename std::remove_reference<T>::type, | 
|  | 64 | +    typename std::remove_const<typename std::remove_reference<T>::type>::type, | 
|  | 65 | +    exprt>(base); | 
|  | 66 | +} | 
|  | 67 | + | 
|  | 68 | +/// \brief Try to cast a reference to a generic exprt to a specific derived | 
|  | 69 | +///    class | 
|  | 70 | +/// \tparam T The reference or const reference type to \a TUnderlying to cast | 
|  | 71 | +///    to | 
|  | 72 | +/// \tparam TUnderlying An exprt-derived class type | 
|  | 73 | +/// \tparam TExpr The original type to cast from, either exprt or const exprt | 
|  | 74 | +/// \param base Reference to a generic \ref exprt | 
|  | 75 | +/// \return Reference to object of type \a TUnderlying | 
|  | 76 | +///   or valueless optional if \a base is not an instance of \a TUnderlying | 
|  | 77 | +template<typename T, typename TConst, typename TUnderlying, typename TExpr> | 
|  | 78 | +optionalt<std::reference_wrapper<TConst>> expr_try_dynamic_cast(TExpr &base) | 
|  | 79 | +{ | 
|  | 80 | +  static_assert( | 
|  | 81 | +    std::is_same<typename std::remove_const<TExpr>::type, exprt>::value, | 
|  | 82 | +    "Tried to expr_try_dynamic_cast from something that wasn't an exprt"); | 
|  | 83 | +  static_assert( | 
|  | 84 | +    std::is_reference<T>::value, | 
|  | 85 | +    "Tried to convert exprt & to non-reference type"); | 
|  | 86 | +  static_assert( | 
|  | 87 | +    std::is_base_of<exprt, TUnderlying>::value, | 
|  | 88 | +    "The template argument T must be derived from exprt."); | 
|  | 89 | +  if(!can_cast_expr<TUnderlying>(base)) | 
|  | 90 | +    return optionalt<std::reference_wrapper<TConst>>(); | 
|  | 91 | +  T value=static_cast<T>(base); | 
|  | 92 | +  validate_expr(value); | 
|  | 93 | +  return optionalt<std::reference_wrapper<TConst>>(value); | 
|  | 94 | +} | 
|  | 95 | + | 
|  | 96 | +/// \brief Cast a constant reference to a generic exprt to a specific derived | 
|  | 97 | +///   class | 
|  | 98 | +/// \tparam T The exprt-derived class to cast to | 
|  | 99 | +/// \param base Reference to a generic \ref exprt | 
|  | 100 | +/// \return Reference to object of type \a T | 
|  | 101 | +/// \throw std::bad_cast If \a base is not an instance of \a T | 
|  | 102 | +/// \remark If CBMC assertions (PRECONDITION) are set to abort then this will | 
|  | 103 | +///   abort rather than throw if \a base is not an instance of \a T | 
|  | 104 | +template<typename T> | 
|  | 105 | +T expr_dynamic_cast(const exprt &base) | 
|  | 106 | +{ | 
|  | 107 | +  return expr_dynamic_cast< | 
|  | 108 | +    T, | 
|  | 109 | +    typename std::remove_const<typename std::remove_reference<T>::type>::type, | 
|  | 110 | +    const exprt>(base); | 
|  | 111 | +} | 
|  | 112 | + | 
|  | 113 | +/// \brief Cast a reference to a generic exprt to a specific derived class | 
|  | 114 | +/// \tparam T The exprt-derived class to cast to | 
|  | 115 | +/// \param base Reference to a generic \ref exprt | 
|  | 116 | +/// \return Reference to object of type \a T | 
|  | 117 | +/// \throw std::bad_cast If \a base is not an instance of \a T | 
|  | 118 | +/// \remark If CBMC assertions (PRECONDITION) are set to abort then this will | 
|  | 119 | +///   abort rather than throw if \a base is not an instance of \a T | 
|  | 120 | +template<typename T> | 
|  | 121 | +T expr_dynamic_cast(exprt &base) | 
|  | 122 | +{ | 
|  | 123 | +  return expr_dynamic_cast< | 
|  | 124 | +    T, | 
|  | 125 | +    typename std::remove_const<typename std::remove_reference<T>::type>::type, | 
|  | 126 | +    exprt>(base); | 
|  | 127 | +} | 
|  | 128 | + | 
|  | 129 | +/// \brief Cast a reference to a generic exprt to a specific derived class | 
|  | 130 | +/// \tparam T The reference or const reference type to \a TUnderlying to cast to | 
|  | 131 | +/// \tparam TUnderlying An exprt-derived class type | 
|  | 132 | +/// \tparam TExpr The original type to cast from, either exprt or const exprt | 
|  | 133 | +/// \param base Reference to a generic \ref exprt | 
|  | 134 | +/// \return Reference to object of type \a T | 
|  | 135 | +/// \throw std::bad_cast If \a base is not an instance of \a TUnderlying | 
|  | 136 | +/// \remark If CBMC assertions (PRECONDITION) are set to abort then this will | 
|  | 137 | +///   abort rather than throw if \a base is not an instance of \a TUnderlying | 
|  | 138 | +template<typename T, typename TUnderlying, typename TExpr> | 
|  | 139 | +T expr_dynamic_cast(TExpr &base) | 
|  | 140 | +{ | 
|  | 141 | +  static_assert( | 
|  | 142 | +    std::is_same<typename std::remove_const<TExpr>::type, exprt>::value, | 
|  | 143 | +    "Tried to expr_dynamic_cast from something that wasn't an exprt"); | 
|  | 144 | +  static_assert( | 
|  | 145 | +    std::is_reference<T>::value, | 
|  | 146 | +    "Tried to convert exprt & to non-reference type"); | 
|  | 147 | +  static_assert( | 
|  | 148 | +    std::is_base_of<exprt, TUnderlying>::value, | 
|  | 149 | +    "The template argument T must be derived from exprt."); | 
|  | 150 | +  PRECONDITION(can_cast_expr<TUnderlying>(base)); | 
|  | 151 | +  if(!can_cast_expr<TUnderlying>(base)) | 
|  | 152 | +    throw std::bad_cast(); | 
|  | 153 | +  T value=static_cast<T>(base); | 
|  | 154 | +  validate_expr(value); | 
|  | 155 | +  return value; | 
|  | 156 | +} | 
|  | 157 | + | 
|  | 158 | + | 
|  | 159 | +inline void validate_operands( | 
|  | 160 | +  const exprt &value, | 
|  | 161 | +  exprt::operandst::size_type number, | 
|  | 162 | +  const char *message, | 
|  | 163 | +  bool allow_more=false) | 
|  | 164 | +{ | 
|  | 165 | +  DATA_INVARIANT( | 
|  | 166 | +    allow_more | 
|  | 167 | +      ? value.operands().size()==number | 
|  | 168 | +      : value.operands().size()>=number, | 
|  | 169 | +    message); | 
|  | 170 | +} | 
|  | 171 | + | 
|  | 172 | +#endif  // CPROVER_UTIL_EXPR_CAST_H | 
0 commit comments