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  UNREACHABLE;
1488  return false;
1489 }
1490 
1492  exprt &op0,
1493  exprt &op1)
1494 {
1495  // we can't eliminate zeros
1496  if(op0.is_zero() ||
1497  op1.is_zero() ||
1498  (op0.is_constant() &&
1499  to_constant_expr(op0).get_value()==ID_NULL) ||
1500  (op1.is_constant() &&
1501  to_constant_expr(op1).get_value()==ID_NULL))
1502  return true;
1503 
1504  if(op0.id()==ID_plus)
1505  {
1506  bool result=true;
1507 
1508  Forall_operands(it, op0)
1509  if(!eliminate_common_addends(*it, op1))
1510  result=false;
1511 
1512  return result;
1513  }
1514  else if(op1.id()==ID_plus)
1515  {
1516  bool result=true;
1517 
1518  Forall_operands(it, op1)
1519  if(!eliminate_common_addends(op0, *it))
1520  result=false;
1521 
1522  return result;
1523  }
1524  else if(op0==op1)
1525  {
1526  if(!op0.is_zero() &&
1527  op0.type().id()!=ID_complex)
1528  {
1529  // elimination!
1530  op0=from_integer(0, op0.type());
1531  op1=from_integer(0, op1.type());
1532  return false;
1533  }
1534  }
1535 
1536  return true;
1537 }
1538 
1540 {
1541  exprt::operandst &operands=expr.operands();
1542 
1543  // pretty much all of the simplifications below are unsound
1544  // for IEEE float because of NaN!
1545 
1546  if(ns.follow(expr.op0().type()).id()==ID_floatbv)
1547  return true;
1548 
1549  // eliminate strict inequalities
1550  if(expr.id()==ID_notequal)
1551  {
1552  expr.id(ID_equal);
1554  expr.make_not();
1555  simplify_node(expr);
1556  return false;
1557  }
1558  else if(expr.id()==ID_gt)
1559  {
1560  expr.id(ID_ge);
1561  // swap operands
1562  expr.op0().swap(expr.op1());
1564  expr.make_not();
1565  simplify_node(expr);
1566  return false;
1567  }
1568  else if(expr.id()==ID_lt)
1569  {
1570  expr.id(ID_ge);
1572  expr.make_not();
1573  simplify_node(expr);
1574  return false;
1575  }
1576  else if(expr.id()==ID_le)
1577  {
1578  expr.id(ID_ge);
1579  // swap operands
1580  expr.op0().swap(expr.op1());
1582  return false;
1583  }
1584 
1585  // now we only have >=, =
1586 
1587  assert(expr.id()==ID_ge || expr.id()==ID_equal);
1588 
1589  // syntactically equal?
1590 
1591  if(operands.front()==operands.back())
1592  {
1593  expr=true_exprt();
1594  return false;
1595  }
1596 
1597  // try constants
1598 
1599  value_listt values0, values1;
1600 
1601  bool ok0=!get_values(expr.op0(), values0);
1602  bool ok1=!get_values(expr.op1(), values1);
1603 
1604  if(ok0 && ok1)
1605  {
1606  bool first=true;
1607  bool result=false; // dummy initialization to prevent warning
1608  bool ok=true;
1609 
1610  // compare possible values
1611 
1612  forall_value_list(it0, values0)
1613  forall_value_list(it1, values1)
1614  {
1615  bool tmp;
1616  const mp_integer &int_value0=*it0;
1617  const mp_integer &int_value1=*it1;
1618 
1619  if(expr.id()==ID_ge)
1620  tmp=(int_value0>=int_value1);
1621  else if(expr.id()==ID_equal)
1622  tmp=(int_value0==int_value1);
1623  else
1624  {
1625  tmp=false;
1626  UNREACHABLE;
1627  }
1628 
1629  if(first)
1630  {
1631  result=tmp;
1632  first=false;
1633  }
1634  else if(result!=tmp)
1635  {
1636  ok=false;
1637  break;
1638  }
1639  }
1640 
1641  if(ok)
1642  {
1643  expr.make_bool(result);
1644  return false;
1645  }
1646  }
1647 
1648  // See if we can eliminate common addends on both sides.
1649  // On bit-vectors, this is only sound on '='.
1650  if(expr.id()==ID_equal)
1651  {
1652  if(!eliminate_common_addends(expr.op0(), expr.op1()))
1653  {
1654  // remove zeros
1655  simplify_node(expr.op0());
1656  simplify_node(expr.op1());
1657  simplify_inequality(expr); // recursive call
1658  return false;
1659  }
1660  }
1661 
1662  return true;
1663 }
1664 
1667 {
1668  // the constant is always on the RHS
1669  assert(expr.op1().is_constant());
1670 
1671  if(expr.op0().id()==ID_if && expr.op0().operands().size()==3)
1672  {
1673  if_exprt if_expr=lift_if(expr, 0);
1676  simplify_if(if_expr);
1677  expr.swap(if_expr);
1678 
1679  return false;
1680  }
1681 
1682  // do we deal with pointers?
1683  if(expr.op1().type().id()==ID_pointer)
1684  {
1685  if(expr.id()==ID_notequal)
1686  {
1687  expr.id(ID_equal);
1689  expr.make_not();
1690  simplify_node(expr);
1691  return false;
1692  }
1693 
1694  // very special case for pointers
1695  if(expr.id()==ID_equal &&
1696  expr.op1().is_constant() &&
1697  expr.op1().get(ID_value)==ID_NULL)
1698  {
1699  // the address of an object is never NULL
1700 
1701  if(expr.op0().id()==ID_address_of &&
1702  expr.op0().operands().size()==1)
1703  {
1704  if(expr.op0().op0().id()==ID_symbol ||
1705  expr.op0().op0().id()==ID_dynamic_object ||
1706  expr.op0().op0().id()==ID_member ||
1707  expr.op0().op0().id()==ID_index ||
1708  expr.op0().op0().id()==ID_string_constant)
1709  {
1710  expr=false_exprt();
1711  return false;
1712  }
1713  }
1714  else if(expr.op0().id()==ID_typecast &&
1715  expr.op0().operands().size()==1 &&
1716  expr.op0().type().id()==ID_pointer &&
1717  expr.op0().op0().id()==ID_address_of &&
1718  expr.op0().op0().operands().size()==1)
1719  {
1720  if(expr.op0().op0().op0().id()==ID_symbol ||
1721  expr.op0().op0().op0().id()==ID_dynamic_object ||
1722  expr.op0().op0().op0().id()==ID_member ||
1723  expr.op0().op0().op0().id()==ID_index ||
1724  expr.op0().op0().op0().id()==ID_string_constant)
1725  {
1726  expr=false_exprt();
1727  return false;
1728  }
1729  }
1730  else if(expr.op0().id()==ID_typecast &&
1731  expr.op0().operands().size()==1 &&
1732  expr.op0().type().id()==ID_pointer &&
1733  (expr.op0().op0().type().id()==ID_pointer ||
1735  {
1736  // (type)ptr == NULL -> ptr == NULL
1737  // note that 'ptr' may be an integer
1738  exprt op=expr.op0().op0();
1739  expr.op0().swap(op);
1740  if(expr.op0().type().id()!=ID_pointer)
1741  expr.op1()=from_integer(0, expr.op0().type());
1742  else
1743  expr.op1().type()=expr.op0().type();
1744  simplify_inequality(expr); // do again!
1745  return false;
1746  }
1747  }
1748 
1749  // all we are doing with pointers
1750  return true;
1751  }
1752 
1753  // is it a separation predicate?
1754 
1755  if(expr.op0().id()==ID_plus)
1756  {
1757  // see if there is a constant in the sum
1758 
1759  if(expr.id()==ID_equal || expr.id()==ID_notequal)
1760  {
1761  mp_integer constant=0;
1762  bool changed=false;
1763 
1764  Forall_operands(it, expr.op0())
1765  {
1766  if(it->is_constant())
1767  {
1768  mp_integer i;
1769  if(!to_integer(*it, i))
1770  {
1771  constant+=i;
1772  *it=from_integer(0, it->type());
1773  assert(it->is_not_nil());
1774  changed=true;
1775  }
1776  }
1777  }
1778 
1779  if(changed)
1780  {
1781  // adjust constant
1782  mp_integer i;
1783  to_integer(expr.op1(), i);
1784  i-=constant;
1785  expr.op1()=from_integer(i, expr.op1().type());
1786 
1787  simplify_plus(expr.op0());
1788  simplify_inequality(expr);
1789  return false;
1790  }
1791  }
1792  }
1793 
1794  #if 1
1795  // (double)value REL const ---> value rel const
1796  // if 'const' can be represented exactly.
1797 
1798  if(expr.op0().id()==ID_typecast &&
1799  expr.op0().operands().size()==1 &&
1800  ns.follow(expr.op0().type()).id()==ID_floatbv &&
1801  ns.follow(expr.op0().op0().type()).id()==ID_floatbv)
1802  {
1803  ieee_floatt const_val(to_constant_expr(expr.op1()));
1804  ieee_floatt const_val_converted=const_val;
1805  const_val_converted.change_spec(
1807  ieee_floatt const_val_converted_back=const_val_converted;
1808  const_val_converted_back.change_spec(
1810  if(const_val_converted_back==const_val)
1811  {
1812  exprt result=expr;
1813  result.op0()=expr.op0().op0();
1814  result.op1()=const_val_converted.to_expr();
1815  expr.swap(result);
1816  return false;
1817  }
1818  }
1819  #endif
1820 
1821  // is the constant zero?
1822 
1823  if(expr.op1().is_zero())
1824  {
1825  if(expr.id()==ID_ge &&
1826  expr.op0().type().id()==ID_unsignedbv)
1827  {
1828  // zero is always smaller or equal something unsigned
1829  expr=true_exprt();
1830  return false;
1831  }
1832 
1833  exprt &operand=expr.op0();
1834 
1835  if(expr.id()==ID_equal)
1836  {
1837  // rules below do not hold for >=
1838  if(operand.id()==ID_unary_minus)
1839  {
1840  if(operand.operands().size()!=1)
1841  return true;
1842  exprt tmp;
1843  tmp.swap(operand.op0());
1844  operand.swap(tmp);
1845  return false;
1846  }
1847  else if(operand.id()==ID_plus)
1848  {
1849  // simplify a+-b=0 to a=b
1850 
1851  if(operand.operands().size()==2)
1852  {
1853  // if we have -b+a=0, make that a+(-b)=0
1854 
1855  if(operand.op0().id()==ID_unary_minus)
1856  operand.op0().swap(operand.op1());
1857 
1858  if(operand.op1().id()==ID_unary_minus &&
1859  operand.op1().operands().size()==1)
1860  {
1861  exprt tmp(expr.id(), expr.type());
1862  tmp.operands().resize(2);
1863  tmp.op0().swap(operand.op0());
1864  tmp.op1().swap(operand.op1().op0());
1865  expr.swap(tmp);
1866  return false;
1867  }
1868  }
1869  }
1870  }
1871  }
1872 
1873  // are we comparing with a typecast from bool?
1874  if(expr.op0().id()==ID_typecast &&
1875  expr.op0().operands().size()==1 &&
1876  expr.op0().op0().type().id()==ID_bool)
1877  {
1878  // we re-write (TYPE)boolean == 0 -> !boolean
1879  if(expr.op1().is_zero() && expr.id()==ID_equal)
1880  {
1881  expr=expr.op0().op0();
1882  expr.make_not();
1883  return false;
1884  }
1885 
1886  // we re-write (TYPE)boolean != 0 -> boolean
1887  if(expr.op1().is_zero() && expr.id()==ID_notequal)
1888  {
1889  expr=expr.op0().op0();
1890  return false;
1891  }
1892  }
1893 
1894  #define NORMALISE_CONSTANT_TESTS
1895  #ifdef NORMALISE_CONSTANT_TESTS
1896  // Normalise to >= and = to improve caching and term sharing
1897  if(expr.op0().type().id()==ID_unsignedbv ||
1898  expr.op0().type().id()==ID_signedbv)
1899  {
1900  bv_spect spec(expr.op0().type());
1901  mp_integer max(spec.max_value());
1902 
1903  if(expr.id()==ID_notequal)
1904  {
1905  expr.id(ID_equal);
1907  expr.make_not();
1908  simplify_node(expr);
1909  return false;
1910  }
1911  else if(expr.id()==ID_gt)
1912  {
1913  mp_integer i;
1914  if(to_integer(expr.op1(), i))
1915  throw "bit-vector constant unexpectedly non-integer";
1916 
1917  if(i==max)
1918  {
1919  expr=false_exprt();
1920  return false;
1921  }
1922 
1923  expr.id(ID_ge);
1924  ++i;
1925  expr.op1()=from_integer(i, expr.op1().type());
1927  return false;
1928  }
1929  else if(expr.id()==ID_lt)
1930  {
1931  expr.id(ID_ge);
1933  expr.make_not();
1934  simplify_node(expr);
1935  return false;
1936  }
1937  else if(expr.id()==ID_le)
1938  {
1939  mp_integer i;
1940  if(to_integer(expr.op1(), i))
1941  throw "bit-vector constant unexpectedly non-integer";
1942 
1943  if(i==max)
1944  {
1945  expr=true_exprt();
1946  return false;
1947  }
1948 
1949  expr.id(ID_ge);
1950  ++i;
1951  expr.op1()=from_integer(i, expr.op1().type());
1953  expr.make_not();
1954  simplify_node(expr);
1955  return false;
1956  }
1957  }
1958 #endif
1959  return true;
1960 }
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:1220
exprt & true_case()
Definition: std_expr.h:3395
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:102
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
bool is_not_nil() const
Definition: irep.h:103
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:1150
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:3106
bool is_false() const
Definition: expr.cpp:131
const irep_idt & get_value() const
Definition: std_expr.h:4441
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:3361
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:4424
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:74
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:189
void set_value(const irep_idt &value)
Definition: std_expr.h:4446
The boolean constant true.
Definition: std_expr.h:4488
#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:3096
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:3072
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:3101
size_t size() const
Definition: dstring.h:77
const typet & follow(const typet &) const
Definition: namespace.cpp:55
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:3405
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:4465
bool has_operands() const
Definition: expr.h:63
The boolean constant false.
Definition: std_expr.h:4499
bool simplify_unary_plus(exprt &expr)
bool is_constant() const
Definition: expr.cpp:119
std::size_t get_width() const
Definition: std_types.h:1129
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:1373
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:185
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:250
The NIL type.
Definition: std_types.h:44
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
void swap(irept &irep)
Definition: irep.h:231
#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:257
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:214
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.