diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index a05f909e2de..b3af246508d 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -26,21 +26,29 @@ Author: Daniel Kroening, kroening@kroening.com # include #endif -#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include #include #include #include - #include - #include - #include #include #include #include #include +#include #include #include #include @@ -49,29 +57,14 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include - -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include - #include #include #include #include - #include - -#include - +#include #include +#include #include "c_test_input_generator.h" @@ -230,6 +223,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) cmdline.isset("outfile")) options.set_option("stop-on-fail", true); + if(cmdline.isset("eager-solving")) + options.set_option("eager-solving", true); + if( cmdline.isset("trace") || cmdline.isset("compact-trace") || cmdline.isset("stack-trace") || cmdline.isset("stop-on-fail") || @@ -620,6 +616,12 @@ int cbmc_parse_optionst::doit() all_properties_verifier_with_trace_storaget>( options, ui_message_handler, goto_model); } + else if(options.get_bool_option("eager-solving")) + { + verifier = util_make_unique>( + options, ui_message_handler, goto_model); + } else if( !options.get_bool_option("stop-on-fail") && !options.get_bool_option("paths")) @@ -878,6 +880,7 @@ void cbmc_parse_optionst::help() " --trace give a counterexample trace for failed properties\n" //NOLINT(*) " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*) " (implies --trace)\n" + " --eager-solving check a property as soon as symbolic execution reaches it\n" // NOLINT(*) " --localize-faults localize faults (experimental)\n" "\n" "C/C++ frontend options:\n" diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index b1a7abd9f27..2256dc4c283 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -69,6 +69,7 @@ class optionst; OPT_GOTO_TRACE \ OPT_VALIDATE \ OPT_ANSI_C_LANGUAGE \ + "(eager-solving)" \ "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length) // clang-format on diff --git a/src/goto-checker/Makefile b/src/goto-checker/Makefile index cb8243ecbc1..5aa66f6f6cb 100644 --- a/src/goto-checker/Makefile +++ b/src/goto-checker/Makefile @@ -1,6 +1,7 @@ SRC = bmc_util.cpp \ counterexample_beautification.cpp \ cover_goals_report_util.cpp \ + eager_multi_path_symex_checker.cpp \ incremental_goto_checker.cpp \ goto_symex_fault_localizer.cpp \ goto_symex_property_decider.cpp \ @@ -17,6 +18,7 @@ SRC = bmc_util.cpp \ symex_coverage.cpp \ symex_bmc.cpp \ symex_bmc_incremental_one_loop.cpp \ + symex_bmc_incremental_properties.cpp \ # Empty last line INCLUDES= -I .. diff --git a/src/goto-checker/eager_multi_path_symex_checker.cpp b/src/goto-checker/eager_multi_path_symex_checker.cpp new file mode 100644 index 00000000000..98f7487692f --- /dev/null +++ b/src/goto-checker/eager_multi_path_symex_checker.cpp @@ -0,0 +1,252 @@ +/*******************************************************************\ + +Module: Goto Checker using Bounded Model Checking + +Author: Michael Tautschnig + +\*******************************************************************/ + +/// \file +/// Goto Checker using Bounded Model Checking + +#include "eager_multi_path_symex_checker.h" + +#include + +#include + +#include "bmc_util.h" +#include "counterexample_beautification.h" + +#include + +eager_multi_path_symex_checkert::eager_multi_path_symex_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), + equation(ui_message_handler), + unwindset(goto_model), + symex( + ui_message_handler, + goto_model.get_symbol_table(), + equation, + options, + path_storage, + guard_manager, + unwindset, + ui_message_handler.get_ui()), + property_decider(options, ui_message_handler, equation, ns) +{ + setup_symex(symex, ns, options, ui_message_handler); + + // Freeze all symbols if we are using a prop_conv_solvert + prop_conv_solvert *prop_conv_solver = dynamic_cast( + &property_decider.get_stack_decision_procedure()); + if(prop_conv_solver != nullptr) + prop_conv_solver->set_all_frozen(); +} + +static void output_incremental_status( + const propertiest &properties, + messaget &message_hander) +{ + const auto any_failures = std::any_of( + properties.begin(), + properties.end(), + [](const std::pair &property) { + return property.second.status == property_statust::FAIL; + }); + std::string status = any_failures ? "FAILURE" : "INCONCLUSIVE"; + structured_datat incremental_status{ + {{labelt({"incremental", "status"}), + structured_data_entryt::data_node(json_stringt(status))}}}; + message_hander.statistics() << incremental_status; +} + +incremental_goto_checkert::resultt +eager_multi_path_symex_checkert::operator()(propertiest &properties) +{ + resultt result(resultt::progresst::DONE); + + std::chrono::duration solver_runtime(0); + + // we haven't got an equation yet + if(!initial_equation_generated) + { + full_equation_generated = !symex.from_entry_point_of( + goto_symext::get_goto_function(goto_model), symex_symbol_table); + + // This might add new properties such as unwinding assertions, for instance. + update_properties_status_from_symex_target_equation( + properties, result.updated_properties, equation); + + initial_equation_generated = true; + } + + while(has_properties_to_check(properties)) + { + // There are NOT_CHECKED or UNKNOWN properties. + + if(count_properties(properties, property_statust::UNKNOWN) > 0) + { + // We have UNKNOWN properties, i.e. properties that we can check + // on the current equation. + + log.status() + << "Passing problem to " + << property_decider.get_decision_procedure().decision_procedure_text() + << messaget::eom; + + const auto solver_start = std::chrono::steady_clock::now(); + + if(!current_equation_converted) + { + postprocess_equation(symex, equation, options, ns, ui_message_handler); + + log.status() << "converting SSA" << messaget::eom; + equation.convert_without_assertions( + property_decider.get_decision_procedure()); + + property_decider.update_properties_goals_from_symex_target_equation( + properties); + + // We convert the assertions in a new context. + property_decider.get_stack_decision_procedure().push(); + prop_conv_solvert *maybe_prop_conv = dynamic_cast(&property_decider.get_decision_procedure()); + assert(maybe_prop_conv); + maybe_prop_conv->post_processing_done = false; + equation.convert_assertions( + property_decider.get_decision_procedure(), false); + property_decider.convert_goals(); + + current_equation_converted = true; + } + + property_decider.add_constraint_from_goals( + [&properties](const irep_idt &property_id) { + return is_property_to_check(properties.at(property_id).status); + }); + + log.status() + << "Running " + << property_decider.get_decision_procedure().decision_procedure_text() + << messaget::eom; + + decision_proceduret::resultt dec_result = property_decider.solve(); + + property_decider.update_properties_status_from_goals( + properties, result.updated_properties, dec_result, false); + + const auto solver_stop = std::chrono::steady_clock::now(); + solver_runtime += + std::chrono::duration(solver_stop - solver_start); + log.status() << "Runtime decision procedure: " << solver_runtime.count() + << "s" << messaget::eom; + + result.progress = + dec_result == decision_proceduret::resultt::D_SATISFIABLE + ? resultt::progresst::FOUND_FAIL + : resultt::progresst::DONE; + + // We've got a trace to report. + if(result.progress == resultt::progresst::FOUND_FAIL) + break; + + // Nothing else to do with the current set of assertions. + // Let's pop them. + property_decider.get_stack_decision_procedure().pop(); + } + + // Now we are finally done. + if(full_equation_generated) + { + // For now, we assume that UNKNOWN properties are PASS. + update_status_of_unknown_properties( + properties, result.updated_properties); + + // For now, we assume that NOT_REACHED properties are PASS. + update_status_of_not_checked_properties( + properties, result.updated_properties); + + break; + } + + output_incremental_status(properties, log); + + // We continue symbolic execution + full_equation_generated = + !symex.resume(goto_symext::get_goto_function(goto_model)); + revert_slice(equation); + + // This might add new properties such as unwinding assertions, for instance. + update_properties_status_from_symex_target_equation( + properties, result.updated_properties, equation); + + current_equation_converted = false; + } + + return result; +} + +goto_tracet eager_multi_path_symex_checkert::build_full_trace() const +{ + goto_tracet goto_trace; + build_goto_trace( + equation, + equation.SSA_steps.end(), + property_decider.get_decision_procedure(), + ns, + goto_trace); + + return goto_trace; +} + +goto_tracet eager_multi_path_symex_checkert::build_shortest_trace() const +{ + if(options.get_bool_option("beautify")) + { + // NOLINTNEXTLINE(whitespace/braces) + counterexample_beautificationt{ui_message_handler}( + dynamic_cast(property_decider.get_stack_decision_procedure()), + equation); + } + + goto_tracet goto_trace; + build_goto_trace( + equation, property_decider.get_decision_procedure(), ns, goto_trace); + + return goto_trace; +} + +goto_tracet +eager_multi_path_symex_checkert::build_trace(const irep_idt &property_id) const +{ + goto_tracet goto_trace; + build_goto_trace( + equation, + ssa_step_matches_failing_property(property_id), + property_decider.get_decision_procedure(), + ns, + goto_trace); + + return goto_trace; +} + +const namespacet &eager_multi_path_symex_checkert::get_namespace() const +{ + return ns; +} + +void eager_multi_path_symex_checkert::output_proof() +{ + output_graphml(equation, ns, options); +} + +void eager_multi_path_symex_checkert::output_error_witness( + const goto_tracet &error_trace) +{ + output_graphml(error_trace, ns, options); +} diff --git a/src/goto-checker/eager_multi_path_symex_checker.h b/src/goto-checker/eager_multi_path_symex_checker.h new file mode 100644 index 00000000000..3aeb6f82ffc --- /dev/null +++ b/src/goto-checker/eager_multi_path_symex_checker.h @@ -0,0 +1,66 @@ +/*******************************************************************\ + +Module: Goto Checker using Multi-Path Symbolic Execution + +Author: Michael Tautschnig + +\*******************************************************************/ + +/// \file +/// Goto Checker using Multi-Path Symbolic Execution with early solving + +#ifndef CPROVER_GOTO_CHECKER_EAGER_MULTI_PATH_SYMEX_CHECKER_H +#define CPROVER_GOTO_CHECKER_EAGER_MULTI_PATH_SYMEX_CHECKER_H + +#include +#include + +#include "goto_symex_property_decider.h" +#include "goto_trace_provider.h" +#include "incremental_goto_checker.h" +#include "symex_bmc_incremental_properties.h" +#include "witness_provider.h" + +/// Performs a multi-path symbolic execution using goto-symex +/// and calls a SAT/SMT solver to check the status of the properties as soon as +/// properties are encountered. +class eager_multi_path_symex_checkert : public incremental_goto_checkert, + public goto_trace_providert, + public witness_providert +{ +public: + eager_multi_path_symex_checkert( + const optionst &options, + ui_message_handlert &ui_message_handler, + abstract_goto_modelt &goto_model); + + /// \copydoc incremental_goto_checkert::operator()(propertiest &properties) + /// + /// Note: This operator can handle shrinking and expanding sets of properties + /// in repeated invocations. + resultt operator()(propertiest &) override; + + goto_tracet build_full_trace() const override; + goto_tracet build_trace(const irep_idt &) const override; + goto_tracet build_shortest_trace() const override; + const namespacet &get_namespace() const override; + + void output_error_witness(const goto_tracet &) override; + void output_proof() override; + +protected: + abstract_goto_modelt &goto_model; + symbol_tablet symex_symbol_table; + namespacet ns; + symex_target_equationt equation; + path_fifot path_storage; // should go away + guard_managert guard_manager; + unwindsett unwindset; + symex_bmc_incremental_propertiest symex; + bool initial_equation_generated = false; + bool full_equation_generated = false; + bool current_equation_converted = false; + goto_symex_property_decidert property_decider; +}; + +#endif // CPROVER_GOTO_CHECKER_EAGER_MULTI_PATH_SYMEX_CHECKER_H diff --git a/src/goto-checker/single_loop_incremental_symex_checker.cpp b/src/goto-checker/single_loop_incremental_symex_checker.cpp index 6369847c30b..7b93d6bfae3 100644 --- a/src/goto-checker/single_loop_incremental_symex_checker.cpp +++ b/src/goto-checker/single_loop_incremental_symex_checker.cpp @@ -51,7 +51,7 @@ single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert( prop_conv_solver->set_all_frozen(); } -void output_incremental_status( +static void output_incremental_status( const propertiest &properties, messaget &message_hander) { diff --git a/src/goto-checker/symex_bmc_incremental_properties.cpp b/src/goto-checker/symex_bmc_incremental_properties.cpp new file mode 100644 index 00000000000..6967ac69616 --- /dev/null +++ b/src/goto-checker/symex_bmc_incremental_properties.cpp @@ -0,0 +1,65 @@ +/*******************************************************************\ + +Module: Incremental Bounded Model Checking for ANSI-C + +Author: Michael Tautschnig + +\*******************************************************************/ + +#include "symex_bmc_incremental_properties.h" + +#include + +#include + +#include + +symex_bmc_incremental_propertiest::symex_bmc_incremental_propertiest( + message_handlert &message_handler, + const symbol_tablet &outer_symbol_table, + symex_target_equationt &target, + const optionst &options, + path_storaget &path_storage, + guard_managert &guard_manager, + unwindsett &unwindset, + ui_message_handlert::uit output_ui) + : symex_bmct( + message_handler, + outer_symbol_table, + target, + options, + path_storage, + guard_manager, + unwindset), + output_ui(output_ui) +{ +} + +bool symex_bmc_incremental_propertiest::from_entry_point_of( + const get_goto_functiont &get_goto_function, + symbol_tablet &new_symbol_table) +{ + state = initialize_entry_point_state(get_goto_function); + + symex_with_state(*state, get_goto_function, new_symbol_table); + + return should_pause_symex; +} + +bool symex_bmc_incremental_propertiest::resume( + const get_goto_functiont &get_goto_function) +{ + should_pause_symex = false; + + symex_with_state(*state, get_goto_function, state->symbol_table); + + return should_pause_symex; +} + +void symex_bmc_incremental_propertiest::symex_assert( + const goto_programt::instructiont &instruction, + statet &goto_state) +{ + symex_bmct::symex_assert(instruction, goto_state); + should_pause_symex = true; +} diff --git a/src/goto-checker/symex_bmc_incremental_properties.h b/src/goto-checker/symex_bmc_incremental_properties.h new file mode 100644 index 00000000000..6e0b1405e79 --- /dev/null +++ b/src/goto-checker/symex_bmc_incremental_properties.h @@ -0,0 +1,45 @@ +/*******************************************************************\ + + Module: Incremental Bounded Model Checking for ANSI-C + + Author: Michael Tautschnig + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_CHECKER_SYMEX_BMC_INCREMENTAL_PROPERTIES_H +#define CPROVER_GOTO_CHECKER_SYMEX_BMC_INCREMENTAL_PROPERTIES_H + +#include + +#include "symex_bmc.h" + +class symex_bmc_incremental_propertiest : public symex_bmct +{ +public: + symex_bmc_incremental_propertiest( + message_handlert &, + const symbol_tablet &outer_symbol_table, + symex_target_equationt &, + const optionst &, + path_storaget &, + guard_managert &, + unwindsett &, + ui_message_handlert::uit output_ui); + + /// Return true if symex can be resumed + bool from_entry_point_of( + const get_goto_functiont &get_goto_function, + symbol_tablet &new_symbol_table); + + /// Return true if symex can be resumed + bool resume(const get_goto_functiont &get_goto_function); + +protected: + void symex_assert(const goto_programt::instructiont &, statet &) override; + + std::unique_ptr state; + + ui_message_handlert::uit output_ui; +}; + +#endif // CPROVER_GOTO_CHECKER_SYMEX_BMC_INCREMENTAL_PROPERTIES_H diff --git a/src/goto-symex/Makefile b/src/goto-symex/Makefile index 232ca74dacb..cf1cd62004e 100644 --- a/src/goto-symex/Makefile +++ b/src/goto-symex/Makefile @@ -1,5 +1,6 @@ SRC = auto_objects.cpp \ build_goto_trace.cpp \ + eager_equation.cpp \ expr_skeleton.cpp \ field_sensitivity.cpp \ goto_state.cpp \ diff --git a/src/goto-symex/eager_equation.cpp b/src/goto-symex/eager_equation.cpp new file mode 100644 index 00000000000..f91ab244796 --- /dev/null +++ b/src/goto-symex/eager_equation.cpp @@ -0,0 +1,176 @@ +/*******************************************************************\ + +Module: Generate equation and solve upon encountering an assertion + +Author: Michael Tautschnig + +\*******************************************************************/ + +#include "eager_equation.h" + +#if 0 + +void eager_equationt::assertion( + const exprt &guard, + const exprt &cond, + const std::string &msg, + const sourcet &source) +{ + symex_target_equationt::assertion(guard, cond, msg, source); + + // from symex_target_equationt::convert(decision_procedure) + const auto convert_SSA_start = std::chrono::steady_clock::now(); + + convert_without_assertions(decision_procedure); + // TODO now convert all prior assertions into assumptions + // TODO convert just this assertion + // DON'T convert_assertions(decision_procedure); + + const auto convert_SSA_stop = std::chrono::steady_clock::now(); + std::chrono::duration convert_SSA_runtime = + std::chrono::duration(convert_SSA_stop - convert_SSA_start); + log.status() << "Runtime Convert SSA: " << convert_SSA_runtime.count() << "s" + << messaget::eom; +} + +void symex_target_equationt::convert_assumptions( + decision_proceduret &decision_procedure) +{ + std::size_t step_index = 0; + for(auto &step : SSA_steps) + { + if(step.is_assume()) + { + if(step.ignore) + step.cond_handle = true_exprt(); + else + { + log.conditional_output( + log.debug(), [&step](messaget::mstreamt &mstream) { + step.output(mstream); + mstream << messaget::eom; + }); + + step.cond_handle = decision_procedure.handle(step.cond_expr); + + with_solver_hardness( + decision_procedure, hardness_register_ssa(step_index, step)); + } + } + ++step_index; + } +} + +void symex_target_equationt::convert_assertions( + decision_proceduret &decision_procedure, + bool optimized_for_single_assertions) +{ + // we find out if there is only _one_ assertion, + // which allows for a simpler formula + + std::size_t number_of_assertions=count_assertions(); + + if(number_of_assertions==0) + return; + + if(number_of_assertions == 1 && optimized_for_single_assertions) + { + std::size_t step_index = 0; + for(auto &step : SSA_steps) + { + // hide already converted assertions in the error trace + if(step.is_assert() && step.converted) + step.hidden = true; + + if(step.is_assert() && !step.ignore && !step.converted) + { + step.converted = true; + decision_procedure.set_to_false(step.cond_expr); + step.cond_handle = false_exprt(); + + with_solver_hardness( + decision_procedure, hardness_register_ssa(step_index, step)); + return; // prevent further assumptions! + } + else if(step.is_assume()) + { + decision_procedure.set_to_true(step.cond_expr); + + with_solver_hardness( + decision_procedure, hardness_register_ssa(step_index, step)); + } + ++step_index; + } + + UNREACHABLE; // unreachable + } + + // We do (NOT a1) OR (NOT a2) ... + // where the a's are the assertions + or_exprt::operandst disjuncts; + disjuncts.reserve(number_of_assertions); + + exprt assumption=true_exprt(); + + std::vector involved_steps; + + for(auto &step : SSA_steps) + { + // hide already converted assertions in the error trace + if(step.is_assert() && step.converted) + step.hidden = true; + + if(step.is_assert() && !step.ignore && !step.converted) + { + step.converted = true; + + log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) { + step.output(mstream); + mstream << messaget::eom; + }); + + implies_exprt implication( + assumption, + step.cond_expr); + + // do the conversion + step.cond_handle = decision_procedure.handle(implication); + + with_solver_hardness( + decision_procedure, + [&involved_steps, &step](solver_hardnesst &hardness) { + involved_steps.push_back(step.source.pc); + }); + + // store disjunct + disjuncts.push_back(not_exprt(step.cond_handle)); + } + else if(step.is_assume()) + { + // the assumptions have been converted before + // avoid deep nesting of ID_and expressions + if(assumption.id()==ID_and) + assumption.copy_to_operands(step.cond_handle); + else + assumption = and_exprt(assumption, step.cond_handle); + + with_solver_hardness( + decision_procedure, + [&involved_steps, &step](solver_hardnesst &hardness) { + involved_steps.push_back(step.source.pc); + }); + } + } + + const auto assertion_disjunction = disjunction(disjuncts); + // the below is 'true' if there are no assertions + decision_procedure.set_to_true(assertion_disjunction); + + with_solver_hardness( + decision_procedure, + [&assertion_disjunction, &involved_steps](solver_hardnesst &hardness) { + hardness.register_assertion_ssas(assertion_disjunction, involved_steps); + }); +} + +#endif diff --git a/src/goto-symex/eager_equation.h b/src/goto-symex/eager_equation.h new file mode 100644 index 00000000000..0ca0372b532 --- /dev/null +++ b/src/goto-symex/eager_equation.h @@ -0,0 +1,47 @@ +/*******************************************************************\ + +Module: Generate equation and solve upon encountering an assertion + +Author: Michael Tautschnig + +\*******************************************************************/ + +#if 0 + +/// \file +/// Generate equation and solve upon encountering an assertion + +# ifndef CPROVER_GOTO_SYMEX_EAGER_EQUATION_H +# define CPROVER_GOTO_SYMEX_EAGER_EQUATION_H + +# include "symex_target_equation.h" + +class decision_proceduret; +class namespacet; + +/// Extends \ref symex_target_equationt by immediately solving after each +/// encountered assertion. +class eager_equationt:public symex_target_equationt +{ +public: + eager_equationt(message_handlert &message_handler, decision_proceduret &decision_procedure) + : symex_target_equationt(message_handler), decision_procedure(decision_procedure) + { + } + + virtual ~eager_equationt() = default; + + /// \copydoc symex_targett::assertion() + void assertion( + const exprt &guard, + const exprt &cond, + const std::string &msg, + const sourcet &source) override; + +protected: + decision_proceduret &decision_procedure; +}; + +# endif + +#endif // CPROVER_GOTO_SYMEX_EAGER_EQUATION_H diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index c7fb2d37abe..0a78a144ffd 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -335,7 +335,7 @@ class goto_symext /// \param state: Symbolic execution state for current instruction virtual void symex_other(statet &state); - void symex_assert(const goto_programt::instructiont &, statet &); + virtual void symex_assert(const goto_programt::instructiont &, statet &); /// Propagate constants and points-to information implied by a GOTO condition. /// See \ref goto_statet::apply_condition for aspects of this which are common diff --git a/src/solvers/prop/prop_conv_solver.h b/src/solvers/prop/prop_conv_solver.h index ba41bc91222..68a29f74478 100644 --- a/src/solvers/prop/prop_conv_solver.h +++ b/src/solvers/prop/prop_conv_solver.h @@ -104,8 +104,8 @@ class prop_conv_solvert : public conflict_providert, return dynamic_cast(&prop); } -protected: bool post_processing_done = false; +protected: /// Get a _boolean_ value from the model if the formula is satisfiable. /// If the argument is not a boolean expression from the formula,