diff --git a/regression/contracts-dfcc/loop_contracts_do_while/nested.desc b/regression/contracts-dfcc/loop_contracts_do_while/nested.desc index 20cdc6fa135..7a2ee1640c7 100644 --- a/regression/contracts-dfcc/loop_contracts_do_while/nested.desc +++ b/regression/contracts-dfcc/loop_contracts_do_while/nested.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE nested.c --dfcc main --apply-loop-contracts ^EXIT=0$ @@ -6,4 +6,4 @@ nested.c ^VERIFICATION SUCCESSFUL$ -- -- -We spuriously report that x is not assignable. +We properly skip the instrumentation of both loops. diff --git a/regression/contracts-dfcc/loop_contracts_reject_loops_two_latches/test.desc b/regression/contracts-dfcc/loop_contracts_reject_loops_two_latches/test.desc index 044656dbb72..cda8a3f88b7 100644 --- a/regression/contracts-dfcc/loop_contracts_reject_loops_two_latches/test.desc +++ b/regression/contracts-dfcc/loop_contracts_reject_loops_two_latches/test.desc @@ -1,10 +1,11 @@ CORE dfcc-only main.c --dfcc main --apply-loop-contracts -^EXIT=10$ +^EXIT=0$ ^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ -- -^Found loop with more than one latch instruction$ -- This test checks that our loop contract instrumentation first transforms loops -so as to only have a single loop latch. +so as to only have a single loop latch, and skips instrumentation if the result +has no contract. diff --git a/regression/contracts-dfcc/skip_loop_instrumentation/across_functions.c b/regression/contracts-dfcc/skip_loop_instrumentation/across_functions.c new file mode 100644 index 00000000000..aa9ea806443 --- /dev/null +++ b/regression/contracts-dfcc/skip_loop_instrumentation/across_functions.c @@ -0,0 +1,25 @@ +int foo() +{ + int x = 0; + while(x < 10) + { + ++x; + } + return x; +} + +int main() +{ + int x = 0; + + for(int i = 0; i < 10; ++i) + __CPROVER_loop_invariant(0 <= x && x <= 10) + { + if(x < 10) + x++; + } + + x += foo(); + + __CPROVER_assert(x <= 20, ""); +} diff --git a/regression/contracts-dfcc/skip_loop_instrumentation/across_functions.desc b/regression/contracts-dfcc/skip_loop_instrumentation/across_functions.desc new file mode 100644 index 00000000000..4491463a9a4 --- /dev/null +++ b/regression/contracts-dfcc/skip_loop_instrumentation/across_functions.desc @@ -0,0 +1,11 @@ +CORE +across_functions.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +This test case checks that when instrumentation of any look is skipped, we +redirect write set checks to the parent write set. diff --git a/regression/contracts-dfcc/skip_loop_instrumentation/main.c b/regression/contracts-dfcc/skip_loop_instrumentation/main.c new file mode 100644 index 00000000000..530f789df68 --- /dev/null +++ b/regression/contracts-dfcc/skip_loop_instrumentation/main.c @@ -0,0 +1,29 @@ +int global; + +int main() +{ + global = 0; + int argc = 1; + do + { + int local; + global = 1; + local = 1; + for(int i = 0; i < 1; i++) + { + local = 1; + global = 2; + int j = 0; + while(j < 1) + { + local = 1; + global = 3; + j++; + } + __CPROVER_assert(global == 3, "case3"); + } + __CPROVER_assert(global == 3, "case3"); + } while(0); + __CPROVER_assert(global == 3, "case1"); + return 0; +} diff --git a/regression/contracts-dfcc/skip_loop_instrumentation/test.desc b/regression/contracts-dfcc/skip_loop_instrumentation/test.desc new file mode 100644 index 00000000000..95c27f84234 --- /dev/null +++ b/regression/contracts-dfcc/skip_loop_instrumentation/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +This test case checks that when the instrumentation of nested loops is skipped, we redirect the write set checks to the +outer write set. diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp index 40b4495f0bf..b5c607ed7d9 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp @@ -70,8 +70,6 @@ std::string invalid_function_contract_pair_exceptiont::what() const return res; } -#include - static std::pair parse_function_contract_pair(const irep_idt &cli_flag) { diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp index 97b632cbb70..d47e1574d90 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp @@ -628,6 +628,17 @@ void dfcc_cfg_infot::output(std::ostream &out) const } } +std::size_t dfcc_cfg_infot::get_first_id_not_skipped_or_top_level_id( + const std::size_t loop_id) const +{ + if(is_top_level_id(loop_id) || !get_loop_info(loop_id).must_skip()) + { + return loop_id; + } + return get_first_id_not_skipped_or_top_level_id( + get_outer_loop_identifier(loop_id).value_or(top_level_id())); +} + const exprt & dfcc_cfg_infot::get_write_set(goto_programt::const_targett target) const { @@ -635,7 +646,7 @@ dfcc_cfg_infot::get_write_set(goto_programt::const_targett target) const PRECONDITION( loop_id_opt.has_value() && is_valid_loop_or_top_level_id(loop_id_opt.value())); - auto loop_id = loop_id_opt.value(); + auto loop_id = get_first_id_not_skipped_or_top_level_id(loop_id_opt.value()); if(is_top_level_id(loop_id)) { return top_level_write_set; @@ -734,6 +745,11 @@ bool dfcc_cfg_infot::is_top_level_id(const std::size_t id) const return id == loop_info_map.size(); } +size_t dfcc_cfg_infot::top_level_id() const +{ + return loop_info_map.size(); +} + bool dfcc_cfg_infot::must_track_decl_or_dead( goto_programt::const_targett target) const { @@ -743,7 +759,6 @@ bool dfcc_cfg_infot::must_track_decl_or_dead( auto &tracked = get_tracked_set(target); return tracked.find(ident) != tracked.end(); } -#include /// Returns true if the lhs to an assignment must be checked against its write /// set. The set of locally declared identifiers and the subset of that that diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h index ea4e819a5d2..8de5666a6b7 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h @@ -144,6 +144,13 @@ class dfcc_loop_infot /// this loop. This is the one that must be passed as argument to write set /// functions. const symbol_exprt addr_of_write_set_var; + + /// Returns true if the loop has no invariant and no decreases clause + /// and its instrumentation must be skipped. + const bool must_skip() const + { + return invariant.is_nil() && decreases.empty(); + } }; /// Computes natural loops, enforces normal form conditions, computes the @@ -248,7 +255,9 @@ class dfcc_cfg_infot /// \brief Returns the loop info for that loop_id. const dfcc_loop_infot &get_loop_info(const std::size_t loop_id) const; - /// \brief Returns the write set variable for that instruction. + /// \brief Returns the write set variable to use for the given instruction + /// Returns the write set for the loop, or one of the outer loops, + /// or top level, passing through all loops that are [must_skip] const exprt &get_write_set(goto_programt::const_targett target) const; /// \brief Returns the set of local variable for the scope where that @@ -270,6 +279,11 @@ class dfcc_cfg_infot return topsorted_loops; } + /// \brief Returns the id of the first outer loop (including this one) that + /// is not skipped, or the top level id. + std::size_t + get_first_id_not_skipped_or_top_level_id(const std::size_t loop_id) const; + /// Finds the DFCC id of the loop that contains the given loop, returns /// nullopt when the loop has no outer loop. const std::optional @@ -314,6 +328,9 @@ class dfcc_cfg_infot /// True iff \p id is in the valid range for a loop id for this function. bool is_top_level_id(const std::size_t id) const; + /// Returns the top level ID + size_t top_level_id() const; + /// Loop identifiers sorted from most deeply nested to less deeply nested std::vector topsorted_loops; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp index 707feaedffd..b37d6a7c55c 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp @@ -1239,7 +1239,7 @@ void dfcc_instrumentt::apply_loop_contracts( for(const auto &loop_id : cfg_info.get_loops_toposorted()) { const auto &loop = cfg_info.get_loop_info(loop_id); - if(loop.invariant.is_nil() && loop.decreases.empty()) + if(loop.must_skip()) { // skip loops that do not have contracts log.warning() << "loop " << function_id << "." << loop.cbmc_loop_id