Refactor path strategy chooser into free functions
Since keeping an instance is not an option, we should avoid having to create an instance on every stateless function call.
This commit is contained in:
parent
6ce9bf4dfd
commit
50a9ef1570
|
@ -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,
|
||||
|
|
|
@ -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<path_storaget> 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
|
||||
{
|
||||
{
|
||||
|
|
|
@ -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,
|
||||
|
|
|
@ -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()
|
||||
|
|
|
@ -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<std::unique_ptr<path_storaget>()>>>
|
||||
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<path_lifot>();
|
||||
}}},
|
||||
{"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<path_fifot>();
|
||||
}}}});
|
||||
|
||||
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<path_storaget> 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<path_lifot>();
|
||||
}}},
|
||||
{"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<path_fifot>();
|
||||
}}}})
|
||||
{
|
||||
}
|
||||
|
|
|
@ -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<path_storaget> 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<const std::string,
|
||||
std::pair<const std::string,
|
||||
const std::function<std::unique_ptr<path_storaget>()>>>
|
||||
strategies;
|
||||
};
|
||||
/// Ensure that is_valid_strategy() returns true for a
|
||||
/// particular string before calling this function on that string.
|
||||
std::unique_ptr<path_storaget> get_path_strategy(const std::string strategy);
|
||||
|
||||
/// \brief add `paths` and `exploration-strategy` option, suitable to be
|
||||
/// invoked from front-ends.
|
||||
|
|
|
@ -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<path_storaget> worklist = chooser.get(strategy);
|
||||
REQUIRE(is_valid_path_strategy(strategy));
|
||||
std::unique_ptr<path_storaget> worklist = get_path_strategy(strategy);
|
||||
|
||||
goto_modelt gm;
|
||||
int ret;
|
||||
|
|
Loading…
Reference in New Issue