diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 34edbb516a6..ea7b3e17f30 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -342,6 +342,9 @@ safety_checkert::resultt bmct::execute( const goto_functionst &goto_functions = goto_model.get_goto_functions(); + if(symex.should_pause_symex) + return safety_checkert::resultt::PAUSED; + // This provides the driver program the opportunity to do things like a // symbol-table or goto-functions dump instead of actually running the // checker, like show-vcc except driver-program specific. @@ -595,6 +598,7 @@ void bmct::setup_unwind() /// \param callback_after_symex: optional callback to be run after symex. /// See class member `bmct::driver_callback_after_symex` for details. int bmct::do_language_agnostic_bmc( + const path_strategy_choosert &path_strategy_chooser, const optionst &opts, abstract_goto_modelt &model, const ui_message_handlert::uit &ui, @@ -602,10 +606,16 @@ int bmct::do_language_agnostic_bmc( std::function driver_configure_bmc, std::function callback_after_symex) { + safety_checkert::resultt final_result = safety_checkert::resultt::UNKNOWN; + safety_checkert::resultt tmp_result = safety_checkert::resultt::UNKNOWN; const symbol_tablet &symbol_table = model.get_symbol_table(); message_handlert &mh = message.get_message_handler(); - safety_checkert::resultt result; - goto_symext::branch_worklistt worklist; + std::unique_ptr worklist; + std::string strategy = opts.get_option("exploration-strategy"); + INVARIANT( + path_strategy_chooser.is_valid_strategy(strategy), + "Front-end passed us invalid path strategy '" + strategy + "'"); + worklist = path_strategy_chooser.get(strategy); try { { @@ -614,21 +624,23 @@ int bmct::do_language_agnostic_bmc( std::unique_ptr cbmc_solver; cbmc_solver = solvers.get_solver(); prop_convt &pc = cbmc_solver->prop_conv(); - bmct bmc(opts, symbol_table, mh, pc, worklist, callback_after_symex); + bmct bmc(opts, symbol_table, mh, pc, *worklist, callback_after_symex); bmc.set_ui(ui); if(driver_configure_bmc) driver_configure_bmc(bmc, symbol_table); - result = bmc.run(model); + tmp_result = bmc.run(model); + if(tmp_result != safety_checkert::resultt::PAUSED) + final_result = tmp_result; } INVARIANT( - opts.get_bool_option("paths") || worklist.empty(), + opts.get_bool_option("paths") || worklist->empty(), "the worklist should be empty after doing full-program " "model checking, but the worklist contains " + - std::to_string(worklist.size()) + " unexplored branches."); + std::to_string(worklist->size()) + " unexplored branches."); // When model checking, the bmc.run() above will already have explored - // the entire program, and result contains the verification result. The - // worklist (containing paths that have not yet been explored) is thus + // the entire program, and final_result contains the verification result. + // The worklist (containing paths that have not yet been explored) is thus // empty, and we don't enter this loop. // // When doing path exploration, there will be some saved paths left to @@ -641,18 +653,19 @@ int bmct::do_language_agnostic_bmc( // difference between the implementations of perform_symbolic_exection() // in bmct and path_explorert, for more information. - while(!worklist.empty()) + while(!worklist->empty()) { - message.status() << "___________________________\n" - << "Starting new path (" << worklist.size() - << " to go)\n" - << message.eom; + if(tmp_result != safety_checkert::resultt::PAUSED) + message.status() << "___________________________\n" + << "Starting new path (" << worklist->size() + << " to go)\n" + << message.eom; cbmc_solverst solvers(opts, symbol_table, message.get_message_handler()); solvers.set_ui(ui); std::unique_ptr cbmc_solver; cbmc_solver = solvers.get_solver(); prop_convt &pc = cbmc_solver->prop_conv(); - goto_symext::branch_pointt &resume = worklist.front(); + path_storaget::patht &resume = worklist->peek(); path_explorert pe( opts, symbol_table, @@ -660,12 +673,14 @@ int bmct::do_language_agnostic_bmc( pc, resume.equation, resume.state, - worklist, + *worklist, callback_after_symex); if(driver_configure_bmc) driver_configure_bmc(pe, symbol_table); - result &= pe.run(model); - worklist.pop_front(); + tmp_result = pe.run(model); + if(tmp_result != safety_checkert::resultt::PAUSED) + final_result &= tmp_result; + worklist->pop(); } } catch(const char *error_msg) @@ -684,7 +699,7 @@ int bmct::do_language_agnostic_bmc( throw std::current_exception(); } - switch(result) + switch(final_result) { case safety_checkert::resultt::SAFE: return CPROVER_EXIT_VERIFICATION_SAFE; @@ -692,6 +707,10 @@ int bmct::do_language_agnostic_bmc( return CPROVER_EXIT_VERIFICATION_UNSAFE; case safety_checkert::resultt::ERROR: return CPROVER_EXIT_INTERNAL_ERROR; + case safety_checkert::resultt::UNKNOWN: + return CPROVER_EXIT_INTERNAL_ERROR; + case safety_checkert::resultt::PAUSED: + UNREACHABLE; } UNREACHABLE; } @@ -701,7 +720,7 @@ void bmct::perform_symbolic_execution( { symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table); INVARIANT( - options.get_bool_option("paths") || branch_worklist.empty(), + options.get_bool_option("paths") || path_storage.empty(), "Branch points were saved even though we should have been " "executing the entire program and merging paths"); } diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index 551fa7c2b3d..0e7efe46da9 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -23,6 +23,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include #include #include @@ -49,32 +51,32 @@ class bmct:public safety_checkert /// constructor is `false` (unset), an instance of this class will /// symbolically execute the entire program, performing path merging /// to build a formula corresponding to all executions of the program - /// up to the unwinding limit. In this case, the `branch_worklist` + /// up to the unwinding limit. In this case, the `path_storage` /// member shall not be touched; this is enforced by the assertion in /// this class' implementation of bmct::perform_symbolic_execution(). /// /// - If the `--paths` flag is `true`, this `bmct` object will explore a /// single path through the codebase without doing any path merging. /// If some paths were not taken, the state at those branch points - /// will be appended to `branch_worklist`. After the single path that + /// will be appended to `path_storage`. After the single path that /// this `bmct` object executed has been model-checked, you can resume /// exploring further paths by popping an element from - /// `branch_worklist` and using it to construct a path_explorert + /// `path_storage` and using it to construct a path_explorert /// object. bmct( const optionst &_options, const symbol_tablet &outer_symbol_table, message_handlert &_message_handler, prop_convt &_prop_conv, - goto_symext::branch_worklistt &_branch_worklist, + path_storaget &_path_storage, std::function callback_after_symex) : safety_checkert(ns, _message_handler), options(_options), outer_symbol_table(outer_symbol_table), ns(outer_symbol_table, symex_symbol_table), equation(), - branch_worklist(_branch_worklist), - symex(_message_handler, outer_symbol_table, equation, branch_worklist), + path_storage(_path_storage), + symex(_message_handler, outer_symbol_table, equation, path_storage), prop_conv(_prop_conv), ui(ui_message_handlert::uit::PLAIN), driver_callback_after_symex(callback_after_symex) @@ -115,6 +117,7 @@ class bmct:public safety_checkert } static int do_language_agnostic_bmc( + const path_strategy_choosert &path_strategy_chooser, const optionst &opts, abstract_goto_modelt &goto_model, const ui_message_handlert::uit &ui, @@ -128,7 +131,7 @@ class bmct:public safety_checkert /// /// This constructor exists as a delegate for the path_explorert class. /// It differs from \ref bmct's public constructor in that it actually - /// does something with the branch_worklistt argument, and also takes a + /// does something with the path_storaget argument, and also takes a /// symex_target_equationt. See the documentation for path_explorert for /// details. bmct( @@ -137,15 +140,15 @@ class bmct:public safety_checkert message_handlert &_message_handler, prop_convt &_prop_conv, symex_target_equationt &_equation, - goto_symext::branch_worklistt &_branch_worklist, + path_storaget &_path_storage, std::function callback_after_symex) : safety_checkert(ns, _message_handler), options(_options), outer_symbol_table(outer_symbol_table), ns(outer_symbol_table), equation(_equation), - branch_worklist(_branch_worklist), - symex(_message_handler, outer_symbol_table, equation, branch_worklist), + path_storage(_path_storage), + symex(_message_handler, outer_symbol_table, equation, path_storage), prop_conv(_prop_conv), ui(ui_message_handlert::uit::PLAIN), driver_callback_after_symex(callback_after_symex) @@ -166,7 +169,7 @@ class bmct:public safety_checkert symbol_tablet symex_symbol_table; namespacet ns; symex_target_equationt equation; - goto_symext::branch_worklistt &branch_worklist; + path_storaget &path_storage; symex_bmct symex; prop_convt &prop_conv; std::unique_ptr memory_model; @@ -257,7 +260,7 @@ class path_explorert : public bmct prop_convt &_prop_conv, symex_target_equationt &saved_equation, const goto_symex_statet &saved_state, - goto_symext::branch_worklistt &branch_worklist, + path_storaget &path_storage, std::function callback_after_symex) : bmct( _options, @@ -265,7 +268,7 @@ class path_explorert : public bmct _message_handler, _prop_conv, saved_equation, - branch_worklist, + path_storage, callback_after_symex), saved_state(saved_state) { @@ -292,7 +295,8 @@ class path_explorert : public bmct "(no-unwinding-assertions)" \ "(no-pretty-names)" \ "(partial-loops)" \ - "(paths)" \ + "(paths):" \ + "(show-symex-strategies)" \ "(depth):" \ "(unwind):" \ "(unwindset):" \ @@ -300,7 +304,8 @@ class path_explorert : public bmct "(unwindset):" #define HELP_BMC \ - " --paths explore paths one at a time\n" \ + " --paths [strategy] explore paths one at a time\n" \ + " --show-symex-strategies list strategies for use with --paths\n" \ " --program-only only show program expression\n" \ " --show-loops show the loops in the program\n" \ " --depth nr limit search depth\n" \ diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index f18d7756b95..295efe9c38f 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -68,7 +68,8 @@ cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv): parse_options_baset(CBMC_OPTIONS, argc, argv), xml_interfacet(cmdline), messaget(ui_message_handler), - ui_message_handler(cmdline, "CBMC " CBMC_VERSION) + ui_message_handler(cmdline, "CBMC " CBMC_VERSION), + path_strategy_chooser() { } @@ -79,7 +80,8 @@ ::cbmc_parse_optionst::cbmc_parse_optionst( parse_options_baset(CBMC_OPTIONS+extra_options, argc, argv), xml_interfacet(cmdline), messaget(ui_message_handler), - ui_message_handler(cmdline, "CBMC " CBMC_VERSION) + ui_message_handler(cmdline, "CBMC " CBMC_VERSION), + path_strategy_chooser() { } @@ -146,8 +148,13 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) exit(CPROVER_EXIT_USAGE_ERROR); } - if(cmdline.isset("paths")) - options.set_option("paths", true); + if(cmdline.isset("show-symex-strategies")) + { + std::cout << path_strategy_chooser.show_strategies(); + exit(CPROVER_EXIT_SUCCESS); + } + + path_strategy_chooser.set_path_strategy_options(cmdline, options, *this); if(cmdline.isset("program-only")) options.set_option("program-only", true); @@ -531,7 +538,11 @@ int cbmc_parse_optionst::doit() return CPROVER_EXIT_SET_PROPERTIES_FAILED; return bmct::do_language_agnostic_bmc( - options, goto_model, ui_message_handler.get_ui(), *this); + path_strategy_chooser, + options, + goto_model, + ui_message_handler.get_ui(), + *this); } bool cbmc_parse_optionst::set_properties() diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index b50c5160ba3..25ff6b50628 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -110,6 +110,7 @@ class cbmc_parse_optionst: protected: goto_modelt goto_model; ui_message_handlert ui_message_handler; + const path_strategy_choosert path_strategy_chooser; void eval_verbosity(); void register_languages(); diff --git a/src/cbmc/symex_bmc.cpp b/src/cbmc/symex_bmc.cpp index 1bbd5af77e0..986e368ea45 100644 --- a/src/cbmc/symex_bmc.cpp +++ b/src/cbmc/symex_bmc.cpp @@ -22,8 +22,8 @@ symex_bmct::symex_bmct( message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, - goto_symext::branch_worklistt &branch_worklist) - : goto_symext(mh, outer_symbol_table, _target, branch_worklist), + path_storaget &path_storage) + : goto_symext(mh, outer_symbol_table, _target, path_storage), record_coverage(false), max_unwind(0), max_unwind_is_set(false), diff --git a/src/cbmc/symex_bmc.h b/src/cbmc/symex_bmc.h index b1b6108de9a..bc43242037b 100644 --- a/src/cbmc/symex_bmc.h +++ b/src/cbmc/symex_bmc.h @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include "symex_coverage.h" @@ -26,7 +27,7 @@ class symex_bmct: public goto_symext message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, - goto_symext::branch_worklistt &branch_worklist); + path_storaget &path_storage); // To show progress source_locationt last_source_location; diff --git a/src/doxyfile b/src/doxyfile index 1c21026929f..409422346ce 100644 --- a/src/doxyfile +++ b/src/doxyfile @@ -281,7 +281,7 @@ OPTIMIZE_OUTPUT_VHDL = NO # Note that for custom extensions you also need to set FILE_PATTERNS otherwise # the files are not read by doxygen. -EXTENSION_MAPPING = +EXTENSION_MAPPING = h=c++ # If the MARKDOWN_SUPPORT tag is enabled then doxygen pre-processes all comments # according to the Markdown format, which allows for more readable diff --git a/src/goto-instrument/accelerate/scratch_program.h b/src/goto-instrument/accelerate/scratch_program.h index 0bd76634bd0..ef07e370115 100644 --- a/src/goto-instrument/accelerate/scratch_program.h +++ b/src/goto-instrument/accelerate/scratch_program.h @@ -23,6 +23,7 @@ Author: Matt Lewis #include #include +#include #include #include @@ -41,8 +42,8 @@ class scratch_programt:public goto_programt symex_symbol_table(), ns(symbol_table, symex_symbol_table), equation(), - branch_worklist(), - symex(mh, symbol_table, equation, branch_worklist), + path_storage(), + symex(mh, symbol_table, equation, path_storage), satcheck(util_make_unique()), satchecker(ns, *satcheck), z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3), @@ -78,7 +79,7 @@ class scratch_programt:public goto_programt symbol_tablet symex_symbol_table; namespacet ns; symex_target_equationt equation; - goto_symext::branch_worklistt branch_worklist; + path_fifot path_storage; goto_symext symex; std::unique_ptr satcheck; diff --git a/src/goto-programs/safety_checker.h b/src/goto-programs/safety_checker.h index 599669f4cce..b2aee4fab3e 100644 --- a/src/goto-programs/safety_checker.h +++ b/src/goto-programs/safety_checker.h @@ -30,7 +30,23 @@ class safety_checkert:public messaget const namespacet &_ns, message_handlert &_message_handler); - enum class resultt { SAFE, UNSAFE, ERROR }; + enum class resultt + { + /// No safety properties were violated + SAFE, + /// Some safety properties were violated + UNSAFE, + /// Safety is unknown due to an error during safety checking + ERROR, + /// Symbolic execution has been suspended due to encountering a GOTO while + /// doing path exploration; the symex state has been saved, and symex should + /// be resumed by the caller. + PAUSED, + /// We haven't yet assigned a safety check result to this object. A value of + /// UNKNOWN can be used to initialize a resultt object, and that object may + /// then safely be used with the |= and &= operators. + UNKNOWN + }; // check whether all assertions in goto_functions are safe // if UNSAFE, then a trace is returned @@ -47,11 +63,22 @@ class safety_checkert:public messaget }; /// \brief The worst of two results +/// +/// A result of PAUSED means that the safety check has not yet completed, +/// thus it makes no sense to compare it to the result of a completed safety +/// check. Therefore do not pass safety_checkert::resultt:PAUSED as an +/// argument to this function. inline safety_checkert::resultt & operator&=(safety_checkert::resultt &a, safety_checkert::resultt const &b) { + PRECONDITION( + a != safety_checkert::resultt::PAUSED && + b != safety_checkert::resultt::PAUSED); switch(a) { + case safety_checkert::resultt::UNKNOWN: + a = b; + return a; case safety_checkert::resultt::ERROR: return a; case safety_checkert::resultt::SAFE: @@ -60,16 +87,29 @@ operator&=(safety_checkert::resultt &a, safety_checkert::resultt const &b) case safety_checkert::resultt::UNSAFE: a = b == safety_checkert::resultt::ERROR ? b : a; return a; + case safety_checkert::resultt::PAUSED: + UNREACHABLE; } UNREACHABLE; } /// \brief The best of two results +/// +/// A result of PAUSED means that the safety check has not yet completed, +/// thus it makes no sense to compare it to the result of a completed safety +/// check. Therefore do not pass safety_checkert::resultt:PAUSED as an +/// argument to this function. inline safety_checkert::resultt & operator|=(safety_checkert::resultt &a, safety_checkert::resultt const &b) { + PRECONDITION( + a != safety_checkert::resultt::PAUSED && + b != safety_checkert::resultt::PAUSED); switch(a) { + case safety_checkert::resultt::UNKNOWN: + a = b; + return a; case safety_checkert::resultt::SAFE: return a; case safety_checkert::resultt::ERROR: @@ -78,6 +118,8 @@ operator|=(safety_checkert::resultt &a, safety_checkert::resultt const &b) case safety_checkert::resultt::UNSAFE: a = b == safety_checkert::resultt::SAFE ? b : a; return a; + case safety_checkert::resultt::PAUSED: + UNREACHABLE; } UNREACHABLE; } diff --git a/src/goto-symex/Makefile b/src/goto-symex/Makefile index 76f9bb61d91..dc4c73f3c15 100644 --- a/src/goto-symex/Makefile +++ b/src/goto-symex/Makefile @@ -8,6 +8,7 @@ SRC = adjust_float_expressions.cpp \ memory_model_sc.cpp \ memory_model_tso.cpp \ partial_order_concurrency.cpp \ + path_storage.cpp \ postcondition.cpp \ precondition.cpp \ rewrite_union.cpp \ diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 117693b8391..7811a4497eb 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "goto_symex_state.h" +#include "path_storage.h" #include "symex_target_equation.h" class byte_extract_exprt; @@ -47,31 +48,13 @@ class goto_symext public: typedef goto_symex_statet statet; - /// \brief Information saved at a conditional goto to resume execution - struct branch_pointt - { - symex_target_equationt equation; - statet state; - - explicit branch_pointt(const symex_target_equationt &e, const statet &s) - : equation(e), state(s, &equation) - { - } - - explicit branch_pointt(const branch_pointt &other) - : equation(other.equation), state(other.state, &equation) - { - } - }; - - typedef std::list branch_worklistt; - goto_symext( message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, - branch_worklistt &branch_worklist) - : total_vccs(0), + path_storaget &path_storage) + : should_pause_symex(false), + total_vccs(0), remaining_vccs(0), constant_propagation(true), language_mode(), @@ -81,7 +64,7 @@ class goto_symext atomic_section_counter(0), log(mh), guard_identifier("goto_symex::\\guard"), - branch_worklist(branch_worklist) + path_storage(path_storage) { options.set_option("simplify", true); options.set_option("assertions", true); @@ -177,6 +160,15 @@ class goto_symext goto_programt::const_targett first, goto_programt::const_targett limit); + /// \brief Have states been pushed onto the workqueue? + /// + /// If this flag is set at the end of a symbolic execution run, it means that + /// symex has been paused because we encountered a GOTO instruction while + /// doing path exploration, and thus pushed the successor states of the GOTO + /// onto path_storage. The symbolic execution caller should now choose which + /// successor state to continue executing, and resume symex from that state. + bool should_pause_symex; + protected: /// Initialise the symbolic execution and the given state with pc /// as entry point. @@ -462,7 +454,7 @@ class goto_symext void replace_nondet(exprt &); void rewrite_quantifiers(exprt &, statet &); - branch_worklistt &branch_worklist; + path_storaget &path_storage; }; #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index b30c3a27448..8b00a1db968 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -372,7 +372,13 @@ class goto_symex_statet final incremental_dirtyt dirty; goto_programt::const_targett saved_target; - bool has_saved_target; + + /// \brief This state is saved, with the PC pointing to the target of a GOTO + bool has_saved_jump_target; + + /// \brief This state is saved, with the PC pointing to the next instruction + /// of a GOTO + bool has_saved_next_instruction; bool saved_target_is_backwards; private: diff --git a/src/goto-symex/path_storage.cpp b/src/goto-symex/path_storage.cpp new file mode 100644 index 00000000000..58a2498a07d --- /dev/null +++ b/src/goto-symex/path_storage.cpp @@ -0,0 +1,125 @@ +/*******************************************************************\ + +Module: Path Storage + +Author: Kareem Khazem + +\*******************************************************************/ + +#include "path_storage.h" + +#include + +#include +#include + +// _____________________________________________________________________________ +// path_lifot + +path_storaget::patht &path_lifot::private_peek() +{ + last_peeked = paths.end(); + --last_peeked; + return paths.back(); +} + +void path_lifot::push( + const path_storaget::patht &next_instruction, + const path_storaget::patht &jump_target) +{ + paths.push_back(next_instruction); + paths.push_back(jump_target); +} + +void path_lifot::private_pop() +{ + PRECONDITION(last_peeked != paths.end()); + paths.erase(last_peeked); + last_peeked = paths.end(); +} + +std::size_t path_lifot::size() const +{ + return paths.size(); +} + +// _____________________________________________________________________________ +// path_fifot + +path_storaget::patht &path_fifot::private_peek() +{ + return paths.front(); +} + +void path_fifot::push( + const path_storaget::patht &next_instruction, + const path_storaget::patht &jump_target) +{ + paths.push_back(next_instruction); + paths.push_back(jump_target); +} + +void path_fifot::private_pop() +{ + paths.pop_front(); +} + +std::size_t path_fifot::size() const +{ + return paths.size(); +} + +// _____________________________________________________________________________ +// path_strategy_choosert + +std::string path_strategy_choosert::show_strategies() const +{ + std::stringstream ss; + for(auto &pair : strategies) + ss << pair.second.first; + return ss.str(); +} + +void path_strategy_choosert::set_path_strategy_options( + const cmdlinet &cmdline, + optionst &options, + messaget &message) const +{ + if(cmdline.isset("paths")) + { + options.set_option("paths", true); + std::string strategy = cmdline.get_value("paths"); + if(!is_valid_strategy(strategy)) + { + message.error() << "Unknown strategy '" << strategy + << "'. Pass the --show-symex-strategies flag to list " + "available strategies." + << message.eom; + exit(CPROVER_EXIT_USAGE_ERROR); + } + options.set_option("exploration-strategy", strategy); + } + else + options.set_option("exploration-strategy", default_strategy()); +} + +path_strategy_choosert::path_strategy_choosert() + : strategies( + {{"lifo", + {" lifo next instruction is pushed before\n" + " goto target; paths are popped in\n" + " last-in, first-out order. Explores\n" + " the program tree depth-first.\n", + []() { // NOLINT(whitespace/braces) + return util_make_unique(); + }}}, + {"fifo", + {" fifo next instruction is pushed before\n" + " goto target; paths are popped in\n" + " first-in, first-out order. Explores\n" + " the program tree breadth-first.\n", + []() { // NOLINT(whitespace/braces) + return util_make_unique(); + }}}}) +{ +} diff --git a/src/goto-symex/path_storage.h b/src/goto-symex/path_storage.h new file mode 100644 index 00000000000..e5d5120cfea --- /dev/null +++ b/src/goto-symex/path_storage.h @@ -0,0 +1,165 @@ +/// \file path_storage.h +/// \brief Storage of symbolic execution paths to resume +/// \author Kareem Khazem + +#ifndef CPROVER_GOTO_SYMEX_PATH_STORAGE_H +#define CPROVER_GOTO_SYMEX_PATH_STORAGE_H + +#include "goto_symex_state.h" +#include "symex_target_equation.h" + +#include +#include +#include +#include + +#include + +/// \brief Storage for symbolic execution paths to be resumed later +/// +/// This data structure supports saving partially-executed symbolic +/// execution \ref path_storaget::patht "paths" so that their execution can +/// be halted and resumed later. The choice of which path should be +/// resumed next is implemented by subtypes of this abstract class. +class path_storaget +{ +public: + /// \brief Information saved at a conditional goto to resume execution + struct patht + { + symex_target_equationt equation; + goto_symex_statet state; + + explicit patht(const symex_target_equationt &e, const goto_symex_statet &s) + : equation(e), state(s, &equation) + { + } + + explicit patht(const patht &other) + : equation(other.equation), state(other.state, &equation) + { + } + }; + + virtual ~path_storaget() = default; + + /// \brief Reference to the next path to resume + patht &peek() + { + PRECONDITION(!empty()); + return private_peek(); + } + + /// \brief Add paths to resume to the storage + /// + /// Symbolic execution is suspended when we reach a conditional goto + /// instruction with two successors. Thus, we always add a pair of paths to + /// the path storage. + /// + /// \param next_instruction the instruction following the goto instruction + /// \param jump_target the target instruction of the goto instruction + virtual void + push(const patht &next_instruction, const patht &jump_target) = 0; + + /// \brief Remove the next path to resume from the storage + void pop() + { + PRECONDITION(!empty()); + private_pop(); + } + + /// \brief How many paths does this storage contain? + virtual std::size_t size() const = 0; + + /// \brief Is this storage empty? + bool empty() const + { + return size() == 0; + }; + +private: + // Derived classes should override these methods, allowing the base class to + // enforce preconditions. + virtual patht &private_peek() = 0; + virtual void private_pop() = 0; +}; + +/// \brief LIFO save queue: depth-first search, try to finish paths +class path_lifot : public path_storaget +{ +public: + void push(const patht &, const patht &) override; + std::size_t size() const override; + +protected: + std::list::iterator last_peeked; + std::list paths; + +private: + patht &private_peek() override; + void private_pop() override; +}; + +/// \brief FIFO save queue: paths are resumed in the order that they were saved +class path_fifot : public path_storaget +{ +public: + void push(const patht &, const patht &) override; + std::size_t size() const override; + +protected: + std::list paths; + +private: + patht &private_peek() override; + void private_pop() override; +}; + +/// \brief Factory and information for path_storaget +class path_strategy_choosert +{ +public: + path_strategy_choosert(); + + /// \brief suitable for displaying as a front-end help message + std::string show_strategies() const; + + /// \brief is there a factory constructor for the named strategy? + bool is_valid_strategy(const std::string strategy) const + { + return strategies.find(strategy) != strategies.end(); + } + + /// \brief Factory for a path_storaget + /// + /// Ensure that path_strategy_choosert::is_valid_strategy() returns true for a + /// particular string before calling this function on that string. + std::unique_ptr get(const std::string strategy) const + { + auto found = strategies.find(strategy); + INVARIANT( + found != strategies.end(), "Unknown strategy '" + strategy + "'."); + return found->second.second(); + } + + /// \brief add `paths` and `exploration-strategy` option, suitable to be + /// invoked from front-ends. + void + set_path_strategy_options(const cmdlinet &, optionst &, messaget &) const; + +protected: + std::string default_strategy() const + { + return "lifo"; + } + + /// Map from the name of a strategy (to be supplied on the command line), to + /// the help text for that strategy and a factory thunk returning a pointer to + /// a derived class of path_storaget that implements that strategy. + std::map()>>> + strategies; +}; + +#endif /* CPROVER_GOTO_SYMEX_PATH_STORAGE_H */ diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index e25add14741..5951cd8284c 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -152,7 +152,7 @@ void goto_symext::symex_goto(statet &state) // new_state_pc for later. But if we're executing from a saved state, then // new_state_pc should be the state that we saved from earlier, so let's // execute that instead. - if(state.has_saved_target) + if(state.has_saved_jump_target) { INVARIANT( new_state_pc == state.saved_target, @@ -169,28 +169,46 @@ void goto_symext::symex_goto(statet &state) goto_programt::const_targett tmp = new_state_pc; new_state_pc = state_pc; state_pc = tmp; - log.debug() << "Resuming from '" << state_pc->code.source_location() << "'" - << log.eom; + + log.debug() << "Resuming from jump target '" << state_pc->source_location + << "'" << log.eom; + } + else if(state.has_saved_next_instruction) + { + log.debug() << "Resuming from next instruction '" + << state_pc->source_location << "'" << log.eom; } else if(options.get_bool_option("paths")) { - // At this point, `state_pc` is the instruction we should execute - // immediately, and `new_state_pc` is the instruction that we should execute - // later (after we've finished exploring this branch). For path-based - // exploration, save `new_state_pc` to the saved state that we will resume - // executing from, so that goto_symex::symex_goto() knows that we've already - // explored the branch starting from `state_pc` when it is later called at - // this branch. - branch_pointt branch_point(target, state); - branch_point.state.saved_target = new_state_pc; - branch_point.state.has_saved_target = true; + // We should save both the instruction after this goto, and the target of + // the goto. + + path_storaget::patht next_instruction(target, state); + next_instruction.state.saved_target = state_pc; + next_instruction.state.has_saved_next_instruction = true; + next_instruction.state.saved_target_is_backwards = !forward; + + path_storaget::patht jump_target(target, state); + jump_target.state.saved_target = new_state_pc; + jump_target.state.has_saved_jump_target = true; // `forward` tells us where the branch we're _currently_ executing is // pointing to; this needs to be inverted for the branch that we're saving, // so let its truth value for `backwards` be the same as ours for `forward`. - branch_point.state.saved_target_is_backwards = forward; - branch_worklist.push_back(branch_point); - log.debug() << "Saving '" << new_state_pc->source_location << "'" + jump_target.state.saved_target_is_backwards = forward; + + log.debug() << "Saving next instruction '" + << next_instruction.state.saved_target->source_location << "'" + << log.eom; + log.debug() << "Saving jump target '" + << jump_target.state.saved_target->source_location << "'" << log.eom; + path_storage.push(next_instruction, jump_target); + + // It is now up to the caller of symex to decide which path to continue + // executing. Signal to the caller that states have been pushed (therefore + // symex has not yet completed and must be resumed), and bail out. + should_pause_symex = true; + return; } // put into state-queue @@ -241,7 +259,7 @@ void goto_symext::symex_goto(statet &state) state.rename(guard_expr, ns); } - if(state.has_saved_target) + if(state.has_saved_jump_target) { if(forward) state.guard.add(guard_expr); diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 97c2c127c22..83e5b7e22ae 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -149,6 +149,8 @@ void goto_symext::symex_threaded_step( statet &state, const get_goto_functiont &get_goto_function) { symex_step(get_goto_function, state); + if(should_pause_symex) + return; // is there another thread to execute? if(state.call_stack().empty() && @@ -197,10 +199,15 @@ void goto_symext::symex_with_state( PRECONDITION(state.top().end_of_function->is_end_function()); symex_threaded_step(state, get_goto_function); + if(should_pause_symex) + return; while(!state.call_stack().empty()) { - state.has_saved_target = false; + state.has_saved_jump_target = false; + state.has_saved_next_instruction = false; symex_threaded_step(state, get_goto_function); + if(should_pause_symex) + return; } // Clients may need to construct a namespace with both the names in @@ -227,7 +234,6 @@ void goto_symext::resume_symex_from_saved_state( // its equation member point to the (valid) equation passed as an argument. statet state(saved_state, saved_equation); - symex_transition(state, state.source.pc); // Do NOT do the same initialization that `symex_with_state` does for a // fresh state, as that would clobber the saved state's program counter symex_with_state( diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 26427ffe703..72c7c1eacdd 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -63,7 +64,8 @@ Author: Daniel Kroening, kroening@kroening.com jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv): parse_options_baset(JBMC_OPTIONS, argc, argv), messaget(ui_message_handler), - ui_message_handler(cmdline, "JBMC " CBMC_VERSION) + ui_message_handler(cmdline, "JBMC " CBMC_VERSION), + path_strategy_chooser() { } @@ -73,7 +75,8 @@ ::jbmc_parse_optionst::jbmc_parse_optionst( const std::string &extra_options): parse_options_baset(JBMC_OPTIONS+extra_options, argc, argv), messaget(ui_message_handler), - ui_message_handler(cmdline, "JBMC " CBMC_VERSION) + ui_message_handler(cmdline, "JBMC " CBMC_VERSION), + path_strategy_chooser() { } @@ -100,6 +103,14 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) exit(1); // should contemplate EX_USAGE from sysexits.h } + if(cmdline.isset("show-symex-strategies")) + { + std::cout << path_strategy_chooser.show_strategies(); + exit(CPROVER_EXIT_SUCCESS); + } + + path_strategy_chooser.set_path_strategy_options(cmdline, options, *this); + if(cmdline.isset("program-only")) options.set_option("program-only", true); @@ -533,7 +544,12 @@ int jbmc_parse_optionst::doit() // The `configure_bmc` callback passed will enable enum-unwind-static if // applicable. return bmct::do_language_agnostic_bmc( - options, goto_model, ui_message_handler.get_ui(), *this, configure_bmc); + path_strategy_chooser, + options, + goto_model, + ui_message_handler.get_ui(), + *this, + configure_bmc); } else { @@ -573,6 +589,7 @@ int jbmc_parse_optionst::doit() // applicable. return bmct::do_language_agnostic_bmc( + path_strategy_chooser, options, lazy_goto_model, ui_message_handler.get_ui(), diff --git a/src/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h index 22871752ab4..d0c1919d93c 100644 --- a/src/jbmc/jbmc_parse_options.h +++ b/src/jbmc/jbmc_parse_options.h @@ -27,6 +27,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include class bmct; @@ -103,6 +105,7 @@ class jbmc_parse_optionst: protected: ui_message_handlert ui_message_handler; std::unique_ptr cover_config; + path_strategy_choosert path_strategy_chooser; void eval_verbosity(); void get_command_line_options(optionst &); diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt index 5b4cdf42335..300f6c08fef 100644 --- a/unit/CMakeLists.txt +++ b/unit/CMakeLists.txt @@ -43,6 +43,7 @@ target_link_libraries( java_bytecode goto-programs goto-instrument-lib + cbmc-lib ) add_test( diff --git a/unit/Makefile b/unit/Makefile index b150bfa632c..b7b2ceef442 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -30,6 +30,7 @@ SRC += unit_tests.cpp \ java_bytecode/java_types/java_type_from_string.cpp \ java_bytecode/java_utils_test.cpp \ java_bytecode/inherited_static_fields/inherited_static_fields.cpp \ + path_strategies.cpp \ pointer-analysis/custom_value_set_analysis.cpp \ sharing_node.cpp \ solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp \ @@ -71,6 +72,34 @@ cprover.dir: testing-utils.dir: $(MAKE) $(MAKEARGS) -C testing-utils +# We need to link bmc.o to the unit test, so here's everything it depends on... +BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \ + ../src/cbmc/bmc$(OBJEXT) \ + ../src/cbmc/bmc_cover$(OBJEXT) \ + ../src/cbmc/bv_cbmc$(OBJEXT) \ + ../src/cbmc/cbmc_dimacs$(OBJEXT) \ + ../src/cbmc/cbmc_languages$(OBJEXT) \ + ../src/cbmc/cbmc_parse_options$(OBJEXT) \ + ../src/cbmc/cbmc_solvers$(OBJEXT) \ + ../src/cbmc/counterexample_beautification$(OBJEXT) \ + ../src/cbmc/fault_localization$(OBJEXT) \ + ../src/cbmc/show_vcc$(OBJEXT) \ + ../src/cbmc/symex_bmc$(OBJEXT) \ + ../src/cbmc/symex_coverage$(OBJEXT) \ + ../src/cbmc/xml_interface$(OBJEXT) \ + ../src/jsil/expr2jsil$(OBJEXT) \ + ../src/jsil/jsil_convert$(OBJEXT) \ + ../src/jsil/jsil_entry_point$(OBJEXT) \ + ../src/jsil/jsil_internal_additions$(OBJEXT) \ + ../src/jsil/jsil_language$(OBJEXT) \ + ../src/jsil/jsil_lex.yy$(OBJEXT) \ + ../src/jsil/jsil_parser$(OBJEXT) \ + ../src/jsil/jsil_parse_tree$(OBJEXT) \ + ../src/jsil/jsil_typecheck$(OBJEXT) \ + ../src/jsil/jsil_types$(OBJEXT) \ + ../src/jsil/jsil_y.tab$(OBJEXT) \ + # Empty last line +# CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \ ../src/miniz/miniz$(OBJEXT) \ ../src/ansi-c/ansi-c$(LIBEXT) \ @@ -86,6 +115,7 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \ ../src/assembler/assembler$(LIBEXT) \ ../src/analyses/analyses$(LIBEXT) \ ../src/solvers/solvers$(LIBEXT) \ + $(BMC_DEPS) # Empty last line OBJ += $(CPROVER_LIBS) testing-utils/testing-utils$(LIBEXT) diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp new file mode 100644 index 00000000000..171fe71d7ee --- /dev/null +++ b/unit/path_strategies.cpp @@ -0,0 +1,364 @@ +/*******************************************************************\ + +Module: Path Strategy Tests + +Author: Kareem Khazem , 2018 + +\*******************************************************************/ + +#include + +#include + +#include +#include +#include + +#include + +#include +#include +#include + +#include +#include + +#include +#include +#include +#include + +// The actual test suite. +// +// Whenever you add a new path exploration strategy 'my-cool-strategy', for each +// of the test programs (under the GIVEN macros), add a new test using a call to +// `check_with_strategy("my-cool-strategy", c, event_list)` where `event_list` +// is a list of the events that you expect to see during symbolic execution. +// Events are either resumes or results. +// +// Whenever symbolic execution pauses and picks a path to resume from, you +// should note the line number of the path you expect that path strategy to +// resume from. A resume is either a JUMP, meaning that it's the target of a +// `goto` instruction, or a NEXT, meaning that it's the instruction following a +// `goto` instruction. +// +// Whenever symbolic execution reaches the end of a path, you should expect a +// result. Results are either SUCCESS, meaning that verification of that path +// succeeded, or FAILURE, meaning that there was an assertion failure on that +// path. +// +// To figure out what the events should be, run CBMC on the test program with +// your strategy with `--verbosity 10` and look out for lines like +// +// Resuming from jump target 'file nested-if/main.c line 13 function main' +// +// Resuming from next instruction 'file nested-if/main.c line 14 function main' +// +// VERIFICATION SUCCESSFUL +// +// VERIFICATION FAILED +// +// And note the order in which they occur. + +SCENARIO("path strategies") +{ + std::string c; + GIVEN("a simple conditional program") + { + c = + "/* 1 */ int main() \n" + "/* 2 */ { \n" + "/* 3 */ int x; \n" + "/* 4 */ if(x) \n" + "/* 5 */ x = 1; \n" + "/* 6 */ else \n" + "/* 7 */ x = 0; \n" + "/* 8 */ } \n"; + + const unsigned unwind_limit = 0U; + + check_with_strategy( + "lifo", + c, + {symex_eventt::resume(symex_eventt::enumt::JUMP, 7), + symex_eventt::result(symex_eventt::enumt::SUCCESS), + symex_eventt::resume(symex_eventt::enumt::NEXT, 5), + symex_eventt::result(symex_eventt::enumt::SUCCESS)}, + unwind_limit); + check_with_strategy( + "fifo", + c, + {symex_eventt::resume(symex_eventt::enumt::NEXT, 5), + symex_eventt::result(symex_eventt::enumt::SUCCESS), + symex_eventt::resume(symex_eventt::enumt::JUMP, 7), + symex_eventt::result(symex_eventt::enumt::SUCCESS)}, + unwind_limit); + } + + GIVEN("a program with nested conditionals") + { + c = + "/* 1 */ int main() \n" + "/* 2 */ { \n" + "/* 3 */ int x, y; \n" + "/* 4 */ if(x) \n" + "/* 5 */ { \n" + "/* 6 */ if(y) \n" + "/* 7 */ y = 1; \n" + "/* 8 */ else \n" + "/* 9 */ y = 0; \n" + "/* 10 */ } \n" + "/* 11 */ else \n" + "/* 12 */ { \n" + "/* 13 */ if(y) \n" + "/* 14 */ y = 1; \n" + "/* 15 */ else \n" + "/* 16 */ y = 0; \n" + "/* 17 */ } \n" + "/* 18 */ } \n"; + + const unsigned unwind_limit = 0U; + + check_with_strategy( + "lifo", + c, + {// Outer else, inner else + symex_eventt::resume(symex_eventt::enumt::JUMP, 13), + symex_eventt::resume(symex_eventt::enumt::JUMP, 16), + symex_eventt::result(symex_eventt::enumt::SUCCESS), + // Outer else, inner if + symex_eventt::resume(symex_eventt::enumt::NEXT, 14), + symex_eventt::result(symex_eventt::enumt::SUCCESS), + // Outer if, inner else + symex_eventt::resume(symex_eventt::enumt::NEXT, 6), + symex_eventt::resume(symex_eventt::enumt::JUMP, 9), + symex_eventt::result(symex_eventt::enumt::SUCCESS), + // Outer if, inner if + symex_eventt::resume(symex_eventt::enumt::NEXT, 7), + symex_eventt::result(symex_eventt::enumt::SUCCESS)}, + unwind_limit); + + check_with_strategy( + "fifo", + c, + {// Expand outer if, but don't continue depth-first + symex_eventt::resume(symex_eventt::enumt::NEXT, 6), + // Jump to outer else, but again don't continue depth-first + symex_eventt::resume(symex_eventt::enumt::JUMP, 13), + // Expand inner if of the outer if + symex_eventt::resume(symex_eventt::enumt::NEXT, 7), + // No more branch points, so complete the path + symex_eventt::result(symex_eventt::enumt::SUCCESS), + // Continue BFSing + symex_eventt::resume(symex_eventt::enumt::JUMP, 9), + symex_eventt::result(symex_eventt::enumt::SUCCESS), + symex_eventt::resume(symex_eventt::enumt::NEXT, 14), + symex_eventt::result(symex_eventt::enumt::SUCCESS), + symex_eventt::resume(symex_eventt::enumt::JUMP, 16), + symex_eventt::result(symex_eventt::enumt::SUCCESS)}, + unwind_limit); + } + + GIVEN("a loop program to test functional correctness") + { + c = + "/* 1 */ int main() \n" + "/* 2 */ { \n" + "/* 3 */ int x; \n" + "/* 4 */ __CPROVER_assume(x == 1); \n" + "/* 5 */ \n" + "/* 6 */ while(x) \n" + "/* 7 */ --x; \n" + "/* 8 */ \n" + "/* 9 */ assert(x); \n" + "/* 10 */ } \n"; + + const unsigned unwind_limit = 2U; + + check_with_strategy( + "lifo", + c, + { + // The path where we skip the loop body. Successful because the path is + // implausible, we cannot have skipped the body if x == 1. + symex_eventt::resume(symex_eventt::enumt::JUMP, 9), + symex_eventt::result(symex_eventt::enumt::SUCCESS), + + // Enter the loop body once. Since we decrement x, the assertion should + // fail. + symex_eventt::resume(symex_eventt::enumt::NEXT, 7), + symex_eventt::resume(symex_eventt::enumt::JUMP, 9), + symex_eventt::result(symex_eventt::enumt::FAILURE), + + // The path where we enter the loop body twice. Successful because + // infeasible. + symex_eventt::resume(symex_eventt::enumt::NEXT, 7), + symex_eventt::result(symex_eventt::enumt::SUCCESS), + }, + unwind_limit); + + check_with_strategy( + "fifo", + c, + { + // The path where we skip the loop body. Successful because the path is + // implausible, we cannot have skipped the body if x == 1. + // + // In this case, although we resume from line 7, we don't proceed until + // the end of the path after executing line 7. + symex_eventt::resume(symex_eventt::enumt::NEXT, 7), + symex_eventt::resume(symex_eventt::enumt::JUMP, 9), + symex_eventt::result(symex_eventt::enumt::SUCCESS), + + // Pop line 7 that we saved from above, and execute the loop a second + // time. Successful, since this path is infeasible. + symex_eventt::resume(symex_eventt::enumt::NEXT, 7), + symex_eventt::result(symex_eventt::enumt::SUCCESS), + + // Pop line 7 that we saved from above and bail out. That corresponds to + // executing the loop once, decrementing x to 0; assert(x) should fail. + symex_eventt::resume(symex_eventt::enumt::JUMP, 9), + symex_eventt::result(symex_eventt::enumt::FAILURE), + }, + unwind_limit); + } +} + +// In theory, there should be no need to change the code below when adding new +// test cases... + +void symex_eventt::validate_result( + listt &events, + const safety_checkert::resultt result) +{ + INFO( + "Expecting result to be '" + << (result == safety_checkert::resultt::SAFE ? "success" : "failure") + << "'"); + + REQUIRE(result != safety_checkert::resultt::ERROR); + + if(result == safety_checkert::resultt::SAFE) + { + REQUIRE(!events.empty()); + REQUIRE(events.front().first == symex_eventt::enumt::SUCCESS); + events.pop_front(); + } + else if(result == safety_checkert::resultt::UNSAFE) + { + REQUIRE(!events.empty()); + REQUIRE(events.front().first == symex_eventt::enumt::FAILURE); + events.pop_front(); + } +} + +void symex_eventt::validate_resume( + listt &events, + const goto_symex_statet &state) +{ + REQUIRE(!events.empty()); + + int dst = std::stoi(state.saved_target->source_location.get_line().c_str()); + + if(state.has_saved_jump_target) + { + INFO("Expecting resume to be 'jump' to line " << dst); + REQUIRE(events.front().first == symex_eventt::enumt::JUMP); + } + else if(state.has_saved_next_instruction) + { + INFO("Expecting resume to be 'next' to line " << dst); + REQUIRE(events.front().first == symex_eventt::enumt::NEXT); + } + else + REQUIRE(false); + + REQUIRE(events.front().second == dst); + + events.pop_front(); +} + +// This is a simplified version of bmct::do_language_agnostic_bmc, without all +// the edge cases to deal with java programs, bytecode loaded on demand, etc. We +// need to replicate some of this stuff because the worklist is a local variable +// of do_language_agnostic_bmc, and we need to check the worklist every time +// symex returns. +void _check_with_strategy( + const std::string &strategy, + const std::string &program, + const unsigned unwind_limit, + symex_eventt::listt &events) +{ + temporary_filet tmp("path-explore_", ".c"); + std::ofstream of(tmp().c_str()); + REQUIRE(of.is_open()); + + of << program << std::endl; + of.close(); + + register_language(new_ansi_c_language); + cmdlinet cmdline; + cmdline.args.push_back(tmp()); + config.main = "main"; + config.set(cmdline); + + optionst opts; + cbmc_parse_optionst::set_default_options(opts); + opts.set_option("paths", true); + opts.set_option("exploration-strategy", strategy); + + if(unwind_limit) + { + opts.set_option("unwind", unwind_limit); + cmdline.set("unwind", std::to_string(unwind_limit)); + } + + ui_message_handlert mh(cmdline, "path-explore"); + messaget log(mh); + + path_strategy_choosert chooser; + REQUIRE(chooser.is_valid_strategy(strategy)); + std::unique_ptr worklist = chooser.get(strategy); + + goto_modelt gm; + int ret; + ret = cbmc_parse_optionst::get_goto_program(gm, opts, cmdline, log, mh); + REQUIRE(ret == -1); + + cbmc_solverst solvers(opts, gm.get_symbol_table(), mh); + solvers.set_ui(mh.get_ui()); + std::unique_ptr cbmc_solver = solvers.get_solver(); + prop_convt &pc = cbmc_solver->prop_conv(); + std::function callback = []() { return false; }; + + bmct bmc(opts, gm.get_symbol_table(), mh, pc, *worklist, callback); + bmc.set_ui(mh.get_ui()); + safety_checkert::resultt result = bmc.run(gm); + symex_eventt::validate_result(events, result); + + while(!worklist->empty()) + { + cbmc_solverst solvers(opts, gm.get_symbol_table(), mh); + solvers.set_ui(mh.get_ui()); + cbmc_solver = solvers.get_solver(); + prop_convt &pc = cbmc_solver->prop_conv(); + path_storaget::patht &resume = worklist->peek(); + + symex_eventt::validate_resume(events, resume.state); + + path_explorert pe( + opts, + gm.get_symbol_table(), + mh, + pc, + resume.equation, + resume.state, + *worklist, + callback); + result = pe.run(gm); + + symex_eventt::validate_result(events, result); + worklist->pop(); + } + REQUIRE(events.empty()); +} diff --git a/unit/path_strategies.h b/unit/path_strategies.h new file mode 100644 index 00000000000..c1f4c63c8d1 --- /dev/null +++ b/unit/path_strategies.h @@ -0,0 +1,62 @@ +/// \file Test for path strategies set through `cbmc --paths ...` +/// +/// \author Kareem Khazem + +#ifndef CPROVER_PATH_STRATEGIES_H +#define CPROVER_PATH_STRATEGIES_H + +#include +#include + +#include + +/// \brief Events that we expect to happen during path exploration +/// +/// See the description in the .cpp file on how to use this class. +struct symex_eventt +{ +public: + enum class enumt + { + JUMP, + NEXT, + SUCCESS, + FAILURE + }; + typedef std::pair pairt; + typedef std::list listt; + + static pairt resume(enumt kind, int location) + { + return pairt(kind, location); + } + + static pairt result(enumt kind) + { + return pairt(kind, -1); + } + + static void + validate_result(listt &events, const safety_checkert::resultt result); + + static void validate_resume(listt &events, const goto_symex_statet &state); +}; + +void _check_with_strategy( + const std::string &strategy, + const std::string &program, + const unsigned unwind_limit, + symex_eventt::listt &events); + +/// Call this one, not the underscore version +void check_with_strategy( + const std::string &strategy, + const std::string &program, + symex_eventt::listt events, + const unsigned unwind_limit) +{ + WHEN("strategy is '" + strategy + "'") + _check_with_strategy(strategy, program, unwind_limit, events); +} + +#endif // CPROVER_PATH_STRATEGIES_H