From 26bbcc6bb13543a24c01d4904256fe9043ba03f7 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 22 Jan 2019 22:01:25 +0000 Subject: [PATCH 01/14] Add SSA validation As introduced into bmct in eb0b86be. --- src/goto-checker/multi_path_symex_only_checker.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/goto-checker/multi_path_symex_only_checker.cpp b/src/goto-checker/multi_path_symex_only_checker.cpp index 89477c97529..881ee44bce1 100644 --- a/src/goto-checker/multi_path_symex_only_checker.cpp +++ b/src/goto-checker/multi_path_symex_only_checker.cpp @@ -89,6 +89,11 @@ void multi_path_symex_only_checkert::perform_symex() << equation.SSA_steps.size() << " steps" << messaget::eom; slice(symex, equation, ns, options, ui_message_handler); + + if(options.get_bool_option("validate-ssa-equation")) + { + symex.validate(validation_modet::INVARIANT); + } } void multi_path_symex_only_checkert::output_coverage_report() From cbcff00ca8819dfda46100bda34cc5bbf568cd14 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 4 Feb 2019 18:27:23 +0000 Subject: [PATCH 02/14] Set message handler in solver factory Allows us to remove set_message_handler() calls on solvers in other parts of the code. --- src/goto-checker/solver_factory.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp index fbb86fb83e0..a9dd5dd3a9c 100644 --- a/src/goto-checker/solver_factory.cpp +++ b/src/goto-checker/solver_factory.cpp @@ -158,6 +158,7 @@ std::unique_ptr solver_factoryt::get_default() } auto bv_pointers = util_make_unique(ns, solver->prop()); + bv_pointers->set_message_handler(message_handler); if(options.get_option("arrays-uf") == "never") bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_NONE; @@ -180,6 +181,7 @@ std::unique_ptr solver_factoryt::get_dimacs() std::string filename = options.get_option("outfile"); auto bv_dimacs = util_make_unique(ns, *prop, filename); + bv_dimacs->set_message_handler(message_handler); return util_make_unique(std::move(bv_dimacs), std::move(prop)); } @@ -209,6 +211,7 @@ std::unique_ptr solver_factoryt::get_bv_refinement() info.refine_arithmetic = options.get_bool_option("refine-arithmetic"); auto prop_conv = util_make_unique(info); + prop_conv->set_message_handler(message_handler); set_prop_conv_time_limit(*prop_conv); return util_make_unique(std::move(prop_conv), std::move(prop)); } @@ -232,6 +235,7 @@ solver_factoryt::get_string_refinement() info.refine_arithmetic = options.get_bool_option("refine-arithmetic"); auto prop_conv = util_make_unique(info); + prop_conv->set_message_handler(message_handler); set_prop_conv_time_limit(*prop_conv); return util_make_unique(std::move(prop_conv), std::move(prop)); } @@ -259,6 +263,7 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver) std::string("Generated by CBMC ") + CBMC_VERSION, "QF_AUFBV", solver); + smt2_dec->set_message_handler(message_handler); if(options.get_bool_option("fpa")) smt2_dec->use_FPA_theory = true; From 36ef9eeeb69dcce13bf08280497c2a697c339246 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 4 Feb 2019 16:12:39 +0000 Subject: [PATCH 03/14] Use in,out for in/out params in doxygen --- src/goto-checker/bmc_util.h | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index abe0a6b9e17..ef8fd13c071 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -71,8 +71,8 @@ void slice( /// Sets property status to PASS for properties whose /// conditions are constant true in the \p equation. -/// \param [inout] properties: The status is updated in this data structure -/// \param [inout] updated_properties: The set of property IDs of +/// \param [in,out] properties: The status is updated in this data structure +/// \param [in,out] updated_properties: The set of property IDs of /// updated properties /// \param equation: A equation generated by goto-symex void update_properties_status_from_symex_target_equation( @@ -81,8 +81,8 @@ void update_properties_status_from_symex_target_equation( const symex_target_equationt &equation); /// Sets the property status of NOT_CHECKED properties to PASS. -/// \param [inout] properties: The status is updated in this data structure -/// \param [inout] updated_properties: The IDs of updated properties are +/// \param [in,out] properties: The status is updated in this data structure +/// \param [in,out] updated_properties: The IDs of updated properties are /// added here /// Note: this should inspect the equation, but the equation doesn't have /// any useful information at the moment. From 6ca7fbfcc3bc019c019edc4e04d5904f35acf40e Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 21 Jan 2019 22:05:48 +0000 Subject: [PATCH 04/14] Factor out output_coverage_report into bmc_util Reduces code duplication across goto checkers. --- src/goto-checker/bmc_util.cpp | 16 ++++++++++++++++ src/goto-checker/bmc_util.h | 13 +++++++++++++ src/goto-checker/multi_path_symex_checker.cpp | 8 +++++++- .../multi_path_symex_only_checker.cpp | 18 +++++------------- .../multi_path_symex_only_checker.h | 1 - 5 files changed, 41 insertions(+), 15 deletions(-) diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index 3389f086505..93bfed6303a 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/src/goto-checker/bmc_util.cpp @@ -269,3 +269,19 @@ void update_status_of_not_checked_properties( } } } + +void output_coverage_report( + const std::string &cov_out, + const abstract_goto_modelt &goto_model, + const symex_bmct &symex, + ui_message_handlert &ui_message_handler) +{ + if( + !cov_out.empty() && + symex.output_coverage_report(goto_model.get_goto_functions(), cov_out)) + { + messaget log(ui_message_handler); + log.error() << "Failed to write symex coverage report to '" << cov_out + << "'" << messaget::eom; + } +} diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index ef8fd13c071..3fa59529abd 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -69,6 +69,19 @@ void slice( const optionst &, ui_message_handlert &); +/// Output a coverage report as generated by \ref symex_coveraget +/// if \p cov_out is non-empty. +/// \param cov_out: file to write the report to; no report is generated +/// if this is empty +/// \param goto_model: goto model to build the coverage report for +/// \param symex: symbolic execution run to report coverage for +/// \param ui_message_handler: status/warning message handler +void output_coverage_report( + const std::string &cov_out, + const abstract_goto_modelt &goto_model, + const symex_bmct &symex, + ui_message_handlert &ui_message_handler); + /// Sets property status to PASS for properties whose /// conditions are constant true in the \p equation. /// \param [in,out] properties: The status is updated in this data structure diff --git a/src/goto-checker/multi_path_symex_checker.cpp b/src/goto-checker/multi_path_symex_checker.cpp index 3b8b4073197..c2db62fb83a 100644 --- a/src/goto-checker/multi_path_symex_checker.cpp +++ b/src/goto-checker/multi_path_symex_checker.cpp @@ -49,7 +49,13 @@ operator()(propertiest &properties) if(!equation_generated) { perform_symex(); - output_coverage_report(); + + output_coverage_report( + options.get_option("symex-coverage-report"), + goto_model, + symex, + ui_message_handler); + // This might add new properties such as unwinding assertions, for instance. update_properties_status_from_symex_target_equation( properties, result.updated_properties, equation); diff --git a/src/goto-checker/multi_path_symex_only_checker.cpp b/src/goto-checker/multi_path_symex_only_checker.cpp index 881ee44bce1..2db87f3e77e 100644 --- a/src/goto-checker/multi_path_symex_only_checker.cpp +++ b/src/goto-checker/multi_path_symex_only_checker.cpp @@ -41,7 +41,11 @@ operator()(propertiest &properties) { perform_symex(); - output_coverage_report(); + output_coverage_report( + options.get_option("symex-coverage-report"), + goto_model, + symex, + ui_message_handler); if(options.get_bool_option("show-vcc")) { @@ -95,15 +99,3 @@ void multi_path_symex_only_checkert::perform_symex() symex.validate(validation_modet::INVARIANT); } } - -void multi_path_symex_only_checkert::output_coverage_report() -{ - std::string cov_out = options.get_option("symex-coverage-report"); - if( - !cov_out.empty() && - symex.output_coverage_report(goto_model.get_goto_functions(), cov_out)) - { - log.error() << "Failed to write symex coverage report to '" << cov_out - << "'" << messaget::eom; - } -} diff --git a/src/goto-checker/multi_path_symex_only_checker.h b/src/goto-checker/multi_path_symex_only_checker.h index ba05aaef730..b989311f84a 100644 --- a/src/goto-checker/multi_path_symex_only_checker.h +++ b/src/goto-checker/multi_path_symex_only_checker.h @@ -35,7 +35,6 @@ class multi_path_symex_only_checkert : public incremental_goto_checkert symex_bmct symex; void perform_symex(); - void output_coverage_report(); }; #endif // CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_ONLY_CHECKER_H From 0be41fb8cb23caef6d3d3841f04cfbc7204a9493 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 22 Jan 2019 22:20:39 +0000 Subject: [PATCH 05/14] Factor out perform_symex into bmc_util Better provide it as a utility than hiding it inside a class. Reduces code duplication across goto checkers. --- src/goto-checker/bmc_util.cpp | 48 +++++++++++++++++++ src/goto-checker/bmc_util.h | 10 ++++ src/goto-checker/multi_path_symex_checker.cpp | 9 +++- .../multi_path_symex_only_checker.cpp | 41 ++++------------ .../multi_path_symex_only_checker.h | 2 - 5 files changed, 74 insertions(+), 36 deletions(-) diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index 93bfed6303a..c9c72d600c3 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/src/goto-checker/bmc_util.cpp @@ -285,3 +285,51 @@ void output_coverage_report( << "'" << messaget::eom; } } + +static void postprocess_equation( + symex_bmct &symex, + symex_target_equationt &equation, + const optionst &options, + const namespacet &ns, + ui_message_handlert &ui_message_handler) +{ + // add a partial ordering, if required + if(equation.has_threads()) + { + std::unique_ptr memory_model = + get_memory_model(options, ns); + memory_model->set_message_handler(ui_message_handler); + (*memory_model)(equation); + } + + messaget log(ui_message_handler); + log.statistics() << "size of program expression: " + << equation.SSA_steps.size() << " steps" << messaget::eom; + + slice(symex, equation, ns, options, ui_message_handler); + + if(options.get_bool_option("validate-ssa-equation")) + { + symex.validate(validation_modet::INVARIANT); + } +} + +void perform_symex( + abstract_goto_modelt &goto_model, + symex_bmct &symex, + symbol_tablet &symex_symbol_table, + symex_target_equationt &equation, + const optionst &options, + const namespacet &ns, + ui_message_handlert &ui_message_handler) +{ + auto get_goto_function = + [&goto_model]( + const irep_idt &id) -> const goto_functionst::goto_functiont & { + return goto_model.get_goto_function(id); + }; + + symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table); + + postprocess_equation(symex, equation, options, ns, ui_message_handler); +} diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index 3fa59529abd..666ecc4a356 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -69,6 +69,16 @@ void slice( const optionst &, ui_message_handlert &); +/// Perform symbolic execution from the entry point +void perform_symex( + abstract_goto_modelt &, + symex_bmct &, + symbol_tablet &, + symex_target_equationt &, + const optionst &, + const namespacet &, + ui_message_handlert &); + /// Output a coverage report as generated by \ref symex_coveraget /// if \p cov_out is non-empty. /// \param cov_out: file to write the report to; no report is generated diff --git a/src/goto-checker/multi_path_symex_checker.cpp b/src/goto-checker/multi_path_symex_checker.cpp index c2db62fb83a..e399a50152b 100644 --- a/src/goto-checker/multi_path_symex_checker.cpp +++ b/src/goto-checker/multi_path_symex_checker.cpp @@ -48,7 +48,14 @@ operator()(propertiest &properties) // we haven't got an equation yet if(!equation_generated) { - perform_symex(); + perform_symex( + goto_model, + symex, + symex_symbol_table, + equation, + options, + ns, + ui_message_handler); output_coverage_report( options.get_option("symex-coverage-report"), diff --git a/src/goto-checker/multi_path_symex_only_checker.cpp b/src/goto-checker/multi_path_symex_only_checker.cpp index 2db87f3e77e..4fbb22f2d8a 100644 --- a/src/goto-checker/multi_path_symex_only_checker.cpp +++ b/src/goto-checker/multi_path_symex_only_checker.cpp @@ -39,7 +39,14 @@ multi_path_symex_only_checkert::multi_path_symex_only_checkert( incremental_goto_checkert::resultt multi_path_symex_only_checkert:: operator()(propertiest &properties) { - perform_symex(); + perform_symex( + goto_model, + symex, + symex_symbol_table, + equation, + options, + ns, + ui_message_handler); output_coverage_report( options.get_option("symex-coverage-report"), @@ -67,35 +74,3 @@ operator()(propertiest &properties) properties, result.updated_properties); return result; } - -void multi_path_symex_only_checkert::perform_symex() -{ - auto get_goto_function = - [this](const irep_idt &id) -> const goto_functionst::goto_functiont & { - return goto_model.get_goto_function(id); - }; - - // perform symbolic execution - symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table); - - // add a partial ordering, if required - // We won't be able to decide any properties by adding this, - // but we'd like to see the entire SSA. - if(equation.has_threads()) - { - std::unique_ptr memory_model = - get_memory_model(options, ns); - memory_model->set_message_handler(ui_message_handler); - (*memory_model)(equation); - } - - log.statistics() << "size of program expression: " - << equation.SSA_steps.size() << " steps" << messaget::eom; - - slice(symex, equation, ns, options, ui_message_handler); - - if(options.get_bool_option("validate-ssa-equation")) - { - symex.validate(validation_modet::INVARIANT); - } -} diff --git a/src/goto-checker/multi_path_symex_only_checker.h b/src/goto-checker/multi_path_symex_only_checker.h index b989311f84a..2d8a72ab0f1 100644 --- a/src/goto-checker/multi_path_symex_only_checker.h +++ b/src/goto-checker/multi_path_symex_only_checker.h @@ -33,8 +33,6 @@ class multi_path_symex_only_checkert : public incremental_goto_checkert symex_target_equationt equation; path_fifot path_storage; // should go away symex_bmct symex; - - void perform_symex(); }; #endif // CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_ONLY_CHECKER_H From 23150a4a0a18268f695223911adfbfa4c40c990f Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 22 Jan 2019 23:43:47 +0000 Subject: [PATCH 06/14] Add perform_symex for resuming from state Copied from bmct. Going to be used by single_path_symex_checkert. --- src/goto-checker/bmc_util.cpp | 21 +++++++++++++++++++++ src/goto-checker/bmc_util.h | 11 +++++++++++ 2 files changed, 32 insertions(+) diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index c9c72d600c3..43d9181e3c3 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/src/goto-checker/bmc_util.cpp @@ -333,3 +333,24 @@ void perform_symex( postprocess_equation(symex, equation, options, ns, ui_message_handler); } + +void perform_symex( + abstract_goto_modelt &goto_model, + symex_bmct &symex, + path_storaget::patht &resume, + symbol_tablet &symex_symbol_table, + const optionst &options, + const namespacet &ns, + ui_message_handlert &ui_message_handler) +{ + auto get_goto_function = + [&goto_model]( + const irep_idt &id) -> const goto_functionst::goto_functiont & { + return goto_model.get_goto_function(id); + }; + + symex.resume_symex_from_saved_state( + get_goto_function, resume.state, &resume.equation, symex_symbol_table); + + postprocess_equation(symex, resume.equation, options, ns, ui_message_handler); +} diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index 666ecc4a356..5b77ec3328b 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -15,6 +15,7 @@ Author: Daniel Kroening, Peter Schrammel #include #include +#include #include "properties.h" @@ -79,6 +80,16 @@ void perform_symex( const namespacet &, ui_message_handlert &); +/// Perform symbolic execution starting from \p resume. +void perform_symex( + abstract_goto_modelt &, + symex_bmct &, + path_storaget::patht &resume, + symbol_tablet &, + const optionst &, + const namespacet &, + ui_message_handlert &); + /// Output a coverage report as generated by \ref symex_coveraget /// if \p cov_out is non-empty. /// \param cov_out: file to write the report to; no report is generated From 8f7ffc4ec9b1cf563d0a14a96521dbbdcc4ef883 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 26 Jan 2019 21:34:37 +0000 Subject: [PATCH 07/14] Set final status of UNKNOWN properties Utility function to set all UNKNOWN properties to PASS when the verification algorithm has finished. Corresponds to the current behaviour of CBMC replying 'successful' when the given bounds have been reached. --- src/goto-checker/bmc_util.cpp | 16 ++++++++++++++++ src/goto-checker/bmc_util.h | 10 ++++++++++ 2 files changed, 26 insertions(+) diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index 43d9181e3c3..89f1d421b17 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/src/goto-checker/bmc_util.cpp @@ -270,6 +270,22 @@ void update_status_of_not_checked_properties( } } +void update_status_of_unknown_properties( + propertiest &properties, + std::unordered_set &updated_properties) +{ + for(auto &property_pair : properties) + { + if(property_pair.second.status == property_statust::UNKNOWN) + { + // This could have any status except NOT_CHECKED. + // We consider them PASS because we do verification modulo bounds. + property_pair.second.status = property_statust::PASS; + updated_properties.insert(property_pair.first); + } + } +} + void output_coverage_report( const std::string &cov_out, const abstract_goto_modelt &goto_model, diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index 5b77ec3328b..271dc97888b 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -124,6 +124,16 @@ void update_status_of_not_checked_properties( propertiest &properties, std::unordered_set &updated_properties); +/// Sets the property status of UNKNOWN properties to PASS. +/// \param [in,out] properties: The status is updated in this data structure +/// \param [in,out] updated_properties: The set of property IDs of +/// updated properties +/// Note: we currently declare everything PASS that is UNKNOWN at the +/// end of the model checking algorithm. +void update_status_of_unknown_properties( + propertiest &properties, + std::unordered_set &updated_properties); + // clang-format off #define OPT_BMC \ "(program-only)" \ From 584bb2b2f6287ebd2316b59893c60a743da22318 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Fri, 25 Jan 2019 23:05:07 +0000 Subject: [PATCH 08/14] Factor out goto_symex_property_decider Provides functionality close to solvers/prop/cover_goals but without callbacks. It allows us to iteratively get all counterexamples for a set of properties on a fixed equation. This is used as a component by multi-path and single-path symex checkers. --- src/goto-checker/Makefile | 1 + .../goto_symex_property_decider.cpp | 161 ++++++++++++++++++ .../goto_symex_property_decider.h | 93 ++++++++++ src/goto-checker/multi_path_symex_checker.cpp | 161 +++--------------- src/goto-checker/multi_path_symex_checker.h | 46 +---- 5 files changed, 281 insertions(+), 181 deletions(-) create mode 100644 src/goto-checker/goto_symex_property_decider.cpp create mode 100644 src/goto-checker/goto_symex_property_decider.h diff --git a/src/goto-checker/Makefile b/src/goto-checker/Makefile index ea625131c9c..51c5c221447 100644 --- a/src/goto-checker/Makefile +++ b/src/goto-checker/Makefile @@ -2,6 +2,7 @@ SRC = bmc_util.cpp \ counterexample_beautification.cpp \ cover_goals_report_util.cpp \ incremental_goto_checker.cpp \ + goto_symex_property_decider.cpp \ goto_trace_storage.cpp \ goto_verifier.cpp \ multi_path_symex_checker.cpp \ diff --git a/src/goto-checker/goto_symex_property_decider.cpp b/src/goto-checker/goto_symex_property_decider.cpp new file mode 100644 index 00000000000..d9093eedce2 --- /dev/null +++ b/src/goto-checker/goto_symex_property_decider.cpp @@ -0,0 +1,161 @@ +/*******************************************************************\ + +Module: Property Decider for Goto-Symex + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Property Decider for Goto-Symex + +#include "goto_symex_property_decider.h" + +goto_symex_property_decidert::goto_symex_property_decidert( + const optionst &options, + ui_message_handlert &ui_message_handler, + symex_target_equationt &equation, + const namespacet &ns) + : options(options), ui_message_handler(ui_message_handler), equation(equation) +{ + solver_factoryt solvers( + options, + ns, + ui_message_handler, + ui_message_handler.get_ui() == ui_message_handlert::uit::XML_UI); + solver = solvers.get_solver(); +} + +exprt goto_symex_property_decidert::goalt::as_expr() const +{ + exprt::operandst conjuncts; + conjuncts.reserve(instances.size()); + for(const auto &inst : instances) + conjuncts.push_back(literal_exprt(inst->cond_literal)); + return conjunction(conjuncts); +} + +void goto_symex_property_decidert:: + update_properties_goals_from_symex_target_equation(propertiest &properties) +{ + for(symex_target_equationt::SSA_stepst::iterator it = + equation.SSA_steps.begin(); + it != equation.SSA_steps.end(); + ++it) + { + if(it->is_assert()) + { + irep_idt property_id = it->get_property_id(); + CHECK_RETURN(!property_id.empty()); + + // consider goal instance if it is in the given properties + auto property_pair_it = properties.find(property_id); + if( + property_pair_it != properties.end() && + is_property_to_check(property_pair_it->second.status)) + { + // it's going to be checked, but we don't know the status yet + property_pair_it->second.status |= property_statust::UNKNOWN; + goal_map[property_id].instances.push_back(it); + } + } + } +} + +void goto_symex_property_decidert::convert_goals() +{ + for(auto &goal_pair : goal_map) + { + // Our goal is to falsify a property, i.e., we will + // add the negation of the property as goal. + goal_pair.second.condition = + !solver->prop_conv().convert(goal_pair.second.as_expr()); + } +} + +void goto_symex_property_decidert::freeze_goal_variables() +{ + for(const auto &goal_pair : goal_map) + { + if(!goal_pair.second.condition.is_constant()) + solver->prop_conv().set_frozen(goal_pair.second.condition); + } +} + +void goto_symex_property_decidert::add_constraint_from_goals( + std::function select_property) +{ + exprt::operandst disjuncts; + + for(const auto &goal_pair : goal_map) + { + if( + select_property(goal_pair.first) && + !goal_pair.second.condition.is_false()) + { + disjuncts.push_back(literal_exprt(goal_pair.second.condition)); + } + } + + // this is 'false' if there are no disjuncts + solver->prop_conv().set_to_true(disjunction(disjuncts)); +} + +decision_proceduret::resultt goto_symex_property_decidert::solve() +{ + return solver->prop_conv().dec_solve(); +} + +prop_convt &goto_symex_property_decidert::get_solver() const +{ + return solver->prop_conv(); +} + +symex_target_equationt &goto_symex_property_decidert::get_equation() const +{ + return equation; +} + +void goto_symex_property_decidert::update_properties_status_from_goals( + propertiest &properties, + std::unordered_set &updated_properties, + decision_proceduret::resultt dec_result, + bool set_pass) const +{ + switch(dec_result) + { + case decision_proceduret::resultt::D_SATISFIABLE: + for(auto &goal_pair : goal_map) + { + if(solver->prop_conv().l_get(goal_pair.second.condition).is_true()) + { + properties.at(goal_pair.first).status |= property_statust::FAIL; + updated_properties.insert(goal_pair.first); + } + } + break; + case decision_proceduret::resultt::D_UNSATISFIABLE: + if(!set_pass) + break; + + for(auto &property_pair : properties) + { + if(property_pair.second.status == property_statust::UNKNOWN) + { + property_pair.second.status |= property_statust::PASS; + updated_properties.insert(property_pair.first); + } + } + break; + case decision_proceduret::resultt::D_ERROR: + for(auto &property_pair : properties) + { + if(property_pair.second.status == property_statust::UNKNOWN) + { + property_pair.second.status |= property_statust::ERROR; + updated_properties.insert(property_pair.first); + } + } + break; + } +} diff --git a/src/goto-checker/goto_symex_property_decider.h b/src/goto-checker/goto_symex_property_decider.h new file mode 100644 index 00000000000..6ff272fdce3 --- /dev/null +++ b/src/goto-checker/goto_symex_property_decider.h @@ -0,0 +1,93 @@ +/*******************************************************************\ + +Module: Property Decider for Goto-Symex + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Property Decider for Goto-Symex + +#ifndef CPROVER_GOTO_CHECKER_GOTO_SYMEX_PROPERTY_DECIDER_H +#define CPROVER_GOTO_CHECKER_GOTO_SYMEX_PROPERTY_DECIDER_H + +#include + +#include + +#include "properties.h" +#include "solver_factory.h" + +/// Provides management of goal variables that encode properties +class goto_symex_property_decidert +{ +public: + goto_symex_property_decidert( + const optionst &options, + ui_message_handlert &ui_message_handler, + symex_target_equationt &equation, + const namespacet &ns); + + /// Get the conditions for the properties from the equation + /// and collect all 'instances' of the properties in the `goal_map` + void + update_properties_goals_from_symex_target_equation(propertiest &properties); + + /// Convert the instances of a property into a goal variable + void convert_goals(); + + /// Prevent the solver to optimize-away the goal variables + /// (necessary for incremental solving) + void freeze_goal_variables(); + + /// Add disjunction of negated selected properties to the equation + void add_constraint_from_goals( + std::function select_property); + + /// Calls solve() on the solver instance + decision_proceduret::resultt solve(); + + /// Returns the solver instance + prop_convt &get_solver() const; + + /// Return the equation associated with this instance + symex_target_equationt &get_equation() const; + + /// Update the property status from the truth value of the goal variable + /// \param [inout] properties: The status is updated in this data structure + /// \param [inout] updated_properties: The set of property IDs of + /// updated properties + /// \param dec_result: The result returned by the solver + /// \param set_pass: If true then update UNKNOWN properties to PASS + /// if the solver returns UNSATISFIABLE + void update_properties_status_from_goals( + propertiest &properties, + std::unordered_set &updated_properties, + decision_proceduret::resultt dec_result, + bool set_pass = true) const; + +protected: + const optionst &options; + ui_message_handlert &ui_message_handler; + symex_target_equationt &equation; + std::unique_ptr solver; + + struct goalt + { + /// A property holds if all instances of it are true + std::vector instances; + + /// The goal variable + literalt condition; + + exprt as_expr() const; + }; + + /// Maintains the relation between a property ID and + /// the corresponding goal variable that encodes + /// the negation of the conjunction of the instances of the property + std::map goal_map; +}; + +#endif // CPROVER_GOTO_CHECKER_GOTO_SYMEX_PROPERTY_DECIDER_H diff --git a/src/goto-checker/multi_path_symex_checker.cpp b/src/goto-checker/multi_path_symex_checker.cpp index e399a50152b..838839da5b6 100644 --- a/src/goto-checker/multi_path_symex_checker.cpp +++ b/src/goto-checker/multi_path_symex_checker.cpp @@ -21,15 +21,9 @@ multi_path_symex_checkert::multi_path_symex_checkert( ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model) : multi_path_symex_only_checkert(options, ui_message_handler, goto_model), - equation_generated(false) + equation_generated(false), + property_decider(options, ui_message_handler, equation, ns) { - solver_factoryt solvers( - options, - ns, - ui_message_handler, - ui_message_handler.get_ui() == ui_message_handlert::uit::XML_UI); - solver = solvers.get_solver(); - solver->prop_conv().set_message_handler(ui_message_handler); } incremental_goto_checkert::resultt multi_path_symex_checkert:: @@ -42,7 +36,6 @@ operator()(propertiest &properties) if(equation_generated && !has_properties_to_check(properties)) return result; - prop_convt &prop_conv = solver->prop_conv(); std::chrono::duration solver_runtime(0); // we haven't got an equation yet @@ -76,31 +69,38 @@ operator()(propertiest &properties) if(!has_properties_to_check(properties)) return result; - log.status() << "Passing problem to " << prop_conv.decision_procedure_text() + 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, prop_conv, ui_message_handler); - update_properties_goals_from_symex_target_equation(properties); - convert_goals(); - freeze_goal_variables(); + 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(); const auto solver_stop = std::chrono::steady_clock::now(); solver_runtime += std::chrono::duration(solver_stop - solver_start); - log.status() << "Running " << prop_conv.decision_procedure_text() + log.status() << "Running " + << property_decider.get_solver().decision_procedure_text() << messaget::eom; equation_generated = true; } const auto solver_start = std::chrono::steady_clock::now(); - add_constraint_from_goals(properties); + 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 = prop_conv.dec_solve(); + decision_proceduret::resultt dec_result = property_decider.solve(); - update_properties_status_from_goals( + property_decider.update_properties_status_from_goals( properties, result.updated_properties, dec_result); const auto solver_stop = std::chrono::steady_clock::now(); @@ -119,11 +119,15 @@ goto_tracet multi_path_symex_checkert::build_trace() const if(options.get_bool_option("beautify")) { counterexample_beautificationt()( - dynamic_cast(solver->prop_conv()), equation); + dynamic_cast(property_decider.get_solver()), equation); } goto_tracet goto_trace; ::build_error_trace( - goto_trace, ns, equation, solver->prop_conv(), ui_message_handler); + goto_trace, + ns, + equation, + property_decider.get_solver(), + ui_message_handler); return goto_trace; } @@ -142,120 +146,3 @@ void multi_path_symex_checkert::output_error_witness( { output_graphml(error_trace, ns, options); } - -exprt multi_path_symex_checkert::goalt::as_expr() const -{ - std::vector tmp; - tmp.reserve(instances.size()); - for(const auto &inst : instances) - tmp.push_back(literal_exprt(inst->cond_literal)); - return conjunction(tmp); -} - -void multi_path_symex_checkert:: - update_properties_goals_from_symex_target_equation(propertiest &properties) -{ - for(symex_target_equationt::SSA_stepst::iterator it = - equation.SSA_steps.begin(); - it != equation.SSA_steps.end(); - ++it) - { - if(it->is_assert()) - { - irep_idt property_id = it->get_property_id(); - CHECK_RETURN(!property_id.empty()); - - // consider goal instance if it is in the given properties - auto property_pair_it = properties.find(property_id); - if( - property_pair_it != properties.end() && - is_property_to_check(property_pair_it->second.status)) - { - // it's going to be checked, but we don't know the status yet - property_pair_it->second.status |= property_statust::UNKNOWN; - goal_map[property_id].instances.push_back(it); - } - } - } -} - -void multi_path_symex_checkert::convert_goals() -{ - for(auto &goal_pair : goal_map) - { - // Our goal is to falsify a property, i.e., we will - // add the negation of the property as goal. - goal_pair.second.condition = - !solver->prop_conv().convert(goal_pair.second.as_expr()); - } -} - -void multi_path_symex_checkert::freeze_goal_variables() -{ - for(const auto &goal_pair : goal_map) - { - if(!goal_pair.second.condition.is_constant()) - solver->prop_conv().set_frozen(goal_pair.second.condition); - } -} - -void multi_path_symex_checkert::add_constraint_from_goals( - const propertiest &properties) -{ - exprt::operandst disjuncts; - - // cover at least one unknown goal - - for(const auto &goal_pair : goal_map) - { - if( - is_property_to_check(properties.at(goal_pair.first).status) && - !goal_pair.second.condition.is_false()) - { - disjuncts.push_back(literal_exprt(goal_pair.second.condition)); - } - } - - // this is 'false' if there are no disjuncts - solver->prop_conv().set_to_true(disjunction(disjuncts)); -} - -void multi_path_symex_checkert::update_properties_status_from_goals( - propertiest &properties, - std::unordered_set &updated_properties, - decision_proceduret::resultt dec_result) -{ - switch(dec_result) - { - case decision_proceduret::resultt::D_SATISFIABLE: - for(auto &goal_pair : goal_map) - { - if(solver->prop_conv().l_get(goal_pair.second.condition).is_true()) - { - properties.at(goal_pair.first).status |= property_statust::FAIL; - updated_properties.insert(goal_pair.first); - } - } - break; - case decision_proceduret::resultt::D_UNSATISFIABLE: - for(auto &property_pair : properties) - { - if(property_pair.second.status == property_statust::UNKNOWN) - { - property_pair.second.status |= property_statust::PASS; - updated_properties.insert(property_pair.first); - } - } - break; - case decision_proceduret::resultt::D_ERROR: - for(auto &property_pair : properties) - { - if(property_pair.second.status == property_statust::UNKNOWN) - { - property_pair.second.status |= property_statust::ERROR; - updated_properties.insert(property_pair.first); - } - } - break; - } -} diff --git a/src/goto-checker/multi_path_symex_checker.h b/src/goto-checker/multi_path_symex_checker.h index 82675a47554..9e2b443a97e 100644 --- a/src/goto-checker/multi_path_symex_checker.h +++ b/src/goto-checker/multi_path_symex_checker.h @@ -12,9 +12,9 @@ Author: Daniel Kroening, Peter Schrammel #ifndef CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_CHECKER_H #define CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_CHECKER_H +#include "goto_symex_property_decider.h" #include "goto_trace_provider.h" #include "multi_path_symex_only_checker.h" -#include "solver_factory.h" #include "witness_provider.h" /// Performs a multi-path symbolic execution using goto-symex @@ -46,50 +46,8 @@ class multi_path_symex_checkert : public multi_path_symex_only_checkert, void output_proof() override; protected: - std::unique_ptr solver; - - struct goalt - { - /// A property holds if all instances of it are true - std::vector instances; - - /// The goal variable - literalt condition; - - exprt as_expr() const; - }; - - /// Maintains the relation between a property ID and - /// the corresponding goal variable that encodes - /// the negation of the conjunction of the instances of the property - std::map goal_map; - bool equation_generated; - - /// Get the conditions for the properties from the equation - /// and collect all 'instances' of the properties in the `goal_map` - void - update_properties_goals_from_symex_target_equation(propertiest &properties); - - /// Convert the instances of a property into a goal variable - void convert_goals(); - - /// Prevent the solver to optimize-away the goal variables - /// (necessary for incremental solving) - void freeze_goal_variables(); - - /// Add disjunction of negated properties to the equation - void add_constraint_from_goals(const propertiest &properties); - - /// Update the property status from the truth value of the goal variable - /// \param [inout] properties: The status is updated in this data structure - /// \param [inout] updated_properties: The set of property IDs of - /// updated properties - /// \param dec_result: The result returned by the solver - void update_properties_status_from_goals( - propertiest &properties, - std::unordered_set &updated_properties, - decision_proceduret::resultt dec_result); + goto_symex_property_decidert property_decider; }; #endif // CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_CHECKER_H From 2bfd25eba3e7528428775373bbfad8e8f34cd951 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 21 Jan 2019 22:06:15 +0000 Subject: [PATCH 09/14] Add single-path symex-only checker Replaces the path_explorert variant of bmct. The current implementation of this is overly complicated because path_explorert distinguishes the first run of goto-symex from the following ones. To drastically simplify the code goto-symex/symex_bmc needs to be refactored so that all runs can be handled uniformly (e.g. push entry point into work list and then 'resume' from there). See also single_path_symex_checkert. --- src/goto-checker/Makefile | 1 + .../single_path_symex_only_checker.cpp | 122 ++++++++++++++++++ .../single_path_symex_only_checker.h | 47 +++++++ 3 files changed, 170 insertions(+) create mode 100644 src/goto-checker/single_path_symex_only_checker.cpp create mode 100644 src/goto-checker/single_path_symex_only_checker.h diff --git a/src/goto-checker/Makefile b/src/goto-checker/Makefile index 51c5c221447..49342110667 100644 --- a/src/goto-checker/Makefile +++ b/src/goto-checker/Makefile @@ -9,6 +9,7 @@ SRC = bmc_util.cpp \ multi_path_symex_only_checker.cpp \ properties.cpp \ report_util.cpp \ + single_path_symex_only_checker.cpp \ solver_factory.cpp \ symex_coverage.cpp \ symex_bmc.cpp \ diff --git a/src/goto-checker/single_path_symex_only_checker.cpp b/src/goto-checker/single_path_symex_only_checker.cpp new file mode 100644 index 00000000000..29c4dde9bf0 --- /dev/null +++ b/src/goto-checker/single_path_symex_only_checker.cpp @@ -0,0 +1,122 @@ +/*******************************************************************\ + +Module: Goto Checker using Single Path Symbolic Execution only + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Goto Checker using Single Path Symbolic Execution only + +#include "single_path_symex_only_checker.h" + +#include + +#include +#include +#include +#include + +#include "bmc_util.h" +#include "symex_bmc.h" + +single_path_symex_only_checkert::single_path_symex_only_checkert( + const optionst &options, + ui_message_handlert &ui_message_handler, + abstract_goto_modelt &goto_model) + : incremental_goto_checkert(options, ui_message_handler), + goto_model(goto_model), + ns(goto_model.get_symbol_table(), symex_symbol_table), + worklist(get_path_strategy(options.get_option("exploration-strategy"))) +{ +} + +incremental_goto_checkert::resultt single_path_symex_only_checkert:: +operator()(propertiest &properties) +{ + resultt result(resultt::progresst::DONE); + + // First run goto-symex from entry point to initialize worklist + { + symex_target_equationt first_equation; + symex_bmct symex( + ui_message_handler, + goto_model.get_symbol_table(), + first_equation, + options, + *worklist); + + setup_symex(symex); + perform_symex( + goto_model, + symex, + symex_symbol_table, + first_equation, + options, + ns, + ui_message_handler); + + equation_output(symex, first_equation); + update_properties_status_from_symex_target_equation( + properties, result.updated_properties, first_equation); + } + + while(!worklist->empty()) + { + path_storaget::patht &resume = worklist->peek(); + symex_bmct symex( + ui_message_handler, + goto_model.get_symbol_table(), + resume.equation, + options, + *worklist); + + setup_symex(symex); + perform_symex( + goto_model, + symex, + resume, + symex_symbol_table, + options, + ns, + ui_message_handler); + equation_output(symex, resume.equation); + update_properties_status_from_symex_target_equation( + properties, result.updated_properties, resume.equation); + + worklist->pop(); + } + + // For now, we assume that NOT_REACHED properties are PASS. + update_status_of_not_checked_properties( + properties, result.updated_properties); + return result; +} + +void single_path_symex_only_checkert::equation_output( + const symex_bmct &symex, + const symex_target_equationt &equation) +{ + output_coverage_report( + options.get_option("symex-coverage-report"), + goto_model, + symex, + ui_message_handler); + + if(options.get_bool_option("show-vcc")) + show_vcc(options, ui_message_handler, equation); + + if(options.get_bool_option("program-only")) + show_program(ns, equation); + + if(options.get_bool_option("validate-ssa-equation")) + { + symex.validate(validation_modet::INVARIANT); + } +} + +void single_path_symex_only_checkert::setup_symex(symex_bmct &symex) +{ + ::setup_symex(symex, ns, options, ui_message_handler); +} diff --git a/src/goto-checker/single_path_symex_only_checker.h b/src/goto-checker/single_path_symex_only_checker.h new file mode 100644 index 00000000000..008c882bcf0 --- /dev/null +++ b/src/goto-checker/single_path_symex_only_checker.h @@ -0,0 +1,47 @@ +/*******************************************************************\ + +Module: Goto Checker using Single Path Symbolic Execution only + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Goto Checker using Single Path Symbolic Execution only + +#ifndef CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_ONLY_CHECKER_H +#define CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_ONLY_CHECKER_H + +#include "incremental_goto_checker.h" + +#include + +class symex_bmct; + +/// Uses goto-symex to generate a `symex_target_equationt` for each path. +class single_path_symex_only_checkert : public incremental_goto_checkert +{ +public: + single_path_symex_only_checkert( + const optionst &options, + ui_message_handlert &ui_message_handler, + abstract_goto_modelt &goto_model); + + resultt operator()(propertiest &) override; + + virtual ~single_path_symex_only_checkert() = default; + +protected: + abstract_goto_modelt &goto_model; + symbol_tablet symex_symbol_table; + namespacet ns; + std::unique_ptr worklist; + + void equation_output( + const symex_bmct &symex, + const symex_target_equationt &equation); + + virtual void setup_symex(symex_bmct &symex); +}; + +#endif // CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_ONLY_CHECKER_H From 258b7a9f5d50522ec5c57bfbcf87e1bd2bf29b85 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 21 Jan 2019 22:07:06 +0000 Subject: [PATCH 10/14] Use goto verifier for --paths with show-vcc and -program-only in CBMC We can now use single_path_symex_only_checkert instead of bmct. --- src/cbmc/cbmc_parse_options.cpp | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index c431aeede89..a157d38418c 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -40,6 +40,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -559,13 +560,20 @@ int cbmc_parse_optionst::doit() options.get_bool_option("program-only") || options.get_bool_option("show-vcc")) { - if(!options.get_bool_option("paths")) + if(options.get_bool_option("paths")) + { + all_properties_verifiert verifier( + options, ui_message_handler, goto_model); + (void)verifier(); + } + else { all_properties_verifiert verifier( options, ui_message_handler, goto_model); (void)verifier(); - return CPROVER_EXIT_SUCCESS; } + + return CPROVER_EXIT_SUCCESS; } if( From a588d80c0ad842f248af68cf3c9c3ff59db6a83a Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 21 Jan 2019 22:23:58 +0000 Subject: [PATCH 11/14] Add single-path symex checker Extends single_path_symex_only_checkert with calling the solver and returning traces. --- src/goto-checker/Makefile | 1 + .../single_path_symex_checker.cpp | 238 ++++++++++++++++++ src/goto-checker/single_path_symex_checker.h | 57 +++++ 3 files changed, 296 insertions(+) create mode 100644 src/goto-checker/single_path_symex_checker.cpp create mode 100644 src/goto-checker/single_path_symex_checker.h diff --git a/src/goto-checker/Makefile b/src/goto-checker/Makefile index 49342110667..c6bba2e1a9e 100644 --- a/src/goto-checker/Makefile +++ b/src/goto-checker/Makefile @@ -9,6 +9,7 @@ SRC = bmc_util.cpp \ multi_path_symex_only_checker.cpp \ properties.cpp \ report_util.cpp \ + single_path_symex_checker.cpp \ single_path_symex_only_checker.cpp \ solver_factory.cpp \ symex_coverage.cpp \ diff --git a/src/goto-checker/single_path_symex_checker.cpp b/src/goto-checker/single_path_symex_checker.cpp new file mode 100644 index 00000000000..63168332592 --- /dev/null +++ b/src/goto-checker/single_path_symex_checker.cpp @@ -0,0 +1,238 @@ +/*******************************************************************\ + +Module: Goto Checker using Single Path Symbolic Execution + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Goto Checker using Single Path Symbolic Execution + +#include "single_path_symex_checker.h" + +#include + +#include "bmc_util.h" +#include "counterexample_beautification.h" +#include "symex_bmc.h" + +single_path_symex_checkert::single_path_symex_checkert( + const optionst &options, + ui_message_handlert &ui_message_handler, + abstract_goto_modelt &goto_model) + : single_path_symex_only_checkert(options, ui_message_handler, goto_model) +{ +} + +incremental_goto_checkert::resultt single_path_symex_checkert:: +operator()(propertiest &properties) +{ + resultt result(resultt::progresst::DONE); + + // Unfortunately, the initial symex run is currently handled differently + // from the subsequent runs + if(!initial_symex_has_run) + { + initial_symex_has_run = true; + first_equation = symex_target_equationt(); + symex_bmct symex( + ui_message_handler, + goto_model.get_symbol_table(), + first_equation.value(), + options, + *worklist); + + setup_symex(symex); + perform_symex( + goto_model, + symex, + symex_symbol_table, + first_equation.value(), + options, + ns, + ui_message_handler); + + output_coverage_report( + options.get_option("symex-coverage-report"), + goto_model, + symex, + ui_message_handler); + + if(symex.get_remaining_vccs() > 0) + { + prepare(result, properties, first_equation.value()); + decide(result, properties); + + if(result.progress == resultt::progresst::FOUND_FAIL) + return result; + } + } + + // There might be more solutions from the previous equation. + if(property_decider) + { + decide(result, properties); + if(result.progress == resultt::progresst::FOUND_FAIL) + return result; + } + + if(first_equation.has_value()) + { + // We are in the second iteration. We don't need the equation + // from the first iteration anymore. + first_equation = {}; + } + else + { + if(!worklist->empty()) + { + // We are in iteration 3 or later; we pop the item processed + // in the previous iteration. + worklist->pop(); + } + else + { + // We are already done. + } + } + + while(!worklist->empty()) + { + path_storaget::patht &resume = worklist->peek(); + symex_bmct symex( + ui_message_handler, + goto_model.get_symbol_table(), + resume.equation, + options, + *worklist); + + setup_symex(symex); + perform_symex( + goto_model, + symex, + resume, + symex_symbol_table, + options, + ns, + ui_message_handler); + + output_coverage_report( + options.get_option("symex-coverage-report"), + goto_model, + symex, + ui_message_handler); + + if(symex.get_remaining_vccs() > 0) + { + prepare(result, properties, resume.equation); + decide(result, properties); + + if(result.progress == resultt::progresst::FOUND_FAIL) + return result; + } + + worklist->pop(); + } + + // For now, we assume that NOT_REACHED properties are PASS. + update_status_of_not_checked_properties( + properties, result.updated_properties); + + // For now, we assume that UNKNOWN properties are PASS. + update_status_of_unknown_properties(properties, result.updated_properties); + + // Worklist is empty: we are done. + return result; +} + +goto_tracet single_path_symex_checkert::build_trace() const +{ + if(options.get_bool_option("beautify")) + { + counterexample_beautificationt()( + dynamic_cast(property_decider->get_solver()), + property_decider->get_equation()); + } + goto_tracet goto_trace; + ::build_error_trace( + goto_trace, + ns, + property_decider->get_equation(), + property_decider->get_solver(), + ui_message_handler); + return goto_trace; +} + +const namespacet &single_path_symex_checkert::get_namespace() const +{ + return ns; +} + +void single_path_symex_checkert::output_error_witness( + const goto_tracet &goto_trace) +{ + output_graphml(goto_trace, ns, options); +} + +void single_path_symex_checkert::output_proof() +{ + // This is incorrect, but the best we can do at the moment. + 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( + goto_symex_property_decidert(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 new file mode 100644 index 00000000000..205f09baf2b --- /dev/null +++ b/src/goto-checker/single_path_symex_checker.h @@ -0,0 +1,57 @@ +/*******************************************************************\ + +Module: Goto Checker using Single Path Symbolic Execution + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Goto Checker using Single Path Symbolic Execution + +#ifndef CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_CHECKER_H +#define CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_CHECKER_H + +#include + +#include "goto_symex_property_decider.h" +#include "goto_trace_provider.h" +#include "single_path_symex_only_checker.h" +#include "solver_factory.h" +#include "witness_provider.h" + +/// Uses goto-symex to symbolically execute each path in the +/// goto model and calls a solver to find property violations. +class single_path_symex_checkert : public single_path_symex_only_checkert, + public witness_providert, + public goto_trace_providert +{ +public: + single_path_symex_checkert( + const optionst &options, + ui_message_handlert &ui_message_handler, + abstract_goto_modelt &goto_model); + + resultt operator()(propertiest &) override; + + goto_tracet build_trace() const override; + const namespacet &get_namespace() const override; + + void output_error_witness(const goto_tracet &) override; + void output_proof() override; + + virtual ~single_path_symex_checkert() = default; + +protected: + bool initial_symex_has_run = false; + optionalt first_equation; // for building traces + 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 From fbaa9ead111d201749966f15de12b6605ed67760 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 21 Jan 2019 22:28:13 +0000 Subject: [PATCH 12/14] Use goto verifier for --paths in CBMC We can now use single_path_symex_checkert instead of bmct. --- src/cbmc/cbmc_parse_options.cpp | 44 +++++++++++++++++++++++++-------- 1 file changed, 34 insertions(+), 10 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index a157d38418c..bf53e05ec51 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -40,6 +40,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -579,13 +580,20 @@ int cbmc_parse_optionst::doit() if( options.get_bool_option("dimacs") || !options.get_option("outfile").empty()) { - if(!options.get_bool_option("paths")) + if(options.get_bool_option("paths")) + { + stop_on_fail_verifiert verifier( + options, ui_message_handler, goto_model); + (void)verifier(); + } + else { stop_on_fail_verifiert verifier( options, ui_message_handler, goto_model); (void)verifier(); - return CPROVER_EXIT_SUCCESS; } + + return CPROVER_EXIT_SUCCESS; } if(options.is_set("cover")) @@ -604,20 +612,36 @@ int cbmc_parse_optionst::doit() std::unique_ptr verifier = nullptr; if( - !options.get_bool_option("paths") && !options.is_set("cover") && - !options.get_bool_option("dimacs") && options.get_option("outfile").empty()) + !options.is_set("cover") && !options.get_bool_option("dimacs") && + options.get_option("outfile").empty()) { if(options.get_bool_option("stop-on-fail")) { - verifier = - util_make_unique>( - options, ui_message_handler, goto_model); + if(options.get_bool_option("paths")) + { + verifier = + util_make_unique>( + options, ui_message_handler, goto_model); + } + else + { + verifier = + util_make_unique>( + options, ui_message_handler, goto_model); + } } else { - verifier = util_make_unique< - all_properties_verifier_with_trace_storaget>( - options, ui_message_handler, goto_model); + if(options.get_bool_option("paths")) + { + verifier = util_make_unique>(options, ui_message_handler, goto_model); + } + else + { + verifier = util_make_unique>(options, ui_message_handler, goto_model); + } } } From 8f3f02c50655128b7a3bd7dc429ef8ad8f4d84da Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 26 Jan 2019 22:12:00 +0000 Subject: [PATCH 13/14] Single-path goto checker for Java requires preprocessing JBMC requires further setup of symex_bmct. --- .../java_single_path_symex_checker.h | 37 ++++++++++++++++++ .../java_single_path_symex_only_checker.h | 38 +++++++++++++++++++ 2 files changed, 75 insertions(+) create mode 100644 jbmc/src/java_bytecode/java_single_path_symex_checker.h create mode 100644 jbmc/src/java_bytecode/java_single_path_symex_only_checker.h diff --git a/jbmc/src/java_bytecode/java_single_path_symex_checker.h b/jbmc/src/java_bytecode/java_single_path_symex_checker.h new file mode 100644 index 00000000000..21075d61948 --- /dev/null +++ b/jbmc/src/java_bytecode/java_single_path_symex_checker.h @@ -0,0 +1,37 @@ +/*******************************************************************\ + +Module: Goto Checker using Single Path Symbolic Execution for Java + +Author: Daniel Kroening, Peter Schrammel + + \*******************************************************************/ + +/// \file +/// Goto Checker using Single Path Symbolic Execution for Java + +#ifndef CPROVER_JAVA_BYTECODE_JAVA_SINGLE_PATH_SYMEX_CHECKER_H +#define CPROVER_JAVA_BYTECODE_JAVA_SINGLE_PATH_SYMEX_CHECKER_H + +#include + +#include "java_bmc_util.h" + +class java_single_path_symex_checkert : public single_path_symex_checkert +{ +public: + java_single_path_symex_checkert( + const optionst &options, + ui_message_handlert &ui_message_handler, + abstract_goto_modelt &goto_model) + : single_path_symex_checkert(options, ui_message_handler, goto_model) + { + } + + void setup_symex(symex_bmct &symex) override + { + single_path_symex_checkert::setup_symex(symex); + java_setup_symex(options, goto_model, symex); + } +}; + +#endif // CPROVER_JAVA_BYTECODE_JAVA_SINGLE_PATH_SYMEX_CHECKER_H diff --git a/jbmc/src/java_bytecode/java_single_path_symex_only_checker.h b/jbmc/src/java_bytecode/java_single_path_symex_only_checker.h new file mode 100644 index 00000000000..84d494c4ed7 --- /dev/null +++ b/jbmc/src/java_bytecode/java_single_path_symex_only_checker.h @@ -0,0 +1,38 @@ +/*******************************************************************\ + +Module: Goto Checker using Single Path Symbolic Execution for Java + +Author: Daniel Kroening, Peter Schrammel + + \*******************************************************************/ + +/// \file +/// Goto Checker using Single Path Symbolic Execution for Java + +#ifndef CPROVER_JAVA_BYTECODE_JAVA_SINGLE_PATH_SYMEX_ONLY_CHECKER_H +#define CPROVER_JAVA_BYTECODE_JAVA_SINGLE_PATH_SYMEX_ONLY_CHECKER_H + +#include + +#include "java_bmc_util.h" + +class java_single_path_symex_only_checkert + : public single_path_symex_only_checkert +{ +public: + java_single_path_symex_only_checkert( + const optionst &options, + ui_message_handlert &ui_message_handler, + abstract_goto_modelt &goto_model) + : single_path_symex_only_checkert(options, ui_message_handler, goto_model) + { + } + + void setup_symex(symex_bmct &symex) override + { + single_path_symex_only_checkert::setup_symex(symex); + java_setup_symex(options, goto_model, symex); + } +}; + +#endif // CPROVER_JAVA_BYTECODE_JAVA_SINGLE_PATH_SYMEX_ONLY_CHECKER_H From 1f9f4756d8eb7f6fba819ba2d3913fca3517a61e Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 26 Jan 2019 22:13:35 +0000 Subject: [PATCH 14/14] Use goto verifier for --paths in JBMC We can now use single_path_symex_checkert instead of bmct. --- jbmc/src/jbmc/jbmc_parse_options.cpp | 61 ++++++++++++++++++++++------ 1 file changed, 48 insertions(+), 13 deletions(-) diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 484cb8b3a22..94a34f48000 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -66,6 +66,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include +#include #include #include #include @@ -559,46 +561,79 @@ int jbmc_parse_optionst::doit() options.get_bool_option("program-only") || options.get_bool_option("show-vcc")) { - if(!options.get_bool_option("paths")) + if(options.get_bool_option("paths")) + { + all_properties_verifiert verifier( + options, ui_message_handler, goto_model); + (void)verifier(); + } + else { all_properties_verifiert verifier( options, ui_message_handler, goto_model); (void)verifier(); - return CPROVER_EXIT_SUCCESS; } + + return CPROVER_EXIT_SUCCESS; } if( options.get_bool_option("dimacs") || !options.get_option("outfile").empty()) { - if(!options.get_bool_option("paths")) + if(options.get_bool_option("paths")) + { + stop_on_fail_verifiert verifier( + options, ui_message_handler, goto_model); + (void)verifier(); + } + else { - stop_on_fail_verifiert verifier( + stop_on_fail_verifiert verifier( options, ui_message_handler, goto_model); (void)verifier(); - return CPROVER_EXIT_SUCCESS; } + + return CPROVER_EXIT_SUCCESS; } std::unique_ptr verifier = nullptr; if( - !options.get_bool_option("paths") && !options.is_set("cover") && - !options.get_bool_option("dimacs") && + !options.is_set("cover") && !options.get_bool_option("dimacs") && options.get_option("outfile").empty()) { if(options.get_bool_option("stop-on-fail")) { - verifier = util_make_unique< - stop_on_fail_verifiert>( - options, ui_message_handler, goto_model); + if(options.get_bool_option("paths")) + { + verifier = util_make_unique< + stop_on_fail_verifiert>( + options, ui_message_handler, goto_model); + } + else + { + verifier = util_make_unique< + stop_on_fail_verifiert>( + options, ui_message_handler, goto_model); + } } else { - verifier = util_make_unique>( - options, ui_message_handler, goto_model); + if(options.get_bool_option("paths")) + { + verifier = + util_make_unique>( + options, ui_message_handler, goto_model); + } + else + { + verifier = + util_make_unique>( + options, ui_message_handler, goto_model); + } } }