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 "c_types.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_plus(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_boolean(new_expr);
650 
651  return changed(simplify_typecast(typecast_exprt(new_expr, expr.type())));
652  }
653  }
654 
655  bool no_change = true;
656  auto new_expr = expr;
657 
658  // try to merge constants
659 
660  const std::size_t width = to_bitvector_type(expr.type()).get_width();
661 
662  while(new_expr.operands().size() >= 2)
663  {
664  if(!new_expr.op0().is_constant())
665  break;
666 
667  if(!new_expr.op1().is_constant())
668  break;
669 
670  if(new_expr.op0().type() != new_expr.type())
671  break;
672 
673  if(new_expr.op1().type() != new_expr.type())
674  break;
675 
676  const auto &a_val = to_constant_expr(new_expr.op0()).get_value();
677  const auto &b_val = to_constant_expr(new_expr.op1()).get_value();
678 
679  std::function<bool(bool, bool)> f;
680 
681  if(new_expr.id() == ID_bitand)
682  f = [](bool a, bool b) { return a && b; };
683  else if(new_expr.id() == ID_bitor)
684  f = [](bool a, bool b) { return a || b; };
685  else if(new_expr.id() == ID_bitxor)
686  f = [](bool a, bool b) { return a != b; };
687  else
688  UNREACHABLE;
689 
690  const irep_idt new_value =
691  make_bvrep(width, [&a_val, &b_val, &width, &f](std::size_t i) {
692  return f(
693  get_bvrep_bit(a_val, width, i), get_bvrep_bit(b_val, width, i));
694  });
695 
696  constant_exprt new_op(new_value, expr.type());
697 
698  // erase first operand
699  new_expr.operands().erase(new_expr.operands().begin());
700  new_expr.op0().swap(new_op);
701 
702  no_change = false;
703  }
704 
705  // now erase 'all zeros' out of bitor, bitxor
706 
707  if(new_expr.id() == ID_bitor || new_expr.id() == ID_bitxor)
708  {
709  for(exprt::operandst::iterator it = new_expr.operands().begin();
710  it != new_expr.operands().end();) // no it++
711  {
712  if(it->is_zero() && new_expr.operands().size() > 1)
713  {
714  it = new_expr.operands().erase(it);
715  no_change = false;
716  }
717  else if(
718  it->is_constant() && it->type().id() == ID_bv &&
720  new_expr.operands().size() > 1)
721  {
722  it = new_expr.operands().erase(it);
723  no_change = false;
724  }
725  else
726  it++;
727  }
728  }
729 
730  // now erase 'all ones' out of bitand
731 
732  if(new_expr.id() == ID_bitand)
733  {
734  const auto all_ones = power(2, width) - 1;
735  for(exprt::operandst::iterator it = new_expr.operands().begin();
736  it != new_expr.operands().end();) // no it++
737  {
738  if(
739  it->is_constant() &&
740  bvrep2integer(to_constant_expr(*it).get_value(), width, false) ==
741  all_ones &&
742  new_expr.operands().size() > 1)
743  {
744  it = new_expr.operands().erase(it);
745  no_change = false;
746  }
747  else
748  it++;
749  }
750  }
751 
752  // two operands that are syntactically the same
753 
754  if(new_expr.operands().size() == 2 && new_expr.op0() == new_expr.op1())
755  {
756  if(new_expr.id() == ID_bitand || new_expr.id() == ID_bitor)
757  {
758  return new_expr.op0();
759  }
760  else if(new_expr.id() == ID_bitxor)
761  {
762  return constant_exprt(integer2bvrep(0, width), new_expr.type());
763  }
764  }
765 
766  if(new_expr.operands().size() == 1)
767  return new_expr.op0();
768 
769  if(no_change)
770  return unchanged(expr);
771  else
772  return std::move(new_expr);
773 }
774 
777 {
778  const typet &src_type = expr.src().type();
779 
780  if(!is_bitvector_type(src_type))
781  return unchanged(expr);
782 
783  const std::size_t src_bit_width = to_bitvector_type(src_type).get_width();
784 
785  const auto index_converted_to_int = numeric_cast<mp_integer>(expr.index());
786  if(
787  !index_converted_to_int.has_value() || *index_converted_to_int < 0 ||
788  *index_converted_to_int >= src_bit_width)
789  {
790  return unchanged(expr);
791  }
792 
793  if(!expr.src().is_constant())
794  return unchanged(expr);
795 
796  const bool bit = get_bvrep_bit(
797  to_constant_expr(expr.src()).get_value(),
798  src_bit_width,
799  numeric_cast_v<std::size_t>(*index_converted_to_int));
800 
801  return make_boolean_expr(bit);
802 }
803 
806 {
807  bool no_change = true;
808 
809  concatenation_exprt new_expr = expr;
810 
811  if(is_bitvector_type(new_expr.type()))
812  {
813  // first, turn bool into bvec[1]
814  Forall_operands(it, new_expr)
815  {
816  exprt &op=*it;
817  if(op.is_true() || op.is_false())
818  {
819  const bool value = op.is_true();
820  op = from_integer(value, unsignedbv_typet(1));
821  no_change = false;
822  }
823  }
824 
825  // search for neighboring constants to merge
826  size_t i=0;
827 
828  while(i < new_expr.operands().size() - 1)
829  {
830  exprt &opi = new_expr.operands()[i];
831  exprt &opn = new_expr.operands()[i + 1];
832 
833  if(opi.is_constant() &&
834  opn.is_constant() &&
835  is_bitvector_type(opi.type()) &&
836  is_bitvector_type(opn.type()))
837  {
838  // merge!
839  const auto &value_i = to_constant_expr(opi).get_value();
840  const auto &value_n = to_constant_expr(opn).get_value();
841  const auto width_i = to_bitvector_type(opi.type()).get_width();
842  const auto width_n = to_bitvector_type(opn.type()).get_width();
843  const auto new_width = width_i + width_n;
844 
845  const auto new_value = make_bvrep(
846  new_width, [&value_i, &value_n, width_i, width_n](std::size_t x) {
847  return x < width_n ? get_bvrep_bit(value_n, width_n, x)
848  : get_bvrep_bit(value_i, width_i, x - width_n);
849  });
850 
851  to_constant_expr(opi).set_value(new_value);
852  to_bitvector_type(opi.type()).set_width(new_width);
853  // erase opn
854  new_expr.operands().erase(new_expr.operands().begin() + i + 1);
855  no_change = false;
856  }
857  else
858  i++;
859  }
860  }
861  else if(new_expr.type().id() == ID_verilog_unsignedbv)
862  {
863  // search for neighboring constants to merge
864  size_t i=0;
865 
866  while(i < new_expr.operands().size() - 1)
867  {
868  exprt &opi = new_expr.operands()[i];
869  exprt &opn = new_expr.operands()[i + 1];
870 
871  if(opi.is_constant() &&
872  opn.is_constant() &&
873  (opi.type().id()==ID_verilog_unsignedbv ||
874  is_bitvector_type(opi.type())) &&
875  (opn.type().id()==ID_verilog_unsignedbv ||
876  is_bitvector_type(opn.type())))
877  {
878  // merge!
879  const std::string new_value=
880  opi.get_string(ID_value)+opn.get_string(ID_value);
881  opi.set(ID_value, new_value);
882  to_bitvector_type(opi.type()).set_width(new_value.size());
883  opi.type().id(ID_verilog_unsignedbv);
884  // erase opn
885  new_expr.operands().erase(new_expr.operands().begin() + i + 1);
886  no_change = false;
887  }
888  else
889  i++;
890  }
891  }
892 
893  // { x } = x
894  if(
895  new_expr.operands().size() == 1 && new_expr.op0().type() == new_expr.type())
896  {
897  return new_expr.op0();
898  }
899 
900  if(no_change)
901  return unchanged(expr);
902  else
903  return std::move(new_expr);
904 }
905 
908 {
909  if(!is_bitvector_type(expr.type()))
910  return unchanged(expr);
911 
912  const auto distance = numeric_cast<mp_integer>(expr.distance());
913 
914  if(!distance.has_value())
915  return unchanged(expr);
916 
917  if(*distance == 0)
918  return expr.op();
919 
920  auto value = numeric_cast<mp_integer>(expr.op());
921 
922  if(
923  !value.has_value() && expr.op().type().id() == ID_bv &&
924  expr.op().id() == ID_constant)
925  {
926  const std::size_t width = to_bitvector_type(expr.op().type()).get_width();
927  value =
928  bvrep2integer(to_constant_expr(expr.op()).get_value(), width, false);
929  }
930 
931  if(!value.has_value())
932  return unchanged(expr);
933 
934  if(
935  expr.op().type().id() == ID_unsignedbv ||
936  expr.op().type().id() == ID_signedbv || expr.op().type().id() == ID_bv)
937  {
938  const std::size_t width = to_bitvector_type(expr.op().type()).get_width();
939 
940  if(expr.id()==ID_lshr)
941  {
942  // this is to guard against large values of distance
943  if(*distance >= width)
944  {
945  return from_integer(0, expr.type());
946  }
947  else if(*distance >= 0)
948  {
949  if(*value < 0)
950  *value += power(2, width);
951  *value /= power(2, *distance);
952  return from_integer(*value, expr.type());
953  }
954  }
955  else if(expr.id()==ID_ashr)
956  {
957  if(*distance >= 0)
958  {
959  // this is to simulate an arithmetic right shift
960  mp_integer new_value = *value >> *distance;
961  return from_integer(new_value, expr.type());
962  }
963  }
964  else if(expr.id()==ID_shl)
965  {
966  // this is to guard against large values of distance
967  if(*distance >= width)
968  {
969  return from_integer(0, expr.type());
970  }
971  else if(*distance >= 0)
972  {
973  *value *= power(2, *distance);
974  return from_integer(*value, expr.type());
975  }
976  }
977  }
978  else if(
979  expr.op().type().id() == ID_integer || expr.op().type().id() == ID_natural)
980  {
981  if(expr.id()==ID_lshr)
982  {
983  if(*distance >= 0)
984  {
985  *value /= power(2, *distance);
986  return from_integer(*value, expr.type());
987  }
988  }
989  else if(expr.id()==ID_ashr)
990  {
991  // this is to simulate an arithmetic right shift
992  if(*distance >= 0)
993  {
994  mp_integer new_value = *value / power(2, *distance);
995  if(*value < 0 && new_value == 0)
996  new_value=-1;
997 
998  return from_integer(new_value, expr.type());
999  }
1000  }
1001  else if(expr.id()==ID_shl)
1002  {
1003  if(*distance >= 0)
1004  {
1005  *value *= power(2, *distance);
1006  return from_integer(*value, expr.type());
1007  }
1008  }
1009  }
1010 
1011  return unchanged(expr);
1012 }
1013 
1016 {
1017  if(!is_number(expr.type()))
1018  return unchanged(expr);
1019 
1020  const auto base = numeric_cast<mp_integer>(expr.op0());
1021  const auto exponent = numeric_cast<mp_integer>(expr.op1());
1022 
1023  if(!base.has_value())
1024  return unchanged(expr);
1025 
1026  if(!exponent.has_value())
1027  return unchanged(expr);
1028 
1029  mp_integer result = power(*base, *exponent);
1030 
1031  return from_integer(result, expr.type());
1032 }
1033 
1037 {
1038  const typet &op0_type = expr.src().type();
1039 
1040  if(!is_bitvector_type(op0_type) &&
1041  !is_bitvector_type(expr.type()))
1042  {
1043  return unchanged(expr);
1044  }
1045 
1046  const auto start = numeric_cast<mp_integer>(expr.upper());
1047  const auto end = numeric_cast<mp_integer>(expr.lower());
1048 
1049  if(!start.has_value())
1050  return unchanged(expr);
1051 
1052  if(!end.has_value())
1053  return unchanged(expr);
1054 
1055  const auto width = pointer_offset_bits(op0_type, ns);
1056 
1057  if(!width.has_value())
1058  return unchanged(expr);
1059 
1060  if(*start < 0 || *start >= (*width) || *end < 0 || *end >= (*width))
1061  return unchanged(expr);
1062 
1063  DATA_INVARIANT(*start >= *end, "extractbits must have upper() >= lower()");
1064 
1065  if(expr.src().is_constant())
1066  {
1067  const auto svalue = expr2bits(expr.src(), true, ns);
1068 
1069  if(!svalue.has_value() || svalue->size() != *width)
1070  return unchanged(expr);
1071 
1072  std::string extracted_value = svalue->substr(
1073  numeric_cast_v<std::size_t>(*end),
1074  numeric_cast_v<std::size_t>(*start - *end + 1));
1075 
1076  auto result = bits2expr(extracted_value, expr.type(), true, ns);
1077  if(!result.has_value())
1078  return unchanged(expr);
1079 
1080  return std::move(*result);
1081  }
1082  else if(expr.src().id() == ID_concatenation)
1083  {
1084  // the most-significant bit comes first in an concatenation_exprt, hence we
1085  // count down
1086  mp_integer offset = *width;
1087 
1088  forall_operands(it, expr.src())
1089  {
1090  auto op_width = pointer_offset_bits(it->type(), ns);
1091 
1092  if(!op_width.has_value() || *op_width <= 0)
1093  return unchanged(expr);
1094 
1095  if(*start + 1 == offset && *end + *op_width == offset)
1096  {
1097  exprt tmp = *it;
1098  if(tmp.type() != expr.type())
1099  return unchanged(expr);
1100 
1101  return std::move(tmp);
1102  }
1103 
1104  offset -= *op_width;
1105  }
1106  }
1107 
1108  return unchanged(expr);
1109 }
1110 
1113 {
1114  // simply remove, this is always 'nop'
1115  return expr.op();
1116 }
1117 
1120 {
1121  if(!is_number(expr.type()))
1122  return unchanged(expr);
1123 
1124  const exprt &operand = expr.op();
1125 
1126  if(expr.type()!=operand.type())
1127  return unchanged(expr);
1128 
1129  if(operand.id()==ID_unary_minus)
1130  {
1131  // cancel out "-(-x)" to "x"
1132  if(!is_number(to_unary_minus_expr(operand).op().type()))
1133  return unchanged(expr);
1134 
1135  return to_unary_minus_expr(operand).op();
1136  }
1137  else if(operand.id()==ID_constant)
1138  {
1139  const irep_idt &type_id=expr.type().id();
1140  const auto &constant_expr = to_constant_expr(operand);
1141 
1142  if(type_id==ID_integer ||
1143  type_id==ID_signedbv ||
1144  type_id==ID_unsignedbv)
1145  {
1146  const auto int_value = numeric_cast<mp_integer>(constant_expr);
1147 
1148  if(!int_value.has_value())
1149  return unchanged(expr);
1150 
1151  return from_integer(-*int_value, expr.type());
1152  }
1153  else if(type_id==ID_rational)
1154  {
1155  rationalt r;
1156  if(to_rational(constant_expr, r))
1157  return unchanged(expr);
1158 
1159  return from_rational(-r);
1160  }
1161  else if(type_id==ID_fixedbv)
1162  {
1163  fixedbvt f(constant_expr);
1164  f.negate();
1165  return f.to_expr();
1166  }
1167  else if(type_id==ID_floatbv)
1168  {
1169  ieee_floatt f(constant_expr);
1170  f.negate();
1171  return f.to_expr();
1172  }
1173  }
1174 
1175  return unchanged(expr);
1176 }
1177 
1180 {
1181  const exprt &op = expr.op();
1182 
1183  const auto &type = expr.type();
1184 
1185  if(
1186  type.id() == ID_bv || type.id() == ID_unsignedbv ||
1187  type.id() == ID_signedbv)
1188  {
1189  const auto width = to_bitvector_type(type).get_width();
1190 
1191  if(op.type() == type)
1192  {
1193  if(op.id()==ID_constant)
1194  {
1195  const auto &value = to_constant_expr(op).get_value();
1196  const auto new_value =
1197  make_bvrep(width, [&value, &width](std::size_t i) {
1198  return !get_bvrep_bit(value, width, i);
1199  });
1200  return constant_exprt(new_value, op.type());
1201  }
1202  }
1203  }
1204 
1205  return unchanged(expr);
1206 }
1207 
1211 {
1212  if(expr.type().id()!=ID_bool)
1213  return unchanged(expr);
1214 
1215  exprt tmp0=expr.op0();
1216  exprt tmp1=expr.op1();
1217 
1218  // types must match
1219  if(tmp0.type() != tmp1.type())
1220  return unchanged(expr);
1221 
1222  // if rhs is ID_if (and lhs is not), swap operands for == and !=
1223  if((expr.id()==ID_equal || expr.id()==ID_notequal) &&
1224  tmp0.id()!=ID_if &&
1225  tmp1.id()==ID_if)
1226  {
1227  auto new_expr = expr;
1228  new_expr.op0().swap(new_expr.op1());
1229  return changed(simplify_inequality(new_expr)); // recursive call
1230  }
1231 
1232  if(tmp0.id()==ID_if && tmp0.operands().size()==3)
1233  {
1234  if_exprt if_expr=lift_if(expr, 0);
1235  if_expr.true_case() =
1237  if_expr.false_case() =
1239  return changed(simplify_if(if_expr));
1240  }
1241 
1242  // see if we are comparing pointers that are address_of
1243  if(
1244  skip_typecast(tmp0).id() == ID_address_of &&
1245  skip_typecast(tmp1).id() == ID_address_of &&
1246  (expr.id() == ID_equal || expr.id() == ID_notequal))
1247  {
1248  return simplify_inequality_address_of(expr);
1249  }
1250 
1251  if(tmp0.id()==ID_pointer_object &&
1252  tmp1.id()==ID_pointer_object &&
1253  (expr.id()==ID_equal || expr.id()==ID_notequal))
1254  {
1256  }
1257 
1258  if(tmp0.type().id()==ID_c_enum_tag)
1259  tmp0.type()=ns.follow_tag(to_c_enum_tag_type(tmp0.type()));
1260 
1261  if(tmp1.type().id()==ID_c_enum_tag)
1262  tmp1.type()=ns.follow_tag(to_c_enum_tag_type(tmp1.type()));
1263 
1264  const bool tmp0_const = tmp0.is_constant();
1265  const bool tmp1_const = tmp1.is_constant();
1266 
1267  // are _both_ constant?
1268  if(tmp0_const && tmp1_const)
1269  {
1270  return simplify_inequality_both_constant(expr);
1271  }
1272  else if(tmp0_const)
1273  {
1274  // we want the constant on the RHS
1275 
1276  binary_relation_exprt new_expr = expr;
1277 
1278  if(expr.id()==ID_ge)
1279  new_expr.id(ID_le);
1280  else if(expr.id()==ID_le)
1281  new_expr.id(ID_ge);
1282  else if(expr.id()==ID_gt)
1283  new_expr.id(ID_lt);
1284  else if(expr.id()==ID_lt)
1285  new_expr.id(ID_gt);
1286 
1287  new_expr.op0().swap(new_expr.op1());
1288 
1289  // RHS is constant, LHS is not
1290  return changed(simplify_inequality_rhs_is_constant(new_expr));
1291  }
1292  else if(tmp1_const)
1293  {
1294  // RHS is constant, LHS is not
1296  }
1297  else
1298  {
1299  // both are not constant
1300  return simplify_inequality_no_constant(expr);
1301  }
1302 }
1303 
1307  const binary_relation_exprt &expr)
1308 {
1309  exprt tmp0 = expr.op0();
1310  exprt tmp1 = expr.op1();
1311 
1312  if(tmp0.type().id() == ID_c_enum_tag)
1313  tmp0.type() = ns.follow_tag(to_c_enum_tag_type(tmp0.type()));
1314 
1315  if(tmp1.type().id() == ID_c_enum_tag)
1316  tmp1.type() = ns.follow_tag(to_c_enum_tag_type(tmp1.type()));
1317 
1318  const auto &tmp0_const = to_constant_expr(tmp0);
1319  const auto &tmp1_const = to_constant_expr(tmp1);
1320 
1321  if(expr.id() == ID_equal || expr.id() == ID_notequal)
1322  {
1323  // two constants compare equal when there values (as strings) are the same
1324  // or both of them are pointers and both represent NULL in some way
1325  bool equal = (tmp0_const.get_value() == tmp1_const.get_value());
1326  if(
1327  !equal && tmp0_const.type().id() == ID_pointer &&
1328  tmp1_const.type().id() == ID_pointer)
1329  {
1330  if(
1331  !config.ansi_c.NULL_is_zero && (tmp0_const.get_value() == ID_NULL ||
1332  tmp1_const.get_value() == ID_NULL))
1333  {
1334  // if NULL is not zero on this platform, we really don't know what it
1335  // is and therefore cannot simplify
1336  return unchanged(expr);
1337  }
1338  equal = tmp0_const.is_zero() && tmp1_const.is_zero();
1339  }
1340  return make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
1341  }
1342 
1343  if(tmp0.type().id() == ID_fixedbv)
1344  {
1345  fixedbvt f0(tmp0_const);
1346  fixedbvt f1(tmp1_const);
1347 
1348  if(expr.id() == ID_ge)
1349  return make_boolean_expr(f0 >= f1);
1350  else if(expr.id() == ID_le)
1351  return make_boolean_expr(f0 <= f1);
1352  else if(expr.id() == ID_gt)
1353  return make_boolean_expr(f0 > f1);
1354  else if(expr.id() == ID_lt)
1355  return make_boolean_expr(f0 < f1);
1356  else
1357  UNREACHABLE;
1358  }
1359  else if(tmp0.type().id() == ID_floatbv)
1360  {
1361  ieee_floatt f0(tmp0_const);
1362  ieee_floatt f1(tmp1_const);
1363 
1364  if(expr.id() == ID_ge)
1365  return make_boolean_expr(f0 >= f1);
1366  else if(expr.id() == ID_le)
1367  return make_boolean_expr(f0 <= f1);
1368  else if(expr.id() == ID_gt)
1369  return make_boolean_expr(f0 > f1);
1370  else if(expr.id() == ID_lt)
1371  return make_boolean_expr(f0 < f1);
1372  else
1373  UNREACHABLE;
1374  }
1375  else if(tmp0.type().id() == ID_rational)
1376  {
1377  rationalt r0, r1;
1378 
1379  if(to_rational(tmp0, r0))
1380  return unchanged(expr);
1381 
1382  if(to_rational(tmp1, r1))
1383  return unchanged(expr);
1384 
1385  if(expr.id() == ID_ge)
1386  return make_boolean_expr(r0 >= r1);
1387  else if(expr.id() == ID_le)
1388  return make_boolean_expr(r0 <= r1);
1389  else if(expr.id() == ID_gt)
1390  return make_boolean_expr(r0 > r1);
1391  else if(expr.id() == ID_lt)
1392  return make_boolean_expr(r0 < r1);
1393  else
1394  UNREACHABLE;
1395  }
1396  else
1397  {
1398  const auto v0 = numeric_cast<mp_integer>(tmp0_const);
1399 
1400  if(!v0.has_value())
1401  return unchanged(expr);
1402 
1403  const auto v1 = numeric_cast<mp_integer>(tmp1_const);
1404 
1405  if(!v1.has_value())
1406  return unchanged(expr);
1407 
1408  if(expr.id() == ID_ge)
1409  return make_boolean_expr(*v0 >= *v1);
1410  else if(expr.id() == ID_le)
1411  return make_boolean_expr(*v0 <= *v1);
1412  else if(expr.id() == ID_gt)
1413  return make_boolean_expr(*v0 > *v1);
1414  else if(expr.id() == ID_lt)
1415  return make_boolean_expr(*v0 < *v1);
1416  else
1417  UNREACHABLE;
1418  }
1419 }
1420 
1421 static bool eliminate_common_addends(exprt &op0, exprt &op1)
1422 {
1423  // we can't eliminate zeros
1424  if(op0.is_zero() ||
1425  op1.is_zero() ||
1426  (op0.is_constant() &&
1427  to_constant_expr(op0).get_value()==ID_NULL) ||
1428  (op1.is_constant() &&
1429  to_constant_expr(op1).get_value()==ID_NULL))
1430  return true;
1431 
1432  if(op0.id()==ID_plus)
1433  {
1434  bool no_change = true;
1435 
1436  Forall_operands(it, op0)
1437  if(!eliminate_common_addends(*it, op1))
1438  no_change = false;
1439 
1440  return no_change;
1441  }
1442  else if(op1.id()==ID_plus)
1443  {
1444  bool no_change = true;
1445 
1446  Forall_operands(it, op1)
1447  if(!eliminate_common_addends(op0, *it))
1448  no_change = false;
1449 
1450  return no_change;
1451  }
1452  else if(op0==op1)
1453  {
1454  if(!op0.is_zero() &&
1455  op0.type().id()!=ID_complex)
1456  {
1457  // elimination!
1458  op0=from_integer(0, op0.type());
1459  op1=from_integer(0, op1.type());
1460  return false;
1461  }
1462  }
1463 
1464  return true;
1465 }
1466 
1468  const binary_relation_exprt &expr)
1469 {
1470  // pretty much all of the simplifications below are unsound
1471  // for IEEE float because of NaN!
1472 
1473  if(expr.op0().type().id() == ID_floatbv)
1474  return unchanged(expr);
1475 
1476  // eliminate strict inequalities
1477  if(expr.id()==ID_notequal)
1478  {
1479  auto new_rel_expr = expr;
1480  new_rel_expr.id(ID_equal);
1481  auto new_expr = simplify_inequality_no_constant(new_rel_expr);
1482  return changed(simplify_not(not_exprt(new_expr)));
1483  }
1484  else if(expr.id()==ID_gt)
1485  {
1486  auto new_rel_expr = expr;
1487  new_rel_expr.id(ID_ge);
1488  // swap operands
1489  new_rel_expr.lhs().swap(new_rel_expr.rhs());
1490  auto new_expr = simplify_inequality_no_constant(new_rel_expr);
1491  return changed(simplify_not(not_exprt(new_expr)));
1492  }
1493  else if(expr.id()==ID_lt)
1494  {
1495  auto new_rel_expr = expr;
1496  new_rel_expr.id(ID_ge);
1497  auto new_expr = simplify_inequality_no_constant(new_rel_expr);
1498  return changed(simplify_not(not_exprt(new_expr)));
1499  }
1500  else if(expr.id()==ID_le)
1501  {
1502  auto new_rel_expr = expr;
1503  new_rel_expr.id(ID_ge);
1504  // swap operands
1505  new_rel_expr.lhs().swap(new_rel_expr.rhs());
1506  return changed(simplify_inequality_no_constant(new_rel_expr));
1507  }
1508 
1509  // now we only have >=, =
1510 
1511  INVARIANT(
1512  expr.id() == ID_ge || expr.id() == ID_equal,
1513  "we previously converted all other cases to >= or ==");
1514 
1515  // syntactically equal?
1516 
1517  if(expr.op0() == expr.op1())
1518  return true_exprt();
1519 
1520  // See if we can eliminate common addends on both sides.
1521  // On bit-vectors, this is only sound on '='.
1522  if(expr.id()==ID_equal)
1523  {
1524  auto new_expr = to_equal_expr(expr);
1525  if(!eliminate_common_addends(new_expr.lhs(), new_expr.rhs()))
1526  {
1527  // remove zeros
1528  new_expr.lhs() = simplify_node(new_expr.lhs());
1529  new_expr.rhs() = simplify_node(new_expr.rhs());
1530  return changed(simplify_inequality(new_expr)); // recursive call
1531  }
1532  }
1533 
1534  return unchanged(expr);
1535 }
1536 
1540  const binary_relation_exprt &expr)
1541 {
1542  // the constant is always on the RHS
1543  PRECONDITION(expr.op1().is_constant());
1544 
1545  if(expr.op0().id()==ID_if && expr.op0().operands().size()==3)
1546  {
1547  if_exprt if_expr=lift_if(expr, 0);
1548  if_expr.true_case() =
1550  if_expr.false_case() =
1552  return changed(simplify_if(if_expr));
1553  }
1554 
1555  // do we deal with pointers?
1556  if(expr.op1().type().id()==ID_pointer)
1557  {
1558  if(expr.id()==ID_notequal)
1559  {
1560  auto new_rel_expr = expr;
1561  new_rel_expr.id(ID_equal);
1562  auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
1563  return changed(simplify_not(not_exprt(new_expr)));
1564  }
1565 
1566  // very special case for pointers
1567  if(expr.id()==ID_equal &&
1568  expr.op1().is_constant() &&
1569  expr.op1().get(ID_value)==ID_NULL)
1570  {
1571  // the address of an object is never NULL
1572 
1573  if(expr.op0().id() == ID_address_of)
1574  {
1575  const auto &object = to_address_of_expr(expr.op0()).object();
1576 
1577  if(
1578  object.id() == ID_symbol || object.id() == ID_dynamic_object ||
1579  object.id() == ID_member || object.id() == ID_index ||
1580  object.id() == ID_string_constant)
1581  {
1582  return false_exprt();
1583  }
1584  }
1585  else if(
1586  expr.op0().id() == ID_typecast &&
1587  expr.op0().type().id() == ID_pointer &&
1588  to_typecast_expr(expr.op0()).op().id() == ID_address_of)
1589  {
1590  const auto &object =
1592 
1593  if(
1594  object.id() == ID_symbol || object.id() == ID_dynamic_object ||
1595  object.id() == ID_member || object.id() == ID_index ||
1596  object.id() == ID_string_constant)
1597  {
1598  return false_exprt();
1599  }
1600  }
1601  else if(
1602  expr.op0().id() == ID_typecast && expr.op0().type().id() == ID_pointer)
1603  {
1604  exprt op = to_typecast_expr(expr.op0()).op();
1605  if(
1606  op.type().id() != ID_pointer &&
1607  (!config.ansi_c.NULL_is_zero || !is_number(op.type()) ||
1608  op.type().id() == ID_complex))
1609  {
1610  return unchanged(expr);
1611  }
1612 
1613  // (type)ptr == NULL -> ptr == NULL
1614  // note that 'ptr' may be an integer
1615  auto new_expr = expr;
1616  new_expr.op0().swap(op);
1617  if(new_expr.op0().type().id() != ID_pointer)
1618  new_expr.op1() = from_integer(0, new_expr.op0().type());
1619  else
1620  new_expr.op1().type() = new_expr.op0().type();
1621  return changed(simplify_inequality(new_expr)); // do again!
1622  }
1623  }
1624 
1625  // all we are doing with pointers
1626  return unchanged(expr);
1627  }
1628 
1629  // is it a separation predicate?
1630 
1631  if(expr.op0().id()==ID_plus)
1632  {
1633  // see if there is a constant in the sum
1634 
1635  if(expr.id()==ID_equal || expr.id()==ID_notequal)
1636  {
1637  mp_integer constant=0;
1638  bool op_changed = false;
1639  auto new_expr = expr;
1640 
1641  Forall_operands(it, new_expr.op0())
1642  {
1643  if(it->is_constant())
1644  {
1645  mp_integer i;
1646  if(!to_integer(to_constant_expr(*it), i))
1647  {
1648  constant+=i;
1649  *it=from_integer(0, it->type());
1650  op_changed = true;
1651  }
1652  }
1653  }
1654 
1655  if(op_changed)
1656  {
1657  // adjust the constant on the RHS
1658  mp_integer i =
1659  numeric_cast_v<mp_integer>(to_constant_expr(new_expr.op1()));
1660  i-=constant;
1661  new_expr.op1() = from_integer(i, new_expr.op1().type());
1662 
1663  new_expr.op0() = simplify_plus(to_plus_expr(new_expr.op0()));
1664  return changed(simplify_inequality(new_expr));
1665  }
1666  }
1667  }
1668 
1669  #if 1
1670  // (double)value REL const ---> value rel const
1671  // if 'const' can be represented exactly.
1672 
1673  if(
1674  expr.op0().id() == ID_typecast && expr.op0().type().id() == ID_floatbv &&
1675  to_typecast_expr(expr.op0()).op().type().id() == ID_floatbv)
1676  {
1677  ieee_floatt const_val(to_constant_expr(expr.op1()));
1678  ieee_floatt const_val_converted=const_val;
1679  const_val_converted.change_spec(ieee_float_spect(
1680  to_floatbv_type(to_typecast_expr(expr.op0()).op().type())));
1681  ieee_floatt const_val_converted_back=const_val_converted;
1682  const_val_converted_back.change_spec(
1684  if(const_val_converted_back==const_val)
1685  {
1686  auto result = expr;
1687  result.op0() = to_typecast_expr(expr.op0()).op();
1688  result.op1()=const_val_converted.to_expr();
1689  return std::move(result);
1690  }
1691  }
1692  #endif
1693 
1694  // is the constant zero?
1695 
1696  if(expr.op1().is_zero())
1697  {
1698  if(expr.id()==ID_ge &&
1699  expr.op0().type().id()==ID_unsignedbv)
1700  {
1701  // zero is always smaller or equal something unsigned
1702  return true_exprt();
1703  }
1704 
1705  auto new_expr = expr;
1706  exprt &operand = new_expr.op0();
1707 
1708  if(expr.id()==ID_equal)
1709  {
1710  // rules below do not hold for >=
1711  if(operand.id()==ID_unary_minus)
1712  {
1713  operand = to_unary_minus_expr(operand).op();
1714  return std::move(new_expr);
1715  }
1716  else if(operand.id()==ID_plus)
1717  {
1718  auto &operand_plus_expr = to_plus_expr(operand);
1719 
1720  // simplify a+-b=0 to a=b
1721  if(operand_plus_expr.operands().size() == 2)
1722  {
1723  // if we have -b+a=0, make that a+(-b)=0
1724  if(operand_plus_expr.op0().id() == ID_unary_minus)
1725  operand_plus_expr.op0().swap(operand_plus_expr.op1());
1726 
1727  if(operand_plus_expr.op1().id() == ID_unary_minus)
1728  {
1729  return binary_exprt(
1730  operand_plus_expr.op0(),
1731  expr.id(),
1732  to_unary_minus_expr(operand_plus_expr.op1()).op(),
1733  expr.type());
1734  }
1735  }
1736  }
1737  }
1738  }
1739 
1740  // are we comparing with a typecast from bool?
1741  if(
1742  expr.op0().id() == ID_typecast &&
1743  to_typecast_expr(expr.op0()).op().type().id() == ID_bool)
1744  {
1745  const auto &lhs_typecast_op = to_typecast_expr(expr.op0()).op();
1746 
1747  // we re-write (TYPE)boolean == 0 -> !boolean
1748  if(expr.op1().is_zero() && expr.id()==ID_equal)
1749  {
1750  return changed(simplify_not(not_exprt(lhs_typecast_op)));
1751  }
1752 
1753  // we re-write (TYPE)boolean != 0 -> boolean
1754  if(expr.op1().is_zero() && expr.id()==ID_notequal)
1755  {
1756  return lhs_typecast_op;
1757  }
1758  }
1759 
1760  #define NORMALISE_CONSTANT_TESTS
1761  #ifdef NORMALISE_CONSTANT_TESTS
1762  // Normalise to >= and = to improve caching and term sharing
1763  if(expr.op0().type().id()==ID_unsignedbv ||
1764  expr.op0().type().id()==ID_signedbv)
1765  {
1767 
1768  if(expr.id()==ID_notequal)
1769  {
1770  auto new_rel_expr = expr;
1771  new_rel_expr.id(ID_equal);
1772  auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
1773  return changed(simplify_not(not_exprt(new_expr)));
1774  }
1775  else if(expr.id()==ID_gt)
1776  {
1777  mp_integer i = numeric_cast_v<mp_integer>(to_constant_expr(expr.op1()));
1778 
1779  if(i==max)
1780  {
1781  return false_exprt();
1782  }
1783 
1784  auto new_expr = expr;
1785  new_expr.id(ID_ge);
1786  ++i;
1787  new_expr.op1() = from_integer(i, new_expr.op1().type());
1788  return changed(simplify_inequality_rhs_is_constant(new_expr));
1789  }
1790  else if(expr.id()==ID_lt)
1791  {
1792  auto new_rel_expr = expr;
1793  new_rel_expr.id(ID_ge);
1794  auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
1795  return changed(simplify_not(not_exprt(new_expr)));
1796  }
1797  else if(expr.id()==ID_le)
1798  {
1799  mp_integer i = numeric_cast_v<mp_integer>(to_constant_expr(expr.op1()));
1800 
1801  if(i==max)
1802  {
1803  return true_exprt();
1804  }
1805 
1806  auto new_rel_expr = expr;
1807  new_rel_expr.id(ID_ge);
1808  ++i;
1809  new_rel_expr.op1() = from_integer(i, new_rel_expr.op1().type());
1810  auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
1811  return changed(simplify_not(not_exprt(new_expr)));
1812  }
1813  }
1814 #endif
1815  return unchanged(expr);
1816 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
ieee_floatt
Definition: ieee_float.h:117
Forall_expr
#define Forall_expr(it, expr)
Definition: expr.h:34
configt::ansi_ct::NULL_is_zero
bool NULL_is_zero
Definition: config.h:167
multi_ary_exprt
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:824
simplify_exprt::simplify_shifts
resultt simplify_shifts(const shift_exprt &)
Definition: simplify_expr_int.cpp:907
rationalt::is_zero
bool is_zero() const
Definition: rational.h:74
extractbits_exprt::lower
exprt & lower()
Definition: bitvector_expr.h:461
skip_typecast
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:215
simplify_exprt::simplify_concatenation
resultt simplify_concatenation(const concatenation_exprt &)
Definition: simplify_expr_int.cpp:805
mp_integer
BigInt mp_integer
Definition: smt_terms.h:12
simplify_expr_class.h
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
arith_tools.h
is_number
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
Definition: mathematical_types.cpp:17
make_bvrep
irep_idt make_bvrep(const std::size_t width, const std::function< bool(std::size_t)> f)
construct a bit-vector representation from a functor
Definition: arith_tools.cpp:305
rational.h
simplify_exprt::simplify_unary_plus
resultt simplify_unary_plus(const unary_plus_exprt &)
Definition: simplify_expr_int.cpp:1112
simplify_exprt::simplify_bitwise
resultt simplify_bitwise(const multi_ary_exprt &)
Definition: simplify_expr_int.cpp:600
rational_tools.h
address_of_exprt::object
exprt & object()
Definition: pointer_expr.h:350
simplify_exprt::simplify_bitnot
resultt simplify_bitnot(const bitnot_exprt &)
Definition: simplify_expr_int.cpp:1179
typet
The type of an expression, extends irept.
Definition: type.h:28
fixedbvt::negate
void negate()
Definition: fixedbv.cpp:90
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: bitvector_types.h:367
bits2expr
optionalt< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
Definition: simplify_utils.cpp:193
to_integer_bitvector_type
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
Definition: bitvector_types.h:142
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2172
simplify_exprt::simplify_inequality_address_of
resultt simplify_inequality_address_of(const binary_relation_exprt &)
Definition: simplify_expr_pointer.cpp:410
to_rational
bool to_rational(const exprt &expr, rationalt &rational_value)
Definition: rational_tools.cpp:27
fixedbv.h
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:914
ieee_floatt::change_spec
void change_spec(const ieee_float_spect &dest_spec)
Definition: ieee_float.cpp:1048
simplify_exprt::simplify_boolean
resultt simplify_boolean(const exprt &)
Definition: simplify_expr_boolean.cpp:17
exprt
Base class for all expressions.
Definition: expr.h:54
simplify_exprt::simplify_extractbit
resultt simplify_extractbit(const extractbit_exprt &)
Definition: simplify_expr_int.cpp:776
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:550
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
bswap_exprt::get_bits_per_byte
std::size_t get_bits_per_byte() const
Definition: bitvector_expr.h:33
exprt::op0
exprt & op0()
Definition: expr.h:99
to_integer
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
bool_typet
The Boolean type.
Definition: std_types.h:36
concatenation_exprt
Concatenation of bit-vector operands.
Definition: bitvector_expr.h:590
lift_if
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:199
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
configt::ansi_c
struct configt::ansi_ct ansi_c
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: bitvector_types.h:32
div_exprt
Division.
Definition: std_expr.h:1064
shift_exprt::op
exprt & op()
Definition: bitvector_expr.h:239
simplify_exprt::simplify_plus
resultt simplify_plus(const plus_exprt &)
Definition: simplify_expr_int.cpp:402
namespace.h
from_rational
constant_exprt from_rational(const rationalt &a)
Definition: rational_tools.cpp:81
fixedbvt::to_expr
constant_exprt to_expr() const
Definition: fixedbv.cpp:43
simplify_exprt::simplify_not
resultt simplify_not(const not_exprt &)
Definition: simplify_expr_boolean.cpp:162
to_minus_expr
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:998
simplify_exprt::simplify_inequality_both_constant
resultt simplify_inequality_both_constant(const binary_relation_exprt &)
simplifies inequalities for the case in which both sides of the inequality are constants
Definition: simplify_expr_int.cpp:1306
simplify_exprt::unchanged
static resultt unchanged(exprt expr)
Definition: simplify_expr_class.h:130
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:2209
simplify_exprt::simplify_node
resultt simplify_node(exprt)
Definition: simplify_expr.cpp:2314
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: bitvector_types.h:159
extractbits_exprt::upper
exprt & upper()
Definition: bitvector_expr.h:456
ieee_float_spect
Definition: ieee_float.h:23
simplify_exprt::simplify_if
resultt simplify_if(const if_exprt &)
Definition: simplify_expr_if.cpp:330
mathematical_types.h
Mathematical types.
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
simplify_exprt::simplify_minus
resultt simplify_minus(const minus_exprt &)
Definition: simplify_expr_int.cpp:558
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
simplify_exprt::simplify_power
resultt simplify_power(const binary_exprt &)
Definition: simplify_expr_int.cpp:1015
simplify_exprt::simplify_div
resultt simplify_div(const div_exprt &)
Definition: simplify_expr_int.cpp:271
dstringt::swap
void swap(dstringt &b)
Definition: dstring.h:145
simplify_exprt::simplify_inequality_no_constant
resultt simplify_inequality_no_constant(const binary_relation_exprt &)
Definition: simplify_expr_int.cpp:1467
simplify_exprt::simplify_typecast
resultt simplify_typecast(const typecast_exprt &)
Definition: simplify_expr.cpp:732
integer2bvrep
irep_idt integer2bvrep(const mp_integer &src, std::size_t width)
convert an integer to bit-vector representation with given width This uses two's complement for negat...
Definition: arith_tools.cpp:379
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
simplify_exprt::simplify_mod
resultt simplify_mod(const mod_exprt &)
Definition: simplify_expr_int.cpp:365
to_c_enum_tag_type
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: c_types.h:317
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
multi_ary_exprt::op1
exprt & op1()
Definition: std_expr.h:850
simplify_exprt::changed
static resultt changed(resultt<> result)
Definition: simplify_expr_class.h:135
simplify_exprt::is_bitvector_type
static bool is_bitvector_type(const typet &type)
Definition: simplify_expr_class.h:240
eliminate_common_addends
static bool eliminate_common_addends(exprt &op0, exprt &op1)
Definition: simplify_expr_int.cpp:1421
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:101
simplify_exprt::simplify_inequality_rhs_is_constant
resultt simplify_inequality_rhs_is_constant(const binary_relation_exprt &)
Definition: simplify_expr_int.cpp:1539
simplify_exprt::simplify_bswap
resultt simplify_bswap(const bswap_exprt &)
Definition: simplify_expr_int.cpp:29
to_plus_expr
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:953
pointer_expr.h
API to expression classes for Pointers.
extractbits_exprt::src
exprt & src()
Definition: bitvector_expr.h:451
exprt::op1
exprt & op1()
Definition: expr.h:102
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1019
simplify_exprt::simplify_inequality
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
Definition: simplify_expr_int.cpp:1210
to_unary_minus_expr
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:420
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:390
irept::swap
void swap(irept &irep)
Definition: irep.h:453
extractbit_exprt::index
exprt & index()
Definition: bitvector_expr.h:378
irept::id
const irep_idt & id() const
Definition: irep.h:407
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
false_exprt
The Boolean constant false.
Definition: std_expr.h:2811
unary_plus_exprt
The unary plus expression.
Definition: std_expr.h:439
simplify_exprt::simplify_mult
resultt simplify_mult(const mult_exprt &)
Definition: simplify_expr_int.cpp:159
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
simplify_exprt::resultt
Definition: simplify_expr_class.h:97
ieee_floatt::negate
void negate()
Definition: ieee_float.h:179
simplify_exprt::simplify_unary_minus
resultt simplify_unary_minus(const unary_minus_exprt &)
Definition: simplify_expr_int.cpp:1119
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
bitvector_typet::set_width
void set_width(std::size_t width)
Definition: std_types.h:848
minus_exprt
Binary minus.
Definition: std_expr.h:973
config
configt config
Definition: config.cpp:25
expr2bits
optionalt< std::string > expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
Definition: simplify_utils.cpp:405
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:843
bitnot_exprt
Bit-wise negation of bit-vectors.
Definition: bitvector_expr.h:82
mul_expr
static bool mul_expr(constant_exprt &dest, const constant_exprt &expr)
produce a product of two expressions of the same type
Definition: simplify_expr_int.cpp:112
extractbit_exprt
Extracts a single bit of a bit-vector operand.
Definition: bitvector_expr.h:363
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
expr_util.h
Deprecated expression utility functions.
bvrep2integer
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
Definition: arith_tools.cpp:401
irept::get_string
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:420
shift_exprt
A base class for shift and rotate operators.
Definition: bitvector_expr.h:230
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2199
simplify_exprt::simplify_inequality_pointer_object
resultt simplify_inequality_pointer_object(const binary_relation_exprt &)
Definition: simplify_expr_pointer.cpp:475
shift_exprt::distance
exprt & distance()
Definition: bitvector_expr.h:249
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
constant_exprt::value_is_zero_string
bool value_is_zero_string() const
Definition: std_expr.cpp:16
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
extractbit_exprt::src
exprt & src()
Definition: bitvector_expr.h:373
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900
ieee_float.h
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
invariant.h
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:194
to_equal_expr
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1265
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
config.h
integer_bitvector_typet::largest
mp_integer largest() const
Return the largest value that can be represented using this type.
Definition: bitvector_types.cpp:38
fixedbvt
Definition: fixedbv.h:42
simplify_exprt::simplify_extractbits
resultt simplify_extractbits(const extractbits_exprt &)
Simplifies extracting of bits from a constant.
Definition: simplify_expr_int.cpp:1036
exprt::is_one
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:114
simplify_exprt::ns
const namespacet & ns
Definition: simplify_expr_class.h:248
sum_expr
static bool sum_expr(constant_exprt &dest, const constant_exprt &expr)
produce a sum of two constant expressions of the same type
Definition: simplify_expr_int.cpp:63
bswap_exprt
The byte swap expression.
Definition: bitvector_expr.h:19
ieee_floatt::to_expr
constant_exprt to_expr() const
Definition: ieee_float.cpp:702
make_boolean_expr
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Definition: expr_util.cpp:281
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:378
extractbits_exprt
Extracts a sub-range of a bit-vector operand.
Definition: bitvector_expr.h:430
exprt::operands
operandst & operands()
Definition: expr.h:92
r
static int8_t r
Definition: irep_hash.h:60
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1866
true_exprt
The Boolean constant true.
Definition: std_expr.h:2802
constant_exprt
A constant literal expression.
Definition: std_expr.h:2753
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:844
binary_exprt::op1
exprt & op1()
Definition: expr.h:102
simplify_utils.h
expr_mapt
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
Definition: acceleration_utils.h:31
std_expr.h
API to expression classes.
to_binary_relation_expr
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:807
constant_exprt::set_value
void set_value(const irep_idt &value)
Definition: std_expr.h:2766
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2761
c_types.h
rationalt
Definition: rational.h:16
bitvector_expr.h
API to expression classes for bitvectors.
binary_exprt::op0
exprt & op0()
Definition: expr.h:99
fixedbvt::is_zero
bool is_zero() const
Definition: fixedbv.h:71
mod_exprt
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1135
get_bvrep_bit
bool get_bvrep_bit(const irep_idt &src, std::size_t width, std::size_t bit_index)
Get a bit with given index from bit-vector representation.
Definition: arith_tools.cpp:261
rationalt::is_one
bool is_one() const
Definition: rational.h:77
not_exprt
Boolean negation.
Definition: std_expr.h:2127
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2786