cprover
goto_check.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: GOTO Programs
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_check.h"
13 
14 #include <algorithm>
15 
16 #include <util/simplify_expr.h>
17 #include <util/array_name.h>
18 #include <util/ieee_float.h>
19 #include <util/arith_tools.h>
20 #include <util/expr_util.h>
21 #include <util/find_symbols.h>
22 #include <util/std_expr.h>
23 #include <util/std_types.h>
24 #include <util/guard.h>
25 #include <util/base_type.h>
28 #include <util/cprover_prefix.h>
29 #include <util/options.h>
30 
31 #include <langapi/language.h>
32 #include <langapi/mode.h>
33 
35 
37 
39 {
40 public:
42  const namespacet &_ns,
43  const optionst &_options):
44  ns(_ns),
46  {
47  enable_bounds_check=_options.get_bool_option("bounds-check");
48  enable_pointer_check=_options.get_bool_option("pointer-check");
49  enable_memory_leak_check=_options.get_bool_option("memory-leak-check");
50  enable_div_by_zero_check=_options.get_bool_option("div-by-zero-check");
52  _options.get_bool_option("signed-overflow-check");
54  _options.get_bool_option("unsigned-overflow-check");
56  _options.get_bool_option("pointer-overflow-check");
57  enable_conversion_check=_options.get_bool_option("conversion-check");
59  _options.get_bool_option("undefined-shift-check");
61  _options.get_bool_option("float-overflow-check");
62  enable_simplify=_options.get_bool_option("simplify");
63  enable_nan_check=_options.get_bool_option("nan-check");
64  retain_trivial=_options.get_bool_option("retain-trivial");
65  enable_assert_to_assume=_options.get_bool_option("assert-to-assume");
66  enable_assertions=_options.get_bool_option("assertions");
67  enable_built_in_assertions=_options.get_bool_option("built-in-assertions");
68  enable_assumptions=_options.get_bool_option("assumptions");
69  error_labels=_options.get_list_option("error-label");
70  }
71 
73 
74  void goto_check(goto_functiont &goto_function, const irep_idt &mode);
75 
76  void collect_allocations(const goto_functionst &goto_functions);
77 
78 protected:
79  const namespacet &ns;
82 
83  void check_rec(
84  const exprt &expr,
85  guardt &guard,
86  bool address);
87  void check(const exprt &expr);
88 
89  void bounds_check(const index_exprt &expr, const guardt &guard);
90  void div_by_zero_check(const div_exprt &expr, const guardt &guard);
91  void mod_by_zero_check(const mod_exprt &expr, const guardt &guard);
92  void undefined_shift_check(const shift_exprt &expr, const guardt &guard);
93  void pointer_rel_check(const exprt &expr, const guardt &guard);
94  void pointer_overflow_check(const exprt &expr, const guardt &guard);
96  const dereference_exprt &expr,
97  const guardt &guard,
98  const exprt &access_lb,
99  const exprt &access_ub);
100  void integer_overflow_check(const exprt &expr, const guardt &guard);
101  void conversion_check(const exprt &expr, const guardt &guard);
102  void float_overflow_check(const exprt &expr, const guardt &guard);
103  void nan_check(const exprt &expr, const guardt &guard);
104 
105  std::string array_name(const exprt &expr);
106 
107  void add_guarded_claim(
108  const exprt &expr,
109  const std::string &comment,
110  const std::string &property_class,
111  const source_locationt &,
112  const exprt &src_expr,
113  const guardt &guard);
114 
116  typedef std::set<exprt> assertionst;
118 
119  void invalidate(const exprt &lhs);
120 
138 
141 
142  typedef std::pair<exprt, exprt> allocationt;
143  typedef std::list<allocationt> allocationst;
145 
147 };
148 
150  const goto_functionst &goto_functions)
151 {
153  return;
154 
155  forall_goto_functions(itf, goto_functions)
156  forall_goto_program_instructions(it, itf->second.body)
157  {
158  const goto_programt::instructiont &instruction=*it;
159  if(!instruction.is_function_call())
160  continue;
161 
162  const code_function_callt &call=
163  to_code_function_call(instruction.code);
164  if(call.function().id()!=ID_symbol ||
165  to_symbol_expr(call.function()).get_identifier()!=
166  CPROVER_PREFIX "allocated_memory")
167  continue;
168 
169  const code_function_callt::argumentst &args= call.arguments();
170  if(args.size()!=2 ||
171  args[0].type().id()!=ID_unsignedbv ||
172  args[1].type().id()!=ID_unsignedbv)
173  throw "expected two unsigned arguments to "
174  CPROVER_PREFIX "allocated_memory";
175 
176  assert(args[0].type()==args[1].type());
177  allocations.push_back({args[0], args[1]});
178  }
179 }
180 
182 {
183  if(lhs.id()==ID_index)
185  else if(lhs.id()==ID_member)
187  else if(lhs.id()==ID_symbol)
188  {
189  // clear all assertions about 'symbol'
190  find_symbols_sett find_symbols_set;
191  find_symbols_set.insert(to_symbol_expr(lhs).get_identifier());
192 
193  for(assertionst::iterator
194  it=assertions.begin();
195  it!=assertions.end();
196  ) // no it++
197  {
198  assertionst::iterator next=it;
199  next++;
200 
201  if(has_symbol(*it, find_symbols_set) || has_subexpr(*it, ID_dereference))
202  assertions.erase(it);
203 
204  it=next;
205  }
206  }
207  else
208  {
209  // give up, clear all
210  assertions.clear();
211  }
212 }
213 
215  const div_exprt &expr,
216  const guardt &guard)
217 {
219  return;
220 
221  // add divison by zero subgoal
222 
223  exprt zero=from_integer(0, expr.op1().type());
224 
225  if(zero.is_nil())
226  throw "no zero of argument type of operator "+expr.id_string();
227 
228  const notequal_exprt inequality(expr.op1(), zero);
229 
231  inequality,
232  "division by zero",
233  "division-by-zero",
234  expr.find_source_location(),
235  expr,
236  guard);
237 }
238 
240  const shift_exprt &expr,
241  const guardt &guard)
242 {
244  return;
245 
246  // Undefined for all types and shifts if distance exceeds width,
247  // and also undefined for negative distances.
248 
249  const typet &distance_type=
250  ns.follow(expr.distance().type());
251 
252  if(distance_type.id()==ID_signedbv)
253  {
254  binary_relation_exprt inequality(
255  expr.distance(), ID_ge, from_integer(0, distance_type));
256 
258  inequality,
259  "shift distance is negative",
260  "undefined-shift",
261  expr.find_source_location(),
262  expr,
263  guard);
264  }
265 
266  const typet &op_type=
267  ns.follow(expr.op().type());
268 
269  if(op_type.id()==ID_unsignedbv || op_type.id()==ID_signedbv)
270  {
271  exprt width_expr=
272  from_integer(to_bitvector_type(op_type).get_width(), distance_type);
273 
274  if(width_expr.is_nil())
275  throw "no number for width for operator "+expr.id_string();
276 
277  binary_relation_exprt inequality(
278  expr.distance(), ID_lt, width_expr);
279 
281  inequality,
282  "shift distance too large",
283  "undefined-shift",
284  expr.find_source_location(),
285  expr,
286  guard);
287 
288  if(op_type.id()==ID_signedbv && expr.id()==ID_shl)
289  {
290  binary_relation_exprt inequality(
291  expr.op(), ID_ge, from_integer(0, op_type));
292 
294  inequality,
295  "shift operand is negative",
296  "undefined-shift",
297  expr.find_source_location(),
298  expr,
299  guard);
300  }
301  }
302  else
303  {
305  false_exprt(),
306  "shift of non-integer type",
307  "undefined-shift",
308  expr.find_source_location(),
309  expr,
310  guard);
311  }
312 }
313 
315  const mod_exprt &expr,
316  const guardt &guard)
317 {
319  return;
320 
321  // add divison by zero subgoal
322 
323  exprt zero=from_integer(0, expr.op1().type());
324 
325  if(zero.is_nil())
326  throw "no zero of argument type of operator "+expr.id_string();
327 
328  const notequal_exprt inequality(expr.op1(), zero);
329 
331  inequality,
332  "division by zero",
333  "division-by-zero",
334  expr.find_source_location(),
335  expr,
336  guard);
337 }
338 
340  const exprt &expr,
341  const guardt &guard)
342 {
344  return;
345 
346  // First, check type.
347  const typet &type=ns.follow(expr.type());
348 
349  if(type.id()!=ID_signedbv &&
350  type.id()!=ID_unsignedbv)
351  return;
352 
353  if(expr.id()==ID_typecast)
354  {
355  // conversion to signed int may overflow
356 
357  if(expr.operands().size()!=1)
358  throw "typecast takes one operand";
359 
360  const typet &old_type=ns.follow(expr.op0().type());
361 
362  if(type.id()==ID_signedbv)
363  {
364  std::size_t new_width=to_signedbv_type(type).get_width();
365 
366  if(old_type.id()==ID_signedbv) // signed -> signed
367  {
368  std::size_t old_width=to_signedbv_type(old_type).get_width();
369  if(new_width>=old_width)
370  return; // always ok
371 
372  const binary_relation_exprt no_overflow_upper(
373  expr.op0(),
374  ID_le,
375  from_integer(power(2, new_width - 1) - 1, old_type));
376 
377  const binary_relation_exprt no_overflow_lower(
378  expr.op0(), ID_ge, from_integer(-power(2, new_width - 1), old_type));
379 
381  and_exprt(no_overflow_lower, no_overflow_upper),
382  "arithmetic overflow on signed type conversion",
383  "overflow",
384  expr.find_source_location(),
385  expr,
386  guard);
387  }
388  else if(old_type.id()==ID_unsignedbv) // unsigned -> signed
389  {
390  std::size_t old_width=to_unsignedbv_type(old_type).get_width();
391  if(new_width>=old_width+1)
392  return; // always ok
393 
394  const binary_relation_exprt no_overflow_upper(
395  expr.op0(),
396  ID_le,
397  from_integer(power(2, new_width - 1) - 1, old_type));
398 
400  no_overflow_upper,
401  "arithmetic overflow on unsigned to signed type conversion",
402  "overflow",
403  expr.find_source_location(),
404  expr,
405  guard);
406  }
407  else if(old_type.id()==ID_floatbv) // float -> signed
408  {
409  // Note that the fractional part is truncated!
410  ieee_floatt upper(to_floatbv_type(old_type));
411  upper.from_integer(power(2, new_width-1));
412  const binary_relation_exprt no_overflow_upper(
413  expr.op0(), ID_lt, upper.to_expr());
414 
415  ieee_floatt lower(to_floatbv_type(old_type));
416  lower.from_integer(-power(2, new_width-1)-1);
417  const binary_relation_exprt no_overflow_lower(
418  expr.op0(), ID_gt, lower.to_expr());
419 
421  and_exprt(no_overflow_lower, no_overflow_upper),
422  "arithmetic overflow on float to signed integer type conversion",
423  "overflow",
424  expr.find_source_location(),
425  expr,
426  guard);
427  }
428  }
429  else if(type.id()==ID_unsignedbv)
430  {
431  std::size_t new_width=to_unsignedbv_type(type).get_width();
432 
433  if(old_type.id()==ID_signedbv) // signed -> unsigned
434  {
435  std::size_t old_width=to_signedbv_type(old_type).get_width();
436 
437  if(new_width>=old_width-1)
438  {
439  // only need lower bound check
440  const binary_relation_exprt no_overflow_lower(
441  expr.op0(), ID_ge, from_integer(0, old_type));
442 
444  no_overflow_lower,
445  "arithmetic overflow on signed to unsigned type conversion",
446  "overflow",
447  expr.find_source_location(),
448  expr,
449  guard);
450  }
451  else
452  {
453  // need both
454  const binary_relation_exprt no_overflow_upper(
455  expr.op0(), ID_le, from_integer(power(2, new_width) - 1, old_type));
456 
457  const binary_relation_exprt no_overflow_lower(
458  expr.op0(), ID_ge, from_integer(0, old_type));
459 
461  and_exprt(no_overflow_lower, no_overflow_upper),
462  "arithmetic overflow on signed to unsigned type conversion",
463  "overflow",
464  expr.find_source_location(),
465  expr,
466  guard);
467  }
468  }
469  else if(old_type.id()==ID_unsignedbv) // unsigned -> unsigned
470  {
471  std::size_t old_width=to_unsignedbv_type(old_type).get_width();
472  if(new_width>=old_width)
473  return; // always ok
474 
475  const binary_relation_exprt no_overflow_upper(
476  expr.op0(), ID_le, from_integer(power(2, new_width) - 1, old_type));
477 
479  no_overflow_upper,
480  "arithmetic overflow on unsigned to unsigned type conversion",
481  "overflow",
482  expr.find_source_location(),
483  expr,
484  guard);
485  }
486  else if(old_type.id()==ID_floatbv) // float -> unsigned
487  {
488  // Note that the fractional part is truncated!
489  ieee_floatt upper(to_floatbv_type(old_type));
490  upper.from_integer(power(2, new_width)-1);
491  const binary_relation_exprt no_overflow_upper(
492  expr.op0(), ID_lt, upper.to_expr());
493 
494  ieee_floatt lower(to_floatbv_type(old_type));
495  lower.from_integer(-1);
496  const binary_relation_exprt no_overflow_lower(
497  expr.op0(), ID_gt, lower.to_expr());
498 
500  and_exprt(no_overflow_lower, no_overflow_upper),
501  "arithmetic overflow on float to unsigned integer type conversion",
502  "overflow",
503  expr.find_source_location(),
504  expr,
505  guard);
506  }
507  }
508  }
509 }
510 
512  const exprt &expr,
513  const guardt &guard)
514 {
517  return;
518 
519  // First, check type.
520  const typet &type=ns.follow(expr.type());
521 
522  if(type.id()==ID_signedbv && !enable_signed_overflow_check)
523  return;
524 
525  if(type.id()==ID_unsignedbv && !enable_unsigned_overflow_check)
526  return;
527 
528  // add overflow subgoal
529 
530  if(expr.id()==ID_div)
531  {
532  assert(expr.operands().size()==2);
533 
534  // undefined for signed division INT_MIN/-1
535  if(type.id()==ID_signedbv)
536  {
537  equal_exprt int_min_eq(
538  expr.op0(), to_signedbv_type(type).smallest_expr());
539 
540  equal_exprt minus_one_eq(
541  expr.op1(), from_integer(-1, type));
542 
544  not_exprt(and_exprt(int_min_eq, minus_one_eq)),
545  "arithmetic overflow on signed division",
546  "overflow",
547  expr.find_source_location(),
548  expr,
549  guard);
550  }
551 
552  return;
553  }
554  else if(expr.id()==ID_mod)
555  {
556  // these can't overflow
557  return;
558  }
559  else if(expr.id()==ID_unary_minus)
560  {
561  if(type.id()==ID_signedbv)
562  {
563  // overflow on unary- can only happen with the smallest
564  // representable number 100....0
565 
566  equal_exprt int_min_eq(
567  expr.op0(), to_signedbv_type(type).smallest_expr());
568 
570  not_exprt(int_min_eq),
571  "arithmetic overflow on signed unary minus",
572  "overflow",
573  expr.find_source_location(),
574  expr,
575  guard);
576  }
577 
578  return;
579  }
580 
581  exprt overflow("overflow-"+expr.id_string(), bool_typet());
582  overflow.operands()=expr.operands();
583 
584  if(expr.operands().size()>=3)
585  {
586  // The overflow checks are binary!
587  // We break these up.
588 
589  for(std::size_t i=1; i<expr.operands().size(); i++)
590  {
591  exprt tmp;
592 
593  if(i==1)
594  tmp=expr.op0();
595  else
596  {
597  tmp=expr;
598  tmp.operands().resize(i);
599  }
600 
601  overflow.operands().resize(2);
602  overflow.op0()=tmp;
603  overflow.op1()=expr.operands()[i];
604 
605  std::string kind=
606  type.id()==ID_unsignedbv?"unsigned":"signed";
607 
609  not_exprt(overflow),
610  "arithmetic overflow on "+kind+" "+expr.id_string(),
611  "overflow",
612  expr.find_source_location(),
613  expr,
614  guard);
615  }
616  }
617  else
618  {
619  std::string kind=
620  type.id()==ID_unsignedbv?"unsigned":"signed";
621 
623  not_exprt(overflow),
624  "arithmetic overflow on "+kind+" "+expr.id_string(),
625  "overflow",
626  expr.find_source_location(),
627  expr,
628  guard);
629  }
630 }
631 
633  const exprt &expr,
634  const guardt &guard)
635 {
637  return;
638 
639  // First, check type.
640  const typet &type=ns.follow(expr.type());
641 
642  if(type.id()!=ID_floatbv)
643  return;
644 
645  // add overflow subgoal
646 
647  if(expr.id()==ID_typecast)
648  {
649  // Can overflow if casting from larger
650  // to smaller type.
651  assert(expr.operands().size()==1);
652 
653  if(ns.follow(expr.op0().type()).id()==ID_floatbv)
654  {
655  // float-to-float
656  const isinf_exprt op0_inf(expr.op0());
657  const isinf_exprt new_inf(expr);
658 
659  or_exprt overflow_check(op0_inf, not_exprt(new_inf));
660 
662  overflow_check,
663  "arithmetic overflow on floating-point typecast",
664  "overflow",
665  expr.find_source_location(),
666  expr,
667  guard);
668  }
669  else
670  {
671  // non-float-to-float
672  const isinf_exprt new_inf(expr);
673 
675  not_exprt(new_inf),
676  "arithmetic overflow on floating-point typecast",
677  "overflow",
678  expr.find_source_location(),
679  expr,
680  guard);
681  }
682 
683  return;
684  }
685  else if(expr.id()==ID_div)
686  {
687  assert(expr.operands().size()==2);
688 
689  // Can overflow if dividing by something small
690  const isinf_exprt new_inf(expr);
691  const isinf_exprt op0_inf(expr.op0());
692 
693  or_exprt overflow_check(op0_inf, not_exprt(new_inf));
694 
696  overflow_check,
697  "arithmetic overflow on floating-point division",
698  "overflow",
699  expr.find_source_location(),
700  expr,
701  guard);
702 
703  return;
704  }
705  else if(expr.id()==ID_mod)
706  {
707  // Can't overflow
708  return;
709  }
710  else if(expr.id()==ID_unary_minus)
711  {
712  // Can't overflow
713  return;
714  }
715  else if(expr.id()==ID_plus || expr.id()==ID_mult ||
716  expr.id()==ID_minus)
717  {
718  if(expr.operands().size()==2)
719  {
720  // Can overflow
721  const isinf_exprt new_inf(expr);
722  const isinf_exprt op0_inf(expr.op0());
723  const isinf_exprt op1_inf(expr.op1());
724 
725  or_exprt overflow_check(op0_inf, op1_inf, not_exprt(new_inf));
726 
727  std::string kind=
728  expr.id()==ID_plus?"addition":
729  expr.id()==ID_minus?"subtraction":
730  expr.id()==ID_mult?"multiplication":"";
731 
733  overflow_check,
734  "arithmetic overflow on floating-point "+kind,
735  "overflow",
736  expr.find_source_location(),
737  expr,
738  guard);
739 
740  return;
741  }
742  else if(expr.operands().size()>=3)
743  {
744  assert(expr.id()!=ID_minus);
745 
746  // break up
747  exprt tmp=make_binary(expr);
748  float_overflow_check(tmp, guard);
749  return;
750  }
751  }
752 }
753 
755  const exprt &expr,
756  const guardt &guard)
757 {
758  if(!enable_nan_check)
759  return;
760 
761  // first, check type
762  if(expr.type().id()!=ID_floatbv)
763  return;
764 
765  if(expr.id()!=ID_plus &&
766  expr.id()!=ID_mult &&
767  expr.id()!=ID_div &&
768  expr.id()!=ID_minus)
769  return;
770 
771  // add NaN subgoal
772 
773  exprt isnan;
774 
775  if(expr.id()==ID_div)
776  {
777  assert(expr.operands().size()==2);
778 
779  // there a two ways to get a new NaN on division:
780  // 0/0 = NaN and x/inf = NaN
781  // (note that x/0 = +-inf for x!=0 and x!=inf)
782  const and_exprt zero_div_zero(
783  ieee_float_equal_exprt(expr.op0(), from_integer(0, expr.op0().type())),
784  ieee_float_equal_exprt(expr.op1(), from_integer(0, expr.op1().type())));
785 
786  const isinf_exprt div_inf(expr.op1());
787 
788  isnan=or_exprt(zero_div_zero, div_inf);
789  }
790  else if(expr.id()==ID_mult)
791  {
792  if(expr.operands().size()>=3)
793  return nan_check(make_binary(expr), guard);
794 
795  assert(expr.operands().size()==2);
796 
797  // Inf * 0 is NaN
798  const and_exprt inf_times_zero(
799  isinf_exprt(expr.op0()),
800  ieee_float_equal_exprt(expr.op1(), from_integer(0, expr.op1().type())));
801 
802  const and_exprt zero_times_inf(
803  ieee_float_equal_exprt(expr.op1(), from_integer(0, expr.op1().type())),
804  isinf_exprt(expr.op0()));
805 
806  isnan=or_exprt(inf_times_zero, zero_times_inf);
807  }
808  else if(expr.id()==ID_plus)
809  {
810  if(expr.operands().size()>=3)
811  return nan_check(make_binary(expr), guard);
812 
813  assert(expr.operands().size()==2);
814 
815  // -inf + +inf = NaN and +inf + -inf = NaN,
816  // i.e., signs differ
818  exprt plus_inf=ieee_floatt::plus_infinity(spec).to_expr();
819  exprt minus_inf=ieee_floatt::minus_infinity(spec).to_expr();
820 
821  isnan=
822  or_exprt(
823  and_exprt(
824  equal_exprt(expr.op0(), minus_inf),
825  equal_exprt(expr.op1(), plus_inf)),
826  and_exprt(
827  equal_exprt(expr.op0(), plus_inf),
828  equal_exprt(expr.op1(), minus_inf)));
829  }
830  else if(expr.id()==ID_minus)
831  {
832  assert(expr.operands().size()==2);
833  // +inf - +inf = NaN and -inf - -inf = NaN,
834  // i.e., signs match
835 
837  exprt plus_inf=ieee_floatt::plus_infinity(spec).to_expr();
838  exprt minus_inf=ieee_floatt::minus_infinity(spec).to_expr();
839 
840  isnan=
841  or_exprt(
842  and_exprt(
843  equal_exprt(expr.op0(), plus_inf),
844  equal_exprt(expr.op1(), plus_inf)),
845  and_exprt(
846  equal_exprt(expr.op0(), minus_inf),
847  equal_exprt(expr.op1(), minus_inf)));
848  }
849  else
850  UNREACHABLE;
851 
852  isnan.make_not();
853 
855  isnan,
856  "NaN on "+expr.id_string(),
857  "NaN",
858  expr.find_source_location(),
859  expr,
860  guard);
861 }
862 
864  const exprt &expr,
865  const guardt &guard)
866 {
868  return;
869 
870  if(expr.operands().size()!=2)
871  throw expr.id_string()+" takes two arguments";
872 
873  if(expr.op0().type().id()==ID_pointer &&
874  expr.op1().type().id()==ID_pointer)
875  {
876  // add same-object subgoal
877 
879  {
880  exprt same_object=::same_object(expr.op0(), expr.op1());
881 
883  same_object,
884  "same object violation",
885  "pointer",
886  expr.find_source_location(),
887  expr,
888  guard);
889  }
890  }
891 }
892 
894  const exprt &expr,
895  const guardt &guard)
896 {
898  return;
899 
900  if(expr.id()==ID_plus ||
901  expr.id()==ID_minus)
902  {
903  if(expr.operands().size()==2)
904  {
905  exprt overflow("overflow-"+expr.id_string(), bool_typet());
906  overflow.operands()=expr.operands();
907 
909  not_exprt(overflow),
910  "pointer arithmetic overflow on "+expr.id_string(),
911  "overflow",
912  expr.find_source_location(),
913  expr,
914  guard);
915  }
916  }
917 }
918 
920  const dereference_exprt &expr,
921  const guardt &guard,
922  const exprt &access_lb,
923  const exprt &access_ub)
924 {
926  return;
927 
928  const exprt &pointer=expr.op0();
930  to_pointer_type(ns.follow(pointer.type()));
931 
932  assert(base_type_eq(pointer_type.subtype(), expr.type(), ns));
933 
935  local_bitvector_analysis->get(t, pointer);
936 
937  const typet &dereference_type=pointer_type.subtype();
938 
939  // For Java, we only need to check for null
940  if(mode==ID_java)
941  {
942  if(flags.is_unknown() || flags.is_null())
943  {
944  notequal_exprt not_eq_null(pointer, null_pointer_exprt(pointer_type));
945 
947  not_eq_null,
948  "reference is null",
949  "pointer dereference",
950  expr.find_source_location(),
951  expr,
952  guard);
953  }
954  }
955  else
956  {
957  exprt allocs=false_exprt();
958 
959  if(!allocations.empty())
960  {
961  exprt::operandst disjuncts;
962 
963  for(const auto &a : allocations)
964  {
965  typecast_exprt int_ptr(pointer, a.first.type());
966 
967  exprt lb(int_ptr);
968  if(access_lb.is_not_nil())
969  {
970  if(!base_type_eq(lb.type(), access_lb.type(), ns))
971  lb=plus_exprt(lb, typecast_exprt(access_lb, lb.type()));
972  else
973  lb=plus_exprt(lb, access_lb);
974  }
975 
976  binary_relation_exprt lb_check(a.first, ID_le, lb);
977 
978  exprt ub(int_ptr);
979  if(access_ub.is_not_nil())
980  {
981  if(!base_type_eq(ub.type(), access_ub.type(), ns))
982  ub=plus_exprt(ub, typecast_exprt(access_ub, ub.type()));
983  else
984  ub=plus_exprt(ub, access_ub);
985  }
986 
987  binary_relation_exprt ub_check(
988  ub, ID_le, plus_exprt(a.first, a.second));
989 
990  disjuncts.push_back(and_exprt(lb_check, ub_check));
991  }
992 
993  allocs=disjunction(disjuncts);
994  }
995 
996  if(flags.is_unknown() || flags.is_null())
997  {
999  or_exprt(allocs, not_exprt(null_pointer(pointer))),
1000  "dereference failure: pointer NULL",
1001  "pointer dereference",
1002  expr.find_source_location(),
1003  expr,
1004  guard);
1005  }
1006 
1007  if(flags.is_unknown())
1009  or_exprt(allocs, not_exprt(invalid_pointer(pointer))),
1010  "dereference failure: pointer invalid",
1011  "pointer dereference",
1012  expr.find_source_location(),
1013  expr,
1014  guard);
1015 
1016  if(flags.is_uninitialized())
1018  or_exprt(allocs, not_exprt(invalid_pointer(pointer))),
1019  "dereference failure: pointer uninitialized",
1020  "pointer dereference",
1021  expr.find_source_location(),
1022  expr,
1023  guard);
1024 
1025  if(flags.is_unknown() || flags.is_dynamic_heap())
1027  or_exprt(allocs, not_exprt(deallocated(pointer, ns))),
1028  "dereference failure: deallocated dynamic object",
1029  "pointer dereference",
1030  expr.find_source_location(),
1031  expr,
1032  guard);
1033 
1034  if(flags.is_unknown() || flags.is_dynamic_local())
1036  or_exprt(allocs, not_exprt(dead_object(pointer, ns))),
1037  "dereference failure: dead object",
1038  "pointer dereference",
1039  expr.find_source_location(),
1040  expr,
1041  guard);
1042 
1043  if(flags.is_unknown() || flags.is_dynamic_heap())
1044  {
1045  const or_exprt dynamic_bounds(
1046  dynamic_object_lower_bound(pointer, ns, access_lb),
1047  dynamic_object_upper_bound(pointer, dereference_type, ns, access_ub));
1048 
1050  or_exprt(
1051  allocs,
1052  implies_exprt(
1053  malloc_object(pointer, ns),
1054  not_exprt(dynamic_bounds))),
1055  "dereference failure: pointer outside dynamic object bounds",
1056  "pointer dereference",
1057  expr.find_source_location(),
1058  expr,
1059  guard);
1060  }
1061 
1062  if(flags.is_unknown() ||
1063  flags.is_dynamic_local() ||
1064  flags.is_static_lifetime())
1065  {
1066  const or_exprt object_bounds(
1067  object_lower_bound(pointer, ns, access_lb),
1068  object_upper_bound(pointer, dereference_type, ns, access_ub));
1069 
1071  or_exprt(allocs, dynamic_object(pointer), not_exprt(object_bounds)),
1072  "dereference failure: pointer outside object bounds",
1073  "pointer dereference",
1074  expr.find_source_location(),
1075  expr,
1076  guard);
1077  }
1078  }
1079 }
1080 
1081 std::string goto_checkt::array_name(const exprt &expr)
1082 {
1083  return ::array_name(ns, expr);
1084 }
1085 
1087  const index_exprt &expr,
1088  const guardt &guard)
1089 {
1090  if(!enable_bounds_check)
1091  return;
1092 
1093  if(expr.find("bounds_check").is_not_nil() &&
1094  !expr.get_bool("bounds_check"))
1095  return;
1096 
1097  typet array_type=ns.follow(expr.array().type());
1098 
1099  if(array_type.id()==ID_pointer)
1100  throw "index got pointer as array type";
1101  else if(array_type.id()==ID_incomplete_array)
1102  throw "index got incomplete array";
1103  else if(array_type.id()!=ID_array && array_type.id()!=ID_vector)
1104  throw "bounds check expected array or vector type, got "
1105  +array_type.id_string();
1106 
1107  std::string name=array_name(expr.array());
1108 
1109  const exprt &index=expr.index();
1111  ode.build(expr, ns);
1112 
1113  if(index.type().id()!=ID_unsignedbv)
1114  {
1115  // we undo typecasts to signedbv
1116  if(index.id()==ID_typecast &&
1117  index.operands().size()==1 &&
1118  index.op0().type().id()==ID_unsignedbv)
1119  {
1120  // ok
1121  }
1122  else
1123  {
1124  mp_integer i;
1125 
1126  if(!to_integer(index, i) && i>=0)
1127  {
1128  // ok
1129  }
1130  else
1131  {
1132  exprt effective_offset=ode.offset();
1133 
1134  if(ode.root_object().id()==ID_dereference)
1135  {
1136  exprt p_offset=pointer_offset(
1137  to_dereference_expr(ode.root_object()).pointer());
1138  assert(p_offset.type()==effective_offset.type());
1139 
1140  effective_offset=plus_exprt(p_offset, effective_offset);
1141  }
1142 
1143  exprt zero=from_integer(0, ode.offset().type());
1144  assert(zero.is_not_nil());
1145 
1146  // the final offset must not be negative
1147  binary_relation_exprt inequality(effective_offset, ID_ge, zero);
1148 
1150  inequality,
1151  name+" lower bound",
1152  "array bounds",
1153  expr.find_source_location(),
1154  expr,
1155  guard);
1156  }
1157  }
1158  }
1159 
1160  exprt type_matches_size=true_exprt();
1161 
1162  if(ode.root_object().id()==ID_dereference)
1163  {
1164  const exprt &pointer=
1165  to_dereference_expr(ode.root_object()).pointer();
1166 
1167  if_exprt size(
1168  dynamic_object(pointer),
1169  typecast_exprt(dynamic_size(ns), object_size(pointer).type()),
1170  object_size(pointer));
1171 
1172  plus_exprt effective_offset(ode.offset(), pointer_offset(pointer));
1173 
1174  assert(effective_offset.op0().type()==effective_offset.op1().type());
1175  if(effective_offset.type()!=size.type())
1176  size.make_typecast(effective_offset.type());
1177 
1178  binary_relation_exprt inequality(effective_offset, ID_lt, size);
1179 
1180  or_exprt precond(
1181  and_exprt(
1182  dynamic_object(pointer),
1183  not_exprt(malloc_object(pointer, ns))),
1184  inequality);
1185 
1187  precond,
1188  name+" dynamic object upper bound",
1189  "array bounds",
1190  expr.find_source_location(),
1191  expr,
1192  guard);
1193 
1194  exprt type_size=size_of_expr(ode.root_object().type(), ns);
1195  if(type_size.is_not_nil())
1196  type_matches_size=
1197  equal_exprt(
1198  size,
1199  typecast_exprt(type_size, size.type()));
1200  }
1201 
1202  const exprt &size=array_type.id()==ID_array ?
1203  to_array_type(array_type).size() :
1204  to_vector_type(array_type).size();
1205 
1206  if(size.is_nil())
1207  {
1208  // Linking didn't complete, we don't have a size.
1209  // Not clear what to do.
1210  }
1211  else if(size.id()==ID_infinity)
1212  {
1213  }
1214  else if(size.is_zero() &&
1215  expr.array().id()==ID_member)
1216  {
1217  // a variable sized struct member
1218  //
1219  // Excerpt from the C standard on flexible array members:
1220  // However, when a . (or ->) operator has a left operand that is (a pointer
1221  // to) a structure with a flexible array member and the right operand names
1222  // that member, it behaves as if that member were replaced with the longest
1223  // array (with the same element type) that would not make the structure
1224  // larger than the object being accessed; [...]
1225  const exprt type_size = size_of_expr(ode.root_object().type(), ns);
1226 
1227  binary_relation_exprt inequality(
1228  typecast_exprt::conditional_cast(ode.offset(), type_size.type()),
1229  ID_lt,
1230  type_size);
1231 
1233  implies_exprt(type_matches_size, inequality),
1234  name + " upper bound",
1235  "array bounds",
1236  expr.find_source_location(),
1237  expr,
1238  guard);
1239  }
1240  else
1241  {
1242  binary_relation_exprt inequality(index, ID_lt, size);
1243 
1244  // typecast size
1245  if(inequality.op1().type()!=inequality.op0().type())
1246  inequality.op1().make_typecast(inequality.op0().type());
1247 
1248  // typecast size
1249  if(inequality.op1().type()!=inequality.op0().type())
1250  inequality.op1().make_typecast(inequality.op0().type());
1251 
1253  implies_exprt(type_matches_size, inequality),
1254  name+" upper bound",
1255  "array bounds",
1256  expr.find_source_location(),
1257  expr,
1258  guard);
1259  }
1260 }
1261 
1263  const exprt &_expr,
1264  const std::string &comment,
1265  const std::string &property_class,
1266  const source_locationt &source_location,
1267  const exprt &src_expr,
1268  const guardt &guard)
1269 {
1270  exprt expr(_expr);
1271 
1272  // first try simplifier on it
1273  if(enable_simplify)
1274  simplify(expr, ns);
1275 
1276  // throw away trivial properties?
1277  if(!retain_trivial && expr.is_true())
1278  return;
1279 
1280  // add the guard
1281  exprt guard_expr=guard.as_expr();
1282 
1283  exprt new_expr;
1284 
1285  if(guard_expr.is_true())
1286  new_expr.swap(expr);
1287  else
1288  {
1289  new_expr=exprt(ID_implies, bool_typet());
1290  new_expr.move_to_operands(guard_expr, expr);
1291  }
1292 
1293  if(assertions.insert(new_expr).second)
1294  {
1297 
1299 
1300  std::string source_expr_string;
1301  get_language_from_mode(mode)->from_expr(src_expr, source_expr_string, ns);
1302 
1303  t->guard.swap(new_expr);
1304  t->source_location=source_location;
1305  t->source_location.set_comment(comment+" in "+source_expr_string);
1306  t->source_location.set_property_class(property_class);
1307  }
1308 }
1309 
1310 void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
1311 {
1312  // we don't look into quantifiers
1313  if(expr.id()==ID_exists || expr.id()==ID_forall)
1314  return;
1315 
1316  if(address)
1317  {
1318  if(expr.id()==ID_dereference)
1319  {
1320  assert(expr.operands().size()==1);
1321  check_rec(expr.op0(), guard, false);
1322  }
1323  else if(expr.id()==ID_index)
1324  {
1325  assert(expr.operands().size()==2);
1326  check_rec(expr.op0(), guard, true);
1327  check_rec(expr.op1(), guard, false);
1328  }
1329  else
1330  {
1331  forall_operands(it, expr)
1332  check_rec(*it, guard, true);
1333  }
1334  return;
1335  }
1336 
1337  if(expr.id()==ID_address_of)
1338  {
1339  assert(expr.operands().size()==1);
1340  check_rec(expr.op0(), guard, true);
1341  return;
1342  }
1343  else if(expr.id()==ID_and || expr.id()==ID_or)
1344  {
1345  if(!expr.is_boolean())
1346  throw "`"+expr.id_string()+"' must be Boolean, but got "+
1347  expr.pretty();
1348 
1349  guardt old_guard=guard;
1350 
1351  for(const auto &op : expr.operands())
1352  {
1353  if(!op.is_boolean())
1354  throw "`"+expr.id_string()+"' takes Boolean operands only, but got "+
1355  op.pretty();
1356 
1357  check_rec(op, guard, false);
1358 
1359  if(expr.id()==ID_or)
1360  guard.add(not_exprt(op));
1361  else
1362  guard.add(op);
1363  }
1364 
1365  guard.swap(old_guard);
1366 
1367  return;
1368  }
1369  else if(expr.id()==ID_if)
1370  {
1371  if(expr.operands().size()!=3)
1372  throw "if takes three arguments";
1373 
1374  if(!expr.op0().is_boolean())
1375  {
1376  std::string msg=
1377  "first argument of if must be boolean, but got "
1378  +expr.op0().pretty();
1379  throw msg;
1380  }
1381 
1382  check_rec(expr.op0(), guard, false);
1383 
1384  {
1385  guardt old_guard=guard;
1386  guard.add(expr.op0());
1387  check_rec(expr.op1(), guard, false);
1388  guard.swap(old_guard);
1389  }
1390 
1391  {
1392  guardt old_guard=guard;
1393  guard.add(not_exprt(expr.op0()));
1394  check_rec(expr.op2(), guard, false);
1395  guard.swap(old_guard);
1396  }
1397 
1398  return;
1399  }
1400  else if(expr.id()==ID_member &&
1401  to_member_expr(expr).struct_op().id()==ID_dereference)
1402  {
1403  const member_exprt &member=to_member_expr(expr);
1404  const dereference_exprt &deref=
1405  to_dereference_expr(member.struct_op());
1406 
1407  check_rec(deref.op0(), guard, false);
1408 
1409  // avoid building the following expressions when pointer_validity_check
1410  // would return immediately anyway
1412  return;
1413 
1414  exprt access_ub=nil_exprt();
1415 
1417  exprt size=size_of_expr(expr.type(), ns);
1418 
1419  if(member_offset.is_not_nil() && size.is_not_nil())
1420  access_ub=plus_exprt(member_offset, size);
1421 
1422  pointer_validity_check(deref, guard, member_offset, access_ub);
1423 
1424  return;
1425  }
1426 
1427  forall_operands(it, expr)
1428  check_rec(*it, guard, false);
1429 
1430  if(expr.id()==ID_index)
1431  {
1432  bounds_check(to_index_expr(expr), guard);
1433  }
1434  else if(expr.id()==ID_div)
1435  {
1436  div_by_zero_check(to_div_expr(expr), guard);
1437 
1438  if(expr.type().id()==ID_signedbv)
1439  integer_overflow_check(expr, guard);
1440  else if(expr.type().id()==ID_floatbv)
1441  {
1442  nan_check(expr, guard);
1443  float_overflow_check(expr, guard);
1444  }
1445  }
1446  else if(expr.id()==ID_shl || expr.id()==ID_ashr || expr.id()==ID_lshr)
1447  {
1448  undefined_shift_check(to_shift_expr(expr), guard);
1449 
1450  if(expr.id()==ID_shl && expr.type().id()==ID_signedbv)
1451  integer_overflow_check(expr, guard);
1452  }
1453  else if(expr.id()==ID_mod)
1454  {
1455  mod_by_zero_check(to_mod_expr(expr), guard);
1456  }
1457  else if(expr.id()==ID_plus || expr.id()==ID_minus ||
1458  expr.id()==ID_mult ||
1459  expr.id()==ID_unary_minus)
1460  {
1461  if(expr.type().id()==ID_signedbv ||
1462  expr.type().id()==ID_unsignedbv)
1463  {
1464  if(expr.operands().size()==2 &&
1465  expr.op0().type().id()==ID_pointer)
1466  pointer_overflow_check(expr, guard);
1467  else
1468  integer_overflow_check(expr, guard);
1469  }
1470  else if(expr.type().id()==ID_floatbv)
1471  {
1472  nan_check(expr, guard);
1473  float_overflow_check(expr, guard);
1474  }
1475  else if(expr.type().id()==ID_pointer)
1476  {
1477  pointer_overflow_check(expr, guard);
1478  }
1479  }
1480  else if(expr.id()==ID_typecast)
1481  conversion_check(expr, guard);
1482  else if(expr.id()==ID_le || expr.id()==ID_lt ||
1483  expr.id()==ID_ge || expr.id()==ID_gt)
1484  pointer_rel_check(expr, guard);
1485  else if(expr.id()==ID_dereference)
1487  to_dereference_expr(expr),
1488  guard,
1489  nil_exprt(),
1490  size_of_expr(expr.type(), ns));
1491 }
1492 
1493 void goto_checkt::check(const exprt &expr)
1494 {
1495  guardt guard;
1496  check_rec(expr, guard, false);
1497 }
1498 
1500  goto_functiont &goto_function,
1501  const irep_idt &_mode)
1502 {
1503  assertions.clear();
1504  mode = _mode;
1505 
1506  bool did_something = false;
1507 
1508  local_bitvector_analysist local_bitvector_analysis_obj(goto_function);
1509  local_bitvector_analysis=&local_bitvector_analysis_obj;
1510 
1511  goto_programt &goto_program=goto_function.body;
1512 
1514  {
1515  t=it;
1517 
1518  new_code.clear();
1519 
1520  // we clear all recorded assertions if
1521  // 1) we want to generate all assertions or
1522  // 2) the instruction is a branch target
1523  if(retain_trivial ||
1524  i.is_target())
1525  assertions.clear();
1526 
1527  check(i.guard);
1528 
1529  // magic ERROR label?
1530  for(const auto &label : error_labels)
1531  {
1532  if(std::find(i.labels.begin(), i.labels.end(), label)!=i.labels.end())
1533  {
1536 
1538 
1539  t->guard=false_exprt();
1540  t->source_location=i.source_location;
1541  t->source_location.set_property_class("error label");
1542  t->source_location.set_comment("error label "+label);
1543  t->source_location.set("user-provided", true);
1544  }
1545  }
1546 
1547  if(i.is_other())
1548  {
1549  const irep_idt &statement=i.code.get(ID_statement);
1550 
1551  if(statement==ID_expression)
1552  {
1553  check(i.code);
1554  }
1555  else if(statement==ID_printf)
1556  {
1557  forall_operands(it, i.code)
1558  check(*it);
1559  }
1560  }
1561  else if(i.is_assign())
1562  {
1563  const code_assignt &code_assign=to_code_assign(i.code);
1564 
1565  check(code_assign.lhs());
1566  check(code_assign.rhs());
1567 
1568  // the LHS might invalidate any assertion
1569  invalidate(code_assign.lhs());
1570  }
1571  else if(i.is_function_call())
1572  {
1573  const code_function_callt &code_function_call=
1575 
1576  // for Java, need to check whether 'this' is null
1577  // on non-static method invocations
1578  if(mode==ID_java &&
1580  !code_function_call.arguments().empty() &&
1581  code_function_call.function().type().id()==ID_code &&
1582  to_code_type(code_function_call.function().type()).has_this())
1583  {
1584  exprt pointer=code_function_call.arguments()[0];
1585 
1587  local_bitvector_analysis->get(t, pointer);
1588 
1589  if(flags.is_unknown() || flags.is_null())
1590  {
1591  notequal_exprt not_eq_null(
1592  pointer,
1594 
1596  not_eq_null,
1597  "this is null on method invocation",
1598  "pointer dereference",
1599  i.source_location,
1600  pointer,
1601  guardt());
1602  }
1603  }
1604 
1605  forall_operands(it, code_function_call)
1606  check(*it);
1607 
1608  // the call might invalidate any assertion
1609  assertions.clear();
1610  }
1611  else if(i.is_return())
1612  {
1613  if(i.code.operands().size()==1)
1614  {
1615  check(i.code.op0());
1616  // the return value invalidate any assertion
1617  invalidate(i.code.op0());
1618  }
1619  }
1620  else if(i.is_throw())
1621  {
1622  if(i.code.get_statement()==ID_expression &&
1623  i.code.operands().size()==1 &&
1624  i.code.op0().operands().size()==1)
1625  {
1626  // must not throw NULL
1627 
1628  exprt pointer=i.code.op0().op0();
1629 
1630  const notequal_exprt not_eq_null(
1631  pointer, null_pointer_exprt(to_pointer_type(pointer.type())));
1632 
1634  not_eq_null,
1635  "throwing null",
1636  "pointer dereference",
1637  i.source_location,
1638  pointer,
1639  guardt());
1640  }
1641 
1642  // this has no successor
1643  assertions.clear();
1644  }
1645  else if(i.is_assert())
1646  {
1647  bool is_user_provided=i.source_location.get_bool("user-provided");
1648  if((is_user_provided && !enable_assertions &&
1649  i.source_location.get_property_class()!="error label") ||
1650  (!is_user_provided && !enable_built_in_assertions))
1651  {
1652  i.make_skip();
1653  did_something = true;
1654  }
1655  }
1656  else if(i.is_assume())
1657  {
1658  if(!enable_assumptions)
1659  {
1660  i.make_skip();
1661  did_something = true;
1662  }
1663  }
1664  else if(i.is_dead())
1665  {
1667  {
1668  assert(i.code.operands().size()==1);
1669  const symbol_exprt &variable=to_symbol_expr(i.code.op0());
1670 
1671  // is it dirty?
1672  if(local_bitvector_analysis->dirty(variable))
1673  {
1674  // need to mark the dead variable as dead
1676  exprt address_of_expr=address_of_exprt(variable);
1677  exprt lhs=ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
1678  if(!base_type_eq(lhs.type(), address_of_expr.type(), ns))
1679  address_of_expr.make_typecast(lhs.type());
1680  const if_exprt rhs(
1682  address_of_expr,
1683  lhs,
1684  lhs.type());
1685  t->source_location=i.source_location;
1686  t->code=code_assignt(lhs, rhs);
1687  t->code.add_source_location()=i.source_location;
1688  }
1689  }
1690  }
1691  else if(i.is_end_function())
1692  {
1695  {
1696  const symbolt &leak=ns.lookup(CPROVER_PREFIX "memory_leak");
1697  const symbol_exprt leak_expr=leak.symbol_expr();
1698 
1699  // add self-assignment to get helpful counterexample output
1701  t->make_assignment();
1702  t->code=code_assignt(leak_expr, leak_expr);
1703 
1704  source_locationt source_location;
1705  source_location.set_function(i.function);
1706 
1707  equal_exprt eq(
1708  leak_expr,
1711  eq,
1712  "dynamically allocated memory never freed",
1713  "memory-leak",
1714  source_location,
1715  eq,
1716  guardt());
1717  }
1718  }
1719 
1721  {
1722  if(i_it->source_location.is_nil())
1723  {
1724  i_it->source_location.id(irep_idt());
1725 
1726  if(!it->source_location.get_file().empty())
1727  i_it->source_location.set_file(it->source_location.get_file());
1728 
1729  if(!it->source_location.get_line().empty())
1730  i_it->source_location.set_line(it->source_location.get_line());
1731 
1732  if(!it->source_location.get_function().empty())
1733  i_it->source_location.set_function(
1734  it->source_location.get_function());
1735 
1736  if(!it->source_location.get_column().empty())
1737  i_it->source_location.set_column(it->source_location.get_column());
1738 
1739  if(!it->source_location.get_java_bytecode_index().empty())
1740  i_it->source_location.set_java_bytecode_index(
1741  it->source_location.get_java_bytecode_index());
1742  }
1743 
1744  if(i_it->function.empty())
1745  i_it->function=it->function;
1746  }
1747 
1748  // insert new instructions -- make sure targets are not moved
1749  did_something |= !new_code.instructions.empty();
1750 
1751  while(!new_code.instructions.empty())
1752  {
1754  new_code.instructions.pop_front();
1755  it++;
1756  }
1757  }
1758 
1759  if(did_something)
1761 }
1762 
1764  const namespacet &ns,
1765  const optionst &options,
1766  const irep_idt &mode,
1767  goto_functionst::goto_functiont &goto_function)
1768 {
1769  goto_checkt goto_check(ns, options);
1770  goto_check.goto_check(goto_function, mode);
1771 }
1772 
1774  const namespacet &ns,
1775  const optionst &options,
1776  goto_functionst &goto_functions)
1777 {
1778  goto_checkt goto_check(ns, options);
1779 
1780  goto_check.collect_allocations(goto_functions);
1781 
1782  Forall_goto_functions(it, goto_functions)
1783  {
1784  irep_idt mode=ns.lookup(it->first).mode;
1785  goto_check.goto_check(it->second, mode);
1786  }
1787 }
1788 
1790  const optionst &options,
1791  goto_modelt &goto_model)
1792 {
1793  const namespacet ns(goto_model.symbol_table);
1794  goto_check(ns, options, goto_model.goto_functions);
1795 }
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:188
const irep_idt & get_statement() const
Definition: std_code.h:39
irep_idt function
The function this instruction belongs to.
Definition: goto_program.h:179
The type of an expression.
Definition: type.h:22
exprt as_expr() const
Definition: guard.h:43
exprt size_of_expr(const typet &type, const namespacet &ns)
bool enable_div_by_zero_check
Definition: goto_check.cpp:124
Boolean negation.
Definition: std_expr.h:3230
void set_function(const irep_idt &function)
semantic type conversion
Definition: std_expr.h:2111
BigInt mp_integer
Definition: mp_arith.h:22
void pointer_rel_check(const exprt &expr, const guardt &guard)
Definition: goto_check.cpp:863
void goto_check(goto_functiont &goto_function, const irep_idt &mode)
exprt member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
bool is_boolean() const
Definition: expr.cpp:156
bool is_nil() const
Definition: irep.h:102
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
bool is_not_nil() const
Definition: irep.h:103
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:441
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
bool enable_signed_overflow_check
Definition: goto_check.cpp:125
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1287
const mod_exprt & to_mod_expr(const exprt &expr)
Cast a generic exprt to a mod_exprt.
Definition: std_expr.h:1158
boolean OR
Definition: std_expr.h:2391
exprt & op0()
Definition: expr.h:72
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
#define CPROVER_PREFIX
constant_exprt to_expr() const
Definition: ieee_float.cpp:686
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1150
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:203
const div_exprt & to_div_expr(const exprt &expr)
Cast a generic exprt to a div_exprt.
Definition: std_expr.h:1100
goto_checkt(const namespacet &_ns, const optionst &_options)
Definition: goto_check.cpp:41
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:107
exprt object_lower_bound(const exprt &pointer, const namespacet &ns, const exprt &offset)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:326
bool enable_assert_to_assume
Definition: goto_check.cpp:134
Evaluates to true if the operand is infinite.
Definition: std_expr.h:4040
Deprecated expression utility functions.
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:50
bool enable_float_overflow_check
Definition: goto_check.cpp:130
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
goto_programt body
Definition: goto_function.h:23
local_bitvector_analysist * local_bitvector_analysis
Definition: goto_check.cpp:80
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
void undefined_shift_check(const shift_exprt &expr, const guardt &guard)
Definition: goto_check.cpp:239
The null pointer constant.
Definition: std_expr.h:4520
bool enable_undefined_shift_check
Definition: goto_check.cpp:129
allocationst allocations
Definition: goto_check.cpp:144
const exprt & root_object() const
Definition: std_expr.h:1966
The trinary if-then-else operator.
Definition: std_expr.h:3361
bool is_true() const
Definition: expr.cpp:124
Definition: guard.h:19
typet & type()
Definition: expr.h:56
exprt::operandst argumentst
Definition: std_code.h:858
Field-insensitive, location-sensitive bitvector analysis.
void bounds_check(const index_exprt &expr, const guardt &guard)
irep_idt mode
Definition: goto_check.cpp:146
const value_listt & get_list_option(const std::string &option) const
Definition: options.cpp:78
bool enable_unsigned_overflow_check
Definition: goto_check.cpp:126
void nan_check(const exprt &expr, const guardt &guard)
Definition: goto_check.cpp:754
The proper Booleans.
Definition: std_types.h:34
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
exprt & distance()
Definition: std_expr.h:2797
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
bool enable_simplify
Definition: goto_check.cpp:131
exprt deallocated(const exprt &pointer, const namespacet &ns)
boolean implication
Definition: std_expr.h:2339
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Definition: std_expr.h:3328
Extract member of struct or union.
Definition: std_expr.h:3871
goto_programt new_code
Definition: goto_check.cpp:115
equality
Definition: std_expr.h:1354
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
void clear()
Clear the goto program.
Definition: goto_program.h:611
const namespacet & ns
Definition: goto_check.cpp:79
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:239
goto_programt::const_targett t
Definition: goto_check.cpp:81
std::list< allocationt > allocationst
Definition: goto_check.cpp:143
exprt object_size(const exprt &pointer)
const irep_idt & id() const
Definition: irep.h:189
bool enable_assumptions
Definition: goto_check.cpp:137
bool enable_memory_leak_check
Definition: goto_check.cpp:123
exprt & lhs()
Definition: std_code.h:208
void check(const exprt &expr)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
bool enable_conversion_check
Definition: goto_check.cpp:128
The boolean constant true.
Definition: std_expr.h:4488
argumentst & arguments()
Definition: std_code.h:860
bool retain_trivial
Definition: goto_check.cpp:133
division (integer and real)
Definition: std_expr.h:1075
constant_exprt smallest_expr() const
Definition: std_types.cpp:152
instructionst::iterator targett
Definition: goto_program.h:397
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:125
The NIL expression.
Definition: std_expr.h:4510
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
Definition: std_expr.cpp:121
The pointer type.
Definition: std_types.h:1426
exprt & rhs()
Definition: std_code.h:213
const source_locationt & find_source_location() const
Definition: expr.cpp:246
exprt object_upper_bound(const exprt &pointer, const typet &dereference_type, const namespacet &ns, const exprt &access_size)
Operator to dereference a pointer.
Definition: std_expr.h:3284
boolean AND
Definition: std_expr.h:2255
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
API to expression classes.
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
exprt & op1()
Definition: expr.h:75
void div_by_zero_check(const div_exprt &expr, const guardt &guard)
Definition: goto_check.cpp:214
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
instructionst::const_iterator const_targett
Definition: goto_program.h:398
inequality
Definition: std_expr.h:1406
TO_BE_DOCUMENTED.
Definition: namespace.h:74
std::list< std::string > value_listt
Definition: options.h:22
::goto_functiont goto_functiont
Abstract interface to support a programming language.
const exprt & size() const
Definition: std_types.h:1639
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:29
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3955
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1301
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1660
split an expression into a base object and a (byte) offset
Definition: std_expr.h:1945
const exprt & size() const
Definition: std_types.h:1014
A function call.
Definition: std_code.h:828
#define forall_operands(it, expr)
Definition: expr.h:17
Guard Data Structure.
The plus expression.
Definition: std_expr.h:893
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
Program Transformation.
void collect_allocations(const goto_functionst &goto_functions)
Definition: goto_check.cpp:149
const typet & follow(const typet &) const
Definition: namespace.cpp:55
void pointer_overflow_check(const exprt &expr, const guardt &guard)
Definition: goto_check.cpp:893
void add_guarded_claim(const exprt &expr, const std::string &comment, const std::string &property_class, const source_locationt &, const exprt &src_expr, const guardt &guard)
Operator to return the address of an object.
Definition: std_expr.h:3170
error_labelst error_labels
Definition: goto_check.cpp:140
Various predicates over pointers in programs.
exprt dynamic_object_lower_bound(const exprt &pointer, const namespacet &ns, const exprt &offset)
bool has_symbol(const exprt &src, const find_symbols_sett &symbols, bool current, bool next)
The boolean constant false.
Definition: std_expr.h:4499
void goto_check(const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
std::size_t get_width() const
Definition: std_types.h:1129
exprt disjunction(const exprt::operandst &op)
Definition: std_expr.cpp:24
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2124
std::vector< exprt > operandst
Definition: expr.h:45
Pointer Logic.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
exprt malloc_object(const exprt &pointer, const namespacet &ns)
flagst get(const goto_programt::const_targett t, const exprt &src)
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Definition: std_types.h:1245
typet type
Type of symbol.
Definition: symbol.h:34
void integer_overflow_check(const exprt &expr, const guardt &guard)
Definition: goto_check.cpp:511
API to type classes.
void make_not()
Definition: expr.cpp:91
static irep_idt entry_point()
exprt dynamic_object_upper_bound(const exprt &pointer, const typet &dereference_type, const namespacet &ns, const exprt &access_size)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast a generic exprt to a shift_exprt.
Definition: std_expr.h:2818
exprt & index()
Definition: std_expr.h:1496
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1373
exprt dynamic_size(const namespacet &ns)
exprt & op()
Definition: std_expr.h:2787
std::string array_name(const exprt &expr)
exprt & function()
Definition: std_code.h:848
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:182
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
exprt invalid_pointer(const exprt &pointer)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1045
Base class for all expressions.
Definition: expr.h:42
void mod_by_zero_check(const mod_exprt &expr, const guardt &guard)
Definition: goto_check.cpp:314
const exprt & struct_op() const
Definition: std_expr.h:3911
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
exprt pointer_offset(const exprt &pointer)
bool enable_pointer_check
Definition: goto_check.cpp:122
#define Forall_goto_functions(it, functions)
void float_overflow_check(const exprt &expr, const guardt &guard)
Definition: goto_check.cpp:632
bool enable_bounds_check
Definition: goto_check.cpp:121
#define UNREACHABLE
Definition: invariant.h:250
std::set< exprt > assertionst
Definition: goto_check.cpp:116
bool enable_built_in_assertions
Definition: goto_check.cpp:136
const std::string & id_string() const
Definition: irep.h:192
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:508
void swap(irept &irep)
Definition: irep.h:231
goto_programt & goto_program
Definition: cover.cpp:63
bool enable_nan_check
Definition: goto_check.cpp:132
bool is_zero() const
Definition: expr.cpp:161
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
bool enable_pointer_overflow_check
Definition: goto_check.cpp:127
void conversion_check(const exprt &expr, const guardt &guard)
Definition: goto_check.cpp:339
goto_functionst::goto_functiont goto_functiont
Definition: goto_check.cpp:72
std::pair< exprt, exprt > allocationt
Definition: goto_check.cpp:142
Expression to hold a symbol (variable)
Definition: std_expr.h:90
exprt & op2()
Definition: expr.h:78
Options.
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:200
Misc Utilities.
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:1450
dstringt irep_idt
Definition: irep.h:31
exprt dynamic_object(const exprt &pointer)
bool enable_assertions
Definition: goto_check.cpp:135
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:20
exprt null_pointer(const exprt &pointer)
Base Type Computation.
const typet & subtype() const
Definition: type.h:33
Program Transformation.
#define forall_goto_functions(it, functions)
optionst::value_listt error_labelst
Definition: goto_check.cpp:139
operandst & operands()
Definition: expr.h:66
void pointer_validity_check(const dereference_exprt &expr, const guardt &guard, const exprt &access_lb, const exprt &access_ub)
Definition: goto_check.cpp:919
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
exprt dead_object(const exprt &pointer, const namespacet &ns)
const irep_idt & get_property_class() const
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
exprt same_object(const exprt &p1, const exprt &p2)
bool is_target() const
Is this node a branch target?
Definition: goto_program.h:229
void check_rec(const exprt &expr, guardt &guard, bool address)
exprt & array()
Definition: std_expr.h:1486
void make_typecast(const typet &_type)
Definition: expr.cpp:84
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:22
A base class for shift operators.
Definition: std_expr.h:2765
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
binary modulo
Definition: std_expr.h:1133
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
assertionst assertions
Definition: goto_check.cpp:117
Assignment.
Definition: std_code.h:195
void add(const exprt &expr)
Definition: guard.cpp:64
void invalidate(const exprt &lhs)
Definition: goto_check.cpp:181
std::string array_name(const namespacet &ns, const exprt &expr)
Definition: array_name.cpp:19
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879
bool simplify(exprt &expr, const namespacet &ns)
IEEE-floating-point equality.
Definition: std_expr.h:4200
array index operator
Definition: std_expr.h:1462