From acc1496bec66a454ba61358bf6caaac2d2d452d1 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 10 Mar 2019 22:55:14 +0000 Subject: [PATCH] Factor out property decider utilities so that they can be reused across goto checker implementations and in unit tests. --- src/goto-checker/bmc_util.cpp | 61 ++++++++++++++ src/goto-checker/bmc_util.h | 36 ++++++++ src/goto-checker/multi_path_symex_checker.cpp | 41 +--------- .../single_path_symex_checker.cpp | 82 ++++++------------- src/goto-checker/single_path_symex_checker.h | 6 -- 5 files changed, 125 insertions(+), 101 deletions(-) diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index 335a831e015..c3f6b022651 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/src/goto-checker/bmc_util.cpp @@ -30,6 +30,7 @@ Author: Daniel Kroening, Peter Schrammel #include #include +#include "goto_symex_property_decider.h" #include "symex_bmc.h" void message_building_error_trace(messaget &log) @@ -358,3 +359,63 @@ void postprocess_equation( symex.validate(validation_modet::INVARIANT); } } + +std::chrono::duration prepare_property_decider( + propertiest &properties, + symex_target_equationt &equation, + goto_symex_property_decidert &property_decider, + ui_message_handlert &ui_message_handler) +{ + auto solver_start = std::chrono::steady_clock::now(); + + messaget log(ui_message_handler); + log.status() << "Passing problem to " + << property_decider.get_solver().decision_procedure_text() + << messaget::eom; + + convert_symex_target_equation( + equation, property_decider.get_solver(), ui_message_handler); + property_decider.update_properties_goals_from_symex_target_equation( + properties); + property_decider.convert_goals(); + property_decider.freeze_goal_variables(); + + auto solver_stop = std::chrono::steady_clock::now(); + return std::chrono::duration(solver_stop - solver_start); +} + +void run_property_decider( + incremental_goto_checkert::resultt &result, + propertiest &properties, + goto_symex_property_decidert &property_decider, + ui_message_handlert &ui_message_handler, + std::chrono::duration solver_runtime, + bool set_pass) +{ + auto solver_start = std::chrono::steady_clock::now(); + + messaget log(ui_message_handler); + log.status() << "Running " + << property_decider.get_solver().decision_procedure_text() + << messaget::eom; + + property_decider.add_constraint_from_goals( + [&properties](const irep_idt &property_id) { + return is_property_to_check(properties.at(property_id).status); + }); + + decision_proceduret::resultt dec_result = property_decider.solve(); + + property_decider.update_properties_status_from_goals( + properties, result.updated_properties, dec_result, set_pass); + + auto solver_stop = std::chrono::steady_clock::now(); + solver_runtime += std::chrono::duration(solver_stop - solver_start); + log.status() << "Runtime decision procedure: " << solver_runtime.count() + << "s" << messaget::eom; + + if(dec_result == decision_proceduret::resultt::D_SATISFIABLE) + { + result.progress = incremental_goto_checkert::resultt::progresst::FOUND_FAIL; + } +} diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index ac0e9af788f..6c39c116ed0 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -12,14 +12,17 @@ Author: Daniel Kroening, Peter Schrammel #ifndef CPROVER_GOTO_CHECKER_BMC_UTIL_H #define CPROVER_GOTO_CHECKER_BMC_UTIL_H +#include #include #include #include #include +#include "incremental_goto_checker.h" #include "properties.h" +class goto_symex_property_decidert; class goto_tracet; class memory_model_baset; class message_handlert; @@ -136,6 +139,39 @@ void update_status_of_unknown_properties( propertiest &properties, std::unordered_set &updated_properties); +/// Converts the equation and sets up the property decider, +/// but does not call solve. +/// \param [in,out] properties: Sets the status of properties to be checked to +/// UNKNOWN +/// \param [in,out] equation: The equation that will be converted +/// \param [in,out] property_decider: The property decider that we are going to +/// set up +/// \param [in,out] ui_message_handler: For logging +/// \return The runtime for converting the equation +std::chrono::duration prepare_property_decider( + propertiest &properties, + symex_target_equationt &equation, + goto_symex_property_decidert &property_decider, + ui_message_handlert &ui_message_handler); + +/// Runs the property decider to solve the equation +/// \param [in,out] result: For recording the progress and the updated +/// properties +/// \param [in,out] properties: The status will be updated +/// \param [in,out] property_decider: The property decider that will solve the +/// equation +/// \param [in,out] ui_message_handler: For logging +/// \param solver_runtime: The solver runtime will be added and output +/// \param set_pass: If true then update UNKNOWN properties to PASS +/// if the solver returns UNSATISFIABLE +void run_property_decider( + incremental_goto_checkert::resultt &result, + propertiest &properties, + goto_symex_property_decidert &property_decider, + ui_message_handlert &ui_message_handler, + std::chrono::duration solver_runtime, + bool set_pass = true); + // clang-format off #define OPT_BMC \ "(program-only)" \ diff --git a/src/goto-checker/multi_path_symex_checker.cpp b/src/goto-checker/multi_path_symex_checker.cpp index f3b95cf0133..3cf8eb2bc08 100644 --- a/src/goto-checker/multi_path_symex_checker.cpp +++ b/src/goto-checker/multi_path_symex_checker.cpp @@ -65,51 +65,18 @@ operator()(propertiest &properties) if(!has_properties_to_check(properties)) return result; - log.status() << "Passing problem to " - << property_decider.get_solver().decision_procedure_text() - << messaget::eom; - - const auto solver_start = std::chrono::steady_clock::now(); - - convert_symex_target_equation( - equation, property_decider.get_solver(), ui_message_handler); - property_decider.update_properties_goals_from_symex_target_equation( - properties); - property_decider.convert_goals(); - property_decider.freeze_goal_variables(); + solver_runtime += prepare_property_decider( + properties, equation, property_decider, ui_message_handler); if(options.get_bool_option("localize-faults")) freeze_guards(equation, property_decider.get_solver()); - const auto solver_stop = std::chrono::steady_clock::now(); - solver_runtime += std::chrono::duration(solver_stop - solver_start); - - log.status() << "Running " - << property_decider.get_solver().decision_procedure_text() - << messaget::eom; equation_generated = true; } - const auto solver_start = std::chrono::steady_clock::now(); - - property_decider.add_constraint_from_goals( - [&properties](const irep_idt &property_id) { - return is_property_to_check(properties.at(property_id).status); - }); - - decision_proceduret::resultt dec_result = property_decider.solve(); - - property_decider.update_properties_status_from_goals( - properties, result.updated_properties, dec_result); - - const auto solver_stop = std::chrono::steady_clock::now(); - solver_runtime += std::chrono::duration(solver_stop - solver_start); - log.status() << "Runtime decision procedure: " << solver_runtime.count() - << "s" << messaget::eom; + run_property_decider( + result, properties, property_decider, ui_message_handler, solver_runtime); - result.progress = dec_result == decision_proceduret::resultt::D_SATISFIABLE - ? resultt::progresst::FOUND_FAIL - : resultt::progresst::DONE; return result; } diff --git a/src/goto-checker/single_path_symex_checker.cpp b/src/goto-checker/single_path_symex_checker.cpp index 5fb86458a62..edbceb8f2ff 100644 --- a/src/goto-checker/single_path_symex_checker.cpp +++ b/src/goto-checker/single_path_symex_checker.cpp @@ -33,7 +33,14 @@ operator()(propertiest &properties) // There might be more solutions from the previous equation. if(property_decider) { - decide(result, properties); + run_property_decider( + result, + properties, + *property_decider, + ui_message_handler, + std::chrono::duration(0), + false); + if(result.progress == resultt::progresst::FOUND_FAIL) return result; } @@ -91,8 +98,22 @@ operator()(propertiest &properties) if(symex.get_remaining_vccs() > 0) { - prepare(result, properties, resume.equation); - decide(result, properties); + update_properties_status_from_symex_target_equation( + properties, result.updated_properties, resume.equation); + + property_decider = util_make_unique( + options, ui_message_handler, resume.equation, ns); + + const auto solver_runtime = prepare_property_decider( + properties, resume.equation, *property_decider, ui_message_handler); + + run_property_decider( + result, + properties, + *property_decider, + ui_message_handler, + solver_runtime, + false); if(result.progress == resultt::progresst::FOUND_FAIL) return result; @@ -175,58 +196,3 @@ void single_path_symex_checkert::output_proof() const path_storaget::patht &resume = worklist->peek(); output_graphml(resume.equation, ns, options); } - -void single_path_symex_checkert::prepare( - resultt &result, - propertiest &properties, - symex_target_equationt &equation) -{ - update_properties_status_from_symex_target_equation( - properties, result.updated_properties, equation); - - property_decider = util_make_unique( - options, ui_message_handler, equation, ns); - - log.status() << "Passing problem to " - << property_decider->get_solver().decision_procedure_text() - << messaget::eom; - - convert_symex_target_equation( - equation, property_decider->get_solver(), ui_message_handler); - property_decider->update_properties_goals_from_symex_target_equation( - properties); - property_decider->convert_goals(); - property_decider->freeze_goal_variables(); -} - -void single_path_symex_checkert::decide( - resultt &result, - propertiest &properties) -{ - auto solver_start = std::chrono::steady_clock::now(); - - log.status() << "Running " - << property_decider->get_solver().decision_procedure_text() - << messaget::eom; - - property_decider->add_constraint_from_goals( - [&properties](const irep_idt &property_id) { - return is_property_to_check(properties.at(property_id).status); - }); - - decision_proceduret::resultt dec_result = property_decider->solve(); - - property_decider->update_properties_status_from_goals( - properties, result.updated_properties, dec_result, false); - - auto solver_stop = std::chrono::steady_clock::now(); - log.status() - << "Runtime decision procedure: " - << std::chrono::duration(solver_stop - solver_start).count() << "s" - << messaget::eom; - - if(dec_result == decision_proceduret::resultt::D_SATISFIABLE) - { - result.progress = resultt::progresst::FOUND_FAIL; - } -} diff --git a/src/goto-checker/single_path_symex_checker.h b/src/goto-checker/single_path_symex_checker.h index 2178d107501..f92cb3aaac1 100644 --- a/src/goto-checker/single_path_symex_checker.h +++ b/src/goto-checker/single_path_symex_checker.h @@ -47,12 +47,6 @@ class single_path_symex_checkert : public single_path_symex_only_checkert, protected: bool symex_initialized = false; std::unique_ptr property_decider; - - void prepare( - resultt &result, - propertiest &properties, - symex_target_equationt &equation); - void decide(resultt &result, propertiest &properties); }; #endif // CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_CHECKER_H