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