CBMC
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 #include "threeval.h"
28 
29 #include <algorithm>
30 
33 {
34  if(expr.type().id() == ID_unsignedbv && expr.op().is_constant())
35  {
36  auto bits_per_byte = expr.get_bits_per_byte();
37  std::size_t width=to_bitvector_type(expr.type()).get_width();
38  const mp_integer value =
39  numeric_cast_v<mp_integer>(to_constant_expr(expr.op()));
40  std::vector<mp_integer> bytes;
41 
42  // take apart
43  for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
44  bytes.push_back((value >> bit)%power(2, bits_per_byte));
45 
46  // put back together, but backwards
47  mp_integer new_value=0;
48  for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
49  {
50  INVARIANT(
51  !bytes.empty(),
52  "bytes is not empty because we just pushed just as many elements on "
53  "top of it as we are popping now");
54  new_value+=bytes.back()<<bit;
55  bytes.pop_back();
56  }
57 
58  return from_integer(new_value, expr.type());
59  }
60 
61  return unchanged(expr);
62 }
63 
66 static bool sum_expr(
67  constant_exprt &dest,
68  const constant_exprt &expr)
69 {
70  if(dest.type()!=expr.type())
71  return true;
72 
73  const irep_idt &type_id=dest.type().id();
74 
75  if(
76  type_id == ID_integer || type_id == ID_natural ||
77  type_id == ID_unsignedbv || type_id == ID_signedbv)
78  {
79  mp_integer a, b;
80  if(!to_integer(dest, a) && !to_integer(expr, b))
81  {
82  dest = from_integer(a + b, dest.type());
83  return false;
84  }
85  }
86  else if(type_id==ID_rational)
87  {
88  rationalt a, b;
89  if(!to_rational(dest, a) && !to_rational(expr, b))
90  {
91  dest=from_rational(a+b);
92  return false;
93  }
94  }
95  else if(type_id==ID_fixedbv)
96  {
97  fixedbvt f(dest);
98  f += fixedbvt(expr);
99  dest = f.to_expr();
100  return false;
101  }
102  else if(type_id==ID_floatbv)
103  {
104  ieee_floatt f(dest);
105  f += ieee_floatt(expr);
106  dest=f.to_expr();
107  return false;
108  }
109 
110  return true;
111 }
112 
115 static bool mul_expr(
116  constant_exprt &dest,
117  const constant_exprt &expr)
118 {
119  if(dest.type()!=expr.type())
120  return true;
121 
122  const irep_idt &type_id=dest.type().id();
123 
124  if(
125  type_id == ID_integer || type_id == ID_natural ||
126  type_id == ID_unsignedbv || type_id == ID_signedbv)
127  {
128  mp_integer a, b;
129  if(!to_integer(dest, a) && !to_integer(expr, b))
130  {
131  dest = from_integer(a * b, dest.type());
132  return false;
133  }
134  }
135  else if(type_id==ID_rational)
136  {
137  rationalt a, b;
138  if(!to_rational(dest, a) && !to_rational(expr, b))
139  {
140  dest=from_rational(a*b);
141  return false;
142  }
143  }
144  else if(type_id==ID_fixedbv)
145  {
146  fixedbvt f(to_constant_expr(dest));
147  f*=fixedbvt(to_constant_expr(expr));
148  dest=f.to_expr();
149  return false;
150  }
151  else if(type_id==ID_floatbv)
152  {
153  ieee_floatt f(to_constant_expr(dest));
154  f*=ieee_floatt(to_constant_expr(expr));
155  dest=f.to_expr();
156  return false;
157  }
158 
159  return true;
160 }
161 
163 {
164  // check to see if it is a number type
165  if(!is_number(expr.type()))
166  return unchanged(expr);
167 
168  // vector of operands
169  exprt::operandst new_operands = expr.operands();
170 
171  // result of the simplification
172  bool no_change = true;
173 
174  // position of the constant
175  exprt::operandst::iterator constant;
176 
177  // true if we have found a constant
178  bool constant_found = false;
179 
180  std::optional<typet> c_sizeof_type;
181 
182  // scan all the operands
183  for(exprt::operandst::iterator it = new_operands.begin();
184  it != new_operands.end();)
185  {
186  // if one of the operands is not a number return
187  if(!is_number(it->type()))
188  return unchanged(expr);
189 
190  // if one of the operands is zero the result is zero
191  // note: not true on IEEE floating point arithmetic
192  if(it->is_zero() &&
193  it->type().id()!=ID_floatbv)
194  {
195  return from_integer(0, expr.type());
196  }
197 
198  // true if the given operand has to be erased
199  bool do_erase = false;
200 
201  // if this is a constant of the same time as the result
202  if(it->is_constant() && it->type()==expr.type())
203  {
204  // preserve the sizeof type annotation
205  if(!c_sizeof_type.has_value())
206  {
207  const typet &sizeof_type =
208  static_cast<const typet &>(it->find(ID_C_c_sizeof_type));
209  if(sizeof_type.is_not_nil())
210  c_sizeof_type = sizeof_type;
211  }
212 
213  if(constant_found)
214  {
215  // update the constant factor
216  if(!mul_expr(to_constant_expr(*constant), to_constant_expr(*it)))
217  do_erase=true;
218  }
219  else
220  {
221  // set it as the constant factor if this is the first
222  constant=it;
223  constant_found = true;
224  }
225  }
226 
227  // erase the factor if necessary
228  if(do_erase)
229  {
230  it = new_operands.erase(it);
231  no_change = false;
232  }
233  else
234  it++; // move to the next operand
235  }
236 
237  if(c_sizeof_type.has_value())
238  {
239  INVARIANT(
240  constant_found,
241  "c_sizeof_type is only set to a non-nil value "
242  "if a constant has been found");
243  constant->set(ID_C_c_sizeof_type, *c_sizeof_type);
244  }
245 
246  if(new_operands.size() == 1)
247  {
248  return new_operands.front();
249  }
250  else
251  {
252  // if the constant is a one and there are other factors
253  if(constant_found && constant->is_one())
254  {
255  // just delete it
256  new_operands.erase(constant);
257  no_change = false;
258 
259  if(new_operands.size() == 1)
260  return new_operands.front();
261  }
262  }
263 
264  if(no_change)
265  return unchanged(expr);
266  else
267  {
268  exprt tmp = expr;
269  tmp.operands() = std::move(new_operands);
270  return std::move(tmp);
271  }
272 }
273 
275 {
276  if(!is_number(expr.type()))
277  return unchanged(expr);
278 
279  const typet &expr_type=expr.type();
280 
281  if(expr_type!=expr.op0().type() ||
282  expr_type!=expr.op1().type())
283  {
284  return unchanged(expr);
285  }
286 
287  if(expr_type.id()==ID_signedbv ||
288  expr_type.id()==ID_unsignedbv ||
289  expr_type.id()==ID_natural ||
290  expr_type.id()==ID_integer)
291  {
292  const auto int_value0 = numeric_cast<mp_integer>(expr.op0());
293  const auto int_value1 = numeric_cast<mp_integer>(expr.op1());
294 
295  // division by zero?
296  if(int_value1.has_value() && *int_value1 == 0)
297  return unchanged(expr);
298 
299  // x/1?
300  if(int_value1.has_value() && *int_value1 == 1)
301  {
302  return expr.op0();
303  }
304 
305  // 0/x?
306  if(int_value0.has_value() && *int_value0 == 0)
307  {
308  return expr.op0();
309  }
310 
311  if(int_value0.has_value() && int_value1.has_value())
312  {
313  mp_integer result = *int_value0 / *int_value1;
314  return from_integer(result, expr_type);
315  }
316  }
317  else if(expr_type.id()==ID_rational)
318  {
319  rationalt rat_value0, rat_value1;
320  bool ok0, ok1;
321 
322  ok0=!to_rational(expr.op0(), rat_value0);
323  ok1=!to_rational(expr.op1(), rat_value1);
324 
325  if(ok1 && rat_value1.is_zero())
326  return unchanged(expr);
327 
328  if((ok1 && rat_value1.is_one()) ||
329  (ok0 && rat_value0.is_zero()))
330  {
331  return expr.op0();
332  }
333 
334  if(ok0 && ok1)
335  {
336  rationalt result=rat_value0/rat_value1;
337  exprt tmp=from_rational(result);
338 
339  if(tmp.is_not_nil())
340  return std::move(tmp);
341  }
342  }
343  else if(expr_type.id()==ID_fixedbv)
344  {
345  // division by one?
346  if(expr.op1().is_constant() &&
347  expr.op1().is_one())
348  {
349  return expr.op0();
350  }
351 
352  if(expr.op0().is_constant() &&
353  expr.op1().is_constant())
354  {
355  fixedbvt f0(to_constant_expr(expr.op0()));
356  fixedbvt f1(to_constant_expr(expr.op1()));
357  if(!f1.is_zero())
358  {
359  f0/=f1;
360  return f0.to_expr();
361  }
362  }
363  }
364 
365  return unchanged(expr);
366 }
367 
369 {
370  if(!is_number(expr.type()))
371  return unchanged(expr);
372 
373  if(expr.type().id()==ID_signedbv ||
374  expr.type().id()==ID_unsignedbv ||
375  expr.type().id()==ID_natural ||
376  expr.type().id()==ID_integer)
377  {
378  if(expr.type()==expr.op0().type() &&
379  expr.type()==expr.op1().type())
380  {
381  const auto int_value0 = numeric_cast<mp_integer>(expr.op0());
382  const auto int_value1 = numeric_cast<mp_integer>(expr.op1());
383 
384  if(int_value1.has_value() && *int_value1 == 0)
385  return unchanged(expr); // division by zero
386 
387  if(
388  (int_value1.has_value() && *int_value1 == 1) ||
389  (int_value0.has_value() && *int_value0 == 0))
390  {
391  return from_integer(0, expr.type());
392  }
393 
394  if(int_value0.has_value() && int_value1.has_value())
395  {
396  mp_integer result = *int_value0 % *int_value1;
397  return from_integer(result, expr.type());
398  }
399  }
400  }
401 
402  return unchanged(expr);
403 }
404 
406 {
407  if(!is_number(expr.type()) && expr.type().id() != ID_pointer)
408  return unchanged(expr);
409 
410  bool no_change = true;
411 
412  exprt::operandst new_operands = expr.operands();
413 
414  // floating-point addition is _NOT_ associative; thus,
415  // there is special case for float
416 
417  if(expr.type().id() == ID_floatbv)
418  {
419  // we only merge neighboring constants!
420  Forall_expr(it, new_operands)
421  {
422  const exprt::operandst::iterator next = std::next(it);
423 
424  if(next != new_operands.end())
425  {
426  if(it->type()==next->type() &&
427  it->is_constant() &&
428  next->is_constant())
429  {
431  new_operands.erase(next);
432  no_change = false;
433  }
434  }
435  }
436  }
437  else
438  {
439  // ((T*)p+a)+b -> (T*)p+(a+b)
440  if(
441  expr.type().id() == ID_pointer && expr.operands().size() == 2 &&
442  expr.op0().id() == ID_plus && expr.op0().type().id() == ID_pointer &&
443  expr.op0().operands().size() == 2)
444  {
445  plus_exprt result = to_plus_expr(expr.op0());
446  if(as_const(result).op0().type().id() != ID_pointer)
447  result.op0().swap(result.op1());
448  const exprt &op1 = as_const(result).op1();
449 
450  if(op1.id() == ID_plus)
451  {
452  plus_exprt new_op1 = to_plus_expr(op1);
453  new_op1.add_to_operands(
454  typecast_exprt::conditional_cast(expr.op1(), new_op1.op0().type()));
455  result.op1() = simplify_plus(new_op1);
456  }
457  else
458  {
459  plus_exprt new_op1{
460  op1, typecast_exprt::conditional_cast(expr.op1(), op1.type())};
461  result.op1() = simplify_plus(new_op1);
462  }
463 
464  return changed(simplify_plus(result));
465  }
466 
467  // count the constants
468  size_t count=0;
469  for(const auto &op : expr.operands())
470  {
471  if(is_number(op.type()) && op.is_constant())
472  count++;
473  }
474 
475  // merge constants?
476  if(count>=2)
477  {
478  exprt::operandst::iterator const_sum;
479  bool const_sum_set=false;
480 
481  for(auto it = new_operands.begin(); it != new_operands.end(); it++)
482  {
483  if(is_number(it->type()) && it->is_constant())
484  {
485  if(!const_sum_set)
486  {
487  const_sum=it;
488  const_sum_set=true;
489  }
490  else
491  {
492  if(!sum_expr(to_constant_expr(*const_sum),
493  to_constant_expr(*it)))
494  {
495  *it=from_integer(0, it->type());
496  no_change = false;
497  }
498  }
499  }
500  }
501  }
502 
503  // search for a and -a
504  // first gather all the a's with -a
505  typedef std::unordered_map<exprt, exprt::operandst::iterator, irep_hash>
506  expr_mapt;
507  expr_mapt expr_map;
508 
509  for(auto it = new_operands.begin(); it != new_operands.end(); it++)
510  if(it->id() == ID_unary_minus)
511  {
512  expr_map.insert(std::make_pair(to_unary_minus_expr(*it).op(), it));
513  }
514 
515  // now search for a
516  for(auto it = new_operands.begin(); it != new_operands.end(); it++)
517  {
518  if(expr_map.empty())
519  break;
520  else if(it->id()==ID_unary_minus)
521  continue;
522 
523  expr_mapt::iterator itm=expr_map.find(*it);
524 
525  if(itm!=expr_map.end())
526  {
527  *(itm->second)=from_integer(0, expr.type());
528  *it=from_integer(0, expr.type());
529  expr_map.erase(itm);
530  no_change = false;
531  }
532  }
533 
534  // delete zeros
535  // (can't do for floats, as the result of 0.0 + (-0.0)
536  // need not be -0.0 in std rounding)
537  for(exprt::operandst::iterator it = new_operands.begin();
538  it != new_operands.end();
539  /* no it++ */)
540  {
541  if(is_number(it->type()) && it->is_zero())
542  {
543  it = new_operands.erase(it);
544  no_change = false;
545  }
546  else
547  it++;
548  }
549  }
550 
551  if(new_operands.empty())
552  {
553  return from_integer(0, expr.type());
554  }
555  else if(new_operands.size() == 1)
556  {
557  return new_operands.front();
558  }
559 
560  if(no_change)
561  return unchanged(expr);
562  else
563  {
564  auto tmp = expr;
565  tmp.operands() = std::move(new_operands);
566  return std::move(tmp);
567  }
568 }
569 
572 {
573  auto const &minus_expr = to_minus_expr(expr);
574  if(!is_number(minus_expr.type()) && minus_expr.type().id() != ID_pointer)
575  return unchanged(expr);
576 
577  const exprt::operandst &operands = minus_expr.operands();
578 
579  if(
580  is_number(minus_expr.type()) && is_number(operands[0].type()) &&
581  is_number(operands[1].type()))
582  {
583  // rewrite "a-b" to "a+(-b)"
584  unary_minus_exprt rhs_negated(operands[1]);
585  plus_exprt plus_expr(operands[0], simplify_unary_minus(rhs_negated));
586  return changed(simplify_plus(plus_expr));
587  }
588  else if(
589  minus_expr.type().id() == ID_pointer &&
590  operands[0].type().id() == ID_pointer && is_number(operands[1].type()))
591  {
592  // pointer arithmetic: rewrite "p-i" to "p+(-i)"
593  unary_minus_exprt negated_pointer_offset(operands[1]);
594 
595  plus_exprt pointer_offset_expr(
596  operands[0], simplify_unary_minus(negated_pointer_offset));
597  return changed(simplify_plus(pointer_offset_expr));
598  }
599  else if(
600  is_number(minus_expr.type()) && operands[0].type().id() == ID_pointer &&
601  operands[1].type().id() == ID_pointer)
602  {
603  exprt ptr_op0 = simplify_object(operands[0]).expr;
604  exprt ptr_op1 = simplify_object(operands[1]).expr;
605 
606  auto address_of = expr_try_dynamic_cast<address_of_exprt>(ptr_op0);
607  if(ptr_op0 == ptr_op1 && address_of)
608  {
609  exprt offset_op0 = simplify_pointer_offset(
610  pointer_offset_exprt{operands[0], minus_expr.type()});
611  exprt offset_op1 = simplify_pointer_offset(
612  pointer_offset_exprt{operands[1], minus_expr.type()});
613 
614  const auto object_size =
615  pointer_offset_size(address_of->object().type(), ns);
616  auto element_size =
617  size_of_expr(to_pointer_type(operands[0].type()).base_type(), ns);
618 
619  if(
620  offset_op0.is_constant() && offset_op1.is_constant() &&
621  object_size.has_value() && element_size.has_value() &&
622  element_size->is_constant() && !element_size->is_zero() &&
623  numeric_cast_v<mp_integer>(to_constant_expr(offset_op0)) <=
624  *object_size &&
625  numeric_cast_v<mp_integer>(to_constant_expr(offset_op1)) <=
626  *object_size)
627  {
629  minus_exprt{offset_op0, offset_op1},
630  typecast_exprt{*element_size, minus_expr.type()}}));
631  }
632  }
633 
634  const exprt &ptr_op0_skipped_tc = skip_typecast(ptr_op0);
635  const exprt &ptr_op1_skipped_tc = skip_typecast(ptr_op1);
636  if(
637  is_number(ptr_op0_skipped_tc.type()) &&
638  is_number(ptr_op1_skipped_tc.type()))
639  {
640  exprt offset_op0 = simplify_pointer_offset(
641  pointer_offset_exprt{operands[0], minus_expr.type()});
642  exprt offset_op1 = simplify_pointer_offset(
643  pointer_offset_exprt{operands[1], minus_expr.type()});
644 
645  auto element_size =
646  size_of_expr(to_pointer_type(operands[0].type()).base_type(), ns);
647 
648  if(
649  element_size.has_value() && element_size->is_constant() &&
650  !element_size->is_zero())
651  {
653  minus_exprt{offset_op0, offset_op1},
654  typecast_exprt{*element_size, minus_expr.type()}}));
655  }
656  }
657  }
658 
659  return unchanged(expr);
660 }
661 
664 {
666  return unchanged(expr);
667 
668  // check if these are really boolean
669  if(!expr.is_boolean())
670  {
671  bool all_bool=true;
672 
673  for(const auto &op : expr.operands())
674  {
675  if(op.id() == ID_typecast && to_typecast_expr(op).op().is_boolean())
676  {
677  }
678  else if(op.is_zero() || op.is_one())
679  {
680  }
681  else
682  all_bool=false;
683  }
684 
685  if(all_bool)
686  {
687  // re-write to boolean+typecast
688  exprt new_expr=expr;
689 
690  if(expr.id()==ID_bitand)
691  new_expr.id(ID_and);
692  else if(expr.id()==ID_bitor)
693  new_expr.id(ID_or);
694  else if(expr.id()==ID_bitxor)
695  new_expr.id(ID_xor);
696  else
697  UNREACHABLE;
698 
699  Forall_operands(it, new_expr)
700  {
701  if(it->id()==ID_typecast)
702  *it = to_typecast_expr(*it).op();
703  else if(it->is_zero())
704  *it=false_exprt();
705  else if(it->is_one())
706  *it=true_exprt();
707  }
708 
709  new_expr.type()=bool_typet();
710  new_expr = simplify_boolean(new_expr);
711 
712  return changed(simplify_typecast(typecast_exprt(new_expr, expr.type())));
713  }
714  }
715 
716  bool no_change = true;
717  auto new_expr = expr;
718 
719  // try to merge constants
720 
721  const std::size_t width = to_bitvector_type(expr.type()).get_width();
722 
723  while(new_expr.operands().size() >= 2)
724  {
725  if(!new_expr.op0().is_constant())
726  break;
727 
728  if(!new_expr.op1().is_constant())
729  break;
730 
731  if(new_expr.op0().type() != new_expr.type())
732  break;
733 
734  if(new_expr.op1().type() != new_expr.type())
735  break;
736 
737  const auto &a_val = to_constant_expr(new_expr.op0()).get_value();
738  const auto &b_val = to_constant_expr(new_expr.op1()).get_value();
739 
740  std::function<bool(bool, bool)> f;
741 
742  if(new_expr.id() == ID_bitand)
743  f = [](bool a, bool b) { return a && b; };
744  else if(new_expr.id() == ID_bitor)
745  f = [](bool a, bool b) { return a || b; };
746  else if(new_expr.id() == ID_bitxor)
747  f = [](bool a, bool b) { return a != b; };
748  else
749  UNREACHABLE;
750 
751  const irep_idt new_value =
752  make_bvrep(width, [&a_val, &b_val, &width, &f](std::size_t i) {
753  return f(
754  get_bvrep_bit(a_val, width, i), get_bvrep_bit(b_val, width, i));
755  });
756 
757  constant_exprt new_op(new_value, expr.type());
758 
759  // erase first operand
760  new_expr.operands().erase(new_expr.operands().begin());
761  new_expr.op0().swap(new_op);
762 
763  no_change = false;
764  }
765 
766  // now erase 'all zeros' out of bitor, bitxor
767 
768  if(new_expr.id() == ID_bitor || new_expr.id() == ID_bitxor)
769  {
770  for(exprt::operandst::iterator it = new_expr.operands().begin();
771  it != new_expr.operands().end();) // no it++
772  {
773  if(it->is_zero() && new_expr.operands().size() > 1)
774  {
775  it = new_expr.operands().erase(it);
776  no_change = false;
777  }
778  else if(
779  it->is_constant() && it->type().id() == ID_bv &&
781  new_expr.operands().size() > 1)
782  {
783  it = new_expr.operands().erase(it);
784  no_change = false;
785  }
786  else
787  it++;
788  }
789  }
790 
791  // now erase 'all ones' out of bitand
792 
793  if(new_expr.id() == ID_bitand)
794  {
795  const auto all_ones = power(2, width) - 1;
796  for(exprt::operandst::iterator it = new_expr.operands().begin();
797  it != new_expr.operands().end();) // no it++
798  {
799  if(
800  it->is_constant() &&
801  bvrep2integer(to_constant_expr(*it).get_value(), width, false) ==
802  all_ones &&
803  new_expr.operands().size() > 1)
804  {
805  it = new_expr.operands().erase(it);
806  no_change = false;
807  }
808  else
809  it++;
810  }
811  }
812 
813  // two operands that are syntactically the same
814 
815  if(new_expr.operands().size() == 2 && new_expr.op0() == new_expr.op1())
816  {
817  if(new_expr.id() == ID_bitand || new_expr.id() == ID_bitor)
818  {
819  return new_expr.op0();
820  }
821  else if(new_expr.id() == ID_bitxor)
822  {
823  return constant_exprt(integer2bvrep(0, width), new_expr.type());
824  }
825  }
826 
827  if(new_expr.operands().size() == 1)
828  return new_expr.op0();
829 
830  if(no_change)
831  return unchanged(expr);
832  else
833  return std::move(new_expr);
834 }
835 
838 {
839  const typet &src_type = expr.src().type();
840 
841  if(!can_cast_type<bitvector_typet>(src_type))
842  return unchanged(expr);
843 
844  const std::size_t src_bit_width = to_bitvector_type(src_type).get_width();
845 
846  const auto index_converted_to_int = numeric_cast<mp_integer>(expr.index());
847  if(
848  !index_converted_to_int.has_value() || *index_converted_to_int < 0 ||
849  *index_converted_to_int >= src_bit_width)
850  {
851  return unchanged(expr);
852  }
853 
854  if(!expr.src().is_constant())
855  return unchanged(expr);
856 
857  const bool bit = get_bvrep_bit(
858  to_constant_expr(expr.src()).get_value(),
859  src_bit_width,
860  numeric_cast_v<std::size_t>(*index_converted_to_int));
861 
862  return make_boolean_expr(bit);
863 }
864 
867 {
868  bool no_change = true;
869 
870  concatenation_exprt new_expr = expr;
871 
872  if(can_cast_type<bitvector_typet>(new_expr.type()))
873  {
874  // first, turn bool into bvec[1]
875  Forall_operands(it, new_expr)
876  {
877  exprt &op=*it;
878  if(op.is_true() || op.is_false())
879  {
880  const bool value = op.is_true();
881  op = from_integer(value, unsignedbv_typet(1));
882  no_change = false;
883  }
884  }
885 
886  // search for neighboring constants to merge
887  size_t i=0;
888 
889  while(i < new_expr.operands().size() - 1)
890  {
891  exprt &opi = new_expr.operands()[i];
892  exprt &opn = new_expr.operands()[i + 1];
893 
894  if(
895  opi.is_constant() && opn.is_constant() &&
898  {
899  // merge!
900  const auto &value_i = to_constant_expr(opi).get_value();
901  const auto &value_n = to_constant_expr(opn).get_value();
902  const auto width_i = to_bitvector_type(opi.type()).get_width();
903  const auto width_n = to_bitvector_type(opn.type()).get_width();
904  const auto new_width = width_i + width_n;
905 
906  const auto new_value = make_bvrep(
907  new_width, [&value_i, &value_n, width_i, width_n](std::size_t x) {
908  return x < width_n ? get_bvrep_bit(value_n, width_n, x)
909  : get_bvrep_bit(value_i, width_i, x - width_n);
910  });
911 
912  to_constant_expr(opi).set_value(new_value);
913  to_bitvector_type(opi.type()).set_width(new_width);
914  // erase opn
915  new_expr.operands().erase(new_expr.operands().begin() + i + 1);
916  no_change = false;
917  }
918  else if(
919  skip_typecast(opi).id() == ID_extractbits &&
920  skip_typecast(opn).id() == ID_extractbits)
921  {
924 
925  if(
926  eb_i.src() == eb_n.src() && eb_i.index().is_constant() &&
927  eb_n.index().is_constant() &&
928  numeric_cast_v<mp_integer>(to_constant_expr(eb_i.index())) ==
929  numeric_cast_v<mp_integer>(to_constant_expr(eb_n.index())) +
930  to_bitvector_type(eb_n.type()).get_width())
931  {
932  extractbits_exprt eb_merged = eb_i;
933  eb_merged.index() = eb_n.index();
934  to_bitvector_type(eb_merged.type())
935  .set_width(
936  to_bitvector_type(eb_i.type()).get_width() +
937  to_bitvector_type(eb_n.type()).get_width());
938  if(expr.type().id() != eb_merged.type().id())
939  {
941  bt.set_width(to_bitvector_type(eb_merged.type()).get_width());
942  opi = simplify_typecast(typecast_exprt{eb_merged, bt});
943  }
944  else
945  opi = eb_merged;
946  // erase opn
947  new_expr.operands().erase(new_expr.operands().begin() + i + 1);
948  no_change = false;
949  }
950  else
951  ++i;
952  }
953  else
954  i++;
955  }
956  }
957  else if(new_expr.type().id() == ID_verilog_unsignedbv)
958  {
959  // search for neighboring constants to merge
960  size_t i=0;
961 
962  while(i < new_expr.operands().size() - 1)
963  {
964  exprt &opi = new_expr.operands()[i];
965  exprt &opn = new_expr.operands()[i + 1];
966 
967  if(
968  opi.is_constant() && opn.is_constant() &&
971  {
972  // merge!
973  const std::string new_value=
974  opi.get_string(ID_value)+opn.get_string(ID_value);
975  opi.set(ID_value, new_value);
976  to_bitvector_type(opi.type()).set_width(new_value.size());
977  opi.type().id(ID_verilog_unsignedbv);
978  // erase opn
979  new_expr.operands().erase(new_expr.operands().begin() + i + 1);
980  no_change = false;
981  }
982  else
983  i++;
984  }
985  }
986 
987  // { x } = x
988  if(
989  new_expr.operands().size() == 1 && new_expr.op0().type() == new_expr.type())
990  {
991  return new_expr.op0();
992  }
993 
994  if(no_change)
995  return unchanged(expr);
996  else
997  return std::move(new_expr);
998 }
999 
1002 {
1004  return unchanged(expr);
1005 
1006  const auto distance = numeric_cast<mp_integer>(expr.distance());
1007 
1008  if(!distance.has_value())
1009  return unchanged(expr);
1010 
1011  if(*distance == 0)
1012  return expr.op();
1013 
1014  auto value = numeric_cast<mp_integer>(expr.op());
1015 
1016  if(
1017  !value.has_value() && expr.op().type().id() == ID_bv &&
1018  expr.op().is_constant())
1019  {
1020  const std::size_t width = to_bitvector_type(expr.op().type()).get_width();
1021  value =
1022  bvrep2integer(to_constant_expr(expr.op()).get_value(), width, false);
1023  }
1024 
1025  if(!value.has_value())
1026  return unchanged(expr);
1027 
1028  if(
1029  expr.op().type().id() == ID_unsignedbv ||
1030  expr.op().type().id() == ID_signedbv || expr.op().type().id() == ID_bv)
1031  {
1032  const std::size_t width = to_bitvector_type(expr.op().type()).get_width();
1033 
1034  if(expr.id()==ID_lshr)
1035  {
1036  // this is to guard against large values of distance
1037  if(*distance >= width)
1038  {
1039  return from_integer(0, expr.type());
1040  }
1041  else if(*distance >= 0)
1042  {
1043  if(*value < 0)
1044  *value += power(2, width);
1045  *value /= power(2, *distance);
1046  return from_integer(*value, expr.type());
1047  }
1048  }
1049  else if(expr.id()==ID_ashr)
1050  {
1051  if(*distance >= 0)
1052  {
1053  // this is to simulate an arithmetic right shift
1054  mp_integer new_value = *value >> *distance;
1055  return from_integer(new_value, expr.type());
1056  }
1057  }
1058  else if(expr.id()==ID_shl)
1059  {
1060  // this is to guard against large values of distance
1061  if(*distance >= width)
1062  {
1063  return from_integer(0, expr.type());
1064  }
1065  else if(*distance >= 0)
1066  {
1067  *value *= power(2, *distance);
1068  return from_integer(*value, expr.type());
1069  }
1070  }
1071  }
1072  else if(
1073  expr.op().type().id() == ID_integer || expr.op().type().id() == ID_natural)
1074  {
1075  if(expr.id()==ID_lshr)
1076  {
1077  if(*distance >= 0)
1078  {
1079  *value /= power(2, *distance);
1080  return from_integer(*value, expr.type());
1081  }
1082  }
1083  else if(expr.id()==ID_ashr)
1084  {
1085  // this is to simulate an arithmetic right shift
1086  if(*distance >= 0)
1087  {
1088  mp_integer new_value = *value / power(2, *distance);
1089  if(*value < 0 && new_value == 0)
1090  new_value=-1;
1091 
1092  return from_integer(new_value, expr.type());
1093  }
1094  }
1095  else if(expr.id()==ID_shl)
1096  {
1097  if(*distance >= 0)
1098  {
1099  *value *= power(2, *distance);
1100  return from_integer(*value, expr.type());
1101  }
1102  }
1103  }
1104 
1105  return unchanged(expr);
1106 }
1107 
1110 {
1111  if(!is_number(expr.type()))
1112  return unchanged(expr);
1113 
1114  const auto base = numeric_cast<mp_integer>(expr.op0());
1115  const auto exponent = numeric_cast<mp_integer>(expr.op1());
1116 
1117  if(!base.has_value())
1118  return unchanged(expr);
1119 
1120  if(!exponent.has_value())
1121  return unchanged(expr);
1122 
1123  mp_integer result = power(*base, *exponent);
1124 
1125  return from_integer(result, expr.type());
1126 }
1127 
1131 {
1132  const typet &op0_type = expr.src().type();
1133 
1134  if(
1135  !can_cast_type<bitvector_typet>(op0_type) &&
1137  {
1138  return unchanged(expr);
1139  }
1140 
1141  const auto end = numeric_cast<mp_integer>(expr.index());
1142 
1143  if(!end.has_value())
1144  return unchanged(expr);
1145 
1146  const auto width = pointer_offset_bits(op0_type, ns);
1147 
1148  if(!width.has_value())
1149  return unchanged(expr);
1150 
1151  const auto result_width = pointer_offset_bits(expr.type(), ns);
1152 
1153  if(!result_width.has_value())
1154  return unchanged(expr);
1155 
1156  const auto start = std::optional(*end + *result_width - 1);
1157 
1158  if(*start < 0 || *start >= (*width) || *end < 0 || *end >= (*width))
1159  return unchanged(expr);
1160 
1161  DATA_INVARIANT(*start >= *end, "extractbits must have start >= end");
1162 
1163  if(expr.src().is_constant())
1164  {
1165  const auto svalue = expr2bits(expr.src(), true, ns);
1166 
1167  if(!svalue.has_value() || svalue->size() != *width)
1168  return unchanged(expr);
1169 
1170  std::string extracted_value = svalue->substr(
1171  numeric_cast_v<std::size_t>(*end),
1172  numeric_cast_v<std::size_t>(*start - *end + 1));
1173 
1174  auto result = bits2expr(extracted_value, expr.type(), true, ns);
1175  if(!result.has_value())
1176  return unchanged(expr);
1177 
1178  return std::move(*result);
1179  }
1180  else if(expr.src().id() == ID_concatenation)
1181  {
1182  // the most-significant bit comes first in an concatenation_exprt, hence we
1183  // count down
1184  mp_integer offset = *width;
1185 
1186  for(const auto &op : expr.src().operands())
1187  {
1188  auto op_width = pointer_offset_bits(op.type(), ns);
1189 
1190  if(!op_width.has_value() || *op_width <= 0)
1191  return unchanged(expr);
1192 
1193  if(*start < offset && offset <= *end + *op_width)
1194  {
1195  extractbits_exprt result = expr;
1196  result.src() = op;
1197  result.index() =
1198  from_integer(*end - (offset - *op_width), expr.index().type());
1199  return changed(simplify_extractbits(result));
1200  }
1201 
1202  offset -= *op_width;
1203  }
1204  }
1205  else if(auto eb_src = expr_try_dynamic_cast<extractbits_exprt>(expr.src()))
1206  {
1207  if(eb_src->index().is_constant())
1208  {
1209  extractbits_exprt result = *eb_src;
1210  result.type() = expr.type();
1211  const mp_integer src_index =
1212  numeric_cast_v<mp_integer>(to_constant_expr(eb_src->index()));
1213  result.index() = from_integer(src_index + *end, eb_src->index().type());
1214  return changed(simplify_extractbits(result));
1215  }
1216  }
1217  else if(*end == 0 && *start + 1 == *width)
1218  {
1219  typecast_exprt tc{expr.src(), expr.type()};
1220  return changed(simplify_typecast(tc));
1221  }
1222 
1223  return unchanged(expr);
1224 }
1225 
1228 {
1229  // simply remove, this is always 'nop'
1230  return expr.op();
1231 }
1232 
1235 {
1236  if(!is_number(expr.type()))
1237  return unchanged(expr);
1238 
1239  const exprt &operand = expr.op();
1240 
1241  if(expr.type()!=operand.type())
1242  return unchanged(expr);
1243 
1244  if(operand.id()==ID_unary_minus)
1245  {
1246  // cancel out "-(-x)" to "x"
1247  if(!is_number(to_unary_minus_expr(operand).op().type()))
1248  return unchanged(expr);
1249 
1250  return to_unary_minus_expr(operand).op();
1251  }
1252  else if(operand.is_constant())
1253  {
1254  const irep_idt &type_id=expr.type().id();
1255  const auto &constant_expr = to_constant_expr(operand);
1256 
1257  if(type_id==ID_integer ||
1258  type_id==ID_signedbv ||
1259  type_id==ID_unsignedbv)
1260  {
1261  const auto int_value = numeric_cast<mp_integer>(constant_expr);
1262 
1263  if(!int_value.has_value())
1264  return unchanged(expr);
1265 
1266  return from_integer(-*int_value, expr.type());
1267  }
1268  else if(type_id==ID_rational)
1269  {
1270  rationalt r;
1271  if(to_rational(constant_expr, r))
1272  return unchanged(expr);
1273 
1274  return from_rational(-r);
1275  }
1276  else if(type_id==ID_fixedbv)
1277  {
1278  fixedbvt f(constant_expr);
1279  f.negate();
1280  return f.to_expr();
1281  }
1282  else if(type_id==ID_floatbv)
1283  {
1284  ieee_floatt f(constant_expr);
1285  f.negate();
1286  return f.to_expr();
1287  }
1288  }
1289 
1290  return unchanged(expr);
1291 }
1292 
1295 {
1296  const exprt &op = expr.op();
1297 
1298  const auto &type = expr.type();
1299 
1300  if(
1301  type.id() == ID_bv || type.id() == ID_unsignedbv ||
1302  type.id() == ID_signedbv)
1303  {
1304  const auto width = to_bitvector_type(type).get_width();
1305 
1306  if(op.type() == type)
1307  {
1308  if(op.is_constant())
1309  {
1310  const auto &value = to_constant_expr(op).get_value();
1311  const auto new_value =
1312  make_bvrep(width, [&value, &width](std::size_t i) {
1313  return !get_bvrep_bit(value, width, i);
1314  });
1315  return constant_exprt(new_value, op.type());
1316  }
1317  }
1318  }
1319 
1320  return unchanged(expr);
1321 }
1322 
1326 {
1327  if(!expr.is_boolean())
1328  return unchanged(expr);
1329 
1330  exprt tmp0=expr.op0();
1331  exprt tmp1=expr.op1();
1332 
1333  // types must match
1334  if(tmp0.type() != tmp1.type())
1335  return unchanged(expr);
1336 
1337  // if rhs is ID_if (and lhs is not), swap operands for == and !=
1338  if((expr.id()==ID_equal || expr.id()==ID_notequal) &&
1339  tmp0.id()!=ID_if &&
1340  tmp1.id()==ID_if)
1341  {
1342  auto new_expr = expr;
1343  new_expr.op0().swap(new_expr.op1());
1344  return changed(simplify_inequality(new_expr)); // recursive call
1345  }
1346 
1347  if(tmp0.id()==ID_if && tmp0.operands().size()==3)
1348  {
1349  if_exprt if_expr=lift_if(expr, 0);
1350  if_expr.true_case() =
1352  if_expr.false_case() =
1354  return changed(simplify_if(if_expr));
1355  }
1356 
1357  // see if we are comparing pointers that are address_of
1358  if(
1359  skip_typecast(tmp0).id() == ID_address_of &&
1360  skip_typecast(tmp1).id() == ID_address_of &&
1361  (expr.id() == ID_equal || expr.id() == ID_notequal))
1362  {
1363  return simplify_inequality_address_of(expr);
1364  }
1365 
1366  if(tmp0.id()==ID_pointer_object &&
1367  tmp1.id()==ID_pointer_object &&
1368  (expr.id()==ID_equal || expr.id()==ID_notequal))
1369  {
1371  }
1372 
1373  if(tmp0.type().id()==ID_c_enum_tag)
1374  tmp0.type()=ns.follow_tag(to_c_enum_tag_type(tmp0.type()));
1375 
1376  if(tmp1.type().id()==ID_c_enum_tag)
1377  tmp1.type()=ns.follow_tag(to_c_enum_tag_type(tmp1.type()));
1378 
1379  const bool tmp0_const = tmp0.is_constant();
1380  const bool tmp1_const = tmp1.is_constant();
1381 
1382  // are _both_ constant?
1383  if(tmp0_const && tmp1_const)
1384  {
1385  return simplify_inequality_both_constant(expr);
1386  }
1387  else if(tmp0_const)
1388  {
1389  // we want the constant on the RHS
1390 
1391  binary_relation_exprt new_expr = expr;
1392 
1393  if(expr.id()==ID_ge)
1394  new_expr.id(ID_le);
1395  else if(expr.id()==ID_le)
1396  new_expr.id(ID_ge);
1397  else if(expr.id()==ID_gt)
1398  new_expr.id(ID_lt);
1399  else if(expr.id()==ID_lt)
1400  new_expr.id(ID_gt);
1401 
1402  new_expr.op0().swap(new_expr.op1());
1403 
1404  // RHS is constant, LHS is not
1405  return changed(simplify_inequality_rhs_is_constant(new_expr));
1406  }
1407  else if(tmp1_const)
1408  {
1409  // RHS is constant, LHS is not
1411  }
1412  else
1413  {
1414  // both are not constant
1415  return simplify_inequality_no_constant(expr);
1416  }
1417 }
1418 
1422  const binary_relation_exprt &expr)
1423 {
1424  exprt tmp0 = expr.op0();
1425  exprt tmp1 = expr.op1();
1426 
1427  if(tmp0.type().id() == ID_c_enum_tag)
1428  tmp0.type() = ns.follow_tag(to_c_enum_tag_type(tmp0.type()));
1429 
1430  if(tmp1.type().id() == ID_c_enum_tag)
1431  tmp1.type() = ns.follow_tag(to_c_enum_tag_type(tmp1.type()));
1432 
1433  const auto &tmp0_const = to_constant_expr(tmp0);
1434  const auto &tmp1_const = to_constant_expr(tmp1);
1435 
1436  if(expr.id() == ID_equal || expr.id() == ID_notequal)
1437  {
1438  // two constants compare equal when there values (as strings) are the same
1439  // or both of them are pointers and both represent NULL in some way
1440  bool equal = (tmp0_const.get_value() == tmp1_const.get_value());
1441  if(
1442  !equal && tmp0_const.type().id() == ID_pointer &&
1443  tmp1_const.type().id() == ID_pointer)
1444  {
1445  if(
1446  !config.ansi_c.NULL_is_zero && (tmp0_const.get_value() == ID_NULL ||
1447  tmp1_const.get_value() == ID_NULL))
1448  {
1449  // if NULL is not zero on this platform, we really don't know what it
1450  // is and therefore cannot simplify
1451  return unchanged(expr);
1452  }
1453  equal = tmp0_const.is_zero() && tmp1_const.is_zero();
1454  }
1455  return make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
1456  }
1457 
1458  if(tmp0.type().id() == ID_fixedbv)
1459  {
1460  fixedbvt f0(tmp0_const);
1461  fixedbvt f1(tmp1_const);
1462 
1463  if(expr.id() == ID_ge)
1464  return make_boolean_expr(f0 >= f1);
1465  else if(expr.id() == ID_le)
1466  return make_boolean_expr(f0 <= f1);
1467  else if(expr.id() == ID_gt)
1468  return make_boolean_expr(f0 > f1);
1469  else if(expr.id() == ID_lt)
1470  return make_boolean_expr(f0 < f1);
1471  else
1472  UNREACHABLE;
1473  }
1474  else if(tmp0.type().id() == ID_floatbv)
1475  {
1476  ieee_floatt f0(tmp0_const);
1477  ieee_floatt f1(tmp1_const);
1478 
1479  if(expr.id() == ID_ge)
1480  return make_boolean_expr(f0 >= f1);
1481  else if(expr.id() == ID_le)
1482  return make_boolean_expr(f0 <= f1);
1483  else if(expr.id() == ID_gt)
1484  return make_boolean_expr(f0 > f1);
1485  else if(expr.id() == ID_lt)
1486  return make_boolean_expr(f0 < f1);
1487  else
1488  UNREACHABLE;
1489  }
1490  else if(tmp0.type().id() == ID_rational)
1491  {
1492  rationalt r0, r1;
1493 
1494  if(to_rational(tmp0, r0))
1495  return unchanged(expr);
1496 
1497  if(to_rational(tmp1, r1))
1498  return unchanged(expr);
1499 
1500  if(expr.id() == ID_ge)
1501  return make_boolean_expr(r0 >= r1);
1502  else if(expr.id() == ID_le)
1503  return make_boolean_expr(r0 <= r1);
1504  else if(expr.id() == ID_gt)
1505  return make_boolean_expr(r0 > r1);
1506  else if(expr.id() == ID_lt)
1507  return make_boolean_expr(r0 < r1);
1508  else
1509  UNREACHABLE;
1510  }
1511  else
1512  {
1513  const auto v0 = numeric_cast<mp_integer>(tmp0_const);
1514 
1515  if(!v0.has_value())
1516  return unchanged(expr);
1517 
1518  const auto v1 = numeric_cast<mp_integer>(tmp1_const);
1519 
1520  if(!v1.has_value())
1521  return unchanged(expr);
1522 
1523  if(expr.id() == ID_ge)
1524  return make_boolean_expr(*v0 >= *v1);
1525  else if(expr.id() == ID_le)
1526  return make_boolean_expr(*v0 <= *v1);
1527  else if(expr.id() == ID_gt)
1528  return make_boolean_expr(*v0 > *v1);
1529  else if(expr.id() == ID_lt)
1530  return make_boolean_expr(*v0 < *v1);
1531  else
1532  UNREACHABLE;
1533  }
1534 }
1535 
1536 static bool eliminate_common_addends(exprt &op0, exprt &op1)
1537 {
1538  // we can't eliminate zeros
1539  if(
1540  op0.is_zero() || op1.is_zero() ||
1541  (op0.is_constant() && to_constant_expr(op0).is_null_pointer()) ||
1542  (op1.is_constant() && to_constant_expr(op1).is_null_pointer()))
1543  {
1544  return true;
1545  }
1546 
1547  if(op0.id()==ID_plus)
1548  {
1549  bool no_change = true;
1550 
1551  Forall_operands(it, op0)
1552  if(!eliminate_common_addends(*it, op1))
1553  no_change = false;
1554 
1555  return no_change;
1556  }
1557  else if(op1.id()==ID_plus)
1558  {
1559  bool no_change = true;
1560 
1561  Forall_operands(it, op1)
1562  if(!eliminate_common_addends(op0, *it))
1563  no_change = false;
1564 
1565  return no_change;
1566  }
1567  else if(op0==op1)
1568  {
1569  if(!op0.is_zero() &&
1570  op0.type().id()!=ID_complex)
1571  {
1572  // elimination!
1573  op0=from_integer(0, op0.type());
1574  op1=from_integer(0, op1.type());
1575  return false;
1576  }
1577  }
1578 
1579  return true;
1580 }
1581 
1583  const binary_relation_exprt &expr)
1584 {
1585  // pretty much all of the simplifications below are unsound
1586  // for IEEE float because of NaN!
1587 
1588  if(expr.op0().type().id() == ID_floatbv)
1589  return unchanged(expr);
1590 
1591  if(expr.op0().type().id() == ID_pointer)
1592  {
1593  exprt ptr_op0 = simplify_object(expr.op0()).expr;
1594  exprt ptr_op1 = simplify_object(expr.op1()).expr;
1595 
1596  if(ptr_op0 == ptr_op1)
1597  {
1598  pointer_offset_exprt offset_op0{expr.op0(), size_type()};
1599  pointer_offset_exprt offset_op1{expr.op1(), size_type()};
1600 
1602  std::move(offset_op0), expr.id(), std::move(offset_op1)}));
1603  }
1604  // simplifications below require same-object, which we don't check for
1605  else if(expr.id() != ID_equal && expr.id() != ID_notequal)
1606  {
1607  return unchanged(expr);
1608  }
1609  else if(
1610  expr.id() == ID_equal && ptr_op0.id() == ID_address_of &&
1611  ptr_op1.id() == ID_address_of)
1612  {
1613  // comparing pointers: if both are address-of-plus-some-constant such that
1614  // the resulting pointer remains within object bounds then they can never
1615  // be equal
1616  auto in_bounds = [this](const exprt &object_ptr, const exprt &expr_op) {
1617  auto object_size =
1618  size_of_expr(to_address_of_expr(object_ptr).object().type(), ns);
1619 
1620  if(object_size.has_value())
1621  {
1622  pointer_offset_exprt offset{expr_op, object_size->type()};
1623  exprt in_object_bounds =
1625  std::move(offset), ID_lt, std::move(*object_size)})
1626  .expr;
1627  if(in_object_bounds.is_constant())
1628  return tvt{in_object_bounds.is_true()};
1629  }
1630 
1631  return tvt::unknown();
1632  };
1633 
1634  if(
1635  in_bounds(ptr_op0, expr.op0()).is_true() &&
1636  in_bounds(ptr_op1, expr.op1()).is_true())
1637  {
1638  return false_exprt{};
1639  }
1640  }
1641  }
1642 
1643  // eliminate strict inequalities
1644  if(expr.id()==ID_notequal)
1645  {
1646  auto new_rel_expr = expr;
1647  new_rel_expr.id(ID_equal);
1648  auto new_expr = simplify_inequality_no_constant(new_rel_expr);
1649  return changed(simplify_not(not_exprt(new_expr)));
1650  }
1651  else if(expr.id()==ID_gt)
1652  {
1653  auto new_rel_expr = expr;
1654  new_rel_expr.id(ID_ge);
1655  // swap operands
1656  new_rel_expr.lhs().swap(new_rel_expr.rhs());
1657  auto new_expr = simplify_inequality_no_constant(new_rel_expr);
1658  return changed(simplify_not(not_exprt(new_expr)));
1659  }
1660  else if(expr.id()==ID_lt)
1661  {
1662  auto new_rel_expr = expr;
1663  new_rel_expr.id(ID_ge);
1664  auto new_expr = simplify_inequality_no_constant(new_rel_expr);
1665  return changed(simplify_not(not_exprt(new_expr)));
1666  }
1667  else if(expr.id()==ID_le)
1668  {
1669  auto new_rel_expr = expr;
1670  new_rel_expr.id(ID_ge);
1671  // swap operands
1672  new_rel_expr.lhs().swap(new_rel_expr.rhs());
1673  return changed(simplify_inequality_no_constant(new_rel_expr));
1674  }
1675 
1676  // now we only have >=, =
1677 
1678  INVARIANT(
1679  expr.id() == ID_ge || expr.id() == ID_equal,
1680  "we previously converted all other cases to >= or ==");
1681 
1682  // syntactically equal?
1683 
1684  if(expr.op0() == expr.op1())
1685  return true_exprt();
1686 
1687  // See if we can eliminate common addends on both sides.
1688  // On bit-vectors, this is only sound on '='.
1689  if(expr.id()==ID_equal)
1690  {
1691  auto new_expr = to_equal_expr(expr);
1692  if(!eliminate_common_addends(new_expr.lhs(), new_expr.rhs()))
1693  {
1694  // remove zeros
1695  new_expr.lhs() = simplify_node(new_expr.lhs());
1696  new_expr.rhs() = simplify_node(new_expr.rhs());
1697  return changed(simplify_inequality(new_expr)); // recursive call
1698  }
1699  }
1700 
1701  return unchanged(expr);
1702 }
1703 
1707  const binary_relation_exprt &expr)
1708 {
1709  // the constant is always on the RHS
1710  PRECONDITION(expr.op1().is_constant());
1711 
1712  if(expr.op0().id()==ID_if && expr.op0().operands().size()==3)
1713  {
1714  if_exprt if_expr=lift_if(expr, 0);
1715  if_expr.true_case() =
1717  if_expr.false_case() =
1719  return changed(simplify_if(if_expr));
1720  }
1721 
1722  // do we deal with pointers?
1723  if(expr.op1().type().id()==ID_pointer)
1724  {
1725  if(expr.id()==ID_notequal)
1726  {
1727  auto new_rel_expr = expr;
1728  new_rel_expr.id(ID_equal);
1729  auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
1730  return changed(simplify_not(not_exprt(new_expr)));
1731  }
1732 
1733  // very special case for pointers
1734  if(expr.id() != ID_equal)
1735  return unchanged(expr);
1736 
1737  const constant_exprt &op1_constant = to_constant_expr(expr.op1());
1738 
1739  if(op1_constant.is_null_pointer())
1740  {
1741  // the address of an object is never NULL
1742 
1743  if(expr.op0().id() == ID_address_of)
1744  {
1745  const auto &object = to_address_of_expr(expr.op0()).object();
1746 
1747  if(
1748  object.id() == ID_symbol || object.id() == ID_dynamic_object ||
1749  object.id() == ID_member || object.id() == ID_index ||
1750  object.id() == ID_string_constant)
1751  {
1752  return false_exprt();
1753  }
1754  }
1755  else if(
1756  expr.op0().id() == ID_typecast &&
1757  expr.op0().type().id() == ID_pointer &&
1758  to_typecast_expr(expr.op0()).op().id() == ID_address_of)
1759  {
1760  const auto &object =
1762 
1763  if(
1764  object.id() == ID_symbol || object.id() == ID_dynamic_object ||
1765  object.id() == ID_member || object.id() == ID_index ||
1766  object.id() == ID_string_constant)
1767  {
1768  return false_exprt();
1769  }
1770  }
1771  else if(
1772  expr.op0().id() == ID_typecast && expr.op0().type().id() == ID_pointer)
1773  {
1774  exprt op = to_typecast_expr(expr.op0()).op();
1775  if(
1776  op.type().id() != ID_pointer &&
1777  (!config.ansi_c.NULL_is_zero || !is_number(op.type()) ||
1778  op.type().id() == ID_complex))
1779  {
1780  return unchanged(expr);
1781  }
1782 
1783  // (type)ptr == NULL -> ptr == NULL
1784  // note that 'ptr' may be an integer
1785  auto new_expr = expr;
1786  new_expr.op0().swap(op);
1787  if(new_expr.op0().type().id() != ID_pointer)
1788  new_expr.op1() = from_integer(0, new_expr.op0().type());
1789  else
1790  new_expr.op1().type() = new_expr.op0().type();
1791  return changed(simplify_inequality(new_expr)); // do again!
1792  }
1793  else if(expr.op0().id() == ID_plus)
1794  {
1795  exprt offset =
1797  if(!offset.is_constant())
1798  return unchanged(expr);
1799 
1800  exprt ptr = simplify_object(expr.op0()).expr;
1801  // NULL + N == NULL is N == 0
1802  if(ptr.is_constant() && to_constant_expr(ptr).is_null_pointer())
1803  return make_boolean_expr(offset.is_zero());
1804  // &x + N == NULL is false when the offset is in bounds
1805  else if(auto address_of = expr_try_dynamic_cast<address_of_exprt>(ptr))
1806  {
1807  const auto object_size =
1808  pointer_offset_size(address_of->object().type(), ns);
1809  if(
1810  object_size.has_value() &&
1811  numeric_cast_v<mp_integer>(to_constant_expr(offset)) < *object_size)
1812  {
1813  return false_exprt();
1814  }
1815  }
1816  }
1817  }
1818 
1819  // all we are doing with pointers
1820  return unchanged(expr);
1821  }
1822 
1823  // is it a separation predicate?
1824 
1825  if(expr.op0().id()==ID_plus)
1826  {
1827  // see if there is a constant in the sum
1828 
1829  if(expr.id()==ID_equal || expr.id()==ID_notequal)
1830  {
1831  mp_integer constant=0;
1832  bool op_changed = false;
1833  auto new_expr = expr;
1834 
1835  Forall_operands(it, new_expr.op0())
1836  {
1837  if(it->is_constant())
1838  {
1839  mp_integer i;
1840  if(!to_integer(to_constant_expr(*it), i))
1841  {
1842  constant+=i;
1843  *it=from_integer(0, it->type());
1844  op_changed = true;
1845  }
1846  }
1847  }
1848 
1849  if(op_changed)
1850  {
1851  // adjust the constant on the RHS
1852  mp_integer i =
1853  numeric_cast_v<mp_integer>(to_constant_expr(new_expr.op1()));
1854  i-=constant;
1855  new_expr.op1() = from_integer(i, new_expr.op1().type());
1856 
1857  new_expr.op0() = simplify_plus(to_plus_expr(new_expr.op0()));
1858  return changed(simplify_inequality(new_expr));
1859  }
1860  }
1861  }
1862 
1863  #if 1
1864  // (double)value REL const ---> value rel const
1865  // if 'const' can be represented exactly.
1866 
1867  if(
1868  expr.op0().id() == ID_typecast && expr.op0().type().id() == ID_floatbv &&
1869  to_typecast_expr(expr.op0()).op().type().id() == ID_floatbv)
1870  {
1871  ieee_floatt const_val(to_constant_expr(expr.op1()));
1872  ieee_floatt const_val_converted=const_val;
1873  const_val_converted.change_spec(ieee_float_spect(
1874  to_floatbv_type(to_typecast_expr(expr.op0()).op().type())));
1875  ieee_floatt const_val_converted_back=const_val_converted;
1876  const_val_converted_back.change_spec(
1878  if(const_val_converted_back==const_val)
1879  {
1880  auto result = expr;
1881  result.op0() = to_typecast_expr(expr.op0()).op();
1882  result.op1()=const_val_converted.to_expr();
1883  return std::move(result);
1884  }
1885  }
1886  #endif
1887 
1888  // is the constant zero?
1889 
1890  if(expr.op1().is_zero())
1891  {
1892  if(expr.id()==ID_ge &&
1893  expr.op0().type().id()==ID_unsignedbv)
1894  {
1895  // zero is always smaller or equal something unsigned
1896  return true_exprt();
1897  }
1898 
1899  auto new_expr = expr;
1900  exprt &operand = new_expr.op0();
1901 
1902  if(expr.id()==ID_equal)
1903  {
1904  // rules below do not hold for >=
1905  if(operand.id()==ID_unary_minus)
1906  {
1907  operand = to_unary_minus_expr(operand).op();
1908  return std::move(new_expr);
1909  }
1910  else if(operand.id()==ID_plus)
1911  {
1912  auto &operand_plus_expr = to_plus_expr(operand);
1913 
1914  // simplify a+-b=0 to a=b
1915  if(operand_plus_expr.operands().size() == 2)
1916  {
1917  // if we have -b+a=0, make that a+(-b)=0
1918  if(operand_plus_expr.op0().id() == ID_unary_minus)
1919  operand_plus_expr.op0().swap(operand_plus_expr.op1());
1920 
1921  if(operand_plus_expr.op1().id() == ID_unary_minus)
1922  {
1923  return binary_exprt(
1924  operand_plus_expr.op0(),
1925  expr.id(),
1926  to_unary_minus_expr(operand_plus_expr.op1()).op(),
1927  expr.type());
1928  }
1929  }
1930  }
1931  }
1932 
1934  {
1935  const exprt &maybe_tc_op = skip_typecast(expr.op0());
1936  if(maybe_tc_op.type().id() == ID_pointer)
1937  {
1938  // make sure none of the type casts lose information
1939  const pointer_typet &p_type = to_pointer_type(maybe_tc_op.type());
1940  bool bitwidth_unchanged = true;
1941  const exprt *ep = &(expr.op0());
1942  while(bitwidth_unchanged && ep->id() == ID_typecast)
1943  {
1944  if(auto t = type_try_dynamic_cast<bitvector_typet>(ep->type()))
1945  {
1946  bitwidth_unchanged = t->get_width() == p_type.get_width();
1947  }
1948  else
1949  bitwidth_unchanged = false;
1950 
1951  ep = &to_typecast_expr(*ep).op();
1952  }
1953 
1954  if(bitwidth_unchanged)
1955  {
1956  if(expr.id() == ID_equal || expr.id() == ID_ge || expr.id() == ID_le)
1957  {
1958  return changed(simplify_rec(
1959  equal_exprt{maybe_tc_op, null_pointer_exprt{p_type}}));
1960  }
1961  else
1962  {
1963  return changed(simplify_rec(
1964  notequal_exprt{maybe_tc_op, null_pointer_exprt{p_type}}));
1965  }
1966  }
1967  }
1968  }
1969  }
1970 
1971  // are we comparing with a typecast from bool?
1972  if(
1973  expr.op0().id() == ID_typecast &&
1974  to_typecast_expr(expr.op0()).op().is_boolean())
1975  {
1976  const auto &lhs_typecast_op = to_typecast_expr(expr.op0()).op();
1977 
1978  // we re-write (TYPE)boolean == 0 -> !boolean
1979  if(expr.op1().is_zero() && expr.id()==ID_equal)
1980  {
1981  return changed(simplify_not(not_exprt(lhs_typecast_op)));
1982  }
1983 
1984  // we re-write (TYPE)boolean != 0 -> boolean
1985  if(expr.op1().is_zero() && expr.id()==ID_notequal)
1986  {
1987  return lhs_typecast_op;
1988  }
1989  }
1990 
1991  #define NORMALISE_CONSTANT_TESTS
1992  #ifdef NORMALISE_CONSTANT_TESTS
1993  // Normalise to >= and = to improve caching and term sharing
1994  if(expr.op0().type().id()==ID_unsignedbv ||
1995  expr.op0().type().id()==ID_signedbv)
1996  {
1998 
1999  if(expr.id()==ID_notequal)
2000  {
2001  auto new_rel_expr = expr;
2002  new_rel_expr.id(ID_equal);
2003  auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
2004  return changed(simplify_not(not_exprt(new_expr)));
2005  }
2006  else if(expr.id()==ID_gt)
2007  {
2008  mp_integer i = numeric_cast_v<mp_integer>(to_constant_expr(expr.op1()));
2009 
2010  if(i==max)
2011  {
2012  return false_exprt();
2013  }
2014 
2015  auto new_expr = expr;
2016  new_expr.id(ID_ge);
2017  ++i;
2018  new_expr.op1() = from_integer(i, new_expr.op1().type());
2019  return changed(simplify_inequality_rhs_is_constant(new_expr));
2020  }
2021  else if(expr.id()==ID_lt)
2022  {
2023  auto new_rel_expr = expr;
2024  new_rel_expr.id(ID_ge);
2025  auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
2026  return changed(simplify_not(not_exprt(new_expr)));
2027  }
2028  else if(expr.id()==ID_le)
2029  {
2030  mp_integer i = numeric_cast_v<mp_integer>(to_constant_expr(expr.op1()));
2031 
2032  if(i==max)
2033  {
2034  return true_exprt();
2035  }
2036 
2037  auto new_rel_expr = expr;
2038  new_rel_expr.id(ID_ge);
2039  ++i;
2040  new_rel_expr.op1() = from_integer(i, new_rel_expr.op1().type());
2041  auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
2042  return changed(simplify_not(not_exprt(new_expr)));
2043  }
2044  }
2045 #endif
2046  return unchanged(expr);
2047 }
2048 
2051 {
2052  auto const_bits_opt = expr2bits(
2053  expr.op(),
2055  ns);
2056 
2057  if(!const_bits_opt.has_value())
2058  return unchanged(expr);
2059 
2060  std::reverse(const_bits_opt->begin(), const_bits_opt->end());
2061 
2062  auto result = bits2expr(
2063  *const_bits_opt,
2064  expr.type(),
2066  ns);
2067  if(!result.has_value())
2068  return unchanged(expr);
2069 
2070  return std::move(*result);
2071 }
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
configt config
Definition: config.cpp:25
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)
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:20
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.
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
API to expression classes for bitvectors.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
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:377
exprt & object()
Definition: pointer_expr.h:549
A base class for binary expressions.
Definition: std_expr.h:638
exprt & op1()
Definition: expr.h:136
exprt & op0()
Definition: expr.h:133
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:762
Bit-wise negation of bit-vectors.
Reverse the order of bits in a bit-vector.
Base class of fixed-width bit-vector types.
Definition: std_types.h:909
void set_width(std::size_t width)
Definition: std_types.h:932
std::size_t get_width() const
Definition: std_types.h:925
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:2990
const irep_idt & get_value() const
Definition: std_expr.h:2998
bool value_is_zero_string() const
Definition: std_expr.cpp:19
void set_value(const irep_idt &value)
Definition: std_expr.h:3003
bool is_null_pointer() const
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Definition: std_expr.cpp:25
Division.
Definition: std_expr.h:1152
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
void swap(dstringt &b)
Definition: dstring.h:162
Equality.
Definition: std_expr.h:1361
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:96
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:27
exprt & op1()
Definition: expr.h:136
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.h:224
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:34
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:47
typet & type()
Return the type of the expression.
Definition: expr.h:84
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.h:212
exprt & op0()
Definition: expr.h:133
operandst & operands()
Definition: expr.h:94
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:170
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:3072
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:703
void negate()
Definition: ieee_float.h:178
void change_spec(const ieee_float_spect &dest_spec)
The trinary if-then-else operator.
Definition: std_expr.h:2370
exprt & true_case()
Definition: std_expr.h:2397
exprt & false_case()
Definition: std_expr.h:2407
mp_integer largest() const
Return the largest value that can be represented using this type.
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:412
bool is_not_nil() const
Definition: irep.h:372
const irep_idt & id() const
Definition: irep.h:388
void swap(irept &irep)
Definition: irep.h:434
const std::string & get_string(const irep_idt &name) const
Definition: irep.h:401
Binary minus.
Definition: std_expr.h:1061
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1223
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1107
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:912
exprt & op1()
Definition: std_expr.h:938
exprt & op0()
Definition: std_expr.h:932
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:2327
Disequality.
Definition: std_expr.h:1420
The null pointer constant.
Definition: pointer_expr.h:909
The plus expression Associativity is not specified.
Definition: std_expr.h:1002
The offset (in bytes) of a pointer relative to the object.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
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()
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_node(const exprt &)
resultt simplify_minus(const minus_exprt &)
resultt simplify_extractbit(const extractbit_exprt &)
resultt simplify_rec(const exprt &)
resultt simplify_shifts(const shift_exprt &)
resultt simplify_typecast(const typecast_exprt &)
resultt simplify_boolean(const exprt &)
resultt simplify_object(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_pointer_offset(const pointer_offset_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_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:3063
Definition: threeval.h:20
static tvt unknown()
Definition: threeval.h:33
Semantic type conversion.
Definition: std_expr.h:2068
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2076
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:391
The unary minus expression.
Definition: std_expr.h:484
The unary plus expression.
Definition: std_expr.h:531
Fixed-width bit-vector with unsigned binary interpretation.
#define Forall_operands(it, expr)
Definition: expr.h:27
#define Forall_expr(it, expr)
Definition: expr.h:36
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Definition: expr_util.cpp:313
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:193
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:177
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Definition: expr_util.cpp:344
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.
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:577
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Pointer Logic.
exprt object_size(const exprt &pointer)
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)
std::optional< std::string > expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
std::optional< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
BigInt mp_integer
Definition: smt_terms.h:17
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
#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:3045
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2102
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:514
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:1086
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1402
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:1041
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:895
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition: std_types.h:952
endiannesst endianness
Definition: config.h:209
bool NULL_is_zero
Definition: config.h:226
#define size_type
Definition: unistd.c:347