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/c_types.h>
19 #include <util/config.h>
20 #include <util/cprover_prefix.h>
21 #include <util/expr_util.h>
22 #include <util/find_symbols.h>
23 #include <util/ieee_float.h>
24 #include <util/invariant.h>
25 #include <util/make_unique.h>
26 #include <util/options.h>
29 #include <util/simplify_expr.h>
30 #include <util/std_expr.h>
31 #include <util/std_types.h>
32 
33 #include <langapi/language.h>
34 #include <langapi/mode.h>
35 
37 
38 #include "guard.h"
40 
42 {
43 public:
45  const namespacet &_ns,
46  const optionst &_options):
47  ns(_ns),
49  {
50  no_enum_check = false;
51  enable_bounds_check=_options.get_bool_option("bounds-check");
52  enable_pointer_check=_options.get_bool_option("pointer-check");
53  enable_memory_leak_check=_options.get_bool_option("memory-leak-check");
54  enable_div_by_zero_check=_options.get_bool_option("div-by-zero-check");
55  enable_enum_range_check = _options.get_bool_option("enum-range-check");
57  _options.get_bool_option("signed-overflow-check");
59  _options.get_bool_option("unsigned-overflow-check");
61  _options.get_bool_option("pointer-overflow-check");
62  enable_conversion_check=_options.get_bool_option("conversion-check");
64  _options.get_bool_option("undefined-shift-check");
66  _options.get_bool_option("float-overflow-check");
67  enable_simplify=_options.get_bool_option("simplify");
68  enable_nan_check=_options.get_bool_option("nan-check");
69  retain_trivial=_options.get_bool_option("retain-trivial");
70  enable_assert_to_assume=_options.get_bool_option("assert-to-assume");
71  enable_assertions=_options.get_bool_option("assertions");
72  enable_built_in_assertions=_options.get_bool_option("built-in-assertions");
73  enable_assumptions=_options.get_bool_option("assumptions");
74  error_labels=_options.get_list_option("error-label");
75  }
76 
78 
79  void goto_check(
80  const irep_idt &function_identifier,
81  goto_functiont &goto_function);
82 
88  void collect_allocations(const goto_functionst &goto_functions);
89 
90 protected:
91  const namespacet &ns;
92  std::unique_ptr<local_bitvector_analysist> local_bitvector_analysis;
96 
102  void check_rec_address(const exprt &expr, guardt &guard);
103 
111  void check_rec_logical_op(const exprt &expr, guardt &guard);
112 
119  void check_rec_if(const if_exprt &if_expr, guardt &guard);
120 
131  bool check_rec_member(const member_exprt &member, guardt &guard);
132 
137  void check_rec_div(const div_exprt &div_expr, guardt &guard);
138 
143  void check_rec_arithmetic_op(const exprt &expr, guardt &guard);
144 
150  void check_rec(const exprt &expr, guardt &guard);
151 
154  void check(const exprt &expr);
155 
156  struct conditiont
157  {
158  conditiont(const exprt &_assertion, const std::string &_description)
159  : assertion(_assertion), description(_description)
160  {
161  }
162 
164  std::string description;
165  };
166 
167  using conditionst = std::list<conditiont>;
168 
169  void bounds_check(const index_exprt &, const guardt &);
170  void div_by_zero_check(const div_exprt &, const guardt &);
171  void mod_by_zero_check(const mod_exprt &, const guardt &);
172  void mod_overflow_check(const mod_exprt &, const guardt &);
173  void enum_range_check(const exprt &, const guardt &);
174  void undefined_shift_check(const shift_exprt &, const guardt &);
175  void pointer_rel_check(const binary_relation_exprt &, const guardt &);
176  void pointer_overflow_check(const exprt &, const guardt &);
177 
184  const dereference_exprt &expr,
185  const exprt &src_expr,
186  const guardt &guard);
187 
188  conditionst address_check(const exprt &address, const exprt &size);
189  void integer_overflow_check(const exprt &, const guardt &);
190  void conversion_check(const exprt &, const guardt &);
191  void float_overflow_check(const exprt &, const guardt &);
192  void nan_check(const exprt &, const guardt &);
194 
195  std::string array_name(const exprt &);
196 
206  const exprt &asserted_expr,
207  const std::string &comment,
208  const std::string &property_class,
209  const source_locationt &source_location,
210  const exprt &src_expr,
211  const guardt &guard);
212 
214  typedef std::set<exprt> assertionst;
216 
221  void invalidate(const exprt &lhs);
222 
241 
244 
245  // the first element of the pair is the base address,
246  // and the second is the size of the region
247  typedef std::pair<exprt, exprt> allocationt;
248  typedef std::list<allocationt> allocationst;
250 
252 };
253 
255  const goto_functionst &goto_functions)
256 {
258  return;
259 
260  forall_goto_functions(itf, goto_functions)
261  forall_goto_program_instructions(it, itf->second.body)
262  {
263  const goto_programt::instructiont &instruction=*it;
264  if(!instruction.is_function_call())
265  continue;
266 
267  const code_function_callt &call=
268  to_code_function_call(instruction.code);
269  if(call.function().id()!=ID_symbol ||
271  CPROVER_PREFIX "allocated_memory")
272  continue;
273 
274  const code_function_callt::argumentst &args= call.arguments();
275  if(args.size()!=2 ||
276  args[0].type().id()!=ID_unsignedbv ||
277  args[1].type().id()!=ID_unsignedbv)
278  throw "expected two unsigned arguments to "
279  CPROVER_PREFIX "allocated_memory";
280 
281  assert(args[0].type()==args[1].type());
282  allocations.push_back({args[0], args[1]});
283  }
284 }
285 
287 {
288  if(lhs.id()==ID_index)
289  invalidate(to_index_expr(lhs).array());
290  else if(lhs.id()==ID_member)
291  invalidate(to_member_expr(lhs).struct_op());
292  else if(lhs.id()==ID_symbol)
293  {
294  // clear all assertions about 'symbol'
295  find_symbols_sett find_symbols_set{to_symbol_expr(lhs).get_identifier()};
296 
297  for(auto it = assertions.begin(); it != assertions.end();)
298  {
299  if(has_symbol(*it, find_symbols_set) || has_subexpr(*it, ID_dereference))
300  it = assertions.erase(it);
301  else
302  ++it;
303  }
304  }
305  else
306  {
307  // give up, clear all
308  assertions.clear();
309  }
310 }
311 
313  const div_exprt &expr,
314  const guardt &guard)
315 {
317  return;
318 
319  // add divison by zero subgoal
320 
321  exprt zero=from_integer(0, expr.op1().type());
322  const notequal_exprt inequality(expr.op1(), std::move(zero));
323 
325  inequality,
326  "division by zero",
327  "division-by-zero",
328  expr.find_source_location(),
329  expr,
330  guard);
331 }
332 
333 void goto_checkt::enum_range_check(const exprt &expr, const guardt &guard)
334 {
336  return;
337 
338  const c_enum_tag_typet &c_enum_tag_type = to_c_enum_tag_type(expr.type());
339  symbolt enum_type = ns.lookup(c_enum_tag_type.get_identifier());
340  const c_enum_typet &c_enum_type = to_c_enum_type(enum_type.type);
341 
342  const c_enum_typet::memberst enum_values = c_enum_type.members();
343 
344  std::vector<exprt> disjuncts;
345  for(const auto &enum_value : enum_values)
346  {
347  const constant_exprt val{enum_value.get_value(), c_enum_tag_type};
348  disjuncts.push_back(equal_exprt(expr, val));
349  }
350 
351  const exprt check = disjunction(disjuncts);
352 
354  check,
355  "enum range check",
356  "enum-range-check",
357  expr.find_source_location(),
358  expr,
359  guard);
360 }
361 
363  const shift_exprt &expr,
364  const guardt &guard)
365 {
367  return;
368 
369  // Undefined for all types and shifts if distance exceeds width,
370  // and also undefined for negative distances.
371 
372  const typet &distance_type = expr.distance().type();
373 
374  if(distance_type.id()==ID_signedbv)
375  {
376  binary_relation_exprt inequality(
377  expr.distance(), ID_ge, from_integer(0, distance_type));
378 
380  inequality,
381  "shift distance is negative",
382  "undefined-shift",
383  expr.find_source_location(),
384  expr,
385  guard);
386  }
387 
388  const typet &op_type = expr.op().type();
389 
390  if(op_type.id()==ID_unsignedbv || op_type.id()==ID_signedbv)
391  {
392  exprt width_expr=
393  from_integer(to_bitvector_type(op_type).get_width(), distance_type);
394 
396  binary_relation_exprt(expr.distance(), ID_lt, std::move(width_expr)),
397  "shift distance too large",
398  "undefined-shift",
399  expr.find_source_location(),
400  expr,
401  guard);
402 
403  if(op_type.id()==ID_signedbv && expr.id()==ID_shl)
404  {
405  binary_relation_exprt inequality(
406  expr.op(), ID_ge, from_integer(0, op_type));
407 
409  inequality,
410  "shift operand is negative",
411  "undefined-shift",
412  expr.find_source_location(),
413  expr,
414  guard);
415  }
416  }
417  else
418  {
420  false_exprt(),
421  "shift of non-integer type",
422  "undefined-shift",
423  expr.find_source_location(),
424  expr,
425  guard);
426  }
427 }
428 
430  const mod_exprt &expr,
431  const guardt &guard)
432 {
433  if(!enable_div_by_zero_check || mode == ID_java)
434  return;
435 
436  // add divison by zero subgoal
437 
438  exprt zero=from_integer(0, expr.op1().type());
439  const notequal_exprt inequality(expr.op1(), std::move(zero));
440 
442  inequality,
443  "division by zero",
444  "division-by-zero",
445  expr.find_source_location(),
446  expr,
447  guard);
448 }
449 
451 void goto_checkt::mod_overflow_check(const mod_exprt &expr, const guardt &guard)
452 {
454  return;
455 
456  const auto &type = expr.type();
457 
458  if(type.id() == ID_signedbv)
459  {
460  // INT_MIN % -1 is, in principle, defined to be zero in
461  // ANSI C, C99, C++98, and C++11. Most compilers, however,
462  // fail to produce 0, and in some cases generate an exception.
463  // C11 explicitly makes this case undefined.
464 
465  notequal_exprt int_min_neq(
466  expr.op0(), to_signedbv_type(type).smallest_expr());
467 
468  notequal_exprt minus_one_neq(
469  expr.op1(), from_integer(-1, expr.op1().type()));
470 
472  or_exprt(int_min_neq, minus_one_neq),
473  "result of signed mod is not representable",
474  "overflow",
475  expr.find_source_location(),
476  expr,
477  guard);
478  }
479 }
480 
482  const exprt &expr,
483  const guardt &guard)
484 {
486  return;
487 
488  // First, check type.
489  const typet &type = expr.type();
490 
491  if(type.id()!=ID_signedbv &&
492  type.id()!=ID_unsignedbv)
493  return;
494 
495  if(expr.id()==ID_typecast)
496  {
497  const auto &op = to_typecast_expr(expr).op();
498 
499  // conversion to signed int may overflow
500  const typet &old_type = op.type();
501 
502  if(type.id()==ID_signedbv)
503  {
504  std::size_t new_width=to_signedbv_type(type).get_width();
505 
506  if(old_type.id()==ID_signedbv) // signed -> signed
507  {
508  std::size_t old_width=to_signedbv_type(old_type).get_width();
509  if(new_width>=old_width)
510  return; // always ok
511 
512  const binary_relation_exprt no_overflow_upper(
513  op, ID_le, from_integer(power(2, new_width - 1) - 1, old_type));
514 
515  const binary_relation_exprt no_overflow_lower(
516  op, ID_ge, from_integer(-power(2, new_width - 1), old_type));
517 
519  and_exprt(no_overflow_lower, no_overflow_upper),
520  "arithmetic overflow on signed type conversion",
521  "overflow",
522  expr.find_source_location(),
523  expr,
524  guard);
525  }
526  else if(old_type.id()==ID_unsignedbv) // unsigned -> signed
527  {
528  std::size_t old_width=to_unsignedbv_type(old_type).get_width();
529  if(new_width>=old_width+1)
530  return; // always ok
531 
532  const binary_relation_exprt no_overflow_upper(
533  op, ID_le, from_integer(power(2, new_width - 1) - 1, old_type));
534 
536  no_overflow_upper,
537  "arithmetic overflow on unsigned to signed type conversion",
538  "overflow",
539  expr.find_source_location(),
540  expr,
541  guard);
542  }
543  else if(old_type.id()==ID_floatbv) // float -> signed
544  {
545  // Note that the fractional part is truncated!
546  ieee_floatt upper(to_floatbv_type(old_type));
547  upper.from_integer(power(2, new_width-1));
548  const binary_relation_exprt no_overflow_upper(
549  op, ID_lt, upper.to_expr());
550 
551  ieee_floatt lower(to_floatbv_type(old_type));
552  lower.from_integer(-power(2, new_width-1)-1);
553  const binary_relation_exprt no_overflow_lower(
554  op, ID_gt, lower.to_expr());
555 
557  and_exprt(no_overflow_lower, no_overflow_upper),
558  "arithmetic overflow on float to signed integer type conversion",
559  "overflow",
560  expr.find_source_location(),
561  expr,
562  guard);
563  }
564  }
565  else if(type.id()==ID_unsignedbv)
566  {
567  std::size_t new_width=to_unsignedbv_type(type).get_width();
568 
569  if(old_type.id()==ID_signedbv) // signed -> unsigned
570  {
571  std::size_t old_width=to_signedbv_type(old_type).get_width();
572 
573  if(new_width>=old_width-1)
574  {
575  // only need lower bound check
576  const binary_relation_exprt no_overflow_lower(
577  op, ID_ge, from_integer(0, old_type));
578 
580  no_overflow_lower,
581  "arithmetic overflow on signed to unsigned type conversion",
582  "overflow",
583  expr.find_source_location(),
584  expr,
585  guard);
586  }
587  else
588  {
589  // need both
590  const binary_relation_exprt no_overflow_upper(
591  op, ID_le, from_integer(power(2, new_width) - 1, old_type));
592 
593  const binary_relation_exprt no_overflow_lower(
594  op, ID_ge, from_integer(0, old_type));
595 
597  and_exprt(no_overflow_lower, no_overflow_upper),
598  "arithmetic overflow on signed to unsigned type conversion",
599  "overflow",
600  expr.find_source_location(),
601  expr,
602  guard);
603  }
604  }
605  else if(old_type.id()==ID_unsignedbv) // unsigned -> unsigned
606  {
607  std::size_t old_width=to_unsignedbv_type(old_type).get_width();
608  if(new_width>=old_width)
609  return; // always ok
610 
611  const binary_relation_exprt no_overflow_upper(
612  op, ID_le, from_integer(power(2, new_width) - 1, old_type));
613 
615  no_overflow_upper,
616  "arithmetic overflow on unsigned to unsigned type conversion",
617  "overflow",
618  expr.find_source_location(),
619  expr,
620  guard);
621  }
622  else if(old_type.id()==ID_floatbv) // float -> unsigned
623  {
624  // Note that the fractional part is truncated!
625  ieee_floatt upper(to_floatbv_type(old_type));
626  upper.from_integer(power(2, new_width)-1);
627  const binary_relation_exprt no_overflow_upper(
628  op, ID_lt, upper.to_expr());
629 
630  ieee_floatt lower(to_floatbv_type(old_type));
631  lower.from_integer(-1);
632  const binary_relation_exprt no_overflow_lower(
633  op, ID_gt, lower.to_expr());
634 
636  and_exprt(no_overflow_lower, no_overflow_upper),
637  "arithmetic overflow on float to unsigned integer type conversion",
638  "overflow",
639  expr.find_source_location(),
640  expr,
641  guard);
642  }
643  }
644  }
645 }
646 
648  const exprt &expr,
649  const guardt &guard)
650 {
653  return;
654 
655  // First, check type.
656  const typet &type = expr.type();
657 
658  if(type.id()==ID_signedbv && !enable_signed_overflow_check)
659  return;
660 
661  if(type.id()==ID_unsignedbv && !enable_unsigned_overflow_check)
662  return;
663 
664  // add overflow subgoal
665 
666  if(expr.id()==ID_div)
667  {
668  // undefined for signed division INT_MIN/-1
669  if(type.id()==ID_signedbv)
670  {
671  const auto &div_expr = to_div_expr(expr);
672 
673  equal_exprt int_min_eq(
674  div_expr.dividend(), to_signedbv_type(type).smallest_expr());
675 
676  equal_exprt minus_one_eq(div_expr.divisor(), from_integer(-1, type));
677 
679  not_exprt(and_exprt(int_min_eq, minus_one_eq)),
680  "arithmetic overflow on signed division",
681  "overflow",
682  expr.find_source_location(),
683  expr,
684  guard);
685  }
686 
687  return;
688  }
689  else if(expr.id()==ID_unary_minus)
690  {
691  if(type.id()==ID_signedbv)
692  {
693  // overflow on unary- can only happen with the smallest
694  // representable number 100....0
695 
696  equal_exprt int_min_eq(
697  to_unary_minus_expr(expr).op(), to_signedbv_type(type).smallest_expr());
698 
700  not_exprt(int_min_eq),
701  "arithmetic overflow on signed unary minus",
702  "overflow",
703  expr.find_source_location(),
704  expr,
705  guard);
706  }
707 
708  return;
709  }
710  else if(expr.id() == ID_shl)
711  {
712  if(type.id() == ID_signedbv)
713  {
714  const auto &shl_expr = to_shl_expr(expr);
715  const auto &op = shl_expr.op();
716  const auto &op_type = to_signedbv_type(type);
717  const auto op_width = op_type.get_width();
718  const auto &distance = shl_expr.distance();
719  const auto &distance_type = distance.type();
720 
721  // a left shift of a negative value is undefined;
722  // yet this isn't an overflow
723  exprt neg_value_shift;
724 
725  if(op_type.id() == ID_unsignedbv)
726  neg_value_shift = false_exprt();
727  else
728  neg_value_shift =
729  binary_relation_exprt(op, ID_lt, from_integer(0, op_type));
730 
731  // a shift with negative distance is undefined;
732  // yet this isn't an overflow
733  exprt neg_dist_shift;
734 
735  if(distance_type.id() == ID_unsignedbv)
736  neg_dist_shift = false_exprt();
737  else
738  neg_dist_shift =
739  binary_relation_exprt(op, ID_lt, from_integer(0, distance_type));
740 
741  // shifting a non-zero value by more than its width is undefined;
742  // yet this isn't an overflow
743  const exprt dist_too_large = binary_predicate_exprt(
744  distance, ID_gt, from_integer(op_width, distance_type));
745 
746  const exprt op_zero = equal_exprt(op, from_integer(0, op_type));
747 
748  auto new_type = to_bitvector_type(op_type);
749  new_type.set_width(op_width * 2);
750 
751  const exprt op_ext = typecast_exprt(op, new_type);
752 
753  const exprt op_ext_shifted = shl_exprt(op_ext, distance);
754 
755  // The semantics of signed left shifts are contentious for the case
756  // that a '1' is shifted into the signed bit.
757  // Assuming 32-bit integers, 1<<31 is implementation-defined
758  // in ANSI C and C++98, but is explicitly undefined by C99,
759  // C11 and C++11.
760  bool allow_shift_into_sign_bit = true;
761 
762  if(mode == ID_C)
763  {
764  if(
767  {
768  allow_shift_into_sign_bit = false;
769  }
770  }
771  else if(mode == ID_cpp)
772  {
773  if(
776  {
777  allow_shift_into_sign_bit = false;
778  }
779  }
780 
781  const unsigned number_of_top_bits =
782  allow_shift_into_sign_bit ? op_width : op_width + 1;
783 
784  const exprt top_bits = extractbits_exprt(
785  op_ext_shifted,
786  new_type.get_width() - 1,
787  new_type.get_width() - number_of_top_bits,
788  unsignedbv_typet(number_of_top_bits));
789 
790  const exprt top_bits_zero =
791  equal_exprt(top_bits, from_integer(0, top_bits.type()));
792 
793  // a negative distance shift isn't an overflow;
794  // a negative value shift isn't an overflow;
795  // a shift that's too far isn't an overflow;
796  // a shift of zero isn't overflow;
797  // else check the top bits
799  disjunction({neg_value_shift,
800  neg_dist_shift,
801  dist_too_large,
802  op_zero,
803  top_bits_zero}),
804  "arithmetic overflow on signed shl",
805  "overflow",
806  expr.find_source_location(),
807  expr,
808  guard);
809  }
810 
811  return;
812  }
813 
814  multi_ary_exprt overflow("overflow-" + expr.id_string(), bool_typet());
815  overflow.operands()=expr.operands();
816 
817  if(expr.operands().size()>=3)
818  {
819  // The overflow checks are binary!
820  // We break these up.
821 
822  for(std::size_t i=1; i<expr.operands().size(); i++)
823  {
824  exprt tmp;
825 
826  if(i==1)
827  tmp = to_multi_ary_expr(expr).op0();
828  else
829  {
830  tmp=expr;
831  tmp.operands().resize(i);
832  }
833 
834  overflow.operands().resize(2);
835  overflow.op0()=tmp;
836  overflow.op1()=expr.operands()[i];
837 
838  std::string kind=
839  type.id()==ID_unsignedbv?"unsigned":"signed";
840 
842  not_exprt(overflow),
843  "arithmetic overflow on " + kind + " " + expr.id_string(),
844  "overflow",
845  expr.find_source_location(),
846  expr,
847  guard);
848  }
849  }
850  else
851  {
852  std::string kind=
853  type.id()==ID_unsignedbv?"unsigned":"signed";
854 
856  not_exprt(overflow),
857  "arithmetic overflow on " + kind + " " + expr.id_string(),
858  "overflow",
859  expr.find_source_location(),
860  expr,
861  guard);
862  }
863 }
864 
866  const exprt &expr,
867  const guardt &guard)
868 {
870  return;
871 
872  // First, check type.
873  const typet &type = expr.type();
874 
875  if(type.id()!=ID_floatbv)
876  return;
877 
878  // add overflow subgoal
879 
880  if(expr.id()==ID_typecast)
881  {
882  // Can overflow if casting from larger
883  // to smaller type.
884  const auto &op = to_typecast_expr(expr).op();
885  if(op.type().id() == ID_floatbv)
886  {
887  // float-to-float
888  or_exprt overflow_check{isinf_exprt(op), not_exprt(isinf_exprt(expr))};
889 
891  std::move(overflow_check),
892  "arithmetic overflow on floating-point typecast",
893  "overflow",
894  expr.find_source_location(),
895  expr,
896  guard);
897  }
898  else
899  {
900  // non-float-to-float
902  not_exprt(isinf_exprt(expr)),
903  "arithmetic overflow on floating-point typecast",
904  "overflow",
905  expr.find_source_location(),
906  expr,
907  guard);
908  }
909 
910  return;
911  }
912  else if(expr.id()==ID_div)
913  {
914  // Can overflow if dividing by something small
915  or_exprt overflow_check(
916  isinf_exprt(to_div_expr(expr).dividend()), not_exprt(isinf_exprt(expr)));
917 
919  std::move(overflow_check),
920  "arithmetic overflow on floating-point division",
921  "overflow",
922  expr.find_source_location(),
923  expr,
924  guard);
925 
926  return;
927  }
928  else if(expr.id()==ID_mod)
929  {
930  // Can't overflow
931  return;
932  }
933  else if(expr.id()==ID_unary_minus)
934  {
935  // Can't overflow
936  return;
937  }
938  else if(expr.id()==ID_plus || expr.id()==ID_mult ||
939  expr.id()==ID_minus)
940  {
941  if(expr.operands().size()==2)
942  {
943  // Can overflow
944  or_exprt overflow_check(
945  isinf_exprt(to_binary_expr(expr).op0()),
946  isinf_exprt(to_binary_expr(expr).op1()),
947  not_exprt(isinf_exprt(expr)));
948 
949  std::string kind=
950  expr.id()==ID_plus?"addition":
951  expr.id()==ID_minus?"subtraction":
952  expr.id()==ID_mult?"multiplication":"";
953 
955  std::move(overflow_check),
956  "arithmetic overflow on floating-point " + kind,
957  "overflow",
958  expr.find_source_location(),
959  expr,
960  guard);
961 
962  return;
963  }
964  else if(expr.operands().size()>=3)
965  {
966  assert(expr.id()!=ID_minus);
967 
968  // break up
969  float_overflow_check(make_binary(expr), guard);
970  return;
971  }
972  }
973 }
974 
976  const exprt &expr,
977  const guardt &guard)
978 {
979  if(!enable_nan_check)
980  return;
981 
982  // first, check type
983  if(expr.type().id()!=ID_floatbv)
984  return;
985 
986  if(expr.id()!=ID_plus &&
987  expr.id()!=ID_mult &&
988  expr.id()!=ID_div &&
989  expr.id()!=ID_minus)
990  return;
991 
992  // add NaN subgoal
993 
994  exprt isnan;
995 
996  if(expr.id()==ID_div)
997  {
998  const auto &div_expr = to_div_expr(expr);
999 
1000  // there a two ways to get a new NaN on division:
1001  // 0/0 = NaN and x/inf = NaN
1002  // (note that x/0 = +-inf for x!=0 and x!=inf)
1003  const and_exprt zero_div_zero(
1005  div_expr.op0(), from_integer(0, div_expr.dividend().type())),
1007  div_expr.op1(), from_integer(0, div_expr.divisor().type())));
1008 
1009  const isinf_exprt div_inf(div_expr.op1());
1010 
1011  isnan=or_exprt(zero_div_zero, div_inf);
1012  }
1013  else if(expr.id()==ID_mult)
1014  {
1015  if(expr.operands().size()>=3)
1016  return nan_check(make_binary(expr), guard);
1017 
1018  const auto &mult_expr = to_mult_expr(expr);
1019 
1020  // Inf * 0 is NaN
1021  const and_exprt inf_times_zero(
1022  isinf_exprt(mult_expr.op0()),
1024  mult_expr.op1(), from_integer(0, mult_expr.op1().type())));
1025 
1026  const and_exprt zero_times_inf(
1028  mult_expr.op1(), from_integer(0, mult_expr.op1().type())),
1029  isinf_exprt(mult_expr.op0()));
1030 
1031  isnan=or_exprt(inf_times_zero, zero_times_inf);
1032  }
1033  else if(expr.id()==ID_plus)
1034  {
1035  if(expr.operands().size()>=3)
1036  return nan_check(make_binary(expr), guard);
1037 
1038  const auto &plus_expr = to_plus_expr(expr);
1039 
1040  // -inf + +inf = NaN and +inf + -inf = NaN,
1041  // i.e., signs differ
1042  ieee_float_spect spec = ieee_float_spect(to_floatbv_type(plus_expr.type()));
1043  exprt plus_inf=ieee_floatt::plus_infinity(spec).to_expr();
1044  exprt minus_inf=ieee_floatt::minus_infinity(spec).to_expr();
1045 
1046  isnan = or_exprt(
1047  and_exprt(
1048  equal_exprt(plus_expr.op0(), minus_inf),
1049  equal_exprt(plus_expr.op1(), plus_inf)),
1050  and_exprt(
1051  equal_exprt(plus_expr.op0(), plus_inf),
1052  equal_exprt(plus_expr.op1(), minus_inf)));
1053  }
1054  else if(expr.id()==ID_minus)
1055  {
1056  // +inf - +inf = NaN and -inf - -inf = NaN,
1057  // i.e., signs match
1058 
1059  const auto &minus_expr = to_minus_expr(expr);
1060 
1061  ieee_float_spect spec =
1062  ieee_float_spect(to_floatbv_type(minus_expr.type()));
1063  exprt plus_inf=ieee_floatt::plus_infinity(spec).to_expr();
1064  exprt minus_inf=ieee_floatt::minus_infinity(spec).to_expr();
1065 
1066  isnan = or_exprt(
1067  and_exprt(
1068  equal_exprt(minus_expr.lhs(), plus_inf),
1069  equal_exprt(minus_expr.rhs(), plus_inf)),
1070  and_exprt(
1071  equal_exprt(minus_expr.lhs(), minus_inf),
1072  equal_exprt(minus_expr.rhs(), minus_inf)));
1073  }
1074  else
1075  UNREACHABLE;
1076 
1078  boolean_negate(isnan),
1079  "NaN on " + expr.id_string(),
1080  "NaN",
1081  expr.find_source_location(),
1082  expr,
1083  guard);
1084 }
1085 
1087  const binary_relation_exprt &expr,
1088  const guardt &guard)
1089 {
1091  return;
1092 
1093  if(expr.op0().type().id()==ID_pointer &&
1094  expr.op1().type().id()==ID_pointer)
1095  {
1096  // add same-object subgoal
1097 
1099  {
1100  exprt same_object=::same_object(expr.op0(), expr.op1());
1101 
1103  same_object,
1104  "same object violation",
1105  "pointer",
1106  expr.find_source_location(),
1107  expr,
1108  guard);
1109  }
1110  }
1111 }
1112 
1114  const exprt &expr,
1115  const guardt &guard)
1116 {
1118  return;
1119 
1120  if(expr.id() != ID_plus && expr.id() != ID_minus)
1121  return;
1122 
1124  expr.operands().size() == 2,
1125  "pointer arithmetic expected to have exactly 2 operands");
1126 
1127  exprt overflow("overflow-" + expr.id_string(), bool_typet());
1128  overflow.operands() = expr.operands();
1129 
1131  not_exprt(overflow),
1132  "pointer arithmetic overflow on " + expr.id_string(),
1133  "overflow",
1134  expr.find_source_location(),
1135  expr,
1136  guard);
1137 }
1138 
1140  const dereference_exprt &expr,
1141  const exprt &src_expr,
1142  const guardt &guard)
1143 {
1145  return;
1146 
1147  const exprt &pointer=expr.pointer();
1148 
1149  auto size_of_expr_opt = size_of_expr(expr.type(), ns);
1150  CHECK_RETURN(size_of_expr_opt.has_value());
1151 
1152  auto conditions = address_check(pointer, size_of_expr_opt.value());
1153 
1154  for(const auto &c : conditions)
1155  {
1157  c.assertion,
1158  "dereference failure: " + c.description,
1159  "pointer dereference",
1160  src_expr.find_source_location(),
1161  src_expr,
1162  guard);
1163  }
1164 }
1165 
1167 goto_checkt::address_check(const exprt &address, const exprt &size)
1168 {
1170  PRECONDITION(address.type().id() == ID_pointer);
1171  const auto &pointer_type = to_pointer_type(address.type());
1172 
1175 
1176  // For Java, we only need to check for null
1177  if(mode == ID_java)
1178  {
1179  if(flags.is_unknown() || flags.is_null())
1180  {
1181  notequal_exprt not_eq_null(address, null_pointer_exprt(pointer_type));
1182 
1183  return {conditiont(not_eq_null, "reference is null")};
1184  }
1185  else
1186  return {};
1187  }
1188  else
1189  {
1190  conditionst conditions;
1191  exprt::operandst alloc_disjuncts;
1192 
1193  for(const auto &a : allocations)
1194  {
1195  typecast_exprt int_ptr(address, a.first.type());
1196 
1197  binary_relation_exprt lb_check(a.first, ID_le, int_ptr);
1198 
1199  plus_exprt ub{int_ptr, size};
1200 
1201  binary_relation_exprt ub_check(ub, ID_le, plus_exprt(a.first, a.second));
1202 
1203  alloc_disjuncts.push_back(and_exprt(lb_check, ub_check));
1204  }
1205 
1206  const exprt in_bounds_of_some_explicit_allocation =
1207  disjunction(alloc_disjuncts);
1208 
1209  if(flags.is_unknown() || flags.is_null())
1210  {
1211  conditions.push_back(conditiont(
1212  or_exprt(
1213  in_bounds_of_some_explicit_allocation,
1214  not_exprt(null_pointer(address))),
1215  "pointer NULL"));
1216  }
1217 
1218  if(flags.is_unknown())
1219  {
1220  conditions.push_back(conditiont{
1221  not_exprt{is_invalid_pointer_exprt{address}}, "pointer invalid"});
1222  }
1223 
1224  if(flags.is_uninitialized())
1225  {
1226  conditions.push_back(
1227  conditiont{or_exprt{in_bounds_of_some_explicit_allocation,
1229  "pointer uninitialized"});
1230  }
1231 
1232  if(flags.is_unknown() || flags.is_dynamic_heap())
1233  {
1234  conditions.push_back(conditiont(
1235  or_exprt(
1236  in_bounds_of_some_explicit_allocation,
1237  not_exprt(deallocated(address, ns))),
1238  "deallocated dynamic object"));
1239  }
1240 
1241  if(flags.is_unknown() || flags.is_dynamic_local())
1242  {
1243  conditions.push_back(conditiont(
1244  or_exprt(
1245  in_bounds_of_some_explicit_allocation,
1246  not_exprt(dead_object(address, ns))),
1247  "dead object"));
1248  }
1249 
1250  if(flags.is_unknown() || flags.is_dynamic_heap())
1251  {
1252  const or_exprt dynamic_bounds_violation(
1254  dynamic_object_upper_bound(address, ns, size));
1255 
1256  conditions.push_back(conditiont(
1257  or_exprt(
1258  in_bounds_of_some_explicit_allocation,
1259  implies_exprt(
1260  malloc_object(address, ns), not_exprt(dynamic_bounds_violation))),
1261  "pointer outside dynamic object bounds"));
1262  }
1263 
1264  if(
1265  flags.is_unknown() || flags.is_dynamic_local() ||
1266  flags.is_static_lifetime())
1267  {
1268  const or_exprt object_bounds_violation(
1269  object_lower_bound(address, nil_exprt()),
1270  object_upper_bound(address, size));
1271 
1272  conditions.push_back(conditiont(
1273  or_exprt(
1274  in_bounds_of_some_explicit_allocation,
1275  implies_exprt(
1276  not_exprt(dynamic_object(address)),
1277  not_exprt(object_bounds_violation))),
1278  "pointer outside object bounds"));
1279  }
1280 
1281  if(flags.is_unknown() || flags.is_integer_address())
1282  {
1283  conditions.push_back(conditiont(
1284  implies_exprt(
1285  integer_address(address), in_bounds_of_some_explicit_allocation),
1286  "invalid integer address"));
1287  }
1288 
1289  return conditions;
1290  }
1291 }
1292 
1293 std::string goto_checkt::array_name(const exprt &expr)
1294 {
1295  return ::array_name(ns, expr);
1296 }
1297 
1299  const index_exprt &expr,
1300  const guardt &guard)
1301 {
1302  if(!enable_bounds_check)
1303  return;
1304 
1305  if(expr.find("bounds_check").is_not_nil() &&
1306  !expr.get_bool("bounds_check"))
1307  return;
1308 
1309  typet array_type = expr.array().type();
1310 
1311  if(array_type.id()==ID_pointer)
1312  throw "index got pointer as array type";
1313  else if(array_type.id()!=ID_array && array_type.id()!=ID_vector)
1314  throw "bounds check expected array or vector type, got "
1315  +array_type.id_string();
1316 
1317  std::string name=array_name(expr.array());
1318 
1319  const exprt &index=expr.index();
1321  ode.build(expr, ns);
1322 
1323  if(index.type().id()!=ID_unsignedbv)
1324  {
1325  // we undo typecasts to signedbv
1326  if(
1327  index.id() == ID_typecast &&
1328  to_typecast_expr(index).op().type().id() == ID_unsignedbv)
1329  {
1330  // ok
1331  }
1332  else
1333  {
1334  const auto i = numeric_cast<mp_integer>(index);
1335 
1336  if(!i.has_value() || *i < 0)
1337  {
1338  exprt effective_offset=ode.offset();
1339 
1340  if(ode.root_object().id()==ID_dereference)
1341  {
1342  exprt p_offset=pointer_offset(
1344  assert(p_offset.type()==effective_offset.type());
1345 
1346  effective_offset=plus_exprt(p_offset, effective_offset);
1347  }
1348 
1349  exprt zero=from_integer(0, ode.offset().type());
1350 
1351  // the final offset must not be negative
1352  binary_relation_exprt inequality(
1353  effective_offset, ID_ge, std::move(zero));
1354 
1356  inequality,
1357  name + " lower bound",
1358  "array bounds",
1359  expr.find_source_location(),
1360  expr,
1361  guard);
1362  }
1363  }
1364  }
1365 
1366  exprt type_matches_size=true_exprt();
1367 
1368  if(ode.root_object().id()==ID_dereference)
1369  {
1370  const exprt &pointer=
1372 
1373  const if_exprt size(
1374  dynamic_object(pointer),
1375  typecast_exprt(dynamic_size(ns), object_size(pointer).type()),
1376  object_size(pointer));
1377 
1378  const plus_exprt effective_offset(ode.offset(), pointer_offset(pointer));
1379 
1380  assert(effective_offset.op0().type()==effective_offset.op1().type());
1381 
1382  const auto size_casted =
1383  typecast_exprt::conditional_cast(size, effective_offset.type());
1384 
1385  binary_relation_exprt inequality(effective_offset, ID_lt, size_casted);
1386 
1387  exprt::operandst alloc_disjuncts;
1388  for(const auto &a : allocations)
1389  {
1390  typecast_exprt int_ptr{pointer, a.first.type()};
1391 
1392  binary_relation_exprt lower_bound_check{a.first, ID_le, int_ptr};
1393 
1394  plus_exprt upper_bound{
1395  int_ptr,
1396  typecast_exprt::conditional_cast(ode.offset(), int_ptr.type())};
1397 
1398  binary_relation_exprt upper_bound_check{
1399  std::move(upper_bound), ID_lt, plus_exprt{a.first, a.second}};
1400 
1401  alloc_disjuncts.push_back(
1402  and_exprt{std::move(lower_bound_check), std::move(upper_bound_check)});
1403  }
1404 
1405  exprt in_bounds_of_some_explicit_allocation = disjunction(alloc_disjuncts);
1406 
1407  or_exprt precond(
1408  std::move(in_bounds_of_some_explicit_allocation),
1409  and_exprt(dynamic_object(pointer), not_exprt(malloc_object(pointer, ns))),
1410  inequality);
1411 
1413  precond,
1414  name + " dynamic object upper bound",
1415  "array bounds",
1416  expr.find_source_location(),
1417  expr,
1418  guard);
1419 
1420  auto type_size_opt = size_of_expr(ode.root_object().type(), ns);
1421 
1422  if(type_size_opt.has_value())
1423  {
1424  // Build a predicate that evaluates to true iff the size reported by
1425  // sizeof (i.e., compile-time size) matches the actual run-time size. The
1426  // run-time size for a dynamic (i.e., heap-allocated) object is determined
1427  // by the dynamic_size(ns) expression, which can only be used when
1428  // malloc_object(pointer, ns) evaluates to true for a given pointer.
1429  type_matches_size = if_exprt{
1430  dynamic_object(pointer),
1431  and_exprt{malloc_object(pointer, ns),
1433  dynamic_size(ns), type_size_opt->type()),
1434  *type_size_opt}},
1436  object_size(pointer), type_size_opt->type()),
1437  *type_size_opt}};
1438  }
1439  }
1440 
1441  const exprt &size=array_type.id()==ID_array ?
1442  to_array_type(array_type).size() :
1443  to_vector_type(array_type).size();
1444 
1445  if(size.is_nil())
1446  {
1447  // Linking didn't complete, we don't have a size.
1448  // Not clear what to do.
1449  }
1450  else if(size.id()==ID_infinity)
1451  {
1452  }
1453  else if(size.is_zero() &&
1454  expr.array().id()==ID_member)
1455  {
1456  // a variable sized struct member
1457  //
1458  // Excerpt from the C standard on flexible array members:
1459  // However, when a . (or ->) operator has a left operand that is (a pointer
1460  // to) a structure with a flexible array member and the right operand names
1461  // that member, it behaves as if that member were replaced with the longest
1462  // array (with the same element type) that would not make the structure
1463  // larger than the object being accessed; [...]
1464  const auto type_size_opt = size_of_expr(ode.root_object().type(), ns);
1465  CHECK_RETURN(type_size_opt.has_value());
1466 
1467  binary_relation_exprt inequality(
1469  ode.offset(), type_size_opt.value().type()),
1470  ID_lt,
1471  type_size_opt.value());
1472 
1474  implies_exprt(type_matches_size, inequality),
1475  name + " upper bound",
1476  "array bounds",
1477  expr.find_source_location(),
1478  expr,
1479  guard);
1480  }
1481  else
1482  {
1483  binary_relation_exprt inequality(index, ID_lt, size);
1484 
1485  // typecast size
1486  inequality.op1() = typecast_exprt::conditional_cast(
1487  inequality.op1(), inequality.op0().type());
1488 
1490  implies_exprt(type_matches_size, inequality),
1491  name + " upper bound",
1492  "array bounds",
1493  expr.find_source_location(),
1494  expr,
1495  guard);
1496  }
1497 }
1498 
1500  const exprt &asserted_expr,
1501  const std::string &comment,
1502  const std::string &property_class,
1503  const source_locationt &source_location,
1504  const exprt &src_expr,
1505  const guardt &guard)
1506 {
1507  // first try simplifier on it
1508  exprt simplified_expr =
1509  enable_simplify ? simplify_expr(asserted_expr, ns) : asserted_expr;
1510 
1511  // throw away trivial properties?
1512  if(!retain_trivial && simplified_expr.is_true())
1513  return;
1514 
1515  // add the guard
1516  exprt guarded_expr =
1517  guard.is_true()
1518  ? std::move(simplified_expr)
1519  : implies_exprt{guard.as_expr(), std::move(simplified_expr)};
1520 
1521  if(assertions.insert(guarded_expr).second)
1522  {
1523  auto t = new_code.add(
1525  std::move(guarded_expr), source_location)
1527  std::move(guarded_expr), source_location));
1528 
1529  std::string source_expr_string;
1530  get_language_from_mode(mode)->from_expr(src_expr, source_expr_string, ns);
1531 
1532  t->source_location.set_comment(comment + " in " + source_expr_string);
1533  t->source_location.set_property_class(property_class);
1534  }
1535 }
1536 
1538 {
1539  // we don't look into quantifiers
1540  if(expr.id() == ID_exists || expr.id() == ID_forall)
1541  return;
1542 
1543  if(expr.id() == ID_dereference)
1544  {
1545  check_rec(to_dereference_expr(expr).pointer(), guard);
1546  }
1547  else if(expr.id() == ID_index)
1548  {
1549  const index_exprt &index_expr = to_index_expr(expr);
1550  check_rec_address(index_expr.array(), guard);
1551  check_rec(index_expr.index(), guard);
1552  }
1553  else
1554  {
1555  for(const auto &operand : expr.operands())
1556  check_rec_address(operand, guard);
1557  }
1558 }
1559 
1561 {
1562  INVARIANT(
1563  expr.is_boolean(),
1564  "'" + expr.id_string() + "' must be Boolean, but got " + expr.pretty());
1565 
1566  guardt old_guard = guard;
1567 
1568  for(const auto &op : expr.operands())
1569  {
1570  INVARIANT(
1571  op.is_boolean(),
1572  "'" + expr.id_string() + "' takes Boolean operands only, but got " +
1573  op.pretty());
1574 
1575  check_rec(op, guard);
1576  guard.add(expr.id() == ID_or ? boolean_negate(op) : op);
1577  }
1578 
1579  guard = std::move(old_guard);
1580 }
1581 
1582 void goto_checkt::check_rec_if(const if_exprt &if_expr, guardt &guard)
1583 {
1584  INVARIANT(
1585  if_expr.cond().is_boolean(),
1586  "first argument of if must be boolean, but got " + if_expr.cond().pretty());
1587 
1588  check_rec(if_expr.cond(), guard);
1589 
1590  {
1591  guardt old_guard = guard;
1592  guard.add(if_expr.cond());
1593  check_rec(if_expr.true_case(), guard);
1594  guard = std::move(old_guard);
1595  }
1596 
1597  {
1598  guardt old_guard = guard;
1599  guard.add(not_exprt{if_expr.cond()});
1600  check_rec(if_expr.false_case(), guard);
1601  guard = std::move(old_guard);
1602  }
1603 }
1604 
1606 {
1607  const dereference_exprt &deref = to_dereference_expr(member.struct_op());
1608 
1609  check_rec(deref.pointer(), guard);
1610 
1611  // avoid building the following expressions when pointer_validity_check
1612  // would return immediately anyway
1614  return true;
1615 
1616  // we rewrite s->member into *(s+member_offset)
1617  // to avoid requiring memory safety of the entire struct
1618  auto member_offset_opt = member_offset_expr(member, ns);
1619 
1620  if(member_offset_opt.has_value())
1621  {
1622  pointer_typet new_pointer_type = to_pointer_type(deref.pointer().type());
1623  new_pointer_type.subtype() = member.type();
1624 
1625  const exprt char_pointer = typecast_exprt::conditional_cast(
1626  deref.pointer(), pointer_type(char_type()));
1627 
1628  const exprt new_address_casted = typecast_exprt::conditional_cast(
1629  plus_exprt{char_pointer,
1631  member_offset_opt.value(), pointer_diff_type())},
1632  new_pointer_type);
1633 
1634  dereference_exprt new_deref{new_address_casted};
1635  new_deref.add_source_location() = deref.source_location();
1636  pointer_validity_check(new_deref, member, guard);
1637 
1638  return true;
1639  }
1640  return false;
1641 }
1642 
1643 void goto_checkt::check_rec_div(const div_exprt &div_expr, guardt &guard)
1644 {
1645  div_by_zero_check(to_div_expr(div_expr), guard);
1646 
1647  if(div_expr.type().id() == ID_signedbv)
1648  integer_overflow_check(div_expr, guard);
1649  else if(div_expr.type().id() == ID_floatbv)
1650  {
1651  nan_check(div_expr, guard);
1652  float_overflow_check(div_expr, guard);
1653  }
1654 }
1655 
1657 {
1658  if(expr.type().id() == ID_signedbv || expr.type().id() == ID_unsignedbv)
1659  {
1660  integer_overflow_check(expr, guard);
1661  }
1662  else if(expr.type().id() == ID_floatbv)
1663  {
1664  nan_check(expr, guard);
1665  float_overflow_check(expr, guard);
1666  }
1667  else if(expr.type().id() == ID_pointer)
1668  {
1669  pointer_overflow_check(expr, guard);
1670  }
1671 }
1672 
1673 void goto_checkt::check_rec(const exprt &expr, guardt &guard)
1674 {
1675  // we don't look into quantifiers
1676  if(expr.id() == ID_exists || expr.id() == ID_forall)
1677  return;
1678 
1679  if(expr.id() == ID_address_of)
1680  {
1681  check_rec_address(to_address_of_expr(expr).object(), guard);
1682  return;
1683  }
1684  else if(expr.id() == ID_and || expr.id() == ID_or)
1685  {
1686  check_rec_logical_op(expr, guard);
1687  return;
1688  }
1689  else if(expr.id() == ID_if)
1690  {
1691  check_rec_if(to_if_expr(expr), guard);
1692  return;
1693  }
1694  else if(
1695  expr.id() == ID_member &&
1696  to_member_expr(expr).struct_op().id() == ID_dereference)
1697  {
1698  if(check_rec_member(to_member_expr(expr), guard))
1699  return;
1700  }
1701 
1702  forall_operands(it, expr)
1703  check_rec(*it, guard);
1704 
1705  if(expr.type().id() == ID_c_enum_tag)
1706  enum_range_check(expr, guard);
1707 
1708  if(expr.id()==ID_index)
1709  {
1710  bounds_check(to_index_expr(expr), guard);
1711  }
1712  else if(expr.id()==ID_div)
1713  {
1714  check_rec_div(to_div_expr(expr), guard);
1715  }
1716  else if(expr.id()==ID_shl || expr.id()==ID_ashr || expr.id()==ID_lshr)
1717  {
1718  undefined_shift_check(to_shift_expr(expr), guard);
1719 
1720  if(expr.id()==ID_shl && expr.type().id()==ID_signedbv)
1721  integer_overflow_check(expr, guard);
1722  }
1723  else if(expr.id()==ID_mod)
1724  {
1725  mod_by_zero_check(to_mod_expr(expr), guard);
1726  mod_overflow_check(to_mod_expr(expr), guard);
1727  }
1728  else if(expr.id()==ID_plus || expr.id()==ID_minus ||
1729  expr.id()==ID_mult ||
1730  expr.id()==ID_unary_minus)
1731  {
1732  check_rec_arithmetic_op(expr, guard);
1733  }
1734  else if(expr.id()==ID_typecast)
1735  conversion_check(expr, guard);
1736  else if(expr.id()==ID_le || expr.id()==ID_lt ||
1737  expr.id()==ID_ge || expr.id()==ID_gt)
1739  else if(expr.id()==ID_dereference)
1740  {
1741  pointer_validity_check(to_dereference_expr(expr), expr, guard);
1742  }
1743 }
1744 
1745 void goto_checkt::check(const exprt &expr)
1746 {
1747  guardt guard{true_exprt{}, guard_manager};
1748  check_rec(expr, guard);
1749 }
1750 
1753 {
1754  bool modified = false;
1755 
1756  for(auto &op : expr.operands())
1757  {
1758  auto op_result = rw_ok_check(op);
1759  if(op_result.has_value())
1760  {
1761  op = *op_result;
1762  modified = true;
1763  }
1764  }
1765 
1766  if(expr.id() == ID_r_ok || expr.id() == ID_w_ok)
1767  {
1768  // these get an address as first argument and a size as second
1770  expr.operands().size() == 2, "r/w_ok must have two operands");
1771 
1772  const auto conditions =
1773  address_check(to_binary_expr(expr).op0(), to_binary_expr(expr).op1());
1774 
1775  exprt::operandst conjuncts;
1776 
1777  for(const auto &c : conditions)
1778  conjuncts.push_back(c.assertion);
1779 
1780  return conjunction(conjuncts);
1781  }
1782  else if(modified)
1783  return std::move(expr);
1784  else
1785  return {};
1786 }
1787 
1791 {
1792 public:
1794  void set_flag(bool &flag, bool new_value)
1795  {
1796  if(flag != new_value)
1797  {
1798  flags_to_reset.emplace_back(&flag, flag);
1799  flag = new_value;
1800  }
1801  }
1802 
1805  {
1806  for(const auto &flag_pair : flags_to_reset)
1807  *flag_pair.first = flag_pair.second;
1808  }
1809 
1810 private:
1811  std::list<std::pair<bool *, bool>> flags_to_reset;
1812 };
1813 
1815  const irep_idt &function_identifier,
1816  goto_functiont &goto_function)
1817 {
1818  assertions.clear();
1819 
1820  const auto &function_symbol = ns.lookup(function_identifier);
1821  mode = function_symbol.mode;
1822 
1823  bool did_something = false;
1824 
1826  util_make_unique<local_bitvector_analysist>(goto_function, ns);
1827 
1828  goto_programt &goto_program=goto_function.body;
1829 
1830  Forall_goto_program_instructions(it, goto_program)
1831  {
1832  current_target = it;
1834 
1835  flag_resett flag_resetter;
1836  const auto &pragmas = i.source_location.get_pragmas();
1837  for(const auto &d : pragmas)
1838  {
1839  if(d.first == "disable:bounds-check")
1840  flag_resetter.set_flag(enable_bounds_check, false);
1841  else if(d.first == "disable:pointer-check")
1842  flag_resetter.set_flag(enable_pointer_check, false);
1843  else if(d.first == "disable:memory-leak-check")
1844  flag_resetter.set_flag(enable_memory_leak_check, false);
1845  else if(d.first == "disable:div-by-zero-check")
1846  flag_resetter.set_flag(enable_div_by_zero_check, false);
1847  else if(d.first == "disable:enum-range-check")
1848  flag_resetter.set_flag(enable_enum_range_check, false);
1849  else if(d.first == "disable:signed-overflow-check")
1850  flag_resetter.set_flag(enable_signed_overflow_check, false);
1851  else if(d.first == "disable:unsigned-overflow-check")
1852  flag_resetter.set_flag(enable_unsigned_overflow_check, false);
1853  else if(d.first == "disable:pointer-overflow-check")
1854  flag_resetter.set_flag(enable_pointer_overflow_check, false);
1855  else if(d.first == "disable:float-overflow-check")
1856  flag_resetter.set_flag(enable_float_overflow_check, false);
1857  else if(d.first == "disable:conversion-check")
1858  flag_resetter.set_flag(enable_conversion_check, false);
1859  else if(d.first == "disable:undefined-shift-check")
1860  flag_resetter.set_flag(enable_undefined_shift_check, false);
1861  else if(d.first == "disable:nan-check")
1862  flag_resetter.set_flag(enable_nan_check, false);
1863  }
1864 
1865  new_code.clear();
1866 
1867  // we clear all recorded assertions if
1868  // 1) we want to generate all assertions or
1869  // 2) the instruction is a branch target
1870  if(retain_trivial ||
1871  i.is_target())
1872  assertions.clear();
1873 
1874  if(i.has_condition())
1875  {
1876  check(i.get_condition());
1877 
1878  if(has_subexpr(i.get_condition(), [](const exprt &expr) {
1879  return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
1880  }))
1881  {
1882  auto rw_ok_cond = rw_ok_check(i.get_condition());
1883  if(rw_ok_cond.has_value())
1884  i.set_condition(*rw_ok_cond);
1885  }
1886  }
1887 
1888  // magic ERROR label?
1889  for(const auto &label : error_labels)
1890  {
1891  if(std::find(i.labels.begin(), i.labels.end(), label)!=i.labels.end())
1892  {
1893  auto t = new_code.add(
1897 
1898  t->source_location.set_property_class("error label");
1899  t->source_location.set_comment("error label "+label);
1900  t->source_location.set("user-provided", true);
1901  }
1902  }
1903 
1904  if(i.is_other())
1905  {
1906  const auto &code = i.get_other();
1907  const irep_idt &statement = code.get_statement();
1908 
1909  if(statement==ID_expression)
1910  {
1911  check(code);
1912  }
1913  else if(statement==ID_printf)
1914  {
1915  for(const auto &op : code.operands())
1916  check(op);
1917  }
1918  }
1919  else if(i.is_assign())
1920  {
1921  const code_assignt &code_assign=to_code_assign(i.code);
1922 
1923  // Reset the no_enum_check with the flag reset for exception
1924  // safety
1925  {
1926  flag_resett no_enum_check_flag_resetter;
1927  no_enum_check_flag_resetter.set_flag(no_enum_check, true);
1928  check(code_assign.lhs());
1929  }
1930  check(code_assign.rhs());
1931 
1932  // the LHS might invalidate any assertion
1933  invalidate(code_assign.lhs());
1934 
1935  if(has_subexpr(code_assign.rhs(), [](const exprt &expr) {
1936  return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
1937  }))
1938  {
1939  exprt &rhs = to_code_assign(i.code).rhs();
1940  auto rw_ok_cond = rw_ok_check(rhs);
1941  if(rw_ok_cond.has_value())
1942  rhs = *rw_ok_cond;
1943  }
1944  }
1945  else if(i.is_function_call())
1946  {
1947  const code_function_callt &code_function_call=
1949 
1950  // for Java, need to check whether 'this' is null
1951  // on non-static method invocations
1952  if(mode==ID_java &&
1954  !code_function_call.arguments().empty() &&
1955  code_function_call.function().type().id()==ID_code &&
1956  to_code_type(code_function_call.function().type()).has_this())
1957  {
1958  exprt pointer=code_function_call.arguments()[0];
1959 
1962 
1963  if(flags.is_unknown() || flags.is_null())
1964  {
1965  notequal_exprt not_eq_null(
1966  pointer,
1968 
1970  not_eq_null,
1971  "this is null on method invocation",
1972  "pointer dereference",
1973  i.source_location,
1974  pointer,
1976  }
1977  }
1978 
1979  for(const auto &op : code_function_call.operands())
1980  check(op);
1981 
1982  // the call might invalidate any assertion
1983  assertions.clear();
1984  }
1985  else if(i.is_return())
1986  {
1987  if(i.code.operands().size()==1)
1988  {
1989  const code_returnt &code_return = to_code_return(i.code);
1990  check(code_return.return_value());
1991  // the return value invalidate any assertion
1992  invalidate(code_return.return_value());
1993 
1994  if(has_subexpr(code_return.return_value(), [](const exprt &expr) {
1995  return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
1996  }))
1997  {
1998  exprt &return_value = to_code_return(i.code).return_value();
1999  auto rw_ok_cond = rw_ok_check(return_value);
2000  if(rw_ok_cond.has_value())
2001  return_value = *rw_ok_cond;
2002  }
2003  }
2004  }
2005  else if(i.is_throw())
2006  {
2007  if(i.code.get_statement()==ID_expression &&
2008  i.code.operands().size()==1 &&
2009  i.code.op0().operands().size()==1)
2010  {
2011  // must not throw NULL
2012 
2013  exprt pointer = to_unary_expr(i.code.op0()).op();
2014 
2015  const notequal_exprt not_eq_null(
2016  pointer, null_pointer_exprt(to_pointer_type(pointer.type())));
2017 
2019  not_eq_null,
2020  "throwing null",
2021  "pointer dereference",
2022  i.source_location,
2023  pointer,
2025  }
2026 
2027  // this has no successor
2028  assertions.clear();
2029  }
2030  else if(i.is_assert())
2031  {
2032  bool is_user_provided=i.source_location.get_bool("user-provided");
2033 
2034  if((is_user_provided && !enable_assertions &&
2035  i.source_location.get_property_class()!="error label") ||
2036  (!is_user_provided && !enable_built_in_assertions))
2037  {
2038  i.turn_into_skip();
2039  did_something = true;
2040  }
2041  }
2042  else if(i.is_assume())
2043  {
2044  if(!enable_assumptions)
2045  {
2046  i.turn_into_skip();
2047  did_something = true;
2048  }
2049  }
2050  else if(i.is_dead())
2051  {
2053  {
2054  assert(i.code.operands().size()==1);
2055  const symbol_exprt &variable=to_symbol_expr(i.code.op0());
2056 
2057  // is it dirty?
2058  if(local_bitvector_analysis->dirty(variable))
2059  {
2060  // need to mark the dead variable as dead
2061  exprt lhs=ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
2062  exprt address_of_expr = typecast_exprt::conditional_cast(
2063  address_of_exprt(variable), lhs.type());
2064  if_exprt rhs(
2066  std::move(address_of_expr),
2067  lhs);
2070  std::move(lhs), std::move(rhs), i.source_location));
2071  t->code.add_source_location()=i.source_location;
2072  }
2073  }
2074  }
2075  else if(i.is_end_function())
2076  {
2077  if(
2078  function_identifier == goto_functionst::entry_point() &&
2080  {
2081  const symbolt &leak=ns.lookup(CPROVER_PREFIX "memory_leak");
2082  const symbol_exprt leak_expr=leak.symbol_expr();
2083 
2084  // add self-assignment to get helpful counterexample output
2085  new_code.add(goto_programt::make_assignment(leak_expr, leak_expr));
2086 
2087  source_locationt source_location;
2088  source_location.set_function(function_identifier);
2089 
2090  equal_exprt eq(
2091  leak_expr,
2094  eq,
2095  "dynamically allocated memory never freed",
2096  "memory-leak",
2097  source_location,
2098  eq,
2100  }
2101  }
2102 
2104  {
2105  if(i_it->source_location.is_nil())
2106  {
2107  i_it->source_location.id(irep_idt());
2108 
2109  if(!it->source_location.get_file().empty())
2110  i_it->source_location.set_file(it->source_location.get_file());
2111 
2112  if(!it->source_location.get_line().empty())
2113  i_it->source_location.set_line(it->source_location.get_line());
2114 
2115  if(!it->source_location.get_function().empty())
2116  i_it->source_location.set_function(
2117  it->source_location.get_function());
2118 
2119  if(!it->source_location.get_column().empty())
2120  i_it->source_location.set_column(it->source_location.get_column());
2121 
2122  if(!it->source_location.get_java_bytecode_index().empty())
2123  i_it->source_location.set_java_bytecode_index(
2124  it->source_location.get_java_bytecode_index());
2125  }
2126  }
2127 
2128  // insert new instructions -- make sure targets are not moved
2129  did_something |= !new_code.instructions.empty();
2130 
2131  while(!new_code.instructions.empty())
2132  {
2133  goto_program.insert_before_swap(it, new_code.instructions.front());
2134  new_code.instructions.pop_front();
2135  it++;
2136  }
2137  }
2138 
2139  if(did_something)
2140  remove_skip(goto_program);
2141 }
2142 
2144  const irep_idt &function_identifier,
2145  goto_functionst::goto_functiont &goto_function,
2146  const namespacet &ns,
2147  const optionst &options)
2148 {
2149  goto_checkt goto_check(ns, options);
2150  goto_check.goto_check(function_identifier, goto_function);
2151 }
2152 
2154  const namespacet &ns,
2155  const optionst &options,
2156  goto_functionst &goto_functions)
2157 {
2158  goto_checkt goto_check(ns, options);
2159 
2160  goto_check.collect_allocations(goto_functions);
2161 
2162  Forall_goto_functions(it, goto_functions)
2163  {
2164  goto_check.goto_check(it->first, it->second);
2165  }
2166 }
2167 
2169  const optionst &options,
2170  goto_modelt &goto_model)
2171 {
2172  const namespacet ns(goto_model.symbol_table);
2173  goto_check(ns, options, goto_model.goto_functions);
2174 }
goto_checkt::allocationt
std::pair< exprt, exprt > allocationt
Definition: goto_check.cpp:247
goto_checkt::allocationst
std::list< allocationt > allocationst
Definition: goto_check.cpp:248
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1177
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:451
guard_exprt
Definition: guard_expr.h:27
goto_checkt::array_name
std::string array_name(const exprt &)
Definition: goto_check.cpp:1293
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
to_c_enum_tag_type
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: std_types.h:721
goto_functiont::body
goto_programt body
Definition: goto_function.h:30
array_name
std::string array_name(const namespacet &ns, const exprt &expr)
Definition: array_name.cpp:20
ieee_floatt
Definition: ieee_float.h:120
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2050
goto_programt::instructiont::is_throw
bool is_throw() const
Definition: goto_program.h:462
goto_checkt::current_target
goto_programt::const_targett current_target
Definition: goto_check.cpp:93
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:316
multi_ary_exprt
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:791
source_locationt::get_property_class
const irep_idt & get_property_class() const
Definition: source_location.h:66
goto_programt::instructiont::source_location
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:269
typet::subtype
const typet & subtype() const
Definition: type.h:47
c_enum_typet
The type of C enums.
Definition: std_types.h:620
has_subexpr
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:139
conjunction
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:51
goto_checkt::bounds_check
void bounds_check(const index_exprt &, const guardt &)
Definition: goto_check.cpp:1298
goto_checkt::conditiont::assertion
exprt assertion
Definition: goto_check.cpp:163
to_div_expr
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1086
goto_checkt::enable_div_by_zero_check
bool enable_div_by_zero_check
Definition: goto_check.cpp:226
local_bitvector_analysis.h
arith_tools.h
codet::op0
exprt & op0()
Definition: expr.h:101
goto_checkt::enable_undefined_shift_check
bool enable_undefined_shift_check
Definition: goto_check.cpp:232
object_descriptor_exprt::build
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
Definition: std_expr.cpp:141
source_locationt::set_function
void set_function(const irep_idt &function)
Definition: source_location.h:126
goto_checkt::guard_manager
guard_managert guard_manager
Definition: goto_check.cpp:94
null_pointer
exprt null_pointer(const exprt &pointer)
Definition: pointer_predicates.cpp:136
goto_programt::instructiont::is_other
bool is_other() const
Definition: goto_program.h:466
goto_checkt::enable_assumptions
bool enable_assumptions
Definition: goto_check.cpp:240
optionst
Definition: options.h:23
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
goto_checkt::enable_simplify
bool enable_simplify
Definition: goto_check.cpp:234
to_c_enum_type
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: std_types.h:681
typet
The type of an expression, extends irept.
Definition: type.h:29
source_locationt::get_pragmas
const irept::named_subt & get_pragmas() const
Definition: source_location.h:200
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:320
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:488
goto_checkt::enable_nan_check
bool enable_nan_check
Definition: goto_check.cpp:235
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1353
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3058
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2917
local_bitvector_analysist::flagst::is_dynamic_heap
bool is_dynamic_heap() const
Definition: local_bitvector_analysis.h:131
goto_checkt::new_code
goto_programt new_code
Definition: goto_check.cpp:213
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2993
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
goto_checkt::enable_built_in_assertions
bool enable_built_in_assertions
Definition: goto_check.cpp:239
c_enum_typet::memberst
std::vector< c_enum_membert > memberst
Definition: std_types.h:644
goto_checkt::check_rec_address
void check_rec_address(const exprt &expr, guardt &guard)
Check an address-of expression: if it is a dereference then check the pointer if it is an index then ...
Definition: goto_check.cpp:1537
pointer_predicates.h
goto_programt::instructiont::is_dead
bool is_dead() const
Definition: goto_program.h:468
goto_checkt::enable_assert_to_assume
bool enable_assert_to_assume
Definition: goto_check.cpp:237
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:1849
goto_checkt::retain_trivial
bool retain_trivial
Definition: goto_check.cpp:236
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
get_language_from_mode
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:50
invariant.h
and_exprt
Boolean AND.
Definition: std_expr.h:2166
goto_checkt::allocations
allocationst allocations
Definition: goto_check.cpp:249
flag_resett::~flag_resett
~flag_resett()
Restore the values of all flags that have been modified via set_flag.
Definition: goto_check.cpp:1804
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:686
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:887
flag_resett
Set a Boolean flag to a new value (via set_flag) and restore the previous value when the entire objec...
Definition: goto_check.cpp:1791
goto_checkt::pointer_validity_check
void pointer_validity_check(const dereference_exprt &expr, const exprt &src_expr, const guardt &guard)
Generates VCCs for the validity of the given dereferencing operation.
Definition: goto_check.cpp:1139
exprt
Base class for all expressions.
Definition: expr.h:53
goto_checkt::enable_conversion_check
bool enable_conversion_check
Definition: goto_check.cpp:231
goto_checkt::check_rec_div
void check_rec_div(const div_exprt &div_expr, guardt &guard)
Check that a division is valid: check for division by zero, overflow and NaN (for floating point numb...
Definition: goto_check.cpp:1643
goto_modelt
Definition: goto_model.h:26
guard_exprt::is_true
bool is_true() const
Definition: guard_expr.h:63
mode.h
options.h
goto_check
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options)
Definition: goto_check.cpp:2143
irep_idt
dstringt irep_idt
Definition: irep.h:32
goto_checkt::no_enum_check
bool no_enum_check
Definition: goto_check.cpp:95
bool_typet
The Boolean type.
Definition: std_types.h:37
goto_checkt::conditionst
std::list< conditiont > conditionst
Definition: goto_check.cpp:167
optionst::value_listt
std::list< std::string > value_listt
Definition: options.h:25
dynamic_object
exprt dynamic_object(const exprt &pointer)
Definition: pointer_predicates.cpp:71
guardt
guard_exprt guardt
Definition: guard.h:27
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
configt::ansi_c
struct configt::ansi_ct ansi_c
make_binary
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:36
goto_checkt::pointer_rel_check
void pointer_rel_check(const binary_relation_exprt &, const guardt &)
Definition: goto_check.cpp:1086
div_exprt
Division.
Definition: std_expr.h:1037
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
shift_exprt::op
exprt & op()
Definition: std_expr.h:2534
equal_exprt
Equality.
Definition: std_expr.h:1196
goto_checkt::nan_check
void nan_check(const exprt &, const guardt &)
Definition: goto_check.cpp:975
goto_checkt::enable_memory_leak_check
bool enable_memory_leak_check
Definition: goto_check.cpp:225
goto_checkt::enum_range_check
void enum_range_check(const exprt &, const guardt &)
Definition: goto_check.cpp:333
to_minus_expr
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:971
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:1024
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3030
notequal_exprt
Disequality.
Definition: std_expr.h:1254
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1216
goto_programt::instructiont::get_other
const codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:255
ieee_float_spect
Definition: ieee_float.h:26
goto_checkt::enable_unsigned_overflow_check
bool enable_unsigned_overflow_check
Definition: goto_check.cpp:229
goto_checkt::enable_float_overflow_check
bool enable_float_overflow_check
Definition: goto_check.cpp:233
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:678
goto_checkt::mod_by_zero_check
void mod_by_zero_check(const mod_exprt &, const guardt &)
Definition: goto_check.cpp:429
to_shift_expr
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Definition: std_expr.h:2572
array_typet::size
const exprt & size() const
Definition: std_types.h:973
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
guard.h
guard_expr_managert
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:23
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
goto_checkt::pointer_overflow_check
void pointer_overflow_check(const exprt &, const guardt &)
Definition: goto_check.cpp:1113
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1186
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
goto_checkt::check_rec_logical_op
void check_rec_logical_op(const exprt &expr, guardt &guard)
Check a logical operation: check each operand in separation while extending the guarding condition as...
Definition: goto_check.cpp:1560
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
disjunction
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:29
goto_programt::instructiont::turn_into_skip
void turn_into_skip()
Transforms an existing instruction into a skip, retaining the source_location.
Definition: goto_program.h:351
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:893
make_unique.h
find_symbols.h
goto_checkt::check
void check(const exprt &expr)
Initiate the recursively analysis of expr with its ‘guard’ set to TRUE.
Definition: goto_check.cpp:1745
or_exprt
Boolean OR.
Definition: std_expr.h:2274
goto_checkt::check_rec
void check_rec(const exprt &expr, guardt &guard)
Recursively descend into expr and run the appropriate check for each sub-expression,...
Definition: goto_check.cpp:1673
to_mod_expr
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1131
goto_checkt::address_check
conditionst address_check(const exprt &address, const exprt &size)
Definition: goto_check.cpp:1167
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: std_types.h:1248
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
to_mult_expr
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1017
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:4018
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2852
goto_checkt::float_overflow_check
void float_overflow_check(const exprt &, const guardt &)
Definition: goto_check.cpp:865
goto_checkt::conditiont
Definition: goto_check.cpp:157
goto_checkt::enable_pointer_check
bool enable_pointer_check
Definition: goto_check.cpp:224
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:182
guard_exprt::as_expr
exprt as_expr() const
Definition: guard_expr.h:49
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3464
binary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:694
guard_exprt::add
void add(const exprt &expr)
Definition: guard_expr.cpp:40
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
multi_ary_exprt::op1
exprt & op1()
Definition: std_expr.h:823
exprt::find_source_location
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:231
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
goto_checkt::ns
const namespacet & ns
Definition: goto_check.cpp:91
nil_exprt
The NIL expression.
Definition: std_expr.h:4002
dereference_exprt::pointer
exprt & pointer()
Definition: std_expr.h:2930
boolean_negate
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:127
object_upper_bound
exprt object_upper_bound(const exprt &pointer, const exprt &access_size)
Definition: pointer_predicates.cpp:178
std_types.h
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
local_bitvector_analysist::flagst::is_integer_address
bool is_integer_address() const
Definition: local_bitvector_analysis.h:161
to_plus_expr
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:926
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:315
goto_programt::instructiont::labels
labelst labels
Definition: goto_program.h:331
deallocated
exprt deallocated(const exprt &pointer, const namespacet &ns)
Definition: pointer_predicates.cpp:50
irept::id_string
const std::string & id_string() const
Definition: irep.h:421
dead_object
exprt dead_object(const exprt &pointer, const namespacet &ns)
Definition: pointer_predicates.cpp:58
goto_checkt::enable_enum_range_check
bool enable_enum_range_check
Definition: goto_check.cpp:227
goto_checkt::assertionst
std::set< exprt > assertionst
Definition: goto_check.cpp:214
language.h
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2698
integer_address
exprt integer_address(const exprt &pointer)
Definition: pointer_predicates.cpp:129
index_exprt::index
exprt & index()
Definition: std_expr.h:1325
goto_programt::instructiont::has_condition
bool has_condition() const
Does this instruction have a condition?
Definition: goto_program.h:279
goto_checkt::local_bitvector_analysis
std::unique_ptr< local_bitvector_analysist > local_bitvector_analysis
Definition: goto_check.cpp:92
to_unary_minus_expr
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:408
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
index_exprt::array
exprt & array()
Definition: std_expr.h:1315
local_bitvector_analysist::flagst::is_null
bool is_null() const
Definition: local_bitvector_analysis.h:141
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
goto_checkt::enable_assertions
bool enable_assertions
Definition: goto_check.cpp:238
object_size
exprt object_size(const exprt &pointer)
Definition: pointer_predicates.cpp:32
local_bitvector_analysist::flagst::is_static_lifetime
bool is_static_lifetime() const
Definition: local_bitvector_analysis.h:151
irept::is_nil
bool is_nil() const
Definition: irep.h:398
goto_checkt::check_rec_member
bool check_rec_member(const member_exprt &member, guardt &guard)
Check that a member expression is valid:
Definition: goto_check.cpp:1605
irept::id
const irep_idt & id() const
Definition: irep.h:418
goto_programt::instructiont::is_end_function
bool is_end_function() const
Definition: goto_program.h:475
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1297
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:28
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1195
to_code_return
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1362
false_exprt
The Boolean constant false.
Definition: std_expr.h:3993
goto_check.h
goto_checkt::rw_ok_check
optionalt< exprt > rw_ok_check(exprt)
expand the r_ok and w_ok predicates
Definition: goto_check.cpp:1752
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
goto_checkt::collect_allocations
void collect_allocations(const goto_functionst &goto_functions)
Fill the list of allocations allocationst with <address, size> for every allocation instruction.
Definition: goto_check.cpp:254
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
cprover_prefix.h
object_descriptor_exprt::root_object
const exprt & root_object() const
Definition: std_expr.cpp:218
local_bitvector_analysist::flagst::is_dynamic_local
bool is_dynamic_local() const
Definition: local_bitvector_analysis.h:121
ieee_floatt::from_integer
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:511
goto_checkt::undefined_shift_check
void undefined_shift_check(const shift_exprt &, const guardt &)
Definition: goto_check.cpp:362
object_lower_bound
exprt object_lower_bound(const exprt &pointer, const exprt &offset)
Definition: pointer_predicates.cpp:208
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1231
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
vector_typet::size
const constant_exprt & size() const
Definition: std_types.cpp:268
goto_checkt::div_by_zero_check
void div_by_zero_check(const div_exprt &, const guardt &)
Definition: goto_check.cpp:312
pointer_offset
exprt pointer_offset(const exprt &pointer)
Definition: pointer_predicates.cpp:37
goto_checkt::goto_functiont
goto_functionst::goto_functiont goto_functiont
Definition: goto_check.cpp:77
goto_checkt::error_labels
error_labelst error_labels
Definition: goto_check.cpp:243
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
code_typet::has_this
bool has_this() const
Definition: std_types.h:818
goto_programt::clear
void clear()
Clear the goto program.
Definition: goto_program.h:783
ieee_floatt::plus_infinity
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:200
flag_resett::set_flag
void set_flag(bool &flag, bool new_value)
Store the current value of flag and then set its value to new_value.
Definition: goto_check.cpp:1794
config
configt config
Definition: config.cpp:24
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
source_locationt
Definition: source_location.h:20
configt::ansi_ct::c_standardt::C99
@ C99
simplify_expr.h
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1955
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_checkt
Definition: goto_check.cpp:42
malloc_object
exprt malloc_object(const exprt &pointer, const namespacet &ns)
Definition: pointer_predicates.cpp:42
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:132
has_symbol
bool has_symbol(const exprt &src, const find_symbols_sett &symbols, bool current, bool next)
Definition: find_symbols.cpp:37
goto_checkt::enable_bounds_check
bool enable_bounds_check
Definition: goto_check.cpp:223
local_bitvector_analysist::flagst::is_unknown
bool is_unknown() const
Definition: local_bitvector_analysis.h:91
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3434
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
expr_util.h
Deprecated expression utility functions.
configt::ansi_ct::c_standardt::C11
@ C11
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:2973
shift_exprt
A base class for shift operators.
Definition: std_expr.h:2525
goto_programt::instructiont::is_assert
bool is_assert() const
Definition: goto_program.h:470
dynamic_object_upper_bound
exprt dynamic_object_upper_bound(const exprt &pointer, const namespacet &ns, const exprt &access_size)
Definition: pointer_predicates.cpp:149
c_enum_tag_typet
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: std_types.h:696
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1313
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:3020
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
find_symbols_sett
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:22
goto_checkt::goto_check
void goto_check(const irep_idt &function_identifier, goto_functiont &goto_function)
Definition: goto_check.cpp:1814
goto_checkt::mod_overflow_check
void mod_overflow_check(const mod_exprt &, const guardt &)
check a mod expression for the case INT_MIN % -1
Definition: goto_check.cpp:451
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:386
shift_exprt::distance
exprt & distance()
Definition: std_expr.h:2544
local_bitvector_analysist::flagst
Definition: local_bitvector_analysis.h:50
isinf_exprt
Evaluates to true if the operand is infinite.
Definition: std_expr.h:3583
symbolt
Symbol table entry.
Definition: symbol.h:28
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
goto_checkt::invalidate
void invalidate(const exprt &lhs)
Remove all assertions containing the symbol in lhs as well as all assertions containing dereference.
Definition: goto_check.cpp:286
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2076
configt::ansi_ct::c_standard
enum configt::ansi_ct::c_standardt c_standard
ieee_float.h
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
goto_checkt::enable_signed_overflow_check
bool enable_signed_overflow_check
Definition: goto_check.cpp:228
if_exprt::cond
exprt & cond()
Definition: std_expr.h:3010
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: std_types.h:1298
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
goto_checkt::add_guarded_property
void add_guarded_property(const exprt &asserted_expr, const std::string &comment, const std::string &property_class, const source_locationt &source_location, const exprt &src_expr, const guardt &guard)
Include the asserted_expr in the code conditioned by the guard.
Definition: goto_check.cpp:1499
goto_programt::instructiont::is_assign
bool is_assign() const
Definition: goto_program.h:460
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
goto_checkt::integer_overflow_check
void integer_overflow_check(const exprt &, const guardt &)
Definition: goto_check.cpp:647
local_bitvector_analysist::flagst::is_uninitialized
bool is_uninitialized() const
Definition: local_bitvector_analysis.h:101
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
same_object
exprt same_object(const exprt &p1, const exprt &p2)
Definition: pointer_predicates.cpp:27
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:194
goto_checkt::conditiont::description
std::string description
Definition: goto_check.cpp:164
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1424
configt::cppt::cpp_standardt::CPP14
@ CPP14
config.h
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1775
goto_programt::instructiont::set_condition
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
Definition: goto_program.h:292
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:122
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:285
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3518
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
implies_exprt
Boolean implication.
Definition: std_expr.h:2229
ieee_floatt::to_expr
constant_exprt to_expr() const
Definition: ieee_float.cpp:698
goto_checkt::error_labelst
optionst::value_listt error_labelst
Definition: goto_check.cpp:242
configt::cppt::cpp_standardt::CPP11
@ CPP11
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:905
extractbits_exprt
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:2726
exprt::operands
operandst & operands()
Definition: expr.h:95
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:90
index_exprt
Array index operator.
Definition: std_expr.h:1299
is_invalid_pointer_exprt
Definition: pointer_predicates.h:48
goto_programt::instructiont::is_assume
bool is_assume() const
Definition: goto_program.h:469
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2815
goto_checkt::mode
irep_idt mode
Definition: goto_check.cpp:251
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:257
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:606
dynamic_object_lower_bound
exprt dynamic_object_lower_bound(const exprt &pointer, const exprt &offset)
Definition: pointer_predicates.cpp:142
configt::cpp
struct configt::cppt cpp
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2042
pointer_diff_type
signedbv_typet pointer_diff_type()
Definition: c_types.cpp:228
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1488
remove_skip.h
goto_checkt::enable_pointer_overflow_check
bool enable_pointer_overflow_check
Definition: goto_check.cpp:230
code_returnt::return_value
const exprt & return_value() const
Definition: std_code.h:1323
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:298
true_exprt
The Boolean constant true.
Definition: std_expr.h:3984
goto_checkt::check_rec_if
void check_rec_if(const if_exprt &if_expr, guardt &guard)
Check an if expression: check the if-condition alone, and then check the true/false-cases with the gu...
Definition: goto_check.cpp:1582
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:71
goto_programt::instructiont::get_condition
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:285
constant_exprt
A constant literal expression.
Definition: std_expr.h:3935
ieee_float_equal_exprt
IEEE-floating-point equality.
Definition: std_expr.h:3718
goto_checkt::assertions
assertionst assertions
Definition: goto_check.cpp:215
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:461
exprt::is_boolean
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.cpp:119
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:817
member_offset_expr
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
Definition: pointer_offset_size.cpp:226
array_name.h
binary_exprt::op1
exprt & op1()
Definition: expr.h:104
comment
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
to_multi_ary_expr
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:872
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
std_expr.h
to_binary_relation_expr
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:774
goto_programt::instructiont::is_target
bool is_target() const
Is this node a branch target?
Definition: goto_program.h:337
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:3943
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:252
goto_checkt::conditiont::conditiont
conditiont(const exprt &_assertion, const std::string &_description)
Definition: goto_check.cpp:158
dynamic_size
exprt dynamic_size(const namespacet &ns)
Definition: pointer_predicates.cpp:66
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
c_types.h
goto_checkt::check_rec_arithmetic_op
void check_rec_arithmetic_op(const exprt &expr, guardt &guard)
Check that an arithmetic operation is valid: overflow check, NaN-check (for floating point numbers),...
Definition: goto_check.cpp:1656
optionst::get_list_option
const value_listt & get_list_option(const std::string &option) const
Definition: options.cpp:80
to_shl_expr
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
Definition: std_expr.h:2609
ieee_floatt::minus_infinity
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:203
goto_checkt::goto_checkt
goto_checkt(const namespacet &_ns, const optionst &_options)
Definition: goto_check.cpp:44
goto_checkt::conversion_check
void conversion_check(const exprt &, const guardt &)
Definition: goto_check.cpp:481
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
code_function_callt::function
exprt & function()
Definition: std_code.h:1221
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1172
binary_exprt::op0
exprt & op0()
Definition: expr.h:101
validation_modet::INVARIANT
@ INVARIANT
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1089
mod_exprt
Modulo.
Definition: std_expr.h:1106
c_enum_typet::members
const memberst & members() const
Definition: std_types.h:646
flag_resett::flags_to_reset
std::list< std::pair< bool *, bool > > flags_to_reset
Definition: goto_check.cpp:1811
goto_programt::instructiont::is_return
bool is_return() const
Definition: goto_program.h:459
shl_exprt
Left shift.
Definition: std_expr.h:2590
configt::cppt::cpp_standard
enum configt::cppt::cpp_standardt cpp_standard
not_exprt
Boolean negation.
Definition: std_expr.h:2872
object_descriptor_exprt::offset
exprt & offset()
Definition: std_expr.h:1887