Skip to content

Commit 5c9d3dd

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #2434 from tautschnig/vs-ui
Do not artificially separate message handler and uit
2 parents 784b692 + 0c8b108 commit 5c9d3dd

30 files changed

+160
-186
lines changed

‎jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 9 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -523,8 +523,7 @@ int jbmc_parse_optionst::doit()
523523
path_strategy_chooser,
524524
options,
525525
goto_model,
526-
ui_message_handler.get_ui(),
527-
*this,
526+
ui_message_handler,
528527
configure_bmc);
529528
}
530529
else
@@ -557,15 +556,13 @@ int jbmc_parse_optionst::doit()
557556

558557
// The `configure_bmc` callback passed will enable enum-unwind-static if
559558
// applicable.
560-
return
561-
bmct::do_language_agnostic_bmc(
562-
path_strategy_chooser,
563-
options,
564-
lazy_goto_model,
565-
ui_message_handler.get_ui(),
566-
*this,
567-
configure_bmc,
568-
callback_after_symex);
559+
return bmct::do_language_agnostic_bmc(
560+
path_strategy_chooser,
561+
options,
562+
lazy_goto_model,
563+
ui_message_handler,
564+
configure_bmc,
565+
callback_after_symex);
569566
}
570567
}
571568

@@ -618,8 +615,7 @@ int jbmc_parse_optionst::get_goto_program(
618615
{
619616
class_hierarchyt hierarchy;
620617
hierarchy(lazy_goto_model.symbol_table);
621-
show_class_hierarchy(
622-
hierarchy, get_message_handler(), ui_message_handler.get_ui());
618+
show_class_hierarchy(hierarchy, ui_message_handler);
623619
return CPROVER_EXIT_SUCCESS;
624620
}
625621

‎jbmc/src/jdiff/java_syntactic_diff.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ class java_syntactic_difft : public goto_difft
2121
const goto_modelt &_goto_model1,
2222
const goto_modelt &_goto_model2,
2323
const optionst &_options,
24-
message_handlert &_message_handler)
24+
ui_message_handlert &_message_handler)
2525
: goto_difft(_goto_model1, _goto_model2, _options, _message_handler)
2626
{
2727
}

‎jbmc/src/jdiff/jdiff_parse_options.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -274,8 +274,7 @@ int jdiff_parse_optionst::doit()
274274
}
275275

276276
java_syntactic_difft sd(
277-
goto_model1, goto_model2, options, get_message_handler());
278-
sd.set_ui(get_ui());
277+
goto_model1, goto_model2, options, ui_message_handler);
279278
sd();
280279
sd.output_functions();
281280

‎jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -152,8 +152,7 @@ decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns)
152152
bv_refinementt::infot info;
153153
info.ns=&ns;
154154
info.prop=&sat_check;
155-
const auto ui=ui_message_handlert::uit::PLAIN;
156-
info.ui=ui;
155+
info.output_xml = false;
157156
bv_refinementt solver(info);
158157
solver << expr;
159158
return solver();

‎src/cbmc/all_properties.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -152,7 +152,7 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
152152

153153
void bmc_all_propertiest::report(const cover_goalst &cover_goals)
154154
{
155-
switch(bmc.ui)
155+
switch(bmc.ui_message_handler.get_ui())
156156
{
157157
case ui_message_handlert::uit::PLAIN:
158158
{
@@ -202,8 +202,10 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
202202

203203
case ui_message_handlert::uit::JSON_UI:
204204
{
205+
if(result().tellp() > 0)
206+
result() << eom; // force end of previous message
205207
json_stream_objectt &json_result =
206-
result().json_stream().push_back_stream_object();
208+
bmc.ui_message_handler.get_json_stream().push_back_stream_object();
207209
json_stream_arrayt &result_array =
208210
json_result.push_back_stream_array("result");
209211

‎src/cbmc/bmc.cpp

Lines changed: 22 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,7 @@ void bmct::error_trace()
5454
goto_tracet &goto_trace=safety_checkert::error_trace;
5555
build_goto_trace(equation, prop_conv, ns, goto_trace);
5656

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

7373
case ui_message_handlert::uit::JSON_UI:
7474
{
75+
if(status().tellp() > 0)
76+
status() << eom; // force end of previous message
7577
json_stream_objectt &json_result =
76-
status().json_stream().push_back_stream_object();
78+
ui_message_handler.get_json_stream().push_back_stream_object();
7779
const goto_trace_stept &step=goto_trace.steps.back();
7880
json_result["property"] =
7981
json_stringt(step.pc->source_location.get_property_id());
@@ -153,7 +155,7 @@ void bmct::report_success()
153155
{
154156
result() << "VERIFICATION SUCCESSFUL" << eom;
155157

156-
switch(ui)
158+
switch(ui_message_handler.get_ui())
157159
{
158160
case ui_message_handlert::uit::PLAIN:
159161
break;
@@ -180,7 +182,7 @@ void bmct::report_failure()
180182
{
181183
result() << "VERIFICATION FAILED" << eom;
182184

183-
switch(ui)
185+
switch(ui_message_handler.get_ui())
184186
{
185187
case ui_message_handlert::uit::PLAIN:
186188
break;
@@ -294,7 +296,7 @@ safety_checkert::resultt bmct::execute(
294296

295297
if(options.get_bool_option("show-vcc"))
296298
{
297-
show_vcc(options, get_message_handler(), ui, ns, equation);
299+
show_vcc(options, ui_message_handler, ns, equation);
298300
return safety_checkert::resultt::SAFE; // to indicate non-error
299301
}
300302

@@ -420,7 +422,7 @@ void bmct::show()
420422
{
421423
if(options.get_bool_option("show-vcc"))
422424
{
423-
show_vcc(options, get_message_handler(), ui, ns, equation);
425+
show_vcc(options, ui_message_handler, ns, equation);
424426
}
425427

426428
if(options.get_bool_option("program-only"))
@@ -478,15 +480,14 @@ int bmct::do_language_agnostic_bmc(
478480
const path_strategy_choosert &path_strategy_chooser,
479481
const optionst &opts,
480482
abstract_goto_modelt &model,
481-
const ui_message_handlert::uit &ui,
482-
messaget &message,
483+
ui_message_handlert &ui,
483484
std::function<void(bmct &, const symbol_tablet &)> driver_configure_bmc,
484485
std::function<bool(void)> callback_after_symex)
485486
{
486487
safety_checkert::resultt final_result = safety_checkert::resultt::UNKNOWN;
487488
safety_checkert::resultt tmp_result = safety_checkert::resultt::UNKNOWN;
488489
const symbol_tablet &symbol_table = model.get_symbol_table();
489-
message_handlert &mh = message.get_message_handler();
490+
messaget message(ui);
490491
std::unique_ptr<path_storaget> worklist;
491492
std::string strategy = opts.get_option("exploration-strategy");
492493
INVARIANT(
@@ -496,13 +497,15 @@ int bmct::do_language_agnostic_bmc(
496497
try
497498
{
498499
{
499-
cbmc_solverst solvers(opts, symbol_table, message.get_message_handler());
500-
solvers.set_ui(ui);
500+
cbmc_solverst solvers(
501+
opts,
502+
symbol_table,
503+
ui,
504+
ui.get_ui() == ui_message_handlert::uit::XML_UI);
501505
std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
502506
cbmc_solver = solvers.get_solver();
503507
prop_convt &pc = cbmc_solver->prop_conv();
504-
bmct bmc(opts, symbol_table, mh, pc, *worklist, callback_after_symex);
505-
bmc.set_ui(ui);
508+
bmct bmc(opts, symbol_table, ui, pc, *worklist, callback_after_symex);
506509
if(driver_configure_bmc)
507510
driver_configure_bmc(bmc, symbol_table);
508511
tmp_result = bmc.run(model);
@@ -546,16 +549,19 @@ int bmct::do_language_agnostic_bmc(
546549
<< "Starting new path (" << worklist->size()
547550
<< " to go)\n"
548551
<< message.eom;
549-
cbmc_solverst solvers(opts, symbol_table, message.get_message_handler());
550-
solvers.set_ui(ui);
552+
cbmc_solverst solvers(
553+
opts,
554+
symbol_table,
555+
ui,
556+
ui.get_ui() == ui_message_handlert::uit::XML_UI);
551557
std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
552558
cbmc_solver = solvers.get_solver();
553559
prop_convt &pc = cbmc_solver->prop_conv();
554560
path_storaget::patht &resume = worklist->peek();
555561
path_explorert pe(
556562
opts,
557563
symbol_table,
558-
mh,
564+
ui,
559565
pc,
560566
resume.equation,
561567
resume.state,

‎src/cbmc/bmc.h

Lines changed: 9 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -66,7 +66,7 @@ class bmct:public safety_checkert
6666
bmct(
6767
const optionst &_options,
6868
const symbol_tablet &outer_symbol_table,
69-
message_handlert &_message_handler,
69+
ui_message_handlert &_message_handler,
7070
prop_convt &_prop_conv,
7171
path_storaget &_path_storage,
7272
std::function<bool(void)> callback_after_symex)
@@ -83,7 +83,7 @@ class bmct:public safety_checkert
8383
options,
8484
path_storage),
8585
prop_conv(_prop_conv),
86-
ui(ui_message_handlert::uit::PLAIN),
86+
ui_message_handler(_message_handler),
8787
driver_callback_after_symex(callback_after_symex)
8888
{
8989
symex.constant_propagation=options.get_bool_option("propagation");
@@ -103,8 +103,6 @@ class bmct:public safety_checkert
103103
safety_checkert::resultt execute(abstract_goto_modelt &);
104104
virtual ~bmct() { }
105105

106-
void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
107-
108106
// the safety_checkert interface
109107
virtual resultt operator()(
110108
const goto_functionst &goto_functions)
@@ -127,10 +125,9 @@ class bmct:public safety_checkert
127125
const path_strategy_choosert &path_strategy_chooser,
128126
const optionst &opts,
129127
abstract_goto_modelt &goto_model,
130-
const ui_message_handlert::uit &ui,
131-
messaget &message,
132-
std::function<void(bmct &, const symbol_tablet &)>
133-
driver_configure_bmc = nullptr,
128+
ui_message_handlert &ui,
129+
std::function<void(bmct &, const symbol_tablet &)> driver_configure_bmc =
130+
nullptr,
134131
std::function<bool(void)> callback_after_symex = nullptr);
135132

136133
protected:
@@ -144,7 +141,7 @@ class bmct:public safety_checkert
144141
bmct(
145142
const optionst &_options,
146143
const symbol_tablet &outer_symbol_table,
147-
message_handlert &_message_handler,
144+
ui_message_handlert &_message_handler,
148145
prop_convt &_prop_conv,
149146
symex_target_equationt &_equation,
150147
path_storaget &_path_storage,
@@ -162,7 +159,7 @@ class bmct:public safety_checkert
162159
options,
163160
path_storage),
164161
prop_conv(_prop_conv),
165-
ui(ui_message_handlert::uit::PLAIN),
162+
ui_message_handler(_message_handler),
166163
driver_callback_after_symex(callback_after_symex)
167164
{
168165
symex.constant_propagation = options.get_bool_option("propagation");
@@ -186,7 +183,7 @@ class bmct:public safety_checkert
186183
prop_convt &prop_conv;
187184
std::unique_ptr<memory_model_baset> memory_model;
188185
// use gui format
189-
ui_message_handlert::uit ui;
186+
ui_message_handlert &ui_message_handler;
190187

191188
virtual decision_proceduret::resultt
192189
run_decision_procedure(prop_convt &prop_conv);
@@ -259,7 +256,7 @@ class path_explorert : public bmct
259256
path_explorert(
260257
const optionst &_options,
261258
const symbol_tablet &outer_symbol_table,
262-
message_handlert &_message_handler,
259+
ui_message_handlert &_message_handler,
263260
prop_convt &_prop_conv,
264261
symex_target_equationt &saved_equation,
265262
const goto_symex_statet &saved_state,

‎src/cbmc/bmc_cover.cpp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -261,7 +261,7 @@ bool bmc_covert::operator()()
261261
if(g.second.satisfied)
262262
goals_covered++;
263263

264-
switch(bmc.ui)
264+
switch(bmc.ui_message_handler.get_ui())
265265
{
266266
case ui_message_handlert::uit::PLAIN:
267267
{
@@ -341,8 +341,10 @@ bool bmc_covert::operator()()
341341

342342
case ui_message_handlert::uit::JSON_UI:
343343
{
344+
if(status().tellp() > 0)
345+
status() << eom; // force end of previous message
344346
json_stream_objectt &json_result =
345-
status().json_stream().push_back_stream_object();
347+
bmc.ui_message_handler.get_json_stream().push_back_stream_object();
346348
for(const auto &goal_pair : goal_map)
347349
{
348350
const goalt &goal=goal_pair.second;
@@ -406,7 +408,7 @@ bool bmc_covert::operator()()
406408
<< (cover_goals.iterations()==1?"":"s")
407409
<< eom;
408410

409-
if(bmc.ui==ui_message_handlert::uit::PLAIN)
411+
if(bmc.ui_message_handler.get_ui() == ui_message_handlert::uit::PLAIN)
410412
{
411413
result() << "Test suite:" << '\n';
412414

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -527,11 +527,7 @@ int cbmc_parse_optionst::doit()
527527
return CPROVER_EXIT_SET_PROPERTIES_FAILED;
528528

529529
return bmct::do_language_agnostic_bmc(
530-
path_strategy_chooser,
531-
options,
532-
goto_model,
533-
ui_message_handler.get_ui(),
534-
*this);
530+
path_strategy_chooser, options, goto_model, ui_message_handler);
535531
}
536532

537533
bool cbmc_parse_optionst::set_properties()

‎src/cbmc/cbmc_solvers.cpp

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_default()
7272
solver->set_prop(util_make_unique<satcheckt>());
7373
}
7474

75-
solver->prop().set_message_handler(get_message_handler());
75+
solver->prop().set_message_handler(message_handler);
7676

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

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

9494
auto prop=util_make_unique<dimacs_cnft>();
95-
prop->set_message_handler(get_message_handler());
95+
prop->set_message_handler(message_handler);
9696

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

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

116-
prop->set_message_handler(get_message_handler());
116+
prop->set_message_handler(message_handler);
117117

118118
bv_refinementt::infot info;
119119
info.ns=&ns;
120120
info.prop=prop.get();
121-
info.ui=ui;
121+
info.output_xml = output_xml_in_refinement;
122122

123123
// we allow setting some parameters
124124
if(options.get_bool_option("max-node-refinement"))
@@ -141,10 +141,10 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
141141
string_refinementt::infot info;
142142
info.ns=&ns;
143143
auto prop=util_make_unique<satcheck_no_simplifiert>();
144-
prop->set_message_handler(get_message_handler());
144+
prop->set_message_handler(message_handler);
145145
info.prop=prop.get();
146146
info.refinement_bound=DEFAULT_MAX_NB_REFINEMENT;
147-
info.ui=ui;
147+
info.output_xml = output_xml_in_refinement;
148148
if(options.get_bool_option("max-node-refinement"))
149149
info.max_node_refinement=
150150
options.get_unsigned_int_option("max-node-refinement");
@@ -197,7 +197,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
197197
if(options.get_bool_option("fpa"))
198198
smt2_conv->use_FPA_theory=true;
199199

200-
smt2_conv->set_message_handler(get_message_handler());
200+
smt2_conv->set_message_handler(message_handler);
201201

202202
return util_make_unique<solvert>(std::move(smt2_conv));
203203
}
@@ -226,7 +226,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
226226
if(options.get_bool_option("fpa"))
227227
smt2_conv->use_FPA_theory=true;
228228

229-
smt2_conv->set_message_handler(get_message_handler());
229+
smt2_conv->set_message_handler(message_handler);
230230

231231
return util_make_unique<solvert>(std::move(smt2_conv), std::move(out));
232232
}

0 commit comments

Comments
 (0)