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  // TODO - 8 appears to be a magic number here -- or perhaps this should say
368  // ">=" instead, and is meant to restrict types larger than a single byte?
369  if(op_width<=8)
370  {
371  unsigned a;
372  if(get_object(expr, a))
373  return;
374 
375  add_bounds(a, boundst(0, power(2, op_width)-1));
376  }
377  }
378 }
379 
381 {
382  exprt tmp(expr);
383  nnf(tmp);
384  strengthen_rec(tmp);
385 }
386 
388 {
389  if(expr.type().id()!=ID_bool)
390  throw "non-Boolean argument to strengthen()";
391 
392  #if 0
393  std::cout << "S: " << from_expr(*ns, irep_idt(), expr) << '\n';
394 #endif
395 
396  if(is_false)
397  {
398  // we can't get any stronger
399  return;
400  }
401 
402  if(expr.is_true())
403  {
404  // do nothing, it's useless
405  }
406  else if(expr.is_false())
407  {
408  // wow, that's strong
409  make_false();
410  }
411  else if(expr.id()==ID_not)
412  {
413  // give up, we expect NNF
414  }
415  else if(expr.id()==ID_and)
416  {
417  forall_operands(it, expr)
418  strengthen_rec(*it);
419  }
420  else if(expr.id()==ID_le ||
421  expr.id()==ID_lt)
422  {
423  const auto &rel = to_binary_relation_expr(expr);
424 
425  // special rule: x <= (a & b)
426  // implies: x<=a && x<=b
427 
428  if(rel.rhs().id() == ID_bitand)
429  {
430  const exprt &bitand_op = rel.op1();
431 
432  forall_operands(it, bitand_op)
433  {
434  auto tmp(rel);
435  tmp.op1()=*it;
436  strengthen_rec(tmp);
437  }
438 
439  return;
440  }
441 
442  std::pair<unsigned, unsigned> p;
443 
444  if(get_object(rel.op0(), p.first) || get_object(rel.op1(), p.second))
445  return;
446 
447  const auto i0 = numeric_cast<mp_integer>(rel.op0());
448  const auto i1 = numeric_cast<mp_integer>(rel.op1());
449 
450  if(expr.id()==ID_le)
451  {
452  if(i0.has_value())
453  add_bounds(p.second, lower_interval(*i0));
454  else if(i1.has_value())
455  add_bounds(p.first, upper_interval(*i1));
456  else
457  add_le(p);
458  }
459  else if(expr.id()==ID_lt)
460  {
461  if(i0.has_value())
462  add_bounds(p.second, lower_interval(*i0 + 1));
463  else if(i1.has_value())
464  add_bounds(p.first, upper_interval(*i1 - 1));
465  else
466  {
467  add_le(p);
468  add_ne(p);
469  }
470  }
471  else
472  UNREACHABLE;
473  }
474  else if(expr.id()==ID_equal)
475  {
476  const auto &equal_expr = to_equal_expr(expr);
477 
478  const typet &op_type = equal_expr.op0().type();
479 
480  if(op_type.id() == ID_struct || op_type.id() == ID_struct_tag)
481  {
482  const struct_typet &struct_type = to_struct_type(ns.follow(op_type));
483 
484  for(const auto &comp : struct_type.components())
485  {
486  const member_exprt lhs_member_expr(
487  equal_expr.op0(), comp.get_name(), comp.type());
488  const member_exprt rhs_member_expr(
489  equal_expr.op1(), comp.get_name(), comp.type());
490 
491  const equal_exprt equality(lhs_member_expr, rhs_member_expr);
492 
493  // recursive call
494  strengthen_rec(equality);
495  }
496 
497  return;
498  }
499 
500  // special rule: x = (a & b)
501  // implies: x<=a && x<=b
502 
503  if(equal_expr.op1().id() == ID_bitand)
504  {
505  const exprt &bitand_op = equal_expr.op1();
506 
507  forall_operands(it, bitand_op)
508  {
509  auto tmp(equal_expr);
510  tmp.op1()=*it;
511  tmp.id(ID_le);
512  strengthen_rec(tmp);
513  }
514 
515  return;
516  }
517  else if(equal_expr.op0().id() == ID_bitand)
518  {
519  auto tmp(equal_expr);
520  std::swap(tmp.op0(), tmp.op1());
521  strengthen_rec(tmp);
522  return;
523  }
524 
525  // special rule: x = (type) y
526  if(equal_expr.op1().id() == ID_typecast)
527  {
528  const auto &typecast_expr = to_typecast_expr(equal_expr.op1());
529  add_type_bounds(equal_expr.op0(), typecast_expr.op().type());
530  }
531  else if(equal_expr.op0().id() == ID_typecast)
532  {
533  const auto &typecast_expr = to_typecast_expr(equal_expr.op0());
534  add_type_bounds(equal_expr.op1(), typecast_expr.op().type());
535  }
536 
537  std::pair<unsigned, unsigned> p, s;
538 
539  if(
540  get_object(equal_expr.op0(), p.first) ||
541  get_object(equal_expr.op1(), p.second))
542  {
543  return;
544  }
545 
546  const auto i0 = numeric_cast<mp_integer>(equal_expr.op0());
547  const auto i1 = numeric_cast<mp_integer>(equal_expr.op1());
548  if(i0.has_value())
549  add_bounds(p.second, boundst(*i0));
550  else if(i1.has_value())
551  add_bounds(p.first, boundst(*i1));
552 
553  s=p;
554  std::swap(s.first, s.second);
555 
556  // contradiction?
557  if(has_ne(p) || has_ne(s))
558  make_false();
559  else if(!has_eq(p))
560  add_eq(p);
561  }
562  else if(expr.id()==ID_notequal)
563  {
564  const auto &notequal_expr = to_notequal_expr(expr);
565 
566  std::pair<unsigned, unsigned> p;
567 
568  if(
569  get_object(notequal_expr.op0(), p.first) ||
570  get_object(notequal_expr.op1(), p.second))
571  {
572  return;
573  }
574 
575  // check if this is a contradiction
576  if(has_eq(p))
577  make_false();
578  else
579  add_ne(p);
580  }
581 }
582 
584 {
585  exprt tmp(expr);
586  nnf(tmp);
587  return implies_rec(tmp);
588 }
589 
591 {
592  if(expr.type().id()!=ID_bool)
593  throw "implies: non-Boolean expression";
594 
595  #if 0
596  std::cout << "I: " << from_expr(*ns, irep_idt(), expr) << '\n';
597 #endif
598 
599  if(is_false) // can't get any stronger
600  return tvt(true);
601 
602  if(expr.is_true())
603  return tvt(true);
604  else if(expr.id()==ID_not)
605  {
606  // give up, we expect NNF
607  }
608  else if(expr.id()==ID_and)
609  {
610  forall_operands(it, expr)
611  if(implies_rec(*it)!=tvt(true))
612  return tvt::unknown();
613 
614  return tvt(true);
615  }
616  else if(expr.id()==ID_or)
617  {
618  forall_operands(it, expr)
619  if(implies_rec(*it)==tvt(true))
620  return tvt(true);
621  }
622  else if(expr.id()==ID_le ||
623  expr.id()==ID_lt ||
624  expr.id()==ID_equal ||
625  expr.id()==ID_notequal)
626  {
627  const auto &rel = to_binary_relation_expr(expr);
628 
629  std::pair<unsigned, unsigned> p;
630 
631  bool ob0 = get_object(rel.lhs(), p.first);
632  bool ob1 = get_object(rel.rhs(), p.second);
633 
634  if(ob0 || ob1)
635  return tvt::unknown();
636 
637  tvt r;
638 
639  if(rel.id() == ID_le)
640  {
641  r=is_le(p);
642  if(!r.is_unknown())
643  return r;
644 
645  boundst b0, b1;
646  get_bounds(p.first, b0);
647  get_bounds(p.second, b1);
648 
649  return b0<=b1;
650  }
651  else if(rel.id() == ID_lt)
652  {
653  r=is_lt(p);
654  if(!r.is_unknown())
655  return r;
656 
657  boundst b0, b1;
658  get_bounds(p.first, b0);
659  get_bounds(p.second, b1);
660 
661  return b0<b1;
662  }
663  else if(rel.id() == ID_equal)
664  return is_eq(p);
665  else if(rel.id() == ID_notequal)
666  return is_ne(p);
667  else
668  UNREACHABLE;
669  }
670 
671  return tvt::unknown();
672 }
673 
674 void invariant_sett::get_bounds(unsigned a, boundst &bounds) const
675 {
676  // unbounded
677  bounds=boundst();
678 
679  {
680  const exprt &e_a = object_store.get_expr(a);
681  const auto tmp = numeric_cast<mp_integer>(e_a);
682  if(tmp.has_value())
683  {
684  bounds = boundst(*tmp);
685  return;
686  }
687 
688  if(e_a.type().id()==ID_unsignedbv)
689  bounds=lower_interval(mp_integer(0));
690  }
691 
692  bounds_mapt::const_iterator it=bounds_map.find(a);
693 
694  if(it!=bounds_map.end())
695  bounds=it->second;
696 }
697 
698 void invariant_sett::nnf(exprt &expr, bool negate)
699 {
700  if(expr.type().id()!=ID_bool)
701  throw "nnf: non-Boolean expression";
702 
703  if(expr.is_true())
704  {
705  if(negate)
706  expr=false_exprt();
707  }
708  else if(expr.is_false())
709  {
710  if(negate)
711  expr=true_exprt();
712  }
713  else if(expr.id()==ID_not)
714  {
715  nnf(to_not_expr(expr).op(), !negate);
716  exprt tmp;
717  tmp.swap(to_not_expr(expr).op());
718  expr.swap(tmp);
719  }
720  else if(expr.id()==ID_and)
721  {
722  if(negate)
723  expr.id(ID_or);
724 
725  Forall_operands(it, expr)
726  nnf(*it, negate);
727  }
728  else if(expr.id()==ID_or)
729  {
730  if(negate)
731  expr.id(ID_and);
732 
733  Forall_operands(it, expr)
734  nnf(*it, negate);
735  }
736  else if(expr.id()==ID_typecast)
737  {
738  const auto &typecast_expr = to_typecast_expr(expr);
739 
740  if(
741  typecast_expr.op().type().id() == ID_unsignedbv ||
742  typecast_expr.op().type().id() == ID_signedbv)
743  {
744  equal_exprt tmp(
745  typecast_expr.op(), from_integer(0, typecast_expr.op().type()));
746  nnf(tmp, !negate);
747  expr.swap(tmp);
748  }
749  else if(negate)
750  {
751  expr = boolean_negate(expr);
752  }
753  }
754  else if(expr.id()==ID_le)
755  {
756  if(negate)
757  {
758  // !a<=b <-> !b=>a <-> b<a
759  expr.id(ID_lt);
760  auto &rel = to_binary_relation_expr(expr);
761  std::swap(rel.lhs(), rel.rhs());
762  }
763  }
764  else if(expr.id()==ID_lt)
765  {
766  if(negate)
767  {
768  // !a<b <-> !b>a <-> b<=a
769  expr.id(ID_le);
770  auto &rel = to_binary_relation_expr(expr);
771  std::swap(rel.lhs(), rel.rhs());
772  }
773  }
774  else if(expr.id()==ID_ge)
775  {
776  if(negate)
777  expr.id(ID_lt);
778  else
779  {
780  expr.id(ID_le);
781  auto &rel = to_binary_relation_expr(expr);
782  std::swap(rel.lhs(), rel.rhs());
783  }
784  }
785  else if(expr.id()==ID_gt)
786  {
787  if(negate)
788  expr.id(ID_le);
789  else
790  {
791  expr.id(ID_lt);
792  auto &rel = to_binary_relation_expr(expr);
793  std::swap(rel.lhs(), rel.rhs());
794  }
795  }
796  else if(expr.id()==ID_equal)
797  {
798  if(negate)
799  expr.id(ID_notequal);
800  }
801  else if(expr.id()==ID_notequal)
802  {
803  if(negate)
804  expr.id(ID_equal);
805  }
806  else if(negate)
807  {
808  expr = boolean_negate(expr);
809  }
810 }
811 
813  exprt &expr) const
814 {
815  if(expr.id()==ID_address_of)
816  return;
817 
818  Forall_operands(it, expr)
819  simplify(*it);
820 
821  if(expr.id()==ID_symbol ||
822  expr.id()==ID_member)
823  {
824  exprt tmp=get_constant(expr);
825  if(tmp.is_not_nil())
826  expr.swap(tmp);
827  }
828 }
829 
831 {
832  unsigned a;
833 
834  if(!get_object(expr, a))
835  {
836  // bounds?
837  bounds_mapt::const_iterator it=bounds_map.find(a);
838 
839  if(it!=bounds_map.end())
840  {
841  if(it->second.singleton())
842  return from_integer(it->second.get_lower(), expr.type());
843  }
844 
845  unsigned r=eq_set.find(a);
846 
847  // is it a constant?
848  for(std::size_t i=0; i<eq_set.size(); i++)
849  if(eq_set.find(i)==r)
850  {
851  const exprt &e = object_store.get_expr(i);
852 
853  if(e.is_constant())
854  {
855  const mp_integer value =
856  numeric_cast_v<mp_integer>(to_constant_expr(e));
857 
858  if(expr.type().id()==ID_pointer)
859  {
860  if(value==0)
861  return null_pointer_exprt(to_pointer_type(expr.type()));
862  }
863  else
864  return from_integer(value, expr.type());
865  }
867  {
868  if(e.type()==expr.type())
869  return e;
870 
871  return typecast_exprt(e, expr.type());
872  }
873  }
874  }
875 
876  return static_cast<const exprt &>(get_nil_irep());
877 }
878 
879 std::string inv_object_storet::to_string(unsigned a) const
880 {
881  return id2string(map[a]);
882 }
883 
884 std::string invariant_sett::to_string(unsigned a) const
885 {
886  return object_store.to_string(a);
887 }
888 
890 {
891  if(other.threaded &&
892  !threaded)
893  {
894  make_threaded();
895  return true; // change
896  }
897 
898  if(threaded)
899  return false; // no change
900 
901  if(other.is_false)
902  return false; // no change
903 
904  if(is_false)
905  {
906  // copy
907  is_false=false;
908  eq_set=other.eq_set;
909  le_set=other.le_set;
910  ne_set=other.ne_set;
911  bounds_map=other.bounds_map;
912 
913  return true; // change
914  }
915 
916  // equalities first
917  unsigned old_eq_roots=eq_set.count_roots();
918 
919  eq_set.intersection(other.eq_set);
920 
921  // inequalities
922  std::size_t old_ne_set=ne_set.size();
923  std::size_t old_le_set=le_set.size();
924 
925  intersection(ne_set, other.ne_set);
926  intersection(le_set, other.le_set);
927 
928  // bounds
930  return true;
931 
932  if(old_eq_roots!=eq_set.count_roots() ||
933  old_ne_set!=ne_set.size() ||
934  old_le_set!=le_set.size())
935  return true;
936 
937  return false; // no change
938 }
939 
941 {
942  bool changed=false;
943 
944  for(bounds_mapt::iterator
945  it=bounds_map.begin();
946  it!=bounds_map.end();
947  ) // no it++
948  {
949  bounds_mapt::const_iterator o_it=other.find(it->first);
950 
951  if(o_it==other.end())
952  {
953  bounds_mapt::iterator next(it);
954  next++;
955  bounds_map.erase(it);
956  it=next;
957  changed=true;
958  }
959  else
960  {
961  boundst old(it->second);
962  it->second.approx_union_with(o_it->second);
963  if(it->second!=old)
964  changed=true;
965  it++;
966  }
967  }
968 
969  return changed;
970 }
971 
972 void invariant_sett::modifies(unsigned a)
973 {
974  eq_set.isolate(a);
975  remove(ne_set, a);
976  remove(le_set, a);
977  bounds_map.erase(a);
978 }
979 
981 {
982  if(lhs.id()==ID_symbol ||
983  lhs.id()==ID_member)
984  {
985  unsigned a;
986  if(!get_object(lhs, a))
987  modifies(a);
988  }
989  else if(lhs.id()==ID_index)
990  {
991  // we don't track arrays
992  }
993  else if(lhs.id()==ID_dereference)
994  {
995  // be very, very conservative for now
996  make_true();
997  }
998  else if(lhs.id()=="object_value")
999  {
1000  // be very, very conservative for now
1001  make_true();
1002  }
1003  else if(lhs.id()==ID_if)
1004  {
1005  // we just assume both are changed
1006  modifies(to_if_expr(lhs).op1());
1007  modifies(to_if_expr(lhs).op2());
1008  }
1009  else if(lhs.id()==ID_typecast)
1010  {
1011  // just go down
1012  modifies(to_typecast_expr(lhs).op());
1013  }
1014  else if(lhs.id()=="valid_object")
1015  {
1016  }
1017  else if(lhs.id()=="dynamic_size")
1018  {
1019  }
1020  else if(lhs.id()==ID_byte_extract_little_endian ||
1021  lhs.id()==ID_byte_extract_big_endian)
1022  {
1023  // just go down
1024  modifies(to_byte_extract_expr(lhs).op0());
1025  }
1026  else if(lhs.id() == ID_null_object ||
1027  lhs.id() == "is_zero_string" ||
1028  lhs.id() == "zero_string" ||
1029  lhs.id() == "zero_string_length")
1030  {
1031  // ignore
1032  }
1033  else
1034  throw "modifies: unexpected lhs: "+lhs.id_string();
1035 }
1036 
1038  const exprt &lhs,
1039  const exprt &rhs)
1040 {
1041  equal_exprt equality(lhs, rhs);
1042 
1043  // first evaluate RHS
1044  simplify(equality.rhs());
1045  ::simplify(equality.rhs(), ns);
1046 
1047  // now kill LHS
1048  modifies(lhs);
1049 
1050  // and put it back
1051  strengthen(equality);
1052 }
1053 
1055 {
1056  const irep_idt &statement=code.get(ID_statement);
1057 
1058  if(statement==ID_block)
1059  {
1060  forall_operands(it, code)
1061  apply_code(to_code(*it));
1062  }
1063  else if(statement==ID_assign)
1064  {
1065  if(code.operands().size()!=2)
1066  throw "assignment expected to have two operands";
1067 
1068  assignment(code.op0(), code.op1());
1069  }
1070  else if(statement==ID_decl)
1071  {
1072  if(code.operands().size()==2)
1073  assignment(code.op0(), code.op1());
1074  else
1075  modifies(code.op0());
1076  }
1077  else if(statement==ID_expression)
1078  {
1079  // this never modifies anything
1080  }
1081  else if(statement==ID_function_call)
1082  {
1083  // may be a disaster
1084  make_true();
1085  }
1086  else if(statement==ID_cpp_delete ||
1087  statement==ID_cpp_delete_array)
1088  {
1089  // does nothing
1090  }
1091  else if(statement==ID_printf)
1092  {
1093  // does nothing
1094  }
1095  else if(statement=="lock" ||
1096  statement=="unlock" ||
1097  statement==ID_asm)
1098  {
1099  // ignore for now
1100  }
1101  else
1102  {
1103  std::cerr << code.pretty() << '\n';
1104  throw "invariant_sett: unexpected statement: "+id2string(statement);
1105  }
1106 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:141
invariant_sett::strengthen
void strengthen(const exprt &expr)
Definition: invariant_set.cpp:380
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: bitvector_types.h:191
invariant_sett::boundst
interval_templatet< mp_integer > boundst
Definition: invariant_set.h:88
unsigned_union_find::find
size_type find(size_type a) const
Definition: union_find.cpp:141
binary_exprt::rhs
exprt & rhs()
Definition: std_expr.h:590
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
arith_tools.h
codet::op0
exprt & op0()
Definition: expr.h:103
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:302
invariant_sett::implies
tvt implies(const exprt &expr) const
Definition: invariant_set.cpp:583
invariant_sett::ineq_sett
std::set< std::pair< unsigned, unsigned > > ineq_sett
Definition: invariant_set.h:81
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
invariant_sett::get_bounds
void get_bounds(unsigned a, boundst &dest) const
Definition: invariant_set.cpp:674
unsigned_union_find::check_index
void check_index(size_type a)
Definition: union_find.h:111
typet
The type of an expression, extends irept.
Definition: type.h:28
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:501
invariant_sett::add_type_bounds
void add_type_bounds(const exprt &expr, const typet &type)
Definition: invariant_set.cpp:358
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
invariant_sett::make_threaded
void make_threaded()
Definition: invariant_set.h:130
invariant_sett::is_lt
tvt is_lt(std::pair< unsigned, unsigned > p) const
Definition: invariant_set.h:232
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1296
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2151
invariant_sett::object_store
inv_object_storet & object_store
Definition: invariant_set.h:184
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
invariant_sett::threaded
bool threaded
Definition: invariant_set.h:92
unsigned_union_find::size
size_type size() const
Definition: union_find.h:97
exprt
Base class for all expressions.
Definition: expr.h:54
inv_object_storet::to_string
std::string to_string(unsigned n) const
Definition: invariant_set.cpp:879
unsigned_union_find::intersection
void intersection(const unsigned_union_find &other)
Definition: union_find.cpp:120
invariant_sett::is_le
tvt is_le(std::pair< unsigned, unsigned > p) const
Definition: invariant_set.cpp:297
irep_idt
dstringt irep_idt
Definition: irep.h:37
invariant_sett::output
void output(std::ostream &out) const
Definition: invariant_set.cpp:315
invariant_sett::make_union_bounds_map
bool make_union_bounds_map(const bounds_mapt &other)
Definition: invariant_set.cpp:940
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:60
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: bitvector_types.h:32
namespace.h
inv_object_storet::map
mapt map
Definition: invariant_set.h:59
equal_exprt
Equality.
Definition: std_expr.h:1139
invariant_sett::nnf
static void nnf(exprt &expr, bool negate=false)
Definition: invariant_set.cpp:698
inv_object_storet::entries
std::vector< entryt > entries
Definition: invariant_set.h:67
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:69
invariant_sett::apply_code
void apply_code(const codet &code)
Definition: invariant_set.cpp:1054
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
interval_templatet
Definition: interval_template.h:20
base_exceptions.h
Generic exception types primarily designed for use with invariants.
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
inv_object_storet::add
unsigned add(const exprt &expr)
Definition: invariant_set.cpp:65
unsigned_union_find::count
size_type count(size_type a) const
Definition: union_find.h:103
byte_operators.h
Expression classes for byte-level operators.
invariant_sett::intersection
static void intersection(ineq_sett &dest, const ineq_sett &other)
Definition: invariant_set.h:146
invariant_sett::is_false
bool is_false
Definition: invariant_set.h:93
invariant_sett::eq_set
unsigned_union_find eq_set
Definition: invariant_set.h:78
invariant_sett::add_le
void add_le(const std::pair< unsigned, unsigned > &p)
Definition: invariant_set.h:255
null_pointer_exprt
The null pointer constant.
Definition: pointer_expr.h:461
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
unsigned_union_find::make_union
void make_union(size_type a, size_type b)
Definition: union_find.cpp:13
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
language_util.h
invariant_sett::add_eq
void add_eq(const std::pair< unsigned, unsigned > &eq)
Definition: invariant_set.cpp:208
inv_object_storet::get_expr
const exprt & get_expr(unsigned n) const
Definition: invariant_set.h:45
boolean_negate
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:129
inv_object_storet::get
bool get(const exprt &expr, unsigned &n)
Definition: invariant_set.cpp:36
std_types.h
Pre-defined types.
pointer_expr.h
API to expression classes for Pointers.
irept::id_string
const std::string & id_string() const
Definition: irep.h:410
exprt::op1
exprt & op1()
Definition: expr.h:106
to_notequal_expr
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1222
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
invariant_sett::ns
const namespacet & ns
Definition: invariant_set.h:185
irept::swap
void swap(irept &irep)
Definition: irep.h:453
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
irept::id
const irep_idt & id() const
Definition: irep.h:407
invariant_sett::modifies
void modifies(const exprt &lhs)
Definition: invariant_set.cpp:980
inv_object_storet::is_constant
bool is_constant(unsigned n) const
Definition: invariant_set.cpp:82
tvt::unknown
static tvt unknown()
Definition: threeval.h:33
false_exprt
The Boolean constant false.
Definition: std_expr.h:2725
numberingt::get_number
optionalt< number_type > get_number(const key_type &a) const
Definition: numbering.h:50
invariant_sett::to_string
std::string to_string(unsigned a) const
Definition: invariant_set.cpp:884
invariant_sett::remove
static void remove(ineq_sett &dest, unsigned a)
Definition: invariant_set.h:162
invariant_sett::implies_rec
tvt implies_rec(const exprt &expr) const
Definition: invariant_set.cpp:590
invariant_sett::add_ne
void add_ne(const std::pair< unsigned, unsigned > &p)
Definition: invariant_set.h:260
tvt
Definition: threeval.h:20
invariant_sett::has_le
bool has_le(const std::pair< unsigned, unsigned > &p) const
Definition: invariant_set.h:219
inv_object_storet::output
void output(std::ostream &out) const
Definition: invariant_set.cpp:30
simplify_expr.h
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:837
invariant_sett::add
void add(const std::pair< unsigned, unsigned > &p, ineq_sett &dest)
Definition: invariant_set.cpp:186
lower_interval
interval_templatet< T > lower_interval(const T &l)
Definition: interval_template.h:262
invariant_sett::bounds_mapt
std::map< unsigned, boundst > bounds_mapt
Definition: invariant_set.h:89
invariant_sett::make_false
void make_false()
Definition: invariant_set.h:122
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2527
expr_util.h
Deprecated expression utility functions.
irept::get_string
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:420
invariant_sett::le_set
ineq_sett le_set
Definition: invariant_set.h:82
invariant_sett::ne_set
ineq_sett ne_set
Definition: invariant_set.h:85
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:225
invariant_sett
Definition: invariant_set.h:75
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:52
to_not_expr
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2066
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
invariant_sett::assignment
void assignment(const exprt &lhs, const exprt &rhs)
Definition: invariant_set.cpp:1037
numberingt::number
number_type number(const key_type &a)
Definition: numbering.h:37
inv_object_storet::build_string
std::string build_string(const exprt &expr) const
Definition: invariant_set.cpp:94
unsigned_union_find::count_roots
size_type count_roots() const
Definition: union_find.h:118
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:100
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1814
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:53
invariant_sett::simplify
void simplify(exprt &expr) const
Definition: invariant_set.cpp:812
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:195
to_equal_expr
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1179
invariant_sett::get_object
bool get_object(const exprt &expr, unsigned &n) const
Definition: invariant_set.cpp:155
invariant_sett::make_union
bool make_union(const invariant_sett &other_invariants)
Definition: invariant_set.cpp:889
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2611
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:26
invariant_sett::is_ne
tvt is_ne(std::pair< unsigned, unsigned > p) const
Definition: invariant_set.h:248
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:367
exprt::operands
operandst & operands()
Definition: expr.h:96
r
static int8_t r
Definition: irep_hash.h:59
unsigned_union_find::is_root
bool is_root(size_type a) const
Definition: union_find.h:82
codet::op1
exprt & op1()
Definition: expr.h:106
invariant_sett::get_constant
exprt get_constant(const exprt &expr) const
Definition: invariant_set.cpp:830
inv_object_storet::is_constant_address_rec
static bool is_constant_address_rec(const exprt &expr)
Definition: invariant_set.cpp:170
symbol_table.h
Author: Diffblue Ltd.
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1780
true_exprt
The Boolean constant true.
Definition: std_expr.h:2716
inv_object_storet::ns
const namespacet & ns
Definition: invariant_set.h:56
unsigned_union_find::isolate
void isolate(size_type a)
Definition: union_find.cpp:41
invariant_sett::strengthen_rec
void strengthen_rec(const exprt &expr)
Definition: invariant_set.cpp:387
std_expr.h
API to expression classes.
invariant_sett::bounds_map
bounds_mapt bounds_map
Definition: invariant_set.h:90
invariant_sett::is_eq
tvt is_eq(std::pair< unsigned, unsigned > p) const
Definition: invariant_set.cpp:283
to_binary_relation_expr
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:723
invariant_set.h
Value Set.
c_types.h
inv_object_storet::is_constant_address
static bool is_constant_address(const exprt &expr)
Definition: invariant_set.cpp:162
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
invariant_sett::add_bounds
void add_bounds(unsigned a, const boundst &bound)
Definition: invariant_set.h:193
invariant_sett::has_ne
bool has_ne(const std::pair< unsigned, unsigned > &p) const
Definition: invariant_set.h:224
invariant_sett::has_eq
bool has_eq(const std::pair< unsigned, unsigned > &p) const
Definition: invariant_set.h:214
numberingt< irep_idt >::number_type
std::size_t number_type
Definition: numbering.h:24
upper_interval
interval_templatet< T > upper_interval(const T &u)
Definition: interval_template.h:253
invariant_sett::make_true
void make_true()
Definition: invariant_set.h:114
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2700
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106