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