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