cprover
simplify_expr_int.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "simplify_expr_class.h"
10 
11 #include <cassert>
12 
13 #include "arith_tools.h"
14 #include "byte_operators.h"
15 #include "config.h"
16 #include "expr_util.h"
17 #include "fixedbv.h"
18 #include "ieee_float.h"
19 #include "invariant.h"
20 #include "mathematical_types.h"
21 #include "namespace.h"
22 #include "pointer_offset_size.h"
23 #include "rational.h"
24 #include "rational_tools.h"
25 #include "std_expr.h"
26 
29 {
30  if(expr.type().id() == ID_unsignedbv && expr.op().is_constant())
31  {
32  auto bits_per_byte = expr.get_bits_per_byte();
33  std::size_t width=to_bitvector_type(expr.type()).get_width();
34  const mp_integer value =
35  numeric_cast_v<mp_integer>(to_constant_expr(expr.op()));
36  std::vector<mp_integer> bytes;
37 
38  // take apart
39  for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
40  bytes.push_back((value >> bit)%power(2, bits_per_byte));
41 
42  // put back together, but backwards
43  mp_integer new_value=0;
44  for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
45  {
46  INVARIANT(
47  !bytes.empty(),
48  "bytes is not empty because we just pushed just as many elements on "
49  "top of it as we are popping now");
50  new_value+=bytes.back()<<bit;
51  bytes.pop_back();
52  }
53 
54  return from_integer(new_value, expr.type());
55  }
56 
57  return unchanged(expr);
58 }
59 
62 static bool sum_expr(
63  constant_exprt &dest,
64  const constant_exprt &expr)
65 {
66  if(dest.type()!=expr.type())
67  return true;
68 
69  const irep_idt &type_id=dest.type().id();
70 
71  if(
72  type_id == ID_integer || type_id == ID_natural ||
73  type_id == ID_unsignedbv || type_id == ID_signedbv)
74  {
75  mp_integer a, b;
76  if(!to_integer(dest, a) && !to_integer(expr, b))
77  {
78  dest = from_integer(a + b, dest.type());
79  return false;
80  }
81  }
82  else if(type_id==ID_rational)
83  {
84  rationalt a, b;
85  if(!to_rational(dest, a) && !to_rational(expr, b))
86  {
87  dest=from_rational(a+b);
88  return false;
89  }
90  }
91  else if(type_id==ID_fixedbv)
92  {
93  fixedbvt f(dest);
94  f += fixedbvt(expr);
95  dest = f.to_expr();
96  return false;
97  }
98  else if(type_id==ID_floatbv)
99  {
100  ieee_floatt f(dest);
101  f += ieee_floatt(expr);
102  dest=f.to_expr();
103  return false;
104  }
105 
106  return true;
107 }
108 
111 static bool mul_expr(
112  constant_exprt &dest,
113  const constant_exprt &expr)
114 {
115  if(dest.type()!=expr.type())
116  return true;
117 
118  const irep_idt &type_id=dest.type().id();
119 
120  if(
121  type_id == ID_integer || type_id == ID_natural ||
122  type_id == ID_unsignedbv || type_id == ID_signedbv)
123  {
124  mp_integer a, b;
125  if(!to_integer(dest, a) && !to_integer(expr, b))
126  {
127  dest = from_integer(a * b, dest.type());
128  return false;
129  }
130  }
131  else if(type_id==ID_rational)
132  {
133  rationalt a, b;
134  if(!to_rational(dest, a) && !to_rational(expr, b))
135  {
136  dest=from_rational(a*b);
137  return false;
138  }
139  }
140  else if(type_id==ID_fixedbv)
141  {
142  fixedbvt f(to_constant_expr(dest));
143  f*=fixedbvt(to_constant_expr(expr));
144  dest=f.to_expr();
145  return false;
146  }
147  else if(type_id==ID_floatbv)
148  {
149  ieee_floatt f(to_constant_expr(dest));
150  f*=ieee_floatt(to_constant_expr(expr));
151  dest=f.to_expr();
152  return false;
153  }
154 
155  return true;
156 }
157 
159 {
160  // check to see if it is a number type
161  if(!is_number(expr.type()))
162  return unchanged(expr);
163 
164  // vector of operands
165  exprt::operandst new_operands = expr.operands();
166 
167  // result of the simplification
168  bool no_change = true;
169 
170  // position of the constant
171  exprt::operandst::iterator constant;
172 
173  // true if we have found a constant
174  bool constant_found = false;
175 
176  optionalt<typet> c_sizeof_type;
177 
178  // scan all the operands
179  for(exprt::operandst::iterator it = new_operands.begin();
180  it != new_operands.end();)
181  {
182  // if one of the operands is not a number return
183  if(!is_number(it->type()))
184  return unchanged(expr);
185 
186  // if one of the operands is zero the result is zero
187  // note: not true on IEEE floating point arithmetic
188  if(it->is_zero() &&
189  it->type().id()!=ID_floatbv)
190  {
191  return from_integer(0, expr.type());
192  }
193 
194  // true if the given operand has to be erased
195  bool do_erase = false;
196 
197  // if this is a constant of the same time as the result
198  if(it->is_constant() && it->type()==expr.type())
199  {
200  // preserve the sizeof type annotation
201  if(!c_sizeof_type.has_value())
202  {
203  const typet &sizeof_type =
204  static_cast<const typet &>(it->find(ID_C_c_sizeof_type));
205  if(sizeof_type.is_not_nil())
206  c_sizeof_type = sizeof_type;
207  }
208 
209  if(constant_found)
210  {
211  // update the constant factor
212  if(!mul_expr(to_constant_expr(*constant), to_constant_expr(*it)))
213  do_erase=true;
214  }
215  else
216  {
217  // set it as the constant factor if this is the first
218  constant=it;
219  constant_found = true;
220  }
221  }
222 
223  // erase the factor if necessary
224  if(do_erase)
225  {
226  it = new_operands.erase(it);
227  no_change = false;
228  }
229  else
230  it++; // move to the next operand
231  }
232 
233  if(c_sizeof_type.has_value())
234  {
235  INVARIANT(
236  constant_found,
237  "c_sizeof_type is only set to a non-nil value "
238  "if a constant has been found");
239  constant->set(ID_C_c_sizeof_type, *c_sizeof_type);
240  }
241 
242  if(new_operands.size() == 1)
243  {
244  return new_operands.front();
245  }
246  else
247  {
248  // if the constant is a one and there are other factors
249  if(constant_found && constant->is_one())
250  {
251  // just delete it
252  new_operands.erase(constant);
253  no_change = false;
254 
255  if(new_operands.size() == 1)
256  return new_operands.front();
257  }
258  }
259 
260  if(no_change)
261  return unchanged(expr);
262  else
263  {
264  exprt tmp = expr;
265  tmp.operands() = std::move(new_operands);
266  return std::move(tmp);
267  }
268 }
269 
271 {
272  if(!is_number(expr.type()))
273  return unchanged(expr);
274 
275  const typet &expr_type=expr.type();
276 
277  if(expr_type!=expr.op0().type() ||
278  expr_type!=expr.op1().type())
279  {
280  return unchanged(expr);
281  }
282 
283  if(expr_type.id()==ID_signedbv ||
284  expr_type.id()==ID_unsignedbv ||
285  expr_type.id()==ID_natural ||
286  expr_type.id()==ID_integer)
287  {
288  const auto int_value0 = numeric_cast<mp_integer>(expr.op0());
289  const auto int_value1 = numeric_cast<mp_integer>(expr.op1());
290 
291  // division by zero?
292  if(int_value1.has_value() && *int_value1 == 0)
293  return unchanged(expr);
294 
295  // x/1?
296  if(int_value1.has_value() && *int_value1 == 1)
297  {
298  return expr.op0();
299  }
300 
301  // 0/x?
302  if(int_value0.has_value() && *int_value0 == 0)
303  {
304  return expr.op0();
305  }
306 
307  if(int_value0.has_value() && int_value1.has_value())
308  {
309  mp_integer result = *int_value0 / *int_value1;
310  return from_integer(result, expr_type);
311  }
312  }
313  else if(expr_type.id()==ID_rational)
314  {
315  rationalt rat_value0, rat_value1;
316  bool ok0, ok1;
317 
318  ok0=!to_rational(expr.op0(), rat_value0);
319  ok1=!to_rational(expr.op1(), rat_value1);
320 
321  if(ok1 && rat_value1.is_zero())
322  return unchanged(expr);
323 
324  if((ok1 && rat_value1.is_one()) ||
325  (ok0 && rat_value0.is_zero()))
326  {
327  return expr.op0();
328  }
329 
330  if(ok0 && ok1)
331  {
332  rationalt result=rat_value0/rat_value1;
333  exprt tmp=from_rational(result);
334 
335  if(tmp.is_not_nil())
336  return std::move(tmp);
337  }
338  }
339  else if(expr_type.id()==ID_fixedbv)
340  {
341  // division by one?
342  if(expr.op1().is_constant() &&
343  expr.op1().is_one())
344  {
345  return expr.op0();
346  }
347 
348  if(expr.op0().is_constant() &&
349  expr.op1().is_constant())
350  {
351  fixedbvt f0(to_constant_expr(expr.op0()));
352  fixedbvt f1(to_constant_expr(expr.op1()));
353  if(!f1.is_zero())
354  {
355  f0/=f1;
356  return f0.to_expr();
357  }
358  }
359  }
360 
361  return unchanged(expr);
362 }
363 
365 {
366  if(!is_number(expr.type()))
367  return unchanged(expr);
368 
369  if(expr.type().id()==ID_signedbv ||
370  expr.type().id()==ID_unsignedbv ||
371  expr.type().id()==ID_natural ||
372  expr.type().id()==ID_integer)
373  {
374  if(expr.type()==expr.op0().type() &&
375  expr.type()==expr.op1().type())
376  {
377  const auto int_value0 = numeric_cast<mp_integer>(expr.op0());
378  const auto int_value1 = numeric_cast<mp_integer>(expr.op1());
379 
380  if(int_value1.has_value() && *int_value1 == 0)
381  return unchanged(expr); // division by zero
382 
383  if(
384  (int_value1.has_value() && *int_value1 == 1) ||
385  (int_value0.has_value() && *int_value0 == 0))
386  {
387  return from_integer(0, expr.type());
388  }
389 
390  if(int_value0.has_value() && int_value1.has_value())
391  {
392  mp_integer result = *int_value0 % *int_value1;
393  return from_integer(result, expr.type());
394  }
395  }
396  }
397 
398  return unchanged(expr);
399 }
400 
402 {
403  if(!is_number(expr.type()) && expr.type().id() != ID_pointer)
404  return unchanged(expr);
405 
406  bool no_change = true;
407 
408  exprt::operandst new_operands = expr.operands();
409 
410  // floating-point addition is _NOT_ associative; thus,
411  // there is special case for float
412 
413  if(expr.type().id() == ID_floatbv)
414  {
415  // we only merge neighboring constants!
416  Forall_expr(it, new_operands)
417  {
418  const exprt::operandst::iterator next = std::next(it);
419 
420  if(next != new_operands.end())
421  {
422  if(it->type()==next->type() &&
423  it->is_constant() &&
424  next->is_constant())
425  {
427  new_operands.erase(next);
428  no_change = false;
429  }
430  }
431  }
432  }
433  else
434  {
435  // ((T*)p+a)+b -> (T*)p+(a+b)
436  if(
437  expr.type().id() == ID_pointer && expr.operands().size() == 2 &&
438  expr.op0().id() == ID_plus && expr.op0().type().id() == ID_pointer &&
439  expr.op0().operands().size() == 2)
440  {
441  plus_exprt op0 = to_plus_expr(expr.op0());
442 
443  if(op0.op1().id() == ID_plus)
444  to_plus_expr(op0.op1()).add_to_operands(expr.op1());
445  else
446  op0.op1()=plus_exprt(op0.op1(), expr.op1());
447 
448  auto result = op0;
449 
450  result.op1() = simplify_plus(to_plus_expr(result.op1()));
451 
452  return changed(simplify_plus(result));
453  }
454 
455  // count the constants
456  size_t count=0;
457  forall_operands(it, expr)
458  if(is_number(it->type()) && it->is_constant())
459  count++;
460 
461  // merge constants?
462  if(count>=2)
463  {
464  exprt::operandst::iterator const_sum;
465  bool const_sum_set=false;
466 
467  for(auto it = new_operands.begin(); it != new_operands.end(); it++)
468  {
469  if(is_number(it->type()) && it->is_constant())
470  {
471  if(!const_sum_set)
472  {
473  const_sum=it;
474  const_sum_set=true;
475  }
476  else
477  {
478  if(!sum_expr(to_constant_expr(*const_sum),
479  to_constant_expr(*it)))
480  {
481  *it=from_integer(0, it->type());
482  no_change = false;
483  }
484  }
485  }
486  }
487  }
488 
489  // search for a and -a
490  // first gather all the a's with -a
491  typedef std::unordered_map<exprt, exprt::operandst::iterator, irep_hash>
492  expr_mapt;
493  expr_mapt expr_map;
494 
495  for(auto it = new_operands.begin(); it != new_operands.end(); it++)
496  if(it->id() == ID_unary_minus)
497  {
498  expr_map.insert(std::make_pair(to_unary_minus_expr(*it).op(), it));
499  }
500 
501  // now search for a
502  for(auto it = new_operands.begin(); it != new_operands.end(); it++)
503  {
504  if(expr_map.empty())
505  break;
506  else if(it->id()==ID_unary_minus)
507  continue;
508 
509  expr_mapt::iterator itm=expr_map.find(*it);
510 
511  if(itm!=expr_map.end())
512  {
513  *(itm->second)=from_integer(0, expr.type());
514  *it=from_integer(0, expr.type());
515  expr_map.erase(itm);
516  no_change = false;
517  }
518  }
519 
520  // delete zeros
521  // (can't do for floats, as the result of 0.0 + (-0.0)
522  // need not be -0.0 in std rounding)
523  for(exprt::operandst::iterator it = new_operands.begin();
524  it != new_operands.end();
525  /* no it++ */)
526  {
527  if(is_number(it->type()) && it->is_zero())
528  {
529  it = new_operands.erase(it);
530  no_change = false;
531  }
532  else
533  it++;
534  }
535  }
536 
537  if(new_operands.empty())
538  {
539  return from_integer(0, expr.type());
540  }
541  else if(new_operands.size() == 1)
542  {
543  return new_operands.front();
544  }
545 
546  if(no_change)
547  return unchanged(expr);
548  else
549  {
550  auto tmp = expr;
551  tmp.operands() = std::move(new_operands);
552  return std::move(tmp);
553  }
554 }
555 
558 {
559  auto const &minus_expr = to_minus_expr(expr);
560  if(!is_number(minus_expr.type()) && minus_expr.type().id() != ID_pointer)
561  return unchanged(expr);
562 
563  const exprt::operandst &operands = minus_expr.operands();
564 
565  if(
566  is_number(minus_expr.type()) && is_number(operands[0].type()) &&
567  is_number(operands[1].type()))
568  {
569  // rewrite "a-b" to "a+(-b)"
570  unary_minus_exprt rhs_negated(operands[1]);
571  plus_exprt plus_expr(operands[0], simplify_unary_minus(rhs_negated));
572  return changed(simplify_node(plus_expr));
573  }
574  else if(
575  minus_expr.type().id() == ID_pointer &&
576  operands[0].type().id() == ID_pointer && is_number(operands[1].type()))
577  {
578  // pointer arithmetic: rewrite "p-i" to "p+(-i)"
579  unary_minus_exprt negated_pointer_offset(operands[1]);
580 
581  plus_exprt pointer_offset_expr(
582  operands[0], simplify_unary_minus(negated_pointer_offset));
583  return changed(simplify_plus(pointer_offset_expr));
584  }
585  else if(
586  is_number(minus_expr.type()) && operands[0].type().id() == ID_pointer &&
587  operands[1].type().id() == ID_pointer)
588  {
589  // pointer arithmetic: rewrite "p-p" to "0"
590 
591  if(operands[0]==operands[1])
592  return from_integer(0, minus_expr.type());
593  }
594 
595  return unchanged(expr);
596 }
597 
600 {
601  if(!is_bitvector_type(expr.type()))
602  return unchanged(expr);
603 
604  // check if these are really boolean
605  if(expr.type().id()!=ID_bool)
606  {
607  bool all_bool=true;
608 
609  forall_operands(it, expr)
610  {
611  if(
612  it->id() == ID_typecast &&
613  to_typecast_expr(*it).op().type().id() == ID_bool)
614  {
615  }
616  else if(it->is_zero() || it->is_one())
617  {
618  }
619  else
620  all_bool=false;
621  }
622 
623  if(all_bool)
624  {
625  // re-write to boolean+typecast
626  exprt new_expr=expr;
627 
628  if(expr.id()==ID_bitand)
629  new_expr.id(ID_and);
630  else if(expr.id()==ID_bitor)
631  new_expr.id(ID_or);
632  else if(expr.id()==ID_bitxor)
633  new_expr.id(ID_xor);
634  else
635  UNREACHABLE;
636 
637  Forall_operands(it, new_expr)
638  {
639  if(it->id()==ID_typecast)
640  *it = to_typecast_expr(*it).op();
641  else if(it->is_zero())
642  *it=false_exprt();
643  else if(it->is_one())
644  *it=true_exprt();
645  }
646 
647  new_expr.type()=bool_typet();
648  new_expr = simplify_node(new_expr);
649 
650  new_expr = typecast_exprt(new_expr, expr.type());
651  return changed(simplify_node(new_expr));
652  }
653  }
654 
655  bool no_change = true;
656  auto new_expr = expr;
657 
658  // try to merge constants
659 
660  const std::size_t width = to_bitvector_type(expr.type()).get_width();
661 
662  while(new_expr.operands().size() >= 2)
663  {
664  if(!new_expr.op0().is_constant())
665  break;
666 
667  if(!new_expr.op1().is_constant())
668  break;
669 
670  if(new_expr.op0().type() != new_expr.type())
671  break;
672 
673  if(new_expr.op1().type() != new_expr.type())
674  break;
675 
676  const auto &a_val = to_constant_expr(new_expr.op0()).get_value();
677  const auto &b_val = to_constant_expr(new_expr.op1()).get_value();
678 
679  std::function<bool(bool, bool)> f;
680 
681  if(new_expr.id() == ID_bitand)
682  f = [](bool a, bool b) { return a && b; };
683  else if(new_expr.id() == ID_bitor)
684  f = [](bool a, bool b) { return a || b; };
685  else if(new_expr.id() == ID_bitxor)
686  f = [](bool a, bool b) { return a != b; };
687  else
688  UNREACHABLE;
689 
690  const irep_idt new_value =
691  make_bvrep(width, [&a_val, &b_val, &width, &f](std::size_t i) {
692  return f(
693  get_bvrep_bit(a_val, width, i), get_bvrep_bit(b_val, width, i));
694  });
695 
696  constant_exprt new_op(new_value, expr.type());
697 
698  // erase first operand
699  new_expr.operands().erase(new_expr.operands().begin());
700  new_expr.op0().swap(new_op);
701 
702  no_change = false;
703  }
704 
705  // now erase 'all zeros' out of bitor, bitxor
706 
707  if(new_expr.id() == ID_bitor || new_expr.id() == ID_bitxor)
708  {
709  for(exprt::operandst::iterator it = new_expr.operands().begin();
710  it != new_expr.operands().end();) // no it++
711  {
712  if(it->is_zero() && new_expr.operands().size() > 1)
713  {
714  it = new_expr.operands().erase(it);
715  no_change = false;
716  }
717  else
718  it++;
719  }
720  }
721 
722  // now erase 'all ones' out of bitand
723 
724  if(new_expr.id() == ID_bitand)
725  {
726  const auto all_ones = power(2, width) - 1;
727  for(exprt::operandst::iterator it = new_expr.operands().begin();
728  it != new_expr.operands().end();) // no it++
729  {
730  if(
731  it->is_constant() &&
732  bvrep2integer(to_constant_expr(*it).get_value(), width, false) ==
733  all_ones &&
734  new_expr.operands().size() > 1)
735  {
736  it = new_expr.operands().erase(it);
737  no_change = false;
738  }
739  else
740  it++;
741  }
742  }
743 
744  // two operands that are syntactically the same
745 
746  if(new_expr.operands().size() == 2 && new_expr.op0() == new_expr.op1())
747  {
748  if(new_expr.id() == ID_bitand || new_expr.id() == ID_bitor)
749  {
750  return new_expr.op0();
751  }
752  else if(new_expr.id() == ID_bitxor)
753  {
754  return constant_exprt(integer2bvrep(0, width), new_expr.type());
755  }
756  }
757 
758  if(new_expr.operands().size() == 1)
759  return new_expr.op0();
760 
761  if(no_change)
762  return unchanged(expr);
763  else
764  return std::move(new_expr);
765 }
766 
769 {
770  const typet &src_type = expr.src().type();
771 
772  if(!is_bitvector_type(src_type))
773  return unchanged(expr);
774 
775  const std::size_t src_bit_width = to_bitvector_type(src_type).get_width();
776 
777  const auto index_converted_to_int = numeric_cast<mp_integer>(expr.index());
778  if(
779  !index_converted_to_int.has_value() || *index_converted_to_int < 0 ||
780  *index_converted_to_int >= src_bit_width)
781  {
782  return unchanged(expr);
783  }
784 
785  if(!expr.src().is_constant())
786  return unchanged(expr);
787 
788  const bool bit = get_bvrep_bit(
789  to_constant_expr(expr.src()).get_value(),
790  src_bit_width,
791  numeric_cast_v<std::size_t>(*index_converted_to_int));
792 
793  return make_boolean_expr(bit);
794 }
795 
798 {
799  bool no_change = true;
800 
801  concatenation_exprt new_expr = expr;
802 
803  if(is_bitvector_type(new_expr.type()))
804  {
805  // first, turn bool into bvec[1]
806  Forall_operands(it, new_expr)
807  {
808  exprt &op=*it;
809  if(op.is_true() || op.is_false())
810  {
811  const bool value = op.is_true();
812  op = from_integer(value, unsignedbv_typet(1));
813  no_change = false;
814  }
815  }
816 
817  // search for neighboring constants to merge
818  size_t i=0;
819 
820  while(i < new_expr.operands().size() - 1)
821  {
822  exprt &opi = new_expr.operands()[i];
823  exprt &opn = new_expr.operands()[i + 1];
824 
825  if(opi.is_constant() &&
826  opn.is_constant() &&
827  is_bitvector_type(opi.type()) &&
828  is_bitvector_type(opn.type()))
829  {
830  // merge!
831  const auto &value_i = to_constant_expr(opi).get_value();
832  const auto &value_n = to_constant_expr(opn).get_value();
833  const auto width_i = to_bitvector_type(opi.type()).get_width();
834  const auto width_n = to_bitvector_type(opn.type()).get_width();
835  const auto new_width = width_i + width_n;
836 
837  const auto new_value = make_bvrep(
838  new_width, [&value_i, &value_n, width_i, width_n](std::size_t x) {
839  return x < width_n ? get_bvrep_bit(value_n, width_n, x)
840  : get_bvrep_bit(value_i, width_i, x - width_n);
841  });
842 
843  to_constant_expr(opi).set_value(new_value);
844  to_bitvector_type(opi.type()).set_width(new_width);
845  // erase opn
846  new_expr.operands().erase(new_expr.operands().begin() + i + 1);
847  no_change = false;
848  }
849  else
850  i++;
851  }
852  }
853  else if(new_expr.type().id() == ID_verilog_unsignedbv)
854  {
855  // search for neighboring constants to merge
856  size_t i=0;
857 
858  while(i < new_expr.operands().size() - 1)
859  {
860  exprt &opi = new_expr.operands()[i];
861  exprt &opn = new_expr.operands()[i + 1];
862 
863  if(opi.is_constant() &&
864  opn.is_constant() &&
865  (opi.type().id()==ID_verilog_unsignedbv ||
866  is_bitvector_type(opi.type())) &&
867  (opn.type().id()==ID_verilog_unsignedbv ||
868  is_bitvector_type(opn.type())))
869  {
870  // merge!
871  const std::string new_value=
872  opi.get_string(ID_value)+opn.get_string(ID_value);
873  opi.set(ID_value, new_value);
874  to_bitvector_type(opi.type()).set_width(new_value.size());
875  opi.type().id(ID_verilog_unsignedbv);
876  // erase opn
877  new_expr.operands().erase(new_expr.operands().begin() + i + 1);
878  no_change = false;
879  }
880  else
881  i++;
882  }
883  }
884 
885  // { x } = x
886  if(
887  new_expr.operands().size() == 1 && new_expr.op0().type() == new_expr.type())
888  {
889  return new_expr.op0();
890  }
891 
892  if(no_change)
893  return unchanged(expr);
894  else
895  return std::move(new_expr);
896 }
897 
900 {
901  if(!is_bitvector_type(expr.type()))
902  return unchanged(expr);
903 
904  const auto distance = numeric_cast<mp_integer>(expr.distance());
905 
906  if(!distance.has_value())
907  return unchanged(expr);
908 
909  if(*distance == 0)
910  return expr.op();
911 
912  auto value = numeric_cast<mp_integer>(expr.op());
913 
914  if(
915  !value.has_value() && expr.op().type().id() == ID_bv &&
916  expr.op().id() == ID_constant)
917  {
918  const std::size_t width = to_bitvector_type(expr.op().type()).get_width();
919  value =
920  bvrep2integer(to_constant_expr(expr.op()).get_value(), width, false);
921  }
922 
923  if(!value.has_value())
924  return unchanged(expr);
925 
926  if(
927  expr.op().type().id() == ID_unsignedbv ||
928  expr.op().type().id() == ID_signedbv || expr.op().type().id() == ID_bv)
929  {
930  const std::size_t width = to_bitvector_type(expr.op().type()).get_width();
931 
932  if(expr.id()==ID_lshr)
933  {
934  // this is to guard against large values of distance
935  if(*distance >= width)
936  {
937  return from_integer(0, expr.type());
938  }
939  else if(*distance >= 0)
940  {
941  if(*value < 0)
942  *value += power(2, width);
943  *value /= power(2, *distance);
944  return from_integer(*value, expr.type());
945  }
946  }
947  else if(expr.id()==ID_ashr)
948  {
949  if(*distance >= 0)
950  {
951  // this is to simulate an arithmetic right shift
952  mp_integer new_value = *value >> *distance;
953  return from_integer(new_value, expr.type());
954  }
955  }
956  else if(expr.id()==ID_shl)
957  {
958  // this is to guard against large values of distance
959  if(*distance >= width)
960  {
961  return from_integer(0, expr.type());
962  }
963  else if(*distance >= 0)
964  {
965  *value *= power(2, *distance);
966  return from_integer(*value, expr.type());
967  }
968  }
969  }
970  else if(
971  expr.op().type().id() == ID_integer || expr.op().type().id() == ID_natural)
972  {
973  if(expr.id()==ID_lshr)
974  {
975  if(*distance >= 0)
976  {
977  *value /= power(2, *distance);
978  return from_integer(*value, expr.type());
979  }
980  }
981  else if(expr.id()==ID_ashr)
982  {
983  // this is to simulate an arithmetic right shift
984  if(*distance >= 0)
985  {
986  mp_integer new_value = *value / power(2, *distance);
987  if(*value < 0 && new_value == 0)
988  new_value=-1;
989 
990  return from_integer(new_value, expr.type());
991  }
992  }
993  else if(expr.id()==ID_shl)
994  {
995  if(*distance >= 0)
996  {
997  *value *= power(2, *distance);
998  return from_integer(*value, expr.type());
999  }
1000  }
1001  }
1002 
1003  return unchanged(expr);
1004 }
1005 
1008 {
1009  if(!is_number(expr.type()))
1010  return unchanged(expr);
1011 
1012  const auto base = numeric_cast<mp_integer>(expr.op0());
1013  const auto exponent = numeric_cast<mp_integer>(expr.op1());
1014 
1015  if(!base.has_value())
1016  return unchanged(expr);
1017 
1018  if(!exponent.has_value())
1019  return unchanged(expr);
1020 
1021  mp_integer result = power(*base, *exponent);
1022 
1023  return from_integer(result, expr.type());
1024 }
1025 
1029 {
1030  const typet &op0_type = expr.src().type();
1031 
1032  if(!is_bitvector_type(op0_type) &&
1033  !is_bitvector_type(expr.type()))
1034  {
1035  return unchanged(expr);
1036  }
1037 
1038  const auto start = numeric_cast<mp_integer>(expr.upper());
1039  const auto end = numeric_cast<mp_integer>(expr.lower());
1040 
1041  if(!start.has_value())
1042  return unchanged(expr);
1043 
1044  if(!end.has_value())
1045  return unchanged(expr);
1046 
1047  const auto width = pointer_offset_bits(op0_type, ns);
1048 
1049  if(!width.has_value())
1050  return unchanged(expr);
1051 
1052  if(*start < 0 || *start >= (*width) || *end < 0 || *end >= (*width))
1053  return unchanged(expr);
1054 
1055  DATA_INVARIANT(*start >= *end, "extractbits must have upper() >= lower()");
1056 
1057  if(expr.src().is_constant())
1058  {
1059  const auto svalue = expr2bits(expr.src(), true);
1060 
1061  if(!svalue.has_value() || svalue->size() != *width)
1062  return unchanged(expr);
1063 
1064  std::string extracted_value = svalue->substr(
1065  numeric_cast_v<std::size_t>(*end),
1066  numeric_cast_v<std::size_t>(*start - *end + 1));
1067 
1068  auto result = bits2expr(extracted_value, expr.type(), true);
1069  if(!result.has_value())
1070  return unchanged(expr);
1071 
1072  return std::move(*result);
1073  }
1074  else if(expr.src().id() == ID_concatenation)
1075  {
1076  // the most-significant bit comes first in an concatenation_exprt, hence we
1077  // count down
1078  mp_integer offset = *width;
1079 
1080  forall_operands(it, expr.src())
1081  {
1082  auto op_width = pointer_offset_bits(it->type(), ns);
1083 
1084  if(!op_width.has_value() || *op_width <= 0)
1085  return unchanged(expr);
1086 
1087  if(*start + 1 == offset && *end + *op_width == offset)
1088  {
1089  exprt tmp = *it;
1090  if(tmp.type() != expr.type())
1091  return unchanged(expr);
1092 
1093  return std::move(tmp);
1094  }
1095 
1096  offset -= *op_width;
1097  }
1098  }
1099 
1100  return unchanged(expr);
1101 }
1102 
1105 {
1106  // simply remove, this is always 'nop'
1107  return expr.op();
1108 }
1109 
1112 {
1113  if(!is_number(expr.type()))
1114  return unchanged(expr);
1115 
1116  const exprt &operand = expr.op();
1117 
1118  if(expr.type()!=operand.type())
1119  return unchanged(expr);
1120 
1121  if(operand.id()==ID_unary_minus)
1122  {
1123  // cancel out "-(-x)" to "x"
1124  if(!is_number(to_unary_minus_expr(operand).op().type()))
1125  return unchanged(expr);
1126 
1127  return to_unary_minus_expr(operand).op();
1128  }
1129  else if(operand.id()==ID_constant)
1130  {
1131  const irep_idt &type_id=expr.type().id();
1132  const auto &constant_expr = to_constant_expr(operand);
1133 
1134  if(type_id==ID_integer ||
1135  type_id==ID_signedbv ||
1136  type_id==ID_unsignedbv)
1137  {
1138  const auto int_value = numeric_cast<mp_integer>(constant_expr);
1139 
1140  if(!int_value.has_value())
1141  return unchanged(expr);
1142 
1143  return from_integer(-*int_value, expr.type());
1144  }
1145  else if(type_id==ID_rational)
1146  {
1147  rationalt r;
1148  if(to_rational(constant_expr, r))
1149  return unchanged(expr);
1150 
1151  return from_rational(-r);
1152  }
1153  else if(type_id==ID_fixedbv)
1154  {
1155  fixedbvt f(constant_expr);
1156  f.negate();
1157  return f.to_expr();
1158  }
1159  else if(type_id==ID_floatbv)
1160  {
1161  ieee_floatt f(constant_expr);
1162  f.negate();
1163  return f.to_expr();
1164  }
1165  }
1166 
1167  return unchanged(expr);
1168 }
1169 
1172 {
1173  const exprt &op = expr.op();
1174 
1175  const auto &type = expr.type();
1176 
1177  if(
1178  type.id() == ID_bv || type.id() == ID_unsignedbv ||
1179  type.id() == ID_signedbv)
1180  {
1181  const auto width = to_bitvector_type(type).get_width();
1182 
1183  if(op.type() == type)
1184  {
1185  if(op.id()==ID_constant)
1186  {
1187  const auto &value = to_constant_expr(op).get_value();
1188  const auto new_value =
1189  make_bvrep(width, [&value, &width](std::size_t i) {
1190  return !get_bvrep_bit(value, width, i);
1191  });
1192  return constant_exprt(new_value, op.type());
1193  }
1194  }
1195  }
1196 
1197  return unchanged(expr);
1198 }
1199 
1203 {
1204  if(expr.type().id()!=ID_bool)
1205  return unchanged(expr);
1206 
1207  exprt tmp0=expr.op0();
1208  exprt tmp1=expr.op1();
1209 
1210  // types must match
1211  if(tmp0.type() != tmp1.type())
1212  return unchanged(expr);
1213 
1214  // if rhs is ID_if (and lhs is not), swap operands for == and !=
1215  if((expr.id()==ID_equal || expr.id()==ID_notequal) &&
1216  tmp0.id()!=ID_if &&
1217  tmp1.id()==ID_if)
1218  {
1219  auto new_expr = expr;
1220  new_expr.op0().swap(new_expr.op1());
1221  return changed(simplify_inequality(new_expr)); // recursive call
1222  }
1223 
1224  if(tmp0.id()==ID_if && tmp0.operands().size()==3)
1225  {
1226  if_exprt if_expr=lift_if(expr, 0);
1227  if_expr.true_case() =
1229  if_expr.false_case() =
1231  return changed(simplify_if(if_expr));
1232  }
1233 
1234  // see if we are comparing pointers that are address_of
1235  if(
1236  (tmp0.id() == ID_address_of ||
1237  (tmp0.id() == ID_typecast &&
1238  to_typecast_expr(tmp0).op().id() == ID_address_of)) &&
1239  (tmp1.id() == ID_address_of ||
1240  (tmp1.id() == ID_typecast &&
1241  to_typecast_expr(tmp1).op().id() == ID_address_of)) &&
1242  (expr.id() == ID_equal || expr.id() == ID_notequal))
1243  {
1244  return simplify_inequality_address_of(expr);
1245  }
1246 
1247  if(tmp0.id()==ID_pointer_object &&
1248  tmp1.id()==ID_pointer_object &&
1249  (expr.id()==ID_equal || expr.id()==ID_notequal))
1250  {
1252  }
1253 
1254  if(tmp0.type().id()==ID_c_enum_tag)
1255  tmp0.type()=ns.follow_tag(to_c_enum_tag_type(tmp0.type()));
1256 
1257  if(tmp1.type().id()==ID_c_enum_tag)
1258  tmp1.type()=ns.follow_tag(to_c_enum_tag_type(tmp1.type()));
1259 
1260  const bool tmp0_const = tmp0.is_constant();
1261  const bool tmp1_const = tmp1.is_constant();
1262 
1263  // are _both_ constant?
1264  if(tmp0_const && tmp1_const)
1265  {
1266  return simplify_inequality_both_constant(expr);
1267  }
1268  else if(tmp0_const)
1269  {
1270  // we want the constant on the RHS
1271 
1272  binary_relation_exprt new_expr = expr;
1273 
1274  if(expr.id()==ID_ge)
1275  new_expr.id(ID_le);
1276  else if(expr.id()==ID_le)
1277  new_expr.id(ID_ge);
1278  else if(expr.id()==ID_gt)
1279  new_expr.id(ID_lt);
1280  else if(expr.id()==ID_lt)
1281  new_expr.id(ID_gt);
1282 
1283  new_expr.op0().swap(new_expr.op1());
1284 
1285  // RHS is constant, LHS is not
1286  return changed(simplify_inequality_rhs_is_constant(new_expr));
1287  }
1288  else if(tmp1_const)
1289  {
1290  // RHS is constant, LHS is not
1292  }
1293  else
1294  {
1295  // both are not constant
1296  return simplify_inequality_no_constant(expr);
1297  }
1298 }
1299 
1303  const binary_relation_exprt &expr)
1304 {
1305  exprt tmp0 = expr.op0();
1306  exprt tmp1 = expr.op1();
1307 
1308  if(tmp0.type().id() == ID_c_enum_tag)
1309  tmp0.type() = ns.follow_tag(to_c_enum_tag_type(tmp0.type()));
1310 
1311  if(tmp1.type().id() == ID_c_enum_tag)
1312  tmp1.type() = ns.follow_tag(to_c_enum_tag_type(tmp1.type()));
1313 
1314  const auto &tmp0_const = to_constant_expr(tmp0);
1315  const auto &tmp1_const = to_constant_expr(tmp1);
1316 
1317  if(expr.id() == ID_equal || expr.id() == ID_notequal)
1318  {
1319  // two constants compare equal when there values (as strings) are the same
1320  // or both of them are pointers and both represent NULL in some way
1321  bool equal = (tmp0_const.get_value() == tmp1_const.get_value());
1322  if(
1323  !equal && tmp0_const.type().id() == ID_pointer &&
1324  tmp1_const.type().id() == ID_pointer)
1325  {
1326  if(
1327  !config.ansi_c.NULL_is_zero && (tmp0_const.get_value() == ID_NULL ||
1328  tmp1_const.get_value() == ID_NULL))
1329  {
1330  // if NULL is not zero on this platform, we really don't know what it
1331  // is and therefore cannot simplify
1332  return unchanged(expr);
1333  }
1334  equal = tmp0_const.is_zero() && tmp1_const.is_zero();
1335  }
1336  return make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
1337  }
1338 
1339  if(tmp0.type().id() == ID_fixedbv)
1340  {
1341  fixedbvt f0(tmp0_const);
1342  fixedbvt f1(tmp1_const);
1343 
1344  if(expr.id() == ID_ge)
1345  return make_boolean_expr(f0 >= f1);
1346  else if(expr.id() == ID_le)
1347  return make_boolean_expr(f0 <= f1);
1348  else if(expr.id() == ID_gt)
1349  return make_boolean_expr(f0 > f1);
1350  else if(expr.id() == ID_lt)
1351  return make_boolean_expr(f0 < f1);
1352  else
1353  UNREACHABLE;
1354  }
1355  else if(tmp0.type().id() == ID_floatbv)
1356  {
1357  ieee_floatt f0(tmp0_const);
1358  ieee_floatt f1(tmp1_const);
1359 
1360  if(expr.id() == ID_ge)
1361  return make_boolean_expr(f0 >= f1);
1362  else if(expr.id() == ID_le)
1363  return make_boolean_expr(f0 <= f1);
1364  else if(expr.id() == ID_gt)
1365  return make_boolean_expr(f0 > f1);
1366  else if(expr.id() == ID_lt)
1367  return make_boolean_expr(f0 < f1);
1368  else
1369  UNREACHABLE;
1370  }
1371  else if(tmp0.type().id() == ID_rational)
1372  {
1373  rationalt r0, r1;
1374 
1375  if(to_rational(tmp0, r0))
1376  return unchanged(expr);
1377 
1378  if(to_rational(tmp1, r1))
1379  return unchanged(expr);
1380 
1381  if(expr.id() == ID_ge)
1382  return make_boolean_expr(r0 >= r1);
1383  else if(expr.id() == ID_le)
1384  return make_boolean_expr(r0 <= r1);
1385  else if(expr.id() == ID_gt)
1386  return make_boolean_expr(r0 > r1);
1387  else if(expr.id() == ID_lt)
1388  return make_boolean_expr(r0 < r1);
1389  else
1390  UNREACHABLE;
1391  }
1392  else
1393  {
1394  const auto v0 = numeric_cast<mp_integer>(tmp0_const);
1395 
1396  if(!v0.has_value())
1397  return unchanged(expr);
1398 
1399  const auto v1 = numeric_cast<mp_integer>(tmp1_const);
1400 
1401  if(!v1.has_value())
1402  return unchanged(expr);
1403 
1404  if(expr.id() == ID_ge)
1405  return make_boolean_expr(*v0 >= *v1);
1406  else if(expr.id() == ID_le)
1407  return make_boolean_expr(*v0 <= *v1);
1408  else if(expr.id() == ID_gt)
1409  return make_boolean_expr(*v0 > *v1);
1410  else if(expr.id() == ID_lt)
1411  return make_boolean_expr(*v0 < *v1);
1412  else
1413  UNREACHABLE;
1414  }
1415 }
1416 
1418  exprt &op0,
1419  exprt &op1)
1420 {
1421  // we can't eliminate zeros
1422  if(op0.is_zero() ||
1423  op1.is_zero() ||
1424  (op0.is_constant() &&
1425  to_constant_expr(op0).get_value()==ID_NULL) ||
1426  (op1.is_constant() &&
1427  to_constant_expr(op1).get_value()==ID_NULL))
1428  return true;
1429 
1430  if(op0.id()==ID_plus)
1431  {
1432  bool no_change = true;
1433 
1434  Forall_operands(it, op0)
1435  if(!eliminate_common_addends(*it, op1))
1436  no_change = false;
1437 
1438  return no_change;
1439  }
1440  else if(op1.id()==ID_plus)
1441  {
1442  bool no_change = true;
1443 
1444  Forall_operands(it, op1)
1445  if(!eliminate_common_addends(op0, *it))
1446  no_change = false;
1447 
1448  return no_change;
1449  }
1450  else if(op0==op1)
1451  {
1452  if(!op0.is_zero() &&
1453  op0.type().id()!=ID_complex)
1454  {
1455  // elimination!
1456  op0=from_integer(0, op0.type());
1457  op1=from_integer(0, op1.type());
1458  return false;
1459  }
1460  }
1461 
1462  return true;
1463 }
1464 
1466  const binary_relation_exprt &expr)
1467 {
1468  // pretty much all of the simplifications below are unsound
1469  // for IEEE float because of NaN!
1470 
1471  if(expr.op0().type().id() == ID_floatbv)
1472  return unchanged(expr);
1473 
1474  // eliminate strict inequalities
1475  if(expr.id()==ID_notequal)
1476  {
1477  auto new_rel_expr = expr;
1478  new_rel_expr.id(ID_equal);
1479  auto new_expr = simplify_inequality_no_constant(new_rel_expr);
1480  return changed(simplify_not(not_exprt(new_expr)));
1481  }
1482  else if(expr.id()==ID_gt)
1483  {
1484  auto new_rel_expr = expr;
1485  new_rel_expr.id(ID_ge);
1486  // swap operands
1487  new_rel_expr.lhs().swap(new_rel_expr.rhs());
1488  auto new_expr = simplify_inequality_no_constant(new_rel_expr);
1489  return changed(simplify_not(not_exprt(new_expr)));
1490  }
1491  else if(expr.id()==ID_lt)
1492  {
1493  auto new_rel_expr = expr;
1494  new_rel_expr.id(ID_ge);
1495  auto new_expr = simplify_inequality_no_constant(new_rel_expr);
1496  return changed(simplify_not(not_exprt(new_expr)));
1497  }
1498  else if(expr.id()==ID_le)
1499  {
1500  auto new_rel_expr = expr;
1501  new_rel_expr.id(ID_ge);
1502  // swap operands
1503  new_rel_expr.lhs().swap(new_rel_expr.rhs());
1504  return changed(simplify_inequality_no_constant(new_rel_expr));
1505  }
1506 
1507  // now we only have >=, =
1508 
1509  INVARIANT(
1510  expr.id() == ID_ge || expr.id() == ID_equal,
1511  "we previously converted all other cases to >= or ==");
1512 
1513  // syntactically equal?
1514 
1515  if(expr.op0() == expr.op1())
1516  return true_exprt();
1517 
1518  // try constants
1519 
1520  value_listt values0, values1;
1521 
1522  bool ok0=!get_values(expr.op0(), values0);
1523  bool ok1=!get_values(expr.op1(), values1);
1524 
1525  if(ok0 && ok1)
1526  {
1527  bool first=true;
1528  bool result=false; // dummy initialization to prevent warning
1529  bool ok=true;
1530 
1531  // compare possible values
1532 
1533  forall_value_list(it0, values0)
1534  forall_value_list(it1, values1)
1535  {
1536  bool tmp;
1537  const mp_integer &int_value0=*it0;
1538  const mp_integer &int_value1=*it1;
1539 
1540  if(expr.id()==ID_ge)
1541  tmp=(int_value0>=int_value1);
1542  else if(expr.id()==ID_equal)
1543  tmp=(int_value0==int_value1);
1544  else
1545  {
1546  tmp=false;
1547  UNREACHABLE;
1548  }
1549 
1550  if(first)
1551  {
1552  result=tmp;
1553  first=false;
1554  }
1555  else if(result!=tmp)
1556  {
1557  ok=false;
1558  break;
1559  }
1560  }
1561 
1562  if(ok)
1563  {
1564  return make_boolean_expr(result);
1565  }
1566  }
1567 
1568  // See if we can eliminate common addends on both sides.
1569  // On bit-vectors, this is only sound on '='.
1570  if(expr.id()==ID_equal)
1571  {
1572  auto new_expr = to_equal_expr(expr);
1573  if(!eliminate_common_addends(new_expr.lhs(), new_expr.rhs()))
1574  {
1575  // remove zeros
1576  new_expr.lhs() = simplify_node(new_expr.lhs());
1577  new_expr.rhs() = simplify_node(new_expr.rhs());
1578  return changed(simplify_inequality(new_expr)); // recursive call
1579  }
1580  }
1581 
1582  return unchanged(expr);
1583 }
1584 
1588  const binary_relation_exprt &expr)
1589 {
1590  // the constant is always on the RHS
1591  PRECONDITION(expr.op1().is_constant());
1592 
1593  if(expr.op0().id()==ID_if && expr.op0().operands().size()==3)
1594  {
1595  if_exprt if_expr=lift_if(expr, 0);
1597  to_binary_relation_expr(if_expr.true_case()));
1599  to_binary_relation_expr(if_expr.false_case()));
1600  return changed(simplify_if(if_expr));
1601  }
1602 
1603  // do we deal with pointers?
1604  if(expr.op1().type().id()==ID_pointer)
1605  {
1606  if(expr.id()==ID_notequal)
1607  {
1608  auto new_rel_expr = expr;
1609  new_rel_expr.id(ID_equal);
1610  auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
1611  return changed(simplify_not(not_exprt(new_expr)));
1612  }
1613 
1614  // very special case for pointers
1615  if(expr.id()==ID_equal &&
1616  expr.op1().is_constant() &&
1617  expr.op1().get(ID_value)==ID_NULL)
1618  {
1619  // the address of an object is never NULL
1620 
1621  if(expr.op0().id() == ID_address_of)
1622  {
1623  const auto &object = to_address_of_expr(expr.op0()).object();
1624 
1625  if(
1626  object.id() == ID_symbol || object.id() == ID_dynamic_object ||
1627  object.id() == ID_member || object.id() == ID_index ||
1628  object.id() == ID_string_constant)
1629  {
1630  return false_exprt();
1631  }
1632  }
1633  else if(
1634  expr.op0().id() == ID_typecast &&
1635  expr.op0().type().id() == ID_pointer &&
1636  to_typecast_expr(expr.op0()).op().id() == ID_address_of)
1637  {
1638  const auto &object =
1640 
1641  if(
1642  object.id() == ID_symbol || object.id() == ID_dynamic_object ||
1643  object.id() == ID_member || object.id() == ID_index ||
1644  object.id() == ID_string_constant)
1645  {
1646  return false_exprt();
1647  }
1648  }
1649  else if(
1650  expr.op0().id() == ID_typecast &&
1651  expr.op0().type().id() == ID_pointer &&
1652  (to_typecast_expr(expr.op0()).op().type().id() == ID_pointer ||
1654  {
1655  // (type)ptr == NULL -> ptr == NULL
1656  // note that 'ptr' may be an integer
1657  exprt op = to_typecast_expr(expr.op0()).op();
1658  auto new_expr = expr;
1659  new_expr.op0().swap(op);
1660  if(new_expr.op0().type().id() != ID_pointer)
1661  new_expr.op1() = from_integer(0, new_expr.op0().type());
1662  else
1663  new_expr.op1().type() = new_expr.op0().type();
1664  return changed(simplify_inequality(new_expr)); // do again!
1665  }
1666  }
1667 
1668  // all we are doing with pointers
1669  return unchanged(expr);
1670  }
1671 
1672  // is it a separation predicate?
1673 
1674  if(expr.op0().id()==ID_plus)
1675  {
1676  // see if there is a constant in the sum
1677 
1678  if(expr.id()==ID_equal || expr.id()==ID_notequal)
1679  {
1680  mp_integer constant=0;
1681  bool op_changed = false;
1682  auto new_expr = expr;
1683 
1684  Forall_operands(it, new_expr.op0())
1685  {
1686  if(it->is_constant())
1687  {
1688  mp_integer i;
1689  if(!to_integer(to_constant_expr(*it), i))
1690  {
1691  constant+=i;
1692  *it=from_integer(0, it->type());
1693  op_changed = true;
1694  }
1695  }
1696  }
1697 
1698  if(op_changed)
1699  {
1700  // adjust the constant on the RHS
1701  mp_integer i =
1702  numeric_cast_v<mp_integer>(to_constant_expr(new_expr.op1()));
1703  i-=constant;
1704  new_expr.op1() = from_integer(i, new_expr.op1().type());
1705 
1706  new_expr.op0() = simplify_plus(to_plus_expr(new_expr.op0()));
1707  return changed(simplify_inequality(new_expr));
1708  }
1709  }
1710  }
1711 
1712  #if 1
1713  // (double)value REL const ---> value rel const
1714  // if 'const' can be represented exactly.
1715 
1716  if(
1717  expr.op0().id() == ID_typecast && expr.op0().type().id() == ID_floatbv &&
1718  to_typecast_expr(expr.op0()).op().type().id() == ID_floatbv)
1719  {
1720  ieee_floatt const_val(to_constant_expr(expr.op1()));
1721  ieee_floatt const_val_converted=const_val;
1722  const_val_converted.change_spec(ieee_float_spect(
1723  to_floatbv_type(to_typecast_expr(expr.op0()).op().type())));
1724  ieee_floatt const_val_converted_back=const_val_converted;
1725  const_val_converted_back.change_spec(
1727  if(const_val_converted_back==const_val)
1728  {
1729  auto result = expr;
1730  result.op0() = to_typecast_expr(expr.op0()).op();
1731  result.op1()=const_val_converted.to_expr();
1732  return std::move(result);
1733  }
1734  }
1735  #endif
1736 
1737  // is the constant zero?
1738 
1739  if(expr.op1().is_zero())
1740  {
1741  if(expr.id()==ID_ge &&
1742  expr.op0().type().id()==ID_unsignedbv)
1743  {
1744  // zero is always smaller or equal something unsigned
1745  return true_exprt();
1746  }
1747 
1748  auto new_expr = expr;
1749  exprt &operand = new_expr.op0();
1750 
1751  if(expr.id()==ID_equal)
1752  {
1753  // rules below do not hold for >=
1754  if(operand.id()==ID_unary_minus)
1755  {
1756  operand = to_unary_minus_expr(operand).op();
1757  return std::move(new_expr);
1758  }
1759  else if(operand.id()==ID_plus)
1760  {
1761  auto &operand_plus_expr = to_plus_expr(operand);
1762 
1763  // simplify a+-b=0 to a=b
1764  if(operand_plus_expr.operands().size() == 2)
1765  {
1766  // if we have -b+a=0, make that a+(-b)=0
1767  if(operand_plus_expr.op0().id() == ID_unary_minus)
1768  operand_plus_expr.op0().swap(operand_plus_expr.op1());
1769 
1770  if(operand_plus_expr.op1().id() == ID_unary_minus)
1771  {
1772  return binary_exprt(
1773  operand_plus_expr.op0(),
1774  expr.id(),
1775  to_unary_minus_expr(operand_plus_expr.op1()).op(),
1776  expr.type());
1777  }
1778  }
1779  }
1780  }
1781  }
1782 
1783  // are we comparing with a typecast from bool?
1784  if(
1785  expr.op0().id() == ID_typecast &&
1786  to_typecast_expr(expr.op0()).op().type().id() == ID_bool)
1787  {
1788  const auto &lhs_typecast_op = to_typecast_expr(expr.op0()).op();
1789 
1790  // we re-write (TYPE)boolean == 0 -> !boolean
1791  if(expr.op1().is_zero() && expr.id()==ID_equal)
1792  {
1793  return changed(simplify_not(not_exprt(lhs_typecast_op)));
1794  }
1795 
1796  // we re-write (TYPE)boolean != 0 -> boolean
1797  if(expr.op1().is_zero() && expr.id()==ID_notequal)
1798  {
1799  return lhs_typecast_op;
1800  }
1801  }
1802 
1803  #define NORMALISE_CONSTANT_TESTS
1804  #ifdef NORMALISE_CONSTANT_TESTS
1805  // Normalise to >= and = to improve caching and term sharing
1806  if(expr.op0().type().id()==ID_unsignedbv ||
1807  expr.op0().type().id()==ID_signedbv)
1808  {
1810 
1811  if(expr.id()==ID_notequal)
1812  {
1813  auto new_rel_expr = expr;
1814  new_rel_expr.id(ID_equal);
1815  auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
1816  return changed(simplify_not(not_exprt(new_expr)));
1817  }
1818  else if(expr.id()==ID_gt)
1819  {
1820  mp_integer i = numeric_cast_v<mp_integer>(to_constant_expr(expr.op1()));
1821 
1822  if(i==max)
1823  {
1824  return false_exprt();
1825  }
1826 
1827  auto new_expr = expr;
1828  new_expr.id(ID_ge);
1829  ++i;
1830  new_expr.op1() = from_integer(i, new_expr.op1().type());
1831  return changed(simplify_inequality_rhs_is_constant(new_expr));
1832  }
1833  else if(expr.id()==ID_lt)
1834  {
1835  auto new_rel_expr = expr;
1836  new_rel_expr.id(ID_ge);
1837  auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
1838  return changed(simplify_not(not_exprt(new_expr)));
1839  }
1840  else if(expr.id()==ID_le)
1841  {
1842  mp_integer i = numeric_cast_v<mp_integer>(to_constant_expr(expr.op1()));
1843 
1844  if(i==max)
1845  {
1846  return true_exprt();
1847  }
1848 
1849  auto new_rel_expr = expr;
1850  new_rel_expr.id(ID_ge);
1851  ++i;
1852  new_rel_expr.op1() = from_integer(i, new_rel_expr.op1().type());
1853  auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
1854  return changed(simplify_not(not_exprt(new_expr)));
1855  }
1856  }
1857 #endif
1858  return unchanged(expr);
1859 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
to_c_enum_tag_type
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: std_types.h:721
ieee_floatt
Definition: ieee_float.h:120
Forall_expr
#define Forall_expr(it, expr)
Definition: expr.h:33
configt::ansi_ct::NULL_is_zero
bool NULL_is_zero
Definition: config.h:88
multi_ary_exprt
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:791
simplify_exprt::simplify_shifts
resultt simplify_shifts(const shift_exprt &)
Definition: simplify_expr_int.cpp:899
rationalt::is_zero
bool is_zero() const
Definition: rational.h:76
extractbits_exprt::lower
exprt & lower()
Definition: std_expr.h:2728
simplify_exprt::simplify_concatenation
resultt simplify_concatenation(const concatenation_exprt &)
Definition: simplify_expr_int.cpp:797
simplify_expr_class.h
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:24
arith_tools.h
is_number
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
Definition: mathematical_types.cpp:17
make_bvrep
irep_idt make_bvrep(const std::size_t width, const std::function< bool(std::size_t)> f)
construct a bit-vector representation from a functor
Definition: arith_tools.cpp:305
rational.h
simplify_exprt::simplify_unary_plus
resultt simplify_unary_plus(const unary_plus_exprt &)
Definition: simplify_expr_int.cpp:1104
simplify_exprt::simplify_bitwise
resultt simplify_bitwise(const multi_ary_exprt &)
Definition: simplify_expr_int.cpp:599
rational_tools.h
address_of_exprt::object
exprt & object()
Definition: std_expr.h:2795
simplify_exprt::simplify_bitnot
resultt simplify_bitnot(const bitnot_exprt &)
Definition: simplify_expr_int.cpp:1171
typet
The type of an expression, extends irept.
Definition: type.h:29
fixedbvt::negate
void negate()
Definition: fixedbv.cpp:90
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
simplify_exprt::simplify_inequality_address_of
resultt simplify_inequality_address_of(const binary_relation_exprt &)
Definition: simplify_expr_pointer.cpp:422
to_rational
bool to_rational(const exprt &expr, rationalt &rational_value)
Definition: rational_tools.cpp:27
fixedbv.h
simplify_exprt::get_values
bool get_values(const exprt &expr, value_listt &value_list)
Definition: simplify_expr.cpp:1330
simplify_exprt::bits2expr
optionalt< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian)
Definition: simplify_expr.cpp:1567
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
ieee_floatt::change_spec
void change_spec(const ieee_float_spect &dest_spec)
Definition: ieee_float.cpp:1044
exprt
Base class for all expressions.
Definition: expr.h:53
simplify_exprt::simplify_extractbit
resultt simplify_extractbit(const extractbit_exprt &)
Definition: simplify_expr_int.cpp:768
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:601
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:65
bswap_exprt::get_bits_per_byte
std::size_t get_bits_per_byte() const
Definition: std_expr.h:485
exprt::op0
exprt & op0()
Definition: expr.h:102
to_integer
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
bool_typet
The Boolean type.
Definition: std_types.h:37
concatenation_exprt
Concatenation of bit-vector operands.
Definition: std_expr.h:4067
lift_if
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:201
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
configt::ansi_c
struct configt::ansi_ct ansi_c
div_exprt
Division.
Definition: std_expr.h:1031
shift_exprt::op
exprt & op()
Definition: std_expr.h:2505
simplify_exprt::simplify_plus
resultt simplify_plus(const plus_exprt &)
Definition: simplify_expr_int.cpp:401
namespace.h
from_rational
constant_exprt from_rational(const rationalt &a)
Definition: rational_tools.cpp:81
fixedbvt::to_expr
constant_exprt to_expr() const
Definition: fixedbv.cpp:43
simplify_exprt::simplify_not
resultt simplify_not(const not_exprt &)
Definition: simplify_expr_boolean.cpp:165
to_minus_expr
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:965
simplify_exprt::simplify_inequality_both_constant
resultt simplify_inequality_both_constant(const binary_relation_exprt &)
simplifies inequalities for the case in which both sides of the inequality are constants
Definition: simplify_expr_int.cpp:1302
simplify_exprt::unchanged
static resultt unchanged(exprt expr)
Definition: simplify_expr_class.h:130
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3001
simplify_exprt::simplify_node
resultt simplify_node(exprt)
Definition: simplify_expr.cpp:2371
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:101
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1216
extractbits_exprt::upper
exprt & upper()
Definition: std_expr.h:2723
ieee_float_spect
Definition: ieee_float.h:26
simplify_exprt::simplify_if
resultt simplify_if(const if_exprt &)
Definition: simplify_expr_if.cpp:331
mathematical_types.h
Mathematical types.
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
simplify_exprt::simplify_minus
resultt simplify_minus(const minus_exprt &)
Definition: simplify_expr_int.cpp:557
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
byte_operators.h
Expression classes for byte-level operators.
simplify_exprt::simplify_power
resultt simplify_power(const binary_exprt &)
Definition: simplify_expr_int.cpp:1007
simplify_exprt::simplify_div
resultt simplify_div(const div_exprt &)
Definition: simplify_expr_int.cpp:270
dstringt::swap
void swap(dstringt &b)
Definition: dstring.h:145
simplify_exprt::simplify_inequality_no_constant
resultt simplify_inequality_no_constant(const binary_relation_exprt &)
Definition: simplify_expr_int.cpp:1465
integer2bvrep
irep_idt integer2bvrep(const mp_integer &src, std::size_t width)
convert an integer to bit-vector representation with given width This uses two's complement for negat...
Definition: arith_tools.cpp:379
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2823
simplify_exprt::simplify_mod
resultt simplify_mod(const mod_exprt &)
Definition: simplify_expr_int.cpp:364
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
multi_ary_exprt::op1
exprt & op1()
Definition: std_expr.h:817
simplify_exprt::changed
static resultt changed(resultt<> result)
Definition: simplify_expr_class.h:135
simplify_exprt::value_listt
std::set< mp_integer > value_listt
Definition: simplify_expr_class.h:229
simplify_exprt::is_bitvector_type
static bool is_bitvector_type(const typet &type)
Definition: simplify_expr_class.h:232
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:100
simplify_exprt::simplify_inequality_rhs_is_constant
resultt simplify_inequality_rhs_is_constant(const binary_relation_exprt &)
Definition: simplify_expr_int.cpp:1587
simplify_exprt::simplify_bswap
resultt simplify_bswap(const bswap_exprt &)
Definition: simplify_expr_int.cpp:28
to_plus_expr
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:920
extractbits_exprt::src
exprt & src()
Definition: std_expr.h:2718
exprt::op1
exprt & op1()
Definition: expr.h:105
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:986
simplify_exprt::simplify_inequality
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
Definition: simplify_expr_int.cpp:1202
to_unary_minus_expr
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:408
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:378
to_integer_bitvector_type
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
Definition: std_types.h:1199
irept::swap
void swap(irept &irep)
Definition: irep.h:463
extractbit_exprt::index
exprt & index()
Definition: std_expr.h:2644
irept::id
const irep_idt & id() const
Definition: irep.h:418
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
unary_plus_exprt
The unary plus expression.
Definition: std_expr.h:427
simplify_exprt::simplify_mult
resultt simplify_mult(const mult_exprt &)
Definition: simplify_expr_int.cpp:158
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
simplify_exprt::resultt
Definition: simplify_expr_class.h:97
ieee_floatt::negate
void negate()
Definition: ieee_float.h:167
simplify_exprt::simplify_unary_minus
resultt simplify_unary_minus(const unary_minus_exprt &)
Definition: simplify_expr_int.cpp:1111
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
bitvector_typet::set_width
void set_width(std::size_t width)
Definition: std_types.h:1046
minus_exprt
Binary minus.
Definition: std_expr.h:940
config
configt config
Definition: config.cpp:24
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
bitnot_exprt
Bit-wise negation of bit-vectors.
Definition: std_expr.h:2344
simplify_exprt::expr2bits
optionalt< std::string > expr2bits(const exprt &, bool little_endian)
Definition: simplify_expr.cpp:1764
mul_expr
static bool mul_expr(constant_exprt &dest, const constant_exprt &expr)
produce a product of two expressions of the same type
Definition: simplify_expr_int.cpp:111
extractbit_exprt
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:2629
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:132
expr_util.h
Deprecated expression utility functions.
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
irept::get_string
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:431
shift_exprt
A base class for shift operators.
Definition: std_expr.h:2496
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2991
simplify_exprt::simplify_inequality_pointer_object
resultt simplify_inequality_pointer_object(const binary_relation_exprt &)
Definition: simplify_expr_pointer.cpp:495
shift_exprt::distance
exprt & distance()
Definition: std_expr.h:2515
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
extractbit_exprt::src
exprt & src()
Definition: std_expr.h:2639
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
ieee_float.h
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:85
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
invariant.h
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:194
to_equal_expr
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1230
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:157
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1424
forall_value_list
#define forall_value_list(it, value_list)
Definition: simplify_expr_class.h:69
config.h
integer_bitvector_typet::largest
mp_integer largest() const
Return the largest value that can be represented using this type.
Definition: std_types.cpp:171
fixedbvt
Definition: fixedbv.h:42
simplify_exprt::simplify_extractbits
resultt simplify_extractbits(const extractbits_exprt &)
Simplifies extracting of bits from a constant.
Definition: simplify_expr_int.cpp:1028
exprt::is_one
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:182
simplify_exprt::ns
const namespacet & ns
Definition: simplify_expr_class.h:246
sum_expr
static bool sum_expr(constant_exprt &dest, const constant_exprt &expr)
produce a sum of two constant expressions of the same type
Definition: simplify_expr_int.cpp:62
bswap_exprt
The byte swap expression.
Definition: std_expr.h:471
ieee_floatt::to_expr
constant_exprt to_expr() const
Definition: ieee_float.cpp:698
make_boolean_expr
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Definition: expr_util.cpp:283
extractbits_exprt
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:2697
exprt::operands
operandst & operands()
Definition: expr.h:95
r
static int8_t r
Definition: irep_hash.h:59
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
simplify_exprt::eliminate_common_addends
bool eliminate_common_addends(exprt &op0, exprt &op1)
Definition: simplify_expr_int.cpp:1417
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:811
binary_exprt::op1
exprt & op1()
Definition: expr.h:105
expr_mapt
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
Definition: acceleration_utils.h:33
std_expr.h
API to expression classes.
to_binary_relation_expr
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:774
constant_exprt::set_value
void set_value(const irep_idt &value)
Definition: std_expr.h:3919
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:3914
rationalt
Definition: rational.h:18
binary_exprt::op0
exprt & op0()
Definition: expr.h:102
fixedbvt::is_zero
bool is_zero() const
Definition: fixedbv.h:71
validation_modet::INVARIANT
@ INVARIANT
mod_exprt
Modulo.
Definition: std_expr.h:1100
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1089
get_bvrep_bit
bool get_bvrep_bit(const irep_idt &src, std::size_t width, std::size_t bit_index)
Get a bit with given index from bit-vector representation.
Definition: arith_tools.cpp:261
rationalt::is_one
bool is_one() const
Definition: rational.h:79
not_exprt
Boolean negation.
Definition: std_expr.h:2843
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939