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 
202  bool is_constant() const;
203  bool is_true() const;
204  bool is_false() const;
205  bool is_zero() const;
206  bool is_one() const;
207  bool is_boolean() const;
208 
209  const source_locationt &find_source_location() const;
210 
212  {
213  return static_cast<const source_locationt &>(find(ID_C_source_location));
214  }
215 
217  {
218  return static_cast<source_locationt &>(add(ID_C_source_location));
219  }
220 
222  {
223  remove(ID_C_source_location);
224  }
225 
234  static void check(const exprt &, const validation_modet)
235  {
236  }
237 
246  static void validate(
247  const exprt &expr,
248  const namespacet &,
250  {
251  check_expr(expr, vm);
252  }
253 
262  static void validate_full(
263  const exprt &expr,
264  const namespacet &ns,
266  {
267  // first check operands (if any)
268  for(const exprt &op : expr.operands())
269  {
270  validate_full_expr(op, ns, vm);
271  }
272 
273  // type may be nil
274  const typet &t = expr.type();
275 
276  validate_full_type(t, ns, vm);
277 
278  validate_expr(expr, ns, vm);
279  }
280 
281 protected:
282  exprt &add_expr(const irep_idt &name)
283  {
284  return static_cast<exprt &>(add(name));
285  }
286 
287  const exprt &find_expr(const irep_idt &name) const
288  {
289  return static_cast<const exprt &>(find(name));
290  }
291 
292 public:
296  void visit(class expr_visitort &visitor);
297  void visit(class const_expr_visitort &visitor) const;
298  void visit_pre(std::function<void(exprt &)>);
299  void visit_pre(std::function<void(const exprt &)>) const;
300 
304  void visit_post(std::function<void(exprt &)>);
305  void visit_post(std::function<void(const exprt &)>) const;
306 
313  depth_iteratort depth_begin(std::function<exprt &()> mutate_root) const;
318 };
319 
323 class expr_protectedt : public exprt
324 {
325 protected:
326  // constructors
328  : exprt(std::move(_id), std::move(_type))
329  {
330  }
331 
332  expr_protectedt(irep_idt _id, typet _type, operandst _operands)
333  : exprt(std::move(_id), std::move(_type), std::move(_operands))
334  {
335  }
336 
337  // protect these low-level methods
338  using exprt::add;
339  using exprt::op0;
340  using exprt::op1;
341  using exprt::op2;
342  using exprt::op3;
343  using exprt::remove;
344 };
345 
347 {
348 public:
349  virtual ~expr_visitort() { }
350  virtual void operator()(exprt &) { }
351 };
352 
354 {
355 public:
356  virtual ~const_expr_visitort() { }
357  virtual void operator()(const exprt &) { }
358 };
359 
360 #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:55
virtual void operator()(const exprt &)
Definition: expr.h:357
virtual ~const_expr_visitort()
Definition: expr.h:356
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:324
expr_protectedt(irep_idt _id, typet _type)
Definition: expr.h:327
expr_protectedt(irep_idt _id, typet _type, operandst _operands)
Definition: expr.h:332
virtual void operator()(exprt &)
Definition: expr.h:350
virtual ~expr_visitort()
Definition: expr.h:349
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:165
std::vector< exprt > operandst
Definition: expr.h:58
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:114
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:34
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:246
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:282
const typet & type() const
Definition: expr.h:85
depth_iteratort depth_end()
Definition: expr.cpp:267
const_depth_iteratort depth_cend() const
Definition: expr.cpp:275
source_locationt & add_source_location()
Definition: expr.h:216
exprt()
Definition: expr.h:61
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:52
depth_iteratort depth_begin()
Definition: expr.cpp:265
const source_locationt & source_location() const
Definition: expr.h:211
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
exprt & op2()
Definition: expr.h:131
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:43
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:234
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:65
const exprt & op2() const
Definition: expr.h:143
void visit_pre(std::function< void(exprt &)>)
Definition: expr.cpp:245
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:262
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.cpp:27
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:273
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:216
const exprt & find_expr(const irep_idt &name) const
Definition: expr.h:287
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:221
const_unique_depth_iteratort unique_depth_cbegin() const
Definition: expr.cpp:286
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:282
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:105
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:115
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.
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