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 
85 bool exprt::is_constant() const
86 {
87  return id()==ID_constant;
88 }
89 
92 bool exprt::is_true() const
93 {
94  return is_constant() &&
95  type().id()==ID_bool &&
96  get(ID_value)!=ID_false;
97 }
98 
101 bool exprt::is_false() const
102 {
103  return is_constant() &&
104  type().id()==ID_bool &&
105  get(ID_value)==ID_false;
106 }
107 
111 void exprt::make_bool(bool value)
112 {
113  *this=exprt(ID_constant, typet(ID_bool));
114  set(ID_value, value?ID_true:ID_false);
115 }
116 
119 bool exprt::is_boolean() const
120 {
121  return type().id()==ID_bool;
122 }
123 
132 bool exprt::is_zero() const
133 {
134  if(is_constant())
135  {
136  const constant_exprt &constant=to_constant_expr(*this);
137  const irep_idt &type_id=type().id_string();
138 
139  if(type_id==ID_integer || type_id==ID_natural)
140  {
141  return constant.value_is_zero_string();
142  }
143  else if(type_id==ID_rational)
144  {
145  rationalt rat_value;
146  if(to_rational(*this, rat_value))
147  CHECK_RETURN(false);
148  return rat_value.is_zero();
149  }
150  else if(
151  type_id == ID_unsignedbv || type_id == ID_signedbv ||
152  type_id == ID_c_bool || type_id == ID_c_bit_field)
153  {
154  return constant.value_is_zero_string();
155  }
156  else if(type_id==ID_fixedbv)
157  {
158  if(fixedbvt(constant)==0)
159  return true;
160  }
161  else if(type_id==ID_floatbv)
162  {
163  if(ieee_floatt(constant)==0)
164  return true;
165  }
166  else if(type_id==ID_pointer)
167  {
168  return constant.value_is_zero_string() ||
169  constant.get_value()==ID_NULL;
170  }
171  }
172 
173  return false;
174 }
175 
182 bool exprt::is_one() const
183 {
184  if(is_constant())
185  {
186  const auto &constant_expr = to_constant_expr(*this);
187  const irep_idt &type_id = type().id();
188 
189  if(type_id==ID_integer || type_id==ID_natural)
190  {
191  mp_integer int_value =
192  string2integer(id2string(constant_expr.get_value()));
193  if(int_value==1)
194  return true;
195  }
196  else if(type_id==ID_rational)
197  {
198  rationalt rat_value;
199  if(to_rational(*this, rat_value))
200  CHECK_RETURN(false);
201  return rat_value.is_one();
202  }
203  else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
204  {
205  const auto width = to_bitvector_type(type()).get_width();
206  mp_integer int_value =
207  bvrep2integer(id2string(constant_expr.get_value()), width, false);
208  if(int_value==1)
209  return true;
210  }
211  else if(type_id==ID_fixedbv)
212  {
213  if(fixedbvt(constant_expr) == 1)
214  return true;
215  }
216  else if(type_id==ID_floatbv)
217  {
218  if(ieee_floatt(constant_expr) == 1)
219  return true;
220  }
221  }
222 
223  return false;
224 }
225 
232 {
234 
235  if(l.is_not_nil())
236  return l;
237 
238  forall_operands(it, (*this))
239  {
240  const source_locationt &op_l = it->find_source_location();
241  if(op_l.is_not_nil())
242  return op_l;
243  }
244 
245  return static_cast<const source_locationt &>(get_nil_irep());
246 }
247 
248 template <typename T>
249 void visit_post_template(std::function<void(T &)> visitor, T *_expr)
250 {
251  struct stack_entryt
252  {
253  T *e;
254  bool operands_pushed;
255  explicit stack_entryt(T *_e) : e(_e), operands_pushed(false)
256  {
257  }
258  };
259 
260  std::stack<stack_entryt> stack;
261 
262  stack.emplace(_expr);
263 
264  while(!stack.empty())
265  {
266  auto &top = stack.top();
267  if(top.operands_pushed)
268  {
269  visitor(*top.e);
270  stack.pop();
271  }
272  else
273  {
274  // do modification of 'top' before pushing in case 'top' isn't stable
275  top.operands_pushed = true;
276  for(auto &op : top.e->operands())
277  stack.emplace(&op);
278  }
279  }
280 }
281 
282 void exprt::visit_post(std::function<void(exprt &)> visitor)
283 {
284  visit_post_template(visitor, this);
285 }
286 
287 void exprt::visit_post(std::function<void(const exprt &)> visitor) const
288 {
289  visit_post_template(visitor, this);
290 }
291 
292 template <typename T>
293 static void visit_pre_template(std::function<void(T &)> visitor, T *_expr)
294 {
295  std::stack<T *> stack;
296 
297  stack.push(_expr);
298 
299  while(!stack.empty())
300  {
301  T &expr = *stack.top();
302  stack.pop();
303 
304  visitor(expr);
305 
306  for(auto &op : expr.operands())
307  stack.push(&op);
308  }
309 }
310 
311 void exprt::visit_pre(std::function<void(exprt &)> visitor)
312 {
313  visit_pre_template(visitor, this);
314 }
315 
316 void exprt::visit_pre(std::function<void(const exprt &)> visitor) const
317 {
318  visit_pre_template(visitor, this);
319 }
320 
322 {
323  visit_pre([&visitor](exprt &e) { visitor(e); });
324 }
325 
326 void exprt::visit(const_expr_visitort &visitor) const
327 {
328  visit_pre([&visitor](const exprt &e) { visitor(e); });
329 }
330 
332 { return depth_iteratort(*this); }
334 { return depth_iteratort(); }
336 { return const_depth_iteratort(*this); }
338 { return const_depth_iteratort(); }
340 { return const_depth_iteratort(*this); }
342 { return const_depth_iteratort(); }
343 depth_iteratort exprt::depth_begin(std::function<exprt &()> mutate_root) const
344 {
345  return depth_iteratort(*this, std::move(mutate_root));
346 }
347 
349 { return const_unique_depth_iteratort(*this); }
351 { return const_unique_depth_iteratort(); }
353 { return const_unique_depth_iteratort(*this); }
355 { 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:339
rationalt::is_zero
bool is_zero() const
Definition: rational.h:76
const_unique_depth_iteratort
Definition: expr_iterator.h:285
arith_tools.h
rational.h
rational_tools.h
exprt::depth_begin
depth_iteratort depth_begin()
Definition: expr.cpp:331
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:228
fixedbv.h
exprt::make_bool
void make_bool(bool value)
Replace the expression by a Boolean expression representing value.
Definition: expr.cpp:111
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:92
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:321
expr_visitort
Definition: expr.h:390
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:101
expr.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
const_depth_iteratort
Definition: expr_iterator.h:217
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:282
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:231
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:249
const_expr_visitort
Definition: expr.h:397
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:293
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:132
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:341
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:85
exprt::unique_depth_cend
const_unique_depth_iteratort unique_depth_cend() const
Definition: expr.cpp:354
exprt::visit_pre
void visit_pre(std::function< void(exprt &)>)
Definition: expr.cpp:311
fixedbvt
Definition: fixedbv.h:41
exprt::is_one
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:182
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:26
exprt::operands
operandst & operands()
Definition: expr.h:95
exprt::unique_depth_begin
const_unique_depth_iteratort unique_depth_begin() const
Definition: expr.cpp:348
exprt::unique_depth_cbegin
const_unique_depth_iteratort unique_depth_cbegin() const
Definition: expr.cpp:352
constant_exprt
A constant literal expression.
Definition: std_expr.h:3934
exprt::unique_depth_end
const_unique_depth_iteratort unique_depth_end() const
Definition: expr.cpp:350
exprt::depth_end
depth_iteratort depth_end()
Definition: expr.cpp:333
exprt::is_boolean
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.cpp:119
std_expr.h
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:3943
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
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:3968