diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 246a17fdcd..5aa17e58d7 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -119,7 +119,7 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("show-symex-strategies")) { - status() << path_strategy_choosert().show_strategies() << eom; + status() << show_path_strategies() << eom; exit(CPROVER_EXIT_SUCCESS); } @@ -573,7 +573,6 @@ int jbmc_parse_optionst::doit() // The `configure_bmc` callback passed will enable enum-unwind-static if // applicable. return bmct::do_language_agnostic_bmc( - path_strategy_choosert(), options, goto_model, ui_message_handler, @@ -618,7 +617,6 @@ int jbmc_parse_optionst::doit() // The `configure_bmc` callback passed will enable enum-unwind-static if // applicable. return bmct::do_language_agnostic_bmc( - path_strategy_choosert(), options, lazy_goto_model, ui_message_handler, diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 282c749c90..14ad71cdf6 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -255,8 +255,6 @@ safety_checkert::resultt bmct::stop_on_fail() /// Perform core BMC, using an abstract model to supply GOTO function bodies /// (perhaps created on demand). -/// \param path_strategy_chooser: controls whether symex generates a single -/// large equation for the whole program or an equation per path /// \param opts: command-line options affecting BMC /// \param model: provides goto function bodies and the symbol table, perhaps /// creating those function bodies on demand. @@ -266,7 +264,6 @@ safety_checkert::resultt bmct::stop_on_fail() /// \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, ui_message_handlert &ui, @@ -279,10 +276,7 @@ int bmct::do_language_agnostic_bmc( messaget message(ui); 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); + worklist = get_path_strategy(strategy); try { { diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index 0fbfa2f0da..0015389d89 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -118,7 +118,6 @@ public: } static int do_language_agnostic_bmc( - const path_strategy_choosert &path_strategy_chooser, const optionst &opts, abstract_goto_modelt &goto_model, ui_message_handlert &ui, diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 910e31e97f..c1db43c554 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -143,7 +143,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("show-symex-strategies")) { - status() << path_strategy_choosert().show_strategies() << eom; + status() << show_path_strategies() << eom; exit(CPROVER_EXIT_SUCCESS); } @@ -554,7 +554,7 @@ int cbmc_parse_optionst::doit() } return bmct::do_language_agnostic_bmc( - path_strategy_choosert(), options, goto_model, ui_message_handler); + options, goto_model, ui_message_handler); } bool cbmc_parse_optionst::set_properties() diff --git a/src/goto-symex/path_storage.cpp b/src/goto-symex/path_storage.cpp index b7cdb4265f..55a5149d0f 100644 --- a/src/goto-symex/path_storage.cpp +++ b/src/goto-symex/path_storage.cpp @@ -82,26 +82,66 @@ void path_fifot::clear() // _____________________________________________________________________________ // path_strategy_choosert -std::string path_strategy_choosert::show_strategies() const +static const std::map< + const std::string, + std::pair< + const std::string, + const std::function()>>> + path_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(); + }}}}); + +std::string show_path_strategies() { std::stringstream ss; - for(auto &pair : strategies) + for(auto &pair : path_strategies) ss << pair.second.first; return ss.str(); } +std::string default_path_strategy() +{ + return "lifo"; +} + +bool is_valid_path_strategy(const std::string strategy) +{ + return path_strategies.find(strategy) != path_strategies.end(); +} + +std::unique_ptr get_path_strategy(const std::string strategy) +{ + auto found = path_strategies.find(strategy); + INVARIANT( + found != path_strategies.end(), "Unknown strategy '" + strategy + "'."); + return found->second.second(); +} + void parse_path_strategy_options( const cmdlinet &cmdline, optionst &options, message_handlert &message_handler) { messaget log(message_handler); - path_strategy_choosert path_strategy_chooser; if(cmdline.isset("paths")) { options.set_option("paths", true); std::string strategy = cmdline.get_value("paths"); - if(!path_strategy_chooser.is_valid_strategy(strategy)) + if(!is_valid_path_strategy(strategy)) { log.error() << "Unknown strategy '" << strategy << "'. Pass the --show-symex-strategies flag to list " @@ -113,28 +153,6 @@ void parse_path_strategy_options( } else { - options.set_option( - "exploration-strategy", path_strategy_chooser.default_strategy()); + options.set_option("exploration-strategy", default_path_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 index 7f6f8fb6e6..981dac697e 100644 --- a/src/goto-symex/path_storage.h +++ b/src/goto-symex/path_storage.h @@ -125,47 +125,15 @@ private: 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_path_strategies(); - /// \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_path_strategy(const std::string strategy); - /// \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(); - } - - std::string default_strategy() const - { - return "lifo"; - } - -protected: - /// 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; -}; +/// Ensure that is_valid_strategy() returns true for a +/// particular string before calling this function on that string. +std::unique_ptr get_path_strategy(const std::string strategy); /// \brief add `paths` and `exploration-strategy` option, suitable to be /// invoked from front-ends. diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp index be46c93d03..05125ce828 100644 --- a/unit/path_strategies.cpp +++ b/unit/path_strategies.cpp @@ -368,9 +368,8 @@ void _check_with_strategy( mh.set_verbosity(0); messaget log(mh); - path_strategy_choosert chooser; - REQUIRE(chooser.is_valid_strategy(strategy)); - std::unique_ptr worklist = chooser.get(strategy); + REQUIRE(is_valid_path_strategy(strategy)); + std::unique_ptr worklist = get_path_strategy(strategy); goto_modelt gm; int ret;