Skip to content

Commit ba96dde

Browse files
authored
Merge pull request #1441 from reuk/reuk/expr-cast-for-code-types
Allow expr_dynamic_cast to be used with std_code types
2 parents 22a68fe + c25e56f commit ba96dde

File tree

2 files changed

+415
-59
lines changed

2 files changed

+415
-59
lines changed

src/util/expr_cast.h

+109-59
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,50 @@ Author: Nathan Phillips <[email protected]>
3030
/// \return true if \a base is of type \a T
3131
template<typename T> bool can_cast_expr(const exprt &base);
3232

33+
/// Called after casting. Provides a point to assert on the structure of the
34+
/// expr. By default, this is a no-op, but you can provide an overload to
35+
/// validate particular types. Should always succeed unless the program has
36+
/// entered an invalid state. We validate objects at cast time as that is when
37+
/// these checks have been used historically, but it would be reasonable to
38+
/// validate objects in this way at any time.
39+
inline void validate_expr(const exprt &) {}
40+
41+
namespace detail // NOLINT
42+
{
43+
44+
// We hide these functions in a namespace so that they only participate in
45+
// overload resolution when explicitly requested.
46+
47+
/// \brief Try to cast a reference to a generic exprt to a specific derived
48+
/// class
49+
/// \tparam T The reference or const reference type to \a TUnderlying to cast
50+
/// to
51+
/// \tparam TExpr The original type to cast from, either exprt or const exprt
52+
/// \param base Reference to a generic \ref exprt
53+
/// \return Reference to object of type \a TUnderlying
54+
/// or valueless optional if \a base is not an instance of \a TUnderlying
55+
template <typename T, typename TExpr>
56+
optionalt<std::reference_wrapper<typename std::remove_reference<T>::type>>
57+
expr_try_dynamic_cast(TExpr &base)
58+
{
59+
typedef typename std::decay<T>::type decayt;
60+
static_assert(
61+
std::is_same<typename std::remove_const<TExpr>::type, exprt>::value,
62+
"Tried to expr_try_dynamic_cast from something that wasn't an exprt");
63+
static_assert(
64+
std::is_reference<T>::value,
65+
"Tried to convert exprt & to non-reference type");
66+
static_assert(
67+
std::is_base_of<exprt, decayt>::value,
68+
"The template argument T must be derived from exprt.");
69+
if(!can_cast_expr<decayt>(base))
70+
return {};
71+
T ret=static_cast<T>(base);
72+
validate_expr(ret);
73+
return std::reference_wrapper<typename std::remove_reference<T>::type>(ret);
74+
}
75+
76+
} // namespace detail
3377

3478
/// \brief Try to cast a constant reference to a generic exprt to a specific
3579
/// derived class
@@ -41,11 +85,7 @@ template<typename T>
4185
optionalt<std::reference_wrapper<typename std::remove_reference<T>::type>>
4286
expr_try_dynamic_cast(const exprt &base)
4387
{
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);
88+
return detail::expr_try_dynamic_cast<T>(base);
4989
}
5090

5191
/// \brief Try to cast a reference to a generic exprt to a specific derived
@@ -58,41 +98,59 @@ template<typename T>
5898
optionalt<std::reference_wrapper<typename std::remove_reference<T>::type>>
5999
expr_try_dynamic_cast(exprt &base)
60100
{
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);
101+
return detail::expr_try_dynamic_cast<T>(base);
66102
}
67103

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
104+
namespace detail // NOLINT
105+
{
106+
107+
// We hide these functions in a namespace so that they only participate in
108+
// overload resolution when explicitly requested.
109+
110+
/// \brief Cast a reference to a generic exprt to a specific derived class.
111+
/// \tparam T The reference or const reference type to \a TUnderlying to cast to
73112
/// \tparam TExpr The original type to cast from, either exprt or const exprt
74113
/// \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)
114+
/// \return Reference to object of type \a T
115+
/// \throw std::bad_cast If \a base is not an instance of \a TUnderlying
116+
template<typename T, typename TExpr>
117+
T expr_dynamic_cast(TExpr &base)
79118
{
119+
typedef typename std::decay<T>::type decayt;
80120
static_assert(
81121
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");
122+
"Tried to expr_dynamic_cast from something that wasn't an exprt");
83123
static_assert(
84124
std::is_reference<T>::value,
85125
"Tried to convert exprt & to non-reference type");
86126
static_assert(
87-
std::is_base_of<exprt, TUnderlying>::value,
127+
std::is_base_of<exprt, decayt>::value,
88128
"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);
129+
if(!can_cast_expr<decayt>(base))
130+
throw std::bad_cast();
131+
T ret=static_cast<T>(base);
132+
validate_expr(ret);
133+
return ret;
94134
}
95135

136+
/// \brief Cast a reference to a generic exprt to a specific derived class.
137+
/// Also assert that the expression has the expected type.
138+
/// \tparam T The reference or const reference type to \a TUnderlying to cast to
139+
/// \tparam TExpr The original type to cast from, either exprt or const exprt
140+
/// \param base Reference to a generic \ref exprt
141+
/// \return Reference to object of type \a T
142+
/// \throw std::bad_cast If \a base is not an instance of \a TUnderlying
143+
/// \remark If CBMC assertions (PRECONDITION) are set to abort then this will
144+
/// abort rather than throw if \a base is not an instance of \a TUnderlying
145+
template<typename T, typename TExpr>
146+
T expr_checked_cast(TExpr &base)
147+
{
148+
PRECONDITION(can_cast_expr<typename std::decay<T>::type>(base));
149+
return expr_dynamic_cast<T>(base);
150+
}
151+
152+
} // namespace detail
153+
96154
/// \brief Cast a constant reference to a generic exprt to a specific derived
97155
/// class
98156
/// \tparam T The exprt-derived class to cast to
@@ -104,10 +162,7 @@ optionalt<std::reference_wrapper<TConst>> expr_try_dynamic_cast(TExpr &base)
104162
template<typename T>
105163
T expr_dynamic_cast(const exprt &base)
106164
{
107-
return expr_dynamic_cast<
108-
T,
109-
typename std::remove_const<typename std::remove_reference<T>::type>::type,
110-
const exprt>(base);
165+
return detail::expr_dynamic_cast<T>(base);
111166
}
112167

113168
/// \brief Cast a reference to a generic exprt to a specific derived class
@@ -120,41 +175,36 @@ T expr_dynamic_cast(const exprt &base)
120175
template<typename T>
121176
T expr_dynamic_cast(exprt &base)
122177
{
123-
return expr_dynamic_cast<
124-
T,
125-
typename std::remove_const<typename std::remove_reference<T>::type>::type,
126-
exprt>(base);
178+
return detail::expr_dynamic_cast<T>(base);
127179
}
128180

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
181+
/// \brief Cast a constant reference to a generic exprt to a specific derived
182+
/// class. Also assert that the exprt invariants are not violated.
183+
/// \tparam T The exprt-derived class to cast to
133184
/// \param base Reference to a generic \ref exprt
134185
/// \return Reference to object of type \a T
135-
/// \throw std::bad_cast If \a base is not an instance of \a TUnderlying
186+
/// \throw std::bad_cast If \a base is not an instance of \a T
136187
/// \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)
188+
/// abort rather than throw if \a base is not an instance of \a T
189+
template<typename T>
190+
T expr_checked_cast(const exprt &base)
140191
{
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;
192+
return detail::expr_checked_cast<T>(base);
156193
}
157194

195+
/// \brief Cast a reference to a generic exprt to a specific derived class.
196+
/// Also assert that the exprt invariants are not violated.
197+
/// \tparam T The exprt-derived class to cast to
198+
/// \param base Reference to a generic \ref exprt
199+
/// \return Reference to object of type \a T
200+
/// \throw std::bad_cast If \a base is not an instance of \a T
201+
/// \remark If CBMC assertions (PRECONDITION) are set to abort then this will
202+
/// abort rather than throw if \a base is not an instance of \a T
203+
template<typename T>
204+
T expr_checked_cast(exprt &base)
205+
{
206+
return detail::expr_checked_cast<T>(base);
207+
}
158208

159209
inline void validate_operands(
160210
const exprt &value,
@@ -164,8 +214,8 @@ inline void validate_operands(
164214
{
165215
DATA_INVARIANT(
166216
allow_more
167-
? value.operands().size()==number
168-
: value.operands().size()>=number,
217+
? value.operands().size()>=number
218+
: value.operands().size()==number,
169219
message);
170220
}
171221

0 commit comments

Comments
 (0)