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