cprover
goto_check_c.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Checks for Errors in C/C++ Programs
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_check_c.h"
13 
14 #include <algorithm>
15 #include <optional>
16 
17 #include <util/arith_tools.h>
18 #include <util/array_name.h>
19 #include <util/bitvector_expr.h>
20 #include <util/c_types.h>
21 #include <util/config.h>
22 #include <util/cprover_prefix.h>
23 #include <util/expr_util.h>
24 #include <util/find_symbols.h>
25 #include <util/floatbv_expr.h>
26 #include <util/ieee_float.h>
27 #include <util/invariant.h>
28 #include <util/make_unique.h>
29 #include <util/mathematical_expr.h>
30 #include <util/message.h>
31 #include <util/options.h>
32 #include <util/pointer_expr.h>
35 #include <util/prefix.h>
36 #include <util/simplify_expr.h>
37 #include <util/std_code.h>
38 #include <util/std_expr.h>
39 
40 #include <langapi/language.h>
41 #include <langapi/mode.h>
42 
45 
47 
49 {
50 public:
52  const namespacet &_ns,
53  const optionst &_options,
54  message_handlert &_message_handler)
55  : ns(_ns), local_bitvector_analysis(nullptr), log(_message_handler)
56  {
57  no_enum_check = false;
58  enable_bounds_check = _options.get_bool_option("bounds-check");
59  enable_pointer_check = _options.get_bool_option("pointer-check");
60  enable_memory_leak_check = _options.get_bool_option("memory-leak-check");
61  enable_div_by_zero_check = _options.get_bool_option("div-by-zero-check");
62  enable_enum_range_check = _options.get_bool_option("enum-range-check");
64  _options.get_bool_option("signed-overflow-check");
66  _options.get_bool_option("unsigned-overflow-check");
68  _options.get_bool_option("pointer-overflow-check");
69  enable_conversion_check = _options.get_bool_option("conversion-check");
71  _options.get_bool_option("undefined-shift-check");
73  _options.get_bool_option("float-overflow-check");
74  enable_simplify = _options.get_bool_option("simplify");
75  enable_nan_check = _options.get_bool_option("nan-check");
76  retain_trivial = _options.get_bool_option("retain-trivial-checks");
77  enable_assert_to_assume = _options.get_bool_option("assert-to-assume");
78  enable_assertions = _options.get_bool_option("assertions");
80  _options.get_bool_option("built-in-assertions");
81  enable_assumptions = _options.get_bool_option("assumptions");
82  error_labels = _options.get_list_option("error-label");
84  _options.get_bool_option("pointer-primitive-check");
85  }
86 
88 
89  void goto_check(
90  const irep_idt &function_identifier,
91  goto_functiont &goto_function);
92 
98  void collect_allocations(const goto_functionst &goto_functions);
99 
100 protected:
101  const namespacet &ns;
102  std::unique_ptr<local_bitvector_analysist> local_bitvector_analysis;
105 
107 
108  using guardt = std::function<exprt(exprt)>;
109  const guardt identity = [](exprt expr) { return expr; };
110 
116  void check_rec_address(const exprt &expr, const guardt &guard);
117 
125  void check_rec_logical_op(const exprt &expr, const guardt &guard);
126 
133  void check_rec_if(const if_exprt &if_expr, const guardt &guard);
134 
145  bool check_rec_member(const member_exprt &member, const guardt &guard);
146 
151  void check_rec_div(const div_exprt &div_expr, const guardt &guard);
152 
157  void check_rec_arithmetic_op(const exprt &expr, const guardt &guard);
158 
164  void check_rec(const exprt &expr, const guardt &guard);
165 
168  void check(const exprt &expr);
169 
170  struct conditiont
171  {
172  conditiont(const exprt &_assertion, const std::string &_description)
173  : assertion(_assertion), description(_description)
174  {
175  }
176 
178  std::string description;
179  };
180 
181  using conditionst = std::list<conditiont>;
182 
183  void bounds_check(const exprt &, const guardt &);
184  void bounds_check_index(const index_exprt &, const guardt &);
185  void bounds_check_bit_count(const unary_exprt &, const guardt &);
186  void div_by_zero_check(const div_exprt &, const guardt &);
187  void mod_by_zero_check(const mod_exprt &, const guardt &);
188  void mod_overflow_check(const mod_exprt &, const guardt &);
189  void enum_range_check(const exprt &, const guardt &);
190  void undefined_shift_check(const shift_exprt &, const guardt &);
191  void pointer_rel_check(const binary_exprt &, const guardt &);
192  void pointer_overflow_check(const exprt &, const guardt &);
193 
200  const dereference_exprt &expr,
201  const exprt &src_expr,
202  const guardt &guard);
203 
209  void pointer_primitive_check(const exprt &expr, const guardt &guard);
210 
217  bool requires_pointer_primitive_check(const exprt &expr);
218 
220  get_pointer_is_null_condition(const exprt &address, const exprt &size);
222  const exprt &address,
223  const exprt &size);
225  const exprt &pointer,
226  const exprt &size);
227 
229  const exprt &address,
230  const exprt &size);
231  void integer_overflow_check(const exprt &, const guardt &);
232  void conversion_check(const exprt &, const guardt &);
233  void float_overflow_check(const exprt &, const guardt &);
234  void nan_check(const exprt &, const guardt &);
236 
237  std::string array_name(const exprt &);
238 
248  const exprt &asserted_expr,
249  const std::string &comment,
250  const std::string &property_class,
251  const source_locationt &source_location,
252  const exprt &src_expr,
253  const guardt &guard);
254 
256  typedef std::set<std::pair<exprt, exprt>> assertionst;
258 
263  void invalidate(const exprt &lhs);
264 
284 
286  std::map<irep_idt, bool *> name_to_flag{
287  {"bounds-check", &enable_bounds_check},
288  {"pointer-check", &enable_pointer_check},
289  {"memory-leak-check", &enable_memory_leak_check},
290  {"div-by-zero-check", &enable_div_by_zero_check},
291  {"enum-range-check", &enable_enum_range_check},
292  {"signed-overflow-check", &enable_signed_overflow_check},
293  {"unsigned-overflow-check", &enable_unsigned_overflow_check},
294  {"pointer-overflow-check", &enable_pointer_overflow_check},
295  {"conversion-check", &enable_conversion_check},
296  {"undefined-shift-check", &enable_undefined_shift_check},
297  {"float-overflow-check", &enable_float_overflow_check},
298  {"nan-check", &enable_nan_check},
299  {"pointer-primitive-check", &enable_pointer_primitive_check}};
300 
303 
304  // the first element of the pair is the base address,
305  // and the second is the size of the region
306  typedef std::pair<exprt, exprt> allocationt;
307  typedef std::list<allocationt> allocationst;
309 
311 
314  void add_active_named_check_pragmas(source_locationt &source_location) const;
315 
318  void
320 
322  typedef enum
323  {
326  CHECKED
328 
331 
340  named_check_statust match_named_check(const irep_idt &named_check) const;
341 };
342 
343 static exprt implication(exprt lhs, exprt rhs)
344 {
345  // rewrite a => (b => c) to (a && b) => c
346  if(rhs.id() == ID_implies)
347  {
348  const auto &rhs_implication = to_implies_expr(rhs);
349  return implies_exprt(
350  and_exprt(std::move(lhs), rhs_implication.lhs()), rhs_implication.rhs());
351  }
352  else
353  {
354  return implies_exprt(std::move(lhs), std::move(rhs));
355  }
356 }
357 
359 {
360  for(const auto &gf_entry : goto_functions.function_map)
361  {
362  for(const auto &instruction : gf_entry.second.body.instructions)
363  {
364  if(!instruction.is_function_call())
365  continue;
366 
367  const auto &function = instruction.call_function();
368  if(
369  function.id() != ID_symbol ||
371  "allocated_memory")
372  continue;
373 
374  const code_function_callt::argumentst &args =
375  instruction.call_arguments();
376  if(
377  args.size() != 2 || args[0].type().id() != ID_unsignedbv ||
378  args[1].type().id() != ID_unsignedbv)
379  throw "expected two unsigned arguments to " CPROVER_PREFIX
380  "allocated_memory";
381 
383  args[0].type() == args[1].type(),
384  "arguments of allocated_memory must have same type");
385  allocations.push_back({args[0], args[1]});
386  }
387  }
388 }
389 
391 {
392  if(lhs.id() == ID_index)
393  invalidate(to_index_expr(lhs).array());
394  else if(lhs.id() == ID_member)
395  invalidate(to_member_expr(lhs).struct_op());
396  else if(lhs.id() == ID_symbol)
397  {
398  // clear all assertions about 'symbol'
399  find_symbols_sett find_symbols_set{to_symbol_expr(lhs).get_identifier()};
400 
401  for(auto it = assertions.begin(); it != assertions.end();)
402  {
403  if(
404  has_symbol(it->second, find_symbols_set) ||
405  has_subexpr(it->second, ID_dereference))
406  {
407  it = assertions.erase(it);
408  }
409  else
410  ++it;
411  }
412  }
413  else
414  {
415  // give up, clear all
416  assertions.clear();
417  }
418 }
419 
421  const div_exprt &expr,
422  const guardt &guard)
423 {
425  return;
426 
427  // add divison by zero subgoal
428 
429  exprt zero = from_integer(0, expr.op1().type());
430  const notequal_exprt inequality(expr.op1(), std::move(zero));
431 
433  inequality,
434  "division by zero",
435  "division-by-zero",
436  expr.find_source_location(),
437  expr,
438  guard);
439 }
440 
441 void goto_check_ct::enum_range_check(const exprt &expr, const guardt &guard)
442 {
444  return;
445 
446  const c_enum_tag_typet &c_enum_tag_type = to_c_enum_tag_type(expr.type());
447  symbolt enum_type = ns.lookup(c_enum_tag_type.get_identifier());
448  const c_enum_typet &c_enum_type = to_c_enum_type(enum_type.type);
449 
450  const c_enum_typet::memberst enum_values = c_enum_type.members();
451 
452  std::vector<exprt> disjuncts;
453  for(const auto &enum_value : enum_values)
454  {
455  const constant_exprt val{enum_value.get_value(), c_enum_tag_type};
456  disjuncts.push_back(equal_exprt(expr, val));
457  }
458 
459  const exprt check = disjunction(disjuncts);
460 
462  check,
463  "enum range check",
464  "enum-range-check",
465  expr.find_source_location(),
466  expr,
467  guard);
468 }
469 
471  const shift_exprt &expr,
472  const guardt &guard)
473 {
475  return;
476 
477  // Undefined for all types and shifts if distance exceeds width,
478  // and also undefined for negative distances.
479 
480  const typet &distance_type = expr.distance().type();
481 
482  if(distance_type.id() == ID_signedbv)
483  {
484  binary_relation_exprt inequality(
485  expr.distance(), ID_ge, from_integer(0, distance_type));
486 
488  inequality,
489  "shift distance is negative",
490  "undefined-shift",
491  expr.find_source_location(),
492  expr,
493  guard);
494  }
495 
496  const typet &op_type = expr.op().type();
497 
498  if(op_type.id() == ID_unsignedbv || op_type.id() == ID_signedbv)
499  {
500  exprt width_expr =
501  from_integer(to_bitvector_type(op_type).get_width(), distance_type);
502 
504  binary_relation_exprt(expr.distance(), ID_lt, std::move(width_expr)),
505  "shift distance too large",
506  "undefined-shift",
507  expr.find_source_location(),
508  expr,
509  guard);
510 
511  if(op_type.id() == ID_signedbv && expr.id() == ID_shl)
512  {
513  binary_relation_exprt inequality(
514  expr.op(), ID_ge, from_integer(0, op_type));
515 
517  inequality,
518  "shift operand is negative",
519  "undefined-shift",
520  expr.find_source_location(),
521  expr,
522  guard);
523  }
524  }
525  else
526  {
528  false_exprt(),
529  "shift of non-integer type",
530  "undefined-shift",
531  expr.find_source_location(),
532  expr,
533  guard);
534  }
535 }
536 
538  const mod_exprt &expr,
539  const guardt &guard)
540 {
542  return;
543 
544  // add divison by zero subgoal
545 
546  exprt zero = from_integer(0, expr.op1().type());
547  const notequal_exprt inequality(expr.op1(), std::move(zero));
548 
550  inequality,
551  "division by zero",
552  "division-by-zero",
553  expr.find_source_location(),
554  expr,
555  guard);
556 }
557 
560  const mod_exprt &expr,
561  const guardt &guard)
562 {
564  return;
565 
566  const auto &type = expr.type();
567 
568  if(type.id() == ID_signedbv)
569  {
570  // INT_MIN % -1 is, in principle, defined to be zero in
571  // ANSI C, C99, C++98, and C++11. Most compilers, however,
572  // fail to produce 0, and in some cases generate an exception.
573  // C11 explicitly makes this case undefined.
574 
575  notequal_exprt int_min_neq(
576  expr.op0(), to_signedbv_type(type).smallest_expr());
577 
578  notequal_exprt minus_one_neq(
579  expr.op1(), from_integer(-1, expr.op1().type()));
580 
582  or_exprt(int_min_neq, minus_one_neq),
583  "result of signed mod is not representable",
584  "overflow",
585  expr.find_source_location(),
586  expr,
587  guard);
588  }
589 }
590 
591 void goto_check_ct::conversion_check(const exprt &expr, const guardt &guard)
592 {
594  return;
595 
596  // First, check type.
597  const typet &type = expr.type();
598 
599  if(type.id() != ID_signedbv && type.id() != ID_unsignedbv)
600  return;
601 
602  if(expr.id() == ID_typecast)
603  {
604  const auto &op = to_typecast_expr(expr).op();
605 
606  // conversion to signed int may overflow
607  const typet &old_type = op.type();
608 
609  if(type.id() == ID_signedbv)
610  {
611  std::size_t new_width = to_signedbv_type(type).get_width();
612 
613  if(old_type.id() == ID_signedbv) // signed -> signed
614  {
615  std::size_t old_width = to_signedbv_type(old_type).get_width();
616  if(new_width >= old_width)
617  return; // always ok
618 
619  const binary_relation_exprt no_overflow_upper(
620  op, ID_le, from_integer(power(2, new_width - 1) - 1, old_type));
621 
622  const binary_relation_exprt no_overflow_lower(
623  op, ID_ge, from_integer(-power(2, new_width - 1), old_type));
624 
626  and_exprt(no_overflow_lower, no_overflow_upper),
627  "arithmetic overflow on signed type conversion",
628  "overflow",
629  expr.find_source_location(),
630  expr,
631  guard);
632  }
633  else if(old_type.id() == ID_unsignedbv) // unsigned -> signed
634  {
635  std::size_t old_width = to_unsignedbv_type(old_type).get_width();
636  if(new_width >= old_width + 1)
637  return; // always ok
638 
639  const binary_relation_exprt no_overflow_upper(
640  op, ID_le, from_integer(power(2, new_width - 1) - 1, old_type));
641 
643  no_overflow_upper,
644  "arithmetic overflow on unsigned to signed type conversion",
645  "overflow",
646  expr.find_source_location(),
647  expr,
648  guard);
649  }
650  else if(old_type.id() == ID_floatbv) // float -> signed
651  {
652  // Note that the fractional part is truncated!
653  ieee_floatt upper(to_floatbv_type(old_type));
654  upper.from_integer(power(2, new_width - 1));
655  const binary_relation_exprt no_overflow_upper(
656  op, ID_lt, upper.to_expr());
657 
658  ieee_floatt lower(to_floatbv_type(old_type));
659  lower.from_integer(-power(2, new_width - 1) - 1);
660  const binary_relation_exprt no_overflow_lower(
661  op, ID_gt, lower.to_expr());
662 
664  and_exprt(no_overflow_lower, no_overflow_upper),
665  "arithmetic overflow on float to signed integer type conversion",
666  "overflow",
667  expr.find_source_location(),
668  expr,
669  guard);
670  }
671  }
672  else if(type.id() == ID_unsignedbv)
673  {
674  std::size_t new_width = to_unsignedbv_type(type).get_width();
675 
676  if(old_type.id() == ID_signedbv) // signed -> unsigned
677  {
678  std::size_t old_width = to_signedbv_type(old_type).get_width();
679 
680  if(new_width >= old_width - 1)
681  {
682  // only need lower bound check
683  const binary_relation_exprt no_overflow_lower(
684  op, ID_ge, from_integer(0, old_type));
685 
687  no_overflow_lower,
688  "arithmetic overflow on signed to unsigned type conversion",
689  "overflow",
690  expr.find_source_location(),
691  expr,
692  guard);
693  }
694  else
695  {
696  // need both
697  const binary_relation_exprt no_overflow_upper(
698  op, ID_le, from_integer(power(2, new_width) - 1, old_type));
699 
700  const binary_relation_exprt no_overflow_lower(
701  op, ID_ge, from_integer(0, old_type));
702 
704  and_exprt(no_overflow_lower, no_overflow_upper),
705  "arithmetic overflow on signed to unsigned type conversion",
706  "overflow",
707  expr.find_source_location(),
708  expr,
709  guard);
710  }
711  }
712  else if(old_type.id() == ID_unsignedbv) // unsigned -> unsigned
713  {
714  std::size_t old_width = to_unsignedbv_type(old_type).get_width();
715  if(new_width >= old_width)
716  return; // always ok
717 
718  const binary_relation_exprt no_overflow_upper(
719  op, ID_le, from_integer(power(2, new_width) - 1, old_type));
720 
722  no_overflow_upper,
723  "arithmetic overflow on unsigned to unsigned type conversion",
724  "overflow",
725  expr.find_source_location(),
726  expr,
727  guard);
728  }
729  else if(old_type.id() == ID_floatbv) // float -> unsigned
730  {
731  // Note that the fractional part is truncated!
732  ieee_floatt upper(to_floatbv_type(old_type));
733  upper.from_integer(power(2, new_width) - 1);
734  const binary_relation_exprt no_overflow_upper(
735  op, ID_lt, upper.to_expr());
736 
737  ieee_floatt lower(to_floatbv_type(old_type));
738  lower.from_integer(-1);
739  const binary_relation_exprt no_overflow_lower(
740  op, ID_gt, lower.to_expr());
741 
743  and_exprt(no_overflow_lower, no_overflow_upper),
744  "arithmetic overflow on float to unsigned integer type conversion",
745  "overflow",
746  expr.find_source_location(),
747  expr,
748  guard);
749  }
750  }
751  }
752 }
753 
755  const exprt &expr,
756  const guardt &guard)
757 {
759  return;
760 
761  // First, check type.
762  const typet &type = expr.type();
763 
764  if(type.id() == ID_signedbv && !enable_signed_overflow_check)
765  return;
766 
767  if(type.id() == ID_unsignedbv && !enable_unsigned_overflow_check)
768  return;
769 
770  // add overflow subgoal
771 
772  if(expr.id() == ID_div)
773  {
774  // undefined for signed division INT_MIN/-1
775  if(type.id() == ID_signedbv)
776  {
777  const auto &div_expr = to_div_expr(expr);
778 
779  equal_exprt int_min_eq(
780  div_expr.dividend(), to_signedbv_type(type).smallest_expr());
781 
782  equal_exprt minus_one_eq(div_expr.divisor(), from_integer(-1, type));
783 
785  not_exprt(and_exprt(int_min_eq, minus_one_eq)),
786  "arithmetic overflow on signed division",
787  "overflow",
788  expr.find_source_location(),
789  expr,
790  guard);
791  }
792 
793  return;
794  }
795  else if(expr.id() == ID_unary_minus)
796  {
797  if(type.id() == ID_signedbv)
798  {
799  // overflow on unary- on signed integers can only happen with the
800  // smallest representable number 100....0
801 
802  equal_exprt int_min_eq(
803  to_unary_minus_expr(expr).op(), to_signedbv_type(type).smallest_expr());
804 
806  not_exprt(int_min_eq),
807  "arithmetic overflow on signed unary minus",
808  "overflow",
809  expr.find_source_location(),
810  expr,
811  guard);
812  }
813  else if(type.id() == ID_unsignedbv)
814  {
815  // Overflow on unary- on unsigned integers happens for all operands
816  // that are not zero.
817 
818  notequal_exprt not_eq_zero(
819  to_unary_minus_expr(expr).op(), to_unsignedbv_type(type).zero_expr());
820 
822  not_eq_zero,
823  "arithmetic overflow on unsigned unary minus",
824  "overflow",
825  expr.find_source_location(),
826  expr,
827  guard);
828  }
829 
830  return;
831  }
832  else if(expr.id() == ID_shl)
833  {
834  if(type.id() == ID_signedbv)
835  {
836  const auto &shl_expr = to_shl_expr(expr);
837  const auto &op = shl_expr.op();
838  const auto &op_type = to_signedbv_type(type);
839  const auto op_width = op_type.get_width();
840  const auto &distance = shl_expr.distance();
841  const auto &distance_type = distance.type();
842 
843  // a left shift of a negative value is undefined;
844  // yet this isn't an overflow
845  exprt neg_value_shift;
846 
847  if(op_type.id() == ID_unsignedbv)
848  neg_value_shift = false_exprt();
849  else
850  neg_value_shift =
851  binary_relation_exprt(op, ID_lt, from_integer(0, op_type));
852 
853  // a shift with negative distance is undefined;
854  // yet this isn't an overflow
855  exprt neg_dist_shift;
856 
857  if(distance_type.id() == ID_unsignedbv)
858  neg_dist_shift = false_exprt();
859  else
860  {
861  neg_dist_shift = binary_relation_exprt(
862  distance, ID_lt, from_integer(0, distance_type));
863  }
864 
865  // shifting a non-zero value by more than its width is undefined;
866  // yet this isn't an overflow
867  const exprt dist_too_large = binary_predicate_exprt(
868  distance, ID_gt, from_integer(op_width, distance_type));
869 
870  const exprt op_zero = equal_exprt(op, from_integer(0, op_type));
871 
872  auto new_type = to_bitvector_type(op_type);
873  new_type.set_width(op_width * 2);
874 
875  const exprt op_ext = typecast_exprt(op, new_type);
876 
877  const exprt op_ext_shifted = shl_exprt(op_ext, distance);
878 
879  // The semantics of signed left shifts are contentious for the case
880  // that a '1' is shifted into the signed bit.
881  // Assuming 32-bit integers, 1<<31 is implementation-defined
882  // in ANSI C and C++98, but is explicitly undefined by C99,
883  // C11 and C++11.
884  bool allow_shift_into_sign_bit = true;
885 
886  if(mode == ID_C)
887  {
888  if(
891  {
892  allow_shift_into_sign_bit = false;
893  }
894  }
895  else if(mode == ID_cpp)
896  {
897  if(
901  {
902  allow_shift_into_sign_bit = false;
903  }
904  }
905 
906  const unsigned number_of_top_bits =
907  allow_shift_into_sign_bit ? op_width : op_width + 1;
908 
909  const exprt top_bits = extractbits_exprt(
910  op_ext_shifted,
911  new_type.get_width() - 1,
912  new_type.get_width() - number_of_top_bits,
913  unsignedbv_typet(number_of_top_bits));
914 
915  const exprt top_bits_zero =
916  equal_exprt(top_bits, from_integer(0, top_bits.type()));
917 
918  // a negative distance shift isn't an overflow;
919  // a negative value shift isn't an overflow;
920  // a shift that's too far isn't an overflow;
921  // a shift of zero isn't overflow;
922  // else check the top bits
924  disjunction({neg_value_shift,
925  neg_dist_shift,
926  dist_too_large,
927  op_zero,
928  top_bits_zero}),
929  "arithmetic overflow on signed shl",
930  "overflow",
931  expr.find_source_location(),
932  expr,
933  guard);
934  }
935 
936  return;
937  }
938 
939  multi_ary_exprt overflow(
940  "overflow-" + expr.id_string(), expr.operands(), bool_typet());
941 
942  if(expr.operands().size() >= 3)
943  {
944  // The overflow checks are binary!
945  // We break these up.
946 
947  for(std::size_t i = 1; i < expr.operands().size(); i++)
948  {
949  exprt tmp;
950 
951  if(i == 1)
952  tmp = to_multi_ary_expr(expr).op0();
953  else
954  {
955  tmp = expr;
956  tmp.operands().resize(i);
957  }
958 
959  std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed";
960 
962  not_exprt{binary_overflow_exprt{tmp, expr.id(), expr.operands()[i]}},
963  "arithmetic overflow on " + kind + " " + expr.id_string(),
964  "overflow",
965  expr.find_source_location(),
966  expr,
967  guard);
968  }
969  }
970  else if(expr.operands().size() == 2)
971  {
972  std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed";
973 
974  const binary_exprt &bexpr = to_binary_expr(expr);
976  not_exprt{binary_overflow_exprt{bexpr.lhs(), expr.id(), bexpr.rhs()}},
977  "arithmetic overflow on " + kind + " " + expr.id_string(),
978  "overflow",
979  expr.find_source_location(),
980  expr,
981  guard);
982  }
983  else
984  {
985  PRECONDITION(expr.id() == ID_unary_minus);
986 
987  std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed";
988 
990  not_exprt{unary_overflow_exprt{expr.id(), to_unary_expr(expr).op()}},
991  "arithmetic overflow on " + kind + " " + expr.id_string(),
992  "overflow",
993  expr.find_source_location(),
994  expr,
995  guard);
996  }
997 }
998 
999 void goto_check_ct::float_overflow_check(const exprt &expr, const guardt &guard)
1000 {
1002  return;
1003 
1004  // First, check type.
1005  const typet &type = expr.type();
1006 
1007  if(type.id() != ID_floatbv)
1008  return;
1009 
1010  // add overflow subgoal
1011 
1012  if(expr.id() == ID_typecast)
1013  {
1014  // Can overflow if casting from larger
1015  // to smaller type.
1016  const auto &op = to_typecast_expr(expr).op();
1017  if(op.type().id() == ID_floatbv)
1018  {
1019  // float-to-float
1020  or_exprt overflow_check{isinf_exprt(op), not_exprt(isinf_exprt(expr))};
1021 
1023  std::move(overflow_check),
1024  "arithmetic overflow on floating-point typecast",
1025  "overflow",
1026  expr.find_source_location(),
1027  expr,
1028  guard);
1029  }
1030  else
1031  {
1032  // non-float-to-float
1034  not_exprt(isinf_exprt(expr)),
1035  "arithmetic overflow on floating-point typecast",
1036  "overflow",
1037  expr.find_source_location(),
1038  expr,
1039  guard);
1040  }
1041 
1042  return;
1043  }
1044  else if(expr.id() == ID_div)
1045  {
1046  // Can overflow if dividing by something small
1047  or_exprt overflow_check(
1048  isinf_exprt(to_div_expr(expr).dividend()), not_exprt(isinf_exprt(expr)));
1049 
1051  std::move(overflow_check),
1052  "arithmetic overflow on floating-point division",
1053  "overflow",
1054  expr.find_source_location(),
1055  expr,
1056  guard);
1057 
1058  return;
1059  }
1060  else if(expr.id() == ID_mod)
1061  {
1062  // Can't overflow
1063  return;
1064  }
1065  else if(expr.id() == ID_unary_minus)
1066  {
1067  // Can't overflow
1068  return;
1069  }
1070  else if(expr.id() == ID_plus || expr.id() == ID_mult || expr.id() == ID_minus)
1071  {
1072  if(expr.operands().size() == 2)
1073  {
1074  // Can overflow
1075  or_exprt overflow_check(
1076  isinf_exprt(to_binary_expr(expr).op0()),
1077  isinf_exprt(to_binary_expr(expr).op1()),
1078  not_exprt(isinf_exprt(expr)));
1079 
1080  std::string kind = expr.id() == ID_plus
1081  ? "addition"
1082  : expr.id() == ID_minus
1083  ? "subtraction"
1084  : expr.id() == ID_mult ? "multiplication" : "";
1085 
1087  std::move(overflow_check),
1088  "arithmetic overflow on floating-point " + kind,
1089  "overflow",
1090  expr.find_source_location(),
1091  expr,
1092  guard);
1093 
1094  return;
1095  }
1096  else if(expr.operands().size() >= 3)
1097  {
1098  DATA_INVARIANT(expr.id() != ID_minus, "minus expression must be binary");
1099 
1100  // break up
1101  float_overflow_check(make_binary(expr), guard);
1102  return;
1103  }
1104  }
1105 }
1106 
1107 void goto_check_ct::nan_check(const exprt &expr, const guardt &guard)
1108 {
1109  if(!enable_nan_check)
1110  return;
1111 
1112  // first, check type
1113  if(expr.type().id() != ID_floatbv)
1114  return;
1115 
1116  if(
1117  expr.id() != ID_plus && expr.id() != ID_mult && expr.id() != ID_div &&
1118  expr.id() != ID_minus)
1119  return;
1120 
1121  // add NaN subgoal
1122 
1123  exprt isnan;
1124 
1125  if(expr.id() == ID_div)
1126  {
1127  const auto &div_expr = to_div_expr(expr);
1128 
1129  // there a two ways to get a new NaN on division:
1130  // 0/0 = NaN and x/inf = NaN
1131  // (note that x/0 = +-inf for x!=0 and x!=inf)
1132  const and_exprt zero_div_zero(
1134  div_expr.op0(), from_integer(0, div_expr.dividend().type())),
1136  div_expr.op1(), from_integer(0, div_expr.divisor().type())));
1137 
1138  const isinf_exprt div_inf(div_expr.op1());
1139 
1140  isnan = or_exprt(zero_div_zero, div_inf);
1141  }
1142  else if(expr.id() == ID_mult)
1143  {
1144  if(expr.operands().size() >= 3)
1145  return nan_check(make_binary(expr), guard);
1146 
1147  const auto &mult_expr = to_mult_expr(expr);
1148 
1149  // Inf * 0 is NaN
1150  const and_exprt inf_times_zero(
1151  isinf_exprt(mult_expr.op0()),
1153  mult_expr.op1(), from_integer(0, mult_expr.op1().type())));
1154 
1155  const and_exprt zero_times_inf(
1157  mult_expr.op1(), from_integer(0, mult_expr.op1().type())),
1158  isinf_exprt(mult_expr.op0()));
1159 
1160  isnan = or_exprt(inf_times_zero, zero_times_inf);
1161  }
1162  else if(expr.id() == ID_plus)
1163  {
1164  if(expr.operands().size() >= 3)
1165  return nan_check(make_binary(expr), guard);
1166 
1167  const auto &plus_expr = to_plus_expr(expr);
1168 
1169  // -inf + +inf = NaN and +inf + -inf = NaN,
1170  // i.e., signs differ
1171  ieee_float_spect spec = ieee_float_spect(to_floatbv_type(plus_expr.type()));
1172  exprt plus_inf = ieee_floatt::plus_infinity(spec).to_expr();
1173  exprt minus_inf = ieee_floatt::minus_infinity(spec).to_expr();
1174 
1175  isnan = or_exprt(
1176  and_exprt(
1177  equal_exprt(plus_expr.op0(), minus_inf),
1178  equal_exprt(plus_expr.op1(), plus_inf)),
1179  and_exprt(
1180  equal_exprt(plus_expr.op0(), plus_inf),
1181  equal_exprt(plus_expr.op1(), minus_inf)));
1182  }
1183  else if(expr.id() == ID_minus)
1184  {
1185  // +inf - +inf = NaN and -inf - -inf = NaN,
1186  // i.e., signs match
1187 
1188  const auto &minus_expr = to_minus_expr(expr);
1189 
1190  ieee_float_spect spec =
1191  ieee_float_spect(to_floatbv_type(minus_expr.type()));
1192  exprt plus_inf = ieee_floatt::plus_infinity(spec).to_expr();
1193  exprt minus_inf = ieee_floatt::minus_infinity(spec).to_expr();
1194 
1195  isnan = or_exprt(
1196  and_exprt(
1197  equal_exprt(minus_expr.lhs(), plus_inf),
1198  equal_exprt(minus_expr.rhs(), plus_inf)),
1199  and_exprt(
1200  equal_exprt(minus_expr.lhs(), minus_inf),
1201  equal_exprt(minus_expr.rhs(), minus_inf)));
1202  }
1203  else
1204  UNREACHABLE;
1205 
1207  boolean_negate(isnan),
1208  "NaN on " + expr.id_string(),
1209  "NaN",
1210  expr.find_source_location(),
1211  expr,
1212  guard);
1213 }
1214 
1216  const binary_exprt &expr,
1217  const guardt &guard)
1218 {
1220  return;
1221 
1222  if(
1223  expr.op0().type().id() == ID_pointer &&
1224  expr.op1().type().id() == ID_pointer)
1225  {
1226  // add same-object subgoal
1227 
1228  exprt same_object = ::same_object(expr.op0(), expr.op1());
1229 
1231  same_object,
1232  "same object violation",
1233  "pointer",
1234  expr.find_source_location(),
1235  expr,
1236  guard);
1237 
1238  for(const auto &pointer : expr.operands())
1239  {
1240  // just this particular byte must be within object bounds or one past the
1241  // end
1242  const auto size = from_integer(0, size_type());
1243  auto conditions = get_pointer_dereferenceable_conditions(pointer, size);
1244 
1245  for(const auto &c : conditions)
1246  {
1248  c.assertion,
1249  "pointer relation: " + c.description,
1250  "pointer arithmetic",
1251  expr.find_source_location(),
1252  pointer,
1253  guard);
1254  }
1255  }
1256  }
1257 }
1258 
1260  const exprt &expr,
1261  const guardt &guard)
1262 {
1264  return;
1265 
1266  if(expr.id() != ID_plus && expr.id() != ID_minus)
1267  return;
1268 
1270  expr.operands().size() == 2,
1271  "pointer arithmetic expected to have exactly 2 operands");
1272 
1273  // the result must be within object bounds or one past the end
1274  const auto size = from_integer(0, size_type());
1275  auto conditions = get_pointer_dereferenceable_conditions(expr, size);
1276 
1277  for(const auto &c : conditions)
1278  {
1280  c.assertion,
1281  "pointer arithmetic: " + c.description,
1282  "pointer arithmetic",
1283  expr.find_source_location(),
1284  expr,
1285  guard);
1286  }
1287 }
1288 
1290  const dereference_exprt &expr,
1291  const exprt &src_expr,
1292  const guardt &guard)
1293 {
1295  return;
1296 
1297  const exprt &pointer = expr.pointer();
1298 
1299  exprt size;
1300 
1301  if(expr.type().id() == ID_empty)
1302  {
1303  // a dereference *p (with p being a pointer to void) is valid if p points to
1304  // valid memory (of any size). the smallest possible size of the memory
1305  // segment p could be pointing to is 1, hence we use this size for the
1306  // address check
1307  size = from_integer(1, size_type());
1308  }
1309  else
1310  {
1311  auto size_of_expr_opt = size_of_expr(expr.type(), ns);
1312  CHECK_RETURN(size_of_expr_opt.has_value());
1313  size = size_of_expr_opt.value();
1314  }
1315 
1316  auto conditions = get_pointer_dereferenceable_conditions(pointer, size);
1317 
1318  for(const auto &c : conditions)
1319  {
1321  c.assertion,
1322  "dereference failure: " + c.description,
1323  "pointer dereference",
1324  src_expr.find_source_location(),
1325  src_expr,
1326  guard);
1327  }
1328 }
1329 
1331  const exprt &expr,
1332  const guardt &guard)
1333 {
1335  return;
1336 
1337  if(expr.source_location().is_built_in())
1338  return;
1339 
1340  const exprt pointer =
1341  (expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok)
1342  ? to_r_or_w_ok_expr(expr).pointer()
1343  : to_unary_expr(expr).op();
1344 
1345  CHECK_RETURN(pointer.type().id() == ID_pointer);
1346 
1347  if(pointer.id() == ID_symbol)
1348  {
1349  const auto &symbol_expr = to_symbol_expr(pointer);
1350 
1351  if(has_prefix(id2string(symbol_expr.get_identifier()), CPROVER_PREFIX))
1352  return;
1353  }
1354 
1355  const auto size_of_expr_opt =
1356  size_of_expr(to_pointer_type(pointer.type()).base_type(), ns);
1357 
1358  const exprt size = !size_of_expr_opt.has_value()
1359  ? from_integer(1, size_type())
1360  : size_of_expr_opt.value();
1361 
1362  const conditionst &conditions =
1364  for(const auto &c : conditions)
1365  {
1367  or_exprt{null_object(pointer), c.assertion},
1368  c.description,
1369  "pointer primitives",
1370  expr.source_location(),
1371  expr,
1372  guard);
1373  }
1374 }
1375 
1377 {
1378  // we don't need to include the __CPROVER_same_object primitive here as it
1379  // is replaced by lower level primitives in the special function handling
1380  // during typechecking (see c_typecheck_expr.cpp)
1381 
1382  // pointer_object and pointer_offset are well-defined for an arbitrary
1383  // pointer-typed operand (and the operands themselves have been checked
1384  // separately for, e.g., invalid pointer dereferencing via check_rec):
1385  // pointer_object and pointer_offset just extract a subset of bits from the
1386  // pointer. If that pointer was unconstrained (non-deterministic), the result
1387  // will equally be non-deterministic.
1388  return expr.id() == ID_object_size || expr.id() == ID_r_ok ||
1389  expr.id() == ID_w_ok || expr.id() == ID_rw_ok ||
1390  expr.id() == ID_is_dynamic_object;
1391 }
1392 
1395  const exprt &address,
1396  const exprt &size)
1397 {
1398  auto conditions =
1400  if(auto maybe_null_condition = get_pointer_is_null_condition(address, size))
1401  {
1402  conditions.push_front(*maybe_null_condition);
1403  }
1404  return conditions;
1405 }
1406 
1407 std::string goto_check_ct::array_name(const exprt &expr)
1408 {
1409  return ::array_name(ns, expr);
1410 }
1411 
1412 void goto_check_ct::bounds_check(const exprt &expr, const guardt &guard)
1413 {
1414  if(!enable_bounds_check)
1415  return;
1416 
1417  if(
1418  expr.find(ID_C_bounds_check).is_not_nil() &&
1419  !expr.get_bool(ID_C_bounds_check))
1420  {
1421  return;
1422  }
1423 
1424  if(expr.id() == ID_index)
1425  bounds_check_index(to_index_expr(expr), guard);
1426  else if(
1427  expr.id() == ID_count_leading_zeros || expr.id() == ID_count_trailing_zeros)
1428  {
1429  bounds_check_bit_count(to_unary_expr(expr), guard);
1430  }
1431 }
1432 
1434  const index_exprt &expr,
1435  const guardt &guard)
1436 {
1437  const typet &array_type = expr.array().type();
1438 
1439  if(array_type.id() == ID_pointer)
1440  throw "index got pointer as array type";
1441  else if(array_type.id() != ID_array && array_type.id() != ID_vector)
1442  throw "bounds check expected array or vector type, got " +
1443  array_type.id_string();
1444 
1445  std::string name = array_name(expr.array());
1446 
1447  const exprt &index = expr.index();
1449  ode.build(expr, ns);
1450 
1451  if(index.type().id() != ID_unsignedbv)
1452  {
1453  // we undo typecasts to signedbv
1454  if(
1455  index.id() == ID_typecast &&
1456  to_typecast_expr(index).op().type().id() == ID_unsignedbv)
1457  {
1458  // ok
1459  }
1460  else
1461  {
1462  const auto i = numeric_cast<mp_integer>(index);
1463 
1464  if(!i.has_value() || *i < 0)
1465  {
1466  exprt effective_offset = ode.offset();
1467 
1468  if(ode.root_object().id() == ID_dereference)
1469  {
1470  exprt p_offset =
1472 
1473  effective_offset = plus_exprt{p_offset,
1475  effective_offset, p_offset.type())};
1476  }
1477 
1478  exprt zero = from_integer(0, ode.offset().type());
1479 
1480  // the final offset must not be negative
1481  binary_relation_exprt inequality(
1482  effective_offset, ID_ge, std::move(zero));
1483 
1485  inequality,
1486  name + " lower bound",
1487  "array bounds",
1488  expr.find_source_location(),
1489  expr,
1490  guard);
1491  }
1492  }
1493  }
1494 
1495  if(ode.root_object().id() == ID_dereference)
1496  {
1497  const exprt &pointer = to_dereference_expr(ode.root_object()).pointer();
1498 
1499  const plus_exprt effective_offset{
1500  ode.offset(),
1502  pointer_offset(pointer), ode.offset().type())};
1503 
1504  binary_relation_exprt inequality{
1505  effective_offset,
1506  ID_lt,
1508  object_size(pointer), effective_offset.type())};
1509 
1510  exprt in_bounds_of_some_explicit_allocation =
1512  pointer,
1513  plus_exprt{ode.offset(), from_integer(1, ode.offset().type())});
1514 
1515  or_exprt precond(
1516  std::move(in_bounds_of_some_explicit_allocation), inequality);
1517 
1519  precond,
1520  name + " dynamic object upper bound",
1521  "array bounds",
1522  expr.find_source_location(),
1523  expr,
1524  guard);
1525 
1526  return;
1527  }
1528 
1529  const exprt &size = array_type.id() == ID_array
1530  ? to_array_type(array_type).size()
1531  : to_vector_type(array_type).size();
1532 
1533  if(size.is_nil())
1534  {
1535  // Linking didn't complete, we don't have a size.
1536  // Not clear what to do.
1537  }
1538  else if(size.id() == ID_infinity)
1539  {
1540  }
1541  else if(size.is_zero() && expr.array().id() == ID_member)
1542  {
1543  // a variable sized struct member
1544  //
1545  // Excerpt from the C standard on flexible array members:
1546  // However, when a . (or ->) operator has a left operand that is (a pointer
1547  // to) a structure with a flexible array member and the right operand names
1548  // that member, it behaves as if that member were replaced with the longest
1549  // array (with the same element type) that would not make the structure
1550  // larger than the object being accessed; [...]
1551  const auto type_size_opt = size_of_expr(ode.root_object().type(), ns);
1552  CHECK_RETURN(type_size_opt.has_value());
1553 
1554  binary_relation_exprt inequality(
1556  ode.offset(), type_size_opt.value().type()),
1557  ID_lt,
1558  type_size_opt.value());
1559 
1561  inequality,
1562  name + " upper bound",
1563  "array bounds",
1564  expr.find_source_location(),
1565  expr,
1566  guard);
1567  }
1568  else
1569  {
1570  binary_relation_exprt inequality{
1571  typecast_exprt::conditional_cast(index, size.type()), ID_lt, size};
1572 
1574  inequality,
1575  name + " upper bound",
1576  "array bounds",
1577  expr.find_source_location(),
1578  expr,
1579  guard);
1580  }
1581 }
1582 
1584  const unary_exprt &expr,
1585  const guardt &guard)
1586 {
1587  std::string name;
1588 
1589  if(expr.id() == ID_count_leading_zeros)
1590  name = "leading";
1591  else if(expr.id() == ID_count_trailing_zeros)
1592  name = "trailing";
1593  else
1594  PRECONDITION(false);
1595 
1597  notequal_exprt{expr.op(), from_integer(0, expr.op().type())},
1598  "count " + name + " zeros is undefined for value zero",
1599  "bit count",
1600  expr.find_source_location(),
1601  expr,
1602  guard);
1603 }
1604 
1606  const exprt &asserted_expr,
1607  const std::string &comment,
1608  const std::string &property_class,
1609  const source_locationt &source_location,
1610  const exprt &src_expr,
1611  const guardt &guard)
1612 {
1613  // first try simplifier on it
1614  exprt simplified_expr =
1615  enable_simplify ? simplify_expr(asserted_expr, ns) : asserted_expr;
1616 
1617  // throw away trivial properties?
1618  if(!retain_trivial && simplified_expr.is_true())
1619  return;
1620 
1621  // add the guard
1622  exprt guarded_expr = guard(simplified_expr);
1623 
1624  if(assertions.insert(std::make_pair(src_expr, guarded_expr)).second)
1625  {
1626  auto t = new_code.add(
1628  std::move(guarded_expr), source_location)
1630  std::move(guarded_expr), source_location));
1631 
1632  std::string source_expr_string;
1633  get_language_from_mode(mode)->from_expr(src_expr, source_expr_string, ns);
1634 
1635  t->source_location_nonconst().set_comment(
1636  comment + " in " + source_expr_string);
1637  t->source_location_nonconst().set_property_class(property_class);
1638 
1639  add_all_disable_named_check_pragmas(t->source_location_nonconst());
1640  }
1641 }
1642 
1643 void goto_check_ct::check_rec_address(const exprt &expr, const guardt &guard)
1644 {
1645  // we don't look into quantifiers
1646  if(expr.id() == ID_exists || expr.id() == ID_forall)
1647  return;
1648 
1649  if(expr.id() == ID_dereference)
1650  {
1651  check_rec(to_dereference_expr(expr).pointer(), guard);
1652  }
1653  else if(expr.id() == ID_index)
1654  {
1655  const index_exprt &index_expr = to_index_expr(expr);
1656  check_rec_address(index_expr.array(), guard);
1657  check_rec(index_expr.index(), guard);
1658  }
1659  else
1660  {
1661  for(const auto &operand : expr.operands())
1662  check_rec_address(operand, guard);
1663  }
1664 }
1665 
1666 void goto_check_ct::check_rec_logical_op(const exprt &expr, const guardt &guard)
1667 {
1668  PRECONDITION(
1669  expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies);
1670  INVARIANT(
1671  expr.is_boolean(),
1672  "'" + expr.id_string() + "' must be Boolean, but got " + expr.pretty());
1673 
1674  exprt::operandst constraints;
1675 
1676  for(const auto &op : expr.operands())
1677  {
1678  INVARIANT(
1679  op.is_boolean(),
1680  "'" + expr.id_string() + "' takes Boolean operands only, but got " +
1681  op.pretty());
1682 
1683  auto new_guard = [&guard, &constraints](exprt expr) {
1684  return guard(implication(conjunction(constraints), expr));
1685  };
1686 
1687  check_rec(op, new_guard);
1688 
1689  constraints.push_back(expr.id() == ID_or ? boolean_negate(op) : op);
1690  }
1691 }
1692 
1693 void goto_check_ct::check_rec_if(const if_exprt &if_expr, const guardt &guard)
1694 {
1695  INVARIANT(
1696  if_expr.cond().is_boolean(),
1697  "first argument of if must be boolean, but got " + if_expr.cond().pretty());
1698 
1699  check_rec(if_expr.cond(), guard);
1700 
1701  {
1702  auto new_guard = [&guard, &if_expr](exprt expr) {
1703  return guard(implication(if_expr.cond(), std::move(expr)));
1704  };
1705  check_rec(if_expr.true_case(), new_guard);
1706  }
1707 
1708  {
1709  auto new_guard = [&guard, &if_expr](exprt expr) {
1710  return guard(implication(not_exprt(if_expr.cond()), std::move(expr)));
1711  };
1712  check_rec(if_expr.false_case(), new_guard);
1713  }
1714 }
1715 
1717  const member_exprt &member,
1718  const guardt &guard)
1719 {
1720  const dereference_exprt &deref = to_dereference_expr(member.struct_op());
1721 
1722  check_rec(deref.pointer(), guard);
1723 
1724  // avoid building the following expressions when pointer_validity_check
1725  // would return immediately anyway
1727  return true;
1728 
1729  // we rewrite s->member into *(s+member_offset)
1730  // to avoid requiring memory safety of the entire struct
1731  auto member_offset_opt = member_offset_expr(member, ns);
1732 
1733  if(member_offset_opt.has_value())
1734  {
1735  pointer_typet new_pointer_type = to_pointer_type(deref.pointer().type());
1736  new_pointer_type.base_type() = member.type();
1737 
1738  const exprt char_pointer = typecast_exprt::conditional_cast(
1739  deref.pointer(), pointer_type(char_type()));
1740 
1741  const exprt new_address_casted = typecast_exprt::conditional_cast(
1742  plus_exprt{char_pointer,
1744  member_offset_opt.value(), pointer_diff_type())},
1745  new_pointer_type);
1746 
1747  dereference_exprt new_deref{new_address_casted};
1748  new_deref.add_source_location() = deref.source_location();
1749  pointer_validity_check(new_deref, member, guard);
1750 
1751  return true;
1752  }
1753  return false;
1754 }
1755 
1757  const div_exprt &div_expr,
1758  const guardt &guard)
1759 {
1760  div_by_zero_check(to_div_expr(div_expr), guard);
1761 
1762  if(div_expr.type().id() == ID_signedbv)
1763  integer_overflow_check(div_expr, guard);
1764  else if(div_expr.type().id() == ID_floatbv)
1765  {
1766  nan_check(div_expr, guard);
1767  float_overflow_check(div_expr, guard);
1768  }
1769 }
1770 
1772  const exprt &expr,
1773  const guardt &guard)
1774 {
1775  if(expr.type().id() == ID_signedbv || expr.type().id() == ID_unsignedbv)
1776  {
1777  integer_overflow_check(expr, guard);
1778 
1779  if(
1780  expr.operands().size() == 2 && expr.id() == ID_minus &&
1781  expr.operands()[0].type().id() == ID_pointer &&
1782  expr.operands()[1].type().id() == ID_pointer)
1783  {
1784  pointer_rel_check(to_binary_expr(expr), guard);
1785  }
1786  }
1787  else if(expr.type().id() == ID_floatbv)
1788  {
1789  nan_check(expr, guard);
1790  float_overflow_check(expr, guard);
1791  }
1792  else if(expr.type().id() == ID_pointer)
1793  {
1794  pointer_overflow_check(expr, guard);
1795  }
1796 }
1797 
1798 void goto_check_ct::check_rec(const exprt &expr, const guardt &guard)
1799 {
1800  if(expr.id() == ID_exists || expr.id() == ID_forall)
1801  {
1802  // the scoped variables may be used in the assertion
1803  const auto &quantifier_expr = to_quantifier_expr(expr);
1804 
1805  auto new_guard = [&guard, &quantifier_expr](exprt expr) {
1806  return guard(forall_exprt(quantifier_expr.symbol(), expr));
1807  };
1808 
1809  check_rec(quantifier_expr.where(), new_guard);
1810  return;
1811  }
1812  else if(expr.id() == ID_address_of)
1813  {
1814  check_rec_address(to_address_of_expr(expr).object(), guard);
1815  return;
1816  }
1817  else if(expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies)
1818  {
1819  check_rec_logical_op(expr, guard);
1820  return;
1821  }
1822  else if(expr.id() == ID_if)
1823  {
1824  check_rec_if(to_if_expr(expr), guard);
1825  return;
1826  }
1827  else if(
1828  expr.id() == ID_member &&
1829  to_member_expr(expr).struct_op().id() == ID_dereference)
1830  {
1831  if(check_rec_member(to_member_expr(expr), guard))
1832  return;
1833  }
1834 
1835  forall_operands(it, expr)
1836  check_rec(*it, guard);
1837 
1838  if(expr.type().id() == ID_c_enum_tag)
1839  enum_range_check(expr, guard);
1840 
1841  if(expr.id() == ID_index)
1842  {
1843  bounds_check(expr, guard);
1844  }
1845  else if(expr.id() == ID_div)
1846  {
1847  check_rec_div(to_div_expr(expr), guard);
1848  }
1849  else if(expr.id() == ID_shl || expr.id() == ID_ashr || expr.id() == ID_lshr)
1850  {
1851  undefined_shift_check(to_shift_expr(expr), guard);
1852 
1853  if(expr.id() == ID_shl && expr.type().id() == ID_signedbv)
1854  integer_overflow_check(expr, guard);
1855  }
1856  else if(expr.id() == ID_mod)
1857  {
1858  mod_by_zero_check(to_mod_expr(expr), guard);
1859  mod_overflow_check(to_mod_expr(expr), guard);
1860  }
1861  else if(
1862  expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
1863  expr.id() == ID_unary_minus)
1864  {
1865  check_rec_arithmetic_op(expr, guard);
1866  }
1867  else if(expr.id() == ID_typecast)
1868  conversion_check(expr, guard);
1869  else if(
1870  expr.id() == ID_le || expr.id() == ID_lt || expr.id() == ID_ge ||
1871  expr.id() == ID_gt)
1873  else if(expr.id() == ID_dereference)
1874  {
1875  pointer_validity_check(to_dereference_expr(expr), expr, guard);
1876  }
1877  else if(requires_pointer_primitive_check(expr))
1878  {
1879  pointer_primitive_check(expr, guard);
1880  }
1881  else if(
1882  expr.id() == ID_count_leading_zeros || expr.id() == ID_count_trailing_zeros)
1883  {
1884  bounds_check(expr, guard);
1885  }
1886 }
1887 
1888 void goto_check_ct::check(const exprt &expr)
1889 {
1890  check_rec(expr, identity);
1891 }
1892 
1895 {
1896  bool modified = false;
1897 
1898  for(auto &op : expr.operands())
1899  {
1900  auto op_result = rw_ok_check(op);
1901  if(op_result.has_value())
1902  {
1903  op = *op_result;
1904  modified = true;
1905  }
1906  }
1907 
1908  if(expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok)
1909  {
1910  // these get an address as first argument and a size as second
1912  expr.operands().size() == 2, "r/w_ok must have two operands");
1913 
1914  const auto conditions = get_pointer_dereferenceable_conditions(
1915  to_r_or_w_ok_expr(expr).pointer(), to_r_or_w_ok_expr(expr).size());
1916 
1917  exprt::operandst conjuncts;
1918 
1919  for(const auto &c : conditions)
1920  conjuncts.push_back(c.assertion);
1921 
1922  exprt c = conjunction(conjuncts);
1923  if(enable_simplify)
1924  simplify(c, ns);
1925  return c;
1926  }
1927  else if(modified)
1928  return std::move(expr);
1929  else
1930  return {};
1931 }
1932 
1941 {
1942 public:
1943  explicit flag_resett(const goto_programt::instructiont &_instruction)
1944  : instruction(_instruction)
1945  {
1946  }
1947 
1953  void set_flag(bool &flag, bool new_value, const irep_idt &flag_name)
1954  {
1955  // make this a no-op if the flag is disabled
1956  if(disabled_flags.find(&flag) != disabled_flags.end())
1957  return;
1958 
1959  // detect double sets
1960  INVARIANT(
1961  flags_to_reset.find(&flag) == flags_to_reset.end(),
1962  "Flag " + id2string(flag_name) + " set twice at \n" +
1964  if(flag != new_value)
1965  {
1966  flags_to_reset[&flag] = flag;
1967  flag = new_value;
1968  }
1969  }
1970 
1975  void disable_flag(bool &flag, const irep_idt &flag_name)
1976  {
1977  INVARIANT(
1978  disabled_flags.find(&flag) == disabled_flags.end(),
1979  "Flag " + id2string(flag_name) + " disabled twice at \n" +
1981 
1982  disabled_flags.insert(&flag);
1983 
1984  // If the flag has not already been set,
1985  // we store its current value in the reset map.
1986  // Otherwise, the reset map already holds
1987  // the initial value we want to reset it to, keep it as is.
1988  if(flags_to_reset.find(&flag) == flags_to_reset.end())
1989  flags_to_reset[&flag] = flag;
1990 
1991  // set the flag to false in all cases.
1992  flag = false;
1993  }
1994 
1998  {
1999  for(const auto &flag_pair : flags_to_reset)
2000  *flag_pair.first = flag_pair.second;
2001  }
2002 
2003 private:
2005  std::map<bool *, bool> flags_to_reset;
2006  std::set<bool *> disabled_flags;
2007 };
2008 
2010  const irep_idt &function_identifier,
2011  goto_functiont &goto_function)
2012 {
2013  const auto &function_symbol = ns.lookup(function_identifier);
2014  mode = function_symbol.mode;
2015 
2016  if(mode != ID_C && mode != ID_cpp)
2017  return;
2018 
2019  assertions.clear();
2020 
2021  bool did_something = false;
2022 
2024  util_make_unique<local_bitvector_analysist>(goto_function, ns);
2025 
2026  goto_programt &goto_program = goto_function.body;
2027 
2028  Forall_goto_program_instructions(it, goto_program)
2029  {
2030  current_target = it;
2031  goto_programt::instructiont &i = *it;
2032 
2033  flag_resett resetter(i);
2034  const auto &pragmas = i.source_location().get_pragmas();
2035  for(const auto &d : pragmas)
2036  {
2037  // match named-check related pragmas
2038  auto matched = match_named_check(d.first);
2039  if(matched.has_value())
2040  {
2041  auto named_check = matched.value();
2042  auto name = named_check.first;
2043  auto status = named_check.second;
2044  bool *flag = name_to_flag.find(name)->second;
2045  switch(status)
2046  {
2047  case check_statust::ENABLE:
2048  resetter.set_flag(*flag, true, name);
2049  break;
2050  case check_statust::DISABLE:
2051  resetter.set_flag(*flag, false, name);
2052  break;
2053  case check_statust::CHECKED:
2054  resetter.disable_flag(*flag, name);
2055  break;
2056  }
2057  }
2058  }
2059 
2060  // add checked pragmas for all active checks
2062 
2063  new_code.clear();
2064 
2065  // we clear all recorded assertions if
2066  // 1) we want to generate all assertions or
2067  // 2) the instruction is a branch target
2068  if(retain_trivial || i.is_target())
2069  assertions.clear();
2070 
2071  if(i.has_condition())
2072  {
2073  check(i.get_condition());
2074  }
2075 
2076  // magic ERROR label?
2077  for(const auto &label : error_labels)
2078  {
2079  if(std::find(i.labels.begin(), i.labels.end(), label) != i.labels.end())
2080  {
2081  auto t = new_code.add(
2085  false_exprt{}, i.source_location()));
2086 
2087  t->source_location_nonconst().set_property_class("error label");
2088  t->source_location_nonconst().set_comment("error label " + label);
2089  t->source_location_nonconst().set("user-provided", true);
2090  }
2091  }
2092 
2093  if(i.is_other())
2094  {
2095  const auto &code = i.get_other();
2096  const irep_idt &statement = code.get_statement();
2097 
2098  if(statement == ID_expression)
2099  {
2100  check(code);
2101  }
2102  else if(statement == ID_printf)
2103  {
2104  for(const auto &op : code.operands())
2105  check(op);
2106  }
2107  }
2108  else if(i.is_assign())
2109  {
2110  const exprt &assign_lhs = i.assign_lhs();
2111  const exprt &assign_rhs = i.assign_rhs();
2112 
2113  // Reset the no_enum_check with the flag reset for exception
2114  // safety
2115  {
2116  flag_resett resetter(i);
2117  resetter.set_flag(no_enum_check, true, "no_enum_check");
2118  check(assign_lhs);
2119  }
2120 
2121  check(assign_rhs);
2122 
2123  // the LHS might invalidate any assertion
2124  invalidate(assign_lhs);
2125  }
2126  else if(i.is_function_call())
2127  {
2128  check(i.call_lhs());
2129  check(i.call_function());
2130 
2131  for(const auto &arg : i.call_arguments())
2132  check(arg);
2133 
2134  // the call might invalidate any assertion
2135  assertions.clear();
2136  }
2137  else if(i.is_set_return_value())
2138  {
2139  check(i.return_value());
2140  // the return value invalidate any assertion
2141  invalidate(i.return_value());
2142  }
2143  else if(i.is_throw())
2144  {
2145  if(
2146  i.get_code().get_statement() == ID_expression &&
2147  i.get_code().operands().size() == 1 &&
2148  i.get_code().op0().operands().size() == 1)
2149  {
2150  // must not throw NULL
2151 
2152  exprt pointer = to_unary_expr(i.get_code().op0()).op();
2153 
2154  const notequal_exprt not_eq_null(
2155  pointer, null_pointer_exprt(to_pointer_type(pointer.type())));
2156 
2158  not_eq_null,
2159  "throwing null",
2160  "pointer dereference",
2161  i.source_location(),
2162  pointer,
2163  identity);
2164  }
2165 
2166  // this has no successor
2167  assertions.clear();
2168  }
2169  else if(i.is_assert())
2170  {
2171  bool is_user_provided = i.source_location().get_bool("user-provided");
2172 
2173  if(
2174  (is_user_provided && !enable_assertions &&
2175  i.source_location().get_property_class() != "error label") ||
2176  (!is_user_provided && !enable_built_in_assertions))
2177  {
2178  i.turn_into_skip();
2179  did_something = true;
2180  }
2181  }
2182  else if(i.is_assume())
2183  {
2184  if(!enable_assumptions)
2185  {
2186  i.turn_into_skip();
2187  did_something = true;
2188  }
2189  }
2190  else if(i.is_dead())
2191  {
2193  {
2194  const symbol_exprt &variable = i.dead_symbol();
2195 
2196  // is it dirty?
2197  if(local_bitvector_analysis->dirty(variable))
2198  {
2199  // need to mark the dead variable as dead
2200  exprt lhs = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
2201  exprt address_of_expr = typecast_exprt::conditional_cast(
2202  address_of_exprt(variable), lhs.type());
2203  if_exprt rhs(
2205  std::move(address_of_expr),
2206  lhs);
2209  std::move(lhs), std::move(rhs), i.source_location()));
2210  t->code_nonconst().add_source_location() = i.source_location();
2211  }
2212 
2213  if(
2214  variable.type().id() == ID_pointer &&
2215  function_identifier != "alloca" &&
2216  (ns.lookup(variable.get_identifier()).base_name ==
2217  "return_value___builtin_alloca" ||
2218  ns.lookup(variable.get_identifier()).base_name ==
2219  "return_value_alloca"))
2220  {
2221  // mark pointer to alloca result as dead
2222  exprt lhs = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
2223  exprt alloca_result =
2224  typecast_exprt::conditional_cast(variable, lhs.type());
2225  if_exprt rhs(
2227  std::move(alloca_result),
2228  lhs);
2231  std::move(lhs), std::move(rhs), i.source_location()));
2232  t->code_nonconst().add_source_location() = i.source_location();
2233  }
2234  }
2235  }
2236  else if(i.is_end_function())
2237  {
2238  if(
2239  function_identifier == goto_functionst::entry_point() &&
2241  {
2242  const symbolt &leak = ns.lookup(CPROVER_PREFIX "memory_leak");
2243  const symbol_exprt leak_expr = leak.symbol_expr();
2244 
2245  // add self-assignment to get helpful counterexample output
2246  new_code.add(goto_programt::make_assignment(leak_expr, leak_expr));
2247 
2248  source_locationt source_location;
2249  source_location.set_function(function_identifier);
2250 
2251  equal_exprt eq(
2252  leak_expr, null_pointer_exprt(to_pointer_type(leak.type)));
2254  eq,
2255  "dynamically allocated memory never freed",
2256  "memory-leak",
2257  source_location,
2258  eq,
2259  identity);
2260  }
2261  }
2262 
2263  i.transform([this](exprt expr) { return rw_ok_check(expr); });
2264 
2265  for(auto &instruction : new_code.instructions)
2266  {
2267  if(instruction.source_location().is_nil())
2268  {
2269  instruction.source_location_nonconst().id(irep_idt());
2270 
2271  if(!it->source_location().get_file().empty())
2272  instruction.source_location_nonconst().set_file(
2273  it->source_location().get_file());
2274 
2275  if(!it->source_location().get_line().empty())
2276  instruction.source_location_nonconst().set_line(
2277  it->source_location().get_line());
2278 
2279  if(!it->source_location().get_function().empty())
2280  instruction.source_location_nonconst().set_function(
2281  it->source_location().get_function());
2282 
2283  if(!it->source_location().get_column().empty())
2284  {
2285  instruction.source_location_nonconst().set_column(
2286  it->source_location().get_column());
2287  }
2288  }
2289  }
2290 
2291  // insert new instructions -- make sure targets are not moved
2292  did_something |= !new_code.instructions.empty();
2293 
2294  while(!new_code.instructions.empty())
2295  {
2296  goto_program.insert_before_swap(it, new_code.instructions.front());
2297  new_code.instructions.pop_front();
2298  it++;
2299  }
2300  }
2301 
2302  if(did_something)
2303  remove_skip(goto_program);
2304 }
2305 
2308  const exprt &address,
2309  const exprt &size)
2310 {
2312  PRECONDITION(address.type().id() == ID_pointer);
2315 
2316  conditionst conditions;
2317 
2318  const exprt in_bounds_of_some_explicit_allocation =
2320 
2321  const bool unknown = flags.is_unknown() || flags.is_uninitialized();
2322 
2323  if(unknown)
2324  {
2325  conditions.push_back(conditiont{
2326  not_exprt{is_invalid_pointer_exprt{address}}, "pointer invalid"});
2327  }
2328 
2329  if(unknown || flags.is_dynamic_heap())
2330  {
2331  conditions.push_back(conditiont(
2332  or_exprt(
2333  in_bounds_of_some_explicit_allocation,
2334  not_exprt(deallocated(address, ns))),
2335  "deallocated dynamic object"));
2336  }
2337 
2338  if(unknown || flags.is_dynamic_local())
2339  {
2340  conditions.push_back(conditiont(
2341  or_exprt(
2342  in_bounds_of_some_explicit_allocation,
2343  not_exprt(dead_object(address, ns))),
2344  "dead object"));
2345  }
2346 
2347  if(flags.is_dynamic_heap())
2348  {
2349  const or_exprt object_bounds_violation(
2350  object_lower_bound(address, nil_exprt()),
2351  object_upper_bound(address, size));
2352 
2353  conditions.push_back(conditiont(
2354  or_exprt(
2355  in_bounds_of_some_explicit_allocation,
2356  not_exprt(object_bounds_violation)),
2357  "pointer outside dynamic object bounds"));
2358  }
2359 
2360  if(unknown || flags.is_dynamic_local() || flags.is_static_lifetime())
2361  {
2362  const or_exprt object_bounds_violation(
2363  object_lower_bound(address, nil_exprt()),
2364  object_upper_bound(address, size));
2365 
2366  conditions.push_back(conditiont(
2367  or_exprt(
2368  in_bounds_of_some_explicit_allocation,
2369  not_exprt(object_bounds_violation)),
2370  "pointer outside object bounds"));
2371  }
2372 
2373  if(unknown || flags.is_integer_address())
2374  {
2375  conditions.push_back(conditiont(
2376  implies_exprt(
2377  integer_address(address), in_bounds_of_some_explicit_allocation),
2378  "invalid integer address"));
2379  }
2380 
2381  return conditions;
2382 }
2383 
2386  const exprt &address,
2387  const exprt &size)
2388 {
2390  PRECONDITION(address.type().id() == ID_pointer);
2393 
2394  if(flags.is_unknown() || flags.is_uninitialized() || flags.is_null())
2395  {
2396  return {conditiont{
2398  not_exprt(null_pointer(address))},
2399  "pointer NULL"}};
2400  }
2401 
2402  return {};
2403 }
2404 
2406  const exprt &pointer,
2407  const exprt &size)
2408 {
2409  exprt::operandst alloc_disjuncts;
2410  for(const auto &a : allocations)
2411  {
2412  typecast_exprt int_ptr(pointer, a.first.type());
2413 
2414  binary_relation_exprt lb_check(a.first, ID_le, int_ptr);
2415 
2416  plus_exprt upper_bound{
2417  int_ptr, typecast_exprt::conditional_cast(size, int_ptr.type())};
2418 
2419  binary_relation_exprt ub_check{
2420  std::move(upper_bound), ID_le, plus_exprt{a.first, a.second}};
2421 
2422  alloc_disjuncts.push_back(
2423  and_exprt{std::move(lb_check), std::move(ub_check)});
2424  }
2425  return disjunction(alloc_disjuncts);
2426 }
2427 
2429  const irep_idt &function_identifier,
2430  goto_functionst::goto_functiont &goto_function,
2431  const namespacet &ns,
2432  const optionst &options,
2433  message_handlert &message_handler)
2434 {
2435  goto_check_ct goto_check(ns, options, message_handler);
2436  goto_check.goto_check(function_identifier, goto_function);
2437 }
2438 
2440  const namespacet &ns,
2441  const optionst &options,
2442  goto_functionst &goto_functions,
2443  message_handlert &message_handler)
2444 {
2445  goto_check_ct goto_check(ns, options, message_handler);
2446 
2447  goto_check.collect_allocations(goto_functions);
2448 
2449  for(auto &gf_entry : goto_functions.function_map)
2450  {
2451  goto_check.goto_check(gf_entry.first, gf_entry.second);
2452  }
2453 }
2454 
2456  const optionst &options,
2457  goto_modelt &goto_model,
2458  message_handlert &message_handler)
2459 {
2460  const namespacet ns(goto_model.symbol_table);
2461  goto_check_c(ns, options, goto_model.goto_functions, message_handler);
2462 }
2463 
2465  source_locationt &source_location) const
2466 {
2467  for(const auto &entry : name_to_flag)
2468  if(*(entry.second))
2469  source_location.add_pragma("checked:" + id2string(entry.first));
2470 }
2471 
2473  source_locationt &source_location) const
2474 {
2475  for(const auto &entry : name_to_flag)
2476  source_location.add_pragma("disable:" + id2string(entry.first));
2477 }
2478 
2481 {
2482  auto s = id2string(named_check);
2483  auto col = s.find(":");
2484 
2485  if(col == std::string::npos)
2486  return {}; // separator not found
2487 
2488  auto name = s.substr(col + 1);
2489 
2490  if(name_to_flag.find(name) == name_to_flag.end())
2491  return {}; // name unknown
2492 
2493  check_statust status;
2494  if(!s.compare(0, 6, "enable"))
2495  status = check_statust::ENABLE;
2496  else if(!s.compare(0, 7, "disable"))
2497  status = check_statust::DISABLE;
2498  else if(!s.compare(0, 7, "checked"))
2499  status = check_statust::CHECKED;
2500  else
2501  return {}; // prefix unknow
2502 
2503  // success
2504  return std::pair<irep_idt, check_statust>{name, status};
2505 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
std::string array_name(const namespacet &ns, const exprt &expr)
Definition: array_name.cpp:19
Misc Utilities.
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
unsignedbv_typet size_type()
Definition: c_types.cpp:68
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
signedbv_typet pointer_diff_type()
Definition: c_types.cpp:238
bitvector_typet char_type()
Definition: c_types.cpp:124
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:302
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: c_types.h:344
Operator to return the address of an object.
Definition: pointer_expr.h:361
Boolean AND.
Definition: std_expr.h:1974
const exprt & size() const
Definition: std_types.h:790
A base class for binary expressions.
Definition: std_expr.h:550
exprt & op1()
Definition: expr.h:102
exprt & lhs()
Definition: std_expr.h:580
exprt & op0()
Definition: expr.h:99
exprt & rhs()
Definition: std_expr.h:590
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:643
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
std::size_t get_width() const
Definition: std_types.h:864
The Boolean type.
Definition: std_types.h:36
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: c_types.h:319
The type of C enums.
Definition: c_types.h:217
const memberst & members() const
Definition: c_types.h:255
std::vector< c_enum_membert > memberst
Definition: c_types.h:253
exprt::operandst argumentst
exprt & op0()
Definition: expr.h:99
const irep_idt & get_statement() const
Definition: std_code_base.h:65
struct configt::cppt cpp
struct configt::ansi_ct ansi_c
A constant literal expression.
Definition: std_expr.h:2807
const irep_idt & get_value() const
Definition: std_expr.h:2815
Operator to dereference a pointer.
Definition: pointer_expr.h:648
Division.
Definition: std_expr.h:1064
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
std::vector< exprt > operandst
Definition: expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
source_locationt & add_source_location()
Definition: expr.h:235
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.cpp:51
const source_locationt & source_location() const
Definition: expr.h:230
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
Extracts a sub-range of a bit-vector operand.
The Boolean constant false.
Definition: std_expr.h:2865
Allows to:
void set_flag(bool &flag, bool new_value, const irep_idt &flag_name)
Store the current value of flag and then set its value to new_value.
flag_resett(const goto_programt::instructiont &_instruction)
void disable_flag(bool &flag, const irep_idt &flag_name)
Sets the given flag to false, overriding any previous value.
std::set< bool * > disabled_flags
std::map< bool *, bool > flags_to_reset
~flag_resett()
Restore the values of all flags that have been modified via set_flag.
const goto_programt::instructiont & instruction
A forall expression.
named_check_statust match_named_check(const irep_idt &named_check) const
Matches a named-check string of the form.
void goto_check(const irep_idt &function_identifier, goto_functiont &goto_function)
void check_rec(const exprt &expr, const guardt &guard)
Recursively descend into expr and run the appropriate check for each sub-expression,...
void check_rec_logical_op(const exprt &expr, const guardt &guard)
Check a logical operation: check each operand in separation while extending the guarding condition as...
void check_rec_address(const exprt &expr, const guardt &guard)
Check an address-of expression: if it is a dereference then check the pointer if it is an index then ...
std::function< exprt(exprt)> guardt
std::string array_name(const exprt &)
void collect_allocations(const goto_functionst &goto_functions)
Fill the list of allocations allocationst with <address, size> for every allocation instruction.
bool enable_pointer_check
exprt is_in_bounds_of_some_explicit_allocation(const exprt &pointer, const exprt &size)
optionalt< exprt > rw_ok_check(exprt)
expand the r_ok, w_ok and rw_ok predicates
void enum_range_check(const exprt &, const guardt &)
void invalidate(const exprt &lhs)
Remove all assertions containing the symbol in lhs as well as all assertions containing dereference.
const namespacet & ns
check_statust
activation statuses for named checks
void float_overflow_check(const exprt &, const guardt &)
bool enable_pointer_primitive_check
void mod_overflow_check(const mod_exprt &, const guardt &)
check a mod expression for the case INT_MIN % -1
bool requires_pointer_primitive_check(const exprt &expr)
Returns true if the given expression is a pointer primitive that requires validation of the operand t...
std::map< irep_idt, bool * > name_to_flag
Maps a named-check name to the corresponding boolean flag.
std::list< conditiont > conditionst
bool enable_float_overflow_check
bool enable_conversion_check
void check_rec_div(const div_exprt &div_expr, const guardt &guard)
Check that a division is valid: check for division by zero, overflow and NaN (for floating point numb...
bool enable_pointer_overflow_check
void pointer_primitive_check(const exprt &expr, const guardt &guard)
Generates VCCs to check that pointers passed to pointer primitives are either null or valid.
void bounds_check_index(const index_exprt &, const guardt &)
bool enable_signed_overflow_check
void check(const exprt &expr)
Initiate the recursively analysis of expr with its ‘guard’ set to TRUE.
conditionst get_pointer_dereferenceable_conditions(const exprt &address, const exprt &size)
bool check_rec_member(const member_exprt &member, const guardt &guard)
Check that a member expression is valid:
optionalt< goto_check_ct::conditiont > get_pointer_is_null_condition(const exprt &address, const exprt &size)
goto_functionst::goto_functiont goto_functiont
void bounds_check(const exprt &, const guardt &)
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.
std::pair< exprt, exprt > allocationt
allocationst allocations
void pointer_overflow_check(const exprt &, const guardt &)
bool enable_memory_leak_check
void conversion_check(const exprt &, const guardt &)
void check_rec_if(const if_exprt &if_expr, const guardt &guard)
Check an if expression: check the if-condition alone, and then check the true/false-cases with the gu...
bool enable_bounds_check
void integer_overflow_check(const exprt &, const guardt &)
bool enable_assert_to_assume
void nan_check(const exprt &, const guardt &)
bool enable_built_in_assertions
bool enable_undefined_shift_check
std::list< allocationt > allocationst
bool enable_enum_range_check
goto_programt::const_targett current_target
const guardt identity
void div_by_zero_check(const div_exprt &, const guardt &)
optionalt< std::pair< irep_idt, check_statust > > named_check_statust
optional (named-check, status) pair
optionst::value_listt error_labelst
void add_active_named_check_pragmas(source_locationt &source_location) const
Adds "checked" pragmas for all currently active named checks on the given source location.
assertionst assertions
void pointer_rel_check(const binary_exprt &, const guardt &)
goto_programt new_code
goto_check_ct(const namespacet &_ns, const optionst &_options, message_handlert &_message_handler)
conditionst get_pointer_points_to_valid_memory_conditions(const exprt &address, const exprt &size)
void add_all_disable_named_check_pragmas(source_locationt &source_location) const
Adds "disable" pragmas for all named checks on the given source location.
bool enable_unsigned_overflow_check
void bounds_check_bit_count(const unary_exprt &, const guardt &)
bool enable_div_by_zero_check
error_labelst error_labels
void check_rec_arithmetic_op(const exprt &expr, const guardt &guard)
Check that an arithmetic operation is valid: overflow check, NaN-check (for floating point numbers),...
void undefined_shift_check(const shift_exprt &, const guardt &)
std::unique_ptr< local_bitvector_analysist > local_bitvector_analysis
void mod_by_zero_check(const mod_exprt &, const guardt &)
std::set< std::pair< exprt, exprt > > assertionst
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.
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
goto_programt body
Definition: goto_function.h:26
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
void transform(std::function< optionalt< exprt >(exprt)>)
Apply given transformer to all expressions; no return value means no change needed.
void turn_into_skip()
Transforms an existing instruction into a skip, retaining the source_location.
Definition: goto_program.h:448
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
Definition: goto_program.h:285
bool is_target() const
Is this node a branch target?
Definition: goto_program.h:434
bool is_set_return_value() const
Definition: goto_program.h:473
const codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:313
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
Definition: goto_program.h:271
bool has_condition() const
Does this instruction have a condition?
Definition: goto_program.h:360
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
Definition: goto_program.h:257
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:367
const codet & get_code() const
Get the code represented by this instruction.
Definition: goto_program.h:187
source_locationt & source_location_nonconst()
Definition: goto_program.h:337
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
Definition: goto_program.h:213
const source_locationt & source_location() const
Definition: goto_program.h:332
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Definition: goto_program.h:243
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:199
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
Definition: goto_program.h:299
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:934
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
void clear()
Clear the goto program.
Definition: goto_program.h:809
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:619
instructionst::iterator targett
Definition: goto_program.h:592
instructionst::const_iterator const_targett
Definition: goto_program.h:593
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:715
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:922
IEEE-floating-point equality.
Definition: floatbv_expr.h:264
constant_exprt to_expr() const
Definition: ieee_float.cpp:702
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:212
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:215
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:515
The trinary if-then-else operator.
Definition: std_expr.h:2226
exprt & true_case()
Definition: std_expr.h:2253
exprt & false_case()
Definition: std_expr.h:2263
exprt & cond()
Definition: std_expr.h:2243
Boolean implication.
Definition: std_expr.h:2037
Array index operator.
Definition: std_expr.h:1328
exprt & array()
Definition: std_expr.h:1353
exprt & index()
Definition: std_expr.h:1363
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
const std::string & id_string() const
Definition: irep.h:399
bool is_not_nil() const
Definition: irep.h:380
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
Evaluates to true if the operand is infinite.
Definition: floatbv_expr.h:132
Extract member of struct or union.
Definition: std_expr.h:2667
const exprt & struct_op() const
Definition: std_expr.h:2697
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1135
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:824
exprt & op0()
Definition: std_expr.h:844
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
The NIL expression.
Definition: std_expr.h:2874
Boolean negation.
Definition: std_expr.h:2181
Disequality.
Definition: std_expr.h:1283
The null pointer constant.
Definition: pointer_expr.h:723
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:167
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...
static const exprt & root_object(const exprt &expr)
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
const value_listt & get_list_option(const std::string &option) const
Definition: options.cpp:80
std::list< std::string > value_listt
Definition: options.h:25
Boolean OR.
Definition: std_expr.h:2082
The plus expression Associativity is not specified.
Definition: std_expr.h:914
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
const exprt & pointer() const
Definition: pointer_expr.h:741
A base class for shift and rotate operators.
exprt & distance()
exprt & op()
Left shift.
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1520
const irept::named_subt & get_pragmas() const
const irep_idt & get_property_class() const
void add_pragma(const irep_idt &pragma)
static bool is_built_in(const std::string &s)
void set_function(const irep_idt &function)
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
Symbol table entry.
Definition: symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
const irep_idt & get_identifier() const
Definition: std_types.h:410
Semantic type conversion.
Definition: std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
Generic base class for unary expressions.
Definition: std_expr.h:281
const exprt & op() const
Definition: std_expr.h:293
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
Fixed-width bit-vector with unsigned binary interpretation.
const constant_exprt & size() const
Definition: std_types.cpp:253
configt config
Definition: config.cpp:25
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define CPROVER_PREFIX
#define forall_operands(it, expr)
Definition: expr.h:18
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:35
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:138
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:126
Deprecated expression utility functions.
bool has_symbol(const exprt &src, const find_symbols_sett &symbols, bool current, bool next)
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:21
API to expression classes for floating-point arithmetic.
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
Definition: goto_check.cpp:18
void goto_check_c(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
static exprt implication(exprt lhs, exprt rhs)
Program Transformation.
Symbol Table + CFG.
#define Forall_goto_program_instructions(it, program)
dstringt irep_idt
Definition: irep.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
Abstract interface to support a programming language.
Field-insensitive, location-sensitive bitvector analysis.
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:51
nonstd::optional< T > optionalt
Definition: optional.h:35
Options.
API to expression classes for Pointers.
const r_or_w_ok_exprt & to_r_or_w_ok_expr(const exprt &expr)
Definition: pointer_expr.h:752
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:704
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
Pointer Logic.
exprt pointer_offset(const exprt &pointer)
exprt integer_address(const exprt &pointer)
exprt deallocated(const exprt &pointer, const namespacet &ns)
exprt object_size(const exprt &pointer)
exprt object_upper_bound(const exprt &pointer, const exprt &access_size)
exprt dead_object(const exprt &pointer, const namespacet &ns)
exprt same_object(const exprt &p1, const exprt &p2)
exprt null_object(const exprt &pointer)
exprt null_pointer(const exprt &pointer)
exprt object_lower_bound(const exprt &pointer, const exprt &offset)
Various predicates over pointers in programs.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:88
Program Transformation.
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
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:34
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:22
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1160
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:420
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1113
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:998
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:899
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:953
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2062
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:807
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1044
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1040
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
enum configt::ansi_ct::c_standardt c_standard
enum configt::cppt::cpp_standardt cpp_standard
conditiont(const exprt &_assertion, const std::string &_description)