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