-
Notifications
You must be signed in to change notification settings - Fork 286
Expand file tree
/
Copy pathexpr_cast.h
More file actions
263 lines (236 loc) · 9.28 KB
/
expr_cast.h
File metadata and controls
263 lines (236 loc) · 9.28 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
/*******************************************************************\
Module:
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 <type_traits>
#include <functional>
#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> inline bool can_cast_expr(const exprt &base);
/// \brief Check whether a reference to a generic \ref typet is of a specific
/// derived class.
///
/// Implement template specializations of this function to enable casting
///
/// \tparam T: The typet-derived class to check for
/// \param base: Reference to a generic \ref typet
/// \return true if \a base is of type \a T
template <typename T>
inline bool can_cast_type(const typet &base);
/// Called after casting. Provides a point to assert on the structure of the
/// expr. By default, this is a no-op, but you can provide an overload to
/// validate particular types. Should always succeed unless the program has
/// entered an invalid state. We validate objects at cast time as that is when
/// these checks have been used historically, but it would be reasonable to
/// validate objects in this way at any time.
inline void validate_expr(const exprt &) {}
namespace detail // NOLINT
{
template<typename Ret, typename T>
struct expr_try_dynamic_cast_return_typet final
{
static_assert(
!std::is_reference<Ret>::value,
"Ret must not be a reference, i.e. expr_try_dynamic_cast<const thingt> "
"rather than expr_try_dynamic_cast<const thing &>");
typedef
typename std::conditional<
std::is_const<T>::value,
typename std::add_const<Ret>::type,
Ret>::type *
type;
};
} // namespace detail
/// \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 TExpr: The original type to cast from, either exprt or const exprt
/// \param base: Reference to a generic \ref exprt
/// \return Ptr to object of type \a TUnderlying
/// or nullptr if \a base is not an instance of \a TUnderlying
template <typename T, typename TExpr>
auto expr_try_dynamic_cast(TExpr &base)
-> typename detail::expr_try_dynamic_cast_return_typet<T, TExpr>::type
{
typedef
typename detail::expr_try_dynamic_cast_return_typet<T, TExpr>::type
returnt;
static_assert(
std::is_base_of<exprt, typename std::decay<TExpr>::type>::value,
"Tried to expr_try_dynamic_cast from something that wasn't an exprt");
static_assert(
std::is_base_of<exprt, T>::value,
"The template argument T must be derived from exprt.");
if(!can_cast_expr<typename std::remove_const<T>::type>(base))
return nullptr;
const auto ret=static_cast<returnt>(&base);
validate_expr(*ret);
return ret;
}
/// \brief Try to cast a generic exprt to a specific derived class.
/// \tparam T: The type to cast the \p base param to.
/// \tparam TType: The original type to cast from, must be a exprt rvalue.
/// \param base: A generic \ref exprt rvalue.
/// \return Cast value in an std::optional<T> or empty if \a base is not an
/// instance of T.
template <typename T, typename TExpr>
std::optional<T> expr_try_dynamic_cast(TExpr &&base)
{
static_assert(
std::is_rvalue_reference<decltype(base)>::value,
"This template overload must only match where base is an rvalue.");
static_assert(
std::is_base_of<exprt, typename std::decay<TExpr>::type>::value,
"Tried to expr_try_dynamic_cast from something that wasn't an exprt.");
static_assert(
std::is_base_of<exprt, T>::value,
"The template argument T must be derived from exprt.");
static_assert(!std::is_const<TExpr>::value, "Attempted to move from const.");
if(!can_cast_expr<T>(base))
return {};
std::optional<T> ret{static_cast<T &&>(base)};
validate_expr(*ret);
return ret;
}
/// \brief Try to cast a reference to a generic typet to a specific derived
/// class
/// \tparam T: The reference or const reference type to \a TUnderlying to cast
/// to
/// \tparam TType: The original type to cast from, either typet or const typet
/// \param base: Reference to a generic \ref typet
/// \return Ptr to object of type \a TUnderlying
/// or nullptr if \a base is not an instance of \a TUnderlying
template <typename T, typename TType>
auto type_try_dynamic_cast(TType &base) ->
typename detail::expr_try_dynamic_cast_return_typet<T, TType>::type
{
typedef
typename detail::expr_try_dynamic_cast_return_typet<T, TType>::type returnt;
static_assert(
std::is_base_of<typet, typename std::decay<TType>::type>::value,
"Tried to type_try_dynamic_cast from something that wasn't an typet");
static_assert(
std::is_base_of<typet, T>::value,
"The template argument T must be derived from typet.");
if(!can_cast_type<typename std::remove_const<T>::type>(base))
return nullptr;
TType::check(base);
return static_cast<returnt>(&base);
}
/// \brief Try to cast a generic typet to a specific derived class.
/// \tparam T: The type to cast the \p base param to.
/// \tparam TType: The original type to cast from, must be a typet rvalue.
/// \param base: A generic \ref typet rvalue.
/// \return Cast value in an std::optional<T> or empty if \a base is not an
/// instance of T.
template <typename T, typename TType>
std::optional<T> type_try_dynamic_cast(TType &&base)
{
static_assert(
std::is_rvalue_reference<decltype(base)>::value,
"This template overload must only match where base is an rvalue.");
static_assert(
std::is_base_of<typet, typename std::decay<TType>::type>::value,
"Tried to type_try_dynamic_cast from something that wasn't an typet.");
static_assert(
std::is_base_of<typet, T>::value,
"The template argument T must be derived from typet.");
static_assert(!std::is_const<TType>::value, "Attempted to move from const.");
if(!can_cast_type<T>(base))
return {};
TType::check(base);
std::optional<T> ret{static_cast<T &&>(base)};
return ret;
}
namespace detail // NOLINT
{
template<typename Ret, typename T>
struct expr_dynamic_cast_return_typet final
{
static_assert(
!std::is_reference<Ret>::value,
"Ret must not be a reference, i.e. expr_dynamic_cast<const thingt> rather "
"than expr_dynamic_cast<const thing &>");
typedef
typename std::conditional<
std::is_const<T>::value,
typename std::add_const<Ret>::type,
Ret>::type &
type;
};
} // namespace detail
/// \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 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 TExpr>
auto expr_dynamic_cast(TExpr &base)
-> typename detail::expr_dynamic_cast_return_typet<T, TExpr>::type
{
const auto ret=expr_try_dynamic_cast<T>(base);
if(ret==nullptr)
throw std::bad_cast();
return *ret;
}
/// \brief Cast a reference to a generic exprt to a specific derived class.
/// Also assert that the expression has the expected type.
/// \tparam T: The reference or const reference type to \a TUnderlying to cast
/// to
/// \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
/// \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 TExpr>
auto expr_checked_cast(TExpr &base)
-> typename detail::expr_dynamic_cast_return_typet<T, TExpr>::type
{
PRECONDITION(can_cast_expr<T>(base));
return expr_dynamic_cast<T>(base);
}
/// \brief Cast a reference to a generic typet to a specific derived class and
/// checks that the type could be converted.
/// \tparam T: The reference or const reference type to \a TUnderlying to cast
/// to
/// \tparam TType: The original type to cast from, either typet or const typet
/// \param base: Reference to a generic \ref typet
/// \return Reference to object of type \a T
template <typename T, typename TType>
auto type_checked_cast(TType &base) ->
typename detail::expr_dynamic_cast_return_typet<T, TType>::type
{
auto result = type_try_dynamic_cast<T>(base);
CHECK_RETURN(result != nullptr);
return *result;
}
inline void validate_operands(
const exprt &value,
exprt::operandst::size_type number,
const char *message,
bool allow_more=false)
{
DATA_INVARIANT(
allow_more
? value.operands().size()>=number
: value.operands().size()==number,
message);
}
#endif // CPROVER_UTIL_EXPR_CAST_H