Skip to content

Commit 114030b

Browse files
kroeningkroening
authored
Merge pull request diffblue#2664 from romainbrenguier/feature/extend-builtin-functions-part2
Extend builtin functions for string_set_char
2 parents 1bca129 + 31366ad commit 114030b

File tree

11 files changed

+247
-78
lines changed

11 files changed

+247
-78
lines changed

‎jbmc/regression/jbmc-strings/StringBuilderSetCharAt/Test.class‎

1.49 KB
Binary file not shown.

‎jbmc/regression/jbmc-strings/StringBuilderSetCharAt/Test.java‎

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
public class Test {
2+
public String det()
3+
{
4+
StringBuilder builder = new StringBuilder("abcdefghijklmnopqrstuvwxyz");
5+
builder.setCharAt(3, '!');
6+
builder.setCharAt(5, '!');
7+
builder.setCharAt(7, '!');
8+
builder.setCharAt(9, '!');
9+
builder.setCharAt(13, '!');
10+
builder.setCharAt(15, '!');
11+
builder.setCharAt(17, '!');
12+
builder.setCharAt(19, '!');
13+
builder.setCharAt(4, ':');
14+
builder.setCharAt(5, ':');
15+
builder.setCharAt(6, ':');
16+
builder.setCharAt(9, ':');
17+
builder.setCharAt(10, ':');
18+
builder.setCharAt(11, ':');
19+
builder.setCharAt(16, ':');
20+
builder.setCharAt(18, ':');
21+
return builder.toString();
22+
}
23+
24+
public String nonDet(String s, char c, int i)
25+
{
26+
StringBuilder builder = new StringBuilder(s);
27+
if(i + 5 >= s.length() || 19 >= s.length() || i < 0)
28+
return "Out of bounds";
29+
builder.setCharAt(i, c);
30+
builder.setCharAt(i+5, 'x');
31+
builder.setCharAt(7, '!');
32+
builder.setCharAt(9, '!');
33+
builder.setCharAt(13, '!');
34+
builder.setCharAt(15, '!');
35+
builder.setCharAt(17, '!');
36+
builder.setCharAt(19, '!');
37+
builder.setCharAt(4, ':');
38+
builder.setCharAt(5, ':');
39+
builder.setCharAt(6, c);
40+
builder.setCharAt(9, ':');
41+
builder.setCharAt(10, ':');
42+
builder.setCharAt(11, ':');
43+
builder.setCharAt(16, ':');
44+
builder.setCharAt(18, ':');
45+
return builder.toString();
46+
}
47+
48+
public String withDependency(boolean b)
49+
{
50+
StringBuilder builder = new StringBuilder("abcdefghijklmnopqrstuvwxyz");
51+
builder.setCharAt(3, '!');
52+
builder.setCharAt(5, '!');
53+
54+
if(b) {
55+
assert builder.toString().startsWith("abc!");
56+
} else {
57+
assert !builder.toString().startsWith("abc!");
58+
}
59+
return builder.toString();
60+
}
61+
62+
}

‎jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_dependency.desc‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
Test.class
3+
--function Test.withDependency --max-nondet-string-length 1000
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
assertion at file Test.java line 55 .*: SUCCESS
7+
assertion at file Test.java line 57 .*: FAILURE
8+
--
9+
--
10+
Check that when a dependency is present, the correct constraints are added
11+
12+

‎jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_det.desc‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
Test.class
3+
--function Test.det --verbosity 10 --cover location
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
coverage.* file Test.java line 21 .*: SATISFIED
7+
--
8+
adding lemma .*nondet_infinite_array
9+
--
10+
Check that using the string dependence informations, no lemma involving arrays is added

‎jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_nondet.desc‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
Test.class
3+
--function Test.nonDet --verbosity 10 --cover location --max-nondet-string-length 1000
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
coverage.* file Test.java line 45 .*: SATISFIED
7+
--
8+
adding lemma .*nondet_infinite_array
9+
--
10+
Check that using the string dependence informations, no lemma involving arrays is added

‎src/solvers/refinement/string_builtin_function.cpp‎

Lines changed: 49 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -29,33 +29,6 @@ string_transformation_builtin_functiont::
2929
const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
3030
input = array_pool.find(arg1.op1(), arg1.op0());
3131
result = array_pool.find(fun_args[1], fun_args[0]);
32-
args.insert(args.end(), fun_args.begin() + 3, fun_args.end());
33-
}
34-
35-
optionalt<exprt> string_transformation_builtin_functiont::eval(
36-
const std::function<exprt(const exprt &)> &get_value) const
37-
{
38-
const auto &input_value = eval_string(input, get_value);
39-
if(!input_value.has_value())
40-
return {};
41-
42-
std::vector<mp_integer> arg_values;
43-
const auto &insert = std::back_inserter(arg_values);
44-
const mp_integer unknown('?');
45-
std::transform(
46-
args.begin(), args.end(), insert, [&](const exprt &e) { // NOLINT
47-
if(const auto val = numeric_cast<mp_integer>(get_value(e)))
48-
return *val;
49-
INVARIANT(
50-
get_value(e).id() == ID_unknown,
51-
"array valuation should only contain constants and unknown");
52-
return unknown;
53-
});
54-
55-
const auto result_value = eval(*input_value, arg_values);
56-
const auto length = from_integer(result_value.size(), result.length().type());
57-
const array_typet type(result.type().subtype(), length);
58-
return make_string(result_value, type);
5932
}
6033

6134
string_insertion_builtin_functiont::string_insertion_builtin_functiont(
@@ -162,14 +135,56 @@ std::vector<mp_integer> string_concatenation_builtin_functiont::eval(
162135
return result;
163136
}
164137

165-
std::vector<mp_integer> string_concat_char_builtin_functiont::eval(
166-
const std::vector<mp_integer> &input_value,
167-
const std::vector<mp_integer> &args_value) const
138+
optionalt<exprt> string_concat_char_builtin_functiont::eval(
139+
const std::function<exprt(const exprt &)> &get_value) const
168140
{
169-
PRECONDITION(args_value.size() == 1);
170-
std::vector<mp_integer> result(input_value);
171-
result.push_back(args_value[0]);
172-
return result;
141+
auto input_opt = eval_string(input, get_value);
142+
if(!input_opt.has_value())
143+
return {};
144+
const mp_integer char_val = [&] {
145+
if(const auto val = numeric_cast<mp_integer>(get_value(character)))
146+
return *val;
147+
INVARIANT(
148+
get_value(character).id() == ID_unknown,
149+
"character valuation should only contain constants and unknown");
150+
return mp_integer(CHARACTER_FOR_UNKNOWN);
151+
}();
152+
input_opt.value().push_back(char_val);
153+
const auto length =
154+
from_integer(input_opt.value().size(), result.length().type());
155+
const array_typet type(result.type().subtype(), length);
156+
return make_string(input_opt.value(), type);
157+
}
158+
159+
optionalt<exprt> string_set_char_builtin_functiont::eval(
160+
const std::function<exprt(const exprt &)> &get_value) const
161+
{
162+
auto input_opt = eval_string(input, get_value);
163+
const auto char_opt = numeric_cast<mp_integer>(get_value(character));
164+
const auto position_opt = numeric_cast<mp_integer>(get_value(position));
165+
if(!input_opt || !char_opt || !position_opt)
166+
return {};
167+
if(0 <= *position_opt && *position_opt < input_opt.value().size())
168+
input_opt.value()[numeric_cast_v<std::size_t>(*position_opt)] = *char_opt;
169+
const auto length =
170+
from_integer(input_opt.value().size(), result.length().type());
171+
const array_typet type(result.type().subtype(), length);
172+
return make_string(input_opt.value(), type);
173+
}
174+
175+
exprt string_set_char_builtin_functiont::length_constraint() const
176+
{
177+
const exprt out_of_bounds = or_exprt(
178+
binary_relation_exprt(position, ID_ge, input.length()),
179+
binary_relation_exprt(
180+
position, ID_le, from_integer(0, input.length().type())));
181+
const exprt return_value = if_exprt(
182+
out_of_bounds,
183+
from_integer(1, return_code.type()),
184+
from_integer(0, return_code.type()));
185+
return and_exprt(
186+
equal_exprt(result.length(), input.length()),
187+
equal_exprt(return_code, return_value));
173188
}
174189

175190
std::vector<mp_integer> string_insertion_builtin_functiont::eval(

‎src/solvers/refinement/string_builtin_function.h‎

Lines changed: 51 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,8 @@
1111

1212
class array_poolt;
1313

14+
#define CHARACTER_FOR_UNKNOWN '?'
15+
1416
/// Base class for string functions that are built in the solver
1517
class string_builtin_functiont
1618
{
@@ -68,7 +70,6 @@ class string_transformation_builtin_functiont : public string_builtin_functiont
6870
public:
6971
array_string_exprt result;
7072
array_string_exprt input;
71-
std::vector<exprt> args;
7273

7374
/// Constructor from arguments of a function application.
7475
/// The arguments in `fun_args` should be in order:
@@ -88,15 +89,6 @@ class string_transformation_builtin_functiont : public string_builtin_functiont
8889
{
8990
return {input};
9091
}
91-
92-
/// Evaluate the result from a concrete valuation of the arguments
93-
virtual std::vector<mp_integer> eval(
94-
const std::vector<mp_integer> &input_value,
95-
const std::vector<mp_integer> &args_value) const = 0;
96-
97-
optionalt<exprt>
98-
eval(const std::function<exprt(const exprt &)> &get_value) const override;
99-
10092
bool maybe_testing_function() const override
10193
{
10294
return false;
@@ -108,6 +100,8 @@ class string_concat_char_builtin_functiont
108100
: public string_transformation_builtin_functiont
109101
{
110102
public:
103+
exprt character;
104+
111105
/// Constructor from arguments of a function application.
112106
/// The arguments in `fun_args` should be in order:
113107
/// an integer `result.length`, a character pointer `&result[0]`,
@@ -118,11 +112,12 @@ class string_concat_char_builtin_functiont
118112
array_poolt &array_pool)
119113
: string_transformation_builtin_functiont(return_code, fun_args, array_pool)
120114
{
115+
PRECONDITION(fun_args.size() == 4);
116+
character = fun_args[3];
121117
}
122118

123-
std::vector<mp_integer> eval(
124-
const std::vector<mp_integer> &input_value,
125-
const std::vector<mp_integer> &args_value) const override;
119+
optionalt<exprt>
120+
eval(const std::function<exprt(const exprt &)> &get_value) const override;
126121

127122
std::string name() const override
128123
{
@@ -131,7 +126,7 @@ class string_concat_char_builtin_functiont
131126

132127
exprt add_constraints(string_constraint_generatort &generator) const override
133128
{
134-
return generator.add_axioms_for_concat_char(result, input, args[0]);
129+
return generator.add_axioms_for_concat_char(result, input, character);
135130
}
136131

137132
exprt length_constraint() const override
@@ -140,6 +135,48 @@ class string_concat_char_builtin_functiont
140135
}
141136
};
142137

138+
/// Setting a character at a particular position of a string
139+
class string_set_char_builtin_functiont
140+
: public string_transformation_builtin_functiont
141+
{
142+
public:
143+
exprt position;
144+
exprt character;
145+
146+
/// Constructor from arguments of a function application.
147+
/// The arguments in `fun_args` should be in order:
148+
/// an integer `result.length`, a character pointer `&result[0]`,
149+
/// a string `arg1` of type refined_string_typet, a position and a character.
150+
string_set_char_builtin_functiont(
151+
const exprt &return_code,
152+
const std::vector<exprt> &fun_args,
153+
array_poolt &array_pool)
154+
: string_transformation_builtin_functiont(return_code, fun_args, array_pool)
155+
{
156+
PRECONDITION(fun_args.size() == 5);
157+
position = fun_args[3];
158+
character = fun_args[4];
159+
}
160+
161+
optionalt<exprt>
162+
eval(const std::function<exprt(const exprt &)> &get_value) const override;
163+
164+
std::string name() const override
165+
{
166+
return "set_char";
167+
}
168+
169+
exprt add_constraints(string_constraint_generatort &generator) const override
170+
{
171+
return generator.add_axioms_for_set_char(
172+
result, input, position, character);
173+
}
174+
175+
// \todo: length_constraint is not the best possible name because we also
176+
// \todo: add constraint about the return code
177+
exprt length_constraint() const override;
178+
};
179+
143180
/// String inserting a string into another one
144181
class string_insertion_builtin_functiont : public string_builtin_functiont
145182
{

‎src/solvers/refinement/string_constraint_generator.h‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -170,6 +170,11 @@ class string_constraint_generatort final
170170
const exprt &input_int,
171171
const exprt &radix,
172172
size_t max_size = 0);
173+
exprt add_axioms_for_set_char(
174+
const array_string_exprt &res,
175+
const array_string_exprt &str,
176+
const exprt &position,
177+
const exprt &character);
173178

174179
private:
175180
symbol_exprt fresh_boolean(const irep_idt &prefix);

0 commit comments

Comments
 (0)