Merge pull request #1939 from romainbrenguier/bugfix/builtin-string-insert-eval

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

Author: romainbrenguier

regression/jbmc-strings/StringBuilderInsert/Test.class

@@ -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");
+        }
+
+    }
+}

regression/jbmc-strings/StringBuilderInsert/Test.java

@@ -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
+--

regression/jbmc-strings/StringBuilderInsert/test.desc

@@ -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");
+    }
+}

regression/jbmc-strings/StringConcat_StringII/Test.class

@@ -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

regression/jbmc-strings/StringConcat_StringII/Test.java

@@ -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

regression/jbmc-strings/StringConcat_StringII/test.desc

@@ -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");
+    }
+}

regression/jbmc-strings/StringConcat_StringII/test_fail.desc

@@ -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

regression/jbmc-strings/StringSubstring/Test.class

@@ -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

regression/jbmc-strings/StringSubstring/Test.java

@@ -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

regression/jbmc-strings/StringSubstring/test.desc

@@ -14,22 +14,16 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #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
@@ -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

regression/jbmc-strings/StringSubstring/test_fail.desc

@@ -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);
+}

src/solvers/refinement/string_constraint_generator.h

@@ -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
@@ -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));
 }