cprover
Loading...
Searching...
No Matches
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 <util/arith_tools.h>
15#include <util/array_name.h>
16#include <util/bitvector_expr.h>
17#include <util/c_types.h>
18#include <util/config.h>
19#include <util/cprover_prefix.h>
20#include <util/expr_util.h>
21#include <util/find_symbols.h>
22#include <util/floatbv_expr.h>
23#include <util/ieee_float.h>
24#include <util/invariant.h>
26#include <util/message.h>
27#include <util/options.h>
28#include <util/pointer_expr.h>
31#include <util/simplify_expr.h>
32#include <util/std_code.h>
33#include <util/std_expr.h>
34
37
39#include <ansi-c/c_expr.h>
40#include <langapi/language.h>
41#include <langapi/mode.h>
42
43#include <algorithm>
44
46{
47public:
49 const namespacet &_ns,
50 const optionst &_options,
51 message_handlert &_message_handler)
52 : ns(_ns), local_bitvector_analysis(nullptr), log(_message_handler)
53 {
54 enable_bounds_check = _options.get_bool_option("bounds-check");
55 enable_pointer_check = _options.get_bool_option("pointer-check");
56 enable_memory_leak_check = _options.get_bool_option("memory-leak-check");
58 _options.get_bool_option("memory-cleanup-check");
59 enable_div_by_zero_check = _options.get_bool_option("div-by-zero-check");
61 _options.get_bool_option("float-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 error_labels = _options.get_list_option("error-label");
80 _options.get_bool_option("pointer-primitive-check");
81 }
82
84
85 void goto_check(
86 const irep_idt &function_identifier,
87 goto_functiont &goto_function);
88
94 void collect_allocations(const goto_functionst &goto_functions);
95
96protected:
97 const namespacet &ns;
98 std::unique_ptr<local_bitvector_analysist> local_bitvector_analysis;
101
102 using guardt = std::function<exprt(exprt)>;
103 const guardt identity = [](exprt expr) { return expr; };
104
106
112 void check_rec_address(const exprt &expr, const guardt &guard);
113
121 void check_rec_logical_op(const exprt &expr, const guardt &guard);
122
129 void check_rec_if(const if_exprt &if_expr, const guardt &guard);
130
141 bool check_rec_member(const member_exprt &member, const guardt &guard);
142
147 void check_rec_div(const div_exprt &div_expr, const guardt &guard);
148
153 void check_rec_arithmetic_op(const exprt &expr, const guardt &guard);
154
160 void check_rec(const exprt &expr, const guardt &guard);
161
164 void check(const exprt &expr);
165
167 {
168 conditiont(const exprt &_assertion, const std::string &_description)
169 : assertion(_assertion), description(_description)
170 {
171 }
172
174 std::string description;
175 };
176
177 using conditionst = std::list<conditiont>;
178
179 void bounds_check(const exprt &, const guardt &);
180 void bounds_check_index(const index_exprt &, const guardt &);
181 void bounds_check_bit_count(const unary_exprt &, const guardt &);
182 void div_by_zero_check(const div_exprt &, const guardt &);
183 void float_div_by_zero_check(const div_exprt &, const guardt &);
184 void mod_by_zero_check(const mod_exprt &, const guardt &);
185 void mod_overflow_check(const mod_exprt &, const guardt &);
186 void enum_range_check(const exprt &, const guardt &);
187 void undefined_shift_check(const shift_exprt &, const guardt &);
188 void pointer_rel_check(const binary_exprt &, const guardt &);
189 void pointer_overflow_check(const exprt &, const guardt &);
190 void memory_leak_check(const irep_idt &function_id);
191
198 const dereference_exprt &expr,
199 const exprt &src_expr,
200 const guardt &guard);
201
207 void pointer_primitive_check(const exprt &expr, const guardt &guard);
208
215 bool requires_pointer_primitive_check(const exprt &expr);
216
217 std::optional<goto_check_ct::conditiont>
218 get_pointer_is_null_condition(const exprt &address, const exprt &size);
220 const exprt &address,
221 const exprt &size);
223 const exprt &pointer,
224 const exprt &size);
225
227 const exprt &address,
228 const exprt &size);
229 void integer_overflow_check(const exprt &, const guardt &);
230 void conversion_check(const exprt &, const guardt &);
231 void float_overflow_check(const exprt &, const guardt &);
232 void nan_check(const exprt &, const guardt &);
233
234 std::string array_name(const exprt &);
235
246 const exprt &asserted_expr,
247 const std::string &comment,
248 const std::string &property_class,
249 bool is_fatal,
250 const source_locationt &source_location,
251 const exprt &src_expr,
252 const guardt &guard);
253
255 typedef std::set<std::pair<exprt, exprt>> assertionst;
257
262 void invalidate(const exprt &lhs);
263
282
284 std::map<irep_idt, bool *> name_to_flag{
285 {"bounds-check", &enable_bounds_check},
286 {"pointer-check", &enable_pointer_check},
287 {"memory-leak-check", &enable_memory_leak_check},
288 {"memory-cleanup-check", &enable_memory_cleanup_check},
289 {"div-by-zero-check", &enable_div_by_zero_check},
290 {"float-div-by-zero-check", &enable_float_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
330 using named_check_statust = std::optional<std::pair<irep_idt, check_statust>>;
331
340 named_check_statust match_named_check(const irep_idt &named_check) const;
341};
342
351{
352public:
357
363 void set_flag(bool &flag, bool new_value, const irep_idt &flag_name)
364 {
365 // make this a no-op if the flag is disabled
366 if(disabled_flags.find(&flag) != disabled_flags.end())
367 return;
368
369 // detect double sets
370 INVARIANT(
371 flags_to_reset.find(&flag) == flags_to_reset.end(),
372 "Flag " + id2string(flag_name) + " set twice at \n" +
374 if(flag != new_value)
375 {
376 flags_to_reset[&flag] = flag;
377 flag = new_value;
378 }
379 }
380
385 void disable_flag(bool &flag, const irep_idt &flag_name)
386 {
387 INVARIANT(
388 disabled_flags.find(&flag) == disabled_flags.end(),
389 "Flag " + id2string(flag_name) + " disabled twice at \n" +
391
392 disabled_flags.insert(&flag);
393
394 // If the flag has not already been set,
395 // we store its current value in the reset map.
396 // Otherwise, the reset map already holds
397 // the initial value we want to reset it to, keep it as is.
398 if(flags_to_reset.find(&flag) == flags_to_reset.end())
399 flags_to_reset[&flag] = flag;
400
401 // set the flag to false in all cases.
402 flag = false;
403 }
404
408 {
409 for(const auto &flag_pair : flags_to_reset)
410 *flag_pair.first = flag_pair.second;
411 }
412
413private:
415 std::map<bool *, bool> flags_to_reset;
416 std::set<bool *> disabled_flags;
417};
418
419static exprt implication(exprt lhs, exprt rhs)
420{
421 // rewrite a => (b => c) to (a && b) => c
422 if(rhs.id() == ID_implies)
423 {
424 const auto &rhs_implication = to_implies_expr(rhs);
425 return implies_exprt(
426 and_exprt(std::move(lhs), rhs_implication.lhs()), rhs_implication.rhs());
427 }
428 else
429 {
430 return implies_exprt(std::move(lhs), std::move(rhs));
431 }
432}
433
435{
436 for(const auto &gf_entry : goto_functions.function_map)
437 {
438 for(const auto &instruction : gf_entry.second.body.instructions)
439 {
440 if(!instruction.is_function_call())
441 continue;
442
443 const auto &function = instruction.call_function();
444 if(
445 function.id() != ID_symbol ||
446 to_symbol_expr(function).get_identifier() != CPROVER_PREFIX
447 "allocated_memory")
448 continue;
449
451 instruction.call_arguments();
452 if(
453 args.size() != 2 || args[0].type().id() != ID_unsignedbv ||
454 args[1].type().id() != ID_unsignedbv)
455 throw "expected two unsigned arguments to " CPROVER_PREFIX
456 "allocated_memory";
457
459 args[0].type() == args[1].type(),
460 "arguments of allocated_memory must have same type");
461 allocations.push_back({args[0], args[1]});
462 }
463 }
464}
465
467{
468 if(lhs.id() == ID_index)
469 invalidate(to_index_expr(lhs).array());
470 else if(lhs.id() == ID_member)
471 invalidate(to_member_expr(lhs).struct_op());
472 else if(lhs.id() == ID_symbol)
473 {
474 // clear all assertions about 'symbol'
475 const irep_idt &lhs_id = to_symbol_expr(lhs).get_identifier();
476
477 for(auto it = assertions.begin(); it != assertions.end();)
478 {
479 if(
480 has_symbol_expr(it->second, lhs_id, false) ||
481 has_subexpr(it->second, ID_dereference))
482 {
483 it = assertions.erase(it);
484 }
485 else
486 ++it;
487 }
488 }
489 else
490 {
491 // give up, clear all
492 assertions.clear();
493 }
494}
495
497 const div_exprt &expr,
498 const guardt &guard)
499{
501 return;
502
503 // add divison by zero subgoal
504
505 exprt zero = from_integer(0, expr.op1().type());
506 const notequal_exprt inequality(expr.op1(), std::move(zero));
507
509 inequality,
510 "division by zero",
511 "division-by-zero",
512 true, // fatal
514 expr,
515 guard);
516}
517
519 const div_exprt &expr,
520 const guardt &guard)
521{
523 return;
524
525 // add divison by zero subgoal
526
527 exprt zero = from_integer(0, expr.op1().type());
528 const notequal_exprt inequality(expr.op1(), std::move(zero));
529
531 inequality,
532 "floating-point division by zero",
533 "float-division-by-zero",
534 false, // fatal
536 expr,
537 guard);
538}
539
541{
543 return;
544
545 // we might be looking at a lowered enum_is_in_range_exprt, skip over these
546 const auto &pragmas = expr.source_location().get_pragmas();
547 for(const auto &d : pragmas)
548 {
549 if(d.first == "disable:enum-range-check")
550 return;
551 }
552
554
556 check,
557 "enum range check",
558 "enum-range-check",
559 false, // fatal
561 expr,
562 guard);
563}
564
566 const shift_exprt &expr,
567 const guardt &guard)
568{
570 return;
571
572 // Undefined for all types and shifts if distance exceeds width,
573 // and also undefined for negative distances.
574
575 const typet &distance_type = expr.distance().type();
576
577 if(distance_type.id() == ID_signedbv)
578 {
579 binary_relation_exprt inequality(
580 expr.distance(), ID_ge, from_integer(0, distance_type));
581
583 inequality,
584 "shift distance is negative",
585 "undefined-shift",
586 true, // fatal
588 expr,
589 guard);
590 }
591
592 const typet &op_type = expr.op().type();
593
594 if(op_type.id() == ID_unsignedbv || op_type.id() == ID_signedbv)
595 {
596 exprt width_expr =
597 from_integer(to_bitvector_type(op_type).get_width(), distance_type);
598
600 binary_relation_exprt(expr.distance(), ID_lt, std::move(width_expr)),
601 "shift distance too large",
602 "undefined-shift",
603 true, // fatal
605 expr,
606 guard);
607
608 if(op_type.id() == ID_signedbv && expr.id() == ID_shl)
609 {
610 binary_relation_exprt inequality(
611 expr.op(), ID_ge, from_integer(0, op_type));
612
614 inequality,
615 "shift operand is negative",
616 "undefined-shift",
617 true, // fatal
619 expr,
620 guard);
621 }
622 }
623 else
624 {
626 false_exprt(),
627 "shift of non-integer type",
628 "undefined-shift",
629 true, // fatal
631 expr,
632 guard);
633 }
634}
635
637 const mod_exprt &expr,
638 const guardt &guard)
639{
641 return;
642
643 // add divison by zero subgoal
644
645 exprt zero = from_integer(0, expr.divisor().type());
646 const notequal_exprt inequality(expr.divisor(), std::move(zero));
647
649 inequality,
650 "division by zero",
651 "division-by-zero",
652 true, // fatal
654 expr,
655 guard);
656}
657
660 const mod_exprt &expr,
661 const guardt &guard)
662{
664 return;
665
666 const auto &type = expr.type();
667
668 if(type.id() == ID_signedbv)
669 {
670 // INT_MIN % -1 is, in principle, defined to be zero in
671 // ANSI C, C99, C++98, and C++11. Most compilers, however,
672 // fail to produce 0, and in some cases generate an exception.
673 // C11 explicitly makes this case undefined.
674
675 notequal_exprt int_min_neq(
676 expr.op0(), to_signedbv_type(type).smallest_expr());
677
678 notequal_exprt minus_one_neq(
679 expr.op1(), from_integer(-1, expr.op1().type()));
680
682 or_exprt(int_min_neq, minus_one_neq),
683 "result of signed mod is not representable",
684 "overflow",
685 false, // fatal
687 expr,
688 guard);
689 }
690}
691
693{
695 return;
696
697 // First, check type.
698 const typet &type = expr.type();
699
700 if(type.id() != ID_signedbv && type.id() != ID_unsignedbv)
701 return;
702
703 if(expr.id() == ID_typecast)
704 {
705 const auto &op = to_typecast_expr(expr).op();
706
707 // conversion to signed int may overflow
708 const typet &old_type = op.type();
709
710 if(type.id() == ID_signedbv)
711 {
712 std::size_t new_width = to_signedbv_type(type).get_width();
713
714 if(old_type.id() == ID_signedbv) // signed -> signed
715 {
716 std::size_t old_width = to_signedbv_type(old_type).get_width();
717 if(new_width >= old_width)
718 return; // always ok
719
720 const binary_relation_exprt no_overflow_upper(
721 op, ID_le, from_integer(power(2, new_width - 1) - 1, old_type));
722
723 const binary_relation_exprt no_overflow_lower(
724 op, ID_ge, from_integer(-power(2, new_width - 1), old_type));
725
727 and_exprt(no_overflow_lower, no_overflow_upper),
728 "arithmetic overflow on signed type conversion",
729 "overflow",
730 false, // fatal
732 expr,
733 guard);
734 }
735 else if(old_type.id() == ID_unsignedbv) // unsigned -> signed
736 {
737 std::size_t old_width = to_unsignedbv_type(old_type).get_width();
738 if(new_width >= old_width + 1)
739 return; // always ok
740
741 const binary_relation_exprt no_overflow_upper(
742 op, ID_le, from_integer(power(2, new_width - 1) - 1, old_type));
743
745 no_overflow_upper,
746 "arithmetic overflow on unsigned to signed type conversion",
747 "overflow",
748 false, // fatal
750 expr,
751 guard);
752 }
753 else if(old_type.id() == ID_floatbv) // float -> signed
754 {
755 // Note that the fractional part is truncated!
756 ieee_floatt upper(to_floatbv_type(old_type));
757 upper.from_integer(power(2, new_width - 1));
758 const binary_relation_exprt no_overflow_upper(
759 op, ID_lt, upper.to_expr());
760
761 ieee_floatt lower(to_floatbv_type(old_type));
762 lower.from_integer(-power(2, new_width - 1) - 1);
763 const binary_relation_exprt no_overflow_lower(
764 op, ID_gt, lower.to_expr());
765
767 and_exprt(no_overflow_lower, no_overflow_upper),
768 "arithmetic overflow on float to signed integer type conversion",
769 "overflow",
770 false, // fatal
772 expr,
773 guard);
774 }
775 }
776 else if(type.id() == ID_unsignedbv)
777 {
778 std::size_t new_width = to_unsignedbv_type(type).get_width();
779
780 if(old_type.id() == ID_signedbv) // signed -> unsigned
781 {
782 std::size_t old_width = to_signedbv_type(old_type).get_width();
783
784 if(new_width >= old_width - 1)
785 {
786 // only need lower bound check
787 const binary_relation_exprt no_overflow_lower(
788 op, ID_ge, from_integer(0, old_type));
789
791 no_overflow_lower,
792 "arithmetic overflow on signed to unsigned type conversion",
793 "overflow",
794 false, // fatal
796 expr,
797 guard);
798 }
799 else
800 {
801 // need both
802 const binary_relation_exprt no_overflow_upper(
803 op, ID_le, from_integer(power(2, new_width) - 1, old_type));
804
805 const binary_relation_exprt no_overflow_lower(
806 op, ID_ge, from_integer(0, old_type));
807
809 and_exprt(no_overflow_lower, no_overflow_upper),
810 "arithmetic overflow on signed to unsigned type conversion",
811 "overflow",
812 false, // fatal
814 expr,
815 guard);
816 }
817 }
818 else if(old_type.id() == ID_unsignedbv) // unsigned -> unsigned
819 {
820 std::size_t old_width = to_unsignedbv_type(old_type).get_width();
821 if(new_width >= old_width)
822 return; // always ok
823
824 const binary_relation_exprt no_overflow_upper(
825 op, ID_le, from_integer(power(2, new_width) - 1, old_type));
826
828 no_overflow_upper,
829 "arithmetic overflow on unsigned to unsigned type conversion",
830 "overflow",
831 false, // fatal
833 expr,
834 guard);
835 }
836 else if(old_type.id() == ID_floatbv) // float -> unsigned
837 {
838 // Note that the fractional part is truncated!
839 ieee_floatt upper(to_floatbv_type(old_type));
840 upper.from_integer(power(2, new_width));
841 const binary_relation_exprt no_overflow_upper(
842 op, ID_lt, upper.to_expr());
843
844 ieee_floatt lower(to_floatbv_type(old_type));
845 lower.from_integer(-1);
846 const binary_relation_exprt no_overflow_lower(
847 op, ID_gt, lower.to_expr());
848
850 and_exprt(no_overflow_lower, no_overflow_upper),
851 "arithmetic overflow on float to unsigned integer type conversion",
852 "overflow",
853 false, // fatal
855 expr,
856 guard);
857 }
858 }
859 }
860}
861
863 const exprt &expr,
864 const guardt &guard)
865{
867 return;
868
869 // First, check type.
870 const typet &type = expr.type();
871
872 if(type.id() == ID_signedbv && !enable_signed_overflow_check)
873 return;
874
875 if(type.id() == ID_unsignedbv && !enable_unsigned_overflow_check)
876 return;
877
878 // add overflow subgoal
879
880 if(expr.id() == ID_div)
881 {
882 // undefined for signed division INT_MIN/-1
883 if(type.id() == ID_signedbv)
884 {
885 const auto &div_expr = to_div_expr(expr);
886
887 equal_exprt int_min_eq(
888 div_expr.dividend(), to_signedbv_type(type).smallest_expr());
889
890 equal_exprt minus_one_eq(div_expr.divisor(), from_integer(-1, type));
891
893 not_exprt(and_exprt(int_min_eq, minus_one_eq)),
894 "arithmetic overflow on signed division",
895 "overflow",
896 false, // fatal
898 expr,
899 guard);
900 }
901
902 return;
903 }
904 else if(expr.id() == ID_unary_minus)
905 {
906 if(type.id() == ID_signedbv)
907 {
908 // overflow on unary- on signed integers can only happen with the
909 // smallest representable number 100....0
910
911 equal_exprt int_min_eq(
912 to_unary_minus_expr(expr).op(), to_signedbv_type(type).smallest_expr());
913
915 not_exprt(int_min_eq),
916 "arithmetic overflow on signed unary minus",
917 "overflow",
918 false, // fatal
920 expr,
921 guard);
922 }
923 else if(type.id() == ID_unsignedbv)
924 {
925 // Overflow on unary- on unsigned integers happens for all operands
926 // that are not zero.
927
928 notequal_exprt not_eq_zero(
929 to_unary_minus_expr(expr).op(), to_unsignedbv_type(type).zero_expr());
930
932 not_eq_zero,
933 "arithmetic overflow on unsigned unary minus",
934 "overflow",
935 false, // fatal
937 expr,
938 guard);
939 }
940
941 return;
942 }
943 else if(expr.id() == ID_shl)
944 {
945 if(type.id() == ID_signedbv)
946 {
947 const auto &shl_expr = to_shl_expr(expr);
948 const auto &op = shl_expr.op();
949 const auto &op_type = to_signedbv_type(type);
950 const auto op_width = op_type.get_width();
951 const auto &distance = shl_expr.distance();
952 const auto &distance_type = distance.type();
953
954 // a left shift of a negative value is undefined;
955 // yet this isn't an overflow
956 exprt neg_value_shift;
957
958 if(op_type.id() == ID_unsignedbv)
959 neg_value_shift = false_exprt();
960 else
961 neg_value_shift =
962 binary_relation_exprt(op, ID_lt, from_integer(0, op_type));
963
964 // a shift with negative distance is undefined;
965 // yet this isn't an overflow
966 exprt neg_dist_shift;
967
968 if(distance_type.id() == ID_unsignedbv)
969 neg_dist_shift = false_exprt();
970 else
971 {
972 neg_dist_shift = binary_relation_exprt(
973 distance, ID_lt, from_integer(0, distance_type));
974 }
975
976 // shifting a non-zero value by more than its width is undefined;
977 // yet this isn't an overflow
978 const exprt dist_too_large = binary_predicate_exprt(
979 distance, ID_gt, from_integer(op_width, distance_type));
980
981 const exprt op_zero = equal_exprt(op, from_integer(0, op_type));
982
983 auto new_type = to_bitvector_type(op_type);
984 new_type.set_width(op_width * 2);
985
986 const exprt op_ext = typecast_exprt(op, new_type);
987
988 const exprt op_ext_shifted = shl_exprt(op_ext, distance);
989
990 // The semantics of signed left shifts are contentious for the case
991 // that a '1' is shifted into the signed bit.
992 // Assuming 32-bit integers, 1<<31 is implementation-defined
993 // in ANSI C and C++98, but is explicitly undefined by C99,
994 // C11 and C++11.
995 bool allow_shift_into_sign_bit = true;
996
997 if(mode == ID_C)
998 {
999 if(
1002 {
1003 allow_shift_into_sign_bit = false;
1004 }
1005 }
1006 else if(mode == ID_cpp)
1007 {
1008 if(
1012 {
1013 allow_shift_into_sign_bit = false;
1014 }
1015 }
1016
1017 const unsigned number_of_top_bits =
1018 allow_shift_into_sign_bit ? op_width : op_width + 1;
1019
1020 const exprt top_bits = extractbits_exprt(
1021 op_ext_shifted,
1022 new_type.get_width() - number_of_top_bits,
1023 unsignedbv_typet(number_of_top_bits));
1024
1025 const exprt top_bits_zero =
1026 equal_exprt(top_bits, from_integer(0, top_bits.type()));
1027
1028 // a negative distance shift isn't an overflow;
1029 // a negative value shift isn't an overflow;
1030 // a shift that's too far isn't an overflow;
1031 // a shift of zero isn't overflow;
1032 // else check the top bits
1035 {neg_value_shift,
1036 neg_dist_shift,
1037 dist_too_large,
1038 op_zero,
1039 top_bits_zero}),
1040 "arithmetic overflow on signed shl",
1041 "overflow",
1042 false, // fatal
1043 expr.find_source_location(),
1044 expr,
1045 guard);
1046 }
1047
1048 return;
1049 }
1050
1051 multi_ary_exprt overflow(
1052 "overflow-" + expr.id_string(), expr.operands(), bool_typet());
1053
1054 if(expr.operands().size() >= 3)
1055 {
1056 // The overflow checks are binary!
1057 // We break these up.
1058
1059 for(std::size_t i = 1; i < expr.operands().size(); i++)
1060 {
1061 exprt tmp;
1062
1063 if(i == 1)
1064 tmp = to_multi_ary_expr(expr).op0();
1065 else
1066 {
1067 tmp = expr;
1068 tmp.operands().resize(i);
1069 }
1070
1071 std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed";
1072
1074 not_exprt{binary_overflow_exprt{tmp, expr.id(), expr.operands()[i]}},
1075 "arithmetic overflow on " + kind + " " + expr.id_string(),
1076 "overflow",
1077 false, // fatal
1078 expr.find_source_location(),
1079 expr,
1080 guard);
1081 }
1082 }
1083 else if(expr.operands().size() == 2)
1084 {
1085 std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed";
1086
1087 const binary_exprt &bexpr = to_binary_expr(expr);
1089 not_exprt{binary_overflow_exprt{bexpr.lhs(), expr.id(), bexpr.rhs()}},
1090 "arithmetic overflow on " + kind + " " + expr.id_string(),
1091 "overflow",
1092 false, // fatal
1093 expr.find_source_location(),
1094 expr,
1095 guard);
1096 }
1097 else
1098 {
1099 PRECONDITION(expr.id() == ID_unary_minus);
1100
1101 std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed";
1102
1105 "arithmetic overflow on " + kind + " " + expr.id_string(),
1106 "overflow",
1107 false, // fatal
1108 expr.find_source_location(),
1109 expr,
1110 guard);
1111 }
1112}
1113
1115{
1117 return;
1118
1119 // First, check type.
1120 const typet &type = expr.type();
1121
1122 if(type.id() != ID_floatbv)
1123 return;
1124
1125 // add overflow subgoal
1126
1127 if(expr.id() == ID_typecast)
1128 {
1129 // Can overflow if casting from larger
1130 // to smaller type.
1131 const auto &op = to_typecast_expr(expr).op();
1132 if(op.type().id() == ID_floatbv)
1133 {
1134 // float-to-float
1135 or_exprt overflow_check{isinf_exprt(op), not_exprt(isinf_exprt(expr))};
1136
1138 std::move(overflow_check),
1139 "arithmetic overflow on floating-point typecast",
1140 "overflow",
1141 false, // fatal
1142 expr.find_source_location(),
1143 expr,
1144 guard);
1145 }
1146 else
1147 {
1148 // non-float-to-float
1150 not_exprt(isinf_exprt(expr)),
1151 "arithmetic overflow on floating-point typecast",
1152 "overflow",
1153 false, // fatal
1154 expr.find_source_location(),
1155 expr,
1156 guard);
1157 }
1158
1159 return;
1160 }
1161 else if(expr.id() == ID_div)
1162 {
1163 // Can overflow if dividing by something small
1164 or_exprt overflow_check(
1165 isinf_exprt(to_div_expr(expr).dividend()), not_exprt(isinf_exprt(expr)));
1166
1168 std::move(overflow_check),
1169 "arithmetic overflow on floating-point division",
1170 "overflow",
1171 false, // fatal
1172 expr.find_source_location(),
1173 expr,
1174 guard);
1175
1176 return;
1177 }
1178 else if(expr.id() == ID_mod)
1179 {
1180 // Can't overflow
1181 return;
1182 }
1183 else if(expr.id() == ID_unary_minus)
1184 {
1185 // Can't overflow
1186 return;
1187 }
1188 else if(expr.id() == ID_plus || expr.id() == ID_mult || expr.id() == ID_minus)
1189 {
1190 if(expr.operands().size() == 2)
1191 {
1192 // Can overflow
1193 or_exprt overflow_check(
1194 isinf_exprt(to_binary_expr(expr).op0()),
1195 isinf_exprt(to_binary_expr(expr).op1()),
1196 not_exprt(isinf_exprt(expr)));
1197
1198 std::string kind = expr.id() == ID_plus ? "addition"
1199 : expr.id() == ID_minus ? "subtraction"
1200 : expr.id() == ID_mult ? "multiplication"
1201 : "";
1202
1204 std::move(overflow_check),
1205 "arithmetic overflow on floating-point " + kind,
1206 "overflow",
1207 false, // fatal
1208 expr.find_source_location(),
1209 expr,
1210 guard);
1211
1212 return;
1213 }
1214 else if(expr.operands().size() >= 3)
1215 {
1216 DATA_INVARIANT(expr.id() != ID_minus, "minus expression must be binary");
1217
1218 // break up
1220 return;
1221 }
1222 }
1223}
1224
1226{
1227 if(!enable_nan_check)
1228 return;
1229
1230 // first, check type
1231 if(expr.type().id() != ID_floatbv)
1232 return;
1233
1234 if(
1235 expr.id() != ID_plus && expr.id() != ID_mult && expr.id() != ID_div &&
1236 expr.id() != ID_minus)
1237 return;
1238
1239 // add NaN subgoal
1240
1241 exprt isnan;
1242
1243 if(expr.id() == ID_div)
1244 {
1245 const auto &div_expr = to_div_expr(expr);
1246
1247 // there a two ways to get a new NaN on division:
1248 // 0/0 = NaN and x/inf = NaN
1249 // (note that x/0 = +-inf for x!=0 and x!=inf)
1250 const and_exprt zero_div_zero(
1252 div_expr.op0(), from_integer(0, div_expr.dividend().type())),
1254 div_expr.op1(), from_integer(0, div_expr.divisor().type())));
1255
1256 const isinf_exprt div_inf(div_expr.op1());
1257
1258 isnan = or_exprt(zero_div_zero, div_inf);
1259 }
1260 else if(expr.id() == ID_mult)
1261 {
1262 if(expr.operands().size() >= 3)
1263 return nan_check(make_binary(expr), guard);
1264
1265 const auto &mult_expr = to_mult_expr(expr);
1266
1267 // Inf * 0 is NaN
1268 const and_exprt inf_times_zero(
1269 isinf_exprt(mult_expr.op0()),
1271 mult_expr.op1(), from_integer(0, mult_expr.op1().type())));
1272
1273 const and_exprt zero_times_inf(
1275 mult_expr.op1(), from_integer(0, mult_expr.op1().type())),
1276 isinf_exprt(mult_expr.op0()));
1277
1278 isnan = or_exprt(inf_times_zero, zero_times_inf);
1279 }
1280 else if(expr.id() == ID_plus)
1281 {
1282 if(expr.operands().size() >= 3)
1283 return nan_check(make_binary(expr), guard);
1284
1285 const auto &plus_expr = to_plus_expr(expr);
1286
1287 // -inf + +inf = NaN and +inf + -inf = NaN,
1288 // i.e., signs differ
1289 ieee_float_spect spec = ieee_float_spect(to_floatbv_type(plus_expr.type()));
1290 exprt plus_inf = ieee_floatt::plus_infinity(spec).to_expr();
1291 exprt minus_inf = ieee_floatt::minus_infinity(spec).to_expr();
1292
1293 isnan = or_exprt(
1294 and_exprt(
1295 equal_exprt(plus_expr.op0(), minus_inf),
1296 equal_exprt(plus_expr.op1(), plus_inf)),
1297 and_exprt(
1298 equal_exprt(plus_expr.op0(), plus_inf),
1299 equal_exprt(plus_expr.op1(), minus_inf)));
1300 }
1301 else if(expr.id() == ID_minus)
1302 {
1303 // +inf - +inf = NaN and -inf - -inf = NaN,
1304 // i.e., signs match
1305
1306 const auto &minus_expr = to_minus_expr(expr);
1307
1308 ieee_float_spect spec =
1309 ieee_float_spect(to_floatbv_type(minus_expr.type()));
1310 exprt plus_inf = ieee_floatt::plus_infinity(spec).to_expr();
1311 exprt minus_inf = ieee_floatt::minus_infinity(spec).to_expr();
1312
1313 isnan = or_exprt(
1314 and_exprt(
1315 equal_exprt(minus_expr.lhs(), plus_inf),
1316 equal_exprt(minus_expr.rhs(), plus_inf)),
1317 and_exprt(
1318 equal_exprt(minus_expr.lhs(), minus_inf),
1319 equal_exprt(minus_expr.rhs(), minus_inf)));
1320 }
1321 else
1323
1325 boolean_negate(isnan),
1326 "NaN on " + expr.id_string(),
1327 "NaN",
1328 false, // fatal
1329 expr.find_source_location(),
1330 expr,
1331 guard);
1332}
1333
1335 const binary_exprt &expr,
1336 const guardt &guard)
1337{
1339 return;
1340
1341 if(
1342 expr.op0().type().id() == ID_pointer &&
1343 expr.op1().type().id() == ID_pointer)
1344 {
1345 // add same-object subgoal
1346
1347 exprt same_object = ::same_object(expr.op0(), expr.op1());
1348
1351 "same object violation",
1352 "pointer",
1353 false, // fatal
1354 expr.find_source_location(),
1355 expr,
1356 guard);
1357
1358 for(const auto &pointer : expr.operands())
1359 {
1360 // just this particular byte must be within object bounds or one past the
1361 // end
1362 const auto size = from_integer(0, size_type());
1363 auto conditions = get_pointer_dereferenceable_conditions(pointer, size);
1364
1365 for(const auto &c : conditions)
1366 {
1368 c.assertion,
1369 "pointer relation: " + c.description,
1370 "pointer arithmetic",
1371 true, // fatal
1372 expr.find_source_location(),
1373 pointer,
1374 guard);
1375 }
1376 }
1377 }
1378}
1379
1381 const exprt &expr,
1382 const guardt &guard)
1383{
1385 return;
1386
1387 if(expr.id() != ID_plus && expr.id() != ID_minus)
1388 return;
1389
1391 expr.operands().size() == 2,
1392 "pointer arithmetic expected to have exactly 2 operands");
1393
1394 // multiplying the offset by the object size must not result in arithmetic
1395 // overflow
1396 const typet &object_type = to_pointer_type(expr.type()).base_type();
1397 if(object_type.id() != ID_empty)
1398 {
1399 auto size_of_expr_opt = size_of_expr(object_type, ns);
1400 CHECK_RETURN(size_of_expr_opt.has_value());
1401 exprt object_size = size_of_expr_opt.value();
1402
1403 const binary_exprt &binary_expr = to_binary_expr(expr);
1404 exprt offset_operand = binary_expr.lhs().type().id() == ID_pointer
1405 ? binary_expr.rhs()
1406 : binary_expr.lhs();
1407 mult_exprt mul{
1408 offset_operand,
1410 mul.add_source_location() = offset_operand.source_location();
1411
1412 flag_overridet override_overflow(offset_operand.source_location());
1413 override_overflow.set_flag(
1414 enable_signed_overflow_check, true, "signed_overflow_check");
1415 override_overflow.set_flag(
1416 enable_unsigned_overflow_check, true, "unsigned_overflow_check");
1418 }
1419
1420 // the result must be within object bounds or one past the end
1421 const auto size = from_integer(0, size_type());
1422 auto conditions = get_pointer_dereferenceable_conditions(expr, size);
1423
1424 for(const auto &c : conditions)
1425 {
1427 c.assertion,
1428 "pointer arithmetic: " + c.description,
1429 "pointer arithmetic",
1430 true, // fatal
1431 expr.find_source_location(),
1432 expr,
1433 guard);
1434 }
1435}
1436
1438 const dereference_exprt &expr,
1439 const exprt &src_expr,
1440 const guardt &guard)
1441{
1443 return;
1444
1445 const exprt &pointer = expr.pointer();
1446
1447 exprt size;
1448
1449 if(expr.type().id() == ID_empty)
1450 {
1451 // a dereference *p (with p being a pointer to void) is valid if p points to
1452 // valid memory (of any size). the smallest possible size of the memory
1453 // segment p could be pointing to is 1, hence we use this size for the
1454 // address check
1455 size = from_integer(1, size_type());
1456 }
1457 else
1458 {
1459 auto size_of_expr_opt = size_of_expr(expr.type(), ns);
1460 CHECK_RETURN(size_of_expr_opt.has_value());
1461 size = size_of_expr_opt.value();
1462 }
1463
1464 auto conditions = get_pointer_dereferenceable_conditions(pointer, size);
1465
1466 for(const auto &c : conditions)
1467 {
1469 c.assertion,
1470 "dereference failure: " + c.description,
1471 "pointer dereference",
1472 true, // fatal
1473 src_expr.find_source_location(),
1474 src_expr,
1475 guard);
1476 }
1477}
1478
1480 const exprt &expr,
1481 const guardt &guard)
1482{
1484 return;
1485
1486 if(expr.source_location().is_built_in())
1487 return;
1488
1489 const exprt pointer =
1490 (expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok)
1491 ? to_r_or_w_ok_expr(expr).pointer()
1494 : to_unary_expr(expr).op();
1495
1496 CHECK_RETURN(pointer.type().id() == ID_pointer);
1497
1498 if(pointer.id() == ID_symbol)
1499 {
1500 const auto &symbol_expr = to_symbol_expr(pointer);
1501
1502 if(symbol_expr.get_identifier().starts_with(CPROVER_PREFIX))
1503 return;
1504 }
1505
1507 pointer, from_integer(0, size_type()));
1508 for(const auto &c : conditions)
1509 {
1511 or_exprt{null_object(pointer), c.assertion},
1512 c.description,
1513 "pointer primitives",
1514 false, // fatal
1515 expr.source_location(),
1516 expr,
1517 guard);
1518 }
1519}
1520
1522{
1523 // we don't need to include the __CPROVER_same_object primitive here as it
1524 // is replaced by lower level primitives in the special function handling
1525 // during typechecking (see c_typecheck_expr.cpp)
1526
1527 // pointer_object and pointer_offset are well-defined for an arbitrary
1528 // pointer-typed operand (and the operands themselves have been checked
1529 // separately for, e.g., invalid pointer dereferencing via check_rec):
1530 // pointer_object and pointer_offset just extract a subset of bits from the
1531 // pointer. If that pointer was unconstrained (non-deterministic), the result
1532 // will equally be non-deterministic.
1533 return can_cast_expr<object_size_exprt>(expr) || expr.id() == ID_r_ok ||
1534 expr.id() == ID_w_ok || expr.id() == ID_rw_ok ||
1536 expr.id() == ID_is_dynamic_object;
1537}
1538
1541 const exprt &address,
1542 const exprt &size)
1543{
1544 auto conditions =
1546 if(auto maybe_null_condition = get_pointer_is_null_condition(address, size))
1547 {
1548 conditions.push_front(*maybe_null_condition);
1549 }
1550 return conditions;
1551}
1552
1553std::string goto_check_ct::array_name(const exprt &expr)
1554{
1555 return ::array_name(ns, expr);
1556}
1557
1559{
1561 return;
1562
1563 if(expr.id() == ID_index)
1565 else if(
1566 (expr.id() == ID_count_leading_zeros &&
1567 !to_count_leading_zeros_expr(expr).zero_permitted()) ||
1568 (expr.id() == ID_count_trailing_zeros &&
1569 !to_count_trailing_zeros_expr(expr).zero_permitted()))
1570 {
1572 }
1573}
1574
1576 const index_exprt &expr,
1577 const guardt &guard)
1578{
1579 const typet &array_type = expr.array().type();
1580
1581 if(array_type.id() == ID_pointer)
1582 throw "index got pointer as array type";
1583 else if(array_type.id() != ID_array && array_type.id() != ID_vector)
1584 throw "bounds check expected array or vector type, got " +
1585 array_type.id_string();
1586
1587 std::string name = array_name(expr.array());
1588
1589 const exprt &index = expr.index();
1591 ode.build(expr, ns);
1592
1593 if(index.type().id() != ID_unsignedbv)
1594 {
1595 // we undo typecasts to signedbv
1596 if(
1597 index.id() == ID_typecast &&
1598 to_typecast_expr(index).op().type().id() == ID_unsignedbv)
1599 {
1600 // ok
1601 }
1602 else
1603 {
1604 const auto i = numeric_cast<mp_integer>(index);
1605
1606 if(!i.has_value() || *i < 0)
1607 {
1608 exprt effective_offset = ode.offset();
1609
1610 if(ode.root_object().id() == ID_dereference)
1611 {
1612 exprt p_offset =
1614
1615 effective_offset = plus_exprt{
1616 p_offset,
1618 effective_offset, p_offset.type())};
1619 }
1620
1621 exprt zero = from_integer(0, effective_offset.type());
1622
1623 // the final offset must not be negative
1624 binary_relation_exprt inequality(
1625 effective_offset, ID_ge, std::move(zero));
1626
1628 inequality,
1629 name + " lower bound",
1630 "array bounds",
1631 true, // fatal
1632 expr.find_source_location(),
1633 expr,
1634 guard);
1635 }
1636 }
1637 }
1638
1639 if(ode.root_object().id() == ID_dereference)
1640 {
1641 const exprt &pointer = to_dereference_expr(ode.root_object()).pointer();
1642
1643 const plus_exprt effective_offset{
1644 ode.offset(),
1646 pointer_offset(pointer), ode.offset().type())};
1647
1648 binary_relation_exprt inequality{
1649 effective_offset,
1650 ID_lt,
1652 object_size(pointer), effective_offset.type())};
1653
1654 exprt in_bounds_of_some_explicit_allocation =
1656 pointer,
1657 plus_exprt{ode.offset(), from_integer(1, ode.offset().type())});
1658
1659 or_exprt precond(
1660 std::move(in_bounds_of_some_explicit_allocation), inequality);
1661
1663 precond,
1664 name + " dynamic object upper bound",
1665 "array bounds",
1666 false, // fatal
1667 expr.find_source_location(),
1668 expr,
1669 guard);
1670
1671 return;
1672 }
1673
1674 const exprt &size = array_type.id() == ID_array
1675 ? to_array_type(array_type).size()
1676 : to_vector_type(array_type).size();
1677
1678 if(size.is_nil() && !array_type.get_bool(ID_C_flexible_array_member))
1679 {
1680 // Linking didn't complete, we don't have a size.
1681 // Not clear what to do.
1682 }
1683 else if(size.id() == ID_infinity)
1684 {
1685 }
1686 else if(
1687 expr.array().id() == ID_member &&
1688 (size.is_zero() || array_type.get_bool(ID_C_flexible_array_member)))
1689 {
1690 // a variable sized struct member
1691 //
1692 // Excerpt from the C standard on flexible array members:
1693 // However, when a . (or ->) operator has a left operand that is (a pointer
1694 // to) a structure with a flexible array member and the right operand names
1695 // that member, it behaves as if that member were replaced with the longest
1696 // array (with the same element type) that would not make the structure
1697 // larger than the object being accessed; [...]
1698 const auto type_size_opt =
1700 CHECK_RETURN(type_size_opt.has_value());
1701
1702 binary_relation_exprt inequality(
1703 ode.offset(),
1704 ID_lt,
1705 from_integer(type_size_opt.value(), ode.offset().type()));
1706
1708 inequality,
1709 name + " upper bound",
1710 "array bounds",
1711 true, // fatal
1712 expr.find_source_location(),
1713 expr,
1714 guard);
1715 }
1716 else
1717 {
1718 binary_relation_exprt inequality{
1719 typecast_exprt::conditional_cast(index, size.type()), ID_lt, size};
1720
1722 inequality,
1723 name + " upper bound",
1724 "array bounds",
1725 true, // fatal
1726 expr.find_source_location(),
1727 expr,
1728 guard);
1729 }
1730}
1731
1733 const unary_exprt &expr,
1734 const guardt &guard)
1735{
1736 std::string name;
1737
1738 if(expr.id() == ID_count_leading_zeros)
1739 name = "leading";
1740 else if(expr.id() == ID_count_trailing_zeros)
1741 name = "trailing";
1742 else
1743 PRECONDITION(false);
1744
1746 notequal_exprt{expr.op(), from_integer(0, expr.op().type())},
1747 "count " + name + " zeros is undefined for value zero",
1748 "bit count",
1749 false, // fatal
1750 expr.find_source_location(),
1751 expr,
1752 guard);
1753}
1754
1756 const exprt &asserted_expr,
1757 const std::string &comment,
1758 const std::string &property_class,
1759 bool is_fatal,
1760 const source_locationt &source_location,
1761 const exprt &src_expr,
1762 const guardt &guard)
1763{
1764 // first try simplifier on it
1765 exprt simplified_expr =
1766 enable_simplify ? simplify_expr(asserted_expr, ns) : asserted_expr;
1767
1768 // throw away trivial properties?
1769 if(!retain_trivial && simplified_expr.is_true())
1770 return;
1771
1772 // add the guard
1773 exprt guarded_expr = guard(simplified_expr);
1774
1775 if(assertions.insert(std::make_pair(src_expr, guarded_expr)).second)
1776 {
1777 std::string source_expr_string;
1778 get_language_from_mode(mode)->from_expr(src_expr, source_expr_string, ns);
1779
1780 source_locationt annotated_location = source_location;
1781 annotated_location.set_comment(comment + " in " + source_expr_string);
1782 annotated_location.set_property_class(property_class);
1783
1784 add_all_checked_named_check_pragmas(annotated_location);
1785
1787 {
1789 std::move(guarded_expr), annotated_location));
1790 }
1791 else
1792 {
1793 if(is_fatal)
1794 annotated_location.property_fatal(true);
1795
1797 std::move(guarded_expr), annotated_location));
1798 }
1799 }
1800}
1801
1803{
1804 // we don't look into quantifiers
1805 if(expr.id() == ID_exists || expr.id() == ID_forall)
1806 return;
1807
1808 if(expr.id() == ID_dereference)
1809 {
1810 check_rec(to_dereference_expr(expr).pointer(), guard);
1811 }
1812 else if(expr.id() == ID_index)
1813 {
1814 const index_exprt &index_expr = to_index_expr(expr);
1815 check_rec_address(index_expr.array(), guard);
1816 check_rec(index_expr.index(), guard);
1817 }
1818 else
1819 {
1820 for(const auto &operand : expr.operands())
1821 check_rec_address(operand, guard);
1822 }
1823}
1824
1826{
1828 expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies);
1829 INVARIANT(
1830 expr.is_boolean(),
1831 "'" + expr.id_string() + "' must be Boolean, but got " + expr.pretty());
1832
1833 exprt::operandst constraints;
1834
1835 for(const auto &op : expr.operands())
1836 {
1837 INVARIANT(
1838 op.is_boolean(),
1839 "'" + expr.id_string() + "' takes Boolean operands only, but got " +
1840 op.pretty());
1841
1842 auto new_guard = [&guard, &constraints](exprt expr) {
1843 return guard(implication(conjunction(constraints), expr));
1844 };
1845
1846 check_rec(op, new_guard);
1847
1848 constraints.push_back(expr.id() == ID_or ? boolean_negate(op) : op);
1849 }
1850}
1851
1853{
1854 INVARIANT(
1855 if_expr.cond().is_boolean(),
1856 "first argument of if must be boolean, but got " + if_expr.cond().pretty());
1857
1858 check_rec(if_expr.cond(), guard);
1859
1860 {
1861 auto new_guard = [&guard, &if_expr](exprt expr) {
1862 return guard(implication(if_expr.cond(), std::move(expr)));
1863 };
1864 check_rec(if_expr.true_case(), new_guard);
1865 }
1866
1867 {
1868 auto new_guard = [&guard, &if_expr](exprt expr) {
1869 return guard(implication(not_exprt(if_expr.cond()), std::move(expr)));
1870 };
1871 check_rec(if_expr.false_case(), new_guard);
1872 }
1873}
1874
1875bool goto_check_ct::check_rec_member(
1876 const member_exprt &member,
1877 const guardt &guard)
1878{
1879 const dereference_exprt &deref = to_dereference_expr(member.struct_op());
1880
1881 check_rec(deref.pointer(), guard);
1882
1883 // avoid building the following expressions when pointer_validity_check
1884 // would return immediately anyway
1886 return true;
1887
1888 // we rewrite s->member into *(s+member_offset)
1889 // to avoid requiring memory safety of the entire struct
1890 auto member_offset_opt = member_offset_expr(member, ns);
1891
1892 if(member_offset_opt.has_value())
1893 {
1894 pointer_typet new_pointer_type = to_pointer_type(deref.pointer().type());
1895 new_pointer_type.base_type() = member.type();
1896
1897 const exprt char_pointer = typecast_exprt::conditional_cast(
1898 deref.pointer(), pointer_type(char_type()));
1899
1900 const exprt new_address_casted = typecast_exprt::conditional_cast(
1901 plus_exprt{
1902 char_pointer,
1904 member_offset_opt.value(), pointer_diff_type())},
1905 new_pointer_type);
1906
1907 dereference_exprt new_deref{new_address_casted};
1908 new_deref.add_source_location() = deref.source_location();
1909 pointer_validity_check(new_deref, member, guard);
1910
1911 return true;
1912 }
1913 return false;
1914}
1915
1916void goto_check_ct::check_rec_div(
1917 const div_exprt &div_expr,
1918 const guardt &guard)
1919{
1920 if(
1921 div_expr.type().id() == ID_signedbv ||
1922 div_expr.type().id() == ID_unsignedbv || div_expr.type().id() == ID_c_bool)
1923 {
1924 // Division by zero is undefined behavior for all integer types.
1926 }
1927 else if(div_expr.type().id() == ID_floatbv)
1928 {
1929 // Division by zero on floating-point numbers may be undefined behavior.
1930 // Annex F of the ISO C21 suggests that implementations that
1931 // define __STDC_IEC_559__ follow IEEE 754 semantics,
1932 // which defines the outcome of division by zero.
1934 }
1935
1936 if(div_expr.type().id() == ID_signedbv)
1937 integer_overflow_check(div_expr, guard);
1938 else if(div_expr.type().id() == ID_floatbv)
1939 {
1940 nan_check(div_expr, guard);
1941 float_overflow_check(div_expr, guard);
1942 }
1943}
1944
1945void goto_check_ct::check_rec_arithmetic_op(
1946 const exprt &expr,
1947 const guardt &guard)
1948{
1949 if(expr.type().id() == ID_signedbv || expr.type().id() == ID_unsignedbv)
1950 {
1952
1953 if(
1954 expr.operands().size() == 2 && expr.id() == ID_minus &&
1955 expr.operands()[0].type().id() == ID_pointer &&
1956 expr.operands()[1].type().id() == ID_pointer)
1957 {
1959 }
1960 }
1961 else if(expr.type().id() == ID_floatbv)
1962 {
1963 nan_check(expr, guard);
1965 }
1966 else if(expr.type().id() == ID_pointer)
1967 {
1969 }
1970}
1971
1972void goto_check_ct::check_rec(const exprt &expr, const guardt &guard)
1973{
1974 if(expr.id() == ID_exists || expr.id() == ID_forall)
1975 {
1976 // the scoped variables may be used in the assertion
1977 const auto &quantifier_expr = to_quantifier_expr(expr);
1978
1979 auto new_guard = [&guard, &quantifier_expr](exprt expr) {
1980 return guard(forall_exprt(quantifier_expr.symbol(), expr));
1981 };
1982
1983 check_rec(quantifier_expr.where(), new_guard);
1984 return;
1985 }
1986 else if(expr.id() == ID_address_of)
1987 {
1989 return;
1990 }
1991 else if(expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies)
1992 {
1994 return;
1995 }
1996 else if(expr.id() == ID_if)
1997 {
1999 return;
2000 }
2001 else if(
2002 expr.id() == ID_member &&
2003 to_member_expr(expr).struct_op().id() == ID_dereference)
2004 {
2005 if(check_rec_member(to_member_expr(expr), guard))
2006 return;
2007 }
2008
2009 for(const auto &op : expr.operands())
2010 check_rec(op, guard);
2011
2012 if(expr.type().id() == ID_c_enum_tag)
2013 enum_range_check(expr, guard);
2014
2015 if(expr.id() == ID_index)
2016 {
2017 bounds_check(expr, guard);
2018 }
2019 else if(expr.id() == ID_div)
2020 {
2021 check_rec_div(to_div_expr(expr), guard);
2022 }
2023 else if(expr.id() == ID_shl || expr.id() == ID_ashr || expr.id() == ID_lshr)
2024 {
2026
2027 if(expr.id() == ID_shl && expr.type().id() == ID_signedbv)
2029 }
2030 else if(expr.id() == ID_mod)
2031 {
2034 }
2035 else if(
2036 expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
2037 expr.id() == ID_unary_minus)
2038 {
2039 check_rec_arithmetic_op(expr, guard);
2040 }
2041 else if(expr.id() == ID_typecast)
2042 conversion_check(expr, guard);
2043 else if(
2044 expr.id() == ID_le || expr.id() == ID_lt || expr.id() == ID_ge ||
2045 expr.id() == ID_gt)
2047 else if(expr.id() == ID_dereference)
2048 {
2050 }
2052 {
2054 }
2055 else if(
2056 expr.id() == ID_count_leading_zeros || expr.id() == ID_count_trailing_zeros)
2057 {
2058 bounds_check(expr, guard);
2059 }
2060}
2061
2063{
2064 check_rec(expr, identity);
2065}
2066
2068{
2069 const symbolt &leak = ns.lookup(CPROVER_PREFIX "memory_leak");
2070 const symbol_exprt leak_expr = leak.symbol_expr();
2071
2072 // add self-assignment to get helpful counterexample output
2073 new_code.add(goto_programt::make_assignment(leak_expr, leak_expr));
2074
2075 source_locationt source_location;
2076 source_location.set_function(function_id);
2077
2078 equal_exprt eq(leak_expr, null_pointer_exprt(to_pointer_type(leak.type)));
2079
2081 eq,
2082 "dynamically allocated memory never freed",
2083 "memory-leak",
2084 false, // fatal
2085 source_location,
2086 eq,
2087 identity);
2088}
2089
2091 const irep_idt &function_identifier,
2092 goto_functiont &goto_function)
2093{
2094 const auto &function_symbol = ns.lookup(function_identifier);
2095 mode = function_symbol.mode;
2096
2097 if(mode != ID_C && mode != ID_cpp)
2098 return;
2099
2100 assertions.clear();
2101
2102 bool did_something = false;
2103
2105 std::make_unique<local_bitvector_analysist>(goto_function, ns);
2106
2107 goto_programt &goto_program = goto_function.body;
2108
2109 Forall_goto_program_instructions(it, goto_program)
2110 {
2111 current_target = it;
2113
2114 flag_overridet resetter(i.source_location());
2115 const auto &pragmas = i.source_location().get_pragmas();
2116 for(const auto &d : pragmas)
2117 {
2118 // match named-check related pragmas
2119 auto matched = match_named_check(d.first);
2120 if(matched.has_value())
2121 {
2122 auto named_check = matched.value();
2123 auto name = named_check.first;
2124 auto status = named_check.second;
2125 bool *flag = name_to_flag.find(name)->second;
2126 switch(status)
2127 {
2129 resetter.set_flag(*flag, true, name);
2130 break;
2132 resetter.set_flag(*flag, false, name);
2133 break;
2135 resetter.disable_flag(*flag, name);
2136 break;
2137 }
2138 }
2139 }
2140
2141 // add checked pragmas for all active checks
2143
2144 new_code.clear();
2145
2146 // we clear all recorded assertions if
2147 // 1) we want to generate all assertions or
2148 // 2) the instruction is a branch target
2149 if(retain_trivial || i.is_target())
2150 assertions.clear();
2151
2152 if(i.has_condition())
2153 {
2154 check(i.condition());
2155 }
2156
2157 // magic ERROR label?
2158 for(const auto &label : error_labels)
2159 {
2160 if(std::find(i.labels.begin(), i.labels.end(), label) != i.labels.end())
2161 {
2162 source_locationt annotated_location = i.source_location();
2163 annotated_location.set_property_class("error label");
2164 annotated_location.set_comment("error label " + label);
2165 annotated_location.set("user-provided", true);
2166
2168 {
2169 new_code.add(
2170 goto_programt::make_assumption(false_exprt{}, annotated_location));
2171 }
2172 else
2173 {
2174 new_code.add(
2175 goto_programt::make_assertion(false_exprt{}, annotated_location));
2176 }
2177 }
2178 }
2179
2180 if(i.is_other())
2181 {
2182 const auto &code = i.get_other();
2183 const irep_idt &statement = code.get_statement();
2184
2185 if(statement == ID_expression)
2186 {
2187 check(code);
2188 }
2189 else if(statement == ID_printf)
2190 {
2191 for(const auto &op : code.operands())
2192 check(op);
2193 }
2194 }
2195 else if(i.is_assign())
2196 {
2197 const exprt &assign_lhs = i.assign_lhs();
2198 const exprt &assign_rhs = i.assign_rhs();
2199
2200 // Disable enum range checks for left-hand sides as their values are yet
2201 // to be set (by this assignment).
2202 {
2203 flag_overridet resetter(i.source_location());
2204 resetter.disable_flag(enable_enum_range_check, "enum_range_check");
2205 check(assign_lhs);
2206 }
2207
2208 check(assign_rhs);
2209
2210 // the LHS might invalidate any assertion
2211 invalidate(assign_lhs);
2212 }
2213 else if(i.is_function_call())
2214 {
2215 // Disable enum range checks for left-hand sides as their values are yet
2216 // to be set (by this function call).
2217 {
2218 flag_overridet resetter(i.source_location());
2219 resetter.disable_flag(enable_enum_range_check, "enum_range_check");
2220 check(i.call_lhs());
2221 }
2222 check(i.call_function());
2223
2224 for(const auto &arg : i.call_arguments())
2225 check(arg);
2226
2228
2229 // the call might invalidate any assertion
2230 assertions.clear();
2231 }
2232 else if(i.is_set_return_value())
2233 {
2234 check(i.return_value());
2235 // the return value invalidate any assertion
2237 }
2238 else if(i.is_throw())
2239 {
2240 // this has no successor
2241 assertions.clear();
2242 }
2243 else if(i.is_assume())
2244 {
2245 // These are further 'exit points' of the program
2246 const exprt simplified_guard = simplify_expr(i.condition(), ns);
2247 if(
2248 enable_memory_cleanup_check && simplified_guard.is_false() &&
2249 (function_identifier == "abort" || function_identifier == "exit" ||
2250 function_identifier == "_Exit" ||
2251 (i.labels.size() == 1 && i.labels.front() == "__VERIFIER_abort")))
2252 {
2253 memory_leak_check(function_identifier);
2254 }
2255 }
2256 else if(i.is_dead())
2257 {
2259 {
2260 const symbol_exprt &variable = i.dead_symbol();
2261
2262 // is it dirty?
2263 if(local_bitvector_analysis->dirty(variable))
2264 {
2265 // need to mark the dead variable as dead
2266 exprt lhs = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
2267 exprt address_of_expr = typecast_exprt::conditional_cast(
2268 address_of_exprt(variable), lhs.type());
2269 if_exprt rhs(
2271 std::move(address_of_expr),
2272 lhs);
2274 code_assignt{std::move(lhs), std::move(rhs), i.source_location()},
2275 i.source_location()));
2276 }
2277 }
2278 }
2279 else if(i.is_end_function())
2280 {
2281 if(
2282 function_identifier == goto_functionst::entry_point() &&
2284 {
2285 memory_leak_check(function_identifier);
2286 }
2287 }
2288
2289 for(auto &instruction : new_code.instructions)
2290 {
2291 if(instruction.source_location().is_nil())
2292 {
2293 instruction.source_location_nonconst().id(irep_idt());
2294
2295 if(!it->source_location().get_file().empty())
2296 instruction.source_location_nonconst().set_file(
2297 it->source_location().get_file());
2298
2299 if(!it->source_location().get_line().empty())
2300 instruction.source_location_nonconst().set_line(
2301 it->source_location().get_line());
2302
2303 if(!it->source_location().get_function().empty())
2304 instruction.source_location_nonconst().set_function(
2305 it->source_location().get_function());
2306
2307 if(!it->source_location().get_column().empty())
2308 {
2309 instruction.source_location_nonconst().set_column(
2310 it->source_location().get_column());
2311 }
2312 }
2313 }
2314
2315 // insert new instructions -- make sure targets are not moved
2316 did_something |= !new_code.instructions.empty();
2317
2318 while(!new_code.instructions.empty())
2319 {
2320 goto_program.insert_before_swap(it, new_code.instructions.front());
2321 new_code.instructions.pop_front();
2322 it++;
2323 }
2324 }
2325
2326 if(did_something)
2327 remove_skip(goto_program);
2328}
2329
2332{
2333 if(i.call_function().id() != ID_symbol)
2334 return;
2335
2336 const irep_idt &identifier =
2338
2339 if(
2340 identifier == CPROVER_PREFIX "get_field" || identifier == CPROVER_PREFIX
2341 "set_field")
2342 {
2343 const exprt &expr = i.call_arguments()[0];
2344 PRECONDITION(expr.type().id() == ID_pointer);
2345 check(dereference_exprt(expr));
2346 }
2347}
2348
2351 const exprt &address,
2352 const exprt &size)
2353{
2355 PRECONDITION(address.type().id() == ID_pointer);
2358
2359 conditionst conditions;
2360
2361 const exprt in_bounds_of_some_explicit_allocation =
2363
2364 const bool unknown = flags.is_unknown() || flags.is_uninitialized();
2365
2366 if(unknown)
2367 {
2368 conditions.push_back(conditiont{
2369 not_exprt{is_invalid_pointer_exprt{address}}, "pointer invalid"});
2370 }
2371
2372 if(unknown || flags.is_dynamic_heap())
2373 {
2374 conditions.push_back(conditiont(
2375 or_exprt(
2376 in_bounds_of_some_explicit_allocation,
2377 not_exprt(deallocated(address, ns))),
2378 "deallocated dynamic object"));
2379 }
2380
2381 if(unknown || flags.is_dynamic_local())
2382 {
2383 conditions.push_back(conditiont(
2384 or_exprt(
2385 in_bounds_of_some_explicit_allocation,
2386 not_exprt(dead_object(address, ns))),
2387 "dead object"));
2388 }
2389
2390 if(flags.is_dynamic_heap())
2391 {
2392 const or_exprt object_bounds_violation(
2393 object_lower_bound(address, nil_exprt()),
2394 object_upper_bound(address, size));
2395
2396 conditions.push_back(conditiont(
2397 or_exprt(
2398 in_bounds_of_some_explicit_allocation,
2399 not_exprt(object_bounds_violation)),
2400 "pointer outside dynamic object bounds"));
2401 }
2402
2403 if(unknown || flags.is_dynamic_local() || flags.is_static_lifetime())
2404 {
2405 const or_exprt object_bounds_violation(
2406 object_lower_bound(address, nil_exprt()),
2407 object_upper_bound(address, size));
2408
2409 conditions.push_back(conditiont(
2410 or_exprt(
2411 in_bounds_of_some_explicit_allocation,
2412 not_exprt(object_bounds_violation)),
2413 "pointer outside object bounds"));
2414 }
2415
2416 if(unknown || flags.is_integer_address())
2417 {
2418 conditions.push_back(conditiont(
2420 integer_address(address), in_bounds_of_some_explicit_allocation),
2421 "invalid integer address"));
2422 }
2423
2424 return conditions;
2425}
2426
2427std::optional<goto_check_ct::conditiont>
2429 const exprt &address,
2430 const exprt &size)
2431{
2433 PRECONDITION(address.type().id() == ID_pointer);
2436
2437 if(flags.is_unknown() || flags.is_uninitialized() || flags.is_null())
2438 {
2439 return {conditiont{
2440 or_exprt{
2442 not_exprt(null_object(address))},
2443 "pointer NULL"}};
2444 }
2445
2446 return {};
2447}
2448
2450 const exprt &pointer,
2451 const exprt &size)
2452{
2453 exprt::operandst alloc_disjuncts;
2454 for(const auto &a : allocations)
2455 {
2456 typecast_exprt int_ptr(pointer, a.first.type());
2457
2458 binary_relation_exprt lb_check(a.first, ID_le, int_ptr);
2459
2460 plus_exprt upper_bound{
2461 int_ptr, typecast_exprt::conditional_cast(size, int_ptr.type())};
2462
2463 binary_relation_exprt ub_check{
2464 std::move(upper_bound), ID_le, plus_exprt{a.first, a.second}};
2465
2466 alloc_disjuncts.push_back(
2467 and_exprt{std::move(lb_check), std::move(ub_check)});
2468 }
2469 return disjunction(alloc_disjuncts);
2470}
2471
2473 const irep_idt &function_identifier,
2474 goto_functionst::goto_functiont &goto_function,
2475 const namespacet &ns,
2476 const optionst &options,
2477 message_handlert &message_handler)
2478{
2479 goto_check_ct goto_check(ns, options, message_handler);
2480 goto_check.goto_check(function_identifier, goto_function);
2481}
2482
2484 const namespacet &ns,
2485 const optionst &options,
2486 goto_functionst &goto_functions,
2487 message_handlert &message_handler)
2488{
2489 goto_check_ct goto_check(ns, options, message_handler);
2490
2491 goto_check.collect_allocations(goto_functions);
2492
2493 for(auto &gf_entry : goto_functions.function_map)
2494 {
2495 goto_check.goto_check(gf_entry.first, gf_entry.second);
2496 }
2497}
2498
2500 const optionst &options,
2501 goto_modelt &goto_model,
2502 message_handlert &message_handler)
2503{
2504 const namespacet ns(goto_model.symbol_table);
2505 goto_check_c(ns, options, goto_model.goto_functions, message_handler);
2506}
2507
2509 source_locationt &source_location) const
2510{
2511 for(const auto &entry : name_to_flag)
2512 if(*(entry.second))
2513 source_location.add_pragma("checked:" + id2string(entry.first));
2514}
2515
2517 source_locationt &source_location) const
2518{
2519 for(const auto &entry : name_to_flag)
2520 source_location.add_pragma("checked:" + id2string(entry.first));
2521}
2522
2525{
2526 auto s = id2string(named_check);
2527 auto col = s.find(":");
2528
2529 if(col == std::string::npos)
2530 return {}; // separator not found
2531
2532 auto name = s.substr(col + 1);
2533
2534 if(name_to_flag.find(name) == name_to_flag.end())
2535 return {}; // name unknown
2536
2537 check_statust status;
2538 if(!s.compare(0, 6, "enable"))
2539 status = check_statust::ENABLE;
2540 else if(!s.compare(0, 7, "disable"))
2541 status = check_statust::DISABLE;
2542 else if(!s.compare(0, 7, "checked"))
2543 status = check_statust::CHECKED;
2544 else
2545 return {}; // prefix unknow
2546
2547 // success
2548 return std::pair<irep_idt, check_statust>{name, status};
2549}
configt config
Definition config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
std::optional< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
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 count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_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.
API to expression classes that are internal to the C frontend.
static exprt guard(const exprt::operandst &guards, exprt cond)
unsignedbv_typet size_type()
Definition c_types.cpp:50
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
signedbv_typet pointer_diff_type()
Definition c_types.cpp:220
bitvector_typet char_type()
Definition c_types.cpp:106
Operator to return the address of an object.
Boolean AND.
Definition std_expr.h:2120
const exprt & size() const
Definition std_types.h:840
A base class for binary expressions.
Definition std_expr.h:638
exprt & lhs()
Definition std_expr.h:668
exprt & rhs()
Definition std_expr.h:678
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
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:731
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
std::size_t get_width() const
Definition std_types.h:920
The Boolean type.
Definition std_types.h:36
A goto_instruction_codet representing an assignment in the program.
struct configt::cppt cpp
struct configt::ansi_ct ansi_c
Operator to dereference a pointer.
Division.
Definition std_expr.h:1152
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
A Boolean expression returning true, iff the value of an enum-typed symbol equals one of the enum's d...
Definition c_expr.h:327
exprt lower(const namespacet &ns) const
Definition c_expr.cpp:71
Equality.
Definition std_expr.h:1361
Base class for all expressions.
Definition expr.h:56
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:147
std::vector< exprt > operandst
Definition expr.h:58
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:27
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:224
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition expr.cpp:47
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:231
source_locationt & add_source_location()
Definition expr.h:236
Extracts a sub-range of a bit-vector operand.
The Boolean constant false.
Definition std_expr.h:3064
~flag_overridet()
Restore the values of all flags that have been modified via set_flag.
void disable_flag(bool &flag, const irep_idt &flag_name)
Sets the given flag to false, overriding any previous value.
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.
std::map< bool *, bool > flags_to_reset
flag_overridet(const source_locationt &source_location)
std::set< bool * > disabled_flags
const source_locationt & source_location
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_logical_op(const exprt &expr, const guardt &guard)
Check a logical operation: check each operand in separation while extending the guarding condition as...
bool enable_float_div_by_zero_check
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 &)
goto_functionst::goto_functiont goto_functiont
void collect_allocations(const goto_functionst &goto_functions)
Fill the list of allocations allocationst with <address, size> for every allocation instruction.
void memory_leak_check(const irep_idt &function_id)
exprt is_in_bounds_of_some_explicit_allocation(const exprt &pointer, const exprt &size)
std::optional< goto_check_ct::conditiont > get_pointer_is_null_condition(const exprt &address, const exprt &size)
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.
void float_div_by_zero_check(const div_exprt &, const guardt &)
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
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)
Check that a member expression is valid:
conditionst get_pointer_dereferenceable_conditions(const exprt &address, const exprt &size)
std::pair< exprt, exprt > allocationt
std::set< std::pair< exprt, exprt > > assertionst
void bounds_check(const exprt &, const guardt &)
std::optional< std::pair< irep_idt, check_statust > > named_check_statust
optional (named-check, status) pair
allocationst allocations
void pointer_overflow_check(const exprt &, const guardt &)
bool enable_memory_leak_check
void add_guarded_property(const exprt &asserted_expr, const std::string &comment, const std::string &property_class, bool is_fatal, const source_locationt &source_location, const exprt &src_expr, const guardt &guard)
Include the asserted_expr in the code conditioned by the guard.
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...
void integer_overflow_check(const exprt &, const guardt &)
bool enable_assert_to_assume
bool enable_memory_cleanup_check
void nan_check(const exprt &, const guardt &)
bool enable_undefined_shift_check
bool enable_enum_range_check
goto_programt::const_targett current_target
void add_all_checked_named_check_pragmas(source_locationt &source_location) const
Adds "checked" pragmas for all named checks on the given source location (prevents any the instanciat...
std::list< allocationt > allocationst
const guardt identity
void div_by_zero_check(const div_exprt &, const guardt &)
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)
bool enable_unsigned_overflow_check
void bounds_check_bit_count(const unary_exprt &, const guardt &)
bool enable_div_by_zero_check
void check_shadow_memory_api_calls(const goto_programt::instructiont &)
error_labelst error_labels
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 &)
optionst::value_listt error_labelst
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...
goto_programt body
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
This class represents an instruction in the GOTO intermediate representation.
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
const goto_instruction_codet & get_other() const
Get the statement for OTHER.
bool is_target() const
Is this node a branch target?
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
bool has_condition() const
Does this instruction have a condition?
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
const exprt & condition() const
Get the condition of gotos, assume, assert.
source_locationt & source_location_nonconst()
const source_locationt & source_location() const
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst instructions
The list of instructions in the goto program.
void clear()
Clear the goto program.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
instructionst::const_iterator const_targett
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
IEEE-floating-point equality.
constant_exprt to_expr() const
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
Definition ieee_float.h:211
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
Definition ieee_float.h:214
void from_integer(const mp_integer &i)
The trinary if-then-else operator.
Definition std_expr.h:2370
exprt & cond()
Definition std_expr.h:2387
exprt & false_case()
Definition std_expr.h:2407
exprt & true_case()
Definition std_expr.h:2397
Boolean implication.
Definition std_expr.h:2183
Array index operator.
Definition std_expr.h:1465
exprt & index()
Definition std_expr.h:1505
exprt & array()
Definition std_expr.h:1495
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
const std::string & id_string() const
Definition irep.h:391
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
Evaluates to true if the operand is infinite.
virtual bool from_expr(const exprt &expr, std::string &code, const namespacet &ns)
Formats the given expression in a language-specific way.
Definition language.cpp:32
flagst get(const goto_programt::const_targett t, const exprt &src)
Extract member of struct or union.
Definition std_expr.h:2841
const exprt & struct_op() const
Definition std_expr.h:2879
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1223
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition std_expr.h:1243
Binary multiplication Associativity is not specified.
Definition std_expr.h:1107
A base class for multi-ary expressions Associativity is not specified.
Definition std_expr.h:912
exprt & op0()
Definition std_expr.h:932
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The NIL expression.
Definition std_expr.h:3073
Boolean negation.
Definition std_expr.h:2327
Disequality.
Definition std_expr.h:1420
The null pointer constant.
Split an expression into a base object and a (byte) offset.
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)
std::list< std::string > value_listt
Definition options.h:25
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
Boolean OR.
Definition std_expr.h:2228
The plus expression Associativity is not specified.
Definition std_expr.h:1002
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
const exprt & pointer() const
const exprt & pointer() const
A base class for shift and rotate operators.
exprt & distance()
Left shift.
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
void set_comment(const irep_idt &comment)
bool property_fatal() const
void set_property_class(const irep_idt &property_class)
void add_pragma(const irep_idt &pragma)
const irept::named_subt & get_pragmas() const
static bool is_built_in(const std::string &s)
std::string as_string() const
void set_function(const irep_idt &function)
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
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
Semantic type conversion.
Definition std_expr.h:2068
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2076
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:361
const exprt & op() const
Definition std_expr.h:391
A Boolean expression returning true, iff negation would result in an overflow when applied to the (si...
Fixed-width bit-vector with unsigned binary interpretation.
const constant_exprt & size() const
#define CPROVER_PREFIX
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition expr_util.cpp:38
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
bool has_symbol_expr(const exprt &src, const irep_idt &identifier, bool include_bound_symbols)
Returns true if one of the symbol expressions in src has identifier identifier; if include_bound_symb...
API to expression classes for floating-point arithmetic.
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)
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
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
Options.
API to expression classes for Pointers.
const r_or_w_ok_exprt & to_r_or_w_ok_expr(const exprt &expr)
bool can_cast_expr< object_size_exprt >(const exprt &base)
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const prophecy_r_or_w_ok_exprt & to_prophecy_r_or_w_ok_expr(const exprt &expr)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
bool can_cast_expr< prophecy_r_or_w_ok_exprt >(const exprt &base)
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
std::optional< 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 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)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Program Transformation.
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
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:66
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:54
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:895
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1533
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition std_expr.h:1272
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition std_expr.h:1132
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2102
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition std_expr.h:1201
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:1041
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:426
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:987
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2450
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2933
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition std_expr.h:1086
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition std_expr.h:2208
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition std_expr.h:514
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1104
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
enum configt::ansi_ct::c_standardt c_standard
enum configt::cppt::cpp_standardt cpp_standard
conditiont(const exprt &_assertion, const std::string &_description)
dstringt irep_idt