cprover
Loading...
Searching...
No Matches
simplify_expr_int.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
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 =
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 {
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
67static 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
116static 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 {
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() &&
625 *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
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
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(
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
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() &&
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(
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
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(
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 =
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 {
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
1427 }
1428 else if(tmp1_const)
1429 {
1430 // RHS is constant, LHS is not
1432 }
1433 else
1434 {
1435 // both are not constant
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
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
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
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
1554 }
1555}
1556
1557static 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()) ||
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() &&
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 =
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(
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 {
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 {
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());
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 {
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)
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
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.
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
std::optional< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
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 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 floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
unsignedbv_typet size_type()
Definition c_types.cpp:50
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
A base class for binary expressions.
Definition std_expr.h:638
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
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:2995
const irep_idt & get_value() const
Definition std_expr.h:3003
bool value_is_zero_string() const
Definition std_expr.cpp:19
void set_value(const irep_idt &value)
Definition std_expr.h:3008
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
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
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
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:3077
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
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:2375
exprt & false_case()
Definition std_expr.h:2412
exprt & true_case()
Definition std_expr.h:2402
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
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
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:2332
Disequality.
Definition std_expr.h:1425
The null pointer constant.
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 ...
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()
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:3068
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 ...
#define Forall_operands(it, expr)
Definition expr.h:27
#define Forall_expr(it, expr)
Definition expr.h:36
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
Definition expr_cast.h:135
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
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...
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 address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
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.
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)
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< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
std::optional< std::string > expr2bits(const exprt &expr, 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
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
API to expression classes.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition std_expr.h:895
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:1041
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition std_expr.h:1086
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3050
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 equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition std_expr.h:1407
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