CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
expr_cast.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Nathan Phillips <Nathan.Phillips@diffblue.com>
6
7\*******************************************************************/
8
9#ifndef CPROVER_UTIL_EXPR_CAST_H
10#define CPROVER_UTIL_EXPR_CAST_H
11
14
15#include <typeinfo>
16#include <type_traits>
17#include <functional>
18
19#include "invariant.h"
20#include "expr.h"
21
30template<typename T> inline bool can_cast_expr(const exprt &base);
31
40template <typename T>
41inline bool can_cast_type(const typet &base);
42
49inline void validate_expr(const exprt &) {}
50
51namespace detail // NOLINT
52{
53
54template<typename Ret, typename T>
56{
57 static_assert(
58 !std::is_reference<Ret>::value,
59 "Ret must not be a reference, i.e. expr_try_dynamic_cast<const thingt> "
60 "rather than expr_try_dynamic_cast<const thing &>");
61
62 typedef
63 typename std::conditional<
64 std::is_const<T>::value,
65 typename std::add_const<Ret>::type,
66 Ret>::type *
68};
69
70} // namespace detail
71
80template <typename T, typename TExpr>
83{
84 typedef
86 returnt;
87 static_assert(
88 std::is_base_of<exprt, typename std::decay<TExpr>::type>::value,
89 "Tried to expr_try_dynamic_cast from something that wasn't an exprt");
90 static_assert(
91 std::is_base_of<exprt, T>::value,
92 "The template argument T must be derived from exprt.");
93 if(!can_cast_expr<typename std::remove_const<T>::type>(base))
94 return nullptr;
95 const auto ret=static_cast<returnt>(&base);
97 return ret;
98}
99
106template <typename T, typename TExpr>
107std::optional<T> expr_try_dynamic_cast(TExpr &&base)
108{
109 static_assert(
110 std::is_rvalue_reference<decltype(base)>::value,
111 "This template overload must only match where base is an rvalue.");
112 static_assert(
113 std::is_base_of<exprt, typename std::decay<TExpr>::type>::value,
114 "Tried to expr_try_dynamic_cast from something that wasn't an exprt.");
115 static_assert(
116 std::is_base_of<exprt, T>::value,
117 "The template argument T must be derived from exprt.");
118 static_assert(!std::is_const<TExpr>::value, "Attempted to move from const.");
119 if(!can_cast_expr<T>(base))
120 return {};
121 std::optional<T> ret{static_cast<T &&>(base)};
123 return ret;
124}
125
134template <typename T, typename TType>
137{
138 typedef
140 static_assert(
141 std::is_base_of<typet, typename std::decay<TType>::type>::value,
142 "Tried to type_try_dynamic_cast from something that wasn't an typet");
143 static_assert(
144 std::is_base_of<typet, T>::value,
145 "The template argument T must be derived from typet.");
146 if(!can_cast_type<typename std::remove_const<T>::type>(base))
147 return nullptr;
148 TType::check(base);
149 return static_cast<returnt>(&base);
150}
151
158template <typename T, typename TType>
159std::optional<T> type_try_dynamic_cast(TType &&base)
160{
161 static_assert(
162 std::is_rvalue_reference<decltype(base)>::value,
163 "This template overload must only match where base is an rvalue.");
164 static_assert(
165 std::is_base_of<typet, typename std::decay<TType>::type>::value,
166 "Tried to type_try_dynamic_cast from something that wasn't an typet.");
167 static_assert(
168 std::is_base_of<typet, T>::value,
169 "The template argument T must be derived from typet.");
170 static_assert(!std::is_const<TType>::value, "Attempted to move from const.");
171 if(!can_cast_type<T>(base))
172 return {};
173 TType::check(base);
174 std::optional<T> ret{static_cast<T &&>(base)};
175 return ret;
176}
177
178namespace detail // NOLINT
179{
180
181template<typename Ret, typename T>
183{
184 static_assert(
185 !std::is_reference<Ret>::value,
186 "Ret must not be a reference, i.e. expr_dynamic_cast<const thingt> rather "
187 "than expr_dynamic_cast<const thing &>");
188
189 typedef
190 typename std::conditional<
191 std::is_const<T>::value,
192 typename std::add_const<Ret>::type,
193 Ret>::type &
195};
196
197} // namespace detail
198
206template<typename T, typename TExpr>
209{
210 const auto ret=expr_try_dynamic_cast<T>(base);
211 if(ret==nullptr)
212 throw std::bad_cast();
213 return *ret;
214}
215
226template<typename T, typename TExpr>
233
241template <typename T, typename TType>
244{
245 auto result = type_try_dynamic_cast<T>(base);
246 CHECK_RETURN(result != nullptr);
247 return *result;
248}
249
251 const exprt &value,
252 exprt::operandst::size_type number,
253 const char *message,
254 bool allow_more=false)
255{
258 ? value.operands().size()>=number
259 : value.operands().size()==number,
260 message);
261}
262
263#endif // CPROVER_UTIL_EXPR_CAST_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
operandst & operands()
Definition expr.h:94
The type of an expression, extends irept.
Definition type.h:29
auto expr_checked_cast(TExpr &base) -> typename detail::expr_dynamic_cast_return_typet< T, TExpr >::type
Cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:227
bool can_cast_expr(const exprt &base)
Check whether a reference to a generic exprt is of a specific derived class.
auto type_checked_cast(TType &base) -> typename detail::expr_dynamic_cast_return_typet< T, TType >::type
Cast a reference to a generic typet to a specific derived class and checks that the type could be con...
Definition expr_cast.h:242
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
Definition expr_cast.h:135
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition expr_cast.h:250
void validate_expr(const exprt &)
Called after casting.
Definition expr_cast.h:49
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
auto expr_dynamic_cast(TExpr &base) -> typename detail::expr_dynamic_cast_return_typet< T, TExpr >::type
Cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:207
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
std::conditional< std::is_const< T >::value, typenamestd::add_const< Ret >::type, Ret >::type & type
Definition expr_cast.h:194
std::conditional< std::is_const< T >::value, typenamestd::add_const< Ret >::type, Ret >::type * type
Definition expr_cast.h:67