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