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 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); + } } } diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index c431aeede89..bf53e05ec51 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -40,6 +40,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include +#include #include #include @@ -559,25 +561,39 @@ 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( 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")) @@ -596,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); + } } } diff --git a/src/goto-checker/Makefile b/src/goto-checker/Makefile index ea625131c9c..c6bba2e1a9e 100644 --- a/src/goto-checker/Makefile +++ b/src/goto-checker/Makefile @@ -2,12 +2,15 @@ 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 \ 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 \ symex_bmc.cpp \ diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index 3389f086505..89f1d421b17 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/src/goto-checker/bmc_util.cpp @@ -269,3 +269,104 @@ 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, + 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; + } +} + +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); +} + +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 abe0a6b9e17..271dc97888b 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" @@ -69,10 +70,43 @@ 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 &); + +/// 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 +/// 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 [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 +115,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. @@ -90,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)" \ 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 3b8b4073197..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,14 +36,26 @@ 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 if(!equation_generated) { - perform_symex(); - output_coverage_report(); + perform_symex( + goto_model, + symex, + symex_symbol_table, + equation, + options, + ns, + ui_message_handler); + + 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); @@ -63,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(); @@ -106,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; } @@ -129,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 diff --git a/src/goto-checker/multi_path_symex_only_checker.cpp b/src/goto-checker/multi_path_symex_only_checker.cpp index 89477c97529..4fbb22f2d8a 100644 --- a/src/goto-checker/multi_path_symex_only_checker.cpp +++ b/src/goto-checker/multi_path_symex_only_checker.cpp @@ -39,9 +39,20 @@ multi_path_symex_only_checkert::multi_path_symex_only_checkert( incremental_goto_checkert::resultt multi_path_symex_only_checkert:: operator()(propertiest &properties) { - perform_symex(); - - output_coverage_report(); + perform_symex( + goto_model, + symex, + symex_symbol_table, + equation, + options, + ns, + ui_message_handler); + + output_coverage_report( + options.get_option("symex-coverage-report"), + goto_model, + symex, + ui_message_handler); if(options.get_bool_option("show-vcc")) { @@ -63,42 +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); -} - -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..2d8a72ab0f1 100644 --- a/src/goto-checker/multi_path_symex_only_checker.h +++ b/src/goto-checker/multi_path_symex_only_checker.h @@ -33,9 +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(); - void output_coverage_report(); }; #endif // CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_ONLY_CHECKER_H 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 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 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;