Skip to content

Commit 0e70863

Browse files
authored
Merge pull request diffblue#1279 from NathanJPhillips/feature/expr_dynamic_cast
Implementation of expr_dynamic_cast
2 parents 1e9837e + da4df03 commit 0e70863

File tree

6 files changed

+929
-0
lines changed

6 files changed

+929
-0
lines changed

src/util/expr_cast.h

+172
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,172 @@
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

Comments
 (0)