replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Merge pull request #3797 from peterschrammel/refactor-path-strategy-chooser 

Remove path strategy chooser from driver
This commit is contained in:
Peter Schrammel 2019-01-16 18:55:34 +00:00 committed by GitHub
parent af893778b2 50a9ef1570
commit 8984eb90ff
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
9 changed files with 83 additions and 104 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
jbmc/src/jbmc/jbmc_parse_options.cpp
View File

@ -47,6 +47,8 @@ Author: Daniel Kroening, kroening@kroening.com
#include <goto-instrument/reachability_slicer.h>
#include <goto-instrument/nondet_static.h>
#include <goto-symex/path_storage.h>
#include <linking/static_lifetime_init.h>
#include <pointer-analysis/add_failed_symbols.h>
@ -67,8 +69,7 @@ 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, std::string("JBMC ") + CBMC_VERSION),
path_strategy_chooser()
ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION)
{
}
@ -78,8 +79,7 @@ jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv)
const std::string &extra_options)
: parse_options_baset(JBMC_OPTIONS + extra_options, argc, argv),
messaget(ui_message_handler),
ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION),
path_strategy_chooser()
ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION)
{
}
@ -119,11 +119,11 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
if(cmdline.isset("show-symex-strategies"))
{
std::cout << path_strategy_chooser.show_strategies();
status() << show_path_strategies() << eom;
exit(CPROVER_EXIT_SUCCESS);
}
path_strategy_chooser.set_path_strategy_options(cmdline, options, *this);
parse_path_strategy_options(cmdline, options, ui_message_handler);
if(cmdline.isset("program-only"))
options.set_option("program-only", true);
@ -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_chooser,
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_chooser,
options,
lazy_goto_model,
ui_message_handler,

3
jbmc/src/jbmc/jbmc_parse_options.h
View File

@ -28,8 +28,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include <goto-programs/lazy_goto_model.h>
#include <goto-programs/show_properties.h>
#include <goto-symex/path_storage.h>
#include <solvers/refinement/string_refinement.h>
#include <java_bytecode/java_bytecode_language.h>
@ -120,7 +118,6 @@ public:
protected:
ui_message_handlert ui_message_handler;
path_strategy_choosert path_strategy_chooser;
java_object_factory_parameterst object_factory_params;
bool stub_objects_are_not_null;

8
src/cbmc/bmc.cpp
View File

@ -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,
@ -280,10 +277,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
{
solver_factoryt solvers(

1
src/cbmc/bmc.h
View File

@ -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,

14
src/cbmc/cbmc_parse_options.cpp
View File

@ -59,6 +59,8 @@ Author: Daniel Kroening, kroening@kroening.com
#include <goto-instrument/nondet_static.h>
#include <goto-instrument/cover.h>
#include <goto-symex/path_storage.h>
#include <pointer-analysis/add_failed_symbols.h>
#include <langapi/mode.h>
@ -69,8 +71,7 @@ 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, std::string("CBMC ") + CBMC_VERSION),
path_strategy_chooser()
ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION)
{
}
@ -81,8 +82,7 @@ cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv)
: parse_options_baset(CBMC_OPTIONS + extra_options, argc, argv),
xml_interfacet(cmdline),
messaget(ui_message_handler),
ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION),
path_strategy_chooser()
ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION)
{
}
@ -143,11 +143,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
if(cmdline.isset("show-symex-strategies"))
{
std::cout << path_strategy_chooser.show_strategies();
status() << show_path_strategies() << eom;
exit(CPROVER_EXIT_SUCCESS);
}
path_strategy_chooser.set_path_strategy_options(cmdline, options, *this);
parse_path_strategy_options(cmdline, options, ui_message_handler);
if(cmdline.isset("program-only"))
options.set_option("program-only", true);
@ -554,7 +554,7 @@ int cbmc_parse_optionst::doit()
}
return bmct::do_language_agnostic_bmc(
path_strategy_chooser, options, goto_model, ui_message_handler);
options, goto_model, ui_message_handler);
}
bool cbmc_parse_optionst::set_properties()

1
src/cbmc/cbmc_parse_options.h
View File

@ -116,7 +116,6 @@ public:
protected:
goto_modelt goto_model;
ui_message_handlert ui_message_handler;
const path_strategy_choosert path_strategy_chooser;
void register_languages();
void get_command_line_options(optionst &);

85
src/goto-symex/path_storage.cpp
View File

@ -82,54 +82,77 @@ 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();
}
void path_strategy_choosert::set_path_strategy_options(
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,
messaget &message) const
message_handlert &message_handler)
{
messaget log(message_handler);
if(cmdline.isset("paths"))
{
options.set_option("paths", true);
std::string strategy = cmdline.get_value("paths");
if(!is_valid_strategy(strategy))
if(!is_valid_path_strategy(strategy))
{
message.error() << "Unknown strategy '" << strategy
<< "'. Pass the --show-symex-strategies flag to list "
"available strategies."
<< message.eom;
log.error() << "Unknown strategy '" << strategy
<< "'. Pass the --show-symex-strategies flag to list "
"available strategies."
<< messaget::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<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>();
}}}})
{
{
options.set_option("exploration-strategy", default_path_strategy());
}
}

56
src/goto-symex/path_storage.h
View File

@ -125,51 +125,21 @@ 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();
}
/// 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 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();
}
/// \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<const std::string,
std::pair<const std::string,
const std::function<std::unique_ptr<path_storaget>()>>>
strategies;
};
/// \brief add `paths` and `exploration-strategy` option, suitable to be
/// invoked from front-ends.
void parse_path_strategy_options(
const cmdlinet &,
optionst &,
message_handlert &);
#endif /* CPROVER_GOTO_SYMEX_PATH_STORAGE_H */

5
unit/path_strategies.cpp
View File

@ -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;