Skip to content

Commit 462d355

Browse files
romainbrenguierromainbrenguier
committed
Add unit test for the string solver
This tests the solver directly on a set of desired formula instead of through symex as would a regression test. This can be easier to debug when trying to track a bug or add an new feature, as the correspondence with the string solver code would be easier to see.
1 parent 445a880 commit 462d355

File tree

3 files changed

+248
-0
lines changed

3 files changed

+248
-0
lines changed

Diff for: ‎unit/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,7 @@ SRC += analyses/ai/ai.cpp \
5757
solvers/strings/string_format_builtin_function/length_of_decimal_int.cpp \
5858
solvers/strings/string_refinement/concretize_array.cpp \
5959
solvers/strings/string_refinement/sparse_array.cpp \
60+
solvers/strings/string_refinement/string_refinement.cpp \
6061
solvers/strings/string_refinement/substitute_array_list.cpp \
6162
solvers/strings/string_refinement/union_find_replace.cpp \
6263
util/allocate_objects.cpp \

Diff for: ‎unit/solvers/strings/string_refinement/module_dependencies.txt

+1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
solvers/refinement
2+
solvers/sat
23
solvers/strings
34
string_refinement
45
testing-utils

Diff for: ‎unit/solvers/strings/string_refinement/string_refinement.cpp

+246
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,246 @@
1+
/*******************************************************************\
2+
3+
Module: Unit tests for sparse arrays in
4+
solvers/refinement/string_refinement.cpp
5+
6+
Author: Romain Brenguier, [email protected]
7+
8+
\*******************************************************************/
9+
10+
#include <testing-utils/use_catch.h>
11+
12+
#include <solvers/sat/satcheck.h>
13+
#include <solvers/strings/string_refinement.h>
14+
#include <util/arith_tools.h>
15+
#include <util/c_types.h>
16+
#include <util/config.h>
17+
#include <util/mathematical_types.h>
18+
#include <util/std_expr.h>
19+
#include <util/std_types.h>
20+
#include <util/symbol_table.h>
21+
22+
SCENARIO("string refinement", "[core][solvers][strings][string_refinement]")
23+
{
24+
config.set_arch("none");
25+
26+
string_refinementt::infot info;
27+
28+
null_message_handlert log{};
29+
info.message_handler = &log;
30+
31+
symbol_tablet symbol_table;
32+
namespacet ns{symbol_table};
33+
info.ns = &ns;
34+
35+
satcheck_minisat_simplifiert sat_solver{log};
36+
info.prop = &sat_solver;
37+
38+
string_refinementt solver{info};
39+
40+
GIVEN("An array of characters, with its associated pointer and length")
41+
{
42+
const signedbv_typet int_type{64};
43+
const unsignedbv_typet char_type{16};
44+
const array_typet char_array_type{char_type, infinity_exprt{int_type}};
45+
const refined_string_typet string_type{int_type, pointer_type(char_type)};
46+
const symbol_exprt array1{"array1", char_array_type};
47+
const symbol_exprt pointer1{"pointer1", pointer_type(char_type)};
48+
const symbol_exprt length1{"length1", int_type};
49+
const refined_string_exprt string_expr{length1, pointer1, string_type};
50+
51+
// associate_array_to_pointer : (char[], *char) -> int
52+
const symbol_exprt associate_array_to_pointer{
53+
ID_cprover_associate_array_to_pointer_func,
54+
mathematical_function_typet{{char_array_type, pointer_type(char_type)},
55+
int_type}};
56+
57+
// associate_length_to_array : (int, char[]) -> int
58+
const symbol_exprt associate_length_to_array{
59+
ID_cprover_associate_length_to_array_func,
60+
mathematical_function_typet{{int_type, char_array_type}, int_type}};
61+
62+
// length_function : (string) -> int
63+
const symbol_exprt length_function{
64+
ID_cprover_string_length_func,
65+
mathematical_function_typet{{string_type}, int_type}};
66+
67+
// char_at_function : (string, int) -> char
68+
const symbol_exprt char_at_function{
69+
ID_cprover_string_char_at_func,
70+
mathematical_function_typet{{string_type, int_type}, char_type}};
71+
72+
// return_code1 == associate_array_to_pointer(array1, pointer1)
73+
const symbol_exprt return_code1{"return_code1", int_type};
74+
solver.set_to(
75+
equal_exprt{
76+
return_code1,
77+
function_application_exprt{associate_array_to_pointer,
78+
std::vector<exprt>{array1, pointer1}}},
79+
true);
80+
81+
// return_code2 == associate_length_to_array(length1, array1)
82+
const symbol_exprt return_code2{"return_code2", int_type};
83+
solver.set_to(
84+
equal_exprt{
85+
return_code1,
86+
function_application_exprt{associate_length_to_array,
87+
std::vector<exprt>{array1, length1}}},
88+
true);
89+
90+
WHEN(
91+
"return_length == string_length({length1, pointer1}) "
92+
"and return_length == 15")
93+
{
94+
const symbol_exprt return_length{"return_length", int_type};
95+
solver.set_to(
96+
equal_exprt{return_length,
97+
function_application_exprt{
98+
length_function, std::vector<exprt>{string_expr}}},
99+
true);
100+
101+
solver.set_to(
102+
equal_exprt{return_length, from_integer(15, int_type)}, true);
103+
104+
auto result = solver.dec_solve();
105+
THEN("The formula is satisfiable")
106+
{
107+
REQUIRE(result == decision_proceduret::resultt::D_SATISFIABLE);
108+
}
109+
THEN("the model for the result and length1 are `15`")
110+
{
111+
const exprt return_length_model = solver.get(return_length);
112+
REQUIRE(return_length_model == from_integer(15, int_type));
113+
const exprt length1_model = solver.get(length1);
114+
REQUIRE(return_length_model == from_integer(15, int_type));
115+
}
116+
THEN("the model of array1 is an array of length 15")
117+
{
118+
const exprt array_model = solver.get(array1);
119+
REQUIRE(can_cast_expr<array_exprt>(array_model));
120+
REQUIRE(to_array_expr(array_model).operands().size() == 15);
121+
}
122+
}
123+
124+
WHEN("length1 == 10 and 'b' == string_char_at({length1, pointer1}, 9)")
125+
{
126+
solver.set_to(equal_exprt{length1, from_integer(10, int_type)}, true);
127+
128+
solver.set_to(
129+
equal_exprt{
130+
from_integer('b', char_type),
131+
function_application_exprt{
132+
char_at_function,
133+
std::vector<exprt>{string_expr, from_integer(9, int_type)}}},
134+
true);
135+
136+
THEN(
137+
"The formula is satisfiable and the model of the array should have"
138+
"length 10 and end with 'b'")
139+
{
140+
auto result = solver.dec_solve();
141+
REQUIRE(result == decision_proceduret::resultt::D_SATISFIABLE);
142+
const exprt array_model = solver.get(array1);
143+
REQUIRE(can_cast_expr<array_exprt>(array_model));
144+
const std::vector<exprt> &elements =
145+
to_array_expr(array_model).operands();
146+
REQUIRE(elements.size() == 10);
147+
REQUIRE(elements[9].is_constant());
148+
REQUIRE(numeric_cast_v<char>(to_constant_expr(elements[9])) == 'b');
149+
}
150+
}
151+
152+
WHEN(
153+
"g1 => length1 = 10 && 'b' == string_char_at({length1, pointer1}, 9)"
154+
" and g2 => 'c' == string_char_at({length1, pointer1}, 3)"
155+
" and g1 && g2")
156+
{
157+
const symbol_exprt g1{"g1", bool_typet{}};
158+
solver.set_to(
159+
implies_exprt{
160+
g1,
161+
and_exprt{equal_exprt{length1, from_integer(10, int_type)},
162+
equal_exprt{from_integer('b', char_type),
163+
function_application_exprt{
164+
char_at_function,
165+
std::vector<exprt>{
166+
string_expr, from_integer(9, int_type)}}}}},
167+
true);
168+
169+
const symbol_exprt g2{"g2", bool_typet{}};
170+
solver.set_to(
171+
implies_exprt{
172+
g2,
173+
and_exprt{equal_exprt{length1, from_integer(10, int_type)},
174+
equal_exprt{from_integer('c', char_type),
175+
function_application_exprt{
176+
char_at_function,
177+
std::vector<exprt>{
178+
string_expr, from_integer(3, int_type)}}}}},
179+
true);
180+
181+
solver.set_to(and_exprt{g1, g2}, true);
182+
183+
THEN(
184+
"The model for array1 has length 10 and contains 'c' at "
185+
" position 3 and b at position 9")
186+
{
187+
auto result = solver.dec_solve();
188+
REQUIRE(result == decision_proceduret::resultt::D_SATISFIABLE);
189+
const exprt array_model = solver.get(array1);
190+
REQUIRE(can_cast_expr<array_exprt>(array_model));
191+
const std::vector<exprt> &elements =
192+
to_array_expr(array_model).operands();
193+
REQUIRE(elements.size() == 10);
194+
REQUIRE(elements[3].is_constant());
195+
REQUIRE(numeric_cast_v<char>(to_constant_expr(elements[3])) == 'c');
196+
REQUIRE(elements[9].is_constant());
197+
REQUIRE(numeric_cast_v<char>(to_constant_expr(elements[9])) == 'b');
198+
}
199+
}
200+
201+
WHEN(
202+
"g1 => 'b' == string_char_at({length1, pointer1}, 9)"
203+
" and g2 => 'c' == string_char_at({length1, pointer1}, 9) "
204+
" and length1 == 10 && !g1 && g2")
205+
{
206+
const symbol_exprt g1{"g1", bool_typet{}};
207+
solver.set_to(
208+
implies_exprt{
209+
g1,
210+
equal_exprt{
211+
from_integer('b', char_type),
212+
function_application_exprt{
213+
char_at_function,
214+
std::vector<exprt>{string_expr, from_integer(9, int_type)}}}},
215+
true);
216+
217+
const symbol_exprt g2{"g2", bool_typet{}};
218+
solver.set_to(
219+
implies_exprt{
220+
g2,
221+
equal_exprt{
222+
from_integer('c', char_type),
223+
function_application_exprt{
224+
char_at_function,
225+
std::vector<exprt>{string_expr, from_integer(9, int_type)}}}},
226+
true);
227+
228+
solver.set_to(
229+
and_exprt{
230+
equal_exprt{length1, from_integer(10, int_type)}, not_exprt{g1}, g2},
231+
true);
232+
THEN("The model for array1 has length 10 and contains 'c' at position 9")
233+
{
234+
auto result = solver.dec_solve();
235+
REQUIRE(result == decision_proceduret::resultt::D_SATISFIABLE);
236+
const exprt array_model = solver.get(array1);
237+
REQUIRE(can_cast_expr<array_exprt>(array_model));
238+
const std::vector<exprt> &elements =
239+
to_array_expr(array_model).operands();
240+
REQUIRE(elements.size() == 10);
241+
REQUIRE(elements[9].is_constant());
242+
REQUIRE(numeric_cast_v<char>(to_constant_expr(elements[9])) == 'c');
243+
}
244+
}
245+
}
246+
}

0 commit comments

Comments
 (0)