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/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; diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp index caaf3354c6f..92b6c292599 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,46 @@ 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); + }); + } + + 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)}); + } } } @@ -286,7 +327,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 +348,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); @@ -337,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); @@ -360,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()); } 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