From f4dcaa7a5fced0832f99310f87ce75529f24be01 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 30 Sep 2022 13:01:22 +0000 Subject: [PATCH 1/3] WIP: Incremental symbolic execution with eager solving Using the new option --eager-solving, runs symbolic execution only up until an assertion is encountered and then queries the solver. Continues doing so until symbolic execution is complete. --- .../eager_multi_path_symex_checker.cpp | 249 ++++++++++++++++++ .../eager_multi_path_symex_checker.h | 66 +++++ 2 files changed, 315 insertions(+) create mode 100644 src/goto-checker/eager_multi_path_symex_checker.cpp create mode 100644 src/goto-checker/eager_multi_path_symex_checker.h 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..91db967cb75 --- /dev/null +++ b/src/goto-checker/eager_multi_path_symex_checker.cpp @@ -0,0 +1,249 @@ +/*******************************************************************\ + +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(); + 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 From 59f45892784f3ef6a4b746a3d0ad44081aaa35d9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 7 Jun 2022 12:08:57 +0000 Subject: [PATCH 2/3] Checking multiple properties in parallel NEXT STEPS - debug eager_multi_path_symex_checker CEX - solve in background using pool of solvers (worklist?) Overall goal: reducing the overhead when checking multiple properties in parallel. High-level idea: each time an assertion is encountered during symbolic execution, create a new thread to process this assertion (which is part of a property); the parent thread will continue doing symbolic execution. Expected savings: all the steps up to (and including) symbolic execution will be done no more often than when doing all-properties-at-once. The following development tasks need to be completed: 1) Make the solver available to symbolic execution (via a parameter or via a call-back). 2) Generate local copies or overlays of the equation system to annotate these with slicing information. 3) Maintain a map that not only maps expressions to literals, but also makes available the entire formula behind these literals. 4) Run solvers in separate threads, collect their results. 5) Produce output once all results have been obtained. 6) Make output available as soon as possible. This requires to clearly communicate that a property may be revisited (for example, via further loop unwindings) and may change its status from "SUCCESS" to "FAILURE." Ensure output is written by a single thread or under some global lock. --- src/cbmc/cbmc_parse_options.cpp | 45 ++--- src/cbmc/cbmc_parse_options.h | 1 + src/goto-checker/Makefile | 2 + .../single_loop_incremental_symex_checker.cpp | 2 +- .../symex_bmc_incremental_properties.cpp | 65 +++++++ .../symex_bmc_incremental_properties.h | 45 +++++ src/goto-symex/Makefile | 1 + src/goto-symex/eager_equation.cpp | 176 ++++++++++++++++++ src/goto-symex/eager_equation.h | 47 +++++ src/goto-symex/goto_symex.h | 2 +- 10 files changed, 363 insertions(+), 23 deletions(-) create mode 100644 src/goto-checker/symex_bmc_incremental_properties.cpp create mode 100644 src/goto-checker/symex_bmc_incremental_properties.h create mode 100644 src/goto-symex/eager_equation.cpp create mode 100644 src/goto-symex/eager_equation.h 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/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 From 7a41d7d14d91e972a87870856f8b2718abb9ad35 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 30 Sep 2022 12:58:36 +0000 Subject: [PATCH 3/3] WIP: Post-process incrementally Incremental symbolic execution requires post-processing in each step, and not just after the first one. --- src/goto-checker/eager_multi_path_symex_checker.cpp | 3 +++ src/solvers/prop/prop_conv_solver.h | 2 +- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/goto-checker/eager_multi_path_symex_checker.cpp b/src/goto-checker/eager_multi_path_symex_checker.cpp index 91db967cb75..98f7487692f 100644 --- a/src/goto-checker/eager_multi_path_symex_checker.cpp +++ b/src/goto-checker/eager_multi_path_symex_checker.cpp @@ -115,6 +115,9 @@ eager_multi_path_symex_checkert::operator()(propertiest &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(); 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,