Skip to content

Commit 6ce9bf4

Browse files
peterschrammelpeterschrammel
committed
Make parse_path_strategy_options a function
Removes an unnecessary member from *bmc_parse_optionst. To implement an incremental_goto_checker for --paths, we have to encapsulate everything algorithm-specfic inside the incremental_goto_checker. We can only parse the option in the driver, but cannot pass on the path_strategy_chooser instance.
1 parent d2ea098 commit 6ce9bf4

File tree

6 files changed

+36
-33
lines changed

6 files changed

+36
-33
lines changed

‎jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,8 @@ Author: Daniel Kroening, [email protected]
4747
#include <goto-instrument/reachability_slicer.h>
4848
#include <goto-instrument/nondet_static.h>
4949

50+
#include <goto-symex/path_storage.h>
51+
5052
#include <linking/static_lifetime_init.h>
5153

5254
#include <pointer-analysis/add_failed_symbols.h>
@@ -67,8 +69,7 @@ Author: Daniel Kroening, [email protected]
6769
jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv)
6870
: parse_options_baset(JBMC_OPTIONS, argc, argv),
6971
messaget(ui_message_handler),
70-
ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION),
71-
path_strategy_chooser()
72+
ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION)
7273
{
7374
}
7475

@@ -78,8 +79,7 @@ ::jbmc_parse_optionst::jbmc_parse_optionst(
7879
const std::string &extra_options)
7980
: parse_options_baset(JBMC_OPTIONS + extra_options, argc, argv),
8081
messaget(ui_message_handler),
81-
ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION),
82-
path_strategy_chooser()
82+
ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION)
8383
{
8484
}
8585

@@ -119,11 +119,11 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
119119

120120
if(cmdline.isset("show-symex-strategies"))
121121
{
122-
std::cout << path_strategy_chooser.show_strategies();
122+
status() << path_strategy_choosert().show_strategies() << eom;
123123
exit(CPROVER_EXIT_SUCCESS);
124124
}
125125

126-
path_strategy_chooser.set_path_strategy_options(cmdline, options, *this);
126+
parse_path_strategy_options(cmdline, options, ui_message_handler);
127127

128128
if(cmdline.isset("program-only"))
129129
options.set_option("program-only", true);
@@ -573,7 +573,7 @@ int jbmc_parse_optionst::doit()
573573
// The `configure_bmc` callback passed will enable enum-unwind-static if
574574
// applicable.
575575
return bmct::do_language_agnostic_bmc(
576-
path_strategy_chooser,
576+
path_strategy_choosert(),
577577
options,
578578
goto_model,
579579
ui_message_handler,
@@ -618,7 +618,7 @@ int jbmc_parse_optionst::doit()
618618
// The `configure_bmc` callback passed will enable enum-unwind-static if
619619
// applicable.
620620
return bmct::do_language_agnostic_bmc(
621-
path_strategy_chooser,
621+
path_strategy_choosert(),
622622
options,
623623
lazy_goto_model,
624624
ui_message_handler,

‎jbmc/src/jbmc/jbmc_parse_options.h

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -28,8 +28,6 @@ Author: Daniel Kroening, [email protected]
2828
#include <goto-programs/lazy_goto_model.h>
2929
#include <goto-programs/show_properties.h>
3030

31-
#include <goto-symex/path_storage.h>
32-
3331
#include <solvers/refinement/string_refinement.h>
3432

3533
#include <java_bytecode/java_bytecode_language.h>
@@ -120,7 +118,6 @@ class jbmc_parse_optionst:
120118

121119
protected:
122120
ui_message_handlert ui_message_handler;
123-
path_strategy_choosert path_strategy_chooser;
124121
java_object_factory_parameterst object_factory_params;
125122
bool stub_objects_are_not_null;
126123

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,8 @@ Author: Daniel Kroening, [email protected]
5959
#include <goto-instrument/nondet_static.h>
6060
#include <goto-instrument/cover.h>
6161

62+
#include <goto-symex/path_storage.h>
63+
6264
#include <pointer-analysis/add_failed_symbols.h>
6365

6466
#include <langapi/mode.h>
@@ -69,8 +71,7 @@ cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv)
6971
: parse_options_baset(CBMC_OPTIONS, argc, argv),
7072
xml_interfacet(cmdline),
7173
messaget(ui_message_handler),
72-
ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION),
73-
path_strategy_chooser()
74+
ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION)
7475
{
7576
}
7677

@@ -81,8 +82,7 @@ ::cbmc_parse_optionst::cbmc_parse_optionst(
8182
: parse_options_baset(CBMC_OPTIONS + extra_options, argc, argv),
8283
xml_interfacet(cmdline),
8384
messaget(ui_message_handler),
84-
ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION),
85-
path_strategy_chooser()
85+
ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION)
8686
{
8787
}
8888

@@ -143,11 +143,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
143143

144144
if(cmdline.isset("show-symex-strategies"))
145145
{
146-
std::cout << path_strategy_chooser.show_strategies();
146+
status() << path_strategy_choosert().show_strategies() << eom;
147147
exit(CPROVER_EXIT_SUCCESS);
148148
}
149149

150-
path_strategy_chooser.set_path_strategy_options(cmdline, options, *this);
150+
parse_path_strategy_options(cmdline, options, ui_message_handler);
151151

152152
if(cmdline.isset("program-only"))
153153
options.set_option("program-only", true);
@@ -554,7 +554,7 @@ int cbmc_parse_optionst::doit()
554554
}
555555

556556
return bmct::do_language_agnostic_bmc(
557-
path_strategy_chooser, options, goto_model, ui_message_handler);
557+
path_strategy_choosert(), options, goto_model, ui_message_handler);
558558
}
559559

560560
bool cbmc_parse_optionst::set_properties()

‎src/cbmc/cbmc_parse_options.h

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -116,7 +116,6 @@ class cbmc_parse_optionst:
116116
protected:
117117
goto_modelt goto_model;
118118
ui_message_handlert ui_message_handler;
119-
const path_strategy_choosert path_strategy_chooser;
120119

121120
void register_languages();
122121
void get_command_line_options(optionst &);

‎src/goto-symex/path_storage.cpp

Lines changed: 13 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -90,27 +90,32 @@ std::string path_strategy_choosert::show_strategies() const
9090
return ss.str();
9191
}
9292

93-
void path_strategy_choosert::set_path_strategy_options(
93+
void parse_path_strategy_options(
9494
const cmdlinet &cmdline,
9595
optionst &options,
96-
messaget &message) const
96+
message_handlert &message_handler)
9797
{
98+
messaget log(message_handler);
99+
path_strategy_choosert path_strategy_chooser;
98100
if(cmdline.isset("paths"))
99101
{
100102
options.set_option("paths", true);
101103
std::string strategy = cmdline.get_value("paths");
102-
if(!is_valid_strategy(strategy))
104+
if(!path_strategy_chooser.is_valid_strategy(strategy))
103105
{
104-
message.error() << "Unknown strategy '" << strategy
105-
<< "'. Pass the --show-symex-strategies flag to list "
106-
"available strategies."
107-
<< message.eom;
106+
log.error() << "Unknown strategy '" << strategy
107+
<< "'. Pass the --show-symex-strategies flag to list "
108+
"available strategies."
109+
<< messaget::eom;
108110
exit(CPROVER_EXIT_USAGE_ERROR);
109111
}
110112
options.set_option("exploration-strategy", strategy);
111113
}
112114
else
113-
options.set_option("exploration-strategy", default_strategy());
115+
{
116+
options.set_option(
117+
"exploration-strategy", path_strategy_chooser.default_strategy());
118+
}
114119
}
115120

116121
path_strategy_choosert::path_strategy_choosert()

‎src/goto-symex/path_storage.h

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -152,17 +152,12 @@ class path_strategy_choosert
152152
return found->second.second();
153153
}
154154

155-
/// \brief add `paths` and `exploration-strategy` option, suitable to be
156-
/// invoked from front-ends.
157-
void
158-
set_path_strategy_options(const cmdlinet &, optionst &, messaget &) const;
159-
160-
protected:
161155
std::string default_strategy() const
162156
{
163157
return "lifo";
164158
}
165159

160+
protected:
166161
/// Map from the name of a strategy (to be supplied on the command line), to
167162
/// the help text for that strategy and a factory thunk returning a pointer to
168163
/// a derived class of path_storaget that implements that strategy.
@@ -172,4 +167,11 @@ class path_strategy_choosert
172167
strategies;
173168
};
174169

170+
/// \brief add `paths` and `exploration-strategy` option, suitable to be
171+
/// invoked from front-ends.
172+
void parse_path_strategy_options(
173+
const cmdlinet &,
174+
optionst &,
175+
message_handlert &);
176+
175177
#endif /* CPROVER_GOTO_SYMEX_PATH_STORAGE_H */

0 commit comments

Comments
 (0)