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>
25#include <util/make_unique.h>
27#include <util/message.h>
28#include <util/options.h>
29#include <util/pointer_expr.h>
32#include <util/prefix.h>
33#include <util/simplify_expr.h>
34#include <util/std_code.h>
35#include <util/std_expr.h>
36
39
41#include <langapi/language.h>
42#include <langapi/mode.h>
43
44#include "c_expr.h"
45
46#include <algorithm>
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 enable_bounds_check = _options.get_bool_option("bounds-check");
58 enable_pointer_check = _options.get_bool_option("pointer-check");
59 enable_memory_leak_check = _options.get_bool_option("memory-leak-check");
61 _options.get_bool_option("memory-cleanup-check");
62 enable_div_by_zero_check = _options.get_bool_option("div-by-zero-check");
63 enable_enum_range_check = _options.get_bool_option("enum-range-check");
65 _options.get_bool_option("signed-overflow-check");
67 _options.get_bool_option("unsigned-overflow-check");
69 _options.get_bool_option("pointer-overflow-check");
70 enable_conversion_check = _options.get_bool_option("conversion-check");
72 _options.get_bool_option("undefined-shift-check");
74 _options.get_bool_option("float-overflow-check");
75 enable_simplify = _options.get_bool_option("simplify");
76 enable_nan_check = _options.get_bool_option("nan-check");
77 retain_trivial = _options.get_bool_option("retain-trivial-checks");
78 enable_assert_to_assume = _options.get_bool_option("assert-to-assume");
79 error_labels = _options.get_list_option("error-label");
81 _options.get_bool_option("pointer-primitive-check");
82 }
83
85
86 void goto_check(
87 const irep_idt &function_identifier,
88 goto_functiont &goto_function);
89
95 void collect_allocations(const goto_functionst &goto_functions);
96
97protected:
98 const namespacet &ns;
99 std::unique_ptr<local_bitvector_analysist> local_bitvector_analysis;
102
103 using guardt = std::function<exprt(exprt)>;
104 const guardt identity = [](exprt expr) { return expr; };
105
107
113 void check_rec_address(const exprt &expr, const guardt &guard);
114
122 void check_rec_logical_op(const exprt &expr, const guardt &guard);
123
130 void check_rec_if(const if_exprt &if_expr, const guardt &guard);
131
142 bool check_rec_member(const member_exprt &member, const guardt &guard);
143
148 void check_rec_div(const div_exprt &div_expr, const guardt &guard);
149
154 void check_rec_arithmetic_op(const exprt &expr, const guardt &guard);
155
161 void check_rec(const exprt &expr, const guardt &guard);
162
165 void check(const exprt &expr);
166
168 {
169 conditiont(const exprt &_assertion, const std::string &_description)
170 : assertion(_assertion), description(_description)
171 {
172 }
173
175 std::string description;
176 };
177
178 using conditionst = std::list<conditiont>;
179
180 void bounds_check(const exprt &, const guardt &);
181 void bounds_check_index(const index_exprt &, const guardt &);
182 void bounds_check_bit_count(const unary_exprt &, const guardt &);
183 void 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
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
245 const exprt &asserted_expr,
246 const std::string &comment,
247 const std::string &property_class,
248 const source_locationt &source_location,
249 const exprt &src_expr,
250 const guardt &guard);
251
253 typedef std::set<std::pair<exprt, exprt>> assertionst;
255
260 void invalidate(const exprt &lhs);
261
279
281 std::map<irep_idt, bool *> name_to_flag{
282 {"bounds-check", &enable_bounds_check},
283 {"pointer-check", &enable_pointer_check},
284 {"memory-leak-check", &enable_memory_leak_check},
285 {"memory-cleanup-check", &enable_memory_cleanup_check},
286 {"div-by-zero-check", &enable_div_by_zero_check},
287 {"enum-range-check", &enable_enum_range_check},
288 {"signed-overflow-check", &enable_signed_overflow_check},
289 {"unsigned-overflow-check", &enable_unsigned_overflow_check},
290 {"pointer-overflow-check", &enable_pointer_overflow_check},
291 {"conversion-check", &enable_conversion_check},
292 {"undefined-shift-check", &enable_undefined_shift_check},
293 {"float-overflow-check", &enable_float_overflow_check},
294 {"nan-check", &enable_nan_check},
295 {"pointer-primitive-check", &enable_pointer_primitive_check}};
296
299
300 // the first element of the pair is the base address,
301 // and the second is the size of the region
302 typedef std::pair<exprt, exprt> allocationt;
303 typedef std::list<allocationt> allocationst;
305
307
310 void add_active_named_check_pragmas(source_locationt &source_location) const;
311
314 void
316
318 typedef enum
319 {
322 CHECKED
324
327
336 named_check_statust match_named_check(const irep_idt &named_check) const;
337};
338
347{
348public:
353
359 void set_flag(bool &flag, bool new_value, const irep_idt &flag_name)
360 {
361 // make this a no-op if the flag is disabled
362 if(disabled_flags.find(&flag) != disabled_flags.end())
363 return;
364
365 // detect double sets
366 INVARIANT(
367 flags_to_reset.find(&flag) == flags_to_reset.end(),
368 "Flag " + id2string(flag_name) + " set twice at \n" +
370 if(flag != new_value)
371 {
372 flags_to_reset[&flag] = flag;
373 flag = new_value;
374 }
375 }
376
381 void disable_flag(bool &flag, const irep_idt &flag_name)
382 {
383 INVARIANT(
384 disabled_flags.find(&flag) == disabled_flags.end(),
385 "Flag " + id2string(flag_name) + " disabled twice at \n" +
387
388 disabled_flags.insert(&flag);
389
390 // If the flag has not already been set,
391 // we store its current value in the reset map.
392 // Otherwise, the reset map already holds
393 // the initial value we want to reset it to, keep it as is.
394 if(flags_to_reset.find(&flag) == flags_to_reset.end())
395 flags_to_reset[&flag] = flag;
396
397 // set the flag to false in all cases.
398 flag = false;
399 }
400
404 {
405 for(const auto &flag_pair : flags_to_reset)
406 *flag_pair.first = flag_pair.second;
407 }
408
409private:
411 std::map<bool *, bool> flags_to_reset;
412 std::set<bool *> disabled_flags;
413};
414
415static exprt implication(exprt lhs, exprt rhs)
416{
417 // rewrite a => (b => c) to (a && b) => c
418 if(rhs.id() == ID_implies)
419 {
420 const auto &rhs_implication = to_implies_expr(rhs);
421 return implies_exprt(
422 and_exprt(std::move(lhs), rhs_implication.lhs()), rhs_implication.rhs());
423 }
424 else
425 {
426 return implies_exprt(std::move(lhs), std::move(rhs));
427 }
428}
429
431{
432 for(const auto &gf_entry : goto_functions.function_map)
433 {
434 for(const auto &instruction : gf_entry.second.body.instructions)
435 {
436 if(!instruction.is_function_call())
437 continue;
438
439 const auto &function = instruction.call_function();
440 if(
441 function.id() != ID_symbol ||
443 "allocated_memory")
444 continue;
445
447 instruction.call_arguments();
448 if(
449 args.size() != 2 || args[0].type().id() != ID_unsignedbv ||
450 args[1].type().id() != ID_unsignedbv)
451 throw "expected two unsigned arguments to " CPROVER_PREFIX
452 "allocated_memory";
453
455 args[0].type() == args[1].type(),
456 "arguments of allocated_memory must have same type");
457 allocations.push_back({args[0], args[1]});
458 }
459 }
460}
461
463{
464 if(lhs.id() == ID_index)
465 invalidate(to_index_expr(lhs).array());
466 else if(lhs.id() == ID_member)
467 invalidate(to_member_expr(lhs).struct_op());
468 else if(lhs.id() == ID_symbol)
469 {
470 // clear all assertions about 'symbol'
471 const irep_idt &lhs_id = to_symbol_expr(lhs).get_identifier();
472
473 for(auto it = assertions.begin(); it != assertions.end();)
474 {
475 if(
476 has_symbol_expr(it->second, lhs_id, false) ||
477 has_subexpr(it->second, ID_dereference))
478 {
479 it = assertions.erase(it);
480 }
481 else
482 ++it;
483 }
484 }
485 else
486 {
487 // give up, clear all
488 assertions.clear();
489 }
490}
491
493 const div_exprt &expr,
494 const guardt &guard)
495{
497 return;
498
499 // add divison by zero subgoal
500
501 exprt zero = from_integer(0, expr.op1().type());
502 const notequal_exprt inequality(expr.op1(), std::move(zero));
503
505 inequality,
506 "division by zero",
507 "division-by-zero",
509 expr,
510 guard);
511}
512
514{
516 return;
517
518 // we might be looking at a lowered enum_is_in_range_exprt, skip over these
519 const auto &pragmas = expr.source_location().get_pragmas();
520 for(const auto &d : pragmas)
521 {
522 if(d.first == "disable:enum-range-check")
523 return;
524 }
525
526 const exprt check = enum_is_in_range_exprt{expr}.lower(ns);
527
529 check,
530 "enum range check",
531 "enum-range-check",
533 expr,
534 guard);
535}
536
538 const shift_exprt &expr,
539 const guardt &guard)
540{
542 return;
543
544 // Undefined for all types and shifts if distance exceeds width,
545 // and also undefined for negative distances.
546
547 const typet &distance_type = expr.distance().type();
548
549 if(distance_type.id() == ID_signedbv)
550 {
551 binary_relation_exprt inequality(
552 expr.distance(), ID_ge, from_integer(0, distance_type));
553
555 inequality,
556 "shift distance is negative",
557 "undefined-shift",
559 expr,
560 guard);
561 }
562
563 const typet &op_type = expr.op().type();
564
565 if(op_type.id() == ID_unsignedbv || op_type.id() == ID_signedbv)
566 {
567 exprt width_expr =
568 from_integer(to_bitvector_type(op_type).get_width(), distance_type);
569
571 binary_relation_exprt(expr.distance(), ID_lt, std::move(width_expr)),
572 "shift distance too large",
573 "undefined-shift",
575 expr,
576 guard);
577
578 if(op_type.id() == ID_signedbv && expr.id() == ID_shl)
579 {
580 binary_relation_exprt inequality(
581 expr.op(), ID_ge, from_integer(0, op_type));
582
584 inequality,
585 "shift operand is negative",
586 "undefined-shift",
588 expr,
589 guard);
590 }
591 }
592 else
593 {
595 false_exprt(),
596 "shift of non-integer type",
597 "undefined-shift",
599 expr,
600 guard);
601 }
602}
603
605 const mod_exprt &expr,
606 const guardt &guard)
607{
609 return;
610
611 // add divison by zero subgoal
612
613 exprt zero = from_integer(0, expr.divisor().type());
614 const notequal_exprt inequality(expr.divisor(), std::move(zero));
615
617 inequality,
618 "division by zero",
619 "division-by-zero",
621 expr,
622 guard);
623}
624
627 const mod_exprt &expr,
628 const guardt &guard)
629{
631 return;
632
633 const auto &type = expr.type();
634
635 if(type.id() == ID_signedbv)
636 {
637 // INT_MIN % -1 is, in principle, defined to be zero in
638 // ANSI C, C99, C++98, and C++11. Most compilers, however,
639 // fail to produce 0, and in some cases generate an exception.
640 // C11 explicitly makes this case undefined.
641
642 notequal_exprt int_min_neq(
643 expr.op0(), to_signedbv_type(type).smallest_expr());
644
645 notequal_exprt minus_one_neq(
646 expr.op1(), from_integer(-1, expr.op1().type()));
647
649 or_exprt(int_min_neq, minus_one_neq),
650 "result of signed mod is not representable",
651 "overflow",
653 expr,
654 guard);
655 }
656}
657
659{
661 return;
662
663 // First, check type.
664 const typet &type = expr.type();
665
666 if(type.id() != ID_signedbv && type.id() != ID_unsignedbv)
667 return;
668
669 if(expr.id() == ID_typecast)
670 {
671 const auto &op = to_typecast_expr(expr).op();
672
673 // conversion to signed int may overflow
674 const typet &old_type = op.type();
675
676 if(type.id() == ID_signedbv)
677 {
678 std::size_t new_width = to_signedbv_type(type).get_width();
679
680 if(old_type.id() == ID_signedbv) // signed -> signed
681 {
682 std::size_t old_width = to_signedbv_type(old_type).get_width();
683 if(new_width >= old_width)
684 return; // always ok
685
686 const binary_relation_exprt no_overflow_upper(
687 op, ID_le, from_integer(power(2, new_width - 1) - 1, old_type));
688
689 const binary_relation_exprt no_overflow_lower(
690 op, ID_ge, from_integer(-power(2, new_width - 1), old_type));
691
693 and_exprt(no_overflow_lower, no_overflow_upper),
694 "arithmetic overflow on signed type conversion",
695 "overflow",
697 expr,
698 guard);
699 }
700 else if(old_type.id() == ID_unsignedbv) // unsigned -> signed
701 {
702 std::size_t old_width = to_unsignedbv_type(old_type).get_width();
703 if(new_width >= old_width + 1)
704 return; // always ok
705
706 const binary_relation_exprt no_overflow_upper(
707 op, ID_le, from_integer(power(2, new_width - 1) - 1, old_type));
708
710 no_overflow_upper,
711 "arithmetic overflow on unsigned to signed type conversion",
712 "overflow",
714 expr,
715 guard);
716 }
717 else if(old_type.id() == ID_floatbv) // float -> signed
718 {
719 // Note that the fractional part is truncated!
720 ieee_floatt upper(to_floatbv_type(old_type));
721 upper.from_integer(power(2, new_width - 1));
722 const binary_relation_exprt no_overflow_upper(
723 op, ID_lt, upper.to_expr());
724
725 ieee_floatt lower(to_floatbv_type(old_type));
726 lower.from_integer(-power(2, new_width - 1) - 1);
727 const binary_relation_exprt no_overflow_lower(
728 op, ID_gt, lower.to_expr());
729
731 and_exprt(no_overflow_lower, no_overflow_upper),
732 "arithmetic overflow on float to signed integer type conversion",
733 "overflow",
735 expr,
736 guard);
737 }
738 }
739 else if(type.id() == ID_unsignedbv)
740 {
741 std::size_t new_width = to_unsignedbv_type(type).get_width();
742
743 if(old_type.id() == ID_signedbv) // signed -> unsigned
744 {
745 std::size_t old_width = to_signedbv_type(old_type).get_width();
746
747 if(new_width >= old_width - 1)
748 {
749 // only need lower bound check
750 const binary_relation_exprt no_overflow_lower(
751 op, ID_ge, from_integer(0, old_type));
752
754 no_overflow_lower,
755 "arithmetic overflow on signed to unsigned type conversion",
756 "overflow",
758 expr,
759 guard);
760 }
761 else
762 {
763 // need both
764 const binary_relation_exprt no_overflow_upper(
765 op, ID_le, from_integer(power(2, new_width) - 1, old_type));
766
767 const binary_relation_exprt no_overflow_lower(
768 op, ID_ge, from_integer(0, old_type));
769
771 and_exprt(no_overflow_lower, no_overflow_upper),
772 "arithmetic overflow on signed to unsigned type conversion",
773 "overflow",
775 expr,
776 guard);
777 }
778 }
779 else if(old_type.id() == ID_unsignedbv) // unsigned -> unsigned
780 {
781 std::size_t old_width = to_unsignedbv_type(old_type).get_width();
782 if(new_width >= old_width)
783 return; // always ok
784
785 const binary_relation_exprt no_overflow_upper(
786 op, ID_le, from_integer(power(2, new_width) - 1, old_type));
787
789 no_overflow_upper,
790 "arithmetic overflow on unsigned to unsigned type conversion",
791 "overflow",
793 expr,
794 guard);
795 }
796 else if(old_type.id() == ID_floatbv) // float -> unsigned
797 {
798 // Note that the fractional part is truncated!
799 ieee_floatt upper(to_floatbv_type(old_type));
800 upper.from_integer(power(2, new_width) - 1);
801 const binary_relation_exprt no_overflow_upper(
802 op, ID_lt, upper.to_expr());
803
804 ieee_floatt lower(to_floatbv_type(old_type));
805 lower.from_integer(-1);
806 const binary_relation_exprt no_overflow_lower(
807 op, ID_gt, lower.to_expr());
808
810 and_exprt(no_overflow_lower, no_overflow_upper),
811 "arithmetic overflow on float to unsigned integer type conversion",
812 "overflow",
814 expr,
815 guard);
816 }
817 }
818 }
819}
820
822 const exprt &expr,
823 const guardt &guard)
824{
826 return;
827
828 // First, check type.
829 const typet &type = expr.type();
830
831 if(type.id() == ID_signedbv && !enable_signed_overflow_check)
832 return;
833
834 if(type.id() == ID_unsignedbv && !enable_unsigned_overflow_check)
835 return;
836
837 // add overflow subgoal
838
839 if(expr.id() == ID_div)
840 {
841 // undefined for signed division INT_MIN/-1
842 if(type.id() == ID_signedbv)
843 {
844 const auto &div_expr = to_div_expr(expr);
845
846 equal_exprt int_min_eq(
847 div_expr.dividend(), to_signedbv_type(type).smallest_expr());
848
849 equal_exprt minus_one_eq(div_expr.divisor(), from_integer(-1, type));
850
852 not_exprt(and_exprt(int_min_eq, minus_one_eq)),
853 "arithmetic overflow on signed division",
854 "overflow",
856 expr,
857 guard);
858 }
859
860 return;
861 }
862 else if(expr.id() == ID_unary_minus)
863 {
864 if(type.id() == ID_signedbv)
865 {
866 // overflow on unary- on signed integers can only happen with the
867 // smallest representable number 100....0
868
869 equal_exprt int_min_eq(
870 to_unary_minus_expr(expr).op(), to_signedbv_type(type).smallest_expr());
871
873 not_exprt(int_min_eq),
874 "arithmetic overflow on signed unary minus",
875 "overflow",
877 expr,
878 guard);
879 }
880 else if(type.id() == ID_unsignedbv)
881 {
882 // Overflow on unary- on unsigned integers happens for all operands
883 // that are not zero.
884
885 notequal_exprt not_eq_zero(
886 to_unary_minus_expr(expr).op(), to_unsignedbv_type(type).zero_expr());
887
889 not_eq_zero,
890 "arithmetic overflow on unsigned unary minus",
891 "overflow",
893 expr,
894 guard);
895 }
896
897 return;
898 }
899 else if(expr.id() == ID_shl)
900 {
901 if(type.id() == ID_signedbv)
902 {
903 const auto &shl_expr = to_shl_expr(expr);
904 const auto &op = shl_expr.op();
905 const auto &op_type = to_signedbv_type(type);
906 const auto op_width = op_type.get_width();
907 const auto &distance = shl_expr.distance();
908 const auto &distance_type = distance.type();
909
910 // a left shift of a negative value is undefined;
911 // yet this isn't an overflow
912 exprt neg_value_shift;
913
914 if(op_type.id() == ID_unsignedbv)
915 neg_value_shift = false_exprt();
916 else
917 neg_value_shift =
918 binary_relation_exprt(op, ID_lt, from_integer(0, op_type));
919
920 // a shift with negative distance is undefined;
921 // yet this isn't an overflow
922 exprt neg_dist_shift;
923
924 if(distance_type.id() == ID_unsignedbv)
925 neg_dist_shift = false_exprt();
926 else
927 {
928 neg_dist_shift = binary_relation_exprt(
929 distance, ID_lt, from_integer(0, distance_type));
930 }
931
932 // shifting a non-zero value by more than its width is undefined;
933 // yet this isn't an overflow
934 const exprt dist_too_large = binary_predicate_exprt(
935 distance, ID_gt, from_integer(op_width, distance_type));
936
937 const exprt op_zero = equal_exprt(op, from_integer(0, op_type));
938
939 auto new_type = to_bitvector_type(op_type);
940 new_type.set_width(op_width * 2);
941
942 const exprt op_ext = typecast_exprt(op, new_type);
943
944 const exprt op_ext_shifted = shl_exprt(op_ext, distance);
945
946 // The semantics of signed left shifts are contentious for the case
947 // that a '1' is shifted into the signed bit.
948 // Assuming 32-bit integers, 1<<31 is implementation-defined
949 // in ANSI C and C++98, but is explicitly undefined by C99,
950 // C11 and C++11.
951 bool allow_shift_into_sign_bit = true;
952
953 if(mode == ID_C)
954 {
955 if(
958 {
959 allow_shift_into_sign_bit = false;
960 }
961 }
962 else if(mode == ID_cpp)
963 {
964 if(
968 {
969 allow_shift_into_sign_bit = false;
970 }
971 }
972
973 const unsigned number_of_top_bits =
974 allow_shift_into_sign_bit ? op_width : op_width + 1;
975
976 const exprt top_bits = extractbits_exprt(
977 op_ext_shifted,
978 new_type.get_width() - 1,
979 new_type.get_width() - number_of_top_bits,
980 unsignedbv_typet(number_of_top_bits));
981
982 const exprt top_bits_zero =
983 equal_exprt(top_bits, from_integer(0, top_bits.type()));
984
985 // a negative distance shift isn't an overflow;
986 // a negative value shift isn't an overflow;
987 // a shift that's too far isn't an overflow;
988 // a shift of zero isn't overflow;
989 // else check the top bits
992 {neg_value_shift,
993 neg_dist_shift,
994 dist_too_large,
995 op_zero,
996 top_bits_zero}),
997 "arithmetic overflow on signed shl",
998 "overflow",
1000 expr,
1001 guard);
1002 }
1003
1004 return;
1005 }
1006
1007 multi_ary_exprt overflow(
1008 "overflow-" + expr.id_string(), expr.operands(), bool_typet());
1009
1010 if(expr.operands().size() >= 3)
1011 {
1012 // The overflow checks are binary!
1013 // We break these up.
1014
1015 for(std::size_t i = 1; i < expr.operands().size(); i++)
1016 {
1017 exprt tmp;
1018
1019 if(i == 1)
1020 tmp = to_multi_ary_expr(expr).op0();
1021 else
1022 {
1023 tmp = expr;
1024 tmp.operands().resize(i);
1025 }
1026
1027 std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed";
1028
1030 not_exprt{binary_overflow_exprt{tmp, expr.id(), expr.operands()[i]}},
1031 "arithmetic overflow on " + kind + " " + expr.id_string(),
1032 "overflow",
1033 expr.find_source_location(),
1034 expr,
1035 guard);
1036 }
1037 }
1038 else if(expr.operands().size() == 2)
1039 {
1040 std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed";
1041
1042 const binary_exprt &bexpr = to_binary_expr(expr);
1044 not_exprt{binary_overflow_exprt{bexpr.lhs(), expr.id(), bexpr.rhs()}},
1045 "arithmetic overflow on " + kind + " " + expr.id_string(),
1046 "overflow",
1047 expr.find_source_location(),
1048 expr,
1049 guard);
1050 }
1051 else
1052 {
1053 PRECONDITION(expr.id() == ID_unary_minus);
1054
1055 std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed";
1056
1059 "arithmetic overflow on " + kind + " " + expr.id_string(),
1060 "overflow",
1061 expr.find_source_location(),
1062 expr,
1063 guard);
1064 }
1065}
1066
1068{
1070 return;
1071
1072 // First, check type.
1073 const typet &type = expr.type();
1074
1075 if(type.id() != ID_floatbv)
1076 return;
1077
1078 // add overflow subgoal
1079
1080 if(expr.id() == ID_typecast)
1081 {
1082 // Can overflow if casting from larger
1083 // to smaller type.
1084 const auto &op = to_typecast_expr(expr).op();
1085 if(op.type().id() == ID_floatbv)
1086 {
1087 // float-to-float
1088 or_exprt overflow_check{isinf_exprt(op), not_exprt(isinf_exprt(expr))};
1089
1091 std::move(overflow_check),
1092 "arithmetic overflow on floating-point typecast",
1093 "overflow",
1094 expr.find_source_location(),
1095 expr,
1096 guard);
1097 }
1098 else
1099 {
1100 // non-float-to-float
1102 not_exprt(isinf_exprt(expr)),
1103 "arithmetic overflow on floating-point typecast",
1104 "overflow",
1105 expr.find_source_location(),
1106 expr,
1107 guard);
1108 }
1109
1110 return;
1111 }
1112 else if(expr.id() == ID_div)
1113 {
1114 // Can overflow if dividing by something small
1115 or_exprt overflow_check(
1116 isinf_exprt(to_div_expr(expr).dividend()), not_exprt(isinf_exprt(expr)));
1117
1119 std::move(overflow_check),
1120 "arithmetic overflow on floating-point division",
1121 "overflow",
1122 expr.find_source_location(),
1123 expr,
1124 guard);
1125
1126 return;
1127 }
1128 else if(expr.id() == ID_mod)
1129 {
1130 // Can't overflow
1131 return;
1132 }
1133 else if(expr.id() == ID_unary_minus)
1134 {
1135 // Can't overflow
1136 return;
1137 }
1138 else if(expr.id() == ID_plus || expr.id() == ID_mult || expr.id() == ID_minus)
1139 {
1140 if(expr.operands().size() == 2)
1141 {
1142 // Can overflow
1143 or_exprt overflow_check(
1144 isinf_exprt(to_binary_expr(expr).op0()),
1145 isinf_exprt(to_binary_expr(expr).op1()),
1146 not_exprt(isinf_exprt(expr)));
1147
1148 std::string kind = expr.id() == ID_plus
1149 ? "addition"
1150 : expr.id() == ID_minus
1151 ? "subtraction"
1152 : expr.id() == ID_mult ? "multiplication" : "";
1153
1155 std::move(overflow_check),
1156 "arithmetic overflow on floating-point " + kind,
1157 "overflow",
1158 expr.find_source_location(),
1159 expr,
1160 guard);
1161
1162 return;
1163 }
1164 else if(expr.operands().size() >= 3)
1165 {
1166 DATA_INVARIANT(expr.id() != ID_minus, "minus expression must be binary");
1167
1168 // break up
1170 return;
1171 }
1172 }
1173}
1174
1176{
1177 if(!enable_nan_check)
1178 return;
1179
1180 // first, check type
1181 if(expr.type().id() != ID_floatbv)
1182 return;
1183
1184 if(
1185 expr.id() != ID_plus && expr.id() != ID_mult && expr.id() != ID_div &&
1186 expr.id() != ID_minus)
1187 return;
1188
1189 // add NaN subgoal
1190
1191 exprt isnan;
1192
1193 if(expr.id() == ID_div)
1194 {
1195 const auto &div_expr = to_div_expr(expr);
1196
1197 // there a two ways to get a new NaN on division:
1198 // 0/0 = NaN and x/inf = NaN
1199 // (note that x/0 = +-inf for x!=0 and x!=inf)
1200 const and_exprt zero_div_zero(
1202 div_expr.op0(), from_integer(0, div_expr.dividend().type())),
1204 div_expr.op1(), from_integer(0, div_expr.divisor().type())));
1205
1206 const isinf_exprt div_inf(div_expr.op1());
1207
1208 isnan = or_exprt(zero_div_zero, div_inf);
1209 }
1210 else if(expr.id() == ID_mult)
1211 {
1212 if(expr.operands().size() >= 3)
1213 return nan_check(make_binary(expr), guard);
1214
1215 const auto &mult_expr = to_mult_expr(expr);
1216
1217 // Inf * 0 is NaN
1218 const and_exprt inf_times_zero(
1219 isinf_exprt(mult_expr.op0()),
1221 mult_expr.op1(), from_integer(0, mult_expr.op1().type())));
1222
1223 const and_exprt zero_times_inf(
1225 mult_expr.op1(), from_integer(0, mult_expr.op1().type())),
1226 isinf_exprt(mult_expr.op0()));
1227
1228 isnan = or_exprt(inf_times_zero, zero_times_inf);
1229 }
1230 else if(expr.id() == ID_plus)
1231 {
1232 if(expr.operands().size() >= 3)
1233 return nan_check(make_binary(expr), guard);
1234
1235 const auto &plus_expr = to_plus_expr(expr);
1236
1237 // -inf + +inf = NaN and +inf + -inf = NaN,
1238 // i.e., signs differ
1239 ieee_float_spect spec = ieee_float_spect(to_floatbv_type(plus_expr.type()));
1240 exprt plus_inf = ieee_floatt::plus_infinity(spec).to_expr();
1241 exprt minus_inf = ieee_floatt::minus_infinity(spec).to_expr();
1242
1243 isnan = or_exprt(
1244 and_exprt(
1245 equal_exprt(plus_expr.op0(), minus_inf),
1246 equal_exprt(plus_expr.op1(), plus_inf)),
1247 and_exprt(
1248 equal_exprt(plus_expr.op0(), plus_inf),
1249 equal_exprt(plus_expr.op1(), minus_inf)));
1250 }
1251 else if(expr.id() == ID_minus)
1252 {
1253 // +inf - +inf = NaN and -inf - -inf = NaN,
1254 // i.e., signs match
1255
1256 const auto &minus_expr = to_minus_expr(expr);
1257
1258 ieee_float_spect spec =
1259 ieee_float_spect(to_floatbv_type(minus_expr.type()));
1260 exprt plus_inf = ieee_floatt::plus_infinity(spec).to_expr();
1261 exprt minus_inf = ieee_floatt::minus_infinity(spec).to_expr();
1262
1263 isnan = or_exprt(
1264 and_exprt(
1265 equal_exprt(minus_expr.lhs(), plus_inf),
1266 equal_exprt(minus_expr.rhs(), plus_inf)),
1267 and_exprt(
1268 equal_exprt(minus_expr.lhs(), minus_inf),
1269 equal_exprt(minus_expr.rhs(), minus_inf)));
1270 }
1271 else
1273
1275 boolean_negate(isnan),
1276 "NaN on " + expr.id_string(),
1277 "NaN",
1278 expr.find_source_location(),
1279 expr,
1280 guard);
1281}
1282
1284 const binary_exprt &expr,
1285 const guardt &guard)
1286{
1288 return;
1289
1290 if(
1291 expr.op0().type().id() == ID_pointer &&
1292 expr.op1().type().id() == ID_pointer)
1293 {
1294 // add same-object subgoal
1295
1296 exprt same_object = ::same_object(expr.op0(), expr.op1());
1297
1300 "same object violation",
1301 "pointer",
1302 expr.find_source_location(),
1303 expr,
1304 guard);
1305
1306 for(const auto &pointer : expr.operands())
1307 {
1308 // just this particular byte must be within object bounds or one past the
1309 // end
1310 const auto size = from_integer(0, size_type());
1311 auto conditions = get_pointer_dereferenceable_conditions(pointer, size);
1312
1313 for(const auto &c : conditions)
1314 {
1316 c.assertion,
1317 "pointer relation: " + c.description,
1318 "pointer arithmetic",
1319 expr.find_source_location(),
1320 pointer,
1321 guard);
1322 }
1323 }
1324 }
1325}
1326
1328 const exprt &expr,
1329 const guardt &guard)
1330{
1332 return;
1333
1334 if(expr.id() != ID_plus && expr.id() != ID_minus)
1335 return;
1336
1338 expr.operands().size() == 2,
1339 "pointer arithmetic expected to have exactly 2 operands");
1340
1341 // multiplying the offset by the object size must not result in arithmetic
1342 // overflow
1343 const typet &object_type = to_pointer_type(expr.type()).base_type();
1344 if(object_type.id() != ID_empty)
1345 {
1346 auto size_of_expr_opt = size_of_expr(object_type, ns);
1347 CHECK_RETURN(size_of_expr_opt.has_value());
1348 exprt object_size = size_of_expr_opt.value();
1349
1350 const binary_exprt &binary_expr = to_binary_expr(expr);
1351 exprt offset_operand = binary_expr.lhs().type().id() == ID_pointer
1352 ? binary_expr.rhs()
1353 : binary_expr.lhs();
1354 mult_exprt mul{
1355 offset_operand,
1357 mul.add_source_location() = offset_operand.source_location();
1358
1359 flag_overridet override_overflow(offset_operand.source_location());
1360 override_overflow.set_flag(
1361 enable_signed_overflow_check, true, "signed_overflow_check");
1362 override_overflow.set_flag(
1363 enable_unsigned_overflow_check, true, "unsigned_overflow_check");
1365 }
1366
1367 // the result must be within object bounds or one past the end
1368 const auto size = from_integer(0, size_type());
1369 auto conditions = get_pointer_dereferenceable_conditions(expr, size);
1370
1371 for(const auto &c : conditions)
1372 {
1374 c.assertion,
1375 "pointer arithmetic: " + c.description,
1376 "pointer arithmetic",
1377 expr.find_source_location(),
1378 expr,
1379 guard);
1380 }
1381}
1382
1384 const dereference_exprt &expr,
1385 const exprt &src_expr,
1386 const guardt &guard)
1387{
1389 return;
1390
1391 const exprt &pointer = expr.pointer();
1392
1393 exprt size;
1394
1395 if(expr.type().id() == ID_empty)
1396 {
1397 // a dereference *p (with p being a pointer to void) is valid if p points to
1398 // valid memory (of any size). the smallest possible size of the memory
1399 // segment p could be pointing to is 1, hence we use this size for the
1400 // address check
1401 size = from_integer(1, size_type());
1402 }
1403 else
1404 {
1405 auto size_of_expr_opt = size_of_expr(expr.type(), ns);
1406 CHECK_RETURN(size_of_expr_opt.has_value());
1407 size = size_of_expr_opt.value();
1408 }
1409
1410 auto conditions = get_pointer_dereferenceable_conditions(pointer, size);
1411
1412 for(const auto &c : conditions)
1413 {
1415 c.assertion,
1416 "dereference failure: " + c.description,
1417 "pointer dereference",
1418 src_expr.find_source_location(),
1419 src_expr,
1420 guard);
1421 }
1422}
1423
1425 const exprt &expr,
1426 const guardt &guard)
1427{
1429 return;
1430
1431 if(expr.source_location().is_built_in())
1432 return;
1433
1434 const exprt pointer =
1435 (expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok)
1436 ? to_r_or_w_ok_expr(expr).pointer()
1439 : to_unary_expr(expr).op();
1440
1441 CHECK_RETURN(pointer.type().id() == ID_pointer);
1442
1443 if(pointer.id() == ID_symbol)
1444 {
1445 const auto &symbol_expr = to_symbol_expr(pointer);
1446
1447 if(has_prefix(id2string(symbol_expr.get_identifier()), CPROVER_PREFIX))
1448 return;
1449 }
1450
1452 pointer, from_integer(0, size_type()));
1453 for(const auto &c : conditions)
1454 {
1456 or_exprt{null_object(pointer), c.assertion},
1457 c.description,
1458 "pointer primitives",
1459 expr.source_location(),
1460 expr,
1461 guard);
1462 }
1463}
1464
1466{
1467 // we don't need to include the __CPROVER_same_object primitive here as it
1468 // is replaced by lower level primitives in the special function handling
1469 // during typechecking (see c_typecheck_expr.cpp)
1470
1471 // pointer_object and pointer_offset are well-defined for an arbitrary
1472 // pointer-typed operand (and the operands themselves have been checked
1473 // separately for, e.g., invalid pointer dereferencing via check_rec):
1474 // pointer_object and pointer_offset just extract a subset of bits from the
1475 // pointer. If that pointer was unconstrained (non-deterministic), the result
1476 // will equally be non-deterministic.
1477 return can_cast_expr<object_size_exprt>(expr) || expr.id() == ID_r_ok ||
1478 expr.id() == ID_w_ok || expr.id() == ID_rw_ok ||
1480 expr.id() == ID_is_dynamic_object;
1481}
1482
1485 const exprt &address,
1486 const exprt &size)
1487{
1488 auto conditions =
1490 if(auto maybe_null_condition = get_pointer_is_null_condition(address, size))
1491 {
1492 conditions.push_front(*maybe_null_condition);
1493 }
1494 return conditions;
1495}
1496
1497std::string goto_check_ct::array_name(const exprt &expr)
1498{
1499 return ::array_name(ns, expr);
1500}
1501
1503{
1505 return;
1506
1507 if(expr.id() == ID_index)
1509 else if(
1510 (expr.id() == ID_count_leading_zeros &&
1511 !to_count_leading_zeros_expr(expr).zero_permitted()) ||
1512 (expr.id() == ID_count_trailing_zeros &&
1513 !to_count_trailing_zeros_expr(expr).zero_permitted()))
1514 {
1516 }
1517}
1518
1520 const index_exprt &expr,
1521 const guardt &guard)
1522{
1523 const typet &array_type = expr.array().type();
1524
1525 if(array_type.id() == ID_pointer)
1526 throw "index got pointer as array type";
1527 else if(array_type.id() != ID_array && array_type.id() != ID_vector)
1528 throw "bounds check expected array or vector type, got " +
1529 array_type.id_string();
1530
1531 std::string name = array_name(expr.array());
1532
1533 const exprt &index = expr.index();
1535 ode.build(expr, ns);
1536
1537 if(index.type().id() != ID_unsignedbv)
1538 {
1539 // we undo typecasts to signedbv
1540 if(
1541 index.id() == ID_typecast &&
1542 to_typecast_expr(index).op().type().id() == ID_unsignedbv)
1543 {
1544 // ok
1545 }
1546 else
1547 {
1548 const auto i = numeric_cast<mp_integer>(index);
1549
1550 if(!i.has_value() || *i < 0)
1551 {
1552 exprt effective_offset = ode.offset();
1553
1554 if(ode.root_object().id() == ID_dereference)
1555 {
1556 exprt p_offset =
1558
1559 effective_offset = plus_exprt{
1560 p_offset,
1562 effective_offset, p_offset.type())};
1563 }
1564
1565 exprt zero = from_integer(0, effective_offset.type());
1566
1567 // the final offset must not be negative
1568 binary_relation_exprt inequality(
1569 effective_offset, ID_ge, std::move(zero));
1570
1572 inequality,
1573 name + " lower bound",
1574 "array bounds",
1575 expr.find_source_location(),
1576 expr,
1577 guard);
1578 }
1579 }
1580 }
1581
1582 if(ode.root_object().id() == ID_dereference)
1583 {
1584 const exprt &pointer = to_dereference_expr(ode.root_object()).pointer();
1585
1586 const plus_exprt effective_offset{
1587 ode.offset(),
1589 pointer_offset(pointer), ode.offset().type())};
1590
1591 binary_relation_exprt inequality{
1592 effective_offset,
1593 ID_lt,
1595 object_size(pointer), effective_offset.type())};
1596
1597 exprt in_bounds_of_some_explicit_allocation =
1599 pointer,
1600 plus_exprt{ode.offset(), from_integer(1, ode.offset().type())});
1601
1602 or_exprt precond(
1603 std::move(in_bounds_of_some_explicit_allocation), inequality);
1604
1606 precond,
1607 name + " dynamic object upper bound",
1608 "array bounds",
1609 expr.find_source_location(),
1610 expr,
1611 guard);
1612
1613 return;
1614 }
1615
1616 const exprt &size = array_type.id() == ID_array
1617 ? to_array_type(array_type).size()
1618 : to_vector_type(array_type).size();
1619
1620 if(size.is_nil() && !array_type.get_bool(ID_C_flexible_array_member))
1621 {
1622 // Linking didn't complete, we don't have a size.
1623 // Not clear what to do.
1624 }
1625 else if(size.id() == ID_infinity)
1626 {
1627 }
1628 else if(
1629 expr.array().id() == ID_member &&
1630 (size.is_zero() || array_type.get_bool(ID_C_flexible_array_member)))
1631 {
1632 // a variable sized struct member
1633 //
1634 // Excerpt from the C standard on flexible array members:
1635 // However, when a . (or ->) operator has a left operand that is (a pointer
1636 // to) a structure with a flexible array member and the right operand names
1637 // that member, it behaves as if that member were replaced with the longest
1638 // array (with the same element type) that would not make the structure
1639 // larger than the object being accessed; [...]
1640 const auto type_size_opt =
1642 CHECK_RETURN(type_size_opt.has_value());
1643
1644 binary_relation_exprt inequality(
1645 ode.offset(),
1646 ID_lt,
1647 from_integer(type_size_opt.value(), ode.offset().type()));
1648
1650 inequality,
1651 name + " upper bound",
1652 "array bounds",
1653 expr.find_source_location(),
1654 expr,
1655 guard);
1656 }
1657 else
1658 {
1659 binary_relation_exprt inequality{
1660 typecast_exprt::conditional_cast(index, size.type()), ID_lt, size};
1661
1663 inequality,
1664 name + " upper bound",
1665 "array bounds",
1666 expr.find_source_location(),
1667 expr,
1668 guard);
1669 }
1670}
1671
1673 const unary_exprt &expr,
1674 const guardt &guard)
1675{
1676 std::string name;
1677
1678 if(expr.id() == ID_count_leading_zeros)
1679 name = "leading";
1680 else if(expr.id() == ID_count_trailing_zeros)
1681 name = "trailing";
1682 else
1683 PRECONDITION(false);
1684
1686 notequal_exprt{expr.op(), from_integer(0, expr.op().type())},
1687 "count " + name + " zeros is undefined for value zero",
1688 "bit count",
1689 expr.find_source_location(),
1690 expr,
1691 guard);
1692}
1693
1695 const exprt &asserted_expr,
1696 const std::string &comment,
1697 const std::string &property_class,
1698 const source_locationt &source_location,
1699 const exprt &src_expr,
1700 const guardt &guard)
1701{
1702 // first try simplifier on it
1703 exprt simplified_expr =
1704 enable_simplify ? simplify_expr(asserted_expr, ns) : asserted_expr;
1705
1706 // throw away trivial properties?
1707 if(!retain_trivial && simplified_expr.is_true())
1708 return;
1709
1710 // add the guard
1711 exprt guarded_expr = guard(simplified_expr);
1712
1713 if(assertions.insert(std::make_pair(src_expr, guarded_expr)).second)
1714 {
1715 std::string source_expr_string;
1716 get_language_from_mode(mode)->from_expr(src_expr, source_expr_string, ns);
1717
1718 source_locationt annotated_location = source_location;
1719 annotated_location.set_comment(comment + " in " + source_expr_string);
1720 annotated_location.set_property_class(property_class);
1721
1722 add_all_checked_named_check_pragmas(annotated_location);
1723
1725 {
1727 std::move(guarded_expr), annotated_location));
1728 }
1729 else
1730 {
1732 std::move(guarded_expr), annotated_location));
1733 }
1734 }
1735}
1736
1738{
1739 // we don't look into quantifiers
1740 if(expr.id() == ID_exists || expr.id() == ID_forall)
1741 return;
1742
1743 if(expr.id() == ID_dereference)
1744 {
1745 check_rec(to_dereference_expr(expr).pointer(), guard);
1746 }
1747 else if(expr.id() == ID_index)
1748 {
1749 const index_exprt &index_expr = to_index_expr(expr);
1750 check_rec_address(index_expr.array(), guard);
1751 check_rec(index_expr.index(), guard);
1752 }
1753 else
1754 {
1755 for(const auto &operand : expr.operands())
1756 check_rec_address(operand, guard);
1757 }
1758}
1759
1761{
1763 expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies);
1764 INVARIANT(
1765 expr.is_boolean(),
1766 "'" + expr.id_string() + "' must be Boolean, but got " + expr.pretty());
1767
1768 exprt::operandst constraints;
1769
1770 for(const auto &op : expr.operands())
1771 {
1772 INVARIANT(
1773 op.is_boolean(),
1774 "'" + expr.id_string() + "' takes Boolean operands only, but got " +
1775 op.pretty());
1776
1777 auto new_guard = [&guard, &constraints](exprt expr) {
1778 return guard(implication(conjunction(constraints), expr));
1779 };
1780
1781 check_rec(op, new_guard);
1782
1783 constraints.push_back(expr.id() == ID_or ? boolean_negate(op) : op);
1784 }
1785}
1786
1788{
1789 INVARIANT(
1790 if_expr.cond().is_boolean(),
1791 "first argument of if must be boolean, but got " + if_expr.cond().pretty());
1792
1793 check_rec(if_expr.cond(), guard);
1794
1795 {
1796 auto new_guard = [&guard, &if_expr](exprt expr) {
1797 return guard(implication(if_expr.cond(), std::move(expr)));
1798 };
1799 check_rec(if_expr.true_case(), new_guard);
1800 }
1801
1802 {
1803 auto new_guard = [&guard, &if_expr](exprt expr) {
1804 return guard(implication(not_exprt(if_expr.cond()), std::move(expr)));
1805 };
1806 check_rec(if_expr.false_case(), new_guard);
1807 }
1808}
1809
1810bool goto_check_ct::check_rec_member(
1811 const member_exprt &member,
1812 const guardt &guard)
1813{
1814 const dereference_exprt &deref = to_dereference_expr(member.struct_op());
1815
1816 check_rec(deref.pointer(), guard);
1817
1818 // avoid building the following expressions when pointer_validity_check
1819 // would return immediately anyway
1821 return true;
1822
1823 // we rewrite s->member into *(s+member_offset)
1824 // to avoid requiring memory safety of the entire struct
1825 auto member_offset_opt = member_offset_expr(member, ns);
1826
1827 if(member_offset_opt.has_value())
1828 {
1829 pointer_typet new_pointer_type = to_pointer_type(deref.pointer().type());
1830 new_pointer_type.base_type() = member.type();
1831
1832 const exprt char_pointer = typecast_exprt::conditional_cast(
1833 deref.pointer(), pointer_type(char_type()));
1834
1835 const exprt new_address_casted = typecast_exprt::conditional_cast(
1836 plus_exprt{
1837 char_pointer,
1839 member_offset_opt.value(), pointer_diff_type())},
1840 new_pointer_type);
1841
1842 dereference_exprt new_deref{new_address_casted};
1843 new_deref.add_source_location() = deref.source_location();
1844 pointer_validity_check(new_deref, member, guard);
1845
1846 return true;
1847 }
1848 return false;
1849}
1850
1851void goto_check_ct::check_rec_div(
1852 const div_exprt &div_expr,
1853 const guardt &guard)
1854{
1856
1857 if(div_expr.type().id() == ID_signedbv)
1858 integer_overflow_check(div_expr, guard);
1859 else if(div_expr.type().id() == ID_floatbv)
1860 {
1861 nan_check(div_expr, guard);
1862 float_overflow_check(div_expr, guard);
1863 }
1864}
1865
1866void goto_check_ct::check_rec_arithmetic_op(
1867 const exprt &expr,
1868 const guardt &guard)
1869{
1870 if(expr.type().id() == ID_signedbv || expr.type().id() == ID_unsignedbv)
1871 {
1873
1874 if(
1875 expr.operands().size() == 2 && expr.id() == ID_minus &&
1876 expr.operands()[0].type().id() == ID_pointer &&
1877 expr.operands()[1].type().id() == ID_pointer)
1878 {
1880 }
1881 }
1882 else if(expr.type().id() == ID_floatbv)
1883 {
1884 nan_check(expr, guard);
1886 }
1887 else if(expr.type().id() == ID_pointer)
1888 {
1890 }
1891}
1892
1893void goto_check_ct::check_rec(const exprt &expr, const guardt &guard)
1894{
1895 if(expr.id() == ID_exists || expr.id() == ID_forall)
1896 {
1897 // the scoped variables may be used in the assertion
1898 const auto &quantifier_expr = to_quantifier_expr(expr);
1899
1900 auto new_guard = [&guard, &quantifier_expr](exprt expr) {
1901 return guard(forall_exprt(quantifier_expr.symbol(), expr));
1902 };
1903
1904 check_rec(quantifier_expr.where(), new_guard);
1905 return;
1906 }
1907 else if(expr.id() == ID_address_of)
1908 {
1910 return;
1911 }
1912 else if(expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies)
1913 {
1915 return;
1916 }
1917 else if(expr.id() == ID_if)
1918 {
1920 return;
1921 }
1922 else if(
1923 expr.id() == ID_member &&
1924 to_member_expr(expr).struct_op().id() == ID_dereference)
1925 {
1926 if(check_rec_member(to_member_expr(expr), guard))
1927 return;
1928 }
1929
1930 for(const auto &op : expr.operands())
1931 check_rec(op, guard);
1932
1933 if(expr.type().id() == ID_c_enum_tag)
1934 enum_range_check(expr, guard);
1935
1936 if(expr.id() == ID_index)
1937 {
1938 bounds_check(expr, guard);
1939 }
1940 else if(expr.id() == ID_div)
1941 {
1942 check_rec_div(to_div_expr(expr), guard);
1943 }
1944 else if(expr.id() == ID_shl || expr.id() == ID_ashr || expr.id() == ID_lshr)
1945 {
1947
1948 if(expr.id() == ID_shl && expr.type().id() == ID_signedbv)
1950 }
1951 else if(expr.id() == ID_mod)
1952 {
1955 }
1956 else if(
1957 expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
1958 expr.id() == ID_unary_minus)
1959 {
1960 check_rec_arithmetic_op(expr, guard);
1961 }
1962 else if(expr.id() == ID_typecast)
1963 conversion_check(expr, guard);
1964 else if(
1965 expr.id() == ID_le || expr.id() == ID_lt || expr.id() == ID_ge ||
1966 expr.id() == ID_gt)
1968 else if(expr.id() == ID_dereference)
1969 {
1971 }
1973 {
1975 }
1976 else if(
1977 expr.id() == ID_count_leading_zeros || expr.id() == ID_count_trailing_zeros)
1978 {
1979 bounds_check(expr, guard);
1980 }
1981}
1982
1984{
1985 check_rec(expr, identity);
1986}
1987
1989{
1990 const symbolt &leak = ns.lookup(CPROVER_PREFIX "memory_leak");
1991 const symbol_exprt leak_expr = leak.symbol_expr();
1992
1993 // add self-assignment to get helpful counterexample output
1994 new_code.add(goto_programt::make_assignment(leak_expr, leak_expr));
1995
1996 source_locationt source_location;
1997 source_location.set_function(function_id);
1998
1999 equal_exprt eq(leak_expr, null_pointer_exprt(to_pointer_type(leak.type)));
2000
2002 eq,
2003 "dynamically allocated memory never freed",
2004 "memory-leak",
2005 source_location,
2006 eq,
2007 identity);
2008}
2009
2011 const irep_idt &function_identifier,
2012 goto_functiont &goto_function)
2013{
2014 const auto &function_symbol = ns.lookup(function_identifier);
2015 mode = function_symbol.mode;
2016
2017 if(mode != ID_C && mode != ID_cpp)
2018 return;
2019
2020 assertions.clear();
2021
2022 bool did_something = false;
2023
2026
2027 goto_programt &goto_program = goto_function.body;
2028
2029 Forall_goto_program_instructions(it, goto_program)
2030 {
2031 current_target = it;
2033
2034 flag_overridet resetter(i.source_location());
2035 const auto &pragmas = i.source_location().get_pragmas();
2036 for(const auto &d : pragmas)
2037 {
2038 // match named-check related pragmas
2039 auto matched = match_named_check(d.first);
2040 if(matched.has_value())
2041 {
2042 auto named_check = matched.value();
2043 auto name = named_check.first;
2044 auto status = named_check.second;
2045 bool *flag = name_to_flag.find(name)->second;
2046 switch(status)
2047 {
2049 resetter.set_flag(*flag, true, name);
2050 break;
2052 resetter.set_flag(*flag, false, name);
2053 break;
2055 resetter.disable_flag(*flag, name);
2056 break;
2057 }
2058 }
2059 }
2060
2061 // add checked pragmas for all active checks
2063
2064 new_code.clear();
2065
2066 // we clear all recorded assertions if
2067 // 1) we want to generate all assertions or
2068 // 2) the instruction is a branch target
2069 if(retain_trivial || i.is_target())
2070 assertions.clear();
2071
2072 if(i.has_condition())
2073 {
2074 check(i.condition());
2075 }
2076
2077 // magic ERROR label?
2078 for(const auto &label : error_labels)
2079 {
2080 if(std::find(i.labels.begin(), i.labels.end(), label) != i.labels.end())
2081 {
2082 source_locationt annotated_location = i.source_location();
2083 annotated_location.set_property_class("error label");
2084 annotated_location.set_comment("error label " + label);
2085 annotated_location.set("user-provided", true);
2086
2088 {
2089 new_code.add(
2090 goto_programt::make_assumption(false_exprt{}, annotated_location));
2091 }
2092 else
2093 {
2094 new_code.add(
2095 goto_programt::make_assertion(false_exprt{}, annotated_location));
2096 }
2097 }
2098 }
2099
2100 if(i.is_other())
2101 {
2102 const auto &code = i.get_other();
2103 const irep_idt &statement = code.get_statement();
2104
2105 if(statement == ID_expression)
2106 {
2107 check(code);
2108 }
2109 else if(statement == ID_printf)
2110 {
2111 for(const auto &op : code.operands())
2112 check(op);
2113 }
2114 }
2115 else if(i.is_assign())
2116 {
2117 const exprt &assign_lhs = i.assign_lhs();
2118 const exprt &assign_rhs = i.assign_rhs();
2119
2120 // Disable enum range checks for left-hand sides as their values are yet
2121 // to be set (by this assignment).
2122 {
2123 flag_overridet resetter(i.source_location());
2124 resetter.disable_flag(enable_enum_range_check, "enum_range_check");
2125 check(assign_lhs);
2126 }
2127
2128 check(assign_rhs);
2129
2130 // the LHS might invalidate any assertion
2131 invalidate(assign_lhs);
2132 }
2133 else if(i.is_function_call())
2134 {
2135 // Disable enum range checks for left-hand sides as their values are yet
2136 // to be set (by this function call).
2137 {
2138 flag_overridet resetter(i.source_location());
2139 resetter.disable_flag(enable_enum_range_check, "enum_range_check");
2140 check(i.call_lhs());
2141 }
2142 check(i.call_function());
2143
2144 for(const auto &arg : i.call_arguments())
2145 check(arg);
2146
2148
2149 // the call might invalidate any assertion
2150 assertions.clear();
2151 }
2152 else if(i.is_set_return_value())
2153 {
2154 check(i.return_value());
2155 // the return value invalidate any assertion
2157 }
2158 else if(i.is_throw())
2159 {
2160 // this has no successor
2161 assertions.clear();
2162 }
2163 else if(i.is_assume())
2164 {
2165 // These are further 'exit points' of the program
2166 const exprt simplified_guard = simplify_expr(i.condition(), ns);
2167 if(
2168 enable_memory_cleanup_check && simplified_guard.is_false() &&
2169 (function_identifier == "abort" || function_identifier == "exit" ||
2170 function_identifier == "_Exit" ||
2171 (i.labels.size() == 1 && i.labels.front() == "__VERIFIER_abort")))
2172 {
2173 memory_leak_check(function_identifier);
2174 }
2175 }
2176 else if(i.is_dead())
2177 {
2179 {
2180 const symbol_exprt &variable = i.dead_symbol();
2181
2182 // is it dirty?
2183 if(local_bitvector_analysis->dirty(variable))
2184 {
2185 // need to mark the dead variable as dead
2186 exprt lhs = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
2187 exprt address_of_expr = typecast_exprt::conditional_cast(
2188 address_of_exprt(variable), lhs.type());
2189 if_exprt rhs(
2191 std::move(address_of_expr),
2192 lhs);
2194 code_assignt{std::move(lhs), std::move(rhs), i.source_location()},
2195 i.source_location()));
2196 }
2197 }
2198 }
2199 else if(i.is_end_function())
2200 {
2201 if(
2202 function_identifier == goto_functionst::entry_point() &&
2204 {
2205 memory_leak_check(function_identifier);
2206 }
2207 }
2208
2209 for(auto &instruction : new_code.instructions)
2210 {
2211 if(instruction.source_location().is_nil())
2212 {
2213 instruction.source_location_nonconst().id(irep_idt());
2214
2215 if(!it->source_location().get_file().empty())
2216 instruction.source_location_nonconst().set_file(
2217 it->source_location().get_file());
2218
2219 if(!it->source_location().get_line().empty())
2220 instruction.source_location_nonconst().set_line(
2221 it->source_location().get_line());
2222
2223 if(!it->source_location().get_function().empty())
2224 instruction.source_location_nonconst().set_function(
2225 it->source_location().get_function());
2226
2227 if(!it->source_location().get_column().empty())
2228 {
2229 instruction.source_location_nonconst().set_column(
2230 it->source_location().get_column());
2231 }
2232 }
2233 }
2234
2235 // insert new instructions -- make sure targets are not moved
2236 did_something |= !new_code.instructions.empty();
2237
2238 while(!new_code.instructions.empty())
2239 {
2240 goto_program.insert_before_swap(it, new_code.instructions.front());
2241 new_code.instructions.pop_front();
2242 it++;
2243 }
2244 }
2245
2246 if(did_something)
2247 remove_skip(goto_program);
2248}
2249
2252{
2253 if(i.call_function().id() != ID_symbol)
2254 return;
2255
2256 const irep_idt &identifier =
2258
2259 if(
2260 identifier == CPROVER_PREFIX "get_field" || identifier == CPROVER_PREFIX
2261 "set_field")
2262 {
2263 const exprt &expr = i.call_arguments()[0];
2264 PRECONDITION(expr.type().id() == ID_pointer);
2265 check(dereference_exprt(expr));
2266 }
2267}
2268
2271 const exprt &address,
2272 const exprt &size)
2273{
2275 PRECONDITION(address.type().id() == ID_pointer);
2278
2279 conditionst conditions;
2280
2281 const exprt in_bounds_of_some_explicit_allocation =
2283
2284 const bool unknown = flags.is_unknown() || flags.is_uninitialized();
2285
2286 if(unknown)
2287 {
2288 conditions.push_back(conditiont{
2289 not_exprt{is_invalid_pointer_exprt{address}}, "pointer invalid"});
2290 }
2291
2292 if(unknown || flags.is_dynamic_heap())
2293 {
2294 conditions.push_back(conditiont(
2295 or_exprt(
2296 in_bounds_of_some_explicit_allocation,
2297 not_exprt(deallocated(address, ns))),
2298 "deallocated dynamic object"));
2299 }
2300
2301 if(unknown || flags.is_dynamic_local())
2302 {
2303 conditions.push_back(conditiont(
2304 or_exprt(
2305 in_bounds_of_some_explicit_allocation,
2306 not_exprt(dead_object(address, ns))),
2307 "dead object"));
2308 }
2309
2310 if(flags.is_dynamic_heap())
2311 {
2312 const or_exprt object_bounds_violation(
2313 object_lower_bound(address, nil_exprt()),
2314 object_upper_bound(address, size));
2315
2316 conditions.push_back(conditiont(
2317 or_exprt(
2318 in_bounds_of_some_explicit_allocation,
2319 not_exprt(object_bounds_violation)),
2320 "pointer outside dynamic object bounds"));
2321 }
2322
2323 if(unknown || flags.is_dynamic_local() || flags.is_static_lifetime())
2324 {
2325 const or_exprt object_bounds_violation(
2326 object_lower_bound(address, nil_exprt()),
2327 object_upper_bound(address, size));
2328
2329 conditions.push_back(conditiont(
2330 or_exprt(
2331 in_bounds_of_some_explicit_allocation,
2332 not_exprt(object_bounds_violation)),
2333 "pointer outside object bounds"));
2334 }
2335
2336 if(unknown || flags.is_integer_address())
2337 {
2338 conditions.push_back(conditiont(
2340 integer_address(address), in_bounds_of_some_explicit_allocation),
2341 "invalid integer address"));
2342 }
2343
2344 return conditions;
2345}
2346
2349 const exprt &address,
2350 const exprt &size)
2351{
2353 PRECONDITION(address.type().id() == ID_pointer);
2356
2357 if(flags.is_unknown() || flags.is_uninitialized() || flags.is_null())
2358 {
2359 return {conditiont{
2360 or_exprt{
2362 not_exprt(null_object(address))},
2363 "pointer NULL"}};
2364 }
2365
2366 return {};
2367}
2368
2370 const exprt &pointer,
2371 const exprt &size)
2372{
2373 exprt::operandst alloc_disjuncts;
2374 for(const auto &a : allocations)
2375 {
2376 typecast_exprt int_ptr(pointer, a.first.type());
2377
2378 binary_relation_exprt lb_check(a.first, ID_le, int_ptr);
2379
2380 plus_exprt upper_bound{
2381 int_ptr, typecast_exprt::conditional_cast(size, int_ptr.type())};
2382
2383 binary_relation_exprt ub_check{
2384 std::move(upper_bound), ID_le, plus_exprt{a.first, a.second}};
2385
2386 alloc_disjuncts.push_back(
2387 and_exprt{std::move(lb_check), std::move(ub_check)});
2388 }
2389 return disjunction(alloc_disjuncts);
2390}
2391
2393 const irep_idt &function_identifier,
2394 goto_functionst::goto_functiont &goto_function,
2395 const namespacet &ns,
2396 const optionst &options,
2397 message_handlert &message_handler)
2398{
2399 goto_check_ct goto_check(ns, options, message_handler);
2400 goto_check.goto_check(function_identifier, goto_function);
2401}
2402
2404 const namespacet &ns,
2405 const optionst &options,
2406 goto_functionst &goto_functions,
2407 message_handlert &message_handler)
2408{
2409 goto_check_ct goto_check(ns, options, message_handler);
2410
2411 goto_check.collect_allocations(goto_functions);
2412
2413 for(auto &gf_entry : goto_functions.function_map)
2414 {
2415 goto_check.goto_check(gf_entry.first, gf_entry.second);
2416 }
2417}
2418
2420 const optionst &options,
2421 goto_modelt &goto_model,
2422 message_handlert &message_handler)
2423{
2424 const namespacet ns(goto_model.symbol_table);
2425 goto_check_c(ns, options, goto_model.goto_functions, message_handler);
2426}
2427
2429 source_locationt &source_location) const
2430{
2431 for(const auto &entry : name_to_flag)
2432 if(*(entry.second))
2433 source_location.add_pragma("checked:" + id2string(entry.first));
2434}
2435
2437 source_locationt &source_location) const
2438{
2439 for(const auto &entry : name_to_flag)
2440 source_location.add_pragma("checked:" + id2string(entry.first));
2441}
2442
2445{
2446 auto s = id2string(named_check);
2447 auto col = s.find(":");
2448
2449 if(col == std::string::npos)
2450 return {}; // separator not found
2451
2452 auto name = s.substr(col + 1);
2453
2454 if(name_to_flag.find(name) == name_to_flag.end())
2455 return {}; // name unknown
2456
2457 check_statust status;
2458 if(!s.compare(0, 6, "enable"))
2459 status = check_statust::ENABLE;
2460 else if(!s.compare(0, 7, "disable"))
2461 status = check_statust::DISABLE;
2462 else if(!s.compare(0, 7, "checked"))
2463 status = check_statust::CHECKED;
2464 else
2465 return {}; // prefix unknow
2466
2467 // success
2468 return std::pair<irep_idt, check_statust>{name, status};
2469}
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.
optionalt< 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:55
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:240
signedbv_typet pointer_diff_type()
Definition c_types.cpp:225
bitvector_typet char_type()
Definition c_types.cpp:111
Operator to return the address of an object.
Boolean AND.
Definition std_expr.h:2071
const exprt & size() const
Definition std_types.h:796
A base class for binary expressions.
Definition std_expr.h:583
exprt & lhs()
Definition std_expr.h:613
exprt & rhs()
Definition std_expr.h:623
exprt & op0()
Definition expr.h:125
exprt & op1()
Definition expr.h:128
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:676
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:707
std::size_t get_width() const
Definition std_types.h:876
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:1097
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
A Boolean expression returning true, iff the value of an enum-typed symbol equals one of the enum's d...
Definition c_expr.h:326
Equality.
Definition std_expr.h:1306
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:216
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:223
source_locationt & add_source_location()
Definition expr.h:228
Extracts a sub-range of a bit-vector operand.
The Boolean constant false.
Definition std_expr.h:3017
~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...
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.
void memory_leak_check(const irep_idt &function_id)
exprt is_in_bounds_of_some_explicit_allocation(const exprt &pointer, 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.
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)
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...
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
std::list< allocationt > allocationst
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...
const guardt identity
void div_by_zero_check(const div_exprt &, const guardt &)
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 &)
optionalt< std::pair< irep_idt, check_statust > > named_check_statust
optional (named-check, status) pair
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 &)
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...
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".
instructionst::const_iterator const_targett
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.
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:2323
exprt & cond()
Definition std_expr.h:2340
exprt & false_case()
Definition std_expr.h:2360
exprt & true_case()
Definition std_expr.h:2350
Boolean implication.
Definition std_expr.h:2134
Array index operator.
Definition std_expr.h:1410
exprt & index()
Definition std_expr.h:1450
exprt & array()
Definition std_expr.h:1440
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:490
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
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.
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:2794
const exprt & struct_op() const
Definition std_expr.h:2832
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:1168
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition std_expr.h:1188
Binary multiplication Associativity is not specified.
Definition std_expr.h:1052
A base class for multi-ary expressions Associativity is not specified.
Definition std_expr.h:857
exprt & op0()
Definition std_expr.h:877
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().
The NIL expression.
Definition std_expr.h:3026
Boolean negation.
Definition std_expr.h:2278
Disequality.
Definition std_expr.h:1365
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)
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:2179
The plus expression Associativity is not specified.
Definition std_expr.h:947
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)
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:113
const irep_idt & get_identifier() const
Definition std_expr.h:142
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:2017
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:314
const exprt & op() const
Definition std_expr.h:326
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
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#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:47
Abstract interface to support a programming language.
Field-insensitive, location-sensitive bitvector analysis.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition make_unique.h:19
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)
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)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
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 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:63
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:51
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:840
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1478
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition std_expr.h:1217
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition std_expr.h:1077
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2051
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition std_expr.h:1146
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:660
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:986
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:361
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:932
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2403
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition std_expr.h:1031
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition std_expr.h:2159
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition std_expr.h:453
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1060
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:844
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