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