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  // simplifications below require same-object, which we don't check for
1477  if(
1478  expr.op0().type().id() == ID_pointer && expr.id() != ID_equal &&
1479  expr.id() != ID_notequal)
1480  {
1481  return unchanged(expr);
1482  }
1483 
1484  // eliminate strict inequalities
1485  if(expr.id()==ID_notequal)
1486  {
1487  auto new_rel_expr = expr;
1488  new_rel_expr.id(ID_equal);
1489  auto new_expr = simplify_inequality_no_constant(new_rel_expr);
1490  return changed(simplify_not(not_exprt(new_expr)));
1491  }
1492  else if(expr.id()==ID_gt)
1493  {
1494  auto new_rel_expr = expr;
1495  new_rel_expr.id(ID_ge);
1496  // swap operands
1497  new_rel_expr.lhs().swap(new_rel_expr.rhs());
1498  auto new_expr = simplify_inequality_no_constant(new_rel_expr);
1499  return changed(simplify_not(not_exprt(new_expr)));
1500  }
1501  else if(expr.id()==ID_lt)
1502  {
1503  auto new_rel_expr = expr;
1504  new_rel_expr.id(ID_ge);
1505  auto new_expr = simplify_inequality_no_constant(new_rel_expr);
1506  return changed(simplify_not(not_exprt(new_expr)));
1507  }
1508  else if(expr.id()==ID_le)
1509  {
1510  auto new_rel_expr = expr;
1511  new_rel_expr.id(ID_ge);
1512  // swap operands
1513  new_rel_expr.lhs().swap(new_rel_expr.rhs());
1514  return changed(simplify_inequality_no_constant(new_rel_expr));
1515  }
1516 
1517  // now we only have >=, =
1518 
1519  INVARIANT(
1520  expr.id() == ID_ge || expr.id() == ID_equal,
1521  "we previously converted all other cases to >= or ==");
1522 
1523  // syntactically equal?
1524 
1525  if(expr.op0() == expr.op1())
1526  return true_exprt();
1527 
1528  // See if we can eliminate common addends on both sides.
1529  // On bit-vectors, this is only sound on '='.
1530  if(expr.id()==ID_equal)
1531  {
1532  auto new_expr = to_equal_expr(expr);
1533  if(!eliminate_common_addends(new_expr.lhs(), new_expr.rhs()))
1534  {
1535  // remove zeros
1536  new_expr.lhs() = simplify_node(new_expr.lhs());
1537  new_expr.rhs() = simplify_node(new_expr.rhs());
1538  return changed(simplify_inequality(new_expr)); // recursive call
1539  }
1540  }
1541 
1542  return unchanged(expr);
1543 }
1544 
1548  const binary_relation_exprt &expr)
1549 {
1550  // the constant is always on the RHS
1551  PRECONDITION(expr.op1().is_constant());
1552 
1553  if(expr.op0().id()==ID_if && expr.op0().operands().size()==3)
1554  {
1555  if_exprt if_expr=lift_if(expr, 0);
1556  if_expr.true_case() =
1558  if_expr.false_case() =
1560  return changed(simplify_if(if_expr));
1561  }
1562 
1563  // do we deal with pointers?
1564  if(expr.op1().type().id()==ID_pointer)
1565  {
1566  if(expr.id()==ID_notequal)
1567  {
1568  auto new_rel_expr = expr;
1569  new_rel_expr.id(ID_equal);
1570  auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
1571  return changed(simplify_not(not_exprt(new_expr)));
1572  }
1573 
1574  // very special case for pointers
1575  if(expr.id()==ID_equal &&
1576  expr.op1().is_constant() &&
1577  expr.op1().get(ID_value)==ID_NULL)
1578  {
1579  // the address of an object is never NULL
1580 
1581  if(expr.op0().id() == ID_address_of)
1582  {
1583  const auto &object = to_address_of_expr(expr.op0()).object();
1584 
1585  if(
1586  object.id() == ID_symbol || object.id() == ID_dynamic_object ||
1587  object.id() == ID_member || object.id() == ID_index ||
1588  object.id() == ID_string_constant)
1589  {
1590  return false_exprt();
1591  }
1592  }
1593  else if(
1594  expr.op0().id() == ID_typecast &&
1595  expr.op0().type().id() == ID_pointer &&
1596  to_typecast_expr(expr.op0()).op().id() == ID_address_of)
1597  {
1598  const auto &object =
1600 
1601  if(
1602  object.id() == ID_symbol || object.id() == ID_dynamic_object ||
1603  object.id() == ID_member || object.id() == ID_index ||
1604  object.id() == ID_string_constant)
1605  {
1606  return false_exprt();
1607  }
1608  }
1609  else if(
1610  expr.op0().id() == ID_typecast && expr.op0().type().id() == ID_pointer)
1611  {
1612  exprt op = to_typecast_expr(expr.op0()).op();
1613  if(
1614  op.type().id() != ID_pointer &&
1615  (!config.ansi_c.NULL_is_zero || !is_number(op.type()) ||
1616  op.type().id() == ID_complex))
1617  {
1618  return unchanged(expr);
1619  }
1620 
1621  // (type)ptr == NULL -> ptr == NULL
1622  // note that 'ptr' may be an integer
1623  auto new_expr = expr;
1624  new_expr.op0().swap(op);
1625  if(new_expr.op0().type().id() != ID_pointer)
1626  new_expr.op1() = from_integer(0, new_expr.op0().type());
1627  else
1628  new_expr.op1().type() = new_expr.op0().type();
1629  return changed(simplify_inequality(new_expr)); // do again!
1630  }
1631  }
1632 
1633  // all we are doing with pointers
1634  return unchanged(expr);
1635  }
1636 
1637  // is it a separation predicate?
1638 
1639  if(expr.op0().id()==ID_plus)
1640  {
1641  // see if there is a constant in the sum
1642 
1643  if(expr.id()==ID_equal || expr.id()==ID_notequal)
1644  {
1645  mp_integer constant=0;
1646  bool op_changed = false;
1647  auto new_expr = expr;
1648 
1649  Forall_operands(it, new_expr.op0())
1650  {
1651  if(it->is_constant())
1652  {
1653  mp_integer i;
1654  if(!to_integer(to_constant_expr(*it), i))
1655  {
1656  constant+=i;
1657  *it=from_integer(0, it->type());
1658  op_changed = true;
1659  }
1660  }
1661  }
1662 
1663  if(op_changed)
1664  {
1665  // adjust the constant on the RHS
1666  mp_integer i =
1667  numeric_cast_v<mp_integer>(to_constant_expr(new_expr.op1()));
1668  i-=constant;
1669  new_expr.op1() = from_integer(i, new_expr.op1().type());
1670 
1671  new_expr.op0() = simplify_plus(to_plus_expr(new_expr.op0()));
1672  return changed(simplify_inequality(new_expr));
1673  }
1674  }
1675  }
1676 
1677  #if 1
1678  // (double)value REL const ---> value rel const
1679  // if 'const' can be represented exactly.
1680 
1681  if(
1682  expr.op0().id() == ID_typecast && expr.op0().type().id() == ID_floatbv &&
1683  to_typecast_expr(expr.op0()).op().type().id() == ID_floatbv)
1684  {
1685  ieee_floatt const_val(to_constant_expr(expr.op1()));
1686  ieee_floatt const_val_converted=const_val;
1687  const_val_converted.change_spec(ieee_float_spect(
1688  to_floatbv_type(to_typecast_expr(expr.op0()).op().type())));
1689  ieee_floatt const_val_converted_back=const_val_converted;
1690  const_val_converted_back.change_spec(
1692  if(const_val_converted_back==const_val)
1693  {
1694  auto result = expr;
1695  result.op0() = to_typecast_expr(expr.op0()).op();
1696  result.op1()=const_val_converted.to_expr();
1697  return std::move(result);
1698  }
1699  }
1700  #endif
1701 
1702  // is the constant zero?
1703 
1704  if(expr.op1().is_zero())
1705  {
1706  if(expr.id()==ID_ge &&
1707  expr.op0().type().id()==ID_unsignedbv)
1708  {
1709  // zero is always smaller or equal something unsigned
1710  return true_exprt();
1711  }
1712 
1713  auto new_expr = expr;
1714  exprt &operand = new_expr.op0();
1715 
1716  if(expr.id()==ID_equal)
1717  {
1718  // rules below do not hold for >=
1719  if(operand.id()==ID_unary_minus)
1720  {
1721  operand = to_unary_minus_expr(operand).op();
1722  return std::move(new_expr);
1723  }
1724  else if(operand.id()==ID_plus)
1725  {
1726  auto &operand_plus_expr = to_plus_expr(operand);
1727 
1728  // simplify a+-b=0 to a=b
1729  if(operand_plus_expr.operands().size() == 2)
1730  {
1731  // if we have -b+a=0, make that a+(-b)=0
1732  if(operand_plus_expr.op0().id() == ID_unary_minus)
1733  operand_plus_expr.op0().swap(operand_plus_expr.op1());
1734 
1735  if(operand_plus_expr.op1().id() == ID_unary_minus)
1736  {
1737  return binary_exprt(
1738  operand_plus_expr.op0(),
1739  expr.id(),
1740  to_unary_minus_expr(operand_plus_expr.op1()).op(),
1741  expr.type());
1742  }
1743  }
1744  }
1745  }
1746  }
1747 
1748  // are we comparing with a typecast from bool?
1749  if(
1750  expr.op0().id() == ID_typecast &&
1751  to_typecast_expr(expr.op0()).op().type().id() == ID_bool)
1752  {
1753  const auto &lhs_typecast_op = to_typecast_expr(expr.op0()).op();
1754 
1755  // we re-write (TYPE)boolean == 0 -> !boolean
1756  if(expr.op1().is_zero() && expr.id()==ID_equal)
1757  {
1758  return changed(simplify_not(not_exprt(lhs_typecast_op)));
1759  }
1760 
1761  // we re-write (TYPE)boolean != 0 -> boolean
1762  if(expr.op1().is_zero() && expr.id()==ID_notequal)
1763  {
1764  return lhs_typecast_op;
1765  }
1766  }
1767 
1768  #define NORMALISE_CONSTANT_TESTS
1769  #ifdef NORMALISE_CONSTANT_TESTS
1770  // Normalise to >= and = to improve caching and term sharing
1771  if(expr.op0().type().id()==ID_unsignedbv ||
1772  expr.op0().type().id()==ID_signedbv)
1773  {
1775 
1776  if(expr.id()==ID_notequal)
1777  {
1778  auto new_rel_expr = expr;
1779  new_rel_expr.id(ID_equal);
1780  auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
1781  return changed(simplify_not(not_exprt(new_expr)));
1782  }
1783  else if(expr.id()==ID_gt)
1784  {
1785  mp_integer i = numeric_cast_v<mp_integer>(to_constant_expr(expr.op1()));
1786 
1787  if(i==max)
1788  {
1789  return false_exprt();
1790  }
1791 
1792  auto new_expr = expr;
1793  new_expr.id(ID_ge);
1794  ++i;
1795  new_expr.op1() = from_integer(i, new_expr.op1().type());
1796  return changed(simplify_inequality_rhs_is_constant(new_expr));
1797  }
1798  else if(expr.id()==ID_lt)
1799  {
1800  auto new_rel_expr = expr;
1801  new_rel_expr.id(ID_ge);
1802  auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
1803  return changed(simplify_not(not_exprt(new_expr)));
1804  }
1805  else if(expr.id()==ID_le)
1806  {
1807  mp_integer i = numeric_cast_v<mp_integer>(to_constant_expr(expr.op1()));
1808 
1809  if(i==max)
1810  {
1811  return true_exprt();
1812  }
1813 
1814  auto new_rel_expr = expr;
1815  new_rel_expr.id(ID_ge);
1816  ++i;
1817  new_rel_expr.op1() = from_integer(i, new_rel_expr.op1().type());
1818  auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
1819  return changed(simplify_not(not_exprt(new_expr)));
1820  }
1821  }
1822 #endif
1823  return unchanged(expr);
1824 }
1825 
1828 {
1829  auto const_bits_opt = expr2bits(
1830  expr.op(),
1832  ns);
1833 
1834  if(!const_bits_opt.has_value())
1835  return unchanged(expr);
1836 
1837  std::reverse(const_bits_opt->begin(), const_bits_opt->end());
1838 
1839  auto result = bits2expr(
1840  *const_bits_opt,
1841  expr.type(),
1843  ns);
1844  if(!result.has_value())
1845  return unchanged(expr);
1846 
1847  return std::move(*result);
1848 }
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.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
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:344
exprt & object()
Definition: pointer_expr.h:370
A base class for binary expressions.
Definition: std_expr.h:550
exprt & op1()
Definition: expr.h:102
exprt & op0()
Definition: expr.h:99
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
Bit-wise negation of bit-vectors.
Reverse the order of bits in a bit-vector.
void set_width(std::size_t width)
Definition: std_types.h:869
std::size_t get_width() const
Definition: std_types.h:864
The Boolean type.
Definition: std_types.h:36
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:2807
const irep_idt & get_value() const
Definition: std_expr.h:2815
bool value_is_zero_string() const
Definition: std_expr.cpp:16
void set_value(const irep_idt &value)
Definition: std_expr.h:2820
Division.
Definition: std_expr.h:1064
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:114
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
exprt & op1()
Definition: expr.h:102
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
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:26
exprt & op0()
Definition: expr.h:99
operandst & operands()
Definition: expr.h:92
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
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:2865
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:702
void negate()
Definition: ieee_float.h:179
void change_spec(const ieee_float_spect &dest_spec)
The trinary if-then-else operator.
Definition: std_expr.h:2226
exprt & true_case()
Definition: std_expr.h:2253
exprt & false_case()
Definition: std_expr.h:2263
mp_integer largest() const
Return the largest value that can be represented using this type.
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
bool is_not_nil() const
Definition: irep.h:380
const irep_idt & id() const
Definition: irep.h:396
void swap(irept &irep)
Definition: irep.h:442
const std::string & get_string(const irep_idt &name) const
Definition: irep.h:409
Binary minus.
Definition: std_expr.h:973
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1135
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1019
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:824
exprt & op1()
Definition: std_expr.h:850
exprt & op0()
Definition: std_expr.h:844
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
Boolean negation.
Definition: std_expr.h:2181
The plus expression Associativity is not specified.
Definition: std_expr.h:914
bool is_one() const
Definition: rational.h:77
bool is_zero() const
Definition: rational.h:74
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_bitreverse(const bitreverse_exprt &)
Try to simplify bit-reversing to a constant expression.
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_typecast(const typecast_exprt &)
resultt simplify_boolean(const 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:2856
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:293
The unary minus expression.
Definition: std_expr.h:390
The unary plus expression.
Definition: std_expr.h:439
Fixed-width bit-vector with unsigned binary interpretation.
configt config
Definition: config.cpp:25
#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:283
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:216
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:200
Deprecated expression utility functions.
static int8_t r
Definition: irep_hash.h:60
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
Mathematical types.
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:398
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)
BigInt mp_integer
Definition: smt_terms.h:12
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:420
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:998
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1265
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:953
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:807
endiannesst endianness
Definition: config.h:177
bool NULL_is_zero
Definition: config.h:194