Skip to content

Commit 3957f80

Browse files
author
svorenova
authored
Merge pull request #3753 from diffblue/move-string-solver
Move string solver into separate directory
2 parents 6ba3763 + 93a0994 commit 3957f80

File tree

54 files changed

+1329
-1313
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

54 files changed

+1329
-1313
lines changed

‎jbmc/src/jbmc/jbmc_parse_options.h

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,9 @@ Author: Daniel Kroening, [email protected]
2828
#include <goto-programs/lazy_goto_model.h>
2929
#include <goto-programs/show_properties.h>
3030

31-
#include <solvers/refinement/string_refinement.h>
31+
#include <goto-symex/path_storage.h>
32+
33+
#include <solvers/strings/string_refinement.h>
3234

3335
#include <java_bytecode/java_bytecode_language.h>
3436

‎jbmc/src/jbmc/module_dependencies.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,4 +11,5 @@ langapi # should go away
1111
linking
1212
pointer-analysis
1313
solvers/refinement
14+
solvers/strings
1415
util

‎jbmc/unit/Makefile

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -54,9 +54,9 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \
5454
java_bytecode/java_virtual_functions/virtual_functions.cpp \
5555
java_bytecode/load_method_by_regex.cpp \
5656
pointer-analysis/custom_value_set_analysis.cpp \
57-
solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp \
58-
solvers/refinement/string_refinement/dependency_graph.cpp \
59-
solvers/refinement/string_refinement/string_symbol_resolution.cpp \
57+
solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp \
58+
solvers/strings/string_refinement/dependency_graph.cpp \
59+
solvers/strings/string_refinement/string_symbol_resolution.cpp \
6060
util/expr_iterator.cpp \
6161
util/has_subtype.cpp \
6262
util/parameter_indices.cpp \

‎jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp renamed to ‎jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp

Lines changed: 35 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -8,28 +8,36 @@ Author: Jesse Sigal, [email protected]
88

99
#include <testing-utils/catch.hpp>
1010

11-
#include <numeric>
1211
#include <java_bytecode/java_bytecode_language.h>
1312
#include <java_bytecode/java_types.h>
13+
#include <numeric>
1414

15-
#include <langapi/mode.h>
1615
#include <langapi/language_util.h>
16+
#include <langapi/mode.h>
1717

18-
#include <solvers/refinement/string_constraint_instantiation.h>
1918
#include <solvers/sat/satcheck.h>
19+
#include <solvers/strings/string_constraint_instantiation.h>
2020

21-
#include <util/simplify_expr.h>
2221
#include <util/config.h>
22+
#include <util/simplify_expr.h>
2323

2424
/// \class Types used throughout the test. Currently it is impossible to
2525
/// statically initialize this value, there is a PR to allow this
2626
/// diffblue/cbmc/pull/1213
2727
class tt
2828
{
2929
public:
30-
tt() {}
31-
typet char_type() const {return java_char_type();}
32-
typet length_type() const {return java_int_type();}
30+
tt()
31+
{
32+
}
33+
typet char_type() const
34+
{
35+
return java_char_type();
36+
}
37+
typet length_type() const
38+
{
39+
return java_int_type();
40+
}
3341
array_typet array_type() const
3442
{
3543
return array_typet(char_type(), infinity_exprt(length_type()));
@@ -60,7 +68,7 @@ constant_exprt from_integer(const mp_integer &i)
6068
/// \return corresponding `string_exprt`
6169
array_string_exprt make_string_exprt(const std::string &str)
6270
{
63-
const constant_exprt length=from_integer(str.length(), t.length_type());
71+
const constant_exprt length = from_integer(str.length(), t.length_type());
6472
array_exprt content({}, array_typet(t.char_type(), length));
6573

6674
for(const char c : str)
@@ -92,7 +100,7 @@ std::set<exprt> full_index_set(const array_string_exprt &s)
92100
{
93101
const mp_integer n = numeric_cast_v<mp_integer>(s.length());
94102
std::set<exprt> ret;
95-
for(mp_integer i=0; i<n; ++i)
103+
for(mp_integer i = 0; i < n; ++i)
96104
ret.insert(from_integer(i));
97105
return ret;
98106
}
@@ -115,7 +123,7 @@ std::set<std::pair<X, Y>> product(const std::set<X> xs, const std::set<Y> ys)
115123
exprt combine_lemmas(const std::vector<exprt> &lemmas, const namespacet &ns)
116124
{
117125
// Conjunction of new lemmas
118-
exprt conj=conjunction(lemmas);
126+
exprt conj = conjunction(lemmas);
119127
// Simplify
120128
simplify(conj, ns);
121129

@@ -137,7 +145,7 @@ std::string create_info(std::vector<exprt> &lemmas, const namespacet &ns)
137145
get_language_from_mode(ID_java)->from_expr(lemma, lemma_string, ns);
138146
new_lemmas += lemma_string + "\n\n";
139147
}
140-
return "Instantiated lemmas:\n"+new_lemmas;
148+
return "Instantiated lemmas:\n" + new_lemmas;
141149
}
142150

143151
/// Checks the satisfiability of the given expression.
@@ -148,16 +156,17 @@ decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns)
148156
{
149157
satcheck_no_simplifiert sat_check;
150158
bv_refinementt::infot info;
151-
info.ns=&ns;
152-
info.prop=&sat_check;
159+
info.ns = &ns;
160+
info.prop = &sat_check;
153161
info.output_xml = false;
154162
bv_refinementt solver(info);
155163
solver << expr;
156164
return solver();
157165
}
158166

159167
// The [!mayfail] tag allows tests to fail while reporting the failure
160-
SCENARIO("instantiate_not_contains",
168+
SCENARIO(
169+
"instantiate_not_contains",
161170
"[!mayfail][core][solvers][refinement][string_constraint_instantiation]")
162171
{
163172
// For printing expression
@@ -261,10 +270,10 @@ SCENARIO("instantiate_not_contains",
261270
decision_proceduret::resultt result = check_sat(conj, empty_ns);
262271

263272
// Require SAT
264-
if(result==decision_proceduret::resultt::D_ERROR)
273+
if(result == decision_proceduret::resultt::D_ERROR)
265274
INFO("Got an error");
266275

267-
REQUIRE(result==decision_proceduret::resultt::D_SATISFIABLE);
276+
REQUIRE(result == decision_proceduret::resultt::D_SATISFIABLE);
268277
}
269278
}
270279
}
@@ -311,10 +320,10 @@ SCENARIO("instantiate_not_contains",
311320
decision_proceduret::resultt result = check_sat(conj, empty_ns);
312321

313322
// Require SAT
314-
if(result==decision_proceduret::resultt::D_ERROR)
323+
if(result == decision_proceduret::resultt::D_ERROR)
315324
INFO("Got an error");
316325

317-
REQUIRE(result==decision_proceduret::resultt::D_SATISFIABLE);
326+
REQUIRE(result == decision_proceduret::resultt::D_SATISFIABLE);
318327
}
319328
}
320329
}
@@ -362,10 +371,10 @@ SCENARIO("instantiate_not_contains",
362371
decision_proceduret::resultt result = check_sat(conj, empty_ns);
363372

364373
// Require UNSAT
365-
if(result==decision_proceduret::resultt::D_ERROR)
374+
if(result == decision_proceduret::resultt::D_ERROR)
366375
INFO("Got an error");
367376

368-
REQUIRE(result==decision_proceduret::resultt::D_UNSATISFIABLE);
377+
REQUIRE(result == decision_proceduret::resultt::D_UNSATISFIABLE);
369378
}
370379
}
371380
}
@@ -414,10 +423,10 @@ SCENARIO("instantiate_not_contains",
414423
decision_proceduret::resultt result = check_sat(conj, empty_ns);
415424

416425
// Require UNSAT
417-
if(result==decision_proceduret::resultt::D_ERROR)
426+
if(result == decision_proceduret::resultt::D_ERROR)
418427
INFO("Got an error");
419428

420-
REQUIRE(result==decision_proceduret::resultt::D_UNSATISFIABLE);
429+
REQUIRE(result == decision_proceduret::resultt::D_UNSATISFIABLE);
421430
}
422431
}
423432
}
@@ -465,10 +474,10 @@ SCENARIO("instantiate_not_contains",
465474
decision_proceduret::resultt result = check_sat(conj, empty_ns);
466475

467476
// Require UNSAT
468-
if(result==decision_proceduret::resultt::D_ERROR)
477+
if(result == decision_proceduret::resultt::D_ERROR)
469478
INFO("Got an error");
470479

471-
REQUIRE(result==decision_proceduret::resultt::D_UNSATISFIABLE);
480+
REQUIRE(result == decision_proceduret::resultt::D_UNSATISFIABLE);
472481
}
473482
}
474483
}
@@ -517,10 +526,10 @@ SCENARIO("instantiate_not_contains",
517526
decision_proceduret::resultt result = check_sat(conj, empty_ns);
518527

519528
// Require UNSAT
520-
if(result==decision_proceduret::resultt::D_ERROR)
529+
if(result == decision_proceduret::resultt::D_ERROR)
521530
INFO("Got an error");
522531

523-
REQUIRE(result==decision_proceduret::resultt::D_SATISFIABLE);
532+
REQUIRE(result == decision_proceduret::resultt::D_SATISFIABLE);
524533
}
525534
}
526535
}

‎jbmc/unit/solvers/refinement/string_constraint_instantiation/module_dependencies.txt renamed to ‎jbmc/unit/solvers/strings/string_constraint_instantiation/module_dependencies.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ java_bytecode
22
langapi # should go away
33
solvers/refinement
44
solvers/sat
5+
solvers/strings
56
string_constraint_instantiation
67
testing-utils
78
util

‎jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp renamed to ‎jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,11 +9,11 @@ Author: Diffblue Ltd.
99

1010
#include <testing-utils/catch.hpp>
1111

12+
#include <java_bytecode/java_types.h>
13+
#include <solvers/strings/string_refinement_util.h>
1214
#include <util/arith_tools.h>
13-
#include <util/std_types.h>
1415
#include <util/std_expr.h>
15-
#include <java_bytecode/java_types.h>
16-
#include <solvers/refinement/string_refinement_util.h>
16+
#include <util/std_types.h>
1717

1818
#ifdef DEBUG
1919
#include <iostream>

‎jbmc/unit/solvers/refinement/string_refinement/module_dependencies.txt renamed to ‎jbmc/unit/solvers/strings/string_refinement/module_dependencies.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,6 @@ java_bytecode
22
langapi # should go away
33
string_refinement
44
solvers/refinement
5+
solvers/strings
56
testing-utils
67
util

‎jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp renamed to ‎jbmc/unit/solvers/strings/string_refinement/string_symbol_resolution.cpp

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -9,17 +9,19 @@ Author: Diffblue Ltd.
99

1010
#include <testing-utils/catch.hpp>
1111

12+
#include <solvers/strings/string_refinement.h>
13+
14+
#include <iostream>
15+
#include <java_bytecode/java_bytecode_language.h>
16+
#include <langapi/mode.h>
1217
#include <util/arith_tools.h>
1318
#include <util/c_types.h>
1419
#include <util/std_expr.h>
15-
#include <solvers/refinement/string_refinement.h>
1620
#include <util/symbol_table.h>
17-
#include <langapi/mode.h>
18-
#include <java_bytecode/java_bytecode_language.h>
19-
#include <iostream>
2021

21-
SCENARIO("string_identifiers_resolution_from_equations",
22-
"[core][solvers][refinement][string_refinement]")
22+
SCENARIO(
23+
"string_identifiers_resolution_from_equations",
24+
"[core][solvers][refinement][string_refinement]")
2325
{
2426
// For printing expression
2527
register_language(new_java_bytecode_language);
@@ -50,8 +52,7 @@ SCENARIO("string_identifiers_resolution_from_equations",
5052
WHEN("There is no function call")
5153
{
5254
union_find_replacet symbol_resolve =
53-
string_identifiers_resolution_from_equations(
54-
equations, ns, stream);
55+
string_identifiers_resolution_from_equations(equations, ns, stream);
5556

5657
THEN("The symbol resolution structure is empty")
5758
{
@@ -69,8 +70,7 @@ SCENARIO("string_identifiers_resolution_from_equations",
6970
symbol_exprt bool_sym("bool_b", bool_typet());
7071
equations.emplace_back(bool_sym, fun);
7172
union_find_replacet symbol_resolve =
72-
string_identifiers_resolution_from_equations(
73-
equations, ns, stream);
73+
string_identifiers_resolution_from_equations(equations, ns, stream);
7474

7575
THEN("Equations that depend on it should be added")
7676
{

‎src/cbmc/cbmc_parse_options.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ Author: Daniel Kroening, [email protected]
2929

3030
#include <goto-programs/goto_trace.h>
3131

32-
#include <solvers/refinement/string_refinement.h>
32+
#include <solvers/strings/string_refinement.h>
3333

3434
#include "bmc.h"
3535
#include "xml_interface.h"

‎src/goto-checker/solver_factory.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,9 +28,9 @@ Author: Daniel Kroening, Peter Schrammel
2828
#include <solvers/prop/prop.h>
2929
#include <solvers/prop/prop_conv.h>
3030
#include <solvers/refinement/bv_refinement.h>
31-
#include <solvers/refinement/string_refinement.h>
3231
#include <solvers/sat/dimacs_cnf.h>
3332
#include <solvers/sat/satcheck.h>
33+
#include <solvers/strings/string_refinement.h>
3434

3535
solver_factoryt::solver_factoryt(
3636
const optionst &_options,

‎src/solvers/Makefile

Lines changed: 17 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -161,23 +161,23 @@ SRC = $(BOOLEFORCE_SRC) \
161161
refinement/bv_refinement_loop.cpp \
162162
refinement/refine_arithmetic.cpp \
163163
refinement/refine_arrays.cpp \
164-
refinement/string_builtin_function.cpp \
165-
refinement/string_refinement.cpp \
166-
refinement/string_refinement_util.cpp \
167-
refinement/string_constraint.cpp \
168-
refinement/string_constraint_generator_code_points.cpp \
169-
refinement/string_constraint_generator_comparison.cpp \
170-
refinement/string_constraint_generator_concat.cpp \
171-
refinement/string_constraint_generator_constants.cpp \
172-
refinement/string_constraint_generator_indexof.cpp \
173-
refinement/string_constraint_generator_insert.cpp \
174-
refinement/string_constraint_generator_float.cpp \
175-
refinement/string_constraint_generator_format.cpp \
176-
refinement/string_constraint_generator_main.cpp \
177-
refinement/string_constraint_generator_testing.cpp \
178-
refinement/string_constraint_generator_transformation.cpp \
179-
refinement/string_constraint_generator_valueof.cpp \
180-
refinement/string_constraint_instantiation.cpp \
164+
strings/string_builtin_function.cpp \
165+
strings/string_refinement.cpp \
166+
strings/string_refinement_util.cpp \
167+
strings/string_constraint.cpp \
168+
strings/string_constraint_generator_code_points.cpp \
169+
strings/string_constraint_generator_comparison.cpp \
170+
strings/string_constraint_generator_concat.cpp \
171+
strings/string_constraint_generator_constants.cpp \
172+
strings/string_constraint_generator_indexof.cpp \
173+
strings/string_constraint_generator_insert.cpp \
174+
strings/string_constraint_generator_float.cpp \
175+
strings/string_constraint_generator_format.cpp \
176+
strings/string_constraint_generator_main.cpp \
177+
strings/string_constraint_generator_testing.cpp \
178+
strings/string_constraint_generator_transformation.cpp \
179+
strings/string_constraint_generator_valueof.cpp \
180+
strings/string_constraint_instantiation.cpp \
181181
sat/cnf.cpp \
182182
sat/cnf_clause_list.cpp \
183183
sat/dimacs_cnf.cpp \

‎src/solvers/refinement/refine_arithmetic.cpp

Lines changed: 3 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected]
1313
#include <util/expr_util.h>
1414
#include <util/arith_tools.h>
1515

16-
#include <solvers/refinement/string_refinement_invariant.h>
1716
#include <solvers/floatbv/float_utils.h>
1817

1918
// Parameters
@@ -167,10 +166,7 @@ void bv_refinementt::check_SAT(approximationt &a)
167166

168167
if(type.id()==ID_floatbv)
169168
{
170-
// these are all ternary
171-
INVARIANT(
172-
a.expr.operands().size()==3,
173-
string_refinement_invariantt("all floatbv typed exprs are ternary"));
169+
const auto &float_op = to_ieee_float_op_expr(a.expr);
174170

175171
if(a.over_state==MAX_STATE)
176172
return;
@@ -182,7 +178,7 @@ void bv_refinementt::check_SAT(approximationt &a)
182178
o1.unpack(a.op1_value);
183179

184180
// get actual rounding mode
185-
exprt rounding_mode_expr = get(a.expr.op2());
181+
exprt rounding_mode_expr = get(float_op.rounding_mode());
186182
const std::size_t rounding_mode_int =
187183
numeric_cast_v<std::size_t>(rounding_mode_expr);
188184
ieee_floatt::rounding_modet rounding_mode =
@@ -279,8 +275,7 @@ void bv_refinementt::check_SAT(approximationt &a)
279275
{
280276
// these are all binary
281277
INVARIANT(
282-
a.expr.operands().size()==2,
283-
string_refinement_invariantt("all (un)signedbv typed exprs are binary"));
278+
a.expr.operands().size() == 2, "all (un)signedbv typed exprs are binary");
284279

285280
// already full interpretation?
286281
if(a.over_state>0)

0 commit comments

Comments
 (0)