Skip to content

Commit 13712c4

Browse files
tautschnigtautschnig
authored
Merge pull request #4442 from peterschrammel/prop-conv-solver-messaget
prop_conv_solvert is not a messaget
2 parents 0e928a3 + 6149323 commit 13712c4

32 files changed

+314
-331
lines changed

‎jbmc/src/jbmc/bmc.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -204,8 +204,11 @@ safety_checkert::resultt bmct::stop_on_fail()
204204
if(options.get_bool_option("trace"))
205205
{
206206
if(options.get_bool_option("beautify"))
207-
counterexample_beautificationt()(
207+
{
208+
// NOLINTNEXTLINE(whitespace/braces)
209+
counterexample_beautificationt{ui_message_handler}(
208210
dynamic_cast<boolbvt &>(prop_conv), equation);
211+
}
209212

210213
build_error_trace(
211214
error_trace, ns, equation, prop_conv, ui_message_handler);

‎src/goto-checker/counterexample_beautification.cpp

Lines changed: 10 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,12 @@ Author: Daniel Kroening, [email protected]
1919
#include <solvers/prop/literal_expr.h>
2020
#include <solvers/prop/minimize.h>
2121

22+
counterexample_beautificationt::counterexample_beautificationt(
23+
message_handlert &message_handler)
24+
: log(message_handler)
25+
{
26+
}
27+
2228
void counterexample_beautificationt::get_minimization_list(
2329
prop_convt &prop_conv,
2430
const symex_target_equationt &equation,
@@ -92,7 +98,7 @@ operator()(boolbvt &boolbv, const symex_target_equationt &equation)
9298
boolbv.set_to(literal_exprt(failed->cond_literal), false);
9399

94100
{
95-
boolbv.status() << "Beautifying counterexample (guards)" << messaget::eom;
101+
log.status() << "Beautifying counterexample (guards)" << messaget::eom;
96102

97103
// compute weights for guards
98104
typedef std::map<literalt, unsigned> guard_countt;
@@ -117,8 +123,7 @@ operator()(boolbvt &boolbv, const symex_target_equationt &equation)
117123
}
118124

119125
// give to propositional minimizer
120-
prop_minimizet prop_minimize(boolbv);
121-
prop_minimize.set_message_handler(boolbv.get_message_handler());
126+
prop_minimizet prop_minimize{boolbv, log.get_message_handler()};
122127

123128
for(const auto &g : guard_count)
124129
prop_minimize.objective(g.first, g.second);
@@ -128,16 +133,15 @@ operator()(boolbvt &boolbv, const symex_target_equationt &equation)
128133
}
129134

130135
{
131-
boolbv.status() << "Beautifying counterexample (values)" << messaget::eom;
136+
log.status() << "Beautifying counterexample (values)" << messaget::eom;
132137

133138
// get symbols we care about
134139
minimization_listt minimization_list;
135140

136141
get_minimization_list(boolbv, equation, minimization_list);
137142

138143
// minimize
139-
bv_minimizet bv_minimize(boolbv);
140-
bv_minimize.set_message_handler(boolbv.get_message_handler());
144+
bv_minimizet bv_minimize(boolbv, log.get_message_handler());
141145
bv_minimize(minimization_list);
142146
}
143147
}

‎src/goto-checker/counterexample_beautification.h

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -21,9 +21,8 @@ Author: Daniel Kroening, [email protected]
2121
class counterexample_beautificationt
2222
{
2323
public:
24-
virtual ~counterexample_beautificationt()
25-
{
26-
}
24+
explicit counterexample_beautificationt(message_handlert &message_handler);
25+
virtual ~counterexample_beautificationt() = default;
2726

2827
void operator()(boolbvt &boolbv, const symex_target_equationt &equation);
2928

@@ -41,6 +40,8 @@ class counterexample_beautificationt
4140

4241
// the failed property
4342
symex_target_equationt::SSA_stepst::const_iterator failed;
43+
44+
messaget log;
4445
};
4546

4647
#endif // CPROVER_GOTO_CHECKER_COUNTEREXAMPLE_BEAUTIFICATION_H

‎src/goto-checker/multi_path_symex_checker.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -104,7 +104,8 @@ goto_tracet multi_path_symex_checkert::build_shortest_trace() const
104104
{
105105
if(options.get_bool_option("beautify"))
106106
{
107-
counterexample_beautificationt()(
107+
// NOLINTNEXTLINE(whitespace/braces)
108+
counterexample_beautificationt{ui_message_handler}(
108109
dynamic_cast<boolbvt &>(property_decider.get_solver()), equation);
109110
}
110111

‎src/goto-checker/single_path_symex_checker.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -133,7 +133,8 @@ goto_tracet single_path_symex_checkert::build_shortest_trace() const
133133
{
134134
if(options.get_bool_option("beautify"))
135135
{
136-
counterexample_beautificationt()(
136+
// NOLINTNEXTLINE(whitespace/braces)
137+
counterexample_beautificationt{ui_message_handler}(
137138
dynamic_cast<boolbvt &>(property_decider->get_solver()),
138139
property_decider->get_equation());
139140
}

‎src/goto-checker/solver_factory.cpp

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -157,8 +157,8 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
157157
solver->set_prop(util_make_unique<satcheckt>(message_handler));
158158
}
159159

160-
auto bv_pointers = util_make_unique<bv_pointerst>(ns, solver->prop());
161-
bv_pointers->set_message_handler(message_handler);
160+
auto bv_pointers =
161+
util_make_unique<bv_pointerst>(ns, solver->prop(), message_handler);
162162

163163
if(options.get_option("arrays-uf") == "never")
164164
bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_NONE;
@@ -180,8 +180,8 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
180180

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

183-
auto bv_dimacs = util_make_unique<bv_dimacst>(ns, *prop, filename);
184-
bv_dimacs->set_message_handler(message_handler);
183+
auto bv_dimacs =
184+
util_make_unique<bv_dimacst>(ns, *prop, message_handler, filename);
185185
return util_make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
186186
}
187187

@@ -209,9 +209,9 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
209209

210210
info.refine_arrays = options.get_bool_option("refine-arrays");
211211
info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
212+
info.message_handler = &message_handler;
212213

213214
auto prop_conv = util_make_unique<bv_refinementt>(info);
214-
prop_conv->set_message_handler(message_handler);
215215
set_prop_conv_time_limit(*prop_conv);
216216
return util_make_unique<solvert>(std::move(prop_conv), std::move(prop));
217217
}
@@ -233,9 +233,9 @@ solver_factoryt::get_string_refinement()
233233
options.get_unsigned_int_option("max-node-refinement");
234234
info.refine_arrays = options.get_bool_option("refine-arrays");
235235
info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
236+
info.message_handler = &message_handler;
236237

237238
auto prop_conv = util_make_unique<string_refinementt>(info);
238-
prop_conv->set_message_handler(message_handler);
239239
set_prop_conv_time_limit(*prop_conv);
240240
return util_make_unique<solvert>(std::move(prop_conv), std::move(prop));
241241
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@ class scratch_programt:public goto_programt
4949
options(get_default_options()),
5050
symex(mh, symbol_table, equation, options, path_storage, guard_manager),
5151
satcheck(util_make_unique<satcheckt>(mh)),
52-
satchecker(ns, *satcheck),
52+
satchecker(ns, *satcheck, mh),
5353
z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3),
5454
checker(&z3) // checker(&satchecker)
5555
{

‎src/solvers/flattening/arrays.cpp

Lines changed: 33 additions & 50 deletions
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,11 @@ Author: Daniel Kroening, [email protected]
2222

2323
#include <unordered_set>
2424

25-
arrayst::arrayst(const namespacet &_ns, propt &_prop)
26-
: equalityt(_prop), ns(_ns)
25+
arrayst::arrayst(
26+
const namespacet &_ns,
27+
propt &_prop,
28+
message_handlert &message_handler)
29+
: equalityt(_prop, message_handler), ns(_ns)
2730
{
2831
lazy_arrays = false; // will be set to true when --refine is used
2932
incremental_cache = false; // for incremental solving
@@ -45,14 +48,10 @@ literalt arrayst::record_array_equality(
4548
const exprt &op0=equality.op0();
4649
const exprt &op1=equality.op1();
4750

48-
// check types
49-
if(op0.type() != op1.type())
50-
{
51-
error() << equality.pretty() << messaget::eom;
52-
DATA_INVARIANT(
53-
false,
54-
"record_array_equality got equality without matching types");
55-
}
51+
DATA_INVARIANT_WITH_DIAGNOSTICS(
52+
op0.type() == op1.type(),
53+
"record_array_equality got equality without matching types",
54+
irep_pretty_diagnosticst{equality});
5655

5756
DATA_INVARIANT(
5857
op0.type().id() == ID_array,
@@ -113,12 +112,10 @@ void arrayst::collect_arrays(const exprt &a)
113112
{
114113
const with_exprt &with_expr=to_with_expr(a);
115114

116-
// check types
117-
if(array_type != with_expr.old().type())
118-
{
119-
error() << a.pretty() << messaget::eom;
120-
DATA_INVARIANT(false, "collect_arrays got 'with' without matching types");
121-
}
115+
DATA_INVARIANT_WITH_DIAGNOSTICS(
116+
array_type == with_expr.old().type(),
117+
"collect_arrays got 'with' without matching types",
118+
irep_pretty_diagnosticst{a});
122119

123120
arrays.make_union(a, with_expr.old());
124121
collect_arrays(with_expr.old());
@@ -134,14 +131,10 @@ void arrayst::collect_arrays(const exprt &a)
134131
{
135132
const update_exprt &update_expr=to_update_expr(a);
136133

137-
// check types
138-
if(array_type != update_expr.old().type())
139-
{
140-
error() << a.pretty() << messaget::eom;
141-
DATA_INVARIANT(
142-
false,
143-
"collect_arrays got 'update' without matching types");
144-
}
134+
DATA_INVARIANT_WITH_DIAGNOSTICS(
135+
array_type == update_expr.old().type(),
136+
"collect_arrays got 'update' without matching types",
137+
irep_pretty_diagnosticst{a});
145138

146139
arrays.make_union(a, update_expr.old());
147140
collect_arrays(update_expr.old());
@@ -156,19 +149,15 @@ void arrayst::collect_arrays(const exprt &a)
156149
{
157150
const if_exprt &if_expr=to_if_expr(a);
158151

159-
// check types
160-
if(array_type != if_expr.true_case().type())
161-
{
162-
error() << a.pretty() << messaget::eom;
163-
DATA_INVARIANT(false, "collect_arrays got if without matching types");
164-
}
152+
DATA_INVARIANT_WITH_DIAGNOSTICS(
153+
array_type == if_expr.true_case().type(),
154+
"collect_arrays got if without matching types",
155+
irep_pretty_diagnosticst{a});
165156

166-
// check types
167-
if(array_type != if_expr.false_case().type())
168-
{
169-
error() << a.pretty() << messaget::eom;
170-
DATA_INVARIANT(false, "collect_arrays got if without matching types");
171-
}
157+
DATA_INVARIANT_WITH_DIAGNOSTICS(
158+
array_type == if_expr.false_case().type(),
159+
"collect_arrays got if without matching types",
160+
irep_pretty_diagnosticst{a});
172161

173162
arrays.make_union(a, if_expr.true_case());
174163
arrays.make_union(a, if_expr.false_case());
@@ -518,13 +507,10 @@ void arrayst::add_array_constraints_with(
518507

519508
index_exprt index_expr(expr, index, expr.type().subtype());
520509

521-
if(index_expr.type()!=value.type())
522-
{
523-
error() << expr.pretty() << messaget::eom;
524-
DATA_INVARIANT(
525-
false,
526-
"with-expression operand should match array element type");
527-
}
510+
DATA_INVARIANT_WITH_DIAGNOSTICS(
511+
index_expr.type() == value.type(),
512+
"with-expression operand should match array element type",
513+
irep_pretty_diagnosticst{expr});
528514

529515
lazy_constraintt lazy(
530516
lazy_typet::ARRAY_WITH, equal_exprt(index_expr, value));
@@ -594,13 +580,10 @@ void arrayst::add_array_constraints_update(
594580
{
595581
index_exprt index_expr(expr, index, expr.type().subtype());
596582

597-
if(index_expr.type()!=value.type())
598-
{
599-
prop.message.error() << expr.pretty() << messaget::eom;
600-
DATA_INVARIANT(
601-
false,
602-
"update operand should match array element type");
603-
}
583+
DATA_INVARIANT_WITH_DIAGNOSTICS(
584+
index_expr.type()==value.type(),
585+
"update operand should match array element type",
586+
irep_pretty_diagnosticst{expr});
604587

605588
set_to_true(equal_exprt(index_expr, value));
606589
}

‎src/solvers/flattening/arrays.h

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,10 @@ class update_exprt;
2929
class arrayst:public equalityt
3030
{
3131
public:
32-
arrayst(const namespacet &_ns, propt &_prop);
32+
arrayst(
33+
const namespacet &_ns,
34+
propt &_prop,
35+
message_handlert &message_handler);
3336

3437
void post_process() override
3538
{

‎src/solvers/flattening/boolbv.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -191,7 +191,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
191191
else if(expr.id()==ID_member)
192192
return convert_member(to_member_expr(expr));
193193
else if(expr.id()==ID_with)
194-
return convert_with(expr);
194+
return convert_with(to_with_expr(expr));
195195
else if(expr.id()==ID_update)
196196
return convert_update(expr);
197197
else if(expr.id()==ID_width)

‎src/solvers/flattening/boolbv.h

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -32,8 +32,11 @@ class member_exprt;
3232
class boolbvt:public arrayst
3333
{
3434
public:
35-
boolbvt(const namespacet &_ns, propt &_prop)
36-
: arrayst(_ns, _prop),
35+
boolbvt(
36+
const namespacet &_ns,
37+
propt &_prop,
38+
message_handlert &message_handler)
39+
: arrayst(_ns, _prop, message_handler),
3740
unbounded_array(unbounded_arrayt::U_NONE),
3841
boolbv_width(_ns),
3942
bv_utils(_prop),
@@ -156,7 +159,7 @@ class boolbvt:public arrayst
156159
virtual bvt convert_floatbv_op(const exprt &expr);
157160
virtual bvt convert_floatbv_typecast(const floatbv_typecast_exprt &expr);
158161
virtual bvt convert_member(const member_exprt &expr);
159-
virtual bvt convert_with(const exprt &expr);
162+
virtual bvt convert_with(const with_exprt &expr);
160163
virtual bvt convert_update(const exprt &expr);
161164
virtual bvt convert_case(const exprt &expr);
162165
virtual bvt convert_cond(const cond_exprt &);

‎src/solvers/flattening/boolbv_constant.cpp

Lines changed: 12 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -31,12 +31,10 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)
3131
{
3232
const bvt &tmp=convert_bv(*it);
3333

34-
if(tmp.size()!=op_width)
35-
{
36-
error().source_location=expr.find_source_location();
37-
error() << "convert_constant: unexpected operand width" << eom;
38-
throw 0;
39-
}
34+
DATA_INVARIANT_WITH_DIAGNOSTICS(
35+
tmp.size() == op_width,
36+
"convert_constant: unexpected operand width",
37+
irep_pretty_diagnosticst{expr});
4038

4139
for(std::size_t j=0; j<op_width; j++)
4240
bv[offset+j]=tmp[j];
@@ -99,13 +97,10 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)
9997
{
10098
const std::string &binary=id2string(expr.get_value());
10199

102-
if(binary.size()*2!=width)
103-
{
104-
error().source_location=expr.find_source_location();
105-
error() << "wrong value length in constant: "
106-
<< expr.pretty() << eom;
107-
throw 0;
108-
}
100+
DATA_INVARIANT_WITH_DIAGNOSTICS(
101+
binary.size() * 2 == width,
102+
"wrong value length in constant",
103+
irep_pretty_diagnosticst{expr});
109104

110105
for(std::size_t i=0; i<binary.size(); i++)
111106
{
@@ -135,10 +130,10 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)
135130
break;
136131

137132
default:
138-
error().source_location=expr.find_source_location();
139-
error() << "unknown character in Verilog constant:"
140-
<< expr.pretty() << eom;
141-
throw 0;
133+
DATA_INVARIANT_WITH_DIAGNOSTICS(
134+
false,
135+
"unknown character in Verilog constant",
136+
irep_pretty_diagnosticst{expr});
142137
}
143138
}
144139

0 commit comments

Comments
 (0)