cprover
invariant_set.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Invariant Set
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "invariant_set.h"
13
14#include <iostream>
15
16#include <util/arith_tools.h>
17#include <util/byte_operators.h>
18#include <util/expr_util.h>
19#include <util/namespace.h>
20#include <util/pointer_expr.h>
21#include <util/simplify_expr.h>
22#include <util/std_code.h>
23
25
26void inv_object_storet::output(std::ostream &out) const
27{
28 for(std::size_t i=0; i<entries.size(); i++)
29 out << "STORE " << i << ": " << map[i] << '\n';
30}
31
32bool inv_object_storet::get(const exprt &expr, unsigned &n)
33{
34 std::string s=build_string(expr);
35 if(s.empty())
36 return true;
37
38 // if it's a constant, we add it in any case
39 if(is_constant(expr))
40 {
41 n=map.number(s);
42
43 if(n>=entries.size())
44 {
45 entries.resize(n+1);
46 entries[n].expr=expr;
47 entries[n].is_constant=true;
48 }
49
50 return false;
51 }
52
53 if(const auto number = map.get_number(s))
54 {
55 n = *number;
56 return false;
57 }
58 return true;
59}
60
61unsigned inv_object_storet::add(const exprt &expr)
62{
63 std::string s=build_string(expr);
64 CHECK_RETURN(!s.empty());
65
67
68 if(n>=entries.size())
69 {
70 entries.resize(n+1);
71 entries[n].expr=expr;
72 entries[n].is_constant=is_constant(expr);
73 }
74
75 return n;
76}
77
78bool inv_object_storet::is_constant(unsigned n) const
79{
80 assert(n<entries.size());
81 return entries[n].is_constant;
82}
83
85{
86 return expr.is_constant() ||
88}
89
90std::string inv_object_storet::build_string(const exprt &expr) const
91{
92 // we ignore some casts
93 if(expr.id()==ID_typecast)
94 {
95 const auto &typecast_expr = to_typecast_expr(expr);
96
97 if(
98 typecast_expr.type().id() == ID_signedbv ||
99 typecast_expr.type().id() == ID_unsignedbv)
100 {
101 const typet &op_type = typecast_expr.op().type();
102
103 if(op_type.id() == ID_signedbv || op_type.id() == ID_unsignedbv)
104 {
105 if(
106 to_bitvector_type(typecast_expr.type()).get_width() >=
107 to_bitvector_type(op_type).get_width())
108 {
109 return build_string(typecast_expr.op());
110 }
111 }
112 else if(op_type.id() == ID_bool)
113 {
114 return build_string(typecast_expr.op());
115 }
116 }
117 }
118
119 // we always track constants, but make sure they are uniquely
120 // represented
121 if(expr.is_constant())
122 {
123 // NULL?
124 if(expr.type().id()==ID_pointer)
125 if(expr.get(ID_value)==ID_NULL)
126 return "0";
127
128 const auto i = numeric_cast<mp_integer>(expr);
129 if(i.has_value())
130 return integer2string(*i);
131 }
132
133 // we also like "address_of" if the object is constant
134 // we don't know what mode (language) we are in, so we rely on the default
135 // language to be reasonable for from_expr
136 if(is_constant_address(expr))
137 return from_expr(ns, irep_idt(), expr);
138
139 if(expr.id()==ID_member)
140 {
141 return build_string(to_member_expr(expr).compound()) + "." +
142 expr.get_string(ID_component_name);
143 }
144
145 if(expr.id()==ID_symbol)
147
148 return "";
149}
150
152 const exprt &expr,
153 unsigned &n) const
154{
155 return object_store.get(expr, n);
156}
157
159{
160 if(expr.id()==ID_address_of)
161 return is_constant_address_rec(to_address_of_expr(expr).object());
162
163 return false;
164}
165
167{
168 if(expr.id()==ID_symbol)
169 return true;
170 else if(expr.id()==ID_member)
171 return is_constant_address_rec(to_member_expr(expr).compound());
172 else if(expr.id()==ID_index)
173 {
174 const auto &index_expr = to_index_expr(expr);
175 if(index_expr.index().is_constant())
176 return is_constant_address_rec(index_expr.array());
177 }
178
179 return false;
180}
181
183 const std::pair<unsigned, unsigned> &p,
184 ineq_sett &dest)
185{
186 eq_set.check_index(p.first);
187 eq_set.check_index(p.second);
188
189 // add all. Quadratic.
190 unsigned f_r=eq_set.find(p.first);
191 unsigned s_r=eq_set.find(p.second);
192
193 for(std::size_t f=0; f<eq_set.size(); f++)
194 {
195 if(eq_set.find(f)==f_r)
196 {
197 for(std::size_t s=0; s<eq_set.size(); s++)
198 if(eq_set.find(s)==s_r)
199 dest.insert(std::pair<unsigned, unsigned>(f, s));
200 }
201 }
202}
203
204void invariant_sett::add_eq(const std::pair<unsigned, unsigned> &p)
205{
206 eq_set.make_union(p.first, p.second);
207
208 // check if there is a contradiction with two constants
209 unsigned r=eq_set.find(p.first);
210
211 bool constant_seen=false;
212 mp_integer c;
213
214 for(std::size_t i=0; i<eq_set.size(); i++)
215 {
216 if(eq_set.find(i)==r)
217 {
219 {
220 if(constant_seen)
221 {
222 // contradiction
223 make_false();
224 return;
225 }
226 else
227 constant_seen=true;
228 }
229 }
230 }
231
232 // replicate <= and != constraints
233
234 for(const auto &le : le_set)
235 add_eq(le_set, p, le);
236
237 for(const auto &ne : ne_set)
238 add_eq(ne_set, p, ne);
239}
240
242 ineq_sett &dest,
243 const std::pair<unsigned, unsigned> &eq,
244 const std::pair<unsigned, unsigned> &ineq)
245{
246 std::pair<unsigned, unsigned> n;
247
248 // uhuh. Need to try all pairs
249
250 if(eq.first==ineq.first)
251 {
252 n=ineq;
253 n.first=eq.second;
254 dest.insert(n);
255 }
256
257 if(eq.first==ineq.second)
258 {
259 n=ineq;
260 n.second=eq.second;
261 dest.insert(n);
262 }
263
264 if(eq.second==ineq.first)
265 {
266 n=ineq;
267 n.first=eq.first;
268 dest.insert(n);
269 }
270
271 if(eq.second==ineq.second)
272 {
273 n=ineq;
274 n.second=eq.first;
275 dest.insert(n);
276 }
277}
278
279tvt invariant_sett::is_eq(std::pair<unsigned, unsigned> p) const
280{
281 std::pair<unsigned, unsigned> s=p;
282 std::swap(s.first, s.second);
283
284 if(has_eq(p))
285 return tvt(true);
286
287 if(has_ne(p) || has_ne(s))
288 return tvt(false);
289
290 return tvt::unknown();
291}
292
293tvt invariant_sett::is_le(std::pair<unsigned, unsigned> p) const
294{
295 std::pair<unsigned, unsigned> s=p;
296 std::swap(s.first, s.second);
297
298 if(has_eq(p))
299 return tvt(true);
300
301 if(has_le(p))
302 return tvt(true);
303
304 if(has_le(s))
305 if(has_ne(s) || has_ne(p))
306 return tvt(false);
307
308 return tvt::unknown();
309}
310
311void invariant_sett::output(std::ostream &out) const
312{
313 if(is_false)
314 {
315 out << "FALSE\n";
316 return;
317 }
318
319 for(std::size_t i=0; i<eq_set.size(); i++)
320 if(eq_set.is_root(i) &&
321 eq_set.count(i)>=2)
322 {
323 bool first=true;
324 for(std::size_t j=0; j<eq_set.size(); j++)
325 if(eq_set.find(j)==i)
326 {
327 if(first)
328 first=false;
329 else
330 out << " = ";
331
332 out << to_string(j);
333 }
334
335 out << '\n';
336 }
337
338 for(const auto &bounds : bounds_map)
339 {
340 out << to_string(bounds.first) << " in " << bounds.second << '\n';
341 }
342
343 for(const auto &le : le_set)
344 {
345 out << to_string(le.first) << " <= " << to_string(le.second) << '\n';
346 }
347
348 for(const auto &ne : ne_set)
349 {
350 out << to_string(ne.first) << " != " << to_string(ne.second) << '\n';
351 }
352}
353
354void invariant_sett::add_type_bounds(const exprt &expr, const typet &type)
355{
356 if(expr.type()==type)
357 return;
358
359 if(type.id()==ID_unsignedbv)
360 {
361 std::size_t op_width=to_unsignedbv_type(type).get_width();
362
363 // TODO - 8 appears to be a magic number here -- or perhaps this should say
364 // ">=" instead, and is meant to restrict types larger than a single byte?
365 if(op_width<=8)
366 {
367 unsigned a;
368 if(get_object(expr, a))
369 return;
370
371 add_bounds(a, boundst(0, power(2, op_width)-1));
372 }
373 }
374}
375
377{
378 exprt tmp(expr);
379 nnf(tmp);
380 strengthen_rec(tmp);
381}
382
384{
385 if(expr.type().id()!=ID_bool)
386 throw "non-Boolean argument to strengthen()";
387
388 #if 0
389 std::cout << "S: " << from_expr(*ns, irep_idt(), expr) << '\n';
390#endif
391
392 if(is_false)
393 {
394 // we can't get any stronger
395 return;
396 }
397
398 if(expr.is_true())
399 {
400 // do nothing, it's useless
401 }
402 else if(expr.is_false())
403 {
404 // wow, that's strong
405 make_false();
406 }
407 else if(expr.id()==ID_not)
408 {
409 // give up, we expect NNF
410 }
411 else if(expr.id()==ID_and)
412 {
413 forall_operands(it, expr)
414 strengthen_rec(*it);
415 }
416 else if(expr.id()==ID_le ||
417 expr.id()==ID_lt)
418 {
419 const auto &rel = to_binary_relation_expr(expr);
420
421 // special rule: x <= (a & b)
422 // implies: x<=a && x<=b
423
424 if(rel.rhs().id() == ID_bitand)
425 {
426 const exprt &bitand_op = rel.op1();
427
428 forall_operands(it, bitand_op)
429 {
430 auto tmp(rel);
431 tmp.op1()=*it;
432 strengthen_rec(tmp);
433 }
434
435 return;
436 }
437
438 std::pair<unsigned, unsigned> p;
439
440 if(get_object(rel.op0(), p.first) || get_object(rel.op1(), p.second))
441 return;
442
443 const auto i0 = numeric_cast<mp_integer>(rel.op0());
444 const auto i1 = numeric_cast<mp_integer>(rel.op1());
445
446 if(expr.id()==ID_le)
447 {
448 if(i0.has_value())
449 add_bounds(p.second, lower_interval(*i0));
450 else if(i1.has_value())
451 add_bounds(p.first, upper_interval(*i1));
452 else
453 add_le(p);
454 }
455 else if(expr.id()==ID_lt)
456 {
457 if(i0.has_value())
458 add_bounds(p.second, lower_interval(*i0 + 1));
459 else if(i1.has_value())
460 add_bounds(p.first, upper_interval(*i1 - 1));
461 else
462 {
463 add_le(p);
464 add_ne(p);
465 }
466 }
467 else
469 }
470 else if(expr.id()==ID_equal)
471 {
472 const auto &equal_expr = to_equal_expr(expr);
473
474 const typet &op_type = equal_expr.op0().type();
475
476 if(op_type.id() == ID_struct || op_type.id() == ID_struct_tag)
477 {
478 const struct_typet &struct_type = to_struct_type(ns.follow(op_type));
479
480 for(const auto &comp : struct_type.components())
481 {
482 const member_exprt lhs_member_expr(
483 equal_expr.op0(), comp.get_name(), comp.type());
484 const member_exprt rhs_member_expr(
485 equal_expr.op1(), comp.get_name(), comp.type());
486
487 const equal_exprt equality(lhs_member_expr, rhs_member_expr);
488
489 // recursive call
490 strengthen_rec(equality);
491 }
492
493 return;
494 }
495
496 // special rule: x = (a & b)
497 // implies: x<=a && x<=b
498
499 if(equal_expr.op1().id() == ID_bitand)
500 {
501 const exprt &bitand_op = equal_expr.op1();
502
503 forall_operands(it, bitand_op)
504 {
505 auto tmp(equal_expr);
506 tmp.op1()=*it;
507 tmp.id(ID_le);
508 strengthen_rec(tmp);
509 }
510
511 return;
512 }
513 else if(equal_expr.op0().id() == ID_bitand)
514 {
515 auto tmp(equal_expr);
516 std::swap(tmp.op0(), tmp.op1());
517 strengthen_rec(tmp);
518 return;
519 }
520
521 // special rule: x = (type) y
522 if(equal_expr.op1().id() == ID_typecast)
523 {
524 const auto &typecast_expr = to_typecast_expr(equal_expr.op1());
525 add_type_bounds(equal_expr.op0(), typecast_expr.op().type());
526 }
527 else if(equal_expr.op0().id() == ID_typecast)
528 {
529 const auto &typecast_expr = to_typecast_expr(equal_expr.op0());
530 add_type_bounds(equal_expr.op1(), typecast_expr.op().type());
531 }
532
533 std::pair<unsigned, unsigned> p, s;
534
535 if(
536 get_object(equal_expr.op0(), p.first) ||
537 get_object(equal_expr.op1(), p.second))
538 {
539 return;
540 }
541
542 const auto i0 = numeric_cast<mp_integer>(equal_expr.op0());
543 const auto i1 = numeric_cast<mp_integer>(equal_expr.op1());
544 if(i0.has_value())
545 add_bounds(p.second, boundst(*i0));
546 else if(i1.has_value())
547 add_bounds(p.first, boundst(*i1));
548
549 s=p;
550 std::swap(s.first, s.second);
551
552 // contradiction?
553 if(has_ne(p) || has_ne(s))
554 make_false();
555 else if(!has_eq(p))
556 add_eq(p);
557 }
558 else if(expr.id()==ID_notequal)
559 {
560 const auto &notequal_expr = to_notequal_expr(expr);
561
562 std::pair<unsigned, unsigned> p;
563
564 if(
565 get_object(notequal_expr.op0(), p.first) ||
566 get_object(notequal_expr.op1(), p.second))
567 {
568 return;
569 }
570
571 // check if this is a contradiction
572 if(has_eq(p))
573 make_false();
574 else
575 add_ne(p);
576 }
577}
578
580{
581 exprt tmp(expr);
582 nnf(tmp);
583 return implies_rec(tmp);
584}
585
587{
588 if(expr.type().id()!=ID_bool)
589 throw "implies: non-Boolean expression";
590
591 #if 0
592 std::cout << "I: " << from_expr(*ns, irep_idt(), expr) << '\n';
593#endif
594
595 if(is_false) // can't get any stronger
596 return tvt(true);
597
598 if(expr.is_true())
599 return tvt(true);
600 else if(expr.id()==ID_not)
601 {
602 // give up, we expect NNF
603 }
604 else if(expr.id()==ID_and)
605 {
606 forall_operands(it, expr)
607 if(implies_rec(*it)!=tvt(true))
608 return tvt::unknown();
609
610 return tvt(true);
611 }
612 else if(expr.id()==ID_or)
613 {
614 forall_operands(it, expr)
615 if(implies_rec(*it)==tvt(true))
616 return tvt(true);
617 }
618 else if(expr.id()==ID_le ||
619 expr.id()==ID_lt ||
620 expr.id()==ID_equal ||
621 expr.id()==ID_notequal)
622 {
623 const auto &rel = to_binary_relation_expr(expr);
624
625 std::pair<unsigned, unsigned> p;
626
627 bool ob0 = get_object(rel.lhs(), p.first);
628 bool ob1 = get_object(rel.rhs(), p.second);
629
630 if(ob0 || ob1)
631 return tvt::unknown();
632
633 tvt r;
634
635 if(rel.id() == ID_le)
636 {
637 r=is_le(p);
638 if(!r.is_unknown())
639 return r;
640
641 boundst b0, b1;
642 get_bounds(p.first, b0);
643 get_bounds(p.second, b1);
644
645 return b0<=b1;
646 }
647 else if(rel.id() == ID_lt)
648 {
649 r=is_lt(p);
650 if(!r.is_unknown())
651 return r;
652
653 boundst b0, b1;
654 get_bounds(p.first, b0);
655 get_bounds(p.second, b1);
656
657 return b0<b1;
658 }
659 else if(rel.id() == ID_equal)
660 return is_eq(p);
661 else if(rel.id() == ID_notequal)
662 return is_ne(p);
663 else
665 }
666
667 return tvt::unknown();
668}
669
670void invariant_sett::get_bounds(unsigned a, boundst &bounds) const
671{
672 // unbounded
673 bounds=boundst();
674
675 {
676 const exprt &e_a = object_store.get_expr(a);
677 const auto tmp = numeric_cast<mp_integer>(e_a);
678 if(tmp.has_value())
679 {
680 bounds = boundst(*tmp);
681 return;
682 }
683
684 if(e_a.type().id()==ID_unsignedbv)
685 bounds=lower_interval(mp_integer(0));
686 }
687
688 bounds_mapt::const_iterator it=bounds_map.find(a);
689
690 if(it!=bounds_map.end())
691 bounds=it->second;
692}
693
694void invariant_sett::nnf(exprt &expr, bool negate)
695{
696 if(expr.type().id()!=ID_bool)
697 throw "nnf: non-Boolean expression";
698
699 if(expr.is_true())
700 {
701 if(negate)
702 expr=false_exprt();
703 }
704 else if(expr.is_false())
705 {
706 if(negate)
707 expr=true_exprt();
708 }
709 else if(expr.id()==ID_not)
710 {
711 nnf(to_not_expr(expr).op(), !negate);
712 exprt tmp;
713 tmp.swap(to_not_expr(expr).op());
714 expr.swap(tmp);
715 }
716 else if(expr.id()==ID_and)
717 {
718 if(negate)
719 expr.id(ID_or);
720
721 Forall_operands(it, expr)
722 nnf(*it, negate);
723 }
724 else if(expr.id()==ID_or)
725 {
726 if(negate)
727 expr.id(ID_and);
728
729 Forall_operands(it, expr)
730 nnf(*it, negate);
731 }
732 else if(expr.id()==ID_typecast)
733 {
734 const auto &typecast_expr = to_typecast_expr(expr);
735
736 if(
737 typecast_expr.op().type().id() == ID_unsignedbv ||
738 typecast_expr.op().type().id() == ID_signedbv)
739 {
740 equal_exprt tmp(
741 typecast_expr.op(), from_integer(0, typecast_expr.op().type()));
742 nnf(tmp, !negate);
743 expr.swap(tmp);
744 }
745 else if(negate)
746 {
747 expr = boolean_negate(expr);
748 }
749 }
750 else if(expr.id()==ID_le)
751 {
752 if(negate)
753 {
754 // !a<=b <-> !b=>a <-> b<a
755 expr.id(ID_lt);
756 auto &rel = to_binary_relation_expr(expr);
757 std::swap(rel.lhs(), rel.rhs());
758 }
759 }
760 else if(expr.id()==ID_lt)
761 {
762 if(negate)
763 {
764 // !a<b <-> !b>a <-> b<=a
765 expr.id(ID_le);
766 auto &rel = to_binary_relation_expr(expr);
767 std::swap(rel.lhs(), rel.rhs());
768 }
769 }
770 else if(expr.id()==ID_ge)
771 {
772 if(negate)
773 expr.id(ID_lt);
774 else
775 {
776 expr.id(ID_le);
777 auto &rel = to_binary_relation_expr(expr);
778 std::swap(rel.lhs(), rel.rhs());
779 }
780 }
781 else if(expr.id()==ID_gt)
782 {
783 if(negate)
784 expr.id(ID_le);
785 else
786 {
787 expr.id(ID_lt);
788 auto &rel = to_binary_relation_expr(expr);
789 std::swap(rel.lhs(), rel.rhs());
790 }
791 }
792 else if(expr.id()==ID_equal)
793 {
794 if(negate)
795 expr.id(ID_notequal);
796 }
797 else if(expr.id()==ID_notequal)
798 {
799 if(negate)
800 expr.id(ID_equal);
801 }
802 else if(negate)
803 {
804 expr = boolean_negate(expr);
805 }
806}
807
809 exprt &expr) const
810{
811 if(expr.id()==ID_address_of)
812 return;
813
814 Forall_operands(it, expr)
815 simplify(*it);
816
817 if(expr.id()==ID_symbol ||
818 expr.id()==ID_member)
819 {
820 exprt tmp=get_constant(expr);
821 if(tmp.is_not_nil())
822 expr.swap(tmp);
823 }
824}
825
827{
828 unsigned a;
829
830 if(!get_object(expr, a))
831 {
832 // bounds?
833 bounds_mapt::const_iterator it=bounds_map.find(a);
834
835 if(it!=bounds_map.end())
836 {
837 if(it->second.singleton())
838 return from_integer(it->second.get_lower(), expr.type());
839 }
840
841 unsigned r=eq_set.find(a);
842
843 // is it a constant?
844 for(std::size_t i=0; i<eq_set.size(); i++)
845 if(eq_set.find(i)==r)
846 {
847 const exprt &e = object_store.get_expr(i);
848
849 if(e.is_constant())
850 {
851 const mp_integer value =
852 numeric_cast_v<mp_integer>(to_constant_expr(e));
853
854 if(expr.type().id()==ID_pointer)
855 {
856 if(value==0)
858 }
859 else
860 return from_integer(value, expr.type());
861 }
863 {
864 if(e.type()==expr.type())
865 return e;
866
867 return typecast_exprt(e, expr.type());
868 }
869 }
870 }
871
872 return static_cast<const exprt &>(get_nil_irep());
873}
874
875std::string inv_object_storet::to_string(unsigned a) const
876{
877 return id2string(map[a]);
878}
879
880std::string invariant_sett::to_string(unsigned a) const
881{
882 return object_store.to_string(a);
883}
884
886{
887 if(other.threaded &&
888 !threaded)
889 {
891 return true; // change
892 }
893
894 if(threaded)
895 return false; // no change
896
897 if(other.is_false)
898 return false; // no change
899
900 if(is_false)
901 {
902 // copy
903 is_false=false;
904 eq_set=other.eq_set;
905 le_set=other.le_set;
906 ne_set=other.ne_set;
908
909 return true; // change
910 }
911
912 // equalities first
913 unsigned old_eq_roots=eq_set.count_roots();
914
916
917 // inequalities
918 std::size_t old_ne_set=ne_set.size();
919 std::size_t old_le_set=le_set.size();
920
921 intersection(ne_set, other.ne_set);
922 intersection(le_set, other.le_set);
923
924 // bounds
926 return true;
927
928 if(old_eq_roots!=eq_set.count_roots() ||
929 old_ne_set!=ne_set.size() ||
930 old_le_set!=le_set.size())
931 return true;
932
933 return false; // no change
934}
935
937{
938 bool changed=false;
939
940 for(bounds_mapt::iterator
941 it=bounds_map.begin();
942 it!=bounds_map.end();
943 ) // no it++
944 {
945 bounds_mapt::const_iterator o_it=other.find(it->first);
946
947 if(o_it==other.end())
948 {
949 bounds_mapt::iterator next(it);
950 next++;
951 bounds_map.erase(it);
952 it=next;
953 changed=true;
954 }
955 else
956 {
957 boundst old(it->second);
958 it->second.approx_union_with(o_it->second);
959 if(it->second!=old)
960 changed=true;
961 it++;
962 }
963 }
964
965 return changed;
966}
967
969{
970 eq_set.isolate(a);
971 remove(ne_set, a);
972 remove(le_set, a);
973 bounds_map.erase(a);
974}
975
977{
978 if(lhs.id()==ID_symbol ||
979 lhs.id()==ID_member)
980 {
981 unsigned a;
982 if(!get_object(lhs, a))
983 modifies(a);
984 }
985 else if(lhs.id()==ID_index)
986 {
987 // we don't track arrays
988 }
989 else if(lhs.id()==ID_dereference)
990 {
991 // be very, very conservative for now
992 make_true();
993 }
994 else if(lhs.id()=="object_value")
995 {
996 // be very, very conservative for now
997 make_true();
998 }
999 else if(lhs.id()==ID_if)
1000 {
1001 // we just assume both are changed
1002 modifies(to_if_expr(lhs).op1());
1003 modifies(to_if_expr(lhs).op2());
1004 }
1005 else if(lhs.id()==ID_typecast)
1006 {
1007 // just go down
1008 modifies(to_typecast_expr(lhs).op());
1009 }
1010 else if(lhs.id()=="valid_object")
1011 {
1012 }
1013 else if(lhs.id()==ID_byte_extract_little_endian ||
1014 lhs.id()==ID_byte_extract_big_endian)
1015 {
1016 // just go down
1017 modifies(to_byte_extract_expr(lhs).op0());
1018 }
1019 else if(lhs.id() == ID_null_object ||
1020 lhs.id() == "is_zero_string" ||
1021 lhs.id() == "zero_string" ||
1022 lhs.id() == "zero_string_length")
1023 {
1024 // ignore
1025 }
1026 else
1027 throw "modifies: unexpected lhs: "+lhs.id_string();
1028}
1029
1031 const exprt &lhs,
1032 const exprt &rhs)
1033{
1034 equal_exprt equality(lhs, rhs);
1035
1036 // first evaluate RHS
1037 simplify(equality.rhs());
1038 ::simplify(equality.rhs(), ns);
1039
1040 // now kill LHS
1041 modifies(lhs);
1042
1043 // and put it back
1044 strengthen(equality);
1045}
1046
1048{
1049 const irep_idt &statement=code.get(ID_statement);
1050
1051 if(statement==ID_block)
1052 {
1053 forall_operands(it, code)
1054 apply_code(to_code(*it));
1055 }
1056 else if(statement==ID_assign)
1057 {
1058 if(code.operands().size()!=2)
1059 throw "assignment expected to have two operands";
1060
1061 assignment(code.op0(), code.op1());
1062 }
1063 else if(statement==ID_decl)
1064 {
1065 if(code.operands().size()==2)
1066 assignment(code.op0(), code.op1());
1067 else
1068 modifies(code.op0());
1069 }
1070 else if(statement==ID_expression)
1071 {
1072 // this never modifies anything
1073 }
1074 else if(statement==ID_function_call)
1075 {
1076 // may be a disaster
1077 make_true();
1078 }
1079 else if(statement==ID_cpp_delete ||
1080 statement==ID_cpp_delete_array)
1081 {
1082 // does nothing
1083 }
1084 else if(statement==ID_printf)
1085 {
1086 // does nothing
1087 }
1088 else if(statement=="lock" ||
1089 statement=="unlock" ||
1090 statement==ID_asm)
1091 {
1092 // ignore for now
1093 }
1094 else
1095 {
1096 std::cerr << code.pretty() << '\n';
1097 throw "invariant_sett: unexpected statement: "+id2string(statement);
1098 }
1099}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
exprt & rhs()
Definition: std_expr.h:590
std::size_t get_width() const
Definition: std_types.h:864
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
exprt & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
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
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
The Boolean constant false.
Definition: std_expr.h:2865
const exprt & get_expr(unsigned n) const
Definition: invariant_set.h:50
void output(std::ostream &out) const
static bool is_constant_address_rec(const exprt &expr)
static bool is_constant_address(const exprt &expr)
std::string build_string(const exprt &expr) const
std::string to_string(unsigned n) const
unsigned add(const exprt &expr)
std::vector< entryt > entries
Definition: invariant_set.h:72
bool is_constant(unsigned n) const
bool get(const exprt &expr, unsigned &n)
const namespacet & ns
Definition: invariant_set.h:61
inv_object_storet & object_store
tvt is_lt(std::pair< unsigned, unsigned > p) const
tvt is_le(std::pair< unsigned, unsigned > p) const
void add_ne(const std::pair< unsigned, unsigned > &p)
bool has_le(const std::pair< unsigned, unsigned > &p) const
tvt implies_rec(const exprt &expr) const
void apply_code(const codet &code)
unsigned_union_find eq_set
Definition: invariant_set.h:83
std::map< unsigned, boundst > bounds_mapt
Definition: invariant_set.h:94
ineq_sett ne_set
Definition: invariant_set.h:90
exprt get_constant(const exprt &expr) const
tvt is_ne(std::pair< unsigned, unsigned > p) const
interval_templatet< mp_integer > boundst
Definition: invariant_set.h:93
ineq_sett le_set
Definition: invariant_set.h:87
void simplify(exprt &expr) const
void output(std::ostream &out) const
void add_bounds(unsigned a, const boundst &bound)
bool make_union(const invariant_sett &other_invariants)
void strengthen(const exprt &expr)
void make_threaded()
void assignment(const exprt &lhs, const exprt &rhs)
void add_eq(const std::pair< unsigned, unsigned > &eq)
static void intersection(ineq_sett &dest, const ineq_sett &other)
bounds_mapt bounds_map
Definition: invariant_set.h:95
std::set< std::pair< unsigned, unsigned > > ineq_sett
Definition: invariant_set.h:86
static void nnf(exprt &expr, bool negate=false)
const namespacet & ns
void get_bounds(unsigned a, boundst &dest) const
static void remove(ineq_sett &dest, unsigned a)
tvt implies(const exprt &expr) const
void add(const std::pair< unsigned, unsigned > &p, ineq_sett &dest)
void add_type_bounds(const exprt &expr, const typet &type)
void add_le(const std::pair< unsigned, unsigned > &p)
bool has_ne(const std::pair< unsigned, unsigned > &p) const
bool get_object(const exprt &expr, unsigned &n) const
bool make_union_bounds_map(const bounds_mapt &other)
std::string to_string(unsigned a) const
void modifies(const exprt &lhs)
void strengthen_rec(const exprt &expr)
bool has_eq(const std::pair< unsigned, unsigned > &p) const
tvt is_eq(std::pair< unsigned, unsigned > p) const
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
bool is_not_nil() const
Definition: irep.h:380
const std::string & id_string() const
Definition: irep.h:399
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
Extract member of struct or union.
Definition: std_expr.h:2667
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
The null pointer constant.
Definition: pointer_expr.h:723
number_type number(const key_type &a)
Definition: numbering.h:37
optionalt< number_type > get_number(const key_type &a) const
Definition: numbering.h:50
std::size_t number_type
Definition: numbering.h:24
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const componentst & components() const
Definition: std_types.h:147
The Boolean constant true.
Definition: std_expr.h:2856
Definition: threeval.h:20
static tvt unknown()
Definition: threeval.h:33
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
void intersection(const unsigned_union_find &other)
Definition: union_find.cpp:120
size_type size() const
Definition: union_find.h:97
void check_index(size_type a)
Definition: union_find.h:111
size_type find(size_type a) const
Definition: union_find.cpp:141
size_type count(size_type a) const
Definition: union_find.h:103
size_type count_roots() const
Definition: union_find.h:118
bool is_root(size_type a) const
Definition: union_find.h:82
void make_union(size_type a, size_type b)
Definition: union_find.cpp:13
void isolate(size_type a)
Definition: union_find.cpp:41
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:126
Deprecated expression utility functions.
interval_templatet< T > lower_interval(const T &l)
interval_templatet< T > upper_interval(const T &u)
Value Set.
const irept & get_nil_irep()
Definition: irep.cpp:20
dstringt irep_idt
Definition: irep.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
static int8_t r
Definition: irep_hash.h:60
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103
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
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
BigInt mp_integer
Definition: smt_terms.h:12
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
const codet & to_code(const exprt &expr)
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 index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1308
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2206
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1265
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308