Skip to content

Commit 4851c79

Browse files
tautschnigtautschnig
committed
A decision_proceduret isn't a messaget
Some derived classes may want to generate output, but then it's safe for them to be messaget's.
1 parent 55302b7 commit 4851c79

File tree

13 files changed

+86
-67
lines changed

13 files changed

+86
-67
lines changed

‎src/cbmc/all_properties.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -54,8 +54,6 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
5454
{
5555
status() << "Passing problem to " << solver.decision_procedure_text() << eom;
5656

57-
solver.set_message_handler(get_message_handler());
58-
5957
auto solver_start=std::chrono::steady_clock::now();
6058

6159
convert_symex_target_equation(

‎src/cbmc/bmc.cpp

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -47,8 +47,6 @@ decision_proceduret::resultt bmct::run_decision_procedure()
4747
status() << "Passing problem to "
4848
<< prop_conv.decision_procedure_text() << eom;
4949

50-
prop_conv.set_message_handler(get_message_handler());
51-
5250
auto solver_start = std::chrono::steady_clock::now();
5351

5452
convert_symex_target_equation(equation, prop_conv, get_message_handler());
@@ -207,8 +205,6 @@ safety_checkert::resultt bmct::run(
207205

208206
safety_checkert::resultt bmct::decide(const goto_functionst &goto_functions)
209207
{
210-
prop_conv.set_message_handler(get_message_handler());
211-
212208
if(options.get_bool_option("stop-on-fail"))
213209
return stop_on_fail();
214210
else

‎src/cbmc/bmc_cover.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -189,8 +189,6 @@ bool bmc_covert::operator()()
189189
{
190190
status() << "Passing problem to " << solver.decision_procedure_text() << eom;
191191

192-
solver.set_message_handler(get_message_handler());
193-
194192
auto solver_start=std::chrono::steady_clock::now();
195193

196194
// Collect _all_ goals in `goal_map'.

‎src/cbmc/fault_localization.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -247,8 +247,6 @@ fault_localizationt::run_decision_procedure(prop_convt &prop_conv)
247247
status() << "Passing problem to "
248248
<< prop_conv.decision_procedure_text() << eom;
249249

250-
prop_conv.set_message_handler(bmc.get_message_handler());
251-
252250
auto solver_start=std::chrono::steady_clock::now();
253251

254252
convert_symex_target_equation(

‎src/goto-checker/bmc_util.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -139,7 +139,7 @@ void convert_symex_target_equation(
139139
msg.status() << "converting SSA" << messaget::eom;
140140

141141
// convert SSA
142-
equation.convert(prop_conv);
142+
equation.convert(prop_conv, message_handler);
143143
}
144144

145145
std::unique_ptr<memory_model_baset>

‎src/goto-checker/solver_factory.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -268,6 +268,8 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
268268
if(options.get_bool_option("fpa"))
269269
smt2_dec->use_FPA_theory = true;
270270

271+
smt2_dec->set_message_handler(message_handler);
272+
271273
set_prop_conv_time_limit(*smt2_dec);
272274
return util_make_unique<solvert>(std::move(smt2_dec));
273275
}
@@ -284,8 +286,6 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
284286
if(options.get_bool_option("fpa"))
285287
smt2_conv->use_FPA_theory = true;
286288

287-
smt2_conv->set_message_handler(message_handler);
288-
289289
set_prop_conv_time_limit(*smt2_conv);
290290
return util_make_unique<solvert>(std::move(smt2_conv));
291291
}
@@ -314,8 +314,6 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
314314
if(options.get_bool_option("fpa"))
315315
smt2_conv->use_FPA_theory = true;
316316

317-
smt2_conv->set_message_handler(message_handler);
318-
319317
set_prop_conv_time_limit(*smt2_conv);
320318
return util_make_unique<solvert>(std::move(smt2_conv), std::move(out));
321319
}

‎src/goto-instrument/accelerate/scratch_program.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,7 @@ bool scratch_programt::check_sat(bool do_slice)
5151
return false;
5252
}
5353

54-
equation.convert(*checker);
54+
equation.convert(*checker, message_handler);
5555

5656
#ifdef DEBUG
5757
std::cout << "Finished symex, invoking decision procedure.\n";

‎src/goto-instrument/accelerate/scratch_program.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,7 @@ class scratch_programt:public goto_programt
3838
public:
3939
scratch_programt(symbol_tablet &_symbol_table, message_handlert &mh)
4040
: constant_propagation(true),
41+
message_handler(mh),
4142
symbol_table(_symbol_table),
4243
symex_symbol_table(),
4344
ns(symbol_table, symex_symbol_table),
@@ -74,6 +75,7 @@ class scratch_programt:public goto_programt
7475
bool constant_propagation;
7576

7677
protected:
78+
message_handlert &message_handler;
7779
goto_symex_statet symex_state;
7880
goto_functionst functions;
7981
symbol_tablet &symbol_table;

‎src/goto-symex/symex_target_equation.cpp

Lines changed: 50 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -328,19 +328,20 @@ void symex_target_equationt::constraint(
328328
}
329329

330330
void symex_target_equationt::convert(
331-
prop_convt &prop_conv)
331+
prop_convt &prop_conv,
332+
message_handlert &message_handler)
332333
{
333334
try
334335
{
335-
convert_guards(prop_conv);
336-
convert_assignments(prop_conv);
336+
convert_guards(prop_conv, message_handler);
337+
convert_assignments(prop_conv, message_handler);
337338
convert_decls(prop_conv);
338-
convert_assumptions(prop_conv);
339-
convert_assertions(prop_conv);
340-
convert_goto_instructions(prop_conv);
339+
convert_assumptions(prop_conv, message_handler);
340+
convert_assertions(prop_conv, message_handler);
341+
convert_goto_instructions(prop_conv, message_handler);
341342
convert_function_calls(prop_conv);
342343
convert_io(prop_conv);
343-
convert_constraints(prop_conv);
344+
convert_constraints(prop_conv, message_handler);
344345
}
345346
catch(const equation_conversion_exceptiont &conversion_exception)
346347
{
@@ -351,18 +352,19 @@ void symex_target_equationt::convert(
351352
}
352353

353354
void symex_target_equationt::convert_assignments(
354-
decision_proceduret &decision_procedure) const
355+
decision_proceduret &decision_procedure,
356+
message_handlert &message_handler) const
355357
{
358+
messaget log(message_handler);
359+
356360
for(const auto &step : SSA_steps)
357361
{
358362
if(step.is_assignment() && !step.ignore)
359363
{
360-
decision_procedure.conditional_output(
361-
decision_procedure.debug(),
362-
[&step](messaget::mstreamt &mstream) {
363-
step.output(mstream);
364-
mstream << messaget::eom;
365-
});
364+
log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
365+
step.output(mstream);
366+
mstream << messaget::eom;
367+
});
366368

367369
decision_procedure.set_to_true(step.cond_expr);
368370
}
@@ -393,20 +395,21 @@ void symex_target_equationt::convert_decls(
393395
}
394396

395397
void symex_target_equationt::convert_guards(
396-
prop_convt &prop_conv)
398+
prop_convt &prop_conv,
399+
message_handlert &message_handler)
397400
{
401+
messaget log(message_handler);
402+
398403
for(auto &step : SSA_steps)
399404
{
400405
if(step.ignore)
401406
step.guard_literal=const_literal(false);
402407
else
403408
{
404-
prop_conv.conditional_output(
405-
prop_conv.debug(),
406-
[&step](messaget::mstreamt &mstream) {
407-
step.output(mstream);
408-
mstream << messaget::eom;
409-
});
409+
log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
410+
step.output(mstream);
411+
mstream << messaget::eom;
412+
});
410413

411414
try
412415
{
@@ -423,8 +426,11 @@ void symex_target_equationt::convert_guards(
423426
}
424427

425428
void symex_target_equationt::convert_assumptions(
426-
prop_convt &prop_conv)
429+
prop_convt &prop_conv,
430+
message_handlert &message_handler)
427431
{
432+
messaget log(message_handler);
433+
428434
for(auto &step : SSA_steps)
429435
{
430436
if(step.is_assume())
@@ -433,9 +439,8 @@ void symex_target_equationt::convert_assumptions(
433439
step.cond_literal=const_literal(true);
434440
else
435441
{
436-
prop_conv.conditional_output(
437-
prop_conv.debug(),
438-
[&step](messaget::mstreamt &mstream) {
442+
log.conditional_output(
443+
log.debug(), [&step](messaget::mstreamt &mstream) {
439444
step.output(mstream);
440445
mstream << messaget::eom;
441446
});
@@ -456,8 +461,11 @@ void symex_target_equationt::convert_assumptions(
456461
}
457462

458463
void symex_target_equationt::convert_goto_instructions(
459-
prop_convt &prop_conv)
464+
prop_convt &prop_conv,
465+
message_handlert &message_handler)
460466
{
467+
messaget log(message_handler);
468+
461469
for(auto &step : SSA_steps)
462470
{
463471
if(step.is_goto())
@@ -466,9 +474,8 @@ void symex_target_equationt::convert_goto_instructions(
466474
step.cond_literal=const_literal(true);
467475
else
468476
{
469-
prop_conv.conditional_output(
470-
prop_conv.debug(),
471-
[&step](messaget::mstreamt &mstream) {
477+
log.conditional_output(
478+
log.debug(), [&step](messaget::mstreamt &mstream) {
472479
step.output(mstream);
473480
mstream << messaget::eom;
474481
});
@@ -489,17 +496,19 @@ void symex_target_equationt::convert_goto_instructions(
489496
}
490497

491498
void symex_target_equationt::convert_constraints(
492-
decision_proceduret &decision_procedure) const
499+
decision_proceduret &decision_procedure,
500+
message_handlert &message_handler) const
493501
{
502+
messaget log(message_handler);
503+
494504
for(const auto &step : SSA_steps)
495505
{
496506
if(step.is_constraint())
497507
{
498508
if(!step.ignore)
499509
{
500-
decision_procedure.conditional_output(
501-
decision_procedure.debug(),
502-
[&step](messaget::mstreamt &mstream) {
510+
log.conditional_output(
511+
log.debug(), [&step](messaget::mstreamt &mstream) {
503512
step.output(mstream);
504513
mstream << messaget::eom;
505514
});
@@ -520,7 +529,8 @@ void symex_target_equationt::convert_constraints(
520529
}
521530

522531
void symex_target_equationt::convert_assertions(
523-
prop_convt &prop_conv)
532+
prop_convt &prop_conv,
533+
message_handlert &message_handler)
524534
{
525535
// we find out if there is only _one_ assertion,
526536
// which allows for a simpler formula
@@ -554,16 +564,16 @@ void symex_target_equationt::convert_assertions(
554564

555565
exprt assumption=true_exprt();
556566

567+
messaget log(message_handler);
568+
557569
for(auto &step : SSA_steps)
558570
{
559571
if(step.is_assert())
560572
{
561-
prop_conv.conditional_output(
562-
prop_conv.debug(),
563-
[&step](messaget::mstreamt &mstream) {
564-
step.output(mstream);
565-
mstream << messaget::eom;
566-
});
573+
log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
574+
step.output(mstream);
575+
mstream << messaget::eom;
576+
});
567577

568578
implies_exprt implication(
569579
assumption,

‎src/goto-symex/symex_target_equation.h

Lines changed: 22 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -166,12 +166,16 @@ class symex_target_equationt:public symex_targett
166166
/// format. The method iterates over the equation, i.e. over the SSA steps and
167167
/// converts each type of step separately.
168168
/// \param prop_conv: A handle to a particular decision procedure interface
169-
void convert(prop_convt &prop_conv);
169+
/// \param message_handler: message handler
170+
void convert(prop_convt &prop_conv, message_handlert &message_handler);
170171

171172
/// Converts assignments: set the equality _lhs==rhs_ to _True_.
172173
/// \param decision_procedure: A handle to a particular decision procedure
173174
/// interface
174-
void convert_assignments(decision_proceduret &decision_procedure) const;
175+
/// \param message_handler: message handler
176+
void convert_assignments(
177+
decision_proceduret &decision_procedure,
178+
message_handlert &message_handler) const;
175179

176180
/// Converts declarations: these are effectively ignored by the decision
177181
/// procedure.
@@ -180,25 +184,36 @@ class symex_target_equationt:public symex_targett
180184

181185
/// Converts assumptions: convert the expression the assumption represents.
182186
/// \param prop_conv: A handle to a particular decision procedure interface
183-
void convert_assumptions(prop_convt &prop_conv);
187+
/// \param message_handler: message handler
188+
void
189+
convert_assumptions(prop_convt &prop_conv, message_handlert &message_handler);
184190

185191
/// Converts assertions: build a disjunction of negated assertions.
186192
/// \param prop_conv: A handle to a particular decision procedure interface
187-
void convert_assertions(prop_convt &prop_conv);
193+
/// \param message_handler: message handler
194+
void
195+
convert_assertions(prop_convt &prop_conv, message_handlert &message_handler);
188196

189197
/// Converts constraints: set the represented condition to _True_.
190198
/// \param decision_procedure: A handle to a particular decision procedure
191199
/// interface
192-
void convert_constraints(decision_proceduret &decision_procedure) const;
200+
/// \param message_handler: message handler
201+
void convert_constraints(
202+
decision_proceduret &decision_procedure,
203+
message_handlert &message_handler) const;
193204

194205
/// Converts goto instructions: convert the expression representing the
195206
/// condition of this goto.
196207
/// \param prop_conv: A handle to a particular decision procedure interface
197-
void convert_goto_instructions(prop_convt &prop_conv);
208+
/// \param message_handler: message handler
209+
void convert_goto_instructions(
210+
prop_convt &prop_conv,
211+
message_handlert &message_handler);
198212

199213
/// Converts guards: convert the expression the guard represents.
200214
/// \param prop_conv: A handle to a particular decision procedure interface
201-
void convert_guards(prop_convt &prop_conv);
215+
/// \param message_handler: message handler
216+
void convert_guards(prop_convt &prop_conv, message_handlert &message_handler);
202217

203218
/// Converts function calls: for each argument build an equality between its
204219
/// symbol and the argument itself.

‎src/solvers/prop/prop_conv.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
1515

1616
#include <util/decision_procedure.h>
1717
#include <util/expr.h>
18+
#include <util/message.h>
1819
#include <util/std_expr.h>
1920

2021
#include "literal.h"
@@ -64,7 +65,7 @@ class prop_convt:public decision_proceduret
6465

6566
/*! \brief TO_BE_DOCUMENTED
6667
*/
67-
class prop_conv_solvert:public prop_convt
68+
class prop_conv_solvert : public prop_convt, public messaget
6869
{
6970
public:
7071
explicit prop_conv_solvert(propt &_prop) : prop(_prop)

‎src/solvers/smt2/smt2_dec.h

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,9 @@ class smt2_stringstreamt
2222

2323
/*! \brief Decision procedure interface for various SMT 2.x solvers
2424
*/
25-
class smt2_dect:protected smt2_stringstreamt, public smt2_convt
25+
class smt2_dect : protected smt2_stringstreamt,
26+
public smt2_convt,
27+
public messaget
2628
{
2729
public:
2830
smt2_dect(

0 commit comments

Comments
 (0)