From 88bb4cc3f27ec72ad32cf9dbc8d3824e9bdf623d Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 16 Aug 2024 18:59:53 -0400 Subject: [PATCH] CONTRACTS: redirect checks to outer write set for loops that get skipped --- .../skip_loop_instrumentation/harness.c | 29 +++++++++++++++++++ .../skip_loop_instrumentation/test.desc | 11 +++++++ .../dynamic-frames/dfcc_cfg_info.cpp | 19 +++++++++++- .../contracts/dynamic-frames/dfcc_cfg_info.h | 18 +++++++++++- .../dynamic-frames/dfcc_instrument.cpp | 2 +- 5 files changed, 76 insertions(+), 3 deletions(-) create mode 100644 regression/contracts-dfcc/skip_loop_instrumentation/harness.c create mode 100644 regression/contracts-dfcc/skip_loop_instrumentation/test.desc diff --git a/regression/contracts-dfcc/skip_loop_instrumentation/harness.c b/regression/contracts-dfcc/skip_loop_instrumentation/harness.c new file mode 100644 index 00000000000..1fa7a0380bf --- /dev/null +++ b/regression/contracts-dfcc/skip_loop_instrumentation/harness.c @@ -0,0 +1,29 @@ +int global; + +int harness(int argc) +{ + global = 0; + 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..63e4d593a43 --- /dev/null +++ b/regression/contracts-dfcc/skip_loop_instrumentation/test.desc @@ -0,0 +1,11 @@ +CORE +harness.c --function harness +--dfcc harness --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. \ No newline at end of file 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 69073bbc192..d553afa0c2b 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp @@ -640,6 +640,18 @@ 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())); +} + +#include const exprt & dfcc_cfg_infot::get_write_set(goto_programt::const_targett target) const { @@ -647,7 +659,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; @@ -746,6 +758,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 { 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 3cbd23551a6..3a628c924fa 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,10 @@ 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 +327,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 34e3f44a2b7..ac0b419965d 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp @@ -1254,7 +1254,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