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