From 95d8d0fd54ee76b55c1c8fba4c17da35b84d10ce Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Mon, 7 May 2018 12:37:05 +0100 Subject: [PATCH 1/3] Generalise option setting from strategy unit tests The check_with_strategy methods previously took an argument to set the `unwind-limit` option with. This commit replaces that argument with a function that mutates the optionst that is passed into it. This can be used for setting `unwind-limit` or any other option from the client. This is in preparation for a new strategy that requires additional options to be set. --- unit/path_strategies.cpp | 46 +++++++++++++++++++--------------------- unit/path_strategies.h | 8 +++---- 2 files changed, 26 insertions(+), 28 deletions(-) diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp index caaf3354c6f..b7698d6276b 100644 --- a/unit/path_strategies.cpp +++ b/unit/path_strategies.cpp @@ -65,6 +65,8 @@ SCENARIO("path strategies") std::string c; GIVEN("a simple conditional program") { + std::function opts_callback = [](optionst &opts) {}; + c = "/* 1 */ int main() \n" "/* 2 */ { \n" @@ -75,28 +77,28 @@ SCENARIO("path strategies") "/* 7 */ x = 0; \n" "/* 8 */ } \n"; - const unsigned unwind_limit = 0U; - check_with_strategy( "lifo", + opts_callback, c, {symex_eventt::resume(symex_eventt::enumt::JUMP, 7), symex_eventt::result(symex_eventt::enumt::SUCCESS), symex_eventt::resume(symex_eventt::enumt::NEXT, 5), - symex_eventt::result(symex_eventt::enumt::SUCCESS)}, - unwind_limit); + symex_eventt::result(symex_eventt::enumt::SUCCESS)}); check_with_strategy( "fifo", + opts_callback, c, {symex_eventt::resume(symex_eventt::enumt::NEXT, 5), symex_eventt::result(symex_eventt::enumt::SUCCESS), symex_eventt::resume(symex_eventt::enumt::JUMP, 7), - symex_eventt::result(symex_eventt::enumt::SUCCESS)}, - unwind_limit); + symex_eventt::result(symex_eventt::enumt::SUCCESS)}); } GIVEN("a program with nested conditionals") { + std::function opts_callback = [](optionst &opts) {}; + c = "/* 1 */ int main() \n" "/* 2 */ { \n" @@ -117,10 +119,9 @@ SCENARIO("path strategies") "/* 17 */ } \n" "/* 18 */ } \n"; - const unsigned unwind_limit = 0U; - check_with_strategy( "lifo", + opts_callback, c, {// Outer else, inner else symex_eventt::resume(symex_eventt::enumt::JUMP, 13), @@ -135,11 +136,11 @@ SCENARIO("path strategies") symex_eventt::result(symex_eventt::enumt::SUCCESS), // Outer if, inner if symex_eventt::resume(symex_eventt::enumt::NEXT, 7), - symex_eventt::result(symex_eventt::enumt::SUCCESS)}, - unwind_limit); + symex_eventt::result(symex_eventt::enumt::SUCCESS)}); check_with_strategy( "fifo", + opts_callback, c, {// Expand outer if, but don't continue depth-first symex_eventt::resume(symex_eventt::enumt::NEXT, 6), @@ -155,12 +156,15 @@ SCENARIO("path strategies") symex_eventt::resume(symex_eventt::enumt::NEXT, 14), symex_eventt::result(symex_eventt::enumt::SUCCESS), symex_eventt::resume(symex_eventt::enumt::JUMP, 16), - symex_eventt::result(symex_eventt::enumt::SUCCESS)}, - unwind_limit); + symex_eventt::result(symex_eventt::enumt::SUCCESS)}); } GIVEN("a loop program to test functional correctness") { + std::function opts_callback = [](optionst &opts) { + opts.set_option("unwind", 2U); + }; + c = "/* 1 */ int main() \n" "/* 2 */ { \n" @@ -173,10 +177,9 @@ SCENARIO("path strategies") "/* 9 */ assert(x); \n" "/* 10 */ } \n"; - const unsigned unwind_limit = 2U; - check_with_strategy( "lifo", + opts_callback, c, { // The path where we skip the loop body. Successful because the path is @@ -194,11 +197,11 @@ SCENARIO("path strategies") // infeasible. symex_eventt::resume(symex_eventt::enumt::NEXT, 7), symex_eventt::result(symex_eventt::enumt::SUCCESS), - }, - unwind_limit); + }); check_with_strategy( "fifo", + opts_callback, c, { // The path where we skip the loop body. Successful because the path is @@ -219,8 +222,7 @@ SCENARIO("path strategies") // executing the loop once, decrementing x to 0; assert(x) should fail. symex_eventt::resume(symex_eventt::enumt::JUMP, 9), symex_eventt::result(symex_eventt::enumt::FAILURE), - }, - unwind_limit); + }); } } @@ -286,7 +288,7 @@ void symex_eventt::validate_resume( void _check_with_strategy( const std::string &strategy, const std::string &program, - const unsigned unwind_limit, + std::function opts_callback, symex_eventt::listt &events) { temporary_filet tmp("path-explore_", ".c"); @@ -307,11 +309,7 @@ void _check_with_strategy( opts.set_option("paths", true); opts.set_option("exploration-strategy", strategy); - if(unwind_limit) - { - opts.set_option("unwind", unwind_limit); - cmdline.set("unwind", std::to_string(unwind_limit)); - } + opts_callback(opts); ui_message_handlert mh(cmdline, "path-explore"); mh.set_verbosity(0); diff --git a/unit/path_strategies.h b/unit/path_strategies.h index c1f4c63c8d1..cc0096095e1 100644 --- a/unit/path_strategies.h +++ b/unit/path_strategies.h @@ -45,18 +45,18 @@ struct symex_eventt void _check_with_strategy( const std::string &strategy, const std::string &program, - const unsigned unwind_limit, + std::function, symex_eventt::listt &events); /// Call this one, not the underscore version void check_with_strategy( const std::string &strategy, + std::function opts_callback, const std::string &program, - symex_eventt::listt events, - const unsigned unwind_limit) + symex_eventt::listt events) { WHEN("strategy is '" + strategy + "'") - _check_with_strategy(strategy, program, unwind_limit, events); + _check_with_strategy(strategy, program, opts_callback, events); } #endif // CPROVER_PATH_STRATEGIES_H From 545bff8273907600b84381b682b68cc853b8cfe0 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Sun, 5 Aug 2018 20:59:14 +0100 Subject: [PATCH 2/3] Add clear() to path exploration worklist Subclasses of path_storaget are now required to implement a clear() method. This is so that if we terminate path exploration early, the worklist can be cleared. This commit facilitates writing tests that ensure that the worklist is empty iff symbolic execution has finished; this should happen naturally if symex runs its course over the entire program, but might not happen if we terminate symex early. This commit is in preparation for a future commit that makes the --stop-on-fail flag terminate symbolic execution early. --- src/goto-symex/path_storage.cpp | 10 ++++++++++ src/goto-symex/path_storage.h | 10 ++++++++++ 2 files changed, 20 insertions(+) diff --git a/src/goto-symex/path_storage.cpp b/src/goto-symex/path_storage.cpp index 58a2498a07d..c4d34b411ce 100644 --- a/src/goto-symex/path_storage.cpp +++ b/src/goto-symex/path_storage.cpp @@ -43,6 +43,11 @@ std::size_t path_lifot::size() const return paths.size(); } +void path_lifot::clear() +{ + paths.clear(); +} + // _____________________________________________________________________________ // path_fifot @@ -69,6 +74,11 @@ std::size_t path_fifot::size() const return paths.size(); } +void path_fifot::clear() +{ + paths.clear(); +} + // _____________________________________________________________________________ // path_strategy_choosert diff --git a/src/goto-symex/path_storage.h b/src/goto-symex/path_storage.h index e5d5120cfea..c0e17991482 100644 --- a/src/goto-symex/path_storage.h +++ b/src/goto-symex/path_storage.h @@ -50,6 +50,14 @@ class path_storaget return private_peek(); } + /// \brief Clear all saved paths + /// + /// This is typically used because we want to terminate symbolic execution + /// early. It doesn't matter too much in terms of memory usage since CBMC + /// typically exits soon after we do that, however it's nice to have tests + /// that check that the worklist is always empty when symex finishes. + virtual void clear() = 0; + /// \brief Add paths to resume to the storage /// /// Symbolic execution is suspended when we reach a conditional goto @@ -90,6 +98,7 @@ class path_lifot : public path_storaget public: void push(const patht &, const patht &) override; std::size_t size() const override; + void clear() override; protected: std::list::iterator last_peeked; @@ -106,6 +115,7 @@ class path_fifot : public path_storaget public: void push(const patht &, const patht &) override; std::size_t size() const override; + void clear() override; protected: std::list paths; From 424ab4f18f5591ac690591272ad3a6e2bcf93c4c Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Thu, 2 Aug 2018 18:21:11 +0100 Subject: [PATCH 3/3] --stop-on-fail now stops on failed path When doing path exploration, one sometimes wants CBMC to halt symbolic execution as soon as it encounters a single bug, rather than continuing to explore the program for all bugs. This behaviour can now be enabled by passing the --stop-on-fail flag together with the --paths flag. Prior to this commit, the --stop-on-fail flag --- which was written with model-checking rather than path exploration in mind --- would explore all paths, but only print out a single failed property, which isn't terribly useful because it uses just as much time as printing out all properties. This commit makes this flag more useful when used in conjunction with --paths, while not changing its behaviour for model checking. --- src/cbmc/bmc.cpp | 18 ++++++++++++++ unit/path_strategies.cpp | 53 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 71 insertions(+) diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index fc0bea1efa4..0fbc50aaa15 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -588,6 +588,15 @@ int bmct::do_language_agnostic_bmc( if(driver_configure_bmc) driver_configure_bmc(bmc, symbol_table); tmp_result = bmc.run(model); + + if( + tmp_result == safety_checkert::resultt::UNSAFE && + opts.get_bool_option("stop-on-fail") && opts.is_set("paths")) + { + worklist->clear(); + return CPROVER_EXIT_VERIFICATION_UNSAFE; + } + if(tmp_result != safety_checkert::resultt::PAUSED) final_result = tmp_result; } @@ -637,6 +646,15 @@ int bmct::do_language_agnostic_bmc( if(driver_configure_bmc) driver_configure_bmc(pe, symbol_table); tmp_result = pe.run(model); + + if( + tmp_result == safety_checkert::resultt::UNSAFE && + opts.get_bool_option("stop-on-fail") && opts.is_set("paths")) + { + worklist->clear(); + return CPROVER_EXIT_VERIFICATION_UNSAFE; + } + if(tmp_result != safety_checkert::resultt::PAUSED) final_result &= tmp_result; worklist->pop(); diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp index b7698d6276b..92b6c292599 100644 --- a/unit/path_strategies.cpp +++ b/unit/path_strategies.cpp @@ -224,6 +224,45 @@ SCENARIO("path strategies") symex_eventt::result(symex_eventt::enumt::FAILURE), }); } + + GIVEN("program to check for stop-on-fail with path exploration") + { + std::function halt_callback = [](optionst &opts) { + opts.set_option("stop-on-fail", true); + }; + std::function no_halt_callback = [](optionst &opts) {}; + + c = + "/* 1 */ int main() \n" + "/* 2 */ { \n" + "/* 3 */ int x, y; \n" + "/* 4 */ if(x) \n" + "/* 5 */ assert(0); \n" + "/* 6 */ else \n" + "/* 7 */ assert(0); \n" + "/* 8 */ } \n"; + + GIVEN("no stopping on failure") + { + check_with_strategy( + "lifo", + no_halt_callback, + c, + {symex_eventt::resume(symex_eventt::enumt::JUMP, 7), + symex_eventt::result(symex_eventt::enumt::FAILURE), + symex_eventt::resume(symex_eventt::enumt::NEXT, 5), + symex_eventt::result(symex_eventt::enumt::FAILURE)}); + } + GIVEN("stopping on failure") + { + check_with_strategy( + "lifo", + halt_callback, + c, + {symex_eventt::resume(symex_eventt::enumt::JUMP, 7), + symex_eventt::result(symex_eventt::enumt::FAILURE)}); + } + } } // In theory, there should be no need to change the code below when adding new @@ -335,6 +374,13 @@ void _check_with_strategy( safety_checkert::resultt result = bmc.run(gm); symex_eventt::validate_result(events, result); + if( + result == safety_checkert::resultt::UNSAFE && + opts.get_bool_option("stop-on-fail") && opts.is_set("paths")) + { + worklist->clear(); + } + while(!worklist->empty()) { cbmc_solverst solvers(opts, gm.get_symbol_table(), mh); @@ -358,6 +404,13 @@ void _check_with_strategy( symex_eventt::validate_result(events, result); worklist->pop(); + + if( + result == safety_checkert::resultt::UNSAFE && + opts.get_bool_option("stop-on-fail")) + { + worklist->clear(); + } } REQUIRE(events.empty()); }