Skip to content

Fix StringBuilder.insert and String.substring [TG-2459] #1939

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Binary file not shown.
48 changes: 48 additions & 0 deletions regression/jbmc-strings/StringBuilderInsert/Test.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@

public class Test {
public void check (int i) {
if(i == 0)
{
// Arrange
StringBuilder s = new StringBuilder("bar");

// Act
s = org.cprover.CProverString.insert(s, 0, "foo");

// Should succeed
assert s.toString().equals("foobar");

// Should fail
assert !s.toString().equals("foobar");
}
if(i == 1)
{
// Arrange
StringBuilder s = new StringBuilder("bar");

// Act
s = org.cprover.CProverString.insert(s, -10, "foo");

// Should succeed
assert s.toString().equals("foobar");

// Should fail
assert !s.toString().equals("foobar");
}
if(i == 2)
{
// Arrange
StringBuilder s = new StringBuilder("bar");

// Act
s = org.cprover.CProverString.insert(s, 10, "foo");

// Should succeed
assert s.toString().equals("barfoo");

// Should fail
assert !s.toString().equals("barfoo");
}

}
}
12 changes: 12 additions & 0 deletions regression/jbmc-strings/StringBuilderInsert/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
CORE
Test.class
--refine-strings --function Test.check
^EXIT=10$
^SIGNAL=0$
assertion at file Test.java line 13 .*: SUCCESS
assertion at file Test.java line 16 .*: FAILURE
assertion at file Test.java line 27 .*: SUCCESS
assertion at file Test.java line 30 .*: FAILURE
assertion at file Test.java line 41 .*: SUCCESS
assertion at file Test.java line 44 .*: FAILURE
--
Binary file not shown.
40 changes: 40 additions & 0 deletions regression/jbmc-strings/StringConcat_StringII/Test.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
// This test uses CProverString so should be compiled with
// javac Test.java ../cprover/CProverString.java
import org.cprover.CProverString;

class Test {
public void testSuccess(String s, String t, int start, int end) {
// Filter
if (s == null || t == null)
return;

// Act
StringBuilder sb = new StringBuilder(s);
String result = CProverString.append(sb, t, start, end).toString();

// Arrange
StringBuilder reference = new StringBuilder(s);
if(start < 0)
start = 0;
for (int i = start; i < end && i < t.length(); i++)
reference.append(org.cprover.CProverString.charAt(t, i));

// Assert
assert result.equals(reference.toString());
}

public void testFail(int i) {
// Arrange
StringBuilder sb = new StringBuilder("foo");

// Act
CProverString.append(sb, "bar", 0, 1);
CProverString.append(sb, "bar", 0, 4);
CProverString.append(sb, "foo", -1, 0);
CProverString.append(sb, "foo", -10, -1);
CProverString.append(sb, "bar", -10, 25);

// Assert
assert !sb.toString().equals("foobbarbar");
}
}
8 changes: 8 additions & 0 deletions regression/jbmc-strings/StringConcat_StringII/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
Test.class
--refine-strings --string-max-length 100 --string-max-input-length 4 --verbosity 10 --unwind 5 Test.class --function Test.testSuccess
^EXIT=0$
^SIGNAL=0$
assertion at file Test.java line 23 .*: SUCCESS
--
^warning: ignoring
8 changes: 8 additions & 0 deletions regression/jbmc-strings/StringConcat_StringII/test_fail.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
Test.class
--refine-strings --string-max-length 10000 --verbosity 10 Test.class --function Test.testFail
^EXIT=10$
^SIGNAL=0$
assertion at file Test.java line 38 .*: FAILURE
--
^warning: ignoring
Binary file not shown.
47 changes: 47 additions & 0 deletions regression/jbmc-strings/StringSubstring/Test.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,47 @@
// This test uses CProverString so should be compiled with
// javac Test.java ../cprover/CProverString.java

class Test {
public void testSuccess(String s, int start, int end) {
// Filter
if (s == null)
return;

// Act
String sub = org.cprover.CProverString.substring(s, start, end);

// Arrange
StringBuilder reference = new StringBuilder();
if(start < 0)
start = 0;
for (int i = start; i < end && i < s.length(); i++)
reference.append(org.cprover.CProverString.charAt(s, i));

// Assert
assert sub.equals(reference.toString());
}

public void testFail(int i) {
// Arrange
String[] s = new String[5];

// Act
s[0] = org.cprover.CProverString.substring("foo", 0, 1);
s[1] = org.cprover.CProverString.substring("foo", 0, 4);
s[2] = org.cprover.CProverString.substring("foo", -1, 0);
s[3] = org.cprover.CProverString.substring("foo", -10, -1);
s[4] = org.cprover.CProverString.substring("foo", -10, 25);

// Assert
if(i == 0)
assert !s[0].equals("f");
if(i == 1)
assert !s[1].equals("foo");
if(i == 2)
assert !s[2].equals("");
if(i == 3)
assert !s[3].equals("");
if(i == 4)
assert !s[4].equals("foo");
}
}
6 changes: 6 additions & 0 deletions regression/jbmc-strings/StringSubstring/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
CORE
Test.class
--refine-strings --unwind 10 --string-max-input-length 6 --function Test.testSuccess
^EXIT=0$
^SIGNAL=0$
assertion at file Test.java line 21.*: SUCCESS
10 changes: 10 additions & 0 deletions regression/jbmc-strings/StringSubstring/test_fail.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
Test.class
--refine-strings --unwind 10 --string-max-input-length 6 --function Test.testFail
^EXIT=10$
^SIGNAL=0$
assertion at file Test.java line 37 .*: FAILURE
assertion at file Test.java line 39 .*: FAILURE
assertion at file Test.java line 41 .*: FAILURE
assertion at file Test.java line 43 .*: FAILURE
assertion at file Test.java line 45 .*: FAILURE
3 changes: 3 additions & 0 deletions src/solvers/refinement/string_constraint_generator.h
Original file line number Diff line number Diff line change
Expand Up @@ -439,4 +439,7 @@ utf16_constant_array_to_java(const array_exprt &arr, std::size_t length);
/// \return expression representing the minimum of two expressions
exprt minimum(const exprt &a, const exprt &b);

/// \return expression representing the maximum of two expressions
exprt maximum(const exprt &a, const exprt &b);

#endif
69 changes: 34 additions & 35 deletions src/solvers/refinement/string_constraint_generator_concat.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -14,22 +14,16 @@ Author: Romain Brenguier, [email protected]
#include <solvers/refinement/string_constraint_generator.h>

/// Add axioms enforcing that `res` is the concatenation of `s1` with
/// the substring of `s2` starting at index `start_index` and ending
/// at index `end_index`.
///
/// If `start_index >= end_index`, the value returned is `s1`.
/// If `end_index > |s2|` and/or `start_index < 0`, the appended string will
/// be of length `end_index - start_index` and padded with non-deterministic
/// values.
/// the substring of `s2` starting at index `start_index'` and ending
/// at index `end_index'`.
/// Where start_index' is max(0, start_index) and end_index' is
/// max(min(end_index, s2.length), start_index')
///
/// These axioms are:
/// 1. \f$end\_index > start\_index \Rightarrow |res| = |s_1| + end\_index -
/// start\_index
/// \f$
/// 2. \f$end\_index \le start\_index \Rightarrow res = s_1 \f$
/// 3. \f$\forall i<|s_1|. res[i]=s_1[i] \f$
/// 4. \f$\forall i< end\_index - start\_index.\ res[i+|s_1|]
/// = s_2[start\_index+i]\f$
/// 1. \f$|res| = |s_1| + end\_index' - start\_index' \f$
/// 2. \f$\forall i<|s_1|. res[i]=s_1[i] \f$
/// 3. \f$\forall i< end\_index' - start\_index'.\ res[i+|s_1|]
/// = s_2[start\_index'+i]\f$
///
/// \param res: an array of characters expression
/// \param s1: an array of characters expression
Expand All @@ -44,28 +38,33 @@ exprt string_constraint_generatort::add_axioms_for_concat_substr(
const exprt &start_index,
const exprt &end_index)
{
binary_relation_exprt prem(end_index, ID_gt, start_index);

exprt res_length=plus_exprt_with_overflow_check(
s1.length(), minus_exprt(end_index, start_index));
implies_exprt a1(prem, equal_exprt(res.length(), res_length));
lemmas.push_back(a1);

implies_exprt a2(not_exprt(prem), equal_exprt(res.length(), s1.length()));
lemmas.push_back(a2);
const typet &index_type = start_index.type();
const exprt start1 = maximum(start_index, from_integer(0, index_type));
const exprt end1 = maximum(minimum(end_index, s2.length()), start1);

// Axiom 1.
lemmas.push_back([&] { // NOLINT
const plus_exprt res_length(s1.length(), minus_exprt(end1, start1));
return equal_exprt(res.length(), res_length);
}());

// Axiom 2.
constraints.push_back([&] { // NOLINT
const symbol_exprt idx =
fresh_univ_index("QA_index_concat", res.length().type());
return string_constraintt(idx, s1.length(), equal_exprt(s1[idx], res[idx]));
}());

// Axiom 3.
constraints.push_back([&] { // NOLINT
const symbol_exprt idx2 =
fresh_univ_index("QA_index_concat2", res.length().type());
const equal_exprt res_eq(
res[plus_exprt(idx2, s1.length())], s2[plus_exprt(start1, idx2)]);
return string_constraintt(idx2, minus_exprt(end1, start1), res_eq);
}());

symbol_exprt idx=fresh_univ_index("QA_index_concat", res.length().type());
string_constraintt a3(idx, s1.length(), equal_exprt(s1[idx], res[idx]));
constraints.push_back(a3);

symbol_exprt idx2=fresh_univ_index("QA_index_concat2", res.length().type());
equal_exprt res_eq(
res[plus_exprt(idx2, s1.length())], s2[plus_exprt(start_index, idx2)]);
string_constraintt a4(idx2, minus_exprt(end_index, start_index), res_eq);
constraints.push_back(a4);

// We should have a enum type for the possible error codes
return from_integer(0, res.length().type());
return from_integer(0, get_return_code_type());
}

/// Add axioms enforcing that `res` is the concatenation of `s1` with
Expand Down
5 changes: 5 additions & 0 deletions src/solvers/refinement/string_constraint_generator_main.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -667,3 +667,8 @@ exprt minimum(const exprt &a, const exprt &b)
{
return if_exprt(binary_relation_exprt(a, ID_le, b), a, b);
}

exprt maximum(const exprt &a, const exprt &b)
{
return if_exprt(binary_relation_exprt(a, ID_le, b), b, a);
}
Original file line number Diff line number Diff line change
Expand Up @@ -98,16 +98,14 @@ exprt string_constraint_generatort::add_axioms_for_substring(
}

/// Add axioms ensuring that `res` corresponds to the substring of `str`
/// between indexes `start` and `end`.
/// between indexes `start' = max(start, 0)` and
/// `end' = max(min(end, |str|), start')`.
///
/// These axioms are:
/// 1. \f$ {\tt start} < {\tt end} \Rightarrow
/// |{\tt res}| = {\tt end} - {\tt start} \f$
/// 2. \f$ {\tt start} \ge {\tt end} \Rightarrow |{\tt res}| = 0 \f$
/// 3. \f$ |{\tt str}| > {\tt end} \f$
/// 4. \f$ \forall i<|{\tt str}|.\ {\tt res}[i]={\tt str}[{\tt start}+i] \f$
/// \todo Should return code different from 0 if `|str| <= |end|` instead of
/// adding constraint 3.
/// 1. \f$ |{\tt res}| = end' - start' \f$
/// 2. \f$ \forall i<|{\tt res}|.\ {\tt res}[i]={\tt str}[{\tt start'}+i] \f$
/// \todo Should return code different from 0 if `start' != start` or
/// `end' != end`
/// \param res: array of characters expression
/// \param str: array of characters expression
/// \param start: integer expression
Expand All @@ -123,26 +121,19 @@ exprt string_constraint_generatort::add_axioms_for_substring(
PRECONDITION(start.type()==index_type);
PRECONDITION(end.type()==index_type);

// We add axioms:
const exprt start1 = maximum(start, from_integer(0, start.type()));
const exprt end1 = maximum(minimum(end, str.length()), start1);

implies_exprt a1(
binary_relation_exprt(start, ID_lt, end),
res.axiom_for_has_length(minus_exprt(end, start)));
lemmas.push_back(a1);
// Axiom 1.
lemmas.push_back(equal_exprt(res.length(), minus_exprt(end1, start1)));

exprt is_empty=res.axiom_for_has_length(from_integer(0, index_type));
implies_exprt a2(binary_relation_exprt(start, ID_ge, end), is_empty);
lemmas.push_back(a2);
// Axiom 2.
constraints.push_back([&] { // NOLINT
const symbol_exprt idx = fresh_univ_index("QA_index_substring", index_type);
return string_constraintt(
idx, res.length(), equal_exprt(res[idx], str[plus_exprt(start1, idx)]));
}());

// Warning: check what to do if the string is not long enough
lemmas.push_back(str.axiom_for_length_ge(end));

symbol_exprt idx=fresh_univ_index("QA_index_substring", index_type);
string_constraintt a4(idx,
res.length(),
equal_exprt(res[idx],
str[plus_exprt(start, idx)]));
constraints.push_back(a4);
return from_integer(0, signedbv_typet(32));
}

Expand Down
Loading