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 "type.h"
13 #include "validate_expressions.h"
14 #include "validate_types.h"
15 #include "validation_mode.h"
16 
17 #include <functional>
18 #include <list>
19 
20 #define forall_operands(it, expr) \
21  if((expr).has_operands()) /* NOLINT(readability/braces) */ \
22  for(exprt::operandst::const_iterator it=(expr).operands().begin(), \
23  it##_end=(expr).operands().end(); \
24  it!=it##_end; ++it)
25 
26 #define Forall_operands(it, expr) \
27  if((expr).has_operands()) /* NOLINT(readability/braces) */ \
28  for(exprt::operandst::iterator it=(expr).operands().begin(); \
29  it!=(expr).operands().end(); ++it)
30 
31 #define forall_expr(it, expr) \
32  for(exprt::operandst::const_iterator it=(expr).begin(); \
33  it!=(expr).end(); ++it)
34 
35 #define Forall_expr(it, expr) \
36  for(exprt::operandst::iterator it=(expr).begin(); \
37  it!=(expr).end(); ++it)
38 
39 class depth_iteratort;
42 
54 class exprt:public irept
55 {
56 public:
57  typedef std::vector<exprt> operandst;
58 
59  // constructors
60  exprt() { }
61  explicit exprt(const irep_idt &_id):irept(_id) { }
62  exprt(const irep_idt &_id, const typet &_type):irept(_id)
63  {
64  add(ID_type, _type);
65  }
66 
68  typet &type() { return static_cast<typet &>(add(ID_type)); }
69  const typet &type() const
70  {
71  return static_cast<const typet &>(find(ID_type));
72  }
73 
75  bool has_operands() const
76  { return !operands().empty(); }
77 
79  { return (operandst &)get_sub(); }
80 
81  const operandst &operands() const
82  { return (const operandst &)get_sub(); }
83 
85  { return operands().front(); }
86 
88  { return operands()[1]; }
89 
91  { return operands()[2]; }
92 
94  { return operands()[3]; }
95 
96  const exprt &op0() const
97  { return operands().front(); }
98 
99  const exprt &op1() const
100  { return operands()[1]; }
101 
102  const exprt &op2() const
103  { return operands()[2]; }
104 
105  const exprt &op3() const
106  { return operands()[3]; }
107 
109  { operands().reserve(n) ; }
110 
111  DEPRECATED("use add_to_operands(std::move(expr)) instead")
112  void move_to_operands(exprt &expr);
113 
114  DEPRECATED("use add_to_operands(std::move(e1), std::move(e2)) instead")
115  void move_to_operands(exprt &e1, exprt &e2);
116 
117  DEPRECATED(
118  "use add_to_operands(std::move(e1), std::move(e2), std::move(e3)) instead")
119  void move_to_operands(exprt &e1, exprt &e2, exprt &e3);
120 
123  void copy_to_operands(const exprt &expr)
124  {
125  operands().push_back(expr);
126  }
127 
130  void add_to_operands(const exprt &expr)
131  {
132  copy_to_operands(expr);
133  }
134 
137  void add_to_operands(exprt &&expr)
138  {
139  operands().push_back(std::move(expr));
140  }
141 
145  void copy_to_operands(const exprt &e1, const exprt &e2)
146  {
147  operandst &op = operands();
148  #ifndef USE_LIST
149  op.reserve(op.size() + 2);
150  #endif
151  op.push_back(e1);
152  op.push_back(e2);
153  }
154 
158  void add_to_operands(const exprt &e1, const exprt &e2)
159  {
160  copy_to_operands(e1, e2);
161  }
162 
166  void add_to_operands(exprt &&e1, exprt &&e2)
167  {
168  operandst &op = operands();
169  #ifndef USE_LIST
170  op.reserve(op.size() + 2);
171  #endif
172  op.push_back(std::move(e1));
173  op.push_back(std::move(e2));
174  }
175 
180  void add_to_operands(const exprt &e1, const exprt &e2, const exprt &e3)
181  {
182  copy_to_operands(e1, e2, e3);
183  }
184 
189  void copy_to_operands(const exprt &e1, const exprt &e2, const exprt &e3)
190  {
191  operandst &op = operands();
192  #ifndef USE_LIST
193  op.reserve(op.size() + 3);
194  #endif
195  op.push_back(e1);
196  op.push_back(e2);
197  op.push_back(e3);
198  }
199 
204  void add_to_operands(exprt &&e1, exprt &&e2, exprt &&e3)
205  {
206  operandst &op = operands();
207  #ifndef USE_LIST
208  op.reserve(op.size() + 3);
209  #endif
210  op.push_back(std::move(e1));
211  op.push_back(std::move(e2));
212  op.push_back(std::move(e3));
213  }
214 
215  void make_typecast(const typet &_type);
216 
217  void make_bool(bool value);
218 
219  bool is_constant() const;
220  bool is_true() const;
221  bool is_false() const;
222  bool is_zero() const;
223  bool is_one() const;
224  bool is_boolean() const;
225 
226  const source_locationt &find_source_location() const;
227 
229  {
230  return static_cast<const source_locationt &>(find(ID_C_source_location));
231  }
232 
234  {
235  return static_cast<source_locationt &>(add(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:
305  void visit(class expr_visitort &visitor);
306  void visit(class const_expr_visitort &visitor) const;
307 
314  depth_iteratort depth_begin(std::function<exprt &()> mutate_root) const;
319 };
320 
322 {
323 public:
324  virtual ~expr_visitort() { }
325  virtual void operator()(exprt &) { }
326 };
327 
329 {
330 public:
331  virtual ~const_expr_visitort() { }
332  virtual void operator()(const exprt &) { }
333 };
334 
335 #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:123
exprt::op2
exprt & op2()
Definition: expr.h:90
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
exprt::move_to_operands
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt's operands.
Definition: expr.cpp:29
exprt::depth_cbegin
const_depth_iteratort depth_cbegin() const
Definition: expr.cpp:290
const_unique_depth_iteratort
Definition: expr_iterator.h:292
exprt::op3
exprt & op3()
Definition: expr.h:93
exprt::find_expr
const exprt & find_expr(const irep_idt &name) const
Definition: expr.h:299
exprt::depth_end
depth_iteratort depth_end()
Definition: expr.cpp:284
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:83
expr_visitort::operator()
virtual void operator()(exprt &)
Definition: expr.h:325
const_expr_visitort::~const_expr_visitort
virtual ~const_expr_visitort()
Definition: expr.h:331
typet
The type of an expression, extends irept.
Definition: type.h:27
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:59
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:166
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:305
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
depth_iteratort
Definition: expr_iterator.h:235
exprt::make_bool
void make_bool(bool value)
Replace the expression by a Boolean expression representing value.
Definition: expr.cpp:109
exprt::exprt
exprt()
Definition: expr.h:60
exprt
Base class for all expressions.
Definition: expr.h:54
exprt::exprt
exprt(const irep_idt &_id)
Definition: expr.h:61
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:274
exprt::op0
exprt & op0()
Definition: expr.h:84
const_expr_visitort::operator()
virtual void operator()(const exprt &)
Definition: expr.h:332
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
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:145
exprt::add_to_operands
void add_to_operands(exprt &&expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:137
exprt::visit
void visit(class expr_visitort &visitor)
Definition: expr.cpp:246
expr_visitort
Definition: expr.h:321
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
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:158
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
exprt::operands
const operandst & operands() const
Definition: expr.h:81
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
const_depth_iteratort
Definition: expr_iterator.h:224
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:75
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:229
expr_visitort::~expr_visitort
virtual ~expr_visitort()
Definition: expr.h:324
exprt::op1
exprt & op1()
Definition: expr.h:87
const_expr_visitort
Definition: expr.h:328
validation_modet
validation_modet
Definition: validation_mode.h:12
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
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:189
exprt::type
const typet & type() const
Definition: expr.h:69
source_locationt
Definition: source_location.h:20
exprt::exprt
exprt(const irep_idt &_id, const typet &_type)
Definition: expr.h:62
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:130
exprt::op1
const exprt & op1() const
Definition: expr.h:99
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:180
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:246
exprt::op0
const exprt & op0() const
Definition: expr.h:96
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
exprt::add_expr
exprt & add_expr(const irep_idt &name)
Definition: expr.h:294
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:204
exprt::depth_cend
const_depth_iteratort depth_cend() const
Definition: expr.cpp:292
exprt::depth_begin
depth_iteratort depth_begin()
Definition: expr.cpp:282
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:83
irept::get_sub
subt & get_sub()
Definition: irep.h:317
exprt::unique_depth_cend
const_unique_depth_iteratort unique_depth_cend() const
Definition: expr.cpp:305
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:130
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:88
validate_expressions.h
exprt::is_one
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:180
irept
Base class for tree-like data structures with sharing.
Definition: irep.h:156
exprt::operands
operandst & operands()
Definition: expr.h:78
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:233
validate_expr
void validate_expr(const exprt &)
Called after casting.
Definition: expr_cast.h:49
exprt::make_typecast
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Definition: expr.cpp:74
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:299
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:258
exprt::unique_depth_cbegin
const_unique_depth_iteratort unique_depth_cbegin() const
Definition: expr.cpp:303
exprt::unique_depth_end
const_unique_depth_iteratort unique_depth_end() const
Definition: expr.cpp:301
exprt::is_boolean
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.cpp:117
exprt::reserve_operands
void reserve_operands(operandst::size_type n)
Definition: expr.h:108
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:228
exprt::op3
const exprt & op3() const
Definition: expr.h:105
validation_modet::INVARIANT
@ INVARIANT
exprt::op2
const exprt & op2() const
Definition: expr.h:102