cprover
invariant_set.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Invariant Set
4 
5 Author: 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 
24 #include <langapi/language_util.h>
25 
26 void 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 
32 bool 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 
61 unsigned 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 
78 bool inv_object_storet::is_constant(unsigned n) const
79 {
80  assert(n<entries.size());
81  return entries[n].is_constant;
82 }
83 
84 bool inv_object_storet::is_constant(const exprt &expr) const
85 {
86  return expr.is_constant() ||
87  is_constant_address(expr);
88 }
89 
90 std::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)
146  return id2string(to_symbol_expr(expr).get_identifier());
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 
204 void 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 
279 tvt 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 
293 tvt 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 
311 void 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 
354 void 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
468  UNREACHABLE;
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
664  UNREACHABLE;
665  }
666 
667  return tvt::unknown();
668 }
669 
670 void 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 
694 void 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)
857  return null_pointer_exprt(to_pointer_type(expr.type()));
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 
875 std::string inv_object_storet::to_string(unsigned a) const
876 {
877  return id2string(map[a]);
878 }
879 
880 std::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  {
890  make_threaded();
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;
907  bounds_map=other.bounds_map;
908 
909  return true; // change
910  }
911 
912  // equalities first
913  unsigned old_eq_roots=eq_set.count_roots();
914 
915  eq_set.intersection(other.eq_set);
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 
968 void invariant_sett::modifies(unsigned a)
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:843
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
exprt & op1()
Definition: expr.h:102
exprt & op0()
Definition: expr.h:99
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
exprt & op1()
Definition: expr.h:102
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
operandst & operands()
Definition: expr.h:92
The Boolean constant false.
Definition: std_expr.h:2811
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)
const exprt & get_expr(unsigned n) const
Definition: invariant_set.h:50
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 std::string & get_string(const irep_namet &name) const
Definition: irep.h:420
const std::string & id_string() const
Definition: irep.h:410
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
void swap(irept &irep)
Definition: irep.h:453
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
Extract member of struct or union.
Definition: std_expr.h:2613
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:703
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:2802
Definition: threeval.h:20
static tvt unknown()
Definition: threeval.h:33
Semantic type conversion.
Definition: std_expr.h:1866
The type of an expression, extends irept.
Definition: type.h:28
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:125
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:49
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 pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:378
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)
Definition: std_code.h:153
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:2237
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2786
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2152
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1265
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
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:1382
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308