Fix array length in symex constant string propagation [TG-9048]

jbmc/regression/jbmc-strings/StringBuilderConstructors01/StringBuilderConstructors01.java

@@ -1,13 +1,33 @@
 public class StringBuilderConstructors01
 {
-   public static void main(String[] args)
-   {
-      StringBuilder buffer1 = new StringBuilder();
-      StringBuilder buffer2 = new StringBuilder(10);
-      StringBuilder buffer3 = new StringBuilder("diffblue");
-
-      assert buffer1.length()==0;
-      assert buffer2.length()==0;
-      assert buffer3.length()>0;
-   }
+  public static void noArgPass() {
+    StringBuilder buffer1 = new StringBuilder();
+    assert buffer1.length() == 0;
+  }
+
+  public static void noArgFail() {
+    StringBuilder buffer1 = new StringBuilder();
+    assert buffer1.length() != 0;
+  }
+
+  public static void capacityPass() {
+    StringBuilder buffer2 = new StringBuilder(10);
+    assert buffer2.length() == 0;
+  }
+
+  public static void capacityFail() {
+
+    StringBuilder buffer2 = new StringBuilder(10);
+    assert buffer2.length() != 0;
+  }
+
+  public static void stringPass() {
+    StringBuilder buffer3 = new StringBuilder("diffblue");
+    assert buffer3.length() == 8;
+  }
+
+  public static void stringFail() {
+    StringBuilder buffer3 = new StringBuilder("diffblue");
+    assert buffer3.length() != 8;
+  }
 }

jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-capacity-fail.desc

@@ -0,0 +1,11 @@
+KNOWNBUG
+StringBuilderConstructors01.class
+--function StringBuilderConstructors01.capacityFail --max-nondet-string-length 1000
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+This is not working currently because the StringBuilder constructor with
+capacity argument is not modelled.

jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-capacity-pass.desc

@@ -0,0 +1,11 @@
+KNOWNBUG
+StringBuilderConstructors01.class
+--function StringBuilderConstructors01.capacityPass --max-nondet-string-length 1000
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+This is not working currently because the StringBuilder constructor with
+capacity argument is not modelled.

jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-no-arg-fail.desc

@@ -0,0 +1,12 @@
+CORE
+StringBuilderConstructors01.class
+--function StringBuilderConstructors01.noArgFail --max-nondet-string-length 1000 --trace
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+dynamic_object2=\{\s*\}
+--
+^warning: ignoring
+--
+The check for dynamic_object2 is to make sure the array is created empty and
+is not given arbitrary content before its final assignment.

jbmc/regression/jbmc-strings/StringBuilderConstructors01/test.desc → jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-no-arg-pass.desc

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 StringBuilderConstructors01.class
---max-nondet-string-length 1000
+--function StringBuilderConstructors01.noArgPass --max-nondet-string-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-string-fail.desc

@@ -0,0 +1,8 @@
+CORE
+StringBuilderConstructors01.class
+--function StringBuilderConstructors01.stringFail --max-nondet-string-length 1000
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-string-pass.desc

@@ -0,0 +1,8 @@
+CORE
+StringBuilderConstructors01.class
+--function StringBuilderConstructors01.stringPass --max-nondet-string-length 1000
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/goto-symex/goto_symex.cpp

@@ -199,6 +199,11 @@ void goto_symext::assign_string_constant(
   const ssa_exprt &char_array,
   const array_exprt &new_char_array)
 {
+  // We need to make sure that the length of the previous array isn't
+  // unconstrained, otherwise it could be arbitrarily large which causes
+  // invalid traces
+  symex_assume(state, equal_exprt{length, from_integer(0, length.type())});
+
   // assign length of string
   symex_assign.assign_symbol(length, expr_skeletont{}, new_length, {});
 

src/goto-symex/goto_symex.h

@@ -590,6 +590,9 @@ class goto_symext
   /// "abc", the symbol will be named "abc_constant_char_array"). Then, the
   /// expression `&sym[0]` is assigned to `char_array` (assuming `sym` denotes
   /// the symbol holding the string data given by `new_char_array`.
+  /// The assignment is preceeded by an assume statement ensuring `length`
+  /// before this call was zero, this is to avoid leaving the previous array
+  /// unconstrained.
   ///
   /// \param state: goto symex state
   /// \param symex_assign: object handling symbol assignments