Skip to content

Commit fd2700d

Browse files
committed
Do not artificially separate message handler and uit
They were passed around independently, even though they originated from the very same object.
1 parent 7dfefc7 commit fd2700d

13 files changed

+49
-66
lines changed

jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -562,8 +562,7 @@ int jbmc_parse_optionst::doit()
562562
path_strategy_chooser,
563563
options,
564564
goto_model,
565-
ui_message_handler.get_ui(),
566-
*this,
565+
ui_message_handler,
567566
configure_bmc);
568567
}
569568
else
@@ -607,8 +606,7 @@ int jbmc_parse_optionst::doit()
607606
path_strategy_chooser,
608607
options,
609608
lazy_goto_model,
610-
ui_message_handler.get_ui(),
611-
*this,
609+
ui_message_handler,
612610
configure_bmc,
613611
callback_after_symex);
614612
}
@@ -663,8 +661,7 @@ int jbmc_parse_optionst::get_goto_program(
663661
{
664662
class_hierarchyt hierarchy;
665663
hierarchy(lazy_goto_model.symbol_table);
666-
show_class_hierarchy(
667-
hierarchy, get_message_handler(), ui_message_handler.get_ui());
664+
show_class_hierarchy(hierarchy, ui_message_handler);
668665
return CPROVER_EXIT_SUCCESS;
669666
}
670667

src/cbmc/all_properties.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -157,7 +157,7 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
157157

158158
void bmc_all_propertiest::report(const cover_goalst &cover_goals)
159159
{
160-
switch(bmc.ui)
160+
switch(bmc.ui_message_handler.get_ui())
161161
{
162162
case ui_message_handlert::uit::PLAIN:
163163
{

src/cbmc/bmc.cpp

Lines changed: 9 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,7 @@ void bmct::error_trace()
5151
goto_tracet &goto_trace=safety_checkert::error_trace;
5252
build_goto_trace(equation, prop_conv, ns, goto_trace);
5353

54-
switch(ui)
54+
switch(ui_message_handler.get_ui())
5555
{
5656
case ui_message_handlert::uit::PLAIN:
5757
result() << "Counterexample:" << eom;
@@ -150,7 +150,7 @@ void bmct::report_success()
150150
{
151151
result() << "VERIFICATION SUCCESSFUL" << eom;
152152

153-
switch(ui)
153+
switch(ui_message_handler.get_ui())
154154
{
155155
case ui_message_handlert::uit::PLAIN:
156156
break;
@@ -177,7 +177,7 @@ void bmct::report_failure()
177177
{
178178
result() << "VERIFICATION FAILED" << eom;
179179

180-
switch(ui)
180+
switch(ui_message_handler.get_ui())
181181
{
182182
case ui_message_handlert::uit::PLAIN:
183183
break;
@@ -562,15 +562,14 @@ int bmct::do_language_agnostic_bmc(
562562
const path_strategy_choosert &path_strategy_chooser,
563563
const optionst &opts,
564564
abstract_goto_modelt &model,
565-
const ui_message_handlert::uit &ui,
566-
messaget &message,
565+
ui_message_handlert &ui,
567566
std::function<void(bmct &, const symbol_tablet &)> driver_configure_bmc,
568567
std::function<bool(void)> callback_after_symex)
569568
{
570569
safety_checkert::resultt final_result = safety_checkert::resultt::UNKNOWN;
571570
safety_checkert::resultt tmp_result = safety_checkert::resultt::UNKNOWN;
572571
const symbol_tablet &symbol_table = model.get_symbol_table();
573-
message_handlert &mh = message.get_message_handler();
572+
messaget message(ui);
574573
std::unique_ptr<path_storaget> worklist;
575574
std::string strategy = opts.get_option("exploration-strategy");
576575
INVARIANT(
@@ -580,13 +579,11 @@ int bmct::do_language_agnostic_bmc(
580579
try
581580
{
582581
{
583-
cbmc_solverst solvers(opts, symbol_table, message.get_message_handler());
584-
solvers.set_ui(ui);
582+
cbmc_solverst solvers(opts, symbol_table, ui);
585583
std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
586584
cbmc_solver = solvers.get_solver();
587585
prop_convt &pc = cbmc_solver->prop_conv();
588-
bmct bmc(opts, symbol_table, mh, pc, *worklist, callback_after_symex);
589-
bmc.set_ui(ui);
586+
bmct bmc(opts, symbol_table, ui, pc, *worklist, callback_after_symex);
590587
if(driver_configure_bmc)
591588
driver_configure_bmc(bmc, symbol_table);
592589
tmp_result = bmc.run(model);
@@ -621,16 +618,15 @@ int bmct::do_language_agnostic_bmc(
621618
<< "Starting new path (" << worklist->size()
622619
<< " to go)\n"
623620
<< message.eom;
624-
cbmc_solverst solvers(opts, symbol_table, message.get_message_handler());
625-
solvers.set_ui(ui);
621+
cbmc_solverst solvers(opts, symbol_table, ui);
626622
std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
627623
cbmc_solver = solvers.get_solver();
628624
prop_convt &pc = cbmc_solver->prop_conv();
629625
path_storaget::patht &resume = worklist->peek();
630626
path_explorert pe(
631627
opts,
632628
symbol_table,
633-
mh,
629+
ui,
634630
pc,
635631
resume.equation,
636632
resume.state,

src/cbmc/bmc.h

Lines changed: 7 additions & 10 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,8 +125,7 @@ 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,
128+
ui_message_handlert &ui,
132129
std::function<void(bmct &, const symbol_tablet &)>
133130
driver_configure_bmc = nullptr,
134131
std::function<bool(void)> callback_after_symex = nullptr);
@@ -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);
@@ -266,7 +263,7 @@ class path_explorert : public bmct
266263
path_explorert(
267264
const optionst &_options,
268265
const symbol_tablet &outer_symbol_table,
269-
message_handlert &_message_handler,
266+
ui_message_handlert &_message_handler,
270267
prop_convt &_prop_conv,
271268
symex_target_equationt &saved_equation,
272269
const goto_symex_statet &saved_state,

src/cbmc/bmc_cover.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -267,7 +267,7 @@ bool bmc_covert::operator()()
267267
if(g.second.satisfied)
268268
goals_covered++;
269269

270-
switch(bmc.ui)
270+
switch(bmc.ui_message_handler.get_ui())
271271
{
272272
case ui_message_handlert::uit::PLAIN:
273273
{
@@ -412,7 +412,7 @@ bool bmc_covert::operator()()
412412
<< (cover_goals.iterations()==1?"":"s")
413413
<< eom;
414414

415-
if(bmc.ui==ui_message_handlert::uit::PLAIN)
415+
if(bmc.ui_message_handler.get_ui() == ui_message_handlert::uit::PLAIN)
416416
{
417417
result() << "Test suite:" << '\n';
418418

src/cbmc/cbmc_parse_options.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -533,8 +533,7 @@ int cbmc_parse_optionst::doit()
533533
path_strategy_chooser,
534534
options,
535535
goto_model,
536-
ui_message_handler.get_ui(),
537-
*this);
536+
ui_message_handler);
538537
}
539538

540539
bool cbmc_parse_optionst::set_properties()

src/cbmc/cbmc_solvers.cpp

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

74-
solver->prop().set_message_handler(get_message_handler());
74+
solver->prop().set_message_handler(ui);
7575

7676
auto bv_cbmc=util_make_unique<bv_cbmct>(ns, solver->prop());
7777

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

9393
auto prop=util_make_unique<dimacs_cnft>();
94-
prop->set_message_handler(get_message_handler());
94+
prop->set_message_handler(ui);
9595

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

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

115-
prop->set_message_handler(get_message_handler());
115+
prop->set_message_handler(ui);
116116

117117
bv_refinementt::infot info;
118118
info.ns=&ns;
119119
info.prop=prop.get();
120-
info.ui=ui;
120+
info.ui=ui.get_ui();
121121

122122
// we allow setting some parameters
123123
if(options.get_bool_option("max-node-refinement"))
@@ -140,10 +140,10 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
140140
string_refinementt::infot info;
141141
info.ns=&ns;
142142
auto prop=util_make_unique<satcheck_no_simplifiert>();
143-
prop->set_message_handler(get_message_handler());
143+
prop->set_message_handler(ui);
144144
info.prop=prop.get();
145145
info.refinement_bound=DEFAULT_MAX_NB_REFINEMENT;
146-
info.ui=ui;
146+
info.ui=ui.get_ui();
147147
if(options.get_bool_option("string-max-length"))
148148
info.max_string_length = options.get_signed_int_option("string-max-length");
149149
info.trace=options.get_bool_option("trace");
@@ -160,6 +160,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
160160
std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
161161
smt2_dect::solvert solver)
162162
{
163+
messaget msg(ui);
163164
no_beautification();
164165

165166
const std::string &filename=options.get_option("outfile");
@@ -168,7 +169,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
168169
{
169170
if(solver==smt2_dect::solvert::GENERIC)
170171
{
171-
error() << "please use --outfile" << eom;
172+
msg.error() << "please use --outfile" << messaget::eom;
172173
throw 0;
173174
}
174175

@@ -199,7 +200,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
199200
if(options.get_bool_option("fpa"))
200201
smt2_conv->use_FPA_theory=true;
201202

202-
smt2_conv->set_message_handler(get_message_handler());
203+
smt2_conv->set_message_handler(ui);
203204

204205
return util_make_unique<solvert>(std::move(smt2_conv));
205206
}
@@ -213,7 +214,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
213214

214215
if(!*out)
215216
{
216-
error() << "failed to open " << filename << eom;
217+
msg.error() << "failed to open " << filename << messaget::eom;
217218
throw 0;
218219
}
219220

@@ -229,7 +230,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
229230
if(options.get_bool_option("fpa"))
230231
smt2_conv->use_FPA_theory=true;
231232

232-
smt2_conv->set_message_handler(get_message_handler());
233+
smt2_conv->set_message_handler(ui);
233234

234235
return util_make_unique<solvert>(std::move(smt2_conv), std::move(out));
235236
}
@@ -239,7 +240,8 @@ void cbmc_solverst::no_beautification()
239240
{
240241
if(options.get_bool_option("beautify"))
241242
{
242-
error() << "sorry, this solver does not support beautification" << eom;
243+
messaget(ui).error() << "sorry, this solver does not support beautification"
244+
<< messaget::eom;
243245
throw 0;
244246
}
245247
}
@@ -250,7 +252,8 @@ void cbmc_solverst::no_incremental_check()
250252
options.get_option("cover")!="" ||
251253
options.get_option("incremental-check")!="")
252254
{
253-
error() << "sorry, this solver does not support incremental solving" << eom;
255+
messaget(ui).error() << "sorry, this solver does not support incremental "
256+
<< "solving" << messaget::eom;
254257
throw 0;
255258
}
256259
}

src/cbmc/cbmc_solvers.h

Lines changed: 4 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -29,18 +29,17 @@ Author: Daniel Kroening, [email protected]
2929

3030
#include "bv_cbmc.h"
3131

32-
class cbmc_solverst:public messaget
32+
class cbmc_solverst
3333
{
3434
public:
3535
cbmc_solverst(
3636
const optionst &_options,
3737
const symbol_tablet &_symbol_table,
38-
message_handlert &_message_handler):
39-
messaget(_message_handler),
38+
ui_message_handlert &_message_handler):
4039
options(_options),
4140
symbol_table(_symbol_table),
4241
ns(_symbol_table),
43-
ui(ui_message_handlert::uit::PLAIN)
42+
ui(_message_handler)
4443
{
4544
}
4645

@@ -120,15 +119,11 @@ class cbmc_solverst:public messaget
120119
{
121120
}
122121

123-
void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
124-
125122
protected:
126123
const optionst &options;
127124
const symbol_tablet &symbol_table;
128125
namespacet ns;
129-
130-
// use gui format
131-
ui_message_handlert::uit ui;
126+
ui_message_handlert &ui;
132127

133128
std::unique_ptr<solvert> get_default();
134129
std::unique_ptr<solvert> get_dimacs();

src/cbmc/fault_localization.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -289,7 +289,7 @@ safety_checkert::resultt fault_localizationt::stop_on_fail()
289289
// localize faults
290290
run(ID_nil);
291291

292-
switch(bmc.ui)
292+
switch(bmc.ui_message_handler.get_ui())
293293
{
294294
case ui_message_handlert::uit::PLAIN:
295295
{
@@ -356,7 +356,7 @@ void fault_localizationt::report(
356356
{
357357
bmc_all_propertiest::report(cover_goals);
358358

359-
switch(bmc.ui)
359+
switch(bmc.ui_message_handler.get_ui())
360360
{
361361
case ui_message_handlert::uit::PLAIN:
362362
if(cover_goals.number_covered()>0)

src/cbmc/show_vcc.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -148,7 +148,7 @@ void bmct::show_vcc()
148148

149149
std::ostream &out=have_file?of:std::cout;
150150

151-
switch(ui)
151+
switch(ui_message_handler.get_ui())
152152
{
153153
case ui_message_handlert::uit::XML_UI:
154154
error() << "XML UI not supported" << eom;

0 commit comments

Comments
 (0)