cprover
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
30{
31 if(expr.type().id() == ID_unsignedbv && expr.op().is_constant())
32 {
33 auto bits_per_byte = expr.get_bits_per_byte();
34 std::size_t width=to_bitvector_type(expr.type()).get_width();
35 const mp_integer value =
36 numeric_cast_v<mp_integer>(to_constant_expr(expr.op()));
37 std::vector<mp_integer> bytes;
38
39 // take apart
40 for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
41 bytes.push_back((value >> bit)%power(2, bits_per_byte));
42
43 // put back together, but backwards
44 mp_integer new_value=0;
45 for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
46 {
48 !bytes.empty(),
49 "bytes is not empty because we just pushed just as many elements on "
50 "top of it as we are popping now");
51 new_value+=bytes.back()<<bit;
52 bytes.pop_back();
53 }
54
55 return from_integer(new_value, expr.type());
56 }
57
58 return unchanged(expr);
59}
60
63static bool sum_expr(
64 constant_exprt &dest,
65 const constant_exprt &expr)
66{
67 if(dest.type()!=expr.type())
68 return true;
69
70 const irep_idt &type_id=dest.type().id();
71
72 if(
73 type_id == ID_integer || type_id == ID_natural ||
74 type_id == ID_unsignedbv || type_id == ID_signedbv)
75 {
76 mp_integer a, b;
77 if(!to_integer(dest, a) && !to_integer(expr, b))
78 {
79 dest = from_integer(a + b, dest.type());
80 return false;
81 }
82 }
83 else if(type_id==ID_rational)
84 {
85 rationalt a, b;
86 if(!to_rational(dest, a) && !to_rational(expr, b))
87 {
88 dest=from_rational(a+b);
89 return false;
90 }
91 }
92 else if(type_id==ID_fixedbv)
93 {
94 fixedbvt f(dest);
95 f += fixedbvt(expr);
96 dest = f.to_expr();
97 return false;
98 }
99 else if(type_id==ID_floatbv)
100 {
101 ieee_floatt f(dest);
102 f += ieee_floatt(expr);
103 dest=f.to_expr();
104 return false;
105 }
106
107 return true;
108}
109
112static bool mul_expr(
113 constant_exprt &dest,
114 const constant_exprt &expr)
115{
116 if(dest.type()!=expr.type())
117 return true;
118
119 const irep_idt &type_id=dest.type().id();
120
121 if(
122 type_id == ID_integer || type_id == ID_natural ||
123 type_id == ID_unsignedbv || type_id == ID_signedbv)
124 {
125 mp_integer a, b;
126 if(!to_integer(dest, a) && !to_integer(expr, b))
127 {
128 dest = from_integer(a * b, dest.type());
129 return false;
130 }
131 }
132 else if(type_id==ID_rational)
133 {
134 rationalt a, b;
135 if(!to_rational(dest, a) && !to_rational(expr, b))
136 {
137 dest=from_rational(a*b);
138 return false;
139 }
140 }
141 else if(type_id==ID_fixedbv)
142 {
143 fixedbvt f(to_constant_expr(dest));
144 f*=fixedbvt(to_constant_expr(expr));
145 dest=f.to_expr();
146 return false;
147 }
148 else if(type_id==ID_floatbv)
149 {
152 dest=f.to_expr();
153 return false;
154 }
155
156 return true;
157}
158
160{
161 // check to see if it is a number type
162 if(!is_number(expr.type()))
163 return unchanged(expr);
164
165 // vector of operands
166 exprt::operandst new_operands = expr.operands();
167
168 // result of the simplification
169 bool no_change = true;
170
171 // position of the constant
172 exprt::operandst::iterator constant;
173
174 // true if we have found a constant
175 bool constant_found = false;
176
177 optionalt<typet> c_sizeof_type;
178
179 // scan all the operands
180 for(exprt::operandst::iterator it = new_operands.begin();
181 it != new_operands.end();)
182 {
183 // if one of the operands is not a number return
184 if(!is_number(it->type()))
185 return unchanged(expr);
186
187 // if one of the operands is zero the result is zero
188 // note: not true on IEEE floating point arithmetic
189 if(it->is_zero() &&
190 it->type().id()!=ID_floatbv)
191 {
192 return from_integer(0, expr.type());
193 }
194
195 // true if the given operand has to be erased
196 bool do_erase = false;
197
198 // if this is a constant of the same time as the result
199 if(it->is_constant() && it->type()==expr.type())
200 {
201 // preserve the sizeof type annotation
202 if(!c_sizeof_type.has_value())
203 {
204 const typet &sizeof_type =
205 static_cast<const typet &>(it->find(ID_C_c_sizeof_type));
206 if(sizeof_type.is_not_nil())
207 c_sizeof_type = sizeof_type;
208 }
209
210 if(constant_found)
211 {
212 // update the constant factor
213 if(!mul_expr(to_constant_expr(*constant), to_constant_expr(*it)))
214 do_erase=true;
215 }
216 else
217 {
218 // set it as the constant factor if this is the first
219 constant=it;
220 constant_found = true;
221 }
222 }
223
224 // erase the factor if necessary
225 if(do_erase)
226 {
227 it = new_operands.erase(it);
228 no_change = false;
229 }
230 else
231 it++; // move to the next operand
232 }
233
234 if(c_sizeof_type.has_value())
235 {
236 INVARIANT(
237 constant_found,
238 "c_sizeof_type is only set to a non-nil value "
239 "if a constant has been found");
240 constant->set(ID_C_c_sizeof_type, *c_sizeof_type);
241 }
242
243 if(new_operands.size() == 1)
244 {
245 return new_operands.front();
246 }
247 else
248 {
249 // if the constant is a one and there are other factors
250 if(constant_found && constant->is_one())
251 {
252 // just delete it
253 new_operands.erase(constant);
254 no_change = false;
255
256 if(new_operands.size() == 1)
257 return new_operands.front();
258 }
259 }
260
261 if(no_change)
262 return unchanged(expr);
263 else
264 {
265 exprt tmp = expr;
266 tmp.operands() = std::move(new_operands);
267 return std::move(tmp);
268 }
269}
270
272{
273 if(!is_number(expr.type()))
274 return unchanged(expr);
275
276 const typet &expr_type=expr.type();
277
278 if(expr_type!=expr.op0().type() ||
279 expr_type!=expr.op1().type())
280 {
281 return unchanged(expr);
282 }
283
284 if(expr_type.id()==ID_signedbv ||
285 expr_type.id()==ID_unsignedbv ||
286 expr_type.id()==ID_natural ||
287 expr_type.id()==ID_integer)
288 {
289 const auto int_value0 = numeric_cast<mp_integer>(expr.op0());
290 const auto int_value1 = numeric_cast<mp_integer>(expr.op1());
291
292 // division by zero?
293 if(int_value1.has_value() && *int_value1 == 0)
294 return unchanged(expr);
295
296 // x/1?
297 if(int_value1.has_value() && *int_value1 == 1)
298 {
299 return expr.op0();
300 }
301
302 // 0/x?
303 if(int_value0.has_value() && *int_value0 == 0)
304 {
305 return expr.op0();
306 }
307
308 if(int_value0.has_value() && int_value1.has_value())
309 {
310 mp_integer result = *int_value0 / *int_value1;
311 return from_integer(result, expr_type);
312 }
313 }
314 else if(expr_type.id()==ID_rational)
315 {
316 rationalt rat_value0, rat_value1;
317 bool ok0, ok1;
318
319 ok0=!to_rational(expr.op0(), rat_value0);
320 ok1=!to_rational(expr.op1(), rat_value1);
321
322 if(ok1 && rat_value1.is_zero())
323 return unchanged(expr);
324
325 if((ok1 && rat_value1.is_one()) ||
326 (ok0 && rat_value0.is_zero()))
327 {
328 return expr.op0();
329 }
330
331 if(ok0 && ok1)
332 {
333 rationalt result=rat_value0/rat_value1;
334 exprt tmp=from_rational(result);
335
336 if(tmp.is_not_nil())
337 return std::move(tmp);
338 }
339 }
340 else if(expr_type.id()==ID_fixedbv)
341 {
342 // division by one?
343 if(expr.op1().is_constant() &&
344 expr.op1().is_one())
345 {
346 return expr.op0();
347 }
348
349 if(expr.op0().is_constant() &&
350 expr.op1().is_constant())
351 {
352 fixedbvt f0(to_constant_expr(expr.op0()));
353 fixedbvt f1(to_constant_expr(expr.op1()));
354 if(!f1.is_zero())
355 {
356 f0/=f1;
357 return f0.to_expr();
358 }
359 }
360 }
361
362 return unchanged(expr);
363}
364
366{
367 if(!is_number(expr.type()))
368 return unchanged(expr);
369
370 if(expr.type().id()==ID_signedbv ||
371 expr.type().id()==ID_unsignedbv ||
372 expr.type().id()==ID_natural ||
373 expr.type().id()==ID_integer)
374 {
375 if(expr.type()==expr.op0().type() &&
376 expr.type()==expr.op1().type())
377 {
378 const auto int_value0 = numeric_cast<mp_integer>(expr.op0());
379 const auto int_value1 = numeric_cast<mp_integer>(expr.op1());
380
381 if(int_value1.has_value() && *int_value1 == 0)
382 return unchanged(expr); // division by zero
383
384 if(
385 (int_value1.has_value() && *int_value1 == 1) ||
386 (int_value0.has_value() && *int_value0 == 0))
387 {
388 return from_integer(0, expr.type());
389 }
390
391 if(int_value0.has_value() && int_value1.has_value())
392 {
393 mp_integer result = *int_value0 % *int_value1;
394 return from_integer(result, expr.type());
395 }
396 }
397 }
398
399 return unchanged(expr);
400}
401
403{
404 if(!is_number(expr.type()) && expr.type().id() != ID_pointer)
405 return unchanged(expr);
406
407 bool no_change = true;
408
409 exprt::operandst new_operands = expr.operands();
410
411 // floating-point addition is _NOT_ associative; thus,
412 // there is special case for float
413
414 if(expr.type().id() == ID_floatbv)
415 {
416 // we only merge neighboring constants!
417 Forall_expr(it, new_operands)
418 {
419 const exprt::operandst::iterator next = std::next(it);
420
421 if(next != new_operands.end())
422 {
423 if(it->type()==next->type() &&
424 it->is_constant() &&
425 next->is_constant())
426 {
428 new_operands.erase(next);
429 no_change = false;
430 }
431 }
432 }
433 }
434 else
435 {
436 // ((T*)p+a)+b -> (T*)p+(a+b)
437 if(
438 expr.type().id() == ID_pointer && expr.operands().size() == 2 &&
439 expr.op0().id() == ID_plus && expr.op0().type().id() == ID_pointer &&
440 expr.op0().operands().size() == 2)
441 {
442 plus_exprt op0 = to_plus_expr(expr.op0());
443
444 if(op0.op1().id() == ID_plus)
445 to_plus_expr(op0.op1()).add_to_operands(expr.op1());
446 else
447 op0.op1()=plus_exprt(op0.op1(), expr.op1());
448
449 auto result = op0;
450
451 result.op1() = simplify_plus(to_plus_expr(result.op1()));
452
453 return changed(simplify_plus(result));
454 }
455
456 // count the constants
457 size_t count=0;
458 forall_operands(it, expr)
459 if(is_number(it->type()) && it->is_constant())
460 count++;
461
462 // merge constants?
463 if(count>=2)
464 {
465 exprt::operandst::iterator const_sum;
466 bool const_sum_set=false;
467
468 for(auto it = new_operands.begin(); it != new_operands.end(); it++)
469 {
470 if(is_number(it->type()) && it->is_constant())
471 {
472 if(!const_sum_set)
473 {
474 const_sum=it;
475 const_sum_set=true;
476 }
477 else
478 {
479 if(!sum_expr(to_constant_expr(*const_sum),
480 to_constant_expr(*it)))
481 {
482 *it=from_integer(0, it->type());
483 no_change = false;
484 }
485 }
486 }
487 }
488 }
489
490 // search for a and -a
491 // first gather all the a's with -a
492 typedef std::unordered_map<exprt, exprt::operandst::iterator, irep_hash>
493 expr_mapt;
494 expr_mapt expr_map;
495
496 for(auto it = new_operands.begin(); it != new_operands.end(); it++)
497 if(it->id() == ID_unary_minus)
498 {
499 expr_map.insert(std::make_pair(to_unary_minus_expr(*it).op(), it));
500 }
501
502 // now search for a
503 for(auto it = new_operands.begin(); it != new_operands.end(); it++)
504 {
505 if(expr_map.empty())
506 break;
507 else if(it->id()==ID_unary_minus)
508 continue;
509
510 expr_mapt::iterator itm=expr_map.find(*it);
511
512 if(itm!=expr_map.end())
513 {
514 *(itm->second)=from_integer(0, expr.type());
515 *it=from_integer(0, expr.type());
516 expr_map.erase(itm);
517 no_change = false;
518 }
519 }
520
521 // delete zeros
522 // (can't do for floats, as the result of 0.0 + (-0.0)
523 // need not be -0.0 in std rounding)
524 for(exprt::operandst::iterator it = new_operands.begin();
525 it != new_operands.end();
526 /* no it++ */)
527 {
528 if(is_number(it->type()) && it->is_zero())
529 {
530 it = new_operands.erase(it);
531 no_change = false;
532 }
533 else
534 it++;
535 }
536 }
537
538 if(new_operands.empty())
539 {
540 return from_integer(0, expr.type());
541 }
542 else if(new_operands.size() == 1)
543 {
544 return new_operands.front();
545 }
546
547 if(no_change)
548 return unchanged(expr);
549 else
550 {
551 auto tmp = expr;
552 tmp.operands() = std::move(new_operands);
553 return std::move(tmp);
554 }
555}
556
559{
560 auto const &minus_expr = to_minus_expr(expr);
561 if(!is_number(minus_expr.type()) && minus_expr.type().id() != ID_pointer)
562 return unchanged(expr);
563
564 const exprt::operandst &operands = minus_expr.operands();
565
566 if(
567 is_number(minus_expr.type()) && is_number(operands[0].type()) &&
568 is_number(operands[1].type()))
569 {
570 // rewrite "a-b" to "a+(-b)"
571 unary_minus_exprt rhs_negated(operands[1]);
572 plus_exprt plus_expr(operands[0], simplify_unary_minus(rhs_negated));
573 return changed(simplify_plus(plus_expr));
574 }
575 else if(
576 minus_expr.type().id() == ID_pointer &&
577 operands[0].type().id() == ID_pointer && is_number(operands[1].type()))
578 {
579 // pointer arithmetic: rewrite "p-i" to "p+(-i)"
580 unary_minus_exprt negated_pointer_offset(operands[1]);
581
582 plus_exprt pointer_offset_expr(
583 operands[0], simplify_unary_minus(negated_pointer_offset));
584 return changed(simplify_plus(pointer_offset_expr));
585 }
586 else if(
587 is_number(minus_expr.type()) && operands[0].type().id() == ID_pointer &&
588 operands[1].type().id() == ID_pointer)
589 {
590 // pointer arithmetic: rewrite "p-p" to "0"
591
592 if(operands[0]==operands[1])
593 return from_integer(0, minus_expr.type());
594 }
595
596 return unchanged(expr);
597}
598
601{
602 if(!is_bitvector_type(expr.type()))
603 return unchanged(expr);
604
605 // check if these are really boolean
606 if(expr.type().id()!=ID_bool)
607 {
608 bool all_bool=true;
609
610 forall_operands(it, expr)
611 {
612 if(
613 it->id() == ID_typecast &&
614 to_typecast_expr(*it).op().type().id() == ID_bool)
615 {
616 }
617 else if(it->is_zero() || it->is_one())
618 {
619 }
620 else
621 all_bool=false;
622 }
623
624 if(all_bool)
625 {
626 // re-write to boolean+typecast
627 exprt new_expr=expr;
628
629 if(expr.id()==ID_bitand)
630 new_expr.id(ID_and);
631 else if(expr.id()==ID_bitor)
632 new_expr.id(ID_or);
633 else if(expr.id()==ID_bitxor)
634 new_expr.id(ID_xor);
635 else
637
638 Forall_operands(it, new_expr)
639 {
640 if(it->id()==ID_typecast)
641 *it = to_typecast_expr(*it).op();
642 else if(it->is_zero())
643 *it=false_exprt();
644 else if(it->is_one())
645 *it=true_exprt();
646 }
647
648 new_expr.type()=bool_typet();
649 new_expr = simplify_boolean(new_expr);
650
651 return changed(simplify_typecast(typecast_exprt(new_expr, expr.type())));
652 }
653 }
654
655 bool no_change = true;
656 auto new_expr = expr;
657
658 // try to merge constants
659
660 const std::size_t width = to_bitvector_type(expr.type()).get_width();
661
662 while(new_expr.operands().size() >= 2)
663 {
664 if(!new_expr.op0().is_constant())
665 break;
666
667 if(!new_expr.op1().is_constant())
668 break;
669
670 if(new_expr.op0().type() != new_expr.type())
671 break;
672
673 if(new_expr.op1().type() != new_expr.type())
674 break;
675
676 const auto &a_val = to_constant_expr(new_expr.op0()).get_value();
677 const auto &b_val = to_constant_expr(new_expr.op1()).get_value();
678
679 std::function<bool(bool, bool)> f;
680
681 if(new_expr.id() == ID_bitand)
682 f = [](bool a, bool b) { return a && b; };
683 else if(new_expr.id() == ID_bitor)
684 f = [](bool a, bool b) { return a || b; };
685 else if(new_expr.id() == ID_bitxor)
686 f = [](bool a, bool b) { return a != b; };
687 else
689
690 const irep_idt new_value =
691 make_bvrep(width, [&a_val, &b_val, &width, &f](std::size_t i) {
692 return f(
693 get_bvrep_bit(a_val, width, i), get_bvrep_bit(b_val, width, i));
694 });
695
696 constant_exprt new_op(new_value, expr.type());
697
698 // erase first operand
699 new_expr.operands().erase(new_expr.operands().begin());
700 new_expr.op0().swap(new_op);
701
702 no_change = false;
703 }
704
705 // now erase 'all zeros' out of bitor, bitxor
706
707 if(new_expr.id() == ID_bitor || new_expr.id() == ID_bitxor)
708 {
709 for(exprt::operandst::iterator it = new_expr.operands().begin();
710 it != new_expr.operands().end();) // no it++
711 {
712 if(it->is_zero() && new_expr.operands().size() > 1)
713 {
714 it = new_expr.operands().erase(it);
715 no_change = false;
716 }
717 else if(
718 it->is_constant() && it->type().id() == ID_bv &&
720 new_expr.operands().size() > 1)
721 {
722 it = new_expr.operands().erase(it);
723 no_change = false;
724 }
725 else
726 it++;
727 }
728 }
729
730 // now erase 'all ones' out of bitand
731
732 if(new_expr.id() == ID_bitand)
733 {
734 const auto all_ones = power(2, width) - 1;
735 for(exprt::operandst::iterator it = new_expr.operands().begin();
736 it != new_expr.operands().end();) // no it++
737 {
738 if(
739 it->is_constant() &&
740 bvrep2integer(to_constant_expr(*it).get_value(), width, false) ==
741 all_ones &&
742 new_expr.operands().size() > 1)
743 {
744 it = new_expr.operands().erase(it);
745 no_change = false;
746 }
747 else
748 it++;
749 }
750 }
751
752 // two operands that are syntactically the same
753
754 if(new_expr.operands().size() == 2 && new_expr.op0() == new_expr.op1())
755 {
756 if(new_expr.id() == ID_bitand || new_expr.id() == ID_bitor)
757 {
758 return new_expr.op0();
759 }
760 else if(new_expr.id() == ID_bitxor)
761 {
762 return constant_exprt(integer2bvrep(0, width), new_expr.type());
763 }
764 }
765
766 if(new_expr.operands().size() == 1)
767 return new_expr.op0();
768
769 if(no_change)
770 return unchanged(expr);
771 else
772 return std::move(new_expr);
773}
774
777{
778 const typet &src_type = expr.src().type();
779
780 if(!is_bitvector_type(src_type))
781 return unchanged(expr);
782
783 const std::size_t src_bit_width = to_bitvector_type(src_type).get_width();
784
785 const auto index_converted_to_int = numeric_cast<mp_integer>(expr.index());
786 if(
787 !index_converted_to_int.has_value() || *index_converted_to_int < 0 ||
788 *index_converted_to_int >= src_bit_width)
789 {
790 return unchanged(expr);
791 }
792
793 if(!expr.src().is_constant())
794 return unchanged(expr);
795
796 const bool bit = get_bvrep_bit(
798 src_bit_width,
799 numeric_cast_v<std::size_t>(*index_converted_to_int));
800
801 return make_boolean_expr(bit);
802}
803
806{
807 bool no_change = true;
808
809 concatenation_exprt new_expr = expr;
810
811 if(is_bitvector_type(new_expr.type()))
812 {
813 // first, turn bool into bvec[1]
814 Forall_operands(it, new_expr)
815 {
816 exprt &op=*it;
817 if(op.is_true() || op.is_false())
818 {
819 const bool value = op.is_true();
820 op = from_integer(value, unsignedbv_typet(1));
821 no_change = false;
822 }
823 }
824
825 // search for neighboring constants to merge
826 size_t i=0;
827
828 while(i < new_expr.operands().size() - 1)
829 {
830 exprt &opi = new_expr.operands()[i];
831 exprt &opn = new_expr.operands()[i + 1];
832
833 if(opi.is_constant() &&
834 opn.is_constant() &&
835 is_bitvector_type(opi.type()) &&
836 is_bitvector_type(opn.type()))
837 {
838 // merge!
839 const auto &value_i = to_constant_expr(opi).get_value();
840 const auto &value_n = to_constant_expr(opn).get_value();
841 const auto width_i = to_bitvector_type(opi.type()).get_width();
842 const auto width_n = to_bitvector_type(opn.type()).get_width();
843 const auto new_width = width_i + width_n;
844
845 const auto new_value = make_bvrep(
846 new_width, [&value_i, &value_n, width_i, width_n](std::size_t x) {
847 return x < width_n ? get_bvrep_bit(value_n, width_n, x)
848 : get_bvrep_bit(value_i, width_i, x - width_n);
849 });
850
851 to_constant_expr(opi).set_value(new_value);
852 to_bitvector_type(opi.type()).set_width(new_width);
853 // erase opn
854 new_expr.operands().erase(new_expr.operands().begin() + i + 1);
855 no_change = false;
856 }
857 else
858 i++;
859 }
860 }
861 else if(new_expr.type().id() == ID_verilog_unsignedbv)
862 {
863 // search for neighboring constants to merge
864 size_t i=0;
865
866 while(i < new_expr.operands().size() - 1)
867 {
868 exprt &opi = new_expr.operands()[i];
869 exprt &opn = new_expr.operands()[i + 1];
870
871 if(opi.is_constant() &&
872 opn.is_constant() &&
873 (opi.type().id()==ID_verilog_unsignedbv ||
874 is_bitvector_type(opi.type())) &&
875 (opn.type().id()==ID_verilog_unsignedbv ||
876 is_bitvector_type(opn.type())))
877 {
878 // merge!
879 const std::string new_value=
880 opi.get_string(ID_value)+opn.get_string(ID_value);
881 opi.set(ID_value, new_value);
882 to_bitvector_type(opi.type()).set_width(new_value.size());
883 opi.type().id(ID_verilog_unsignedbv);
884 // erase opn
885 new_expr.operands().erase(new_expr.operands().begin() + i + 1);
886 no_change = false;
887 }
888 else
889 i++;
890 }
891 }
892
893 // { x } = x
894 if(
895 new_expr.operands().size() == 1 && new_expr.op0().type() == new_expr.type())
896 {
897 return new_expr.op0();
898 }
899
900 if(no_change)
901 return unchanged(expr);
902 else
903 return std::move(new_expr);
904}
905
908{
909 if(!is_bitvector_type(expr.type()))
910 return unchanged(expr);
911
912 const auto distance = numeric_cast<mp_integer>(expr.distance());
913
914 if(!distance.has_value())
915 return unchanged(expr);
916
917 if(*distance == 0)
918 return expr.op();
919
920 auto value = numeric_cast<mp_integer>(expr.op());
921
922 if(
923 !value.has_value() && expr.op().type().id() == ID_bv &&
924 expr.op().id() == ID_constant)
925 {
926 const std::size_t width = to_bitvector_type(expr.op().type()).get_width();
927 value =
928 bvrep2integer(to_constant_expr(expr.op()).get_value(), width, false);
929 }
930
931 if(!value.has_value())
932 return unchanged(expr);
933
934 if(
935 expr.op().type().id() == ID_unsignedbv ||
936 expr.op().type().id() == ID_signedbv || expr.op().type().id() == ID_bv)
937 {
938 const std::size_t width = to_bitvector_type(expr.op().type()).get_width();
939
940 if(expr.id()==ID_lshr)
941 {
942 // this is to guard against large values of distance
943 if(*distance >= width)
944 {
945 return from_integer(0, expr.type());
946 }
947 else if(*distance >= 0)
948 {
949 if(*value < 0)
950 *value += power(2, width);
951 *value /= power(2, *distance);
952 return from_integer(*value, expr.type());
953 }
954 }
955 else if(expr.id()==ID_ashr)
956 {
957 if(*distance >= 0)
958 {
959 // this is to simulate an arithmetic right shift
960 mp_integer new_value = *value >> *distance;
961 return from_integer(new_value, expr.type());
962 }
963 }
964 else if(expr.id()==ID_shl)
965 {
966 // this is to guard against large values of distance
967 if(*distance >= width)
968 {
969 return from_integer(0, expr.type());
970 }
971 else if(*distance >= 0)
972 {
973 *value *= power(2, *distance);
974 return from_integer(*value, expr.type());
975 }
976 }
977 }
978 else if(
979 expr.op().type().id() == ID_integer || expr.op().type().id() == ID_natural)
980 {
981 if(expr.id()==ID_lshr)
982 {
983 if(*distance >= 0)
984 {
985 *value /= power(2, *distance);
986 return from_integer(*value, expr.type());
987 }
988 }
989 else if(expr.id()==ID_ashr)
990 {
991 // this is to simulate an arithmetic right shift
992 if(*distance >= 0)
993 {
994 mp_integer new_value = *value / power(2, *distance);
995 if(*value < 0 && new_value == 0)
996 new_value=-1;
997
998 return from_integer(new_value, expr.type());
999 }
1000 }
1001 else if(expr.id()==ID_shl)
1002 {
1003 if(*distance >= 0)
1004 {
1005 *value *= power(2, *distance);
1006 return from_integer(*value, expr.type());
1007 }
1008 }
1009 }
1010
1011 return unchanged(expr);
1012}
1013
1016{
1017 if(!is_number(expr.type()))
1018 return unchanged(expr);
1019
1020 const auto base = numeric_cast<mp_integer>(expr.op0());
1021 const auto exponent = numeric_cast<mp_integer>(expr.op1());
1022
1023 if(!base.has_value())
1024 return unchanged(expr);
1025
1026 if(!exponent.has_value())
1027 return unchanged(expr);
1028
1029 mp_integer result = power(*base, *exponent);
1030
1031 return from_integer(result, expr.type());
1032}
1033
1037{
1038 const typet &op0_type = expr.src().type();
1039
1040 if(!is_bitvector_type(op0_type) &&
1041 !is_bitvector_type(expr.type()))
1042 {
1043 return unchanged(expr);
1044 }
1045
1046 const auto start = numeric_cast<mp_integer>(expr.upper());
1047 const auto end = numeric_cast<mp_integer>(expr.lower());
1048
1049 if(!start.has_value())
1050 return unchanged(expr);
1051
1052 if(!end.has_value())
1053 return unchanged(expr);
1054
1055 const auto width = pointer_offset_bits(op0_type, ns);
1056
1057 if(!width.has_value())
1058 return unchanged(expr);
1059
1060 if(*start < 0 || *start >= (*width) || *end < 0 || *end >= (*width))
1061 return unchanged(expr);
1062
1063 DATA_INVARIANT(*start >= *end, "extractbits must have upper() >= lower()");
1064
1065 if(expr.src().is_constant())
1066 {
1067 const auto svalue = expr2bits(expr.src(), true, ns);
1068
1069 if(!svalue.has_value() || svalue->size() != *width)
1070 return unchanged(expr);
1071
1072 std::string extracted_value = svalue->substr(
1073 numeric_cast_v<std::size_t>(*end),
1074 numeric_cast_v<std::size_t>(*start - *end + 1));
1075
1076 auto result = bits2expr(extracted_value, expr.type(), true, ns);
1077 if(!result.has_value())
1078 return unchanged(expr);
1079
1080 return std::move(*result);
1081 }
1082 else if(expr.src().id() == ID_concatenation)
1083 {
1084 // the most-significant bit comes first in an concatenation_exprt, hence we
1085 // count down
1086 mp_integer offset = *width;
1087
1088 forall_operands(it, expr.src())
1089 {
1090 auto op_width = pointer_offset_bits(it->type(), ns);
1091
1092 if(!op_width.has_value() || *op_width <= 0)
1093 return unchanged(expr);
1094
1095 if(*start + 1 == offset && *end + *op_width == offset)
1096 {
1097 exprt tmp = *it;
1098 if(tmp.type() != expr.type())
1099 return unchanged(expr);
1100
1101 return std::move(tmp);
1102 }
1103
1104 offset -= *op_width;
1105 }
1106 }
1107
1108 return unchanged(expr);
1109}
1110
1113{
1114 // simply remove, this is always 'nop'
1115 return expr.op();
1116}
1117
1120{
1121 if(!is_number(expr.type()))
1122 return unchanged(expr);
1123
1124 const exprt &operand = expr.op();
1125
1126 if(expr.type()!=operand.type())
1127 return unchanged(expr);
1128
1129 if(operand.id()==ID_unary_minus)
1130 {
1131 // cancel out "-(-x)" to "x"
1132 if(!is_number(to_unary_minus_expr(operand).op().type()))
1133 return unchanged(expr);
1134
1135 return to_unary_minus_expr(operand).op();
1136 }
1137 else if(operand.id()==ID_constant)
1138 {
1139 const irep_idt &type_id=expr.type().id();
1140 const auto &constant_expr = to_constant_expr(operand);
1141
1142 if(type_id==ID_integer ||
1143 type_id==ID_signedbv ||
1144 type_id==ID_unsignedbv)
1145 {
1146 const auto int_value = numeric_cast<mp_integer>(constant_expr);
1147
1148 if(!int_value.has_value())
1149 return unchanged(expr);
1150
1151 return from_integer(-*int_value, expr.type());
1152 }
1153 else if(type_id==ID_rational)
1154 {
1155 rationalt r;
1156 if(to_rational(constant_expr, r))
1157 return unchanged(expr);
1158
1159 return from_rational(-r);
1160 }
1161 else if(type_id==ID_fixedbv)
1162 {
1163 fixedbvt f(constant_expr);
1164 f.negate();
1165 return f.to_expr();
1166 }
1167 else if(type_id==ID_floatbv)
1168 {
1169 ieee_floatt f(constant_expr);
1170 f.negate();
1171 return f.to_expr();
1172 }
1173 }
1174
1175 return unchanged(expr);
1176}
1177
1180{
1181 const exprt &op = expr.op();
1182
1183 const auto &type = expr.type();
1184
1185 if(
1186 type.id() == ID_bv || type.id() == ID_unsignedbv ||
1187 type.id() == ID_signedbv)
1188 {
1189 const auto width = to_bitvector_type(type).get_width();
1190
1191 if(op.type() == type)
1192 {
1193 if(op.id()==ID_constant)
1194 {
1195 const auto &value = to_constant_expr(op).get_value();
1196 const auto new_value =
1197 make_bvrep(width, [&value, &width](std::size_t i) {
1198 return !get_bvrep_bit(value, width, i);
1199 });
1200 return constant_exprt(new_value, op.type());
1201 }
1202 }
1203 }
1204
1205 return unchanged(expr);
1206}
1207
1211{
1212 if(expr.type().id()!=ID_bool)
1213 return unchanged(expr);
1214
1215 exprt tmp0=expr.op0();
1216 exprt tmp1=expr.op1();
1217
1218 // types must match
1219 if(tmp0.type() != tmp1.type())
1220 return unchanged(expr);
1221
1222 // if rhs is ID_if (and lhs is not), swap operands for == and !=
1223 if((expr.id()==ID_equal || expr.id()==ID_notequal) &&
1224 tmp0.id()!=ID_if &&
1225 tmp1.id()==ID_if)
1226 {
1227 auto new_expr = expr;
1228 new_expr.op0().swap(new_expr.op1());
1229 return changed(simplify_inequality(new_expr)); // recursive call
1230 }
1231
1232 if(tmp0.id()==ID_if && tmp0.operands().size()==3)
1233 {
1234 if_exprt if_expr=lift_if(expr, 0);
1235 if_expr.true_case() =
1237 if_expr.false_case() =
1239 return changed(simplify_if(if_expr));
1240 }
1241
1242 // see if we are comparing pointers that are address_of
1243 if(
1244 skip_typecast(tmp0).id() == ID_address_of &&
1245 skip_typecast(tmp1).id() == ID_address_of &&
1246 (expr.id() == ID_equal || expr.id() == ID_notequal))
1247 {
1248 return simplify_inequality_address_of(expr);
1249 }
1250
1251 if(tmp0.id()==ID_pointer_object &&
1252 tmp1.id()==ID_pointer_object &&
1253 (expr.id()==ID_equal || expr.id()==ID_notequal))
1254 {
1256 }
1257
1258 if(tmp0.type().id()==ID_c_enum_tag)
1259 tmp0.type()=ns.follow_tag(to_c_enum_tag_type(tmp0.type()));
1260
1261 if(tmp1.type().id()==ID_c_enum_tag)
1262 tmp1.type()=ns.follow_tag(to_c_enum_tag_type(tmp1.type()));
1263
1264 const bool tmp0_const = tmp0.is_constant();
1265 const bool tmp1_const = tmp1.is_constant();
1266
1267 // are _both_ constant?
1268 if(tmp0_const && tmp1_const)
1269 {
1271 }
1272 else if(tmp0_const)
1273 {
1274 // we want the constant on the RHS
1275
1276 binary_relation_exprt new_expr = expr;
1277
1278 if(expr.id()==ID_ge)
1279 new_expr.id(ID_le);
1280 else if(expr.id()==ID_le)
1281 new_expr.id(ID_ge);
1282 else if(expr.id()==ID_gt)
1283 new_expr.id(ID_lt);
1284 else if(expr.id()==ID_lt)
1285 new_expr.id(ID_gt);
1286
1287 new_expr.op0().swap(new_expr.op1());
1288
1289 // RHS is constant, LHS is not
1291 }
1292 else if(tmp1_const)
1293 {
1294 // RHS is constant, LHS is not
1296 }
1297 else
1298 {
1299 // both are not constant
1301 }
1302}
1303
1307 const binary_relation_exprt &expr)
1308{
1309 exprt tmp0 = expr.op0();
1310 exprt tmp1 = expr.op1();
1311
1312 if(tmp0.type().id() == ID_c_enum_tag)
1313 tmp0.type() = ns.follow_tag(to_c_enum_tag_type(tmp0.type()));
1314
1315 if(tmp1.type().id() == ID_c_enum_tag)
1316 tmp1.type() = ns.follow_tag(to_c_enum_tag_type(tmp1.type()));
1317
1318 const auto &tmp0_const = to_constant_expr(tmp0);
1319 const auto &tmp1_const = to_constant_expr(tmp1);
1320
1321 if(expr.id() == ID_equal || expr.id() == ID_notequal)
1322 {
1323 // two constants compare equal when there values (as strings) are the same
1324 // or both of them are pointers and both represent NULL in some way
1325 bool equal = (tmp0_const.get_value() == tmp1_const.get_value());
1326 if(
1327 !equal && tmp0_const.type().id() == ID_pointer &&
1328 tmp1_const.type().id() == ID_pointer)
1329 {
1330 if(
1331 !config.ansi_c.NULL_is_zero && (tmp0_const.get_value() == ID_NULL ||
1332 tmp1_const.get_value() == ID_NULL))
1333 {
1334 // if NULL is not zero on this platform, we really don't know what it
1335 // is and therefore cannot simplify
1336 return unchanged(expr);
1337 }
1338 equal = tmp0_const.is_zero() && tmp1_const.is_zero();
1339 }
1340 return make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
1341 }
1342
1343 if(tmp0.type().id() == ID_fixedbv)
1344 {
1345 fixedbvt f0(tmp0_const);
1346 fixedbvt f1(tmp1_const);
1347
1348 if(expr.id() == ID_ge)
1349 return make_boolean_expr(f0 >= f1);
1350 else if(expr.id() == ID_le)
1351 return make_boolean_expr(f0 <= f1);
1352 else if(expr.id() == ID_gt)
1353 return make_boolean_expr(f0 > f1);
1354 else if(expr.id() == ID_lt)
1355 return make_boolean_expr(f0 < f1);
1356 else
1358 }
1359 else if(tmp0.type().id() == ID_floatbv)
1360 {
1361 ieee_floatt f0(tmp0_const);
1362 ieee_floatt f1(tmp1_const);
1363
1364 if(expr.id() == ID_ge)
1365 return make_boolean_expr(f0 >= f1);
1366 else if(expr.id() == ID_le)
1367 return make_boolean_expr(f0 <= f1);
1368 else if(expr.id() == ID_gt)
1369 return make_boolean_expr(f0 > f1);
1370 else if(expr.id() == ID_lt)
1371 return make_boolean_expr(f0 < f1);
1372 else
1374 }
1375 else if(tmp0.type().id() == ID_rational)
1376 {
1377 rationalt r0, r1;
1378
1379 if(to_rational(tmp0, r0))
1380 return unchanged(expr);
1381
1382 if(to_rational(tmp1, r1))
1383 return unchanged(expr);
1384
1385 if(expr.id() == ID_ge)
1386 return make_boolean_expr(r0 >= r1);
1387 else if(expr.id() == ID_le)
1388 return make_boolean_expr(r0 <= r1);
1389 else if(expr.id() == ID_gt)
1390 return make_boolean_expr(r0 > r1);
1391 else if(expr.id() == ID_lt)
1392 return make_boolean_expr(r0 < r1);
1393 else
1395 }
1396 else
1397 {
1398 const auto v0 = numeric_cast<mp_integer>(tmp0_const);
1399
1400 if(!v0.has_value())
1401 return unchanged(expr);
1402
1403 const auto v1 = numeric_cast<mp_integer>(tmp1_const);
1404
1405 if(!v1.has_value())
1406 return unchanged(expr);
1407
1408 if(expr.id() == ID_ge)
1409 return make_boolean_expr(*v0 >= *v1);
1410 else if(expr.id() == ID_le)
1411 return make_boolean_expr(*v0 <= *v1);
1412 else if(expr.id() == ID_gt)
1413 return make_boolean_expr(*v0 > *v1);
1414 else if(expr.id() == ID_lt)
1415 return make_boolean_expr(*v0 < *v1);
1416 else
1418 }
1419}
1420
1421static bool eliminate_common_addends(exprt &op0, exprt &op1)
1422{
1423 // we can't eliminate zeros
1424 if(op0.is_zero() ||
1425 op1.is_zero() ||
1426 (op0.is_constant() &&
1427 to_constant_expr(op0).get_value()==ID_NULL) ||
1428 (op1.is_constant() &&
1429 to_constant_expr(op1).get_value()==ID_NULL))
1430 return true;
1431
1432 if(op0.id()==ID_plus)
1433 {
1434 bool no_change = true;
1435
1436 Forall_operands(it, op0)
1437 if(!eliminate_common_addends(*it, op1))
1438 no_change = false;
1439
1440 return no_change;
1441 }
1442 else if(op1.id()==ID_plus)
1443 {
1444 bool no_change = true;
1445
1446 Forall_operands(it, op1)
1447 if(!eliminate_common_addends(op0, *it))
1448 no_change = false;
1449
1450 return no_change;
1451 }
1452 else if(op0==op1)
1453 {
1454 if(!op0.is_zero() &&
1455 op0.type().id()!=ID_complex)
1456 {
1457 // elimination!
1458 op0=from_integer(0, op0.type());
1459 op1=from_integer(0, op1.type());
1460 return false;
1461 }
1462 }
1463
1464 return true;
1465}
1466
1468 const binary_relation_exprt &expr)
1469{
1470 // pretty much all of the simplifications below are unsound
1471 // for IEEE float because of NaN!
1472
1473 if(expr.op0().type().id() == ID_floatbv)
1474 return unchanged(expr);
1475
1476 // simplifications below require same-object, which we don't check for
1477 if(
1478 expr.op0().type().id() == ID_pointer && expr.id() != ID_equal &&
1479 expr.id() != ID_notequal)
1480 {
1481 return unchanged(expr);
1482 }
1483
1484 // eliminate strict inequalities
1485 if(expr.id()==ID_notequal)
1486 {
1487 auto new_rel_expr = expr;
1488 new_rel_expr.id(ID_equal);
1489 auto new_expr = simplify_inequality_no_constant(new_rel_expr);
1490 return changed(simplify_not(not_exprt(new_expr)));
1491 }
1492 else if(expr.id()==ID_gt)
1493 {
1494 auto new_rel_expr = expr;
1495 new_rel_expr.id(ID_ge);
1496 // swap operands
1497 new_rel_expr.lhs().swap(new_rel_expr.rhs());
1498 auto new_expr = simplify_inequality_no_constant(new_rel_expr);
1499 return changed(simplify_not(not_exprt(new_expr)));
1500 }
1501 else if(expr.id()==ID_lt)
1502 {
1503 auto new_rel_expr = expr;
1504 new_rel_expr.id(ID_ge);
1505 auto new_expr = simplify_inequality_no_constant(new_rel_expr);
1506 return changed(simplify_not(not_exprt(new_expr)));
1507 }
1508 else if(expr.id()==ID_le)
1509 {
1510 auto new_rel_expr = expr;
1511 new_rel_expr.id(ID_ge);
1512 // swap operands
1513 new_rel_expr.lhs().swap(new_rel_expr.rhs());
1514 return changed(simplify_inequality_no_constant(new_rel_expr));
1515 }
1516
1517 // now we only have >=, =
1518
1519 INVARIANT(
1520 expr.id() == ID_ge || expr.id() == ID_equal,
1521 "we previously converted all other cases to >= or ==");
1522
1523 // syntactically equal?
1524
1525 if(expr.op0() == expr.op1())
1526 return true_exprt();
1527
1528 // See if we can eliminate common addends on both sides.
1529 // On bit-vectors, this is only sound on '='.
1530 if(expr.id()==ID_equal)
1531 {
1532 auto new_expr = to_equal_expr(expr);
1533 if(!eliminate_common_addends(new_expr.lhs(), new_expr.rhs()))
1534 {
1535 // remove zeros
1536 new_expr.lhs() = simplify_node(new_expr.lhs());
1537 new_expr.rhs() = simplify_node(new_expr.rhs());
1538 return changed(simplify_inequality(new_expr)); // recursive call
1539 }
1540 }
1541
1542 return unchanged(expr);
1543}
1544
1548 const binary_relation_exprt &expr)
1549{
1550 // the constant is always on the RHS
1551 PRECONDITION(expr.op1().is_constant());
1552
1553 if(expr.op0().id()==ID_if && expr.op0().operands().size()==3)
1554 {
1555 if_exprt if_expr=lift_if(expr, 0);
1556 if_expr.true_case() =
1558 if_expr.false_case() =
1560 return changed(simplify_if(if_expr));
1561 }
1562
1563 // do we deal with pointers?
1564 if(expr.op1().type().id()==ID_pointer)
1565 {
1566 if(expr.id()==ID_notequal)
1567 {
1568 auto new_rel_expr = expr;
1569 new_rel_expr.id(ID_equal);
1570 auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
1571 return changed(simplify_not(not_exprt(new_expr)));
1572 }
1573
1574 // very special case for pointers
1575 if(expr.id()==ID_equal &&
1576 expr.op1().is_constant() &&
1577 expr.op1().get(ID_value)==ID_NULL)
1578 {
1579 // the address of an object is never NULL
1580
1581 if(expr.op0().id() == ID_address_of)
1582 {
1583 const auto &object = to_address_of_expr(expr.op0()).object();
1584
1585 if(
1586 object.id() == ID_symbol || object.id() == ID_dynamic_object ||
1587 object.id() == ID_member || object.id() == ID_index ||
1588 object.id() == ID_string_constant)
1589 {
1590 return false_exprt();
1591 }
1592 }
1593 else if(
1594 expr.op0().id() == ID_typecast &&
1595 expr.op0().type().id() == ID_pointer &&
1596 to_typecast_expr(expr.op0()).op().id() == ID_address_of)
1597 {
1598 const auto &object =
1600
1601 if(
1602 object.id() == ID_symbol || object.id() == ID_dynamic_object ||
1603 object.id() == ID_member || object.id() == ID_index ||
1604 object.id() == ID_string_constant)
1605 {
1606 return false_exprt();
1607 }
1608 }
1609 else if(
1610 expr.op0().id() == ID_typecast && expr.op0().type().id() == ID_pointer)
1611 {
1612 exprt op = to_typecast_expr(expr.op0()).op();
1613 if(
1614 op.type().id() != ID_pointer &&
1615 (!config.ansi_c.NULL_is_zero || !is_number(op.type()) ||
1616 op.type().id() == ID_complex))
1617 {
1618 return unchanged(expr);
1619 }
1620
1621 // (type)ptr == NULL -> ptr == NULL
1622 // note that 'ptr' may be an integer
1623 auto new_expr = expr;
1624 new_expr.op0().swap(op);
1625 if(new_expr.op0().type().id() != ID_pointer)
1626 new_expr.op1() = from_integer(0, new_expr.op0().type());
1627 else
1628 new_expr.op1().type() = new_expr.op0().type();
1629 return changed(simplify_inequality(new_expr)); // do again!
1630 }
1631 }
1632
1633 // all we are doing with pointers
1634 return unchanged(expr);
1635 }
1636
1637 // is it a separation predicate?
1638
1639 if(expr.op0().id()==ID_plus)
1640 {
1641 // see if there is a constant in the sum
1642
1643 if(expr.id()==ID_equal || expr.id()==ID_notequal)
1644 {
1645 mp_integer constant=0;
1646 bool op_changed = false;
1647 auto new_expr = expr;
1648
1649 Forall_operands(it, new_expr.op0())
1650 {
1651 if(it->is_constant())
1652 {
1653 mp_integer i;
1654 if(!to_integer(to_constant_expr(*it), i))
1655 {
1656 constant+=i;
1657 *it=from_integer(0, it->type());
1658 op_changed = true;
1659 }
1660 }
1661 }
1662
1663 if(op_changed)
1664 {
1665 // adjust the constant on the RHS
1666 mp_integer i =
1667 numeric_cast_v<mp_integer>(to_constant_expr(new_expr.op1()));
1668 i-=constant;
1669 new_expr.op1() = from_integer(i, new_expr.op1().type());
1670
1671 new_expr.op0() = simplify_plus(to_plus_expr(new_expr.op0()));
1672 return changed(simplify_inequality(new_expr));
1673 }
1674 }
1675 }
1676
1677 #if 1
1678 // (double)value REL const ---> value rel const
1679 // if 'const' can be represented exactly.
1680
1681 if(
1682 expr.op0().id() == ID_typecast && expr.op0().type().id() == ID_floatbv &&
1683 to_typecast_expr(expr.op0()).op().type().id() == ID_floatbv)
1684 {
1685 ieee_floatt const_val(to_constant_expr(expr.op1()));
1686 ieee_floatt const_val_converted=const_val;
1687 const_val_converted.change_spec(ieee_float_spect(
1689 ieee_floatt const_val_converted_back=const_val_converted;
1690 const_val_converted_back.change_spec(
1692 if(const_val_converted_back==const_val)
1693 {
1694 auto result = expr;
1695 result.op0() = to_typecast_expr(expr.op0()).op();
1696 result.op1()=const_val_converted.to_expr();
1697 return std::move(result);
1698 }
1699 }
1700 #endif
1701
1702 // is the constant zero?
1703
1704 if(expr.op1().is_zero())
1705 {
1706 if(expr.id()==ID_ge &&
1707 expr.op0().type().id()==ID_unsignedbv)
1708 {
1709 // zero is always smaller or equal something unsigned
1710 return true_exprt();
1711 }
1712
1713 auto new_expr = expr;
1714 exprt &operand = new_expr.op0();
1715
1716 if(expr.id()==ID_equal)
1717 {
1718 // rules below do not hold for >=
1719 if(operand.id()==ID_unary_minus)
1720 {
1721 operand = to_unary_minus_expr(operand).op();
1722 return std::move(new_expr);
1723 }
1724 else if(operand.id()==ID_plus)
1725 {
1726 auto &operand_plus_expr = to_plus_expr(operand);
1727
1728 // simplify a+-b=0 to a=b
1729 if(operand_plus_expr.operands().size() == 2)
1730 {
1731 // if we have -b+a=0, make that a+(-b)=0
1732 if(operand_plus_expr.op0().id() == ID_unary_minus)
1733 operand_plus_expr.op0().swap(operand_plus_expr.op1());
1734
1735 if(operand_plus_expr.op1().id() == ID_unary_minus)
1736 {
1737 return binary_exprt(
1738 operand_plus_expr.op0(),
1739 expr.id(),
1740 to_unary_minus_expr(operand_plus_expr.op1()).op(),
1741 expr.type());
1742 }
1743 }
1744 }
1745 }
1746 }
1747
1748 // are we comparing with a typecast from bool?
1749 if(
1750 expr.op0().id() == ID_typecast &&
1751 to_typecast_expr(expr.op0()).op().type().id() == ID_bool)
1752 {
1753 const auto &lhs_typecast_op = to_typecast_expr(expr.op0()).op();
1754
1755 // we re-write (TYPE)boolean == 0 -> !boolean
1756 if(expr.op1().is_zero() && expr.id()==ID_equal)
1757 {
1758 return changed(simplify_not(not_exprt(lhs_typecast_op)));
1759 }
1760
1761 // we re-write (TYPE)boolean != 0 -> boolean
1762 if(expr.op1().is_zero() && expr.id()==ID_notequal)
1763 {
1764 return lhs_typecast_op;
1765 }
1766 }
1767
1768 #define NORMALISE_CONSTANT_TESTS
1769 #ifdef NORMALISE_CONSTANT_TESTS
1770 // Normalise to >= and = to improve caching and term sharing
1771 if(expr.op0().type().id()==ID_unsignedbv ||
1772 expr.op0().type().id()==ID_signedbv)
1773 {
1775
1776 if(expr.id()==ID_notequal)
1777 {
1778 auto new_rel_expr = expr;
1779 new_rel_expr.id(ID_equal);
1780 auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
1781 return changed(simplify_not(not_exprt(new_expr)));
1782 }
1783 else if(expr.id()==ID_gt)
1784 {
1785 mp_integer i = numeric_cast_v<mp_integer>(to_constant_expr(expr.op1()));
1786
1787 if(i==max)
1788 {
1789 return false_exprt();
1790 }
1791
1792 auto new_expr = expr;
1793 new_expr.id(ID_ge);
1794 ++i;
1795 new_expr.op1() = from_integer(i, new_expr.op1().type());
1797 }
1798 else if(expr.id()==ID_lt)
1799 {
1800 auto new_rel_expr = expr;
1801 new_rel_expr.id(ID_ge);
1802 auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
1803 return changed(simplify_not(not_exprt(new_expr)));
1804 }
1805 else if(expr.id()==ID_le)
1806 {
1807 mp_integer i = numeric_cast_v<mp_integer>(to_constant_expr(expr.op1()));
1808
1809 if(i==max)
1810 {
1811 return true_exprt();
1812 }
1813
1814 auto new_rel_expr = expr;
1815 new_rel_expr.id(ID_ge);
1816 ++i;
1817 new_rel_expr.op1() = from_integer(i, new_rel_expr.op1().type());
1818 auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
1819 return changed(simplify_not(not_exprt(new_expr)));
1820 }
1821 }
1822#endif
1823 return unchanged(expr);
1824}
1825
1828{
1829 auto const_bits_opt = expr2bits(
1830 expr.op(),
1832 ns);
1833
1834 if(!const_bits_opt.has_value())
1835 return unchanged(expr);
1836
1837 std::reverse(const_bits_opt->begin(), const_bits_opt->end());
1838
1839 auto result = bits2expr(
1840 *const_bits_opt,
1841 expr.type(),
1843 ns);
1844 if(!result.has_value())
1845 return unchanged(expr);
1846
1847 return std::move(*result);
1848}
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
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)
Definition: arith_tools.cpp:99
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
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.
API to expression classes for bitvectors.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: c_types.h:344
exprt & object()
Definition: pointer_expr.h:370
A base class for binary expressions.
Definition: std_expr.h:550
exprt & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
Bit-wise negation of bit-vectors.
Reverse the order of bits in a bit-vector.
void set_width(std::size_t width)
Definition: std_types.h:869
std::size_t get_width() const
Definition: std_types.h:864
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:2807
const irep_idt & get_value() const
Definition: std_expr.h:2815
bool value_is_zero_string() const
Definition: std_expr.cpp:16
void set_value(const irep_idt &value)
Definition: std_expr.h:2820
Division.
Definition: std_expr.h:1064
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
void swap(dstringt &b)
Definition: dstring.h:145
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:114
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
exprt & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
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:2865
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
Definition: ieee_float.cpp:702
void negate()
Definition: ieee_float.h:179
void change_spec(const ieee_float_spect &dest_spec)
The trinary if-then-else operator.
Definition: std_expr.h:2226
exprt & false_case()
Definition: std_expr.h:2263
exprt & true_case()
Definition: std_expr.h:2253
mp_integer largest() const
Return the largest value that can be represented using this type.
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
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:973
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1135
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1019
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:824
exprt & op1()
Definition: std_expr.h:850
exprt & op0()
Definition: std_expr.h:844
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:2181
The plus expression Associativity is not specified.
Definition: std_expr.h:914
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()
exprt & op()
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_shifts(const shift_exprt &)
resultt simplify_typecast(const typecast_exprt &)
resultt simplify_boolean(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_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:2856
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:293
The unary minus expression.
Definition: std_expr.h:390
The unary plus expression.
Definition: std_expr.h:439
Fixed-width bit-vector with unsigned binary interpretation.
configt config
Definition: config.cpp:25
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
#define Forall_expr(it, expr)
Definition: expr.h:34
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Definition: expr_util.cpp:283
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:216
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:200
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.
Definition: pointer_expr.h:398
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
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:12
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
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:807
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:953
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:998
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:420
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1265
endiannesst endianness
Definition: config.h:177
bool NULL_is_zero
Definition: config.h:194