cprover
Loading...
Searching...
No Matches
expr.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#ifndef CPROVER_UTIL_EXPR_H
10#define CPROVER_UTIL_EXPR_H
11
12#include "as_const.h"
13#include "type.h"
15#include "validate_types.h"
16#include "validation_mode.h"
17
18#include <functional>
19
20#define forall_operands(it, expr) \
21 for(exprt::operandst::const_iterator \
22 it = as_const(expr).operands().begin(), \
23 it##_end = as_const(expr).operands().end(); \
24 it != it##_end; \
25 ++it)
26
27#define Forall_operands(it, expr) \
28 if((expr).has_operands()) /* NOLINT(readability/braces) */ \
29 for(exprt::operandst::iterator it=(expr).operands().begin(); \
30 it!=(expr).operands().end(); ++it)
31
32#define forall_expr(it, expr) \
33 for(exprt::operandst::const_iterator it=(expr).begin(); \
34 it!=(expr).end(); ++it)
35
36#define Forall_expr(it, expr) \
37 for(exprt::operandst::iterator it=(expr).begin(); \
38 it!=(expr).end(); ++it)
39
40class depth_iteratort;
43
55class exprt:public irept
56{
57public:
58 typedef std::vector<exprt> operandst;
59
60 // constructors
61 exprt() { }
62 explicit exprt(const irep_idt &_id):irept(_id) { }
63
64 exprt(irep_idt _id, typet _type)
65 : irept(std::move(_id), {{ID_type, std::move(_type)}}, {})
66 {
67 }
68
69 exprt(irep_idt _id, typet _type, operandst &&_operands)
70 : irept(
71 std::move(_id),
72 {{ID_type, std::move(_type)}},
73 std::move((irept::subt &&) _operands))
74 {
75 }
76
78 : exprt(id, std::move(type))
79 {
80 add_source_location() = std::move(loc);
81 }
82
84 typet &type() { return static_cast<typet &>(add(ID_type)); }
85 const typet &type() const
86 {
87 return static_cast<const typet &>(find(ID_type));
88 }
89
91 bool has_operands() const
92 { return !operands().empty(); }
93
95 { return (operandst &)get_sub(); }
96
97 const operandst &operands() const
98 { return (const operandst &)get_sub(); }
99
101 template <typename T>
102 T &with_source_location(const exprt &other) &
103 {
104 static_assert(
105 std::is_base_of<exprt, T>::value,
106 "The template argument T must be derived from exprt.");
107 if(other.source_location().is_not_nil())
108 add_source_location() = other.source_location();
109 return *static_cast<T *>(this);
110 }
111
113 template <typename T>
114 T &&with_source_location(const exprt &other) &&
115 {
116 static_assert(
117 std::is_base_of<exprt, T>::value,
118 "The template argument T must be derived from exprt.");
119 if(other.source_location().is_not_nil())
120 add_source_location() = other.source_location();
121 return std::move(*static_cast<T *>(this));
122 }
123
124protected:
126 { return operands().front(); }
127
129 { return operands()[1]; }
130
132 { return operands()[2]; }
133
135 { return operands()[3]; }
136
137 const exprt &op0() const
138 { return operands().front(); }
139
140 const exprt &op1() const
141 { return operands()[1]; }
142
143 const exprt &op2() const
144 { return operands()[2]; }
145
146 const exprt &op3() const
147 { return operands()[3]; }
148
149public:
150 void reserve_operands(operandst::size_type n)
151 { operands().reserve(n) ; }
152
155 void copy_to_operands(const exprt &expr)
156 {
157 operands().push_back(expr);
158 }
159
162 void add_to_operands(const exprt &expr)
163 {
164 copy_to_operands(expr);
165 }
166
170 {
171 operands().push_back(std::move(expr));
172 }
173
177 void add_to_operands(exprt &&e1, exprt &&e2)
178 {
179 operandst &op = operands();
180 #ifndef USE_LIST
181 op.reserve(op.size() + 2);
182 #endif
183 op.push_back(std::move(e1));
184 op.push_back(std::move(e2));
185 }
186
191 void add_to_operands(exprt &&e1, exprt &&e2, exprt &&e3)
192 {
193 operandst &op = operands();
194 #ifndef USE_LIST
195 op.reserve(op.size() + 3);
196 #endif
197 op.push_back(std::move(e1));
198 op.push_back(std::move(e2));
199 op.push_back(std::move(e3));
200 }
201
204 bool is_constant() const
205 {
206 return id() == ID_constant;
207 }
208
209 bool is_true() const;
210 bool is_false() const;
211 bool is_zero() const;
212 bool is_one() const;
213
216 bool is_boolean() const
217 {
218 return type().id() == ID_bool;
219 }
220
222
224 {
225 return static_cast<const source_locationt &>(find(ID_C_source_location));
226 }
227
229 {
230 return static_cast<source_locationt &>(add(ID_C_source_location));
231 }
232
234 {
235 remove(ID_C_source_location);
236 }
237
246 static void check(const exprt &, const validation_modet)
247 {
248 }
249
258 static void validate(
259 const exprt &expr,
260 const namespacet &,
262 {
263 check_expr(expr, vm);
264 }
265
274 static void validate_full(
275 const exprt &expr,
276 const namespacet &ns,
278 {
279 // first check operands (if any)
280 for(const exprt &op : expr.operands())
281 {
282 validate_full_expr(op, ns, vm);
283 }
284
285 // type may be nil
286 const typet &t = expr.type();
287
288 validate_full_type(t, ns, vm);
289
290 validate_expr(expr, ns, vm);
291 }
292
293protected:
294 exprt &add_expr(const irep_idt &name)
295 {
296 return static_cast<exprt &>(add(name));
297 }
298
299 const exprt &find_expr(const irep_idt &name) const
300 {
301 return static_cast<const exprt &>(find(name));
302 }
303
304public:
308 void visit(class expr_visitort &visitor);
309 void visit(class const_expr_visitort &visitor) const;
310 void visit_pre(std::function<void(exprt &)>);
311 void visit_pre(std::function<void(const exprt &)>) const;
312
316 void visit_post(std::function<void(exprt &)>);
317 void visit_post(std::function<void(const exprt &)>) const;
318
325 depth_iteratort depth_begin(std::function<exprt &()> mutate_root) const;
330};
331
335class expr_protectedt : public exprt
336{
337protected:
338 // constructors
340 : exprt(std::move(_id), std::move(_type))
341 {
342 }
343
345 : exprt(std::move(_id), std::move(_type), std::move(_operands))
346 {
347 }
348
349 // protect these low-level methods
350 using exprt::add;
351 using exprt::op0;
352 using exprt::op1;
353 using exprt::op2;
354 using exprt::op3;
355 using exprt::remove;
356};
357
359{
360public:
361 virtual ~expr_visitort() { }
362 virtual void operator()(exprt &) { }
363};
364
366{
367public:
369 virtual void operator()(const exprt &) { }
370};
371
372#endif // CPROVER_UTIL_EXPR_H
void validate_expr(const shuffle_vector_exprt &value)
Definition c_expr.h:81
virtual void operator()(const exprt &)
Definition expr.h:369
virtual ~const_expr_visitort()
Definition expr.h:368
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:336
expr_protectedt(irep_idt _id, typet _type)
Definition expr.h:339
expr_protectedt(irep_idt _id, typet _type, operandst _operands)
Definition expr.h:344
virtual void operator()(exprt &)
Definition expr.h:362
virtual ~expr_visitort()
Definition expr.h:361
Base class for all expressions.
Definition expr.h:56
exprt & op3()
Definition expr.h:134
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:147
std::vector< exprt > operandst
Definition expr.h:58
const typet & type() const
Definition expr.h:85
bool is_one() const
Return whether the expression is a constant representing 1.
Definition expr.cpp:96
bool has_operands() const
Return true if there is at least one operand.
Definition expr.h:91
void add_to_operands(exprt &&e1, exprt &&e2, exprt &&e3)
Add the given arguments to the end of exprt's operands.
Definition expr.h:191
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:27
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Check that the expression is well-formed, assuming that its subexpressions and type have all ready be...
Definition expr.h:258
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition expr.h:155
depth_iteratort depth_end()
Definition expr.cpp:249
const_depth_iteratort depth_cend() const
Definition expr.cpp:257
exprt()
Definition expr.h:61
const_unique_depth_iteratort unique_depth_end() const
Definition expr.cpp:266
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:216
depth_iteratort depth_begin()
Definition expr.cpp:247
const_unique_depth_iteratort unique_depth_cend() const
Definition expr.cpp:270
void visit(class expr_visitort &visitor)
These are pre-order traversal visitors, i.e., the visitor is executed on a node before its children h...
Definition expr.cpp:237
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
void reserve_operands(operandst::size_type n)
Definition expr.h:150
static void check(const exprt &, const validation_modet)
Check that the expression is well-formed (shallow checks only, i.e., subexpressions and its type are ...
Definition expr.h:246
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition expr.cpp:47
void visit_pre(std::function< void(exprt &)>)
Definition expr.cpp:227
static void validate_full(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the expression is well-formed (full check, including checks of all subexpressions and the ...
Definition expr.h:274
exprt(irep_idt _id, typet _type)
Definition expr.h:64
exprt & add_expr(const irep_idt &name)
Definition expr.h:294
const exprt & op0() const
Definition expr.h:137
exprt & op0()
Definition expr.h:125
exprt(irep_idt _id, typet _type, operandst &&_operands)
Definition expr.h:69
exprt & op1()
Definition expr.h:128
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:204
typet & type()
Return the type of the expression.
Definition expr.h:84
exprt(const irep_idt &_id)
Definition expr.h:62
const_depth_iteratort depth_cbegin() const
Definition expr.cpp:255
const exprt & find_expr(const irep_idt &name) const
Definition expr.h:299
void visit_post(std::function< void(exprt &)>)
These are post-order traversal visitors, i.e., the visitor is executed on a node after its children h...
Definition expr.cpp:198
operandst & operands()
Definition expr.h:94
const operandst & operands() const
Definition expr.h:97
void add_to_operands(exprt &&e1, exprt &&e2)
Add the given arguments to the end of exprt's operands.
Definition expr.h:177
void add_to_operands(exprt &&expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:169
exprt(const irep_idt &id, typet type, source_locationt loc)
Definition expr.h:77
exprt & op2()
Definition expr.h:131
const source_locationt & source_location() const
Definition expr.h:223
T && with_source_location(const exprt &other) &&
Add the source location from other, if it has any.
Definition expr.h:114
source_locationt & add_source_location()
Definition expr.h:228
void drop_source_location()
Definition expr.h:233
const exprt & op3() const
Definition expr.h:146
const_unique_depth_iteratort unique_depth_cbegin() const
Definition expr.cpp:268
T & with_source_location(const exprt &other) &
Add the source location from other, if it has any.
Definition expr.h:102
const exprt & op2() const
Definition expr.h:143
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:162
const_unique_depth_iteratort unique_depth_begin() const
Definition expr.cpp:264
const exprt & op1() const
Definition expr.h:140
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:372
const irept & find(const irep_idt &name) const
Definition irep.cpp:101
void remove(const irep_idt &name)
Definition irep.cpp:95
subt & get_sub()
Definition irep.h:456
const irep_idt & id() const
Definition irep.h:396
irept & add(const irep_idt &name)
Definition irep.cpp:111
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The type of an expression, extends irept.
Definition type.h:29
STL namespace.
Defines typet, type_with_subtypet and type_with_subtypest.
void check_expr(const exprt &expr, const validation_modet vm)
Check that the given expression is well-formed (shallow checks only, i.e., subexpressions and its typ...
void validate_full_expr(const exprt &expr, const namespacet &ns, const validation_modet vm)
Check that the given expression is well-formed (full check, including checks of all subexpressions an...
void validate_full_type(const typet &type, const namespacet &ns, const validation_modet vm)
Check that the given type is well-formed (full check, including checks of subtypes)
validation_modet