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