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