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 
7 \*******************************************************************/
8 
11 
12 #include "expr.h"
13 
14 #include <cassert>
15 
16 #include <stack>
17 
18 #include "string2int.h"
19 #include "mp_arith.h"
20 #include "fixedbv.h"
21 #include "ieee_float.h"
22 #include "invariant.h"
23 #include "rational.h"
24 #include "rational_tools.h"
25 #include "arith_tools.h"
26 #include "std_expr.h"
27 
29 {
30  operandst &op=operands();
31  op.push_back(static_cast<const exprt &>(get_nil_irep()));
32  op.back().swap(expr);
33 }
34 
36 {
37  operandst &op=operands();
38  #ifndef USE_LIST
39  op.reserve(op.size()+2);
40  #endif
41  op.push_back(static_cast<const exprt &>(get_nil_irep()));
42  op.back().swap(e1);
43  op.push_back(static_cast<const exprt &>(get_nil_irep()));
44  op.back().swap(e2);
45 }
46 
48 {
49  operandst &op=operands();
50  #ifndef USE_LIST
51  op.reserve(op.size()+3);
52  #endif
53  op.push_back(static_cast<const exprt &>(get_nil_irep()));
54  op.back().swap(e1);
55  op.push_back(static_cast<const exprt &>(get_nil_irep()));
56  op.back().swap(e2);
57  op.push_back(static_cast<const exprt &>(get_nil_irep()));
58  op.back().swap(e3);
59 }
60 
61 void exprt::copy_to_operands(const exprt &expr)
62 {
63  operands().push_back(expr);
64 }
65 
66 void exprt::copy_to_operands(const exprt &e1, const exprt &e2)
67 {
68  operandst &op=operands();
69  #ifndef USE_LIST
70  op.reserve(op.size()+2);
71  #endif
72  op.push_back(e1);
73  op.push_back(e2);
74 }
75 
77  const exprt &e1,
78  const exprt &e2,
79  const exprt &e3)
80 {
81  operandst &op=operands();
82  #ifndef USE_LIST
83  op.reserve(op.size()+3);
84  #endif
85  op.push_back(e1);
86  op.push_back(e2);
87  op.push_back(e3);
88 }
89 
90 void exprt::make_typecast(const typet &_type)
91 {
92  exprt new_expr(ID_typecast);
93 
94  new_expr.move_to_operands(*this);
95  new_expr.set(ID_type, _type);
96 
97  swap(new_expr);
98 }
99 
101 {
102  if(is_true())
103  {
104  *this=false_exprt();
105  return;
106  }
107  else if(is_false())
108  {
109  *this=true_exprt();
110  return;
111  }
112 
113  exprt new_expr;
114 
115  if(id()==ID_not && operands().size()==1)
116  {
117  new_expr.swap(operands().front());
118  }
119  else
120  {
121  new_expr=exprt(ID_not, type());
122  new_expr.move_to_operands(*this);
123  }
124 
125  swap(new_expr);
126 }
127 
128 bool exprt::is_constant() const
129 {
130  return id()==ID_constant;
131 }
132 
133 bool exprt::is_true() const
134 {
135  return is_constant() &&
136  type().id()==ID_bool &&
137  get(ID_value)!=ID_false;
138 }
139 
140 bool exprt::is_false() const
141 {
142  return is_constant() &&
143  type().id()==ID_bool &&
144  get(ID_value)==ID_false;
145 }
146 
147 void exprt::make_bool(bool value)
148 {
149  *this=exprt(ID_constant, typet(ID_bool));
150  set(ID_value, value?ID_true:ID_false);
151 }
152 
154 {
155  *this=exprt(ID_constant, typet(ID_bool));
156  set(ID_value, ID_true);
157 }
158 
160 {
161  *this=exprt(ID_constant, typet(ID_bool));
162  set(ID_value, ID_false);
163 }
164 
166 {
167  const irep_idt &type_id=type().id();
168 
169  if(type_id==ID_bool)
170  make_not();
171  else
172  {
173  if(is_constant())
174  {
175  const irep_idt &value=get(ID_value);
176 
177  if(type_id==ID_integer)
178  {
179  set(ID_value, integer2string(-string2integer(id2string(value))));
180  }
181  else if(type_id==ID_unsignedbv)
182  {
183  mp_integer int_value=binary2integer(id2string(value), false);
184  typet _type=type();
185  *this=from_integer(-int_value, _type);
186  }
187  else if(type_id==ID_signedbv)
188  {
189  mp_integer int_value=binary2integer(id2string(value), true);
190  typet _type=type();
191  *this=from_integer(-int_value, _type);
192  }
193  else if(type_id==ID_fixedbv)
194  {
195  fixedbvt fixedbv_value=fixedbvt(to_constant_expr(*this));
196  fixedbv_value.negate();
197  *this=fixedbv_value.to_expr();
198  }
199  else if(type_id==ID_floatbv)
200  {
201  ieee_floatt ieee_float_value=ieee_floatt(to_constant_expr(*this));
202  ieee_float_value.negate();
203  *this=ieee_float_value.to_expr();
204  }
205  else
206  {
207  make_nil();
208  UNREACHABLE;
209  }
210  }
211  else
212  {
213  if(id()==ID_unary_minus)
214  {
215  exprt tmp;
216  DATA_INVARIANT(operands().size()==1,
217  "Unary minus must have one operand");
218  tmp.swap(op0());
219  swap(tmp);
220  }
221  else
222  {
223  exprt tmp(ID_unary_minus, type());
224  tmp.move_to_operands(*this);
225  swap(tmp);
226  }
227  }
228  }
229 }
230 
231 bool exprt::is_boolean() const
232 {
233  return type().id()==ID_bool;
234 }
235 
236 bool exprt::is_zero() const
237 {
238  if(is_constant())
239  {
240  const constant_exprt &constant=to_constant_expr(*this);
241  const irep_idt &type_id=type().id_string();
242 
243  if(type_id==ID_integer || type_id==ID_natural)
244  {
245  return constant.value_is_zero_string();
246  }
247  else if(type_id==ID_rational)
248  {
249  rationalt rat_value;
250  if(to_rational(*this, rat_value))
251  CHECK_RETURN(false);
252  return rat_value.is_zero();
253  }
254  else if(type_id==ID_unsignedbv ||
255  type_id==ID_signedbv ||
256  type_id==ID_c_bool)
257  {
258  return constant.value_is_zero_string();
259  }
260  else if(type_id==ID_fixedbv)
261  {
262  if(fixedbvt(constant)==0)
263  return true;
264  }
265  else if(type_id==ID_floatbv)
266  {
267  if(ieee_floatt(constant)==0)
268  return true;
269  }
270  else if(type_id==ID_pointer)
271  {
272  return constant.value_is_zero_string() ||
273  constant.get_value()==ID_NULL;
274  }
275  }
276 
277  return false;
278 }
279 
280 bool exprt::is_one() const
281 {
282  if(is_constant())
283  {
284  const std::string &value=get_string(ID_value);
285  const irep_idt &type_id=type().id_string();
286 
287  if(type_id==ID_integer || type_id==ID_natural)
288  {
289  mp_integer int_value=string2integer(value);
290  if(int_value==1)
291  return true;
292  }
293  else if(type_id==ID_rational)
294  {
295  rationalt rat_value;
296  if(to_rational(*this, rat_value))
297  CHECK_RETURN(false);
298  return rat_value.is_one();
299  }
300  else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
301  {
302  mp_integer int_value=binary2integer(value, false);
303  if(int_value==1)
304  return true;
305  }
306  else if(type_id==ID_fixedbv)
307  {
308  if(fixedbvt(to_constant_expr(*this))==1)
309  return true;
310  }
311  else if(type_id==ID_floatbv)
312  {
313  if(ieee_floatt(to_constant_expr(*this))==1)
314  return true;
315  }
316  }
317 
318  return false;
319 }
320 
321 bool exprt::sum(const exprt &expr)
322 {
323  if(!is_constant() || !expr.is_constant())
324  return true;
325  if(type()!=expr.type())
326  return true;
327 
328  const irep_idt &type_id=type().id();
329 
330  if(type_id==ID_integer || type_id==ID_natural)
331  {
332  set(ID_value, integer2string(
333  string2integer(get_string(ID_value))+
334  string2integer(expr.get_string(ID_value))));
335  return false;
336  }
337  else if(type_id==ID_rational)
338  {
339  rationalt a, b;
340  if(!to_rational(*this, a) && !to_rational(expr, b))
341  {
342  exprt a_plus_b=from_rational(a+b);
343  set(ID_value, a_plus_b.get_string(ID_value));
344  return false;
345  }
346  }
347  else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
348  {
349  set(ID_value, integer2binary(
350  binary2integer(get_string(ID_value), false)+
351  binary2integer(expr.get_string(ID_value), false),
352  unsafe_string2unsigned(type().get_string(ID_width))));
353  return false;
354  }
355  else if(type_id==ID_fixedbv)
356  {
357  set(ID_value, integer2binary(
358  binary2integer(get_string(ID_value), false)+
359  binary2integer(expr.get_string(ID_value), false),
360  unsafe_string2unsigned(type().get_string(ID_width))));
361  return false;
362  }
363  else if(type_id==ID_floatbv)
364  {
365  ieee_floatt f(to_constant_expr(*this));
366  f+=ieee_floatt(to_constant_expr(expr));
367  *this=f.to_expr();
368  return false;
369  }
370 
371  return true;
372 }
373 
374 bool exprt::mul(const exprt &expr)
375 {
376  if(!is_constant() || !expr.is_constant())
377  return true;
378  if(type()!=expr.type())
379  return true;
380 
381  const irep_idt &type_id=type().id();
382 
383  if(type_id==ID_integer || type_id==ID_natural)
384  {
385  set(ID_value, integer2string(
386  string2integer(get_string(ID_value))*
387  string2integer(expr.get_string(ID_value))));
388  return false;
389  }
390  else if(type_id==ID_rational)
391  {
392  rationalt a, b;
393  if(!to_rational(*this, a) && !to_rational(expr, b))
394  {
395  exprt a_mul_b=from_rational(a*b);
396  set(ID_value, a_mul_b.get_string(ID_value));
397  return false;
398  }
399  }
400  else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
401  {
402  // the following works for signed and unsigned integers
403  set(ID_value, integer2binary(
404  binary2integer(get_string(ID_value), false)*
405  binary2integer(expr.get_string(ID_value), false),
406  unsafe_string2unsigned(type().get_string(ID_width))));
407  return false;
408  }
409  else if(type_id==ID_fixedbv)
410  {
411  fixedbvt f(to_constant_expr(*this));
412  f*=fixedbvt(to_constant_expr(expr));
413  *this=f.to_expr();
414  return false;
415  }
416  else if(type_id==ID_floatbv)
417  {
418  ieee_floatt f(to_constant_expr(*this));
419  f*=ieee_floatt(to_constant_expr(expr));
420  *this=f.to_expr();
421  return false;
422  }
423 
424  return true;
425 }
426 
427 bool exprt::subtract(const exprt &expr)
428 {
429  if(!is_constant() || !expr.is_constant())
430  return true;
431 
432  if(type()!=expr.type())
433  return true;
434 
435  const irep_idt &type_id=type().id();
436 
437  if(type_id==ID_integer || type_id==ID_natural)
438  {
439  set(ID_value, integer2string(
440  string2integer(get_string(ID_value))-
441  string2integer(expr.get_string(ID_value))));
442  return false;
443  }
444  else if(type_id==ID_rational)
445  {
446  rationalt a, b;
447  if(!to_rational(*this, a) && !to_rational(expr, b))
448  {
449  exprt a_minus_b=from_rational(a-b);
450  set(ID_value, a_minus_b.get_string(ID_value));
451  return false;
452  }
453  }
454  else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
455  {
456  set(ID_value, integer2binary(
457  binary2integer(get_string(ID_value), false)-
458  binary2integer(expr.get_string(ID_value), false),
459  unsafe_string2unsigned(type().get_string(ID_width))));
460  return false;
461  }
462 
463  return true;
464 }
465 
467 {
469 
470  if(l.is_not_nil())
471  return l;
472 
473  forall_operands(it, (*this))
474  {
475  const source_locationt &l=it->find_source_location();
476  if(l.is_not_nil())
477  return l;
478  }
479 
480  return static_cast<const source_locationt &>(get_nil_irep());
481 }
482 
484 {
485  std::stack<exprt *> stack;
486 
487  stack.push(this);
488 
489  while(!stack.empty())
490  {
491  exprt &expr=*stack.top();
492  stack.pop();
493 
494  visitor(expr);
495 
496  Forall_operands(it, expr)
497  stack.push(&(*it));
498  }
499 }
500 
501 void exprt::visit(const_expr_visitort &visitor) const
502 {
503  std::stack<const exprt *> stack;
504 
505  stack.push(this);
506 
507  while(!stack.empty())
508  {
509  const exprt &expr=*stack.top();
510  stack.pop();
511 
512  visitor(expr);
513 
514  forall_operands(it, expr)
515  stack.push(&(*it));
516  }
517 }
const irept & get_nil_irep()
Definition: irep.cpp:56
The type of an expression.
Definition: type.h:20
constant_exprt from_rational(const rationalt &a)
BigInt mp_integer
Definition: mp_arith.h:19
bool is_one() const
Definition: rational.h:82
bool is_boolean() const
Definition: expr.cpp:231
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:53
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:104
exprt & op0()
Definition: expr.h:84
constant_exprt to_expr() const
Definition: ieee_float.cpp:686
bool to_rational(const exprt &expr, rationalt &rational_value)
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:66
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
exprt()
Definition: expr.h:52
bool is_false() const
Definition: expr.cpp:140
const irep_idt & get_value() const
Definition: std_expr.h:3702
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
bool is_true() const
Definition: expr.cpp:133
typet & type()
Definition: expr.h:60
A constant literal expression.
Definition: std_expr.h:3685
void make_bool(bool value)
Definition: expr.cpp:147
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:240
bool value_is_zero_string() const
Definition: std_expr.cpp:20
void make_true()
Definition: expr.cpp:153
const irep_idt & id() const
Definition: irep.h:189
void visit(class expr_visitort &visitor)
Definition: expr.cpp:483
The boolean constant true.
Definition: std_expr.h:3742
const source_locationt & find_source_location() const
Definition: expr.cpp:466
API to expression classes.
#define forall_operands(it, expr)
Definition: expr.h:17
bool is_zero() const
Definition: rational.h:79
constant_exprt to_expr() const
Definition: fixedbv.cpp:43
The boolean constant false.
Definition: std_expr.h:3753
bool is_constant() const
Definition: expr.cpp:128
std::vector< exprt > operandst
Definition: expr.h:49
bool mul(const exprt &expr)
Definition: expr.cpp:374
void make_not()
Definition: expr.cpp:100
Base class for all expressions.
Definition: expr.h:46
void make_false()
Definition: expr.cpp:159
void negate()
Definition: ieee_float.h:156
const source_locationt & source_location() const
Definition: expr.h:142
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:63
#define UNREACHABLE
Definition: invariant.h:245
void negate()
Definition: expr.cpp:165
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
bool subtract(const exprt &expr)
Definition: expr.cpp:427
void make_nil()
Definition: irep.h:243
const std::string & id_string() const
Definition: irep.h:192
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
bool is_zero() const
Definition: expr.cpp:236
void negate()
Definition: fixedbv.cpp:87
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:252
bool sum(const exprt &expr)
Definition: expr.cpp:321
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
#define stack(x)
Definition: parser.h:144
void make_typecast(const typet &_type)
Definition: expr.cpp:90
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
bool is_one() const
Definition: expr.cpp:280