Skip to content

Commit 39f4157

Browse files
romainbrenguiertautschnig
authored andcommitted
Added option to the string solver for string length and printability
Added field in string_refinement and string_constraint_generator to bound size of strings in the program and enforce a range on the characters.
1 parent b194918 commit 39f4157

File tree

5 files changed

+153
-130
lines changed

5 files changed

+153
-130
lines changed

src/solvers/refinement/string_constraint_generator.h

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,9 +33,17 @@ class string_constraint_generatort
3333
// to the axiom list.
3434

3535
string_constraint_generatort():
36-
mode(ID_unknown)
36+
mode(ID_unknown),
37+
max_string_length(-1),
38+
force_printable_characters(false)
3739
{ }
3840

41+
// Constraints on the maximal length of strings
42+
int max_string_length;
43+
44+
// Should we add constraints on the characters
45+
bool force_printable_characters;
46+
3947
void set_mode(irep_idt _mode)
4048
{
4149
// only C and java modes supported
@@ -81,6 +89,8 @@ class string_constraint_generatort
8189
// Maps unresolved symbols to the string_exprt that was created for them
8290
std::map<irep_idt, string_exprt> unresolved_symbols;
8391

92+
// Set of strings that have been created by the generator
93+
std::set<string_exprt> created_strings;
8494

8595
string_exprt find_or_add_string_of_symbol(
8696
const symbol_exprt &sym,
@@ -107,6 +117,7 @@ class string_constraint_generatort
107117

108118
static irep_idt extract_java_string(const symbol_exprt &s);
109119

120+
void add_default_axioms(const string_exprt &s);
110121
exprt axiom_for_is_positive_index(const exprt &x);
111122

112123
// The following functions add axioms for the returned value

src/solvers/refinement/string_constraint_generator_concat.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,8 @@ string_exprt string_constraint_generatort::add_axioms_for_concat(
3030
// a4 : forall i<|s1|. res[i]=s1[i]
3131
// a5 : forall i<|s2|. res[i+|s1|]=s2[i]
3232

33-
res.length()=plus_exprt_with_overflow_check(s1.length(), s2.length());
33+
equal_exprt a1(res.length(), plus_exprt_with_overflow_check(s1.length(), s2.length()));
34+
axioms.push_back(a1);
3435
axioms.push_back(s1.axiom_for_is_shorter_than(res));
3536
axioms.push_back(s2.axiom_for_is_shorter_than(res));
3637

src/solvers/refinement/string_constraint_generator_main.cpp

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -117,10 +117,11 @@ plus_exprt string_constraint_generatort::plus_exprt_with_overflow_check(
117117
string_exprt string_constraint_generatort::fresh_string(
118118
const refined_string_typet &type)
119119
{
120-
symbol_exprt length=
121-
fresh_symbol("string_length", type.get_index_type());
120+
symbol_exprt length=fresh_symbol("string_length", type.get_index_type());
122121
symbol_exprt content=fresh_symbol("string_content", type.get_content_type());
123-
return string_exprt(length, content, type);
122+
string_exprt str(length, content, type);
123+
created_strings.insert(str);
124+
return str;
124125
}
125126

126127
/// casts an expression to a string expression, or fetches the actual
@@ -215,15 +216,13 @@ string_exprt string_constraint_generatort::add_axioms_for_refined_string(
215216
{
216217
const symbol_exprt &sym=to_symbol_expr(string);
217218
string_exprt s=find_or_add_string_of_symbol(sym, type);
218-
axioms.push_back(
219-
s.axiom_for_is_longer_than(from_integer(0, s.length().type())));
219+
add_default_axioms(s);
220220
return s;
221221
}
222222
else if(string.id()==ID_nondet_symbol)
223223
{
224224
string_exprt s=fresh_string(type);
225-
axioms.push_back(
226-
s.axiom_for_is_longer_than(from_integer(0, s.length().type())));
225+
add_default_axioms(s);
227226
return s;
228227
}
229228
else if(string.id()==ID_if)
@@ -233,8 +232,7 @@ string_exprt string_constraint_generatort::add_axioms_for_refined_string(
233232
else if(string.id()==ID_struct)
234233
{
235234
const string_exprt &s=to_string_expr(string);
236-
axioms.push_back(
237-
s.axiom_for_is_longer_than(from_integer(0, s.length().type())));
235+
add_default_axioms(s);
238236
return s;
239237
}
240238
else

0 commit comments

Comments
 (0)