From 4e25501687968517f102f5204a74a8927a845be9 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Thu, 25 Oct 2018 15:37:06 +0100 Subject: [PATCH 1/3] More useful output on path strategy unit tests The path strategy unit tests now emit an index showing which result in the expected list of results was the one that failed. --- unit/path_strategies.cpp | 28 ++++++++++++++++++++-------- unit/path_strategies.h | 9 ++++++--- 2 files changed, 26 insertions(+), 11 deletions(-) diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp index d4b07f67ed4..683f7cf0ee1 100644 --- a/unit/path_strategies.cpp +++ b/unit/path_strategies.cpp @@ -272,12 +272,14 @@ SCENARIO("path strategies") void symex_eventt::validate_result( listt &events, - const safety_checkert::resultt result) + const safety_checkert::resultt result, + std::size_t &counter) { INFO( "Expecting result to be '" << (result == safety_checkert::resultt::SAFE ? "success" : "failure") - << "'"); + << "' (item at index [" << counter << "] in expected results list"); + ++counter; REQUIRE(result != safety_checkert::resultt::ERROR); @@ -297,7 +299,8 @@ void symex_eventt::validate_result( void symex_eventt::validate_resume( listt &events, - const goto_symex_statet &state) + const goto_symex_statet &state, + std::size_t &counter) { REQUIRE(!events.empty()); @@ -305,17 +308,24 @@ void symex_eventt::validate_resume( if(state.has_saved_jump_target) { - INFO("Expecting resume to be 'jump' to line " << dst); + INFO( + "Expecting resume to be 'jump' to line " + << dst << " (item at index [" << counter + << "] in expected resumes list)"); REQUIRE(events.front().first == symex_eventt::enumt::JUMP); } else if(state.has_saved_next_instruction) { - INFO("Expecting resume to be 'next' to line " << dst); + INFO( + "Expecting resume to be 'next' to line " + << dst << " (item at index [" << counter + << "] in expected resumes list)"); REQUIRE(events.front().first == symex_eventt::enumt::NEXT); } else REQUIRE(false); + ++counter; REQUIRE(events.front().second == dst); events.pop_front(); @@ -372,7 +382,9 @@ void _check_with_strategy( bmct bmc(opts, gm.get_symbol_table(), mh, pc, *worklist, callback); safety_checkert::resultt result = bmc.run(gm); - symex_eventt::validate_result(events, result); + + std::size_t expected_results_cnt = 0; + symex_eventt::validate_result(events, result, expected_results_cnt); if( result == safety_checkert::resultt::UNSAFE && @@ -388,7 +400,7 @@ void _check_with_strategy( prop_convt &pc = cbmc_solver->prop_conv(); path_storaget::patht &resume = worklist->peek(); - symex_eventt::validate_resume(events, resume.state); + symex_eventt::validate_resume(events, resume.state, expected_results_cnt); path_explorert pe( opts, @@ -401,7 +413,7 @@ void _check_with_strategy( callback); result = pe.run(gm); - symex_eventt::validate_result(events, result); + symex_eventt::validate_result(events, result, expected_results_cnt); worklist->pop(); if( diff --git a/unit/path_strategies.h b/unit/path_strategies.h index cc0096095e1..c9537896194 100644 --- a/unit/path_strategies.h +++ b/unit/path_strategies.h @@ -36,10 +36,13 @@ struct symex_eventt return pairt(kind, -1); } - static void - validate_result(listt &events, const safety_checkert::resultt result); + static void validate_result( + listt &events, + const safety_checkert::resultt result, + std::size_t &); - static void validate_resume(listt &events, const goto_symex_statet &state); + static void + validate_resume(listt &events, const goto_symex_statet &state, std::size_t &); }; void _check_with_strategy( From c05a30f5f2c517bf66339a38a45ca26ba1d3a4d7 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Thu, 25 Oct 2018 17:47:25 +0100 Subject: [PATCH 2/3] Make bmct::report_{success,failure} static This is in preparation for a future commit, where the static method do_language_agnostic_bmc will need to make a final report after all paths have been exhausted. These methods were previously marked as virtual, so the zero-parameter non-static variants of these methods have been kept as a convenience; they do nothing other than call into the static variant. --- src/cbmc/bmc.cpp | 26 ++++++++++++++++++-------- src/cbmc/bmc.h | 3 +++ 2 files changed, 21 insertions(+), 8 deletions(-) diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index e2f8584b9e4..c4fc947ba16 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -153,9 +153,14 @@ bmct::run_decision_procedure(prop_convt &prop_conv) void bmct::report_success() { - result() << bold << "VERIFICATION SUCCESSFUL" << reset << eom; + report_success(*this, ui_message_handler); +} - switch(ui_message_handler.get_ui()) +void bmct::report_success(messaget &log, ui_message_handlert &handler) +{ + log.result() << log.bold << "VERIFICATION SUCCESSFUL" << log.reset << log.eom; + + switch(handler.get_ui()) { case ui_message_handlert::uit::PLAIN: break; @@ -164,7 +169,7 @@ void bmct::report_success() { xmlt xml("cprover-status"); xml.data="SUCCESS"; - result() << xml; + log.result() << xml; } break; @@ -172,7 +177,7 @@ void bmct::report_success() { json_objectt json_result; json_result["cProverStatus"]=json_stringt("success"); - result() << json_result; + log.result() << json_result; } break; } @@ -180,9 +185,14 @@ void bmct::report_success() void bmct::report_failure() { - result() << bold << "VERIFICATION FAILED" << reset << eom; + report_failure(*this, ui_message_handler); +} - switch(ui_message_handler.get_ui()) +void bmct::report_failure(messaget &log, ui_message_handlert &handler) +{ + log.result() << log.bold << "VERIFICATION FAILED" << log.reset << log.eom; + + switch(handler.get_ui()) { case ui_message_handlert::uit::PLAIN: break; @@ -191,7 +201,7 @@ void bmct::report_failure() { xmlt xml("cprover-status"); xml.data="FAILURE"; - result() << xml; + log.result() << xml; } break; @@ -199,7 +209,7 @@ void bmct::report_failure() { json_objectt json_result; json_result["cProverStatus"]=json_stringt("failure"); - result() << json_result; + log.result() << json_result; } break; } diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index 261b77c96a3..6ff7f937c2a 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -208,6 +208,9 @@ class bmct:public safety_checkert virtual void report_success(); virtual void report_failure(); + static void report_success(messaget &, ui_message_handlert &); + static void report_failure(messaget &, ui_message_handlert &); + virtual void error_trace(); void output_graphml(resultt result); From 5099467b0cf44ff93a7d11af1fe332ef4a3d0e59 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Thu, 25 Oct 2018 17:54:18 +0100 Subject: [PATCH 3/3] Only safety-check paths when new VCCs get added CBMC will no longer bother running safety checks on path segments that did not generate any new VCCs when running in path-exploration mode. A "path segment" is a list of instructions between two program branch points. CBMC would previously pause symbolic execution and run safety checks at every branch point, which is wasteful when no additional VCCs have been generated since the last pause. As of this commit, CBMC will check to see if new VCCs have been added, and only do the safety check if so. To support this, the new member goto_symext::path_segment_vccs records the number of VCCs that were newly generated along this path segment. It differs from the VCC counters in goto_symex_statet, which hold the number of VCCs generated along the current path since the start of the program. goto_symext objects are minted for each path segment, so they don't hold any information about the VCCs previously along the path. This commit also removes the "Starting new path" output, since this no longer makes much sense. On the other hand, there is an additional final status output; CBMC will report failure after the entire program has been explored if even a single path contained a failing assertion, and report success otherwise. The unit tests have been updated to reflect the fact that CBMC no longer emits "SUCCESS" at each branch point and at the end of paths, and also that CBMC makes one final report of the program safety as a whole. This commit fixes #2684. --- src/cbmc/bmc.cpp | 36 +++++++++++++--------- src/goto-programs/safety_checker.h | 10 ------ src/goto-symex/goto_symex.h | 13 ++++++++ src/goto-symex/symex_main.cpp | 1 + unit/path_strategies.cpp | 49 +++++++++++++++++++----------- 5 files changed, 68 insertions(+), 41 deletions(-) diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index c4fc947ba16..7330a2dcbbc 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -270,9 +270,6 @@ safety_checkert::resultt bmct::execute( const goto_functionst &goto_functions = goto_model.get_goto_functions(); - if(symex.should_pause_symex) - return safety_checkert::resultt::PAUSED; - // This provides the driver program the opportunity to do things like a // symbol-table or goto-functions dump instead of actually running the // checker, like show-vcc except driver-program specific. @@ -282,9 +279,14 @@ safety_checkert::resultt bmct::execute( if(driver_callback_after_symex && driver_callback_after_symex()) return safety_checkert::resultt::SAFE; // to indicate non-error - // add a partial ordering, if required if(equation.has_threads()) { + // When doing path exploration in a concurrent setting, we should avoid + // model-checking the program until we reach the end of a path. + if(symex.should_pause_symex) + return safety_checkert::resultt::PAUSED; + + // add a partial ordering, if required memory_model->set_message_handler(get_message_handler()); (*memory_model)(equation); } @@ -328,6 +330,8 @@ safety_checkert::resultt bmct::execute( !options.get_bool_option("program-only") && symex.get_remaining_vccs() == 0) { + if(options.is_set("paths")) + return safety_checkert::resultt::PAUSED; report_success(); output_graphml(resultt::SAFE); return safety_checkert::resultt::SAFE; @@ -339,7 +343,10 @@ safety_checkert::resultt bmct::execute( return safety_checkert::resultt::SAFE; } - return decide(goto_functions, prop_conv); + if(!options.is_set("paths") || symex.path_segment_vccs > 0) + return decide(goto_functions, prop_conv); + + return safety_checkert::resultt::PAUSED; } catch(const std::string &error_str) @@ -406,6 +413,10 @@ void bmct::slice() statistics() << "Generated " << symex.get_total_vccs() << " VCC(s), " << symex.get_remaining_vccs() << " remaining after simplification" << eom; + + if(options.is_set("paths")) + statistics() << "Generated " << symex.path_segment_vccs + << " new VCC(s) along current path segment" << eom; } safety_checkert::resultt bmct::run( @@ -494,8 +505,8 @@ int bmct::do_language_agnostic_bmc( std::function driver_configure_bmc, std::function callback_after_symex) { - safety_checkert::resultt final_result = safety_checkert::resultt::UNKNOWN; - safety_checkert::resultt tmp_result = safety_checkert::resultt::UNKNOWN; + safety_checkert::resultt final_result = safety_checkert::resultt::SAFE; + safety_checkert::resultt tmp_result = safety_checkert::resultt::SAFE; const symbol_tablet &symbol_table = model.get_symbol_table(); messaget message(ui); std::unique_ptr worklist; @@ -554,11 +565,6 @@ int bmct::do_language_agnostic_bmc( while(!worklist->empty()) { - if(tmp_result != safety_checkert::resultt::PAUSED) - message.status() << "___________________________\n" - << "Starting new path (" << worklist->size() - << " to go)\n" - << message.eom; cbmc_solverst solvers( opts, symbol_table, @@ -613,13 +619,15 @@ int bmct::do_language_agnostic_bmc( switch(final_result) { case safety_checkert::resultt::SAFE: + if(opts.is_set("paths")) + report_success(message, ui); return CPROVER_EXIT_VERIFICATION_SAFE; case safety_checkert::resultt::UNSAFE: + if(opts.is_set("paths")) + report_failure(message, ui); return CPROVER_EXIT_VERIFICATION_UNSAFE; case safety_checkert::resultt::ERROR: return CPROVER_EXIT_INTERNAL_ERROR; - case safety_checkert::resultt::UNKNOWN: - return CPROVER_EXIT_INTERNAL_ERROR; case safety_checkert::resultt::PAUSED: UNREACHABLE; } diff --git a/src/goto-programs/safety_checker.h b/src/goto-programs/safety_checker.h index b2aee4fab3e..21d2529b410 100644 --- a/src/goto-programs/safety_checker.h +++ b/src/goto-programs/safety_checker.h @@ -42,10 +42,6 @@ class safety_checkert:public messaget /// doing path exploration; the symex state has been saved, and symex should /// be resumed by the caller. PAUSED, - /// We haven't yet assigned a safety check result to this object. A value of - /// UNKNOWN can be used to initialize a resultt object, and that object may - /// then safely be used with the |= and &= operators. - UNKNOWN }; // check whether all assertions in goto_functions are safe @@ -76,9 +72,6 @@ operator&=(safety_checkert::resultt &a, safety_checkert::resultt const &b) b != safety_checkert::resultt::PAUSED); switch(a) { - case safety_checkert::resultt::UNKNOWN: - a = b; - return a; case safety_checkert::resultt::ERROR: return a; case safety_checkert::resultt::SAFE: @@ -107,9 +100,6 @@ operator|=(safety_checkert::resultt &a, safety_checkert::resultt const &b) b != safety_checkert::resultt::PAUSED); switch(a) { - case safety_checkert::resultt::UNKNOWN: - a = b; - return a; case safety_checkert::resultt::SAFE: return a; case safety_checkert::resultt::ERROR: diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 667f85039ef..90594da545b 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -70,6 +70,7 @@ class goto_symext log(mh), guard_identifier("goto_symex::\\guard"), path_storage(path_storage), + path_segment_vccs(0), _total_vccs(std::numeric_limits::max()), _remaining_vccs(std::numeric_limits::max()) { @@ -464,6 +465,18 @@ class goto_symext path_storaget &path_storage; +public: + /// \brief Number of VCCs generated during the run of this goto_symext object + /// + /// This member is always initialized to `0` upon construction of this object. + /// It therefore differs from goto_symex_statet::total_vccs, which persists + /// across the creation of several goto_symext objects. When CBMC is run in + /// path-exploration mode, the meaning of this member is "the number of VCCs + /// generated between the last branch point and the current instruction," + /// while goto_symex_statet::total_vccs records the total number of VCCs + /// generated along the entire path from the beginning of the program. + std::size_t path_segment_vccs; + protected: /// @{\name Statistics /// diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index fb213414477..e0d7b39790e 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -52,6 +52,7 @@ void goto_symext::vcc( statet &state) { state.total_vccs++; + path_segment_vccs++; exprt expr=vcc_expr; diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp index 683f7cf0ee1..17b8ef244b7 100644 --- a/unit/path_strategies.cpp +++ b/unit/path_strategies.cpp @@ -81,7 +81,6 @@ SCENARIO("path strategies") 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)}); check_with_strategy( @@ -89,7 +88,6 @@ SCENARIO("path strategies") 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)}); } @@ -125,14 +123,11 @@ SCENARIO("path strategies") {// Outer else, inner else symex_eventt::resume(symex_eventt::enumt::JUMP, 13), symex_eventt::resume(symex_eventt::enumt::JUMP, 16), - symex_eventt::result(symex_eventt::enumt::SUCCESS), // Outer else, inner if symex_eventt::resume(symex_eventt::enumt::NEXT, 14), - symex_eventt::result(symex_eventt::enumt::SUCCESS), // Outer if, inner else symex_eventt::resume(symex_eventt::enumt::NEXT, 6), symex_eventt::resume(symex_eventt::enumt::JUMP, 9), - 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)}); @@ -147,13 +142,9 @@ SCENARIO("path strategies") symex_eventt::resume(symex_eventt::enumt::JUMP, 13), // Expand inner if of the outer if symex_eventt::resume(symex_eventt::enumt::NEXT, 7), - // No more branch points, so complete the path - symex_eventt::result(symex_eventt::enumt::SUCCESS), - // Continue BFSing + // No more branch points, so complete the path. Then continue BFSing symex_eventt::resume(symex_eventt::enumt::JUMP, 9), - symex_eventt::result(symex_eventt::enumt::SUCCESS), 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)}); } @@ -199,6 +190,9 @@ SCENARIO("path strategies") // infeasible. symex_eventt::resume(symex_eventt::enumt::NEXT, 7), symex_eventt::result(symex_eventt::enumt::SUCCESS), + + // Overall we fail. + symex_eventt::result(symex_eventt::enumt::FAILURE), }); check_with_strategy( @@ -224,6 +218,9 @@ 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), + + // Overall we fail. + symex_eventt::result(symex_eventt::enumt::FAILURE), }); } @@ -253,6 +250,8 @@ SCENARIO("path strategies") {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), + // Overall result symex_eventt::result(symex_eventt::enumt::FAILURE)}); } GIVEN("stopping on failure") @@ -262,6 +261,8 @@ SCENARIO("path strategies") halt_callback, c, {symex_eventt::resume(symex_eventt::enumt::JUMP, 7), + symex_eventt::result(symex_eventt::enumt::FAILURE), + // Overall result symex_eventt::result(symex_eventt::enumt::FAILURE)}); } } @@ -380,14 +381,20 @@ void _check_with_strategy( prop_convt &pc = cbmc_solver->prop_conv(); std::function callback = []() { return false; }; + safety_checkert::resultt overall_result = safety_checkert::resultt::SAFE; + std::size_t expected_results_cnt = 0; + bmct bmc(opts, gm.get_symbol_table(), mh, pc, *worklist, callback); - safety_checkert::resultt result = bmc.run(gm); + safety_checkert::resultt tmp_result = bmc.run(gm); - std::size_t expected_results_cnt = 0; - symex_eventt::validate_result(events, result, expected_results_cnt); + if(tmp_result != safety_checkert::resultt::PAUSED) + { + symex_eventt::validate_result(events, tmp_result, expected_results_cnt); + overall_result &= tmp_result; + } if( - result == safety_checkert::resultt::UNSAFE && + overall_result == safety_checkert::resultt::UNSAFE && opts.get_bool_option("stop-on-fail") && opts.is_set("paths")) { worklist->clear(); @@ -411,17 +418,25 @@ void _check_with_strategy( resume.state, *worklist, callback); - result = pe.run(gm); + tmp_result = pe.run(gm); - symex_eventt::validate_result(events, result, expected_results_cnt); + if(tmp_result != safety_checkert::resultt::PAUSED) + { + symex_eventt::validate_result(events, tmp_result, expected_results_cnt); + overall_result &= tmp_result; + } worklist->pop(); if( - result == safety_checkert::resultt::UNSAFE && + overall_result == safety_checkert::resultt::UNSAFE && opts.get_bool_option("stop-on-fail")) { worklist->clear(); } } + + symex_eventt::validate_result(events, overall_result, expected_results_cnt); + + INFO("The expected results list contains " << events.size() << " items"); REQUIRE(events.empty()); }