CBMC
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 #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 
40 class depth_iteratort;
43 
55 class exprt:public irept
56 {
57 public:
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 
124 protected:
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 
149 public:
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 
169  void add_to_operands(exprt &&expr)
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 
221  const source_locationt &find_source_location() const;
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 
293 protected:
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 
304 public:
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 
335 class expr_protectedt : public exprt
336 {
337 protected:
338  // constructors
340  : exprt(std::move(_id), std::move(_type))
341  {
342  }
343 
344  expr_protectedt(irep_idt _id, typet _type, operandst _operands)
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 {
360 public:
361  virtual ~expr_visitort() { }
362  virtual void operator()(exprt &) { }
363 };
364 
366 {
367 public:
368  virtual ~const_expr_visitort() { }
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
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
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:96
exprt & op3()
Definition: expr.h:134
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:91
const exprt & op3() const
Definition: expr.h:146
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
exprt & op1()
Definition: expr.h:128
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
exprt & add_expr(const irep_idt &name)
Definition: expr.h:294
const typet & type() const
Definition: expr.h:85
depth_iteratort depth_end()
Definition: expr.cpp:249
const_depth_iteratort depth_cend() const
Definition: expr.cpp:257
source_locationt & add_source_location()
Definition: expr.h:228
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 source_locationt & source_location() const
Definition: expr.h:223
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
exprt & op2()
Definition: expr.h:131
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
const exprt & op2() const
Definition: expr.h:143
void visit_pre(std::function< void(exprt &)>)
Definition: expr.cpp:227
typet & type()
Return the type of the expression.
Definition: expr.h:84
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(irep_idt _id, typet _type, operandst &&_operands)
Definition: expr.h:69
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.h:204
exprt & op0()
Definition: expr.h:125
const exprt & op0() const
Definition: expr.h:137
exprt(const irep_idt &_id)
Definition: expr.h:62
const_depth_iteratort depth_cbegin() const
Definition: expr.cpp:255
const operandst & operands() const
Definition: expr.h:97
operandst & operands()
Definition: expr.h:94
T && with_source_location(const exprt &other) &&
Add the source location from other, if it has any.
Definition: expr.h:114
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
const exprt & find_expr(const irep_idt &name) const
Definition: expr.h:299
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
T & with_source_location(const exprt &other) &
Add the source location from other, if it has any.
Definition: expr.h:102
void drop_source_location()
Definition: expr.h:233
const_unique_depth_iteratort unique_depth_cbegin() const
Definition: expr.cpp:268
const exprt & op1() const
Definition: expr.h:140
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
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:372
subt & get_sub()
Definition: irep.h:456
const irept & find(const irep_idt &name) const
Definition: irep.cpp:101
void remove(const irep_idt &name)
Definition: irep.cpp:95
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
Defines typet, type_with_subtypet and type_with_subtypest.
#define size_type
Definition: unistd.c:312
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