Merge pull request #5149 from smowton/smowton/fix/string-buffer-set-length-negative-values

String solver setLength routine: tolerate negative lengths

Author: smowton

jbmc/regression/jbmc-strings/StringBufferSetLength/SetLengthTest.class

@@ -0,0 +1,30 @@
+public class SetLengthTest {
+
+    public static void main(int unknown) {
+
+        StringBuffer s = new StringBuffer("ABCD");
+        // Avoid producing a huge string that consumes too much memory, or which
+        // string refinement can't handle:
+        if(unknown >= 100)
+          return;
+
+        try {
+            s.setLength(unknown);
+            assert s.length() == unknown;
+
+            if(unknown > 4) {
+                assert s.toString().startsWith("ABCD");
+            }
+            else if(unknown == 4) {
+                assert s.toString().equals("ABCD");
+            }
+            else {
+                assert "ABCD".startsWith(s.toString());
+            }
+        }
+        catch (StringIndexOutOfBoundsException e) {
+            assert unknown < 0;
+        }
+    }
+
+}

jbmc/regression/jbmc-strings/StringBufferSetLength/SetLengthTest.java

@@ -0,0 +1,11 @@
+CORE
+SetLengthTest.class
+--function SetLengthTest.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^VERIFICATION SUCCESSFUL$
+^\[java::SetLengthTest\.main:\(I\)V\.assertion\.1\] line 13 assertion at file SetLengthTest\.java line 13 function java::SetLengthTest\.main:\(I\)V bytecode-index 21: SUCCESS$
+^\[java::SetLengthTest\.main:\(I\)V\.assertion\.2\] line 16 assertion at file SetLengthTest\.java line 16 function java::SetLengthTest\.main:\(I\)V bytecode-index 35: SUCCESS$
+^\[java::SetLengthTest\.main:\(I\)V\.assertion\.3\] line 19 assertion at file SetLengthTest\.java line 19 function java::SetLengthTest\.main:\(I\)V bytecode-index 49: SUCCESS$
+^\[java::SetLengthTest\.main:\(I\)V\.assertion\.4\] line 22 assertion at file SetLengthTest\.java line 22 function java::SetLengthTest\.main:\(I\)V bytecode-index 60: SUCCESS$
+^\[java::SetLengthTest\.main:\(I\)V\.assertion\.5\] line 26 assertion at file SetLengthTest\.java line 26 function java::SetLengthTest\.main:\(I\)V bytecode-index 70: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$

jbmc/regression/jbmc-strings/StringBufferSetLength/test.desc

@@ -18,10 +18,12 @@ Author: Romain Brenguier, [email protected]
 
 /// Reduce or extend a string to have the given length
 ///
-/// Add axioms ensuring the returned string expression `res` has length `k`
-/// and characters at position `i` in `res` are equal to the character at
-/// position `i` in `s1` if `i` is smaller that the length of `s1`, otherwise
-/// it is the null character `\u0000`.
+/// Add axioms ensuring the returned string expression `res` has length
+/// `max(k, 0)` and characters at position `i` in `res` are equal to the
+/// character at position `i` in `s1` if `i` is smaller that the length of `s1`,
+/// otherwise it is the null character `\u0000`.
+/// Note this means if `k` is negative then the string is truncated to length 0;
+/// in practice a wrapper function will usually handle this case.
 ///
 /// These axioms are:
 ///   1. \f$ |{\tt res}|={\tt k} \f$
@@ -47,12 +49,12 @@ string_constraint_generatort::add_axioms_for_set_length(
   const typet &char_type = s1.content().type().subtype();
 
   // We add axioms:
-  // a1 : |res|=k
+  // a1 : |res|=max(k, 0)
   // a2 : forall i< min(|s1|, k) .res[i] = s1[i]
   // a3 : forall |s1| <= i < |res|. res[i] = 0
 
   constraints.existential.push_back(
-    equal_to(array_pool.get_or_create_length(res), k));
+    equal_to(array_pool.get_or_create_length(res), zero_if_negative(k)));
 
   const symbol_exprt idx = fresh_symbol("QA_index_set_length", index_type);
   const string_constraintt a2(