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