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