cprover
goto_check_c.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Checks for Errors in C/C++ Programs
4
5Author: 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>
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{
50public:
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
100protected:
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
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
343static 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
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",
437 expr,
438 guard);
439}
440
441void 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",
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",
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",
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",
521 expr,
522 guard);
523 }
524 }
525 else
526 {
528 false_exprt(),
529 "shift of non-integer type",
530 "undefined-shift",
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",
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",
586 expr,
587 guard);
588 }
589}
590
591void 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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
994 expr,
995 guard);
996 }
997}
998
999void 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
1107void 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
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
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 =
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
1407std::string goto_check_ct::array_name(const exprt &expr)
1408{
1409 return ::array_name(ns, expr);
1410}
1411
1412void goto_check_ct::bounds_check(const exprt &expr, const guardt &guard)
1413{
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 {
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
1643void 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
1666void goto_check_ct::check_rec_logical_op(const exprt &expr, const guardt &guard)
1667{
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
1693void 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
1798void 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 {
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 }
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
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{
1942public:
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
2003private:
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;
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(
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
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 {
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(
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 bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_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 & lhs()
Definition: std_expr.h:580
exprt & rhs()
Definition: std_expr.h:590
exprt & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
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
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.cpp:51
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
const source_locationt & source_location() const
Definition: expr.h:230
source_locationt & add_source_location()
Definition: expr.h:235
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
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Definition: goto_program.h:243
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
Definition: goto_program.h:285
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
bool is_target() const
Is this node a branch target?
Definition: goto_program.h:434
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
Definition: goto_program.h:257
bool is_set_return_value() const
Definition: goto_program.h:473
const codet & get_code() const
Get the code represented by this instruction.
Definition: goto_program.h:187
bool has_condition() const
Does this instruction have a condition?
Definition: goto_program.h:360
const codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:313
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:367
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
Definition: goto_program.h:299
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:199
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
Definition: goto_program.h:213
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
Definition: goto_program.h:271
source_locationt & source_location_nonconst()
Definition: goto_program.h:337
const source_locationt & source_location() const
Definition: goto_program.h:332
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 & cond()
Definition: std_expr.h:2243
exprt & false_case()
Definition: std_expr.h:2263
exprt & true_case()
Definition: std_expr.h:2253
Boolean implication.
Definition: std_expr.h:2037
Array index operator.
Definition: std_expr.h:1328
exprt & index()
Definition: std_expr.h:1363
exprt & array()
Definition: std_expr.h:1353
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
bool is_not_nil() const
Definition: irep.h:380
const std::string & id_string() const
Definition: irep.h:399
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
void add_pragma(const irep_idt &pragma)
const irep_idt & get_property_class() const
const irept::named_subt & get_pragmas() const
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:23
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 address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:704
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
optionalt< exprt > size_of_expr(const typet &type, 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 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 mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1160
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1044
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1113
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 unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
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 if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:998
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2062
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 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)