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 "as_const.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  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 
38 class depth_iteratort;
41 
53 class exprt:public irept
54 {
55 public:
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 
90  std::size_t bounded_size(std::size_t limit) const;
91 
93  bool has_operands() const
94  { return !operands().empty(); }
95 
97  { return (operandst &)get_sub(); }
98 
99  const operandst &operands() const
100  { return (const operandst &)get_sub(); }
101 
102 protected:
104  { return operands().front(); }
105 
107  { return operands()[1]; }
108 
110  { return operands()[2]; }
111 
113  { return operands()[3]; }
114 
115  const exprt &op0() const
116  { return operands().front(); }
117 
118  const exprt &op1() const
119  { return operands()[1]; }
120 
121  const exprt &op2() const
122  { return operands()[2]; }
123 
124  const exprt &op3() const
125  { return operands()[3]; }
126 
129  std::size_t bounded_size(std::size_t count, std::size_t limit) const;
130 
131 public:
133  { operands().reserve(n) ; }
134 
137  void copy_to_operands(const exprt &expr)
138  {
139  operands().push_back(expr);
140  }
141 
144  void add_to_operands(const exprt &expr)
145  {
146  copy_to_operands(expr);
147  }
148 
151  void add_to_operands(exprt &&expr)
152  {
153  operands().push_back(std::move(expr));
154  }
155 
159  void copy_to_operands(const exprt &e1, const exprt &e2)
160  {
161  operandst &op = operands();
162  #ifndef USE_LIST
163  op.reserve(op.size() + 2);
164  #endif
165  op.push_back(e1);
166  op.push_back(e2);
167  }
168 
172  void add_to_operands(const exprt &e1, const exprt &e2)
173  {
174  copy_to_operands(e1, e2);
175  }
176 
180  void add_to_operands(exprt &&e1, exprt &&e2)
181  {
182  operandst &op = operands();
183  #ifndef USE_LIST
184  op.reserve(op.size() + 2);
185  #endif
186  op.push_back(std::move(e1));
187  op.push_back(std::move(e2));
188  }
189 
194  void add_to_operands(const exprt &e1, const exprt &e2, const exprt &e3)
195  {
196  copy_to_operands(e1, e2, e3);
197  }
198 
203  void copy_to_operands(const exprt &e1, const exprt &e2, const exprt &e3)
204  {
205  operandst &op = operands();
206  #ifndef USE_LIST
207  op.reserve(op.size() + 3);
208  #endif
209  op.push_back(e1);
210  op.push_back(e2);
211  op.push_back(e3);
212  }
213 
218  void add_to_operands(exprt &&e1, exprt &&e2, exprt &&e3)
219  {
220  operandst &op = operands();
221  #ifndef USE_LIST
222  op.reserve(op.size() + 3);
223  #endif
224  op.push_back(std::move(e1));
225  op.push_back(std::move(e2));
226  op.push_back(std::move(e3));
227  }
228 
229  bool is_constant() const;
230  bool is_true() const;
231  bool is_false() const;
232  bool is_zero() const;
233  bool is_one() const;
234  bool is_boolean() const;
235 
236  const source_locationt &find_source_location() const;
237 
239  {
240  return static_cast<const source_locationt &>(find(ID_C_source_location));
241  }
242 
244  {
245  return static_cast<source_locationt &>(add(ID_C_source_location));
246  }
247 
249  {
250  remove(ID_C_source_location);
251  }
252 
261  static void check(const exprt &, const validation_modet)
262  {
263  }
264 
273  static void validate(
274  const exprt &expr,
275  const namespacet &,
277  {
278  check_expr(expr, vm);
279  }
280 
289  static void validate_full(
290  const exprt &expr,
291  const namespacet &ns,
293  {
294  // first check operands (if any)
295  for(const exprt &op : expr.operands())
296  {
297  validate_full_expr(op, ns, vm);
298  }
299 
300  // type may be nil
301  const typet &t = expr.type();
302 
303  validate_full_type(t, ns, vm);
304 
305  validate_expr(expr, ns, vm);
306  }
307 
308 protected:
309  exprt &add_expr(const irep_idt &name)
310  {
311  return static_cast<exprt &>(add(name));
312  }
313 
314  const exprt &find_expr(const irep_idt &name) const
315  {
316  return static_cast<const exprt &>(find(name));
317  }
318 
319 public:
323  void visit(class expr_visitort &visitor);
324  void visit(class const_expr_visitort &visitor) const;
325  void visit_pre(std::function<void(exprt &)>);
326  void visit_pre(std::function<void(const exprt &)>) const;
327 
331  void visit_post(std::function<void(exprt &)>);
332  void visit_post(std::function<void(const exprt &)>) const;
333 
340  depth_iteratort depth_begin(std::function<exprt &()> mutate_root) const;
345 };
346 
350 class expr_protectedt : public exprt
351 {
352 protected:
353  // constructors
355  : exprt(std::move(_id), std::move(_type))
356  {
357  }
358 
359  expr_protectedt(irep_idt _id, typet _type, operandst _operands)
360  : exprt(std::move(_id), std::move(_type), std::move(_operands))
361  {
362  }
363 
364  // protect these low-level methods
365  using exprt::add;
366  using exprt::op0;
367  using exprt::op1;
368  using exprt::op2;
369  using exprt::op3;
370  using exprt::remove;
371 };
372 
374 {
375 public:
376  virtual ~expr_visitort() { }
377  virtual void operator()(exprt &) { }
378 };
379 
381 {
382 public:
383  virtual ~const_expr_visitort() { }
384  virtual void operator()(const exprt &) { }
385 };
386 
387 #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:137
exprt::op2
exprt & op2()
Definition: expr.h:109
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
exprt::depth_cbegin
const_depth_iteratort depth_cbegin() const
Definition: expr.cpp:300
const_unique_depth_iteratort
Definition: expr_iterator.h:287
exprt::op3
exprt & op3()
Definition: expr.h:112
exprt::find_expr
const exprt & find_expr(const irep_idt &name) const
Definition: expr.h:314
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:110
expr_visitort::operator()
virtual void operator()(exprt &)
Definition: expr.h:377
exprt::depth_begin
depth_iteratort depth_begin()
Definition: expr.cpp:292
const_expr_visitort::~const_expr_visitort
virtual ~const_expr_visitort()
Definition: expr.h:383
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:68
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:180
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:122
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:112
depth_iteratort
Definition: expr_iterator.h:230
exprt::exprt
exprt()
Definition: expr.h:59
exprt
Base class for all expressions.
Definition: expr.h:54
exprt::exprt
exprt(const irep_idt &_id)
Definition: expr.h:60
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:289
exprt::op0
exprt & op0()
Definition: expr.h:103
const_expr_visitort::operator()
virtual void operator()(const exprt &)
Definition: expr.h:384
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:60
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:159
exprt::add_to_operands
void add_to_operands(exprt &&expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:151
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:282
validate_expr
void validate_expr(const shuffle_vector_exprt &value)
Definition: c_expr.h:81
expr_visitort
Definition: expr.h:374
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:69
type.h
Defines typet, type_with_subtypet and type_with_subtypest.
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:172
exprt::exprt
exprt(const irep_idt &id, typet type, source_locationt loc)
Definition: expr.h:75
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::operands
const operandst & operands() const
Definition: expr.h:99
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
const_depth_iteratort
Definition: expr_iterator.h:219
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:93
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:243
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:192
expr_visitort::~expr_visitort
virtual ~expr_visitort()
Definition: expr.h:376
exprt::bounded_size
std::size_t bounded_size(std::size_t limit) const
Amount of nodes in this expression tree approximately bounded by limit.
Definition: expr.cpp:46
exprt::op1
exprt & op1()
Definition: expr.h:106
const_expr_visitort
Definition: expr.h:381
validation_modet
validation_modet
Definition: validation_mode.h:13
irept::id
const irep_idt & id() const
Definition: irep.h:407
irept::remove
void remove(const irep_namet &name)
Definition: irep.cpp:102
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
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:203
exprt::type
const typet & type() const
Definition: expr.h:83
exprt::drop_source_location
void drop_source_location()
Definition: expr.h:248
sharing_treet< irept, forward_list_as_mapt< irep_namet, irept > >::subt
typename dt::subt subt
Definition: irep.h:171
source_locationt
Definition: source_location.h:20
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:91
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:194
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:261
exprt::add_expr
exprt & add_expr(const irep_idt &name)
Definition: expr.h:309
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:218
exprt::depth_cend
const_depth_iteratort depth_cend() const
Definition: expr.cpp:302
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:53
expr_protectedt::expr_protectedt
expr_protectedt(irep_idt _id, typet _type, operandst _operands)
Definition: expr.h:359
irept::get_sub
subt & get_sub()
Definition: irep.h:467
exprt::unique_depth_cend
const_unique_depth_iteratort unique_depth_cend() const
Definition: expr.cpp:315
exprt::visit_pre
void visit_pre(std::function< void(exprt &)>)
Definition: expr.cpp:272
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:144
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:97
exprt::exprt
exprt(irep_idt _id, typet _type, operandst &&_operands)
Definition: expr.h:67
validate_expressions.h
exprt::is_one
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:141
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
exprt::operands
operandst & operands()
Definition: expr.h:96
expr_protectedt::expr_protectedt
expr_protectedt(irep_idt _id, typet _type)
Definition: expr.h:354
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:243
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:309
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:273
exprt::unique_depth_cbegin
const_unique_depth_iteratort unique_depth_cbegin() const
Definition: expr.cpp:313
exprt::unique_depth_end
const_unique_depth_iteratort unique_depth_end() const
Definition: expr.cpp:311
exprt::depth_end
depth_iteratort depth_end()
Definition: expr.cpp:294
exprt::is_boolean
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.cpp:78
exprt::exprt
exprt(irep_idt _id, typet _type)
Definition: expr.h:62
exprt::reserve_operands
void reserve_operands(operandst::size_type n)
Definition: expr.h:132
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:238
as_const.h
expr_protectedt
Base class for all expressions.
Definition: expr.h:351