cprover
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#define forall_operands(it, expr) \
19 for(exprt::operandst::const_iterator \
20 it = as_const(expr).operands().begin(), \
21 it##_end = as_const(expr).operands().end(); \
22 it != it##_end; \
23 ++it)
24
25#define Forall_operands(it, expr) \
26 if((expr).has_operands()) /* NOLINT(readability/braces) */ \
27 for(exprt::operandst::iterator it=(expr).operands().begin(); \
28 it!=(expr).operands().end(); ++it)
29
30#define forall_expr(it, expr) \
31 for(exprt::operandst::const_iterator it=(expr).begin(); \
32 it!=(expr).end(); ++it)
33
34#define Forall_expr(it, expr) \
35 for(exprt::operandst::iterator it=(expr).begin(); \
36 it!=(expr).end(); ++it)
37
38class depth_iteratort;
41
53class exprt:public irept
54{
55public:
56 typedef std::vector<exprt> operandst;
57
58 // constructors
59 exprt() { }
60 explicit exprt(const irep_idt &_id):irept(_id) { }
61
62 exprt(irep_idt _id, typet _type)
63 : irept(std::move(_id), {{ID_type, std::move(_type)}}, {})
64 {
65 }
66
67 exprt(irep_idt _id, typet _type, operandst &&_operands)
68 : irept(
69 std::move(_id),
70 {{ID_type, std::move(_type)}},
71 std::move((irept::subt &&) _operands))
72 {
73 }
74
76 : exprt(id, std::move(type))
77 {
78 add_source_location() = std::move(loc);
79 }
80
82 typet &type() { return static_cast<typet &>(add(ID_type)); }
83 const typet &type() const
84 {
85 return static_cast<const typet &>(find(ID_type));
86 }
87
89 bool has_operands() const
90 { return !operands().empty(); }
91
93 { return (operandst &)get_sub(); }
94
95 const operandst &operands() const
96 { return (const operandst &)get_sub(); }
97
98protected:
100 { return operands().front(); }
101
103 { return operands()[1]; }
104
106 { return operands()[2]; }
107
109 { return operands()[3]; }
110
111 const exprt &op0() const
112 { return operands().front(); }
113
114 const exprt &op1() const
115 { return operands()[1]; }
116
117 const exprt &op2() const
118 { return operands()[2]; }
119
120 const exprt &op3() const
121 { return operands()[3]; }
122
123public:
125 { operands().reserve(n) ; }
126
129 void copy_to_operands(const exprt &expr)
130 {
131 operands().push_back(expr);
132 }
133
136 void add_to_operands(const exprt &expr)
137 {
138 copy_to_operands(expr);
139 }
140
144 {
145 operands().push_back(std::move(expr));
146 }
147
151 void copy_to_operands(const exprt &e1, const exprt &e2)
152 {
153 operandst &op = operands();
154 #ifndef USE_LIST
155 op.reserve(op.size() + 2);
156 #endif
157 op.push_back(e1);
158 op.push_back(e2);
159 }
160
164 void add_to_operands(const exprt &e1, const exprt &e2)
165 {
166 copy_to_operands(e1, e2);
167 }
168
172 void add_to_operands(exprt &&e1, exprt &&e2)
173 {
174 operandst &op = operands();
175 #ifndef USE_LIST
176 op.reserve(op.size() + 2);
177 #endif
178 op.push_back(std::move(e1));
179 op.push_back(std::move(e2));
180 }
181
186 void add_to_operands(const exprt &e1, const exprt &e2, const exprt &e3)
187 {
188 copy_to_operands(e1, e2, e3);
189 }
190
195 void copy_to_operands(const exprt &e1, const exprt &e2, const exprt &e3)
196 {
197 operandst &op = operands();
198 #ifndef USE_LIST
199 op.reserve(op.size() + 3);
200 #endif
201 op.push_back(e1);
202 op.push_back(e2);
203 op.push_back(e3);
204 }
205
210 void add_to_operands(exprt &&e1, exprt &&e2, exprt &&e3)
211 {
212 operandst &op = operands();
213 #ifndef USE_LIST
214 op.reserve(op.size() + 3);
215 #endif
216 op.push_back(std::move(e1));
217 op.push_back(std::move(e2));
218 op.push_back(std::move(e3));
219 }
220
221 bool is_constant() const;
222 bool is_true() const;
223 bool is_false() const;
224 bool is_zero() const;
225 bool is_one() const;
226 bool is_boolean() const;
227
229
231 {
232 return static_cast<const source_locationt &>(find(ID_C_source_location));
233 }
234
236 {
237 return static_cast<source_locationt &>(add(ID_C_source_location));
238 }
239
241 {
242 remove(ID_C_source_location);
243 }
244
253 static void check(const exprt &, const validation_modet)
254 {
255 }
256
265 static void validate(
266 const exprt &expr,
267 const namespacet &,
269 {
270 check_expr(expr, vm);
271 }
272
281 static void validate_full(
282 const exprt &expr,
283 const namespacet &ns,
285 {
286 // first check operands (if any)
287 for(const exprt &op : expr.operands())
288 {
289 validate_full_expr(op, ns, vm);
290 }
291
292 // type may be nil
293 const typet &t = expr.type();
294
295 validate_full_type(t, ns, vm);
296
297 validate_expr(expr, ns, vm);
298 }
299
300protected:
301 exprt &add_expr(const irep_idt &name)
302 {
303 return static_cast<exprt &>(add(name));
304 }
305
306 const exprt &find_expr(const irep_idt &name) const
307 {
308 return static_cast<const exprt &>(find(name));
309 }
310
311public:
315 void visit(class expr_visitort &visitor);
316 void visit(class const_expr_visitort &visitor) const;
317 void visit_pre(std::function<void(exprt &)>);
318 void visit_pre(std::function<void(const exprt &)>) const;
319
323 void visit_post(std::function<void(exprt &)>);
324 void visit_post(std::function<void(const exprt &)>) const;
325
332 depth_iteratort depth_begin(std::function<exprt &()> mutate_root) const;
337};
338
342class expr_protectedt : public exprt
343{
344protected:
345 // constructors
347 : exprt(std::move(_id), std::move(_type))
348 {
349 }
350
352 : exprt(std::move(_id), std::move(_type), std::move(_operands))
353 {
354 }
355
356 // protect these low-level methods
357 using exprt::add;
358 using exprt::op0;
359 using exprt::op1;
360 using exprt::op2;
361 using exprt::op3;
362 using exprt::remove;
363};
364
366{
367public:
368 virtual ~expr_visitort() { }
369 virtual void operator()(exprt &) { }
370};
371
373{
374public:
376 virtual void operator()(const exprt &) { }
377};
378
379#endif // CPROVER_UTIL_EXPR_H
void validate_expr(const shuffle_vector_exprt &value)
Definition: c_expr.h:81
unsignedbv_typet size_type()
Definition: c_types.cpp:68
virtual void operator()(const exprt &)
Definition: expr.h:376
virtual ~const_expr_visitort()
Definition: expr.h:375
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:343
expr_protectedt(irep_idt _id, typet _type)
Definition: expr.h:346
expr_protectedt(irep_idt _id, typet _type, operandst _operands)
Definition: expr.h:351
virtual void operator()(exprt &)
Definition: expr.h:369
virtual ~expr_visitort()
Definition: expr.h:368
Base class for all expressions.
Definition: expr.h:54
void add_to_operands(const exprt &e1, const exprt &e2, const exprt &e3)
Add the given arguments to the end of exprt's operands.
Definition: expr.h:186
exprt & op3()
Definition: expr.h:108
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
std::vector< exprt > operandst
Definition: expr.h:56
void copy_to_operands(const exprt &e1, const exprt &e2, const exprt &e3)
Copy the given arguments to the end of exprt's operands.
Definition: expr.h:195
const typet & type() const
Definition: expr.h:83
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:114
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:89
void add_to_operands(exprt &&e1, exprt &&e2, exprt &&e3)
Add the given arguments to the end of exprt's operands.
Definition: expr.h:210
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
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:265
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:129
depth_iteratort depth_end()
Definition: expr.cpp:267
const_depth_iteratort depth_cend() const
Definition: expr.cpp:275
exprt()
Definition: expr.h:59
const_unique_depth_iteratort unique_depth_end() const
Definition: expr.cpp:284
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.cpp:51
depth_iteratort depth_begin()
Definition: expr.cpp:265
const_unique_depth_iteratort unique_depth_cend() const
Definition: expr.cpp:288
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:255
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
void reserve_operands(operandst::size_type n)
Definition: expr.h:124
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:253
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
void visit_pre(std::function< void(exprt &)>)
Definition: expr.cpp:245
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:281
exprt(irep_idt _id, typet _type)
Definition: expr.h:62
exprt & add_expr(const irep_idt &name)
Definition: expr.h:301
const exprt & op0() const
Definition: expr.h:111
exprt & op0()
Definition: expr.h:99
exprt(irep_idt _id, typet _type, operandst &&_operands)
Definition: expr.h:67
exprt & op1()
Definition: expr.h:102
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
typet & type()
Return the type of the expression.
Definition: expr.h:82
exprt(const irep_idt &_id)
Definition: expr.h:60
const_depth_iteratort depth_cbegin() const
Definition: expr.cpp:273
const exprt & find_expr(const irep_idt &name) const
Definition: expr.h:306
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:216
operandst & operands()
Definition: expr.h:92
const operandst & operands() const
Definition: expr.h:95
void add_to_operands(exprt &&e1, exprt &&e2)
Add the given arguments to the end of exprt's operands.
Definition: expr.h:172
void add_to_operands(exprt &&expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:143
exprt(const irep_idt &id, typet type, source_locationt loc)
Definition: expr.h:75
exprt & op2()
Definition: expr.h:105
const source_locationt & source_location() const
Definition: expr.h:230
void copy_to_operands(const exprt &e1, const exprt &e2)
Copy the given arguments to the end of exprt's operands.
Definition: expr.h:151
void add_to_operands(const exprt &e1, const exprt &e2)
Add the given arguments to the end of exprt's operands.
Definition: expr.h:164
source_locationt & add_source_location()
Definition: expr.h:235
void drop_source_location()
Definition: expr.h:240
const exprt & op3() const
Definition: expr.h:120
const_unique_depth_iteratort unique_depth_cbegin() const
Definition: expr.cpp:286
const exprt & op2() const
Definition: expr.h:117
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
const_unique_depth_iteratort unique_depth_begin() const
Definition: expr.cpp:282
const exprt & op1() const
Definition: expr.h:114
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:106
void remove(const irep_idt &name)
Definition: irep.cpp:96
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:116
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