Skip to content

Commit de8a8d0

Browse files
NathanJPhillipssmowton
authored andcommitted
Implementation of expr_dynamic_cast
1 parent 0cec13d commit de8a8d0

File tree

5 files changed

+915
-0
lines changed

5 files changed

+915
-0
lines changed

src/util/expr_cast.h

+140
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,140 @@
1+
/*
2+
Author: Nathan Phillips <[email protected]>
3+
*/
4+
5+
#ifndef CPROVER_UTIL_EXPR_CAST_H
6+
#define CPROVER_UTIL_EXPR_CAST_H
7+
8+
/// \file util/expr_cast.h
9+
/// \brief Templated functions to cast to specific exprt-derived classes
10+
11+
#include <typeinfo>
12+
#include "invariant.h"
13+
#include "expr.h"
14+
15+
16+
/// \brief Check whether a reference to a generic \ref exprt is of a specific derived class
17+
/// Implement template specializations of this function to enable casting
18+
/// \tparam T The exprt-derived class to check for
19+
/// \param base Reference to a generic \ref exprt
20+
/// \return true if \a base is of type \a T
21+
template<typename T> bool check_expr_type(const exprt &base);
22+
23+
/// \brief Check whether a reference to a generic \ref exprt is of a specific derived class
24+
/// Implement template specializations of this function to enable casting
25+
/// \tparam T The exprt-derived class to check for
26+
/// \param base Reference to a generic \ref exprt
27+
/// \return true if \a base is of type \a T
28+
template<typename T> void validate_expr(const T &value) { }
29+
30+
template<typename T> struct remove_constt;
31+
template<typename T> struct remove_constt<const T> { using type=T; };
32+
template<typename T> struct ptr_typet;
33+
template<typename T> struct ptr_typet<T *> { using type=T; };
34+
template<typename T> struct ref_typet;
35+
template<typename T> struct ref_typet<T &> { using type=T; };
36+
37+
38+
/// \brief Cast a constant pointer to a generic exprt to a specific derived class
39+
/// \tparam T The exprt-derived class to cast to
40+
/// \param base Pointer to a generic \ref exprt
41+
/// \return Pointer to object of type \a T or null if \a base is not an instance of \a T
42+
template<typename T>
43+
T expr_dynamic_cast(const exprt *base)
44+
{
45+
return expr_dynamic_cast<
46+
T,
47+
typename remove_constt<typename ptr_typet<T>::type>::type,
48+
const exprt>(base);
49+
}
50+
51+
/// \brief Cast a pointer to a generic exprt to a specific derived class
52+
/// \tparam T The exprt-derived class to cast to
53+
/// \param base Pointer to a generic \ref exprt
54+
/// \return Pointer to object of type \a T or null if \a base is not an instance of \a T
55+
template<typename T>
56+
T expr_dynamic_cast(exprt *base)
57+
{
58+
return expr_dynamic_cast<T, typename ptr_typet<T>::type, exprt>(base);
59+
}
60+
61+
/// \brief Cast a pointer to a generic exprt to a specific derived class
62+
/// \tparam T The pointer or const pointer type to \a TUnderlying to cast to
63+
/// \tparam TUnderlying An exprt-derived class type
64+
/// \param base Pointer to a generic \ref exprt
65+
/// \return Pointer to object of type \a TUnderlying
66+
/// or null if \a base is not an instance of \a TUnderlying
67+
template<typename T, typename TUnderlying, typename TExpr>
68+
T expr_dynamic_cast(TExpr *base)
69+
{
70+
static_assert(
71+
std::is_base_of<exprt, TUnderlying>::value,
72+
"The template argument T must be derived from exprt.");
73+
if(base == nullptr)
74+
return nullptr;
75+
if(!check_expr_type<TUnderlying>(*base))
76+
return nullptr;
77+
T value=static_cast<T>(base);
78+
validate_expr<TUnderlying>(*value);
79+
return value;
80+
}
81+
82+
/// \brief Cast a constant reference to a generic exprt to a specific derived class
83+
/// \tparam T The exprt-derived class to cast to
84+
/// \param base Reference to a generic \ref exprt
85+
/// \return Reference to object of type \a T
86+
/// \throw std::bad_cast If \a base is not an instance of \a T
87+
template<typename T>
88+
T expr_dynamic_cast(const exprt &base)
89+
{
90+
return expr_dynamic_cast<
91+
T,
92+
typename remove_constt<typename ref_typet<T>::type>::type,
93+
const exprt>(base);
94+
}
95+
96+
/// \brief Cast a reference to a generic exprt to a specific derived class
97+
/// \tparam T The exprt-derived class to cast to
98+
/// \param base Reference to a generic \ref exprt
99+
/// \return Reference to object of type \a T
100+
/// \throw std::bad_cast If \a base is not an instance of \a T
101+
template<typename T>
102+
T expr_dynamic_cast(exprt &base)
103+
{
104+
return expr_dynamic_cast<T, typename ref_typet<T>::type, exprt>(base);
105+
}
106+
107+
/// \brief Cast a reference to a generic exprt to a specific derived class
108+
/// \tparam T The reference or const reference type to \a TUnderlying to cast to
109+
/// \tparam TUnderlying An exprt-derived class type
110+
/// \param base Reference to a generic \ref exprt
111+
/// \return Reference to object of type \a T
112+
/// \throw std::bad_cast If \a base is not an instance of \a TUnderlying
113+
template<typename T, typename TUnderlying, typename TExpr>
114+
T expr_dynamic_cast(TExpr &base)
115+
{
116+
static_assert(
117+
std::is_base_of<exprt, TUnderlying>::value,
118+
"The template argument T must be derived from exprt.");
119+
if(!check_expr_type<TUnderlying>(base))
120+
throw std::bad_cast();
121+
T value=static_cast<T>(base);
122+
validate_expr<TUnderlying>(value);
123+
return value;
124+
}
125+
126+
127+
inline void validate_operands(
128+
const exprt &value,
129+
exprt::operandst::size_type number,
130+
const char *message,
131+
bool allowMore=false)
132+
{
133+
DATA_INVARIANT(
134+
allowMore
135+
? value.operands().size()==number
136+
: value.operands().size()>=number,
137+
message);
138+
}
139+
140+
#endif // CPROVER_UTIL_EXPR_CAST_H

0 commit comments

Comments
 (0)