diff --git a/regression/contracts/no_redudant_checks/main.c b/regression/contracts/no_redudant_checks/main.c new file mode 100644 index 00000000000..63377b4f588 --- /dev/null +++ b/regression/contracts/no_redudant_checks/main.c @@ -0,0 +1,9 @@ +#include +const int N = 100; +int main() +{ + int *buf = malloc(N * sizeof(*buf)); + char *lb = (((char *)buf) - __CPROVER_POINTER_OFFSET(buf)); + char *ub = (((char *)buf) - __CPROVER_POINTER_OFFSET(buf)) + + __CPROVER_OBJECT_SIZE(buf) - 1; +} diff --git a/regression/contracts/no_redudant_checks/test.desc b/regression/contracts/no_redudant_checks/test.desc new file mode 100644 index 00000000000..c2100ee2a71 --- /dev/null +++ b/regression/contracts/no_redudant_checks/test.desc @@ -0,0 +1,42 @@ +CORE +main.c +--pointer-overflow-check _ --pointer-overflow-check --unsigned-overflow-check +^EXIT=0$ +^SIGNAL=0$ +^\[malloc.assertion.1\].*: SUCCESS +^\[malloc.assertion.2\].*: SUCCESS +^\[main.overflow.1\].*: SUCCESS +^\[main.pointer_arithmetic.1\].*: SUCCESS +^\[main.pointer_arithmetic.2\].*: SUCCESS +^\[main.pointer_arithmetic.3\].*: SUCCESS +^\[main.pointer_arithmetic.4\].*: SUCCESS +^\[main.pointer_arithmetic.5\].*: SUCCESS +^\[main.pointer_arithmetic.6\].*: SUCCESS +^\[main.pointer_arithmetic.7\].*: SUCCESS +^\[main.pointer_arithmetic.8\].*: SUCCESS +^\[main.pointer_arithmetic.9\].*: SUCCESS +^\[main.pointer_arithmetic.10\].*: SUCCESS +^\[main.pointer_arithmetic.11\].*: SUCCESS +^\[main.pointer_arithmetic.12\].*: SUCCESS +^\[main.pointer_arithmetic.13\].*: SUCCESS +^\[main.pointer_arithmetic.14\].*: SUCCESS +^\[main.pointer_arithmetic.15\].*: SUCCESS +^\[main.pointer_arithmetic.16\].*: SUCCESS +^\[main.pointer_arithmetic.17\].*: SUCCESS +^\*\* 0 of 20 failed \(1 iterations\) +^VERIFICATION SUCCESSFUL$ +-- +^\[main.overflow.\d+\].*: FAILURE +-- +Checks that assertions generated by the first --pointer-overflow-check: +- do not get duplicated by the second --unsigned-overflow-check +- do not get instrumented with --unsigned-overflow-check (would fail the proof) + +We expect 20 assertions to be generated: +In the goto-instrument run: +- 2 for using malloc +- 17 caused by --pointer-overflow-check + +In the final cbmc run: +- 0 caused by --pointer-overflow-check +- 1 caused by the --unsigned-overflow-check diff --git a/src/analyses/goto_check_c.cpp b/src/analyses/goto_check_c.cpp index cc9707a42fd..522dc53dac8 100644 --- a/src/analyses/goto_check_c.cpp +++ b/src/analyses/goto_check_c.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_check_c.h" #include +#include #include #include @@ -278,6 +279,22 @@ class goto_check_ct bool enable_assumptions; bool enable_pointer_primitive_check; + /// Maps a named-check name to the corresponding boolean flag. + std::map name_to_flag{ + {"bounds-check", &enable_bounds_check}, + {"pointer-check", &enable_pointer_check}, + {"memory-leak-check", &enable_memory_leak_check}, + {"div-by-zero-check", &enable_div_by_zero_check}, + {"enum-range-check", &enable_enum_range_check}, + {"signed-overflow-check", &enable_signed_overflow_check}, + {"unsigned-overflow-check", &enable_unsigned_overflow_check}, + {"pointer-overflow-check", &enable_pointer_overflow_check}, + {"conversion-check", &enable_conversion_check}, + {"undefined-shift-check", &enable_undefined_shift_check}, + {"float-overflow-check", &enable_float_overflow_check}, + {"nan-check", &enable_nan_check}, + {"pointer-primitive-check", &enable_pointer_primitive_check}}; + typedef optionst::value_listt error_labelst; error_labelst error_labels; @@ -288,6 +305,36 @@ class goto_check_ct allocationst allocations; irep_idt mode; + + /// \brief Adds "checked" pragmas for all currently active named checks + /// on the given source location. + void add_active_named_check_pragmas(source_locationt &source_location) const; + + /// \brief Adds "disable" pragmas for all named checks + /// on the given source location. + void + add_all_disable_named_check_pragmas(source_locationt &source_location) const; + + /// activation statuses for named checks + typedef enum + { + ENABLE, + DISABLE, + CHECKED + } check_statust; + + /// optional (named-check, status) pair + using named_check_statust = optionalt>; + + /// Matches a named-check string of the form + /// + /// ``` + /// ("enable"|"disable"|"checked") ":" + /// ``` + /// + /// \returns a pair (name, status) if the match succeeds + /// and the name is known, nothing otherwise. + named_check_statust match_named_check(const irep_idt &named_check) const; }; void goto_check_ct::collect_allocations(const goto_functionst &goto_functions) @@ -1566,6 +1613,8 @@ void goto_check_ct::add_guarded_property( t->source_location_nonconst().set_comment( comment + " in " + source_expr_string); t->source_location_nonconst().set_property_class(property_class); + + add_all_disable_named_check_pragmas(t->source_location_nonconst()); } } @@ -1840,11 +1889,13 @@ optionalt goto_check_ct::rw_ok_check(exprt expr) return {}; } -/// \brief Set a Boolean flag to a new value (via `set_flag`) and restore -/// the previous value when the entire object goes out of scope. +/// Allows to: +/// - override a Boolean flag with a new value via `set_flag` +/// - set a Boolean flag to false via `disable_flag`, such that +/// previous `set_flag` are overridden and future `set_flag` are ignored. /// -/// \remarks Calls to set_value are tracked to allow detecting doubles sets -/// with different values and trigger an INVARIANT. +/// A flag's initial value (before any `set_flag` or `disable_flag`) is restored +/// when the entire object goes out of scope. class flag_resett { public: @@ -1856,24 +1907,50 @@ class flag_resett /// \brief Store the current value of \p flag and /// then set its value to \p new_value. /// - /// \remarks an INVARIANT triggers iff the flag is set - /// more than once with different values. + /// - calling `set_flag` after `disable_flag` is a no-op + /// - calling `set_flag` twice triggers an INVARIANT void set_flag(bool &flag, bool new_value, const irep_idt &flag_name) { - bool seen = flags_to_reset.find(&flag) != flags_to_reset.end(); + // make this a no-op if the flag is disabled + if(disabled_flags.find(&flag) != disabled_flags.end()) + return; + + // detect double sets INVARIANT( - !(seen && flag != new_value), - "Flag " + id2string(flag_name) + - " set twice with incompatible values " - " at \n" + + flags_to_reset.find(&flag) == flags_to_reset.end(), + "Flag " + id2string(flag_name) + " set twice at \n" + instruction.source_location().pretty()); if(flag != new_value) { - flags_to_reset.emplace(&flag, flag); + flags_to_reset[&flag] = flag; flag = new_value; } } + /// Sets the given flag to false, overriding any previous value. + /// + /// - calling `disable_flag` after `set_flag` overrides the set value + /// - calling `disable_flag` twice triggers an INVARIANT + void disable_flag(bool &flag, const irep_idt &flag_name) + { + INVARIANT( + disabled_flags.find(&flag) == disabled_flags.end(), + "Flag " + id2string(flag_name) + " disabled twice at \n" + + instruction.source_location().pretty()); + + disabled_flags.insert(&flag); + + // If the flag has not already been set, + // we store its current value in the reset map. + // Otherwise, the reset map already holds + // the initial value we want to reset it to, keep it as is. + if(flags_to_reset.find(&flag) == flags_to_reset.end()) + flags_to_reset[&flag] = flag; + + // set the flag to false in all cases. + flag = false; + } + /// \brief Restore the values of all flags that have been /// modified via `set_flag`. ~flag_resett() @@ -1885,6 +1962,7 @@ class flag_resett private: const goto_programt::instructiont &instruction; std::map flags_to_reset; + std::set disabled_flags; }; void goto_check_ct::goto_check( @@ -1915,60 +1993,32 @@ void goto_check_ct::goto_check( const auto &pragmas = i.source_location().get_pragmas(); for(const auto &d : pragmas) { - if(d.first == "disable:bounds-check") - resetter.set_flag(enable_bounds_check, false, d.first); - else if(d.first == "disable:pointer-check") - resetter.set_flag(enable_pointer_check, false, d.first); - else if(d.first == "disable:memory-leak-check") - resetter.set_flag(enable_memory_leak_check, false, d.first); - else if(d.first == "disable:div-by-zero-check") - resetter.set_flag(enable_div_by_zero_check, false, d.first); - else if(d.first == "disable:enum-range-check") - resetter.set_flag(enable_enum_range_check, false, d.first); - else if(d.first == "disable:signed-overflow-check") - resetter.set_flag(enable_signed_overflow_check, false, d.first); - else if(d.first == "disable:unsigned-overflow-check") - resetter.set_flag(enable_unsigned_overflow_check, false, d.first); - else if(d.first == "disable:pointer-overflow-check") - resetter.set_flag(enable_pointer_overflow_check, false, d.first); - else if(d.first == "disable:float-overflow-check") - resetter.set_flag(enable_float_overflow_check, false, d.first); - else if(d.first == "disable:conversion-check") - resetter.set_flag(enable_conversion_check, false, d.first); - else if(d.first == "disable:undefined-shift-check") - resetter.set_flag(enable_undefined_shift_check, false, d.first); - else if(d.first == "disable:nan-check") - resetter.set_flag(enable_nan_check, false, d.first); - else if(d.first == "disable:pointer-primitive-check") - resetter.set_flag(enable_pointer_primitive_check, false, d.first); - else if(d.first == "enable:bounds-check") - resetter.set_flag(enable_bounds_check, true, d.first); - else if(d.first == "enable:pointer-check") - resetter.set_flag(enable_pointer_check, true, d.first); - else if(d.first == "enable:memory_leak-check") - resetter.set_flag(enable_memory_leak_check, true, d.first); - else if(d.first == "enable:div-by-zero-check") - resetter.set_flag(enable_div_by_zero_check, true, d.first); - else if(d.first == "enable:enum-range-check") - resetter.set_flag(enable_enum_range_check, true, d.first); - else if(d.first == "enable:signed-overflow-check") - resetter.set_flag(enable_signed_overflow_check, true, d.first); - else if(d.first == "enable:unsigned-overflow-check") - resetter.set_flag(enable_unsigned_overflow_check, true, d.first); - else if(d.first == "enable:pointer-overflow-check") - resetter.set_flag(enable_pointer_overflow_check, true, d.first); - else if(d.first == "enable:float-overflow-check") - resetter.set_flag(enable_float_overflow_check, true, d.first); - else if(d.first == "enable:conversion-check") - resetter.set_flag(enable_conversion_check, true, d.first); - else if(d.first == "enable:undefined-shift-check") - resetter.set_flag(enable_undefined_shift_check, true, d.first); - else if(d.first == "enable:nan-check") - resetter.set_flag(enable_nan_check, true, d.first); - else if(d.first == "enable:pointer-primitive-check") - resetter.set_flag(enable_pointer_primitive_check, true, d.first); + // match named-check related pragmas + auto matched = match_named_check(d.first); + if(matched.has_value()) + { + auto named_check = matched.value(); + auto name = named_check.first; + auto status = named_check.second; + bool *flag = name_to_flag.find(name)->second; + switch(status) + { + case check_statust::ENABLE: + resetter.set_flag(*flag, true, name); + break; + case check_statust::DISABLE: + resetter.set_flag(*flag, false, name); + break; + case check_statust::CHECKED: + resetter.disable_flag(*flag, name); + break; + } + } } + // add checked pragmas for all active checks + add_active_named_check_pragmas(i.source_location_nonconst()); + new_code.clear(); // we clear all recorded assertions if @@ -2398,3 +2448,46 @@ void goto_check_c( const namespacet ns(goto_model.symbol_table); goto_check_c(ns, options, goto_model.goto_functions, message_handler); } + +void goto_check_ct::add_active_named_check_pragmas( + source_locationt &source_location) const +{ + for(const auto &entry : name_to_flag) + if(*(entry.second)) + source_location.add_pragma("checked:" + id2string(entry.first)); +} + +void goto_check_ct::add_all_disable_named_check_pragmas( + source_locationt &source_location) const +{ + for(const auto &entry : name_to_flag) + source_location.add_pragma("disable:" + id2string(entry.first)); +} + +goto_check_ct::named_check_statust +goto_check_ct::match_named_check(const irep_idt &named_check) const +{ + auto s = id2string(named_check); + auto col = s.find(":"); + + if(col == std::string::npos) + return {}; // separator not found + + auto name = s.substr(col + 1); + + if(name_to_flag.find(name) == name_to_flag.end()) + return {}; // name unknown + + check_statust status; + if(!s.compare(0, 6, "enable")) + status = check_statust::ENABLE; + else if(!s.compare(0, 7, "disable")) + status = check_statust::DISABLE; + else if(!s.compare(0, 7, "checked")) + status = check_statust::CHECKED; + else + return {}; // prefix unknow + + // success + return std::pair{name, status}; +}