Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Do not artificially separate message handler and uit #2434

Merged
merged 4 commits into from
Sep 21, 2018
Merged

Do not artificially separate message handler and uit #2434

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
f4be7b8
Change uit configuration to xml-specific Boolean choice
tautschnig Sep 3, 2018
49920a4
Do not artificially separate message handler and uit
tautschnig Jun 21, 2018
2518473
Restrict get_json_stream to ui_message_handler
tautschnig Sep 5, 2018
0c8b108
Make ui_message_handlert parameterizable in the underlying message ha…
peterschrammel Sep 20, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 9 additions & 13 deletions jbmc/src/jbmc/jbmc_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -523,8 +523,7 @@ int jbmc_parse_optionst::doit()
path_strategy_chooser,
options,
goto_model,
ui_message_handler.get_ui(),
*this,
ui_message_handler,
configure_bmc);
}
else
Expand Down Expand Up @@ -557,15 +556,13 @@ 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.get_ui(),
*this,
configure_bmc,
callback_after_symex);
return bmct::do_language_agnostic_bmc(
path_strategy_chooser,
options,
lazy_goto_model,
ui_message_handler,
configure_bmc,
callback_after_symex);
}
}

Expand Down Expand Up @@ -618,8 +615,7 @@ int jbmc_parse_optionst::get_goto_program(
{
class_hierarchyt hierarchy;
hierarchy(lazy_goto_model.symbol_table);
show_class_hierarchy(
hierarchy, get_message_handler(), ui_message_handler.get_ui());
show_class_hierarchy(hierarchy, ui_message_handler);
return CPROVER_EXIT_SUCCESS;
}

Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/jdiff/java_syntactic_diff.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ class java_syntactic_difft : public goto_difft
const goto_modelt &_goto_model1,
const goto_modelt &_goto_model2,
const optionst &_options,
message_handlert &_message_handler)
ui_message_handlert &_message_handler)
: goto_difft(_goto_model1, _goto_model2, _options, _message_handler)
{
}
Expand Down
3 changes: 1 addition & 2 deletions jbmc/src/jdiff/jdiff_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -274,8 +274,7 @@ int jdiff_parse_optionst::doit()
}

java_syntactic_difft sd(
goto_model1, goto_model2, options, get_message_handler());
sd.set_ui(get_ui());
goto_model1, goto_model2, options, ui_message_handler);
sd();
sd.output_functions();

Expand Down
3 changes: 1 addition & 2 deletions jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -152,8 +152,7 @@ decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns)
bv_refinementt::infot info;
info.ns=&ns;
info.prop=&sat_check;
const auto ui=ui_message_handlert::uit::PLAIN;
info.ui=ui;
info.output_xml = false;
bv_refinementt solver(info);
solver << expr;
return solver();
Expand Down
6 changes: 4 additions & 2 deletions src/cbmc/all_properties.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -152,7 +152,7 @@ safety_checkert::resultt bmc_all_propertiest::operator()()

void bmc_all_propertiest::report(const cover_goalst &cover_goals)
{
switch(bmc.ui)
switch(bmc.ui_message_handler.get_ui())
{
case ui_message_handlert::uit::PLAIN:
{
Expand Down Expand Up @@ -202,8 +202,10 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)

case ui_message_handlert::uit::JSON_UI:
{
if(result().tellp() > 0)
result() << eom; // force end of previous message
json_stream_objectt &json_result =
result().json_stream().push_back_stream_object();
bmc.ui_message_handler.get_json_stream().push_back_stream_object();
json_stream_arrayt &result_array =
json_result.push_back_stream_array("result");

Expand Down
38 changes: 22 additions & 16 deletions src/cbmc/bmc.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ void bmct::error_trace()
goto_tracet &goto_trace=safety_checkert::error_trace;
build_goto_trace(equation, prop_conv, ns, goto_trace);

switch(ui)
switch(ui_message_handler.get_ui())
{
case ui_message_handlert::uit::PLAIN:
result() << "Counterexample:" << eom;
Expand All @@ -72,8 +72,10 @@ void bmct::error_trace()

case ui_message_handlert::uit::JSON_UI:
{
if(status().tellp() > 0)
status() << eom; // force end of previous message
json_stream_objectt &json_result =
status().json_stream().push_back_stream_object();
ui_message_handler.get_json_stream().push_back_stream_object();
const goto_trace_stept &step=goto_trace.steps.back();
json_result["property"] =
json_stringt(step.pc->source_location.get_property_id());
Expand Down Expand Up @@ -153,7 +155,7 @@ void bmct::report_success()
{
result() << "VERIFICATION SUCCESSFUL" << eom;

switch(ui)
switch(ui_message_handler.get_ui())
{
case ui_message_handlert::uit::PLAIN:
break;
Expand All @@ -180,7 +182,7 @@ void bmct::report_failure()
{
result() << "VERIFICATION FAILED" << eom;

switch(ui)
switch(ui_message_handler.get_ui())
{
case ui_message_handlert::uit::PLAIN:
break;
Expand Down Expand Up @@ -294,7 +296,7 @@ safety_checkert::resultt bmct::execute(

if(options.get_bool_option("show-vcc"))
{
show_vcc(options, get_message_handler(), ui, ns, equation);
show_vcc(options, ui_message_handler, ns, equation);
return safety_checkert::resultt::SAFE; // to indicate non-error
}

Expand Down Expand Up @@ -420,7 +422,7 @@ void bmct::show()
{
if(options.get_bool_option("show-vcc"))
{
show_vcc(options, get_message_handler(), ui, ns, equation);
show_vcc(options, ui_message_handler, ns, equation);
}

if(options.get_bool_option("program-only"))
Expand Down Expand Up @@ -478,15 +480,14 @@ 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,
messaget &message,
ui_message_handlert &ui,
std::function<void(bmct &, const symbol_tablet &)> driver_configure_bmc,
std::function<bool(void)> 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();
messaget message(ui);
std::unique_ptr<path_storaget> worklist;
std::string strategy = opts.get_option("exploration-strategy");
INVARIANT(
Expand All @@ -496,13 +497,15 @@ int bmct::do_language_agnostic_bmc(
try
{
{
cbmc_solverst solvers(opts, symbol_table, message.get_message_handler());
solvers.set_ui(ui);
cbmc_solverst solvers(
opts,
symbol_table,
ui,
ui.get_ui() == ui_message_handlert::uit::XML_UI);
std::unique_ptr<cbmc_solverst::solvert> 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);
bmc.set_ui(ui);
bmct bmc(opts, symbol_table, ui, pc, *worklist, callback_after_symex);
if(driver_configure_bmc)
driver_configure_bmc(bmc, symbol_table);
tmp_result = bmc.run(model);
Expand Down Expand Up @@ -546,16 +549,19 @@ int bmct::do_language_agnostic_bmc(
<< "Starting new path (" << worklist->size()
<< " to go)\n"
<< message.eom;
cbmc_solverst solvers(opts, symbol_table, message.get_message_handler());
solvers.set_ui(ui);
cbmc_solverst solvers(
opts,
symbol_table,
ui,
ui.get_ui() == ui_message_handlert::uit::XML_UI);
std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
cbmc_solver = solvers.get_solver();
prop_convt &pc = cbmc_solver->prop_conv();
path_storaget::patht &resume = worklist->peek();
path_explorert pe(
opts,
symbol_table,
mh,
ui,
pc,
resume.equation,
resume.state,
Expand Down
21 changes: 9 additions & 12 deletions src/cbmc/bmc.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@ class bmct:public safety_checkert
bmct(
const optionst &_options,
const symbol_tablet &outer_symbol_table,
message_handlert &_message_handler,
ui_message_handlert &_message_handler,
prop_convt &_prop_conv,
path_storaget &_path_storage,
std::function<bool(void)> callback_after_symex)
Expand All @@ -83,7 +83,7 @@ class bmct:public safety_checkert
options,
path_storage),
prop_conv(_prop_conv),
ui(ui_message_handlert::uit::PLAIN),
ui_message_handler(_message_handler),
driver_callback_after_symex(callback_after_symex)
{
symex.constant_propagation=options.get_bool_option("propagation");
Expand All @@ -103,8 +103,6 @@ class bmct:public safety_checkert
safety_checkert::resultt execute(abstract_goto_modelt &);
virtual ~bmct() { }

void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }

// the safety_checkert interface
virtual resultt operator()(
const goto_functionst &goto_functions)
Expand All @@ -127,10 +125,9 @@ class bmct:public safety_checkert
const path_strategy_choosert &path_strategy_chooser,
const optionst &opts,
abstract_goto_modelt &goto_model,
const ui_message_handlert::uit &ui,
messaget &message,
std::function<void(bmct &, const symbol_tablet &)>
driver_configure_bmc = nullptr,
ui_message_handlert &ui,
std::function<void(bmct &, const symbol_tablet &)> driver_configure_bmc =
nullptr,
std::function<bool(void)> callback_after_symex = nullptr);

protected:
Expand All @@ -144,7 +141,7 @@ class bmct:public safety_checkert
bmct(
const optionst &_options,
const symbol_tablet &outer_symbol_table,
message_handlert &_message_handler,
ui_message_handlert &_message_handler,
prop_convt &_prop_conv,
symex_target_equationt &_equation,
path_storaget &_path_storage,
Expand All @@ -162,7 +159,7 @@ class bmct:public safety_checkert
options,
path_storage),
prop_conv(_prop_conv),
ui(ui_message_handlert::uit::PLAIN),
ui_message_handler(_message_handler),
driver_callback_after_symex(callback_after_symex)
{
symex.constant_propagation = options.get_bool_option("propagation");
Expand All @@ -186,7 +183,7 @@ class bmct:public safety_checkert
prop_convt &prop_conv;
std::unique_ptr<memory_model_baset> memory_model;
// use gui format
ui_message_handlert::uit ui;
ui_message_handlert &ui_message_handler;

virtual decision_proceduret::resultt
run_decision_procedure(prop_convt &prop_conv);
Expand Down Expand Up @@ -259,7 +256,7 @@ class path_explorert : public bmct
path_explorert(
const optionst &_options,
const symbol_tablet &outer_symbol_table,
message_handlert &_message_handler,
ui_message_handlert &_message_handler,
prop_convt &_prop_conv,
symex_target_equationt &saved_equation,
const goto_symex_statet &saved_state,
Expand Down
8 changes: 5 additions & 3 deletions src/cbmc/bmc_cover.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -261,7 +261,7 @@ bool bmc_covert::operator()()
if(g.second.satisfied)
goals_covered++;

switch(bmc.ui)
switch(bmc.ui_message_handler.get_ui())
{
case ui_message_handlert::uit::PLAIN:
{
Expand Down Expand Up @@ -341,8 +341,10 @@ bool bmc_covert::operator()()

case ui_message_handlert::uit::JSON_UI:
{
if(status().tellp() > 0)
status() << eom; // force end of previous message
json_stream_objectt &json_result =
status().json_stream().push_back_stream_object();
bmc.ui_message_handler.get_json_stream().push_back_stream_object();
for(const auto &goal_pair : goal_map)
{
const goalt &goal=goal_pair.second;
Expand Down Expand Up @@ -406,7 +408,7 @@ bool bmc_covert::operator()()
<< (cover_goals.iterations()==1?"":"s")
<< eom;

if(bmc.ui==ui_message_handlert::uit::PLAIN)
if(bmc.ui_message_handler.get_ui() == ui_message_handlert::uit::PLAIN)
{
result() << "Test suite:" << '\n';

Expand Down
6 changes: 1 addition & 5 deletions src/cbmc/cbmc_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -527,11 +527,7 @@ int cbmc_parse_optionst::doit()
return CPROVER_EXIT_SET_PROPERTIES_FAILED;

return bmct::do_language_agnostic_bmc(
path_strategy_chooser,
options,
goto_model,
ui_message_handler.get_ui(),
*this);
path_strategy_chooser, options, goto_model, ui_message_handler);
}

bool cbmc_parse_optionst::set_properties()
Expand Down
16 changes: 8 additions & 8 deletions src/cbmc/cbmc_solvers.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_default()
solver->set_prop(util_make_unique<satcheckt>());
}

solver->prop().set_message_handler(get_message_handler());
solver->prop().set_message_handler(message_handler);

auto bv_pointers = util_make_unique<bv_pointerst>(ns, solver->prop());

Expand All @@ -92,7 +92,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_dimacs()
no_incremental_check();

auto prop=util_make_unique<dimacs_cnft>();
prop->set_message_handler(get_message_handler());
prop->set_message_handler(message_handler);

std::string filename=options.get_option("outfile");

Expand All @@ -113,12 +113,12 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_bv_refinement()
return util_make_unique<satcheck_no_simplifiert>();
}();

prop->set_message_handler(get_message_handler());
prop->set_message_handler(message_handler);

bv_refinementt::infot info;
info.ns=&ns;
info.prop=prop.get();
info.ui=ui;
info.output_xml = output_xml_in_refinement;

// we allow setting some parameters
if(options.get_bool_option("max-node-refinement"))
Expand All @@ -141,10 +141,10 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
string_refinementt::infot info;
info.ns=&ns;
auto prop=util_make_unique<satcheck_no_simplifiert>();
prop->set_message_handler(get_message_handler());
prop->set_message_handler(message_handler);
info.prop=prop.get();
info.refinement_bound=DEFAULT_MAX_NB_REFINEMENT;
info.ui=ui;
info.output_xml = output_xml_in_refinement;
if(options.get_bool_option("max-node-refinement"))
info.max_node_refinement=
options.get_unsigned_int_option("max-node-refinement");
Expand Down Expand Up @@ -197,7 +197,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
if(options.get_bool_option("fpa"))
smt2_conv->use_FPA_theory=true;

smt2_conv->set_message_handler(get_message_handler());
smt2_conv->set_message_handler(message_handler);

return util_make_unique<solvert>(std::move(smt2_conv));
}
Expand Down Expand Up @@ -226,7 +226,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
if(options.get_bool_option("fpa"))
smt2_conv->use_FPA_theory=true;

smt2_conv->set_message_handler(get_message_handler());
smt2_conv->set_message_handler(message_handler);

return util_make_unique<solvert>(std::move(smt2_conv), std::move(out));
}
Expand Down
Loading