cprover
expr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_UTIL_EXPR_H
10 #define CPROVER_UTIL_EXPR_H
11 
12 #include "deprecate.h"
13 #include "type.h"
14 #include "validate_expressions.h"
15 #include "validate_types.h"
16 #include "validation_mode.h"
17 
18 #define forall_operands(it, expr) \
19  if((expr).has_operands()) /* NOLINT(readability/braces) */ \
20  for(exprt::operandst::const_iterator it=(expr).operands().begin(), \
21  it##_end=(expr).operands().end(); \
22  it!=it##_end; ++it)
23 
24 #define Forall_operands(it, expr) \
25  if((expr).has_operands()) /* NOLINT(readability/braces) */ \
26  for(exprt::operandst::iterator it=(expr).operands().begin(); \
27  it!=(expr).operands().end(); ++it)
28 
29 #define forall_expr(it, expr) \
30  for(exprt::operandst::const_iterator it=(expr).begin(); \
31  it!=(expr).end(); ++it)
32 
33 #define Forall_expr(it, expr) \
34  for(exprt::operandst::iterator it=(expr).begin(); \
35  it!=(expr).end(); ++it)
36 
37 class depth_iteratort;
40 
52 class exprt:public irept
53 {
54 public:
55  typedef std::vector<exprt> operandst;
56 
57  // constructors
58  exprt() { }
59  explicit exprt(const irep_idt &_id):irept(_id) { }
60 
61  exprt(irep_idt _id, typet _type)
62  : irept(std::move(_id), {{ID_type, std::move(_type)}}, {})
63  {
64  }
65 
66  exprt(irep_idt _id, typet _type, operandst &&_operands)
67  : irept(
68  std::move(_id),
69  {{ID_type, std::move(_type)}},
70  std::move((irept::subt &&) _operands))
71  {
72  }
73 
75  : exprt(id, std::move(type))
76  {
77  add_source_location() = std::move(loc);
78  }
79 
81  typet &type() { return static_cast<typet &>(add(ID_type)); }
82  const typet &type() const
83  {
84  return static_cast<const typet &>(find(ID_type));
85  }
86 
89  std::size_t size() const;
90 
92  bool has_operands() const
93  { return !operands().empty(); }
94 
96  { return (operandst &)get_sub(); }
97 
98  const operandst &operands() const
99  { return (const operandst &)get_sub(); }
100 
102  { return operands().front(); }
103 
105  { return operands()[1]; }
106 
108  { return operands()[2]; }
109 
111  { return operands()[3]; }
112 
113  const exprt &op0() const
114  { return operands().front(); }
115 
116  const exprt &op1() const
117  { return operands()[1]; }
118 
119  const exprt &op2() const
120  { return operands()[2]; }
121 
122  const exprt &op3() const
123  { return operands()[3]; }
124 
126  { operands().reserve(n) ; }
127 
128  DEPRECATED(SINCE(2018, 10, 1, "use add_to_operands(std::move(expr)) instead"))
129  void move_to_operands(exprt &expr);
130 
132  2018,
133  10,
134  1,
135  "use add_to_operands(std::move(e1), std::move(e2)) instead"))
136  void move_to_operands(exprt &e1, exprt &e2);
137 
139  2018,
140  10,
141  1,
142  "use add_to_operands(std::move(e1), std::move(e2), std::move(e3))"
143  "instead"))
144  void move_to_operands(exprt &e1, exprt &e2, exprt &e3);
145 
148  void copy_to_operands(const exprt &expr)
149  {
150  operands().push_back(expr);
151  }
152 
155  void add_to_operands(const exprt &expr)
156  {
157  copy_to_operands(expr);
158  }
159 
162  void add_to_operands(exprt &&expr)
163  {
164  operands().push_back(std::move(expr));
165  }
166 
170  void copy_to_operands(const exprt &e1, const exprt &e2)
171  {
172  operandst &op = operands();
173  #ifndef USE_LIST
174  op.reserve(op.size() + 2);
175  #endif
176  op.push_back(e1);
177  op.push_back(e2);
178  }
179 
183  void add_to_operands(const exprt &e1, const exprt &e2)
184  {
185  copy_to_operands(e1, e2);
186  }
187 
191  void add_to_operands(exprt &&e1, exprt &&e2)
192  {
193  operandst &op = operands();
194  #ifndef USE_LIST
195  op.reserve(op.size() + 2);
196  #endif
197  op.push_back(std::move(e1));
198  op.push_back(std::move(e2));
199  }
200 
205  void add_to_operands(const exprt &e1, const exprt &e2, const exprt &e3)
206  {
207  copy_to_operands(e1, e2, e3);
208  }
209 
214  void copy_to_operands(const exprt &e1, const exprt &e2, const exprt &e3)
215  {
216  operandst &op = operands();
217  #ifndef USE_LIST
218  op.reserve(op.size() + 3);
219  #endif
220  op.push_back(e1);
221  op.push_back(e2);
222  op.push_back(e3);
223  }
224 
229  void add_to_operands(exprt &&e1, exprt &&e2, exprt &&e3)
230  {
231  operandst &op = operands();
232  #ifndef USE_LIST
233  op.reserve(op.size() + 3);
234  #endif
235  op.push_back(std::move(e1));
236  op.push_back(std::move(e2));
237  op.push_back(std::move(e3));
238  }
239 
240  DEPRECATED(SINCE(2019, 1, 19, "use typecast_exprt() instead"))
241  void make_typecast(const typet &_type);
242 
243  DEPRECATED(SINCE(2019, 5, 28, "use make_boolean_expr(value) instead"))
244  void make_bool(bool value);
245 
246  bool is_constant() const;
247  bool is_true() const;
248  bool is_false() const;
249  bool is_zero() const;
250  bool is_one() const;
251  bool is_boolean() const;
252 
253  const source_locationt &find_source_location() const;
254 
256  {
257  return static_cast<const source_locationt &>(find(ID_C_source_location));
258  }
259 
261  {
262  return static_cast<source_locationt &>(add(ID_C_source_location));
263  }
264 
266  {
267  remove(ID_C_source_location);
268  }
269 
278  static void check(const exprt &, const validation_modet)
279  {
280  }
281 
290  static void validate(
291  const exprt &expr,
292  const namespacet &,
294  {
295  check_expr(expr, vm);
296  }
297 
306  static void validate_full(
307  const exprt &expr,
308  const namespacet &ns,
310  {
311  // first check operands (if any)
312  for(const exprt &op : expr.operands())
313  {
314  validate_full_expr(op, ns, vm);
315  }
316 
317  // type may be nil
318  const typet &t = expr.type();
319 
320  validate_full_type(t, ns, vm);
321 
322  validate_expr(expr, ns, vm);
323  }
324 
325 protected:
326  exprt &add_expr(const irep_idt &name)
327  {
328  return static_cast<exprt &>(add(name));
329  }
330 
331  const exprt &find_expr(const irep_idt &name) const
332  {
333  return static_cast<const exprt &>(find(name));
334  }
335 
336 public:
340  void visit(class expr_visitort &visitor);
341  void visit(class const_expr_visitort &visitor) const;
342  void visit_pre(std::function<void(exprt &)>);
343  void visit_pre(std::function<void(const exprt &)>) const;
344 
348  void visit_post(std::function<void(exprt &)>);
349  void visit_post(std::function<void(const exprt &)>) const;
350 
357  depth_iteratort depth_begin(std::function<exprt &()> mutate_root) const;
362 };
363 
367 class expr_protectedt : public exprt
368 {
369 protected:
370  // constructors
372  : exprt(std::move(_id), std::move(_type))
373  {
374  }
375 
376  expr_protectedt(irep_idt _id, typet _type, operandst _operands)
377  : exprt(std::move(_id), std::move(_type), std::move(_operands))
378  {
379  }
380 
381  // protect these low-level methods
382  using exprt::add;
383  using exprt::make_bool;
384  using exprt::make_typecast;
385  using exprt::op0;
386  using exprt::op1;
387  using exprt::op2;
388  using exprt::op3;
389  using exprt::remove;
390 };
391 
393 {
394 public:
395  virtual ~expr_visitort() { }
396  virtual void operator()(exprt &) { }
397 };
398 
400 {
401 public:
402  virtual ~const_expr_visitort() { }
403  virtual void operator()(const exprt &) { }
404 };
405 
406 #endif // CPROVER_UTIL_EXPR_H
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:148
exprt::op2
exprt & op2()
Definition: expr.h:107
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
exprt::move_to_operands
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt's operands.
Definition: expr.cpp:41
exprt::depth_cbegin
const_depth_iteratort depth_cbegin() const
Definition: expr.cpp:349
const_unique_depth_iteratort
Definition: expr_iterator.h:282
exprt::op3
exprt & op3()
Definition: expr.h:110
exprt::find_expr
const exprt & find_expr(const irep_idt &name) const
Definition: expr.h:331
validate_full_type
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)
Definition: validate_types.cpp:103
expr_visitort::operator()
virtual void operator()(exprt &)
Definition: expr.h:396
exprt::depth_begin
depth_iteratort depth_begin()
Definition: expr.cpp:341
const_expr_visitort::~const_expr_visitort
virtual ~const_expr_visitort()
Definition: expr.h:402
exprt::size
std::size_t size() const
Amount of nodes this expression tree contains.
Definition: expr.cpp:26
typet
The type of an expression, extends irept.
Definition: type.h:28
check_expr
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...
Definition: validate_expressions.cpp:67
exprt::add_to_operands
void add_to_operands(exprt &&e1, exprt &&e2)
Add the given arguments to the end of exprt's operands.
Definition: expr.h:191
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
depth_iteratort
Definition: expr_iterator.h:225
exprt::make_bool
void make_bool(bool value)
Replace the expression by a Boolean expression representing value.
Definition: expr.cpp:121
exprt::exprt
exprt()
Definition: expr.h:58
exprt
Base class for all expressions.
Definition: expr.h:52
exprt::exprt
exprt(const irep_idt &_id)
Definition: expr.h:59
exprt::validate_full
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:306
exprt::op0
exprt & op0()
Definition: expr.h:101
const_expr_visitort::operator()
virtual void operator()(const exprt &)
Definition: expr.h:403
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:102
exprt::copy_to_operands
void copy_to_operands(const exprt &e1, const exprt &e2)
Copy the given arguments to the end of exprt's operands.
Definition: expr.h:170
exprt::add_to_operands
void add_to_operands(exprt &&expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:162
exprt::visit
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:331
validate_expr
void validate_expr(const byte_extract_exprt &value)
Definition: byte_operators.h:79
expr_visitort
Definition: expr.h:392
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:111
type.h
exprt::add_to_operands
void add_to_operands(const exprt &e1, const exprt &e2)
Add the given arguments to the end of exprt's operands.
Definition: expr.h:183
exprt::exprt
exprt(const irep_idt &id, typet type, source_locationt loc)
Definition: expr.h:74
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
exprt::operands
const operandst & operands() const
Definition: expr.h:98
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
const_depth_iteratort
Definition: expr_iterator.h:214
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:92
deprecate.h
exprt::visit_post
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:292
exprt::find_source_location
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:241
expr_visitort::~expr_visitort
virtual ~expr_visitort()
Definition: expr.h:395
exprt::op1
exprt & op1()
Definition: expr.h:104
const_expr_visitort
Definition: expr.h:399
validation_modet
validation_modet
Definition: validation_mode.h:12
irept::id
const irep_idt & id() const
Definition: irep.h:418
irept::remove
void remove(const irep_namet &name)
Definition: irep.cpp:93
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
validation_mode.h
exprt::copy_to_operands
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:214
exprt::type
const typet & type() const
Definition: expr.h:82
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
exprt::drop_source_location
void drop_source_location()
Definition: expr.h:265
sharing_treet< irept, std::map< irep_namet, irept > >::subt
typename dt::subt subt
Definition: irep.h:182
source_locationt
Definition: source_location.h:19
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:142
exprt::op1
const exprt & op1() const
Definition: expr.h:116
exprt::add_to_operands
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:205
exprt::check
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:278
exprt::op0
const exprt & op0() const
Definition: expr.h:113
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
exprt::add_expr
exprt & add_expr(const irep_idt &name)
Definition: expr.h:326
exprt::add_to_operands
void add_to_operands(exprt &&e1, exprt &&e2, exprt &&e3)
Add the given arguments to the end of exprt's operands.
Definition: expr.h:229
exprt::depth_cend
const_depth_iteratort depth_cend() const
Definition: expr.cpp:351
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:95
expr_protectedt::expr_protectedt
expr_protectedt(irep_idt _id, typet _type, operandst _operands)
Definition: expr.h:376
irept::get_sub
subt & get_sub()
Definition: irep.h:477
exprt::unique_depth_cend
const_unique_depth_iteratort unique_depth_cend() const
Definition: expr.cpp:364
exprt::visit_pre
void visit_pre(std::function< void(exprt &)>)
Definition: expr.cpp:321
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:155
validate_full_expr
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...
Definition: validate_expressions.cpp:96
exprt::exprt
exprt(irep_idt _id, typet _type, operandst &&_operands)
Definition: expr.h:66
validate_expressions.h
exprt::is_one
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:192
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:381
make_boolean_expr
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Definition: expr_util.cpp:285
exprt::operands
operandst & operands()
Definition: expr.h:95
expr_protectedt::expr_protectedt
expr_protectedt(irep_idt _id, typet _type)
Definition: expr.h:371
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:260
exprt::make_typecast
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Definition: expr.cpp:86
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
exprt::unique_depth_begin
const_unique_depth_iteratort unique_depth_begin() const
Definition: expr.cpp:358
validate_types.h
exprt::validate
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:290
exprt::unique_depth_cbegin
const_unique_depth_iteratort unique_depth_cbegin() const
Definition: expr.cpp:362
exprt::unique_depth_end
const_unique_depth_iteratort unique_depth_end() const
Definition: expr.cpp:360
exprt::depth_end
depth_iteratort depth_end()
Definition: expr.cpp:343
exprt::is_boolean
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.cpp:129
exprt::exprt
exprt(irep_idt _id, typet _type)
Definition: expr.h:61
exprt::reserve_operands
void reserve_operands(operandst::size_type n)
Definition: expr.h:125
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:255
exprt::op3
const exprt & op3() const
Definition: expr.h:122
expr_protectedt
Base class for all expressions.
Definition: expr.h:367
validation_modet::INVARIANT
exprt::op2
const exprt & op2() const
Definition: expr.h:119