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