From 40a22bce1cf2fd8eee685c123ed76c0d773874a8 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Tue, 20 Aug 2019 13:27:57 +0100
Subject: [PATCH 1/3] Add length assumption at assign_string_constant beginning

This is to make sure that the length of the array before the assignment
isn't unconstrained. Otherwise it could be set to be arbitrarily large
by the solver which will causes invalid traces.
---
 src/goto-symex/goto_symex.cpp | 5 +++++
 src/goto-symex/goto_symex.h   | 3 +++
 2 files changed, 8 insertions(+)

diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp
index 515e89f0656..f140877a0e4 100644
--- a/src/goto-symex/goto_symex.cpp
+++ b/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, {});
 
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 364a83b4376..920b3b1e699 100644
--- a/src/goto-symex/goto_symex.h
+++ b/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

From 7a3202b20c9a7a6f10d4d8211c6313964764265d Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Tue, 20 Aug 2019 13:40:37 +0100
Subject: [PATCH 2/3] Improve the StringBuilder constructor tests

Split the tests for the different constructors, add assertions that
are supposed to fail, and activate the tests that can be.
---
 .../StringBuilderConstructors01.class         | Bin 797 -> 1221 bytes
 .../StringBuilderConstructors01.java          |  40 +++++++++++++-----
 .../test-capacity-fail.desc                   |  11 +++++
 .../test-capacity-pass.desc                   |  11 +++++
 .../test-no-arg-fail.desc                     |   8 ++++
 .../{test.desc => test-no-arg-pass.desc}      |   4 +-
 .../test-string-fail.desc                     |   8 ++++
 .../test-string-pass.desc                     |   8 ++++
 8 files changed, 78 insertions(+), 12 deletions(-)
 create mode 100644 jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-capacity-fail.desc
 create mode 100644 jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-capacity-pass.desc
 create mode 100644 jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-no-arg-fail.desc
 rename jbmc/regression/jbmc-strings/StringBuilderConstructors01/{test.desc => test-no-arg-pass.desc} (54%)
 create mode 100644 jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-string-fail.desc
 create mode 100644 jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-string-pass.desc

diff --git a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/StringBuilderConstructors01.class b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/StringBuilderConstructors01.class
index c7052b38c1f2d4b0cf579a5014877469af80212a..5d0f85de997fd83db5696cf75ba5b7fbeca6371b 100644
GIT binary patch
literal 1221
zcma)*OK;Oa6ot>^Wyf)vM_*}6UL`GQfTl&=Q6Wm8Qbj10f{^IWaopfy?8*-$ehS&Z
zjx``P5|v=jZ$gMWPU0w3LD_ib&fNL#nKReF{(S!dU=Q~sBvBMlk`O{Mjs(hlwl3hN
zgcyoEsEF9$<EDUH5~|n|P-B>{D2}7qu5OvmW8G2OhSp(Vrwp-u-PGL&4B_h5ONL0p
z>Szq9rfzD--rKfjzu?IXanm}myC;NUNVZ%>ee+DY@b^g1X!}sn4F*|NE)-RF-w(2b
zaIh;muC1Fx(l8k8i2JHB6eG1P&sMcVotG}P{1cBn-RNj`gRbD(p6Xh*v$MN>uDnxZ
zq>*7*=JUFtnBDrs2^n)p$+(R>47qX6!N`#(wr$y*ahE~t=x1kb!_#=Y&9F8>nyf9L
zE@KC~4CyiTdHY;bUGmk?%&z;|_w|T;tsZfE7pu*2>HvM8ucyYV4a4_%siQf%t#tyG
z<hkpS`SebwDAU^~sV7)E$1g`S5hMc{`erH0)5vIy*7{&ycp~QM8}k?GwXhJRHmO;7
zYT*i@SAB$^enq5*Z0!=!4@g`gMvKBv&ItL8IfQ8*rGhakBVdstD*hXJ0ZT+)o`u|-
zPEHU_CUWu`ITw(RNdwnh;+oS^AL4APGmyxhBHbfUO}`UYy)qm7Ke}_oULp4CHTG)2
zJ{js>=eo1;KBR%}1@3lQ{5ai}0?~`~?4>ciJW#$iEB(`SdWGm4MBn^}F5*T&-}4;@
jGTFo><Q{~`XGFr^5E-||sJ*zkQH11&yb1FZgi!bk6@b^y

delta 457
zcmZutO-lk%6g_WdoEgWl22=Z(wCqF2)KqBKCP4y2+ZaLUW-K*p8X~M+^c!SW1w!->
zYLSpot2X_MHvJ6g4ldjX@7;4h&b#N``|a(Eg`d&KCx9JnEAT^?u&jWC?wW{<sEaFJ
z_^|4FF$rr5ye@5B!3H)Z#CwHeUbr$lHbdB`l`qUYGi#Z4J6rAEbnNzS@|eM2?V6{T
z74!PYY*<aw=>63r8WIfhS*O)%Shr0T8VnUPm{pO)mUF;#o<VmQ(`5-M6=`IgXBJ8e
zM#*g%GNwz3R?}{G&lz|lS#o|^k?~HP%RPj^5THR{z(XLc55b)bz?WUrlmUc_>jgXm
zh=*^Go)AdALw<yB2rm(puW>RxEt#QYf5LpF{v77WMj?^)K+ZuVd77NImxqFVT4@a`
q!c^A4kC2xzKR&@AWGp!MLM$OoI*Igu&~+bpz^QwTf<+2AEd2w>VNcQk

diff --git a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/StringBuilderConstructors01.java b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/StringBuilderConstructors01.java
index efb5524c2b8..ab8a67e316b 100644
--- a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/StringBuilderConstructors01.java
+++ b/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;
+  }
 }
diff --git a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-capacity-fail.desc b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-capacity-fail.desc
new file mode 100644
index 00000000000..b3ee4c9bb1f
--- /dev/null
+++ b/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.
diff --git a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-capacity-pass.desc b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-capacity-pass.desc
new file mode 100644
index 00000000000..3b5b65a053a
--- /dev/null
+++ b/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.
diff --git a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-no-arg-fail.desc b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-no-arg-fail.desc
new file mode 100644
index 00000000000..c4eded5e470
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-no-arg-fail.desc
@@ -0,0 +1,8 @@
+CORE
+StringBuilderConstructors01.class
+--function StringBuilderConstructors01.noArgFail --max-nondet-string-length 1000
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test.desc b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-no-arg-pass.desc
similarity index 54%
rename from jbmc/regression/jbmc-strings/StringBuilderConstructors01/test.desc
rename to jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-no-arg-pass.desc
index cfbea436519..6c2f63a597f 100644
--- a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test.desc
+++ b/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$
diff --git a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-string-fail.desc b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-string-fail.desc
new file mode 100644
index 00000000000..ceb4abbcbf8
--- /dev/null
+++ b/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
diff --git a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-string-pass.desc b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-string-pass.desc
new file mode 100644
index 00000000000..554c8004014
--- /dev/null
+++ b/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

From 334714a4c1437053c0b0e84cca7c231956645a71 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Tue, 20 Aug 2019 13:48:19 +0100
Subject: [PATCH 3/3] Add trace check in StringBuilder test for empty array

This tests would fail before the fix to the symex constant propagation
of strings.
---
 .../StringBuilderConstructors01/test-no-arg-fail.desc       | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-no-arg-fail.desc b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-no-arg-fail.desc
index c4eded5e470..f1846c50a63 100644
--- a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-no-arg-fail.desc
+++ b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-no-arg-fail.desc
@@ -1,8 +1,12 @@
 CORE
 StringBuilderConstructors01.class
---function StringBuilderConstructors01.noArgFail --max-nondet-string-length 1000
+--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.