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