CBMC: /home/runner/work/cbmc/cbmc/src/util/simplify_expr_int.cpp Source File

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
9#include "simplify_expr_class.h"
10
11#include "arith_tools.h"
12#include "bitvector_expr.h"
13#include "c_types.h"
14#include "config.h"
15#include "expr_util.h"
16#include "fixedbv.h"
17#include "ieee_float.h"
18#include "invariant.h"
19#include "mathematical_expr.h"
20#include "mathematical_types.h"
21#include "namespace.h"
22#include "pointer_expr.h"
23#include "pointer_offset_size.h"
24#include "rational.h"
25#include "rational_tools.h"
26#include "simplify_utils.h"
27#include "std_expr.h"
28#include "threeval.h"
29
30#include <algorithm>
31
32simplify_exprt::resultt<>
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
67 static bool sum_expr(
68 constant_exprt &dest,
69 const constant_exprt &expr)
70{
71 if(dest.type()!=expr.type())
72 return true;
73
74 const irep_idt &type_id=dest.type().id();
75
76 if(
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
117 static 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 == 0 && it->type().id() != ID_floatbv)
196 {
197 return from_integer(0, expr.type());
198 }
199
200 // true if the given operand has to be erased
201 bool do_erase = false;
202
203 // if this is a constant of the same time as the result
204 if(it->is_constant() && it->type()==expr.type())
205 {
206 // preserve the sizeof type annotation
207 if(!c_sizeof_type.has_value())
208 {
209 const typet &sizeof_type =
210 static_cast<const typet &>(it->find(ID_C_c_sizeof_type));
211 if(sizeof_type.is_not_nil())
213 }
214
216 {
217 // update the constant factor
218 if(!mul_expr(to_constant_expr(*constant), to_constant_expr(*it)))
219 do_erase=true;
220 }
221 else
222 {
223 // set it as the constant factor if this is the first
224 constant=it;
225 constant_found = true;
226 }
227 }
228
229 // erase the factor if necessary
230 if(do_erase)
231 {
232 it = new_operands.erase(it);
233 no_change = false;
234 }
235 else
236 it++; // move to the next operand
237 }
238
239 if(c_sizeof_type.has_value())
240 {
241 INVARIANT(
243 "c_sizeof_type is only set to a non-nil value "
244 "if a constant has been found");
245 constant->set(ID_C_c_sizeof_type, *c_sizeof_type);
246 }
247
248 if(new_operands.size() == 1)
249 {
250 return new_operands.front();
251 }
252 else
253 {
254 // if the constant is a one and there are other factors
255 if(constant_found && *constant == 1)
256 {
257 // just delete it
258 new_operands.erase(constant);
259 no_change = false;
260
261 if(new_operands.size() == 1)
262 return new_operands.front();
263 }
264 }
265
266 if(no_change)
267 return unchanged(expr);
268 else
269 {
270 exprt tmp = expr;
271 tmp.operands() = std::move(new_operands);
272 return std::move(tmp);
273 }
274}
275
277{
278 if(!is_number(expr.type()))
279 return unchanged(expr);
280
281 const typet &expr_type=expr.type();
282
283 if(expr_type!=expr.op0().type() ||
284 expr_type!=expr.op1().type())
285 {
286 return unchanged(expr);
287 }
288
289 if(expr_type.id()==ID_signedbv ||
290 expr_type.id()==ID_unsignedbv ||
291 expr_type.id()==ID_natural ||
292 expr_type.id()==ID_integer)
293 {
294 const auto int_value0 = numeric_cast<mp_integer>(expr.op0());
295 const auto int_value1 = numeric_cast<mp_integer>(expr.op1());
296
297 // division by zero?
298 if(int_value1.has_value() && *int_value1 == 0)
299 return unchanged(expr);
300
301 // x/1?
302 if(int_value1.has_value() && *int_value1 == 1)
303 {
304 return expr.op0();
305 }
306
307 // 0/x?
308 if(int_value0.has_value() && *int_value0 == 0)
309 {
310 return expr.op0();
311 }
312
313 if(int_value0.has_value() && int_value1.has_value())
314 {
315 mp_integer result = *int_value0 / *int_value1;
316 return from_integer(result, expr_type);
317 }
318 }
319 else if(expr_type.id()==ID_rational)
320 {
322 bool ok0, ok1;
323
324 ok0=!to_rational(expr.op0(), rat_value0);
325 ok1=!to_rational(expr.op1(), rat_value1);
326
327 if(ok1 && rat_value1.is_zero())
328 return unchanged(expr);
329
330 if((ok1 && rat_value1.is_one()) ||
331 (ok0 && rat_value0.is_zero()))
332 {
333 return expr.op0();
334 }
335
336 if(ok0 && ok1)
337 {
339 exprt tmp=from_rational(result);
340
341 if(tmp.is_not_nil())
342 return std::move(tmp);
343 }
344 }
345 else if(expr_type.id()==ID_fixedbv)
346 {
347 // division by one?
348 if(expr.op1().is_constant() && expr.op1() == 1)
349 {
350 return expr.op0();
351 }
352
353 if(expr.op0().is_constant() &&
354 expr.op1().is_constant())
355 {
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
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!
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 {
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 {
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 {
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 == 0)
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
571simplify_exprt::resultt<>
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]);
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)"
595
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
608 if(ptr_op0 == ptr_op1 && address_of)
609 {
611 pointer_offset_exprt{operands[0], minus_expr.type()});
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 != 0 &&
625 *object_size &&
628 {
632 }
633 }
634
637 if(
640 {
642 pointer_offset_exprt{operands[0], minus_expr.type()});
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 != 0)
652 {
656 }
657 }
658 }
659
660 return unchanged(expr);
661}
662
663simplify_exprt::resultt<>
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 == 0 || op == 1)
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 if(expr.id() == ID_bitxnor)
698 new_expr.id(ID_equal);
699 else
701
703 {
704 if(it->id()==ID_typecast)
705 *it = to_typecast_expr(*it).op();
706 else if(*it == 0)
707 *it=false_exprt();
708 else if(*it == 1)
709 *it=true_exprt();
710 }
711
712 new_expr.type() = bool_typet{};
714
716 }
717 }
718
719 bool no_change = true;
720 auto new_expr = expr;
721
722 // try to merge constants
723
724 const std::size_t width = to_bitvector_type(expr.type()).get_width();
725
726 while(new_expr.operands().size() >= 2)
727 {
728 if(!new_expr.op0().is_constant())
729 break;
730
731 if(!new_expr.op1().is_constant())
732 break;
733
734 if(new_expr.op0().type() != new_expr.type())
735 break;
736
737 if(new_expr.op1().type() != new_expr.type())
738 break;
739
740 const auto &a_val = to_constant_expr(new_expr.op0()).get_value();
741 const auto &b_val = to_constant_expr(new_expr.op1()).get_value();
742
743 std::function<bool(bool, bool)> f;
744
745 if(new_expr.id() == ID_bitand)
746 f = [](bool a, bool b) { return a && b; };
747 else if(new_expr.id() == ID_bitor)
748 f = [](bool a, bool b) { return a || b; };
749 else if(new_expr.id() == ID_bitxor)
750 f = [](bool a, bool b) { return a != b; };
751 else if(new_expr.id() == ID_bitxnor)
752 f = [](bool a, bool b) { return a == b; };
753 else
755
756 const irep_idt new_value =
757 make_bvrep(width, [&a_val, &b_val, &width, &f](std::size_t i) {
758 return f(
759 get_bvrep_bit(a_val, width, i), get_bvrep_bit(b_val, width, i));
760 });
761
762 constant_exprt new_op(new_value, expr.type());
763
764 // erase first operand
765 new_expr.operands().erase(new_expr.operands().begin());
766 new_expr.op0().swap(new_op);
767
768 no_change = false;
769 }
770
771 // 'all zeros' in bitand yields zero
772 if(new_expr.id() == ID_bitand)
773 {
774 const constant_exprt zero =
775 to_bitvector_type(new_expr.type()).all_zeros_expr();
776 for(const auto &op : new_expr.operands())
777 {
778 if(op == zero)
779 return zero;
780 }
781 }
782
783 // 'all ones' in bitor yields all-ones
784 if(new_expr.id() == ID_bitor)
785 {
787 new_expr.type().id() == ID_bv
788 ? to_bv_type(new_expr.type()).all_ones_expr()
789 : from_integer(power(2, width) - 1, new_expr.type());
790 for(const auto &op : new_expr.operands())
791 {
792 if(op == all_ones)
793 return all_ones;
794 }
795 }
796
797 // now erase 'all zeros' out of bitor, bitxor
798
799 if(new_expr.id() == ID_bitor || new_expr.id() == ID_bitxor)
800 {
801 for(exprt::operandst::iterator it = new_expr.operands().begin();
802 it != new_expr.operands().end();) // no it++
803 {
804 if(*it == 0 && new_expr.operands().size() > 1)
805 {
806 it = new_expr.operands().erase(it);
807 no_change = false;
808 }
809 else if(
810 it->is_constant() && it->type().id() == ID_bv &&
811 *it == to_bv_type(it->type()).all_zeros_expr() &&
812 new_expr.operands().size() > 1)
813 {
814 it = new_expr.operands().erase(it);
815 no_change = false;
816 }
817 else
818 it++;
819 }
820 }
821
822 // now erase 'all ones' out of bitand
823
824 if(new_expr.id() == ID_bitand)
825 {
826 const auto all_ones = power(2, width) - 1;
827 for(exprt::operandst::iterator it = new_expr.operands().begin();
828 it != new_expr.operands().end();) // no it++
829 {
830 if(
831 it->is_constant() &&
832 bvrep2integer(to_constant_expr(*it).get_value(), width, false) ==
833 all_ones &&
834 new_expr.operands().size() > 1)
835 {
836 it = new_expr.operands().erase(it);
837 no_change = false;
838 }
839 else
840 it++;
841 }
842 }
843
844 // two operands that are syntactically the same
845
846 if(new_expr.operands().size() == 2 && new_expr.op0() == new_expr.op1())
847 {
848 if(new_expr.id() == ID_bitand || new_expr.id() == ID_bitor)
849 {
850 return new_expr.op0();
851 }
852 else if(new_expr.id() == ID_bitxor)
853 {
854 return constant_exprt(integer2bvrep(0, width), new_expr.type());
855 }
856 }
857
858 if(new_expr.operands().size() == 1)
859 return new_expr.op0();
860
861 if(no_change)
862 return unchanged(expr);
863 else
864 return std::move(new_expr);
865}
866
867simplify_exprt::resultt<>
869{
870 const typet &src_type = expr.src().type();
871
873 return unchanged(expr);
874
875 const std::size_t src_bit_width = to_bitvector_type(src_type).get_width();
876
878 if(
879 !index_converted_to_int.has_value() || *index_converted_to_int < 0 ||
881 {
882 return unchanged(expr);
883 }
884
885 if(!expr.src().is_constant())
886 return unchanged(expr);
887
888 const bool bit = get_bvrep_bit(
889 to_constant_expr(expr.src()).get_value(),
892
893 return make_boolean_expr(bit);
894}
895
896simplify_exprt::resultt<>
898{
899 bool no_change = true;
900
902
904 {
905 // first, turn bool into bvec[1]
907 {
908 exprt &op=*it;
909 if(op == true || op == false)
910 {
911 const bool value = op == true;
912 op = from_integer(value, unsignedbv_typet(1));
913 no_change = false;
914 }
915 }
916
917 // search for neighboring constants to merge
918 size_t i=0;
919
920 while(i < new_expr.operands().size() - 1)
921 {
922 exprt &opi = new_expr.operands()[i];
923 exprt &opn = new_expr.operands()[i + 1];
924
925 if(
926 opi.is_constant() && opn.is_constant() &&
929 {
930 // merge!
931 const auto &value_i = to_constant_expr(opi).get_value();
932 const auto &value_n = to_constant_expr(opn).get_value();
933 const auto width_i = to_bitvector_type(opi.type()).get_width();
934 const auto width_n = to_bitvector_type(opn.type()).get_width();
935 const auto new_width = width_i + width_n;
936
937 const auto new_value = make_bvrep(
938 new_width, [&value_i, &value_n, width_i, width_n](std::size_t x) {
939 return x < width_n ? get_bvrep_bit(value_n, width_n, x)
941 });
942
943 to_constant_expr(opi).set_value(new_value);
944 to_bitvector_type(opi.type()).set_width(new_width);
945 // erase opn
946 new_expr.operands().erase(new_expr.operands().begin() + i + 1);
947 no_change = false;
948 }
949 else if(
952 {
955
956 if(
957 eb_i.src() == eb_n.src() && eb_i.index().is_constant() &&
958 eb_n.index().is_constant() &&
961 to_bitvector_type(eb_n.type()).get_width())
962 {
964 eb_merged.index() = eb_n.index();
966 .set_width(
967 to_bitvector_type(eb_i.type()).get_width() +
968 to_bitvector_type(eb_n.type()).get_width());
969 if(expr.type().id() != eb_merged.type().id())
970 {
972 bt.set_width(to_bitvector_type(eb_merged.type()).get_width());
974 }
975 else
976 opi = eb_merged;
977 // erase opn
978 new_expr.operands().erase(new_expr.operands().begin() + i + 1);
979 no_change = false;
980 }
981 else
982 ++i;
983 }
984 else
985 i++;
986 }
987 }
988 else if(new_expr.type().id() == ID_verilog_unsignedbv)
989 {
990 // search for neighboring constants to merge
991 size_t i=0;
992
993 while(i < new_expr.operands().size() - 1)
994 {
995 exprt &opi = new_expr.operands()[i];
996 exprt &opn = new_expr.operands()[i + 1];
997
998 if(
999 opi.is_constant() && opn.is_constant() &&
1002 {
1003 // merge!
1004 const std::string new_value=
1005 opi.get_string(ID_value)+opn.get_string(ID_value);
1006 opi.set(ID_value, new_value);
1007 to_bitvector_type(opi.type()).set_width(new_value.size());
1008 opi.type().id(ID_verilog_unsignedbv);
1009 // erase opn
1010 new_expr.operands().erase(new_expr.operands().begin() + i + 1);
1011 no_change = false;
1012 }
1013 else
1014 i++;
1015 }
1016 }
1017
1018 // { x } = x
1019 if(new_expr.operands().size() == 1)
1020 {
1021 if(new_expr.op0().type() == new_expr.type())
1022 return new_expr.op0();
1023 else
1024 {
1025 return changed(
1027 }
1028 }
1029
1030 if(no_change)
1031 return unchanged(expr);
1032 else
1033 return std::move(new_expr);
1034}
1035
1036simplify_exprt::resultt<>
1038{
1040 return unchanged(expr);
1041
1042 if(!can_cast_type<bitvector_typet>(expr.op().type()))
1043 return unchanged(expr);
1044
1045 return changed(simplify_node(expr.lower()));
1046}
1047
1048simplify_exprt::resultt<>
1050{
1052 return unchanged(expr);
1053
1054 const auto distance = numeric_cast<mp_integer>(expr.distance());
1055
1056 if(!distance.has_value())
1057 return unchanged(expr);
1058
1059 if(*distance == 0)
1060 return expr.op();
1061
1062 auto value = numeric_cast<mp_integer>(expr.op());
1063
1064 if(
1065 !value.has_value() && expr.op().type().id() == ID_bv &&
1066 expr.op().is_constant())
1067 {
1068 const std::size_t width = to_bitvector_type(expr.op().type()).get_width();
1069 value =
1070 bvrep2integer(to_constant_expr(expr.op()).get_value(), width, false);
1071 }
1072
1073 if(!value.has_value())
1074 return unchanged(expr);
1075
1076 if(
1077 expr.op().type().id() == ID_unsignedbv ||
1078 expr.op().type().id() == ID_signedbv || expr.op().type().id() == ID_bv)
1079 {
1080 const std::size_t width = to_bitvector_type(expr.op().type()).get_width();
1081
1082 if(expr.id()==ID_lshr)
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 if(*value < 0)
1092 *value += power(2, width);
1093 *value /= power(2, *distance);
1094 return from_integer(*value, expr.type());
1095 }
1096 }
1097 else if(expr.id()==ID_ashr)
1098 {
1099 if(*distance >= 0)
1100 {
1101 // this is to simulate an arithmetic right shift
1102 mp_integer new_value = *value >> *distance;
1103 return from_integer(new_value, expr.type());
1104 }
1105 }
1106 else if(expr.id()==ID_shl)
1107 {
1108 // this is to guard against large values of distance
1109 if(*distance >= width)
1110 {
1111 return from_integer(0, expr.type());
1112 }
1113 else if(*distance >= 0)
1114 {
1115 *value *= power(2, *distance);
1116 return from_integer(*value, expr.type());
1117 }
1118 }
1119 }
1120 else if(
1121 expr.op().type().id() == ID_integer || expr.op().type().id() == ID_natural)
1122 {
1123 if(expr.id()==ID_lshr)
1124 {
1125 if(*distance >= 0)
1126 {
1127 *value /= power(2, *distance);
1128 return from_integer(*value, expr.type());
1129 }
1130 }
1131 else if(expr.id()==ID_ashr)
1132 {
1133 // this is to simulate an arithmetic right shift
1134 if(*distance >= 0)
1135 {
1136 mp_integer new_value = *value / power(2, *distance);
1137 if(*value < 0 && new_value == 0)
1138 new_value=-1;
1139
1140 return from_integer(new_value, expr.type());
1141 }
1142 }
1143 else if(expr.id()==ID_shl)
1144 {
1145 if(*distance >= 0)
1146 {
1147 *value *= power(2, *distance);
1148 return from_integer(*value, expr.type());
1149 }
1150 }
1151 }
1152
1153 return unchanged(expr);
1154}
1155
1156simplify_exprt::resultt<>
1158{
1159 if(!is_number(expr.type()))
1160 return unchanged(expr);
1161
1162 const auto base = numeric_cast<mp_integer>(expr.base());
1163 const auto exponent = numeric_cast<mp_integer>(expr.exponent());
1164
1165 if(!exponent.has_value())
1166 return unchanged(expr);
1167
1168 if(exponent.value() == 0)
1169 return from_integer(1, expr.type());
1170
1171 if(exponent.value() == 1)
1172 return expr.base();
1173
1174 if(!base.has_value())
1175 return unchanged(expr);
1176
1177 mp_integer result = power(*base, *exponent);
1178
1179 return from_integer(result, expr.type());
1180}
1181
1183simplify_exprt::resultt<>
1185{
1186 const typet &op0_type = expr.src().type();
1187
1188 if(
1191 {
1192 return unchanged(expr);
1193 }
1194
1195 const auto end = numeric_cast<mp_integer>(expr.index());
1196
1197 if(!end.has_value())
1198 return unchanged(expr);
1199
1200 const auto width = pointer_offset_bits(op0_type, ns);
1201
1202 if(!width.has_value())
1203 return unchanged(expr);
1204
1205 const auto result_width = pointer_offset_bits(expr.type(), ns);
1206
1207 if(!result_width.has_value())
1208 return unchanged(expr);
1209
1210 const auto start = std::optional(*end + *result_width - 1);
1211
1212 if(*start < 0 || *start >= (*width) || *end < 0 || *end >= (*width))
1213 return unchanged(expr);
1214
1215 DATA_INVARIANT(*start >= *end, "extractbits must have start >= end");
1216
1217 if(expr.src().is_constant())
1218 {
1219 const auto svalue = expr2bits(expr.src(), true, ns);
1220
1221 if(!svalue.has_value() || svalue->size() != *width)
1222 return unchanged(expr);
1223
1224 std::string extracted_value = svalue->substr(
1226 numeric_cast_v<std::size_t>(*start - *end + 1));
1227
1228 auto result = bits2expr(extracted_value, expr.type(), true, ns);
1229 if(!result.has_value())
1230 return unchanged(expr);
1231
1232 return std::move(*result);
1233 }
1234 else if(expr.src().id() == ID_concatenation)
1235 {
1236 // the most-significant bit comes first in an concatenation_exprt, hence we
1237 // count down
1238 mp_integer offset = *width;
1239
1240 for(const auto &op : expr.src().operands())
1241 {
1242 auto op_width = pointer_offset_bits(op.type(), ns);
1243
1244 if(!op_width.has_value() || *op_width <= 0)
1245 return unchanged(expr);
1246
1247 if(*start < offset && offset <= *end + *op_width)
1248 {
1249 extractbits_exprt result = expr;
1250 result.src() = op;
1251 result.index() =
1252 from_integer(*end - (offset - *op_width), expr.index().type());
1253 return changed(simplify_extractbits(result));
1254 }
1255
1256 offset -= *op_width;
1257 }
1258 }
1260 {
1261 if(eb_src->index().is_constant())
1262 {
1263 extractbits_exprt result = *eb_src;
1264 result.type() = expr.type();
1265 const mp_integer src_index =
1267 result.index() = from_integer(src_index + *end, eb_src->index().type());
1268 return changed(simplify_extractbits(result));
1269 }
1270 }
1271 else if(*end == 0 && *start + 1 == *width)
1272 {
1273 typecast_exprt tc{expr.src(), expr.type()};
1274 return changed(simplify_typecast(tc));
1275 }
1276
1277 return unchanged(expr);
1278}
1279
1280simplify_exprt::resultt<>
1282{
1283 // simply remove, this is always 'nop'
1284 return expr.op();
1285}
1286
1287simplify_exprt::resultt<>
1289{
1290 if(!is_number(expr.type()))
1291 return unchanged(expr);
1292
1293 const exprt &operand = expr.op();
1294
1295 if(expr.type()!=operand.type())
1296 return unchanged(expr);
1297
1298 if(operand.id()==ID_unary_minus)
1299 {
1300 // cancel out "-(-x)" to "x"
1301 if(!is_number(to_unary_minus_expr(operand).op().type()))
1302 return unchanged(expr);
1303
1304 return to_unary_minus_expr(operand).op();
1305 }
1306 else if(operand.is_constant())
1307 {
1308 const irep_idt &type_id=expr.type().id();
1309 const auto &constant_expr = to_constant_expr(operand);
1310
1311 if(type_id==ID_integer ||
1314 {
1316
1317 if(!int_value.has_value())
1318 return unchanged(expr);
1319
1320 return from_integer(-*int_value, expr.type());
1321 }
1322 else if(type_id==ID_rational)
1323 {
1324 rationalt r;
1326 return unchanged(expr);
1327
1328 return from_rational(-r);
1329 }
1330 else if(type_id==ID_fixedbv)
1331 {
1333 f.negate();
1334 return f.to_expr();
1335 }
1336 else if(type_id==ID_floatbv)
1337 {
1339 f.negate();
1340 return f.to_expr();
1341 }
1342 }
1343
1344 return unchanged(expr);
1345}
1346
1347simplify_exprt::resultt<>
1349{
1350 const exprt &op = expr.op();
1351
1352 const auto &type = expr.type();
1353
1354 if(
1355 type.id() == ID_bv || type.id() == ID_unsignedbv ||
1356 type.id() == ID_signedbv)
1357 {
1358 const auto width = to_bitvector_type(type).get_width();
1359
1360 if(op.type() == type)
1361 {
1362 if(op.is_constant())
1363 {
1364 const auto &value = to_constant_expr(op).get_value();
1365 const auto new_value =
1366 make_bvrep(width, [&value, &width](std::size_t i) {
1367 return !get_bvrep_bit(value, width, i);
1368 });
1369 return constant_exprt(new_value, op.type());
1370 }
1371 }
1372 }
1373
1374 return unchanged(expr);
1375}
1376
1378simplify_exprt::resultt<>
1380{
1381 if(!expr.is_boolean())
1382 return unchanged(expr);
1383
1384 exprt tmp0=expr.op0();
1385 exprt tmp1=expr.op1();
1386
1387 // types must match
1388 if(tmp0.type() != tmp1.type())
1389 return unchanged(expr);
1390
1391 // if rhs is ID_if (and lhs is not), swap operands for == and !=
1392 if((expr.id()==ID_equal || expr.id()==ID_notequal) &&
1393 tmp0.id()!=ID_if &&
1394 tmp1.id()==ID_if)
1395 {
1396 auto new_expr = expr;
1397 new_expr.op0().swap(new_expr.op1());
1398 return changed(simplify_inequality(new_expr)); // recursive call
1399 }
1400
1401 if(tmp0.id()==ID_if && tmp0.operands().size()==3)
1402 {
1403 if_exprt if_expr=lift_if(expr, 0);
1404 if_expr.true_case() =
1406 if_expr.false_case() =
1408 return changed(simplify_if(if_expr));
1409 }
1410
1411 // see if we are comparing pointers that are address_of
1412 if(
1413 skip_typecast(tmp0).id() == ID_address_of &&
1414 skip_typecast(tmp1).id() == ID_address_of &&
1415 (expr.id() == ID_equal || expr.id() == ID_notequal))
1416 {
1417 return simplify_inequality_address_of(expr);
1418 }
1419
1420 if(tmp0.id()==ID_pointer_object &&
1421 tmp1.id()==ID_pointer_object &&
1422 (expr.id()==ID_equal || expr.id()==ID_notequal))
1423 {
1425 }
1426
1427 if(tmp0.type().id()==ID_c_enum_tag)
1428 tmp0.type()=ns.follow_tag(to_c_enum_tag_type(tmp0.type()));
1429
1430 if(tmp1.type().id()==ID_c_enum_tag)
1431 tmp1.type()=ns.follow_tag(to_c_enum_tag_type(tmp1.type()));
1432
1433 const bool tmp0_const = tmp0.is_constant();
1434 const bool tmp1_const = tmp1.is_constant();
1435
1436 // are _both_ constant?
1437 if(tmp0_const && tmp1_const)
1438 {
1440 }
1441 else if(tmp0_const)
1442 {
1443 // we want the constant on the RHS
1444
1446
1447 if(expr.id()==ID_ge)
1448 new_expr.id(ID_le);
1449 else if(expr.id()==ID_le)
1450 new_expr.id(ID_ge);
1451 else if(expr.id()==ID_gt)
1452 new_expr.id(ID_lt);
1453 else if(expr.id()==ID_lt)
1454 new_expr.id(ID_gt);
1455
1456 new_expr.op0().swap(new_expr.op1());
1457
1458 // RHS is constant, LHS is not
1460 }
1461 else if(tmp1_const)
1462 {
1463 // RHS is constant, LHS is not
1465 }
1466 else
1467 {
1468 // both are not constant
1470 }
1471}
1472
1476 const binary_relation_exprt &expr)
1477{
1478 exprt tmp0 = expr.op0();
1479 exprt tmp1 = expr.op1();
1480
1481 if(tmp0.type().id() == ID_c_enum_tag)
1482 tmp0.type() = ns.follow_tag(to_c_enum_tag_type(tmp0.type()));
1483
1484 if(tmp1.type().id() == ID_c_enum_tag)
1485 tmp1.type() = ns.follow_tag(to_c_enum_tag_type(tmp1.type()));
1486
1487 const auto &tmp0_const = to_constant_expr(tmp0);
1488 const auto &tmp1_const = to_constant_expr(tmp1);
1489
1490 if(expr.id() == ID_equal || expr.id() == ID_notequal)
1491 {
1492 // two constants compare equal when there values (as strings) are the same
1493 // or both of them are pointers and both represent NULL in some way
1494 bool equal = (tmp0_const.get_value() == tmp1_const.get_value());
1495 if(
1496 !equal && tmp0_const.type().id() == ID_pointer &&
1497 tmp1_const.type().id() == ID_pointer)
1498 {
1499 if(
1500 !config.ansi_c.NULL_is_zero && (tmp0_const.get_value() == ID_NULL ||
1501 tmp1_const.get_value() == ID_NULL))
1502 {
1503 // if NULL is not zero on this platform, we really don't know what it
1504 // is and therefore cannot simplify
1505 return unchanged(expr);
1506 }
1507 equal = tmp0_const == 0 && tmp1_const == 0;
1508 }
1509 return make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
1510 }
1511
1512 if(tmp0.type().id() == ID_fixedbv)
1513 {
1515 fixedbvt f1(tmp1_const);
1516
1517 if(expr.id() == ID_ge)
1518 return make_boolean_expr(f0 >= f1);
1519 else if(expr.id() == ID_le)
1520 return make_boolean_expr(f0 <= f1);
1521 else if(expr.id() == ID_gt)
1522 return make_boolean_expr(f0 > f1);
1523 else if(expr.id() == ID_lt)
1524 return make_boolean_expr(f0 < f1);
1525 else
1527 }
1528 else if(tmp0.type().id() == ID_floatbv)
1529 {
1532
1533 if(expr.id() == ID_ge)
1534 return make_boolean_expr(f0 >= f1);
1535 else if(expr.id() == ID_le)
1536 return make_boolean_expr(f0 <= f1);
1537 else if(expr.id() == ID_gt)
1538 return make_boolean_expr(f0 > f1);
1539 else if(expr.id() == ID_lt)
1540 return make_boolean_expr(f0 < f1);
1541 else
1543 }
1544 else if(tmp0.type().id() == ID_rational)
1545 {
1546 rationalt r0, r1;
1547
1548 if(to_rational(tmp0, r0))
1549 return unchanged(expr);
1550
1551 if(to_rational(tmp1, r1))
1552 return unchanged(expr);
1553
1554 if(expr.id() == ID_ge)
1555 return make_boolean_expr(r0 >= r1);
1556 else if(expr.id() == ID_le)
1557 return make_boolean_expr(r0 <= r1);
1558 else if(expr.id() == ID_gt)
1559 return make_boolean_expr(r0 > r1);
1560 else if(expr.id() == ID_lt)
1561 return make_boolean_expr(r0 < r1);
1562 else
1564 }
1565 else
1566 {
1568
1569 if(!v0.has_value())
1570 return unchanged(expr);
1571
1573
1574 if(!v1.has_value())
1575 return unchanged(expr);
1576
1577 if(expr.id() == ID_ge)
1578 return make_boolean_expr(*v0 >= *v1);
1579 else if(expr.id() == ID_le)
1580 return make_boolean_expr(*v0 <= *v1);
1581 else if(expr.id() == ID_gt)
1582 return make_boolean_expr(*v0 > *v1);
1583 else if(expr.id() == ID_lt)
1584 return make_boolean_expr(*v0 < *v1);
1585 else
1587 }
1588}
1589
1590 static bool eliminate_common_addends(exprt &op0, exprt &op1)
1591{
1592 // we can't eliminate zeros
1593 if(
1594 op0 == 0 || op1 == 0 ||
1595 (op0.is_constant() && to_constant_expr(op0).is_null_pointer()) ||
1596 (op1.is_constant() && to_constant_expr(op1).is_null_pointer()))
1597 {
1598 return true;
1599 }
1600
1601 if(op0.id()==ID_plus)
1602 {
1603 bool no_change = true;
1604
1605 Forall_operands(it, op0)
1606 if(!eliminate_common_addends(*it, op1))
1607 no_change = false;
1608
1609 return no_change;
1610 }
1611 else if(op1.id()==ID_plus)
1612 {
1613 bool no_change = true;
1614
1615 Forall_operands(it, op1)
1616 if(!eliminate_common_addends(op0, *it))
1617 no_change = false;
1618
1619 return no_change;
1620 }
1621 else if(op0==op1)
1622 {
1623 if(op0 != 0 && op0.type().id() != ID_complex)
1624 {
1625 // elimination!
1626 op0=from_integer(0, op0.type());
1627 op1=from_integer(0, op1.type());
1628 return false;
1629 }
1630 }
1631
1632 return true;
1633}
1634
1636 const binary_relation_exprt &expr)
1637{
1638 // pretty much all of the simplifications below are unsound
1639 // for IEEE float because of NaN!
1640
1641 if(expr.op0().type().id() == ID_floatbv)
1642 return unchanged(expr);
1643
1644 if(expr.op0().type().id() == ID_pointer)
1645 {
1648
1649 if(ptr_op0 == ptr_op1)
1650 {
1653
1655 std::move(offset_op0), expr.id(), std::move(offset_op1)}));
1656 }
1657 // simplifications below require same-object, which we don't check for
1658 else if(expr.id() != ID_equal && expr.id() != ID_notequal)
1659 {
1660 return unchanged(expr);
1661 }
1662 else if(
1663 expr.id() == ID_equal && ptr_op0.id() == ID_address_of &&
1664 ptr_op1.id() == ID_address_of)
1665 {
1666 // comparing pointers: if both are address-of-plus-some-constant such that
1667 // the resulting pointer remains within object bounds then they can never
1668 // be equal
1669 auto in_bounds = [this](const exprt &object_ptr, const exprt &expr_op) {
1670 auto object_size =
1671 size_of_expr(to_address_of_expr(object_ptr).object().type(), ns);
1672
1673 if(object_size.has_value())
1674 {
1678 std::move(offset), ID_lt, std::move(*object_size)})
1679 .expr;
1680 if(in_object_bounds.is_constant())
1681 return tvt{in_object_bounds == true};
1682 }
1683
1684 return tvt::unknown();
1685 };
1686
1687 if(
1688 in_bounds(ptr_op0, expr.op0()).is_true() &&
1689 in_bounds(ptr_op1, expr.op1()).is_true())
1690 {
1691 return false_exprt{};
1692 }
1693 }
1694 }
1695
1696 // eliminate strict inequalities
1697 if(expr.id()==ID_notequal)
1698 {
1699 auto new_rel_expr = expr;
1703 }
1704 else if(expr.id()==ID_gt)
1705 {
1706 auto new_rel_expr = expr;
1707 new_rel_expr.id(ID_ge);
1708 // swap operands
1709 new_rel_expr.lhs().swap(new_rel_expr.rhs());
1712 }
1713 else if(expr.id()==ID_lt)
1714 {
1715 auto new_rel_expr = expr;
1716 new_rel_expr.id(ID_ge);
1719 }
1720 else if(expr.id()==ID_le)
1721 {
1722 auto new_rel_expr = expr;
1723 new_rel_expr.id(ID_ge);
1724 // swap operands
1725 new_rel_expr.lhs().swap(new_rel_expr.rhs());
1727 }
1728
1729 // now we only have >=, =
1730
1731 INVARIANT(
1732 expr.id() == ID_ge || expr.id() == ID_equal,
1733 "we previously converted all other cases to >= or ==");
1734
1735 // syntactically equal?
1736
1737 if(expr.op0() == expr.op1())
1738 return true_exprt();
1739
1740 // See if we can eliminate common addends on both sides.
1741 // On bit-vectors, this is only sound on '='.
1742 if(expr.id()==ID_equal)
1743 {
1744 auto new_expr = to_equal_expr(expr);
1745 if(!eliminate_common_addends(new_expr.lhs(), new_expr.rhs()))
1746 {
1747 // remove zeros
1748 new_expr.lhs() = simplify_node(new_expr.lhs());
1749 new_expr.rhs() = simplify_node(new_expr.rhs());
1750 return changed(simplify_inequality(new_expr)); // recursive call
1751 }
1752 }
1753
1754 return unchanged(expr);
1755}
1756
1760 const binary_relation_exprt &expr)
1761{
1762 // the constant is always on the RHS
1763 PRECONDITION(expr.op1().is_constant());
1764
1765 if(expr.op0().id()==ID_if && expr.op0().operands().size()==3)
1766 {
1767 if_exprt if_expr=lift_if(expr, 0);
1768 if_expr.true_case() =
1770 if_expr.false_case() =
1772 return changed(simplify_if(if_expr));
1773 }
1774
1775 // do we deal with pointers?
1776 if(expr.op1().type().id()==ID_pointer)
1777 {
1778 if(expr.id()==ID_notequal)
1779 {
1780 auto new_rel_expr = expr;
1784 }
1785
1786 // very special case for pointers
1787 if(expr.id() != ID_equal)
1788 return unchanged(expr);
1789
1791
1792 if(op1_constant.is_null_pointer())
1793 {
1794 // the address of an object is never NULL
1795
1796 if(expr.op0().id() == ID_address_of)
1797 {
1798 const auto &object = to_address_of_expr(expr.op0()).object();
1799
1800 if(
1801 object.id() == ID_symbol || object.id() == ID_dynamic_object ||
1802 object.id() == ID_member || object.id() == ID_index ||
1803 object.id() == ID_string_constant)
1804 {
1805 return false_exprt();
1806 }
1807 }
1808 else if(
1809 expr.op0().id() == ID_typecast &&
1810 expr.op0().type().id() == ID_pointer &&
1811 to_typecast_expr(expr.op0()).op().id() == ID_address_of)
1812 {
1813 const auto &object =
1814 to_address_of_expr(to_typecast_expr(expr.op0()).op()).object();
1815
1816 if(
1817 object.id() == ID_symbol || object.id() == ID_dynamic_object ||
1818 object.id() == ID_member || object.id() == ID_index ||
1819 object.id() == ID_string_constant)
1820 {
1821 return false_exprt();
1822 }
1823 }
1824 else if(
1825 expr.op0().id() == ID_typecast && expr.op0().type().id() == ID_pointer)
1826 {
1827 exprt op = to_typecast_expr(expr.op0()).op();
1828 if(
1829 op.type().id() != ID_pointer &&
1830 (!config.ansi_c.NULL_is_zero || !is_number(op.type()) ||
1831 op.type().id() == ID_complex))
1832 {
1833 return unchanged(expr);
1834 }
1835
1836 // (type)ptr == NULL -> ptr == NULL
1837 // note that 'ptr' may be an integer
1838 auto new_expr = expr;
1839 new_expr.op0().swap(op);
1840 if(new_expr.op0().type().id() != ID_pointer)
1841 new_expr.op1() = from_integer(0, new_expr.op0().type());
1842 else
1843 new_expr.op1().type() = new_expr.op0().type();
1844 return changed(simplify_inequality(new_expr)); // do again!
1845 }
1846 else if(expr.op0().id() == ID_plus)
1847 {
1848 exprt offset =
1850 if(!offset.is_constant())
1851 return unchanged(expr);
1852
1853 exprt ptr = simplify_object(expr.op0()).expr;
1854 // NULL + N == NULL is N == 0
1855 if(ptr.is_constant() && to_constant_expr(ptr).is_null_pointer())
1856 return make_boolean_expr(offset == 0);
1857 // &x + N == NULL is false when the offset is in bounds
1859 {
1860 const auto object_size =
1861 pointer_offset_size(address_of->object().type(), ns);
1862 if(
1863 object_size.has_value() &&
1865 {
1866 return false_exprt();
1867 }
1868 }
1869 }
1870 }
1871
1872 // all we are doing with pointers
1873 return unchanged(expr);
1874 }
1875
1876 // is it a separation predicate?
1877
1878 if(expr.op0().id()==ID_plus)
1879 {
1880 // see if there is a constant in the sum
1881
1882 if(expr.id()==ID_equal || expr.id()==ID_notequal)
1883 {
1884 mp_integer constant=0;
1885 bool op_changed = false;
1886 auto new_expr = expr;
1887
1888 Forall_operands(it, new_expr.op0())
1889 {
1890 if(it->is_constant())
1891 {
1892 mp_integer i;
1893 if(!to_integer(to_constant_expr(*it), i))
1894 {
1895 constant+=i;
1896 *it=from_integer(0, it->type());
1897 op_changed = true;
1898 }
1899 }
1900 }
1901
1902 if(op_changed)
1903 {
1904 // adjust the constant on the RHS
1905 mp_integer i =
1907 i-=constant;
1908 new_expr.op1() = from_integer(i, new_expr.op1().type());
1909
1912 }
1913 }
1914 }
1915
1916 #if 1
1917 // (double)value REL const ---> value rel const
1918 // if 'const' can be represented exactly.
1919
1920 if(
1921 expr.op0().id() == ID_typecast && expr.op0().type().id() == ID_floatbv &&
1922 to_typecast_expr(expr.op0()).op().type().id() == ID_floatbv)
1923 {
1928 to_floatbv_type(to_typecast_expr(expr.op0()).op().type())));
1930 const_val_converted_back.change_spec(
1933 {
1934 auto result = expr;
1935 result.op0() = to_typecast_expr(expr.op0()).op();
1936 result.op1()=const_val_converted.to_expr();
1937 return std::move(result);
1938 }
1939 }
1940 #endif
1941
1942 // is the constant zero?
1943
1944 if(expr.op1() == 0)
1945 {
1946 if(expr.id()==ID_ge &&
1947 expr.op0().type().id()==ID_unsignedbv)
1948 {
1949 // zero is always smaller or equal something unsigned
1950 return true_exprt();
1951 }
1952
1953 auto new_expr = expr;
1954 exprt &operand = new_expr.op0();
1955
1956 if(expr.id()==ID_equal)
1957 {
1958 // rules below do not hold for >=
1959 if(operand.id()==ID_unary_minus)
1960 {
1962 return std::move(new_expr);
1963 }
1964 else if(operand.id()==ID_plus)
1965 {
1967
1968 // simplify a+-b=0 to a=b
1969 if(operand_plus_expr.operands().size() == 2)
1970 {
1971 // if we have -b+a=0, make that a+(-b)=0
1972 if(operand_plus_expr.op0().id() == ID_unary_minus)
1973 operand_plus_expr.op0().swap(operand_plus_expr.op1());
1974
1975 if(operand_plus_expr.op1().id() == ID_unary_minus)
1976 {
1977 return binary_exprt(
1978 operand_plus_expr.op0(),
1979 expr.id(),
1981 expr.type());
1982 }
1983 }
1984 }
1985 }
1986
1987 if(config.ansi_c.NULL_is_zero)
1988 {
1989 const exprt &maybe_tc_op = skip_typecast(expr.op0());
1990 if(maybe_tc_op.type().id() == ID_pointer)
1991 {
1992 // make sure none of the type casts lose information
1994 bool bitwidth_unchanged = true;
1995 const exprt *ep = &(expr.op0());
1996 while(bitwidth_unchanged && ep->id() == ID_typecast)
1997 {
1998 if(auto t = type_try_dynamic_cast<bitvector_typet>(ep->type()))
1999 {
2000 bitwidth_unchanged = t->get_width() == p_type.get_width();
2001 }
2002 else
2003 bitwidth_unchanged = false;
2004
2005 ep = &to_typecast_expr(*ep).op();
2006 }
2007
2009 {
2010 if(expr.id() == ID_equal || expr.id() == ID_ge || expr.id() == ID_le)
2011 {
2012 return changed(simplify_rec(
2014 }
2015 else
2016 {
2017 return changed(simplify_rec(
2019 }
2020 }
2021 }
2022 }
2023 }
2024
2025 // are we comparing with a typecast from bool?
2026 if(
2027 expr.op0().id() == ID_typecast &&
2028 to_typecast_expr(expr.op0()).op().is_boolean())
2029 {
2030 const auto &lhs_typecast_op = to_typecast_expr(expr.op0()).op();
2031
2032 // we re-write (TYPE)boolean == 0 -> !boolean
2033 if(expr.op1() == 0 && expr.id() == ID_equal)
2034 {
2036 }
2037
2038 // we re-write (TYPE)boolean != 0 -> boolean
2039 if(expr.op1() == 0 && expr.id() == ID_notequal)
2040 {
2041 return lhs_typecast_op;
2042 }
2043 }
2044
2045 #define NORMALISE_CONSTANT_TESTS
2046 #ifdef NORMALISE_CONSTANT_TESTS
2047 // Normalise to >= and = to improve caching and term sharing
2048 if(expr.op0().type().id()==ID_unsignedbv ||
2049 expr.op0().type().id()==ID_signedbv)
2050 {
2051 mp_integer max(to_integer_bitvector_type(expr.op0().type()).largest());
2052
2053 if(expr.id()==ID_notequal)
2054 {
2055 auto new_rel_expr = expr;
2059 }
2060 else if(expr.id()==ID_gt)
2061 {
2063
2064 if(i==max)
2065 {
2066 return false_exprt();
2067 }
2068
2069 auto new_expr = expr;
2070 new_expr.id(ID_ge);
2071 ++i;
2072 new_expr.op1() = from_integer(i, new_expr.op1().type());
2074 }
2075 else if(expr.id()==ID_lt)
2076 {
2077 auto new_rel_expr = expr;
2078 new_rel_expr.id(ID_ge);
2081 }
2082 else if(expr.id()==ID_le)
2083 {
2085
2086 if(i==max)
2087 {
2088 return true_exprt();
2089 }
2090
2091 auto new_rel_expr = expr;
2092 new_rel_expr.id(ID_ge);
2093 ++i;
2094 new_rel_expr.op1() = from_integer(i, new_rel_expr.op1().type());
2097 }
2098 }
2099#endif
2100 return unchanged(expr);
2101}
2102
2103simplify_exprt::resultt<>
2105{
2107 expr.op(),
2109 ns);
2110
2111 if(!const_bits_opt.has_value())
2112 return unchanged(expr);
2113
2114 std::reverse(const_bits_opt->begin(), const_bits_opt->end());
2115
2116 auto result = bits2expr(
2118 expr.type(),
2120 ns);
2121 if(!result.has_value())
2122 return unchanged(expr);
2123
2124 return std::move(*result);
2125}
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
configt config
Definition config.cpp:25
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
irep_idt make_bvrep(const std::size_t width, const std::function< bool(std::size_t)> f)
construct a bit-vector representation from a functor
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition arith_tools.cpp:21
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 bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
const 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:566
A base class for binary expressions.
Definition std_expr.h:649
exprt & op0()
Definition expr.h:134
exprt & op1()
Definition expr.h:137
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:784
Bit-wise negation of bit-vectors.
Reverse the order of bits in a bit-vector.
Base class of fixed-width bit-vector types.
The Boolean type.
Definition std_types.h:35
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:3007
Division.
Definition std_expr.h:1152
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Equality.
Definition std_expr.h:1339
Base class for all expressions.
Definition expr.h:57
std::vector< exprt > operandst
Definition expr.h:59
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:229
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:213
typet & type()
Return the type of the expression.
Definition expr.h:85
operandst & operands()
Definition expr.h:95
Extracts a single bit of a bit-vector operand.
exprt & index()
exprt & src()
Extracts a sub-range of a bit-vector operand.
exprt & index()
exprt & src()
The Boolean constant false.
Definition std_expr.h:3135
void negate()
Definition fixedbv.cpp:90
bool is_zero() const
Definition fixedbv.h:71
constant_exprt to_expr() const
Definition fixedbv.cpp:43
Definition ieee_float.h:22
An IEEE 754 floating-point value, including specificiation.
Definition ieee_float.h:117
constant_exprt to_expr() const
Definition ieee_float.cpp:579
void negate()
Definition ieee_float.h:155
An IEEE 754 value plus a rounding mode, enabling operations with rounding on values.
Definition ieee_float.h:369
@ ROUND_TO_EVEN
Definition ieee_float.h:379
The trinary if-then-else operator.
Definition std_expr.h:2426
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
Binary minus.
Definition std_expr.h:1065
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1216
Binary multiplication Associativity is not specified.
Definition std_expr.h:1104
A base class for multi-ary expressions Associativity is not specified.
Definition std_expr.h:908
exprt & op1()
Definition std_expr.h:942
exprt & op0()
Definition std_expr.h:936
Boolean negation.
Definition std_expr.h:2388
Disequality.
Definition std_expr.h:1393
The null pointer constant.
Definition pointer_expr.h:909
The plus expression Associativity is not specified.
Definition std_expr.h:1006
The offset (in bytes) of a pointer relative to the object.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition pointer_expr.h:24
Exponentiation.
const exprt & base() const
const exprt & exponent() const
A base class for shift and rotate operators.
exprt & distance()
exprt & op()
resultt simplify_bitwise(const multi_ary_exprt &)
const namespacet & ns
resultt simplify_inequality_address_of(const binary_relation_exprt &)
resultt simplify_div(const div_exprt &)
resultt simplify_bitreverse(const bitreverse_exprt &)
Try to simplify bit-reversing to a constant expression.
resultt simplify_bitnot(const bitnot_exprt &)
resultt simplify_zero_extend(const zero_extend_exprt &)
static resultt changed(resultt<> result)
resultt simplify_if(const if_exprt &)
resultt simplify_node(const exprt &)
resultt simplify_minus(const minus_exprt &)
resultt simplify_extractbit(const extractbit_exprt &)
resultt simplify_rec(const exprt &)
resultt simplify_shifts(const shift_exprt &)
resultt simplify_typecast(const typecast_exprt &)
resultt simplify_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:3126
Definition threeval.h:20
static tvt unknown()
Definition threeval.h:33
Semantic type conversion.
Definition std_expr.h:1995
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2003
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:394
The unary minus expression.
Definition std_expr.h:477
The unary plus expression.
Definition std_expr.h:519
Fixed-width bit-vector with unsigned binary interpretation.
zero extension The operand is converted to the given type by either a) truncating if the new type is ...
exprt lower() const
#define Forall_operands(it, expr)
Definition expr.h:28
#define Forall_expr(it, expr)
Definition expr.h:37
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Definition expr_util.cpp:308
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition expr_util.cpp:188
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition expr_util.cpp:172
Deprecated expression utility functions.
r
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.
Definition pointer_expr.h:577
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition pointer_expr.h:93
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:828
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2024
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:1045
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition std_expr.h:1085
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3078
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition std_expr.h:502
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition std_expr.h:1375
@ IS_LITTLE_ENDIAN
T expr
#define size_type
Definition unistd.c:186

AltStyle によって変換されたページ (->オリジナル) /