Skip to content

Commit 9b32b79

Browse files
tautschnigtautschnig
committed
String solver: pass around a configured message handler
Using null_message_handlert hides errors, as the (now failing) regression test demonstrates.
1 parent aef7513 commit 9b32b79

21 files changed

+172
-106
lines changed

‎jbmc/regression/strings-smoke-tests/java_set_length/test.desc

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
test_set_length
33
--function test_set_length.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=10$
@@ -8,3 +8,4 @@ test_set_length
88
^\[.*assertion.3\].* line 11.* FAILURE$
99
--
1010
non equal types
11+
^warning: ignoring

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

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -218,7 +218,7 @@ SCENARIO(
218218
{ab, b, from_integer(2)}};
219219

220220
// Generating the corresponding axioms and simplifying, recording info
221-
string_constraint_generatort generator(empty_ns);
221+
string_constraint_generatort generator(empty_ns, null_message_handler);
222222
const auto pair = generator.add_axioms_for_function_application(func);
223223
const string_constraintst &constraints = pair.second;
224224

@@ -313,7 +313,7 @@ SCENARIO(
313313
a_array};
314314

315315
// Create witness for axiom
316-
string_constraint_generatort generator(empty_ns);
316+
string_constraint_generatort generator(empty_ns, null_message_handler);
317317
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
318318
witnesses.emplace(vacuous, generator.fresh_symbol("w", t.witness_type()));
319319

@@ -363,7 +363,7 @@ SCENARIO(
363363
b_array};
364364

365365
// Create witness for axiom
366-
string_constraint_generatort generator(empty_ns);
366+
string_constraint_generatort generator(empty_ns, null_message_handler);
367367
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
368368
witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type()));
369369

@@ -414,7 +414,7 @@ SCENARIO(
414414
empty_array};
415415

416416
// Create witness for axiom
417-
string_constraint_generatort generator(empty_ns);
417+
string_constraint_generatort generator(empty_ns, null_message_handler);
418418
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
419419
witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type()));
420420

@@ -467,7 +467,7 @@ SCENARIO(
467467
ab_array};
468468

469469
// Create witness for axiom
470-
string_constraint_generatort generator(empty_ns);
470+
string_constraint_generatort generator(empty_ns, null_message_handler);
471471
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
472472
witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type()));
473473

@@ -518,7 +518,7 @@ SCENARIO(
518518
cd_array};
519519

520520
// Create witness for axiom
521-
string_constraint_generatort generator(empty_ns);
521+
string_constraint_generatort generator(empty_ns, null_message_handler);
522522
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
523523
witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type()));
524524

‎src/solvers/strings/string_builtin_function.cpp

Lines changed: 21 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -101,7 +101,8 @@ optionalt<exprt> string_concat_char_builtin_functiont::eval(
101101
/// * result[input.length] = character
102102
/// * return_code = 0
103103
string_constraintst string_concat_char_builtin_functiont::constraints(
104-
string_constraint_generatort &generator) const
104+
string_constraint_generatort &generator,
105+
message_handlert &message_handler) const
105106
{
106107
string_constraintst constraints;
107108
constraints.existential.push_back(length_constraint());
@@ -111,7 +112,7 @@ string_constraintst string_concat_char_builtin_functiont::constraints(
111112
const exprt upper_bound =
112113
zero_if_negative(array_pool.get_or_create_length(input));
113114
return string_constraintt(
114-
idx, upper_bound, equal_exprt(input[idx], result[idx]));
115+
idx, upper_bound, equal_exprt(input[idx], result[idx]), message_handler);
115116
}());
116117
constraints.existential.push_back(
117118
equal_exprt(result[array_pool.get_or_create_length(input)], character));
@@ -151,7 +152,8 @@ optionalt<exprt> string_set_char_builtin_functiont::eval(
151152
/// 3. forall 0 <= i < max(0, min(res.length, pos)). res[i] = str[i]
152153
/// 4. forall max(0, pos+1) <= i < res.length. res[i] = str[i]
153154
string_constraintst string_set_char_builtin_functiont::constraints(
154-
string_constraint_generatort &generator) const
155+
string_constraint_generatort &generator,
156+
message_handlert &message_handler) const
155157
{
156158
string_constraintst constraints;
157159
constraints.existential.push_back(length_constraint());
@@ -169,7 +171,8 @@ string_constraintst string_set_char_builtin_functiont::constraints(
169171
q,
170172
zero_if_negative(
171173
minimum(array_pool.get_or_create_length(result), position)),
172-
a3_body);
174+
a3_body,
175+
message_handler);
173176
}());
174177
constraints.universal.push_back([&] {
175178
const symbol_exprt q2 =
@@ -179,7 +182,8 @@ string_constraintst string_set_char_builtin_functiont::constraints(
179182
q2,
180183
zero_if_negative(plus_exprt(position, from_integer(1, position.type()))),
181184
zero_if_negative(array_pool.get_or_create_length(result)),
182-
a4_body);
185+
a4_body,
186+
message_handler);
183187
}());
184188
return constraints;
185189
}
@@ -279,7 +283,8 @@ static exprt is_lower_case(const exprt &character)
279283
/// characters: `diff = 'a'-'A' = 0x20` and `is_upper_case` is true for the
280284
/// upper case characters of Basic Latin and Latin-1 supplement of unicode.
281285
string_constraintst string_to_lower_case_builtin_functiont::constraints(
282-
string_constraint_generatort &generator) const
286+
string_constraint_generatort &generator,
287+
message_handlert &message_handler) const
283288
{
284289
// \todo for now, only characters in Basic Latin and Latin-1 supplement
285290
// are supported (up to 0x100), we should add others using case mapping
@@ -302,7 +307,8 @@ string_constraintst string_to_lower_case_builtin_functiont::constraints(
302307
return string_constraintt(
303308
idx,
304309
zero_if_negative(array_pool.get_or_create_length(result)),
305-
conditional_convert);
310+
conditional_convert,
311+
message_handler);
306312
}());
307313
return constraints;
308314
}
@@ -334,7 +340,8 @@ optionalt<exprt> string_to_upper_case_builtin_functiont::eval(
334340
/// \param fresh_symbol: generator of fresh symbols
335341
/// \return set of constraints
336342
string_constraintst string_to_upper_case_builtin_functiont::constraints(
337-
symbol_generatort &fresh_symbol) const
343+
symbol_generatort &fresh_symbol,
344+
message_handlert &message_handler) const
338345
{
339346
string_constraintst constraints;
340347
constraints.existential.push_back(length_constraint());
@@ -350,7 +357,8 @@ string_constraintst string_to_upper_case_builtin_functiont::constraints(
350357
zero_if_negative(array_pool.get_or_create_length(result)),
351358
equal_exprt(
352359
result[idx],
353-
if_exprt(is_lower_case(input[idx]), converted, input[idx])));
360+
if_exprt(is_lower_case(input[idx]), converted, input[idx])),
361+
message_handler);
354362
}());
355363
return constraints;
356364
}
@@ -406,7 +414,8 @@ optionalt<exprt> string_of_int_builtin_functiont::eval(
406414
}
407415

408416
string_constraintst string_of_int_builtin_functiont::constraints(
409-
string_constraint_generatort &generator) const
417+
string_constraint_generatort &generator,
418+
message_handlert &message_handler) const
410419
{
411420
auto pair =
412421
generator.add_axioms_for_string_of_int_with_radix(result, arg, radix, 0);
@@ -475,7 +484,8 @@ string_builtin_function_with_no_evalt::string_builtin_function_with_no_evalt(
475484
}
476485

477486
string_constraintst string_builtin_function_with_no_evalt::constraints(
478-
string_constraint_generatort &generator) const
487+
string_constraint_generatort &generator,
488+
message_handlert &message_handler) const
479489
{
480490
auto pair =
481491
generator.add_axioms_for_function_application(function_application);

‎src/solvers/strings/string_builtin_function.h

Lines changed: 23 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -102,7 +102,7 @@ class string_builtin_functiont
102102
/// the result of this function.
103103
/// This logic is implemented in add_constraints().
104104
virtual string_constraintst
105-
constraints(string_constraint_generatort &constraint_generator) const = 0;
105+
constraints(string_constraint_generatort &, message_handlert &) const = 0;
106106

107107
/// Constraint ensuring that the length of the strings are coherent with
108108
/// the function call.
@@ -198,8 +198,9 @@ class string_concat_char_builtin_functiont
198198
return "concat_char";
199199
}
200200

201-
string_constraintst
202-
constraints(string_constraint_generatort &generator) const override;
201+
string_constraintst constraints(
202+
string_constraint_generatort &generator,
203+
message_handlert &message_handlert) const override;
203204

204205
exprt length_constraint() const override;
205206
};
@@ -235,8 +236,9 @@ class string_set_char_builtin_functiont
235236
return "set_char";
236237
}
237238

238-
string_constraintst
239-
constraints(string_constraint_generatort &generator) const override;
239+
string_constraintst constraints(
240+
string_constraint_generatort &generator,
241+
message_handlert &message_handler) const override;
240242

241243
// \todo: length_constraint is not the best possible name because we also
242244
// \todo: add constraint about the return code
@@ -265,8 +267,9 @@ class string_to_lower_case_builtin_functiont
265267
return "to_lower_case";
266268
}
267269

268-
string_constraintst
269-
constraints(string_constraint_generatort &generator) const override;
270+
string_constraintst constraints(
271+
string_constraint_generatort &generator,
272+
message_handlert &message_handler) const override;
270273

271274
exprt length_constraint() const override
272275
{
@@ -313,12 +316,15 @@ class string_to_upper_case_builtin_functiont
313316
return "to_upper_case";
314317
}
315318

316-
string_constraintst constraints(class symbol_generatort &fresh_symbol) const;
319+
string_constraintst constraints(
320+
class symbol_generatort &fresh_symbol,
321+
message_handlert &message_handler) const;
317322

318-
string_constraintst
319-
constraints(string_constraint_generatort &generator) const override
323+
string_constraintst constraints(
324+
string_constraint_generatort &generator,
325+
message_handlert &message_handler) const override
320326
{
321-
return constraints(generator.fresh_symbol);
327+
return constraints(generator.fresh_symbol, message_handler);
322328
};
323329

324330
exprt length_constraint() const override
@@ -379,8 +385,9 @@ class string_of_int_builtin_functiont : public string_creation_builtin_functiont
379385
return "string_of_int";
380386
}
381387

382-
string_constraintst
383-
constraints(string_constraint_generatort &generator) const override;
388+
string_constraintst constraints(
389+
string_constraint_generatort &generator,
390+
message_handlert &message_handler) const override;
384391

385392
exprt length_constraint() const override;
386393

@@ -439,8 +446,9 @@ class string_builtin_function_with_no_evalt : public string_builtin_functiont
439446
return {};
440447
}
441448

442-
string_constraintst
443-
constraints(string_constraint_generatort &generator) const override;
449+
string_constraintst constraints(
450+
string_constraint_generatort &generator,
451+
message_handlert &message_handler) const override;
444452

445453
exprt length_constraint() const override
446454
{

‎src/solvers/strings/string_concatenation_builtin_function.cpp

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -73,7 +73,8 @@ string_constraint_generatort::add_axioms_for_concat_substr(
7373
return string_constraintt(
7474
idx,
7575
zero_if_negative(array_pool.get_or_create_length(s1)),
76-
equal_exprt(s1[idx], res[idx]));
76+
equal_exprt(s1[idx], res[idx]),
77+
message_handler);
7778
}());
7879

7980
// Axiom 3.
@@ -86,7 +87,8 @@ string_constraint_generatort::add_axioms_for_concat_substr(
8687
const minus_exprt upper_bound(
8788
array_pool.get_or_create_length(res),
8889
array_pool.get_or_create_length(s1));
89-
return string_constraintt(idx2, zero_if_negative(upper_bound), res_eq);
90+
return string_constraintt(
91+
idx2, zero_if_negative(upper_bound), res_eq, message_handler);
9092
}());
9193

9294
return {from_integer(0, get_return_code_type()), std::move(constraints)};
@@ -208,7 +210,8 @@ std::vector<mp_integer> string_concatenation_builtin_functiont::eval(
208210
}
209211

210212
string_constraintst string_concatenation_builtin_functiont::constraints(
211-
string_constraint_generatort &generator) const
213+
string_constraint_generatort &generator,
214+
message_handlert &message_handler) const
212215

213216
{
214217
auto pair = [&]() -> std::pair<exprt, string_constraintst> {

‎src/solvers/strings/string_concatenation_builtin_function.h

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -39,8 +39,9 @@ class string_concatenation_builtin_functiont final
3939
return "concat";
4040
}
4141

42-
string_constraintst
43-
constraints(string_constraint_generatort &generator) const override;
42+
string_constraintst constraints(
43+
string_constraint_generatort &generator,
44+
message_handlert &message_handler) const override;
4445

4546
exprt length_constraint() const override;
4647
};

‎src/solvers/strings/string_constraint.cpp

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -17,15 +17,14 @@ Author: Diffblue Ltd.
1717
/// Runs a solver instance to verify whether an expression can only be
1818
/// non-negative.
1919
/// \param expr: the expression to check for negativity
20+
/// \param message_handler: message handler
2021
/// \return true if `expr < 0` is unsatisfiable, false otherwise
21-
static bool cannot_be_neg(const exprt &expr)
22+
static bool cannot_be_neg(const exprt &expr, message_handlert &message_handler)
2223
{
23-
// this is an internal check, no need for user visibility
24-
null_message_handlert null_message_handler;
25-
satcheck_no_simplifiert sat_check(null_message_handler);
24+
satcheck_no_simplifiert sat_check(message_handler);
2625
symbol_tablet symbol_table;
2726
namespacet ns(symbol_table);
28-
boolbvt solver{ns, sat_check, null_message_handler};
27+
boolbvt solver{ns, sat_check, message_handler};
2928
const exprt zero = from_integer(0, expr.type());
3029
const binary_relation_exprt non_neg(expr, ID_lt, zero);
3130
solver << non_neg;
@@ -36,18 +35,19 @@ string_constraintt::string_constraintt(
3635
const symbol_exprt &_univ_var,
3736
const exprt &lower_bound,
3837
const exprt &upper_bound,
39-
const exprt &body)
38+
const exprt &body,
39+
message_handlert &message_handler)
4040
: univ_var(_univ_var),
4141
lower_bound(lower_bound),
4242
upper_bound(upper_bound),
4343
body(body)
4444
{
4545
INVARIANT(
46-
cannot_be_neg(lower_bound),
46+
cannot_be_neg(lower_bound, message_handler),
4747
"String constraints must have non-negative lower bound.\n" +
4848
lower_bound.pretty());
4949
INVARIANT(
50-
cannot_be_neg(upper_bound),
50+
cannot_be_neg(upper_bound, message_handler),
5151
"String constraints must have non-negative upper bound.\n" +
5252
upper_bound.pretty());
5353
}

‎src/solvers/strings/string_constraint.h

Lines changed: 11 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,8 @@ Author: Romain Brenguier, [email protected]
2424
#include <util/string_expr.h>
2525
#include <util/union_find_replace.h>
2626

27+
class message_handlert;
28+
2729
/// ### Universally quantified string constraint
2830
///
2931
/// This represents a universally quantified string constraint as laid out in
@@ -60,21 +62,25 @@ class string_constraintt final
6062
exprt upper_bound;
6163
exprt body;
6264

63-
string_constraintt() = delete;
64-
6565
string_constraintt(
6666
const symbol_exprt &_univ_var,
6767
const exprt &lower_bound,
6868
const exprt &upper_bound,
69-
const exprt &body);
69+
const exprt &body,
70+
message_handlert &message_handler);
7071

7172
// Default bound inferior is 0
72-
string_constraintt(symbol_exprt univ_var, exprt upper_bound, exprt body)
73+
string_constraintt(
74+
symbol_exprt univ_var,
75+
exprt upper_bound,
76+
exprt body,
77+
message_handlert &message_handler)
7378
: string_constraintt(
7479
univ_var,
7580
from_integer(0, univ_var.type()),
7681
upper_bound,
77-
body)
82+
body,
83+
message_handler)
7884
{
7985
}
8086

0 commit comments

Comments
 (0)