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