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