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