cprover
expr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Expression Representation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6  Joel Allred, joel.allred@diffblue.com
7 
8 \*******************************************************************/
9 
12 
13 // clang-format off
14 #include "arith_tools.h"
15 #include "expr.h"
16 #include "expr_iterator.h"
17 #include "fixedbv.h"
18 #include "ieee_float.h"
19 #include "rational.h"
20 #include "rational_tools.h"
21 #include "std_expr.h"
22 // clang-format on
23 
24 #include <stack>
25 
26 std::size_t exprt::size() const
27 {
28  // Initial size of 1 to count self.
29  std::size_t size = 1;
30  for(const auto &op : operands())
31  {
32  size += op.size();
33  }
34 
35  return size;
36 }
37 
42 {
43  operandst &op=operands();
44  op.push_back(static_cast<const exprt &>(get_nil_irep()));
45  op.back().swap(expr);
46 }
47 
53 {
54  operandst &op=operands();
55  #ifndef USE_LIST
56  op.reserve(op.size()+2);
57  #endif
58  op.push_back(static_cast<const exprt &>(get_nil_irep()));
59  op.back().swap(e1);
60  op.push_back(static_cast<const exprt &>(get_nil_irep()));
61  op.back().swap(e2);
62 }
63 
70 {
71  operandst &op=operands();
72  #ifndef USE_LIST
73  op.reserve(op.size()+3);
74  #endif
75  op.push_back(static_cast<const exprt &>(get_nil_irep()));
76  op.back().swap(e1);
77  op.push_back(static_cast<const exprt &>(get_nil_irep()));
78  op.back().swap(e2);
79  op.push_back(static_cast<const exprt &>(get_nil_irep()));
80  op.back().swap(e3);
81 }
82 
86 void exprt::make_typecast(const typet &_type)
87 {
88  typecast_exprt new_expr(*this, _type);
89 
90  swap(new_expr);
91 }
92 
95 bool exprt::is_constant() const
96 {
97  return id()==ID_constant;
98 }
99 
102 bool exprt::is_true() const
103 {
104  return is_constant() &&
105  type().id()==ID_bool &&
106  get(ID_value)!=ID_false;
107 }
108 
111 bool exprt::is_false() const
112 {
113  return is_constant() &&
114  type().id()==ID_bool &&
115  get(ID_value)==ID_false;
116 }
117 
121 void exprt::make_bool(bool value)
122 {
123  *this=exprt(ID_constant, typet(ID_bool));
124  set(ID_value, value?ID_true:ID_false);
125 }
126 
129 bool exprt::is_boolean() const
130 {
131  return type().id()==ID_bool;
132 }
133 
142 bool exprt::is_zero() const
143 {
144  if(is_constant())
145  {
146  const constant_exprt &constant=to_constant_expr(*this);
147  const irep_idt &type_id=type().id_string();
148 
149  if(type_id==ID_integer || type_id==ID_natural)
150  {
151  return constant.value_is_zero_string();
152  }
153  else if(type_id==ID_rational)
154  {
155  rationalt rat_value;
156  if(to_rational(*this, rat_value))
157  CHECK_RETURN(false);
158  return rat_value.is_zero();
159  }
160  else if(
161  type_id == ID_unsignedbv || type_id == ID_signedbv ||
162  type_id == ID_c_bool || type_id == ID_c_bit_field)
163  {
164  return constant.value_is_zero_string();
165  }
166  else if(type_id==ID_fixedbv)
167  {
168  if(fixedbvt(constant)==0)
169  return true;
170  }
171  else if(type_id==ID_floatbv)
172  {
173  if(ieee_floatt(constant)==0)
174  return true;
175  }
176  else if(type_id==ID_pointer)
177  {
178  return constant.value_is_zero_string() ||
179  constant.get_value()==ID_NULL;
180  }
181  }
182 
183  return false;
184 }
185 
192 bool exprt::is_one() const
193 {
194  if(is_constant())
195  {
196  const auto &constant_expr = to_constant_expr(*this);
197  const irep_idt &type_id = type().id();
198 
199  if(type_id==ID_integer || type_id==ID_natural)
200  {
201  mp_integer int_value =
202  string2integer(id2string(constant_expr.get_value()));
203  if(int_value==1)
204  return true;
205  }
206  else if(type_id==ID_rational)
207  {
208  rationalt rat_value;
209  if(to_rational(*this, rat_value))
210  CHECK_RETURN(false);
211  return rat_value.is_one();
212  }
213  else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
214  {
215  const auto width = to_bitvector_type(type()).get_width();
216  mp_integer int_value =
217  bvrep2integer(id2string(constant_expr.get_value()), width, false);
218  if(int_value==1)
219  return true;
220  }
221  else if(type_id==ID_fixedbv)
222  {
223  if(fixedbvt(constant_expr) == 1)
224  return true;
225  }
226  else if(type_id==ID_floatbv)
227  {
228  if(ieee_floatt(constant_expr) == 1)
229  return true;
230  }
231  }
232 
233  return false;
234 }
235 
242 {
244 
245  if(l.is_not_nil())
246  return l;
247 
248  forall_operands(it, (*this))
249  {
250  const source_locationt &op_l = it->find_source_location();
251  if(op_l.is_not_nil())
252  return op_l;
253  }
254 
255  return static_cast<const source_locationt &>(get_nil_irep());
256 }
257 
258 template <typename T>
259 void visit_post_template(std::function<void(T &)> visitor, T *_expr)
260 {
261  struct stack_entryt
262  {
263  T *e;
264  bool operands_pushed;
265  explicit stack_entryt(T *_e) : e(_e), operands_pushed(false)
266  {
267  }
268  };
269 
270  std::stack<stack_entryt> stack;
271 
272  stack.emplace(_expr);
273 
274  while(!stack.empty())
275  {
276  auto &top = stack.top();
277  if(top.operands_pushed)
278  {
279  visitor(*top.e);
280  stack.pop();
281  }
282  else
283  {
284  // do modification of 'top' before pushing in case 'top' isn't stable
285  top.operands_pushed = true;
286  for(auto &op : top.e->operands())
287  stack.emplace(&op);
288  }
289  }
290 }
291 
292 void exprt::visit_post(std::function<void(exprt &)> visitor)
293 {
294  visit_post_template(visitor, this);
295 }
296 
297 void exprt::visit_post(std::function<void(const exprt &)> visitor) const
298 {
299  visit_post_template(visitor, this);
300 }
301 
302 template <typename T>
303 static void visit_pre_template(std::function<void(T &)> visitor, T *_expr)
304 {
305  std::stack<T *> stack;
306 
307  stack.push(_expr);
308 
309  while(!stack.empty())
310  {
311  T &expr = *stack.top();
312  stack.pop();
313 
314  visitor(expr);
315 
316  for(auto &op : expr.operands())
317  stack.push(&op);
318  }
319 }
320 
321 void exprt::visit_pre(std::function<void(exprt &)> visitor)
322 {
323  visit_pre_template(visitor, this);
324 }
325 
326 void exprt::visit_pre(std::function<void(const exprt &)> visitor) const
327 {
328  visit_pre_template(visitor, this);
329 }
330 
332 {
333  visit_pre([&visitor](exprt &e) { visitor(e); });
334 }
335 
336 void exprt::visit(const_expr_visitort &visitor) const
337 {
338  visit_pre([&visitor](const exprt &e) { visitor(e); });
339 }
340 
342 { return depth_iteratort(*this); }
344 { return depth_iteratort(); }
346 { return const_depth_iteratort(*this); }
348 { return const_depth_iteratort(); }
350 { return const_depth_iteratort(*this); }
352 { return const_depth_iteratort(); }
353 depth_iteratort exprt::depth_begin(std::function<exprt &()> mutate_root) const
354 {
355  return depth_iteratort(*this, std::move(mutate_root));
356 }
357 
359 { return const_unique_depth_iteratort(*this); }
361 { return const_unique_depth_iteratort(); }
363 { return const_unique_depth_iteratort(*this); }
365 { return const_unique_depth_iteratort(); }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
ieee_floatt
Definition: ieee_float.h:119
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
rationalt::is_zero
bool is_zero() const
Definition: rational.h:76
const_unique_depth_iteratort
Definition: expr_iterator.h:282
arith_tools.h
rational.h
rational_tools.h
exprt::depth_begin
depth_iteratort depth_begin()
Definition: expr.cpp:341
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
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
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
string2integer
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
to_rational
bool to_rational(const exprt &expr, rationalt &rational_value)
Definition: rational_tools.cpp:27
depth_iteratort
Definition: expr_iterator.h:225
fixedbv.h
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::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:102
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
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
expr.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
const_depth_iteratort
Definition: expr_iterator.h:214
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
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
irept::id_string
const std::string & id_string() const
Definition: irep.h:421
visit_post_template
void visit_post_template(std::function< void(T &)> visitor, T *_expr)
Definition: expr.cpp:259
const_expr_visitort
Definition: expr.h:399
irept::swap
void swap(irept &irep)
Definition: irep.h:463
irept::id
const irep_idt & id() const
Definition: irep.h:418
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
visit_pre_template
static void visit_pre_template(std::function< void(T &)> visitor, T *_expr)
Definition: expr.cpp:303
source_locationt
Definition: source_location.h:19
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:142
bvrep2integer
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
Definition: arith_tools.cpp:401
expr_iterator.h
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
exprt::depth_cend
const_depth_iteratort depth_cend() const
Definition: expr.cpp:351
constant_exprt::value_is_zero_string
bool value_is_zero_string() const
Definition: std_expr.cpp:23
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
ieee_float.h
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:95
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
fixedbvt
Definition: fixedbv.h:41
exprt::is_one
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:192
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:26
exprt::operands
operandst & operands()
Definition: expr.h:95
exprt::make_typecast
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Definition: expr.cpp:86
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2150
exprt::unique_depth_begin
const_unique_depth_iteratort unique_depth_begin() const
Definition: expr.cpp:358
exprt::unique_depth_cbegin
const_unique_depth_iteratort unique_depth_cbegin() const
Definition: expr.cpp:362
constant_exprt
A constant literal expression.
Definition: std_expr.h:4095
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
std_expr.h
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:4104
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:255
rationalt
Definition: rational.h:17
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1089
rationalt::is_one
bool is_one() const
Definition: rational.h:79
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4129