From c427ac0d6c53c777a6e761b59cfc484c8af0701b Mon Sep 17 00:00:00 2001
From: Daniel Poetzl <daniel.poetzl@diffblue.com>
Date: Mon, 23 Sep 2019 11:17:55 +0100
Subject: [PATCH 1/2] Fix typo in string solver string preprocessing

The typo prevented CProverString.deleteCharAt(StringBuffer) from being replaced
by the corresponding string solver primitive.
---
 jbmc/src/java_bytecode/java_string_library_preprocess.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index 044f13401fc..55ed8dc642c 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -1507,7 +1507,7 @@ void java_string_library_preprocesst::initialize_conversion_table()
       ID_cprover_string_delete_func;
   cprover_equivalent_to_java_assign_and_return_function
     ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
-     "StringBufferI)Ljava/lang/StringBuffer;"] =
+     "StringBuffer;I)Ljava/lang/StringBuffer;"] =
       ID_cprover_string_delete_char_at_func;
   cprover_equivalent_to_java_assign_and_return_function
     ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"

From c785b9bd4c60406cd60b843f8331e7230b04a8dd Mon Sep 17 00:00:00 2001
From: Daniel Poetzl <daniel.poetzl@diffblue.com>
Date: Mon, 23 Sep 2019 12:14:44 +0100
Subject: [PATCH 2/2] Adapt existing CProverString.deleteCharAt() test and add
 new tests

Change existing test such that it cannot be solved by constant propagation, add
a test for which verification fails, and add variants that use StringBuffer
instead of StringBuilder.
---
 .../TestDeleteCharAt.class                    | Bin 0 -> 1698 bytes
 .../java_delete_char_at/TestDeleteCharAt.java |  42 ++++++++++++++++++
 .../java_delete_char_at/test.desc             |   8 ----
 .../test_delete_char_at.class                 | Bin 923 -> 0 bytes
 .../test_delete_char_at.java                  |  11 -----
 .../test_string_buffer_failure.desc           |   8 ++++
 .../test_string_buffer_success.desc           |   8 ++++
 .../test_string_builder_failure.desc          |   8 ++++
 .../test_string_builder_success.desc          |   8 ++++
 9 files changed, 74 insertions(+), 19 deletions(-)
 create mode 100644 jbmc/regression/strings-smoke-tests/java_delete_char_at/TestDeleteCharAt.class
 create mode 100644 jbmc/regression/strings-smoke-tests/java_delete_char_at/TestDeleteCharAt.java
 delete mode 100644 jbmc/regression/strings-smoke-tests/java_delete_char_at/test.desc
 delete mode 100644 jbmc/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.class
 delete mode 100644 jbmc/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.java
 create mode 100644 jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_buffer_failure.desc
 create mode 100644 jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_buffer_success.desc
 create mode 100644 jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_builder_failure.desc
 create mode 100644 jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_builder_success.desc

diff --git a/jbmc/regression/strings-smoke-tests/java_delete_char_at/TestDeleteCharAt.class b/jbmc/regression/strings-smoke-tests/java_delete_char_at/TestDeleteCharAt.class
new file mode 100644
index 0000000000000000000000000000000000000000..d4632a8dfbf1e37f93b43e82e418d31fc76d2f57
GIT binary patch
literal 1698
zcmb`G+fNfg6vn?TExRnMlu{6if(mNOtt#NHsFWh!>LtNQ;BC7daB*#McT3d&#J>6D
zvzmaBMBn|RjNkM^sWh6X*<@yR&UeoI&Y3gce|-50U<O$oeMo2+(=e`LLPrpjI;N16
ztMeU*;(~^YI;JtBVpd0|6kpPCS;G|-S9OG|`fGA^UPVgB9ImUlp`d5f^gQAEcCp|s
z+MbznL|%cirl5V!F4#ULZSllY1;I=)FBEiT?Sgn%dXW?E6Dd~E?+edg_FcQMu~4#|
zyl|IGmL)uoKJhi_dSux*t>+KSt%`?=o6Mn=-;!xNC6^(O9Spg?z8{gfv@q_wX>*oS
zW7e08CD#&5wj}I*Lc&Gi2w!BLnQq#j+BCOK0|SULJ2Pi-eD(SbL(Bc7V-_}&O$kZq
zyo$7e1!N2?;+BD9=vNRhEv92&3AdS0!#iEC=`GhSy41a5^njV;AkXP*DC_6QEM@pR
z3c|nQs<><59`4iBaD0^86qet#RgJ}b<JpF;x|x#qFi><ilGc`6+!k&!^SCnCeT@8p
z`Y4z^9HMr)sk@0o(d#A!nqRC(jK&WOQ*0~ovSd1JjwZ@#HmSs#g6URA%ks27xnf~o
zHZsmQY-tubFFe~7`Te_K7y2a{*w1S?#YfY}$EAe(<yCUk4ps;;j)VL=!CB!P8ry~P
zK?-raCX(w83WhjK={vOX83HS@x6mSi_XtJWvU>=wj_)G$U?TV#?JE;IP#=DTRz^Qn
z(aA{14)iiQ_t3ez3*%eORF<YA%_ezxpmO*SRIWoX$lA;GAT*pLN(wrj^3e~|8bz=p
zt>WYlBsr=$#W6<B>3_pL+RStix2xIoD{dEY!^G_-ZiKi!#ElZS_qVtsf5HvR>ULME
z8<ExR`A^jyAa0CsgZz#Y_XKf=h&$X8ceGaBGyjJB_thOC?kI835ce!`&k;9H+{ABi
uH7e_EK2vFOpgR)XL2nsq@I8WUpP)6aQN9b=^0K=^2pIG7VVvVn0P&y4tzoGE

literal 0
HcmV?d00001

diff --git a/jbmc/regression/strings-smoke-tests/java_delete_char_at/TestDeleteCharAt.java b/jbmc/regression/strings-smoke-tests/java_delete_char_at/TestDeleteCharAt.java
new file mode 100644
index 00000000000..28a084eb58c
--- /dev/null
+++ b/jbmc/regression/strings-smoke-tests/java_delete_char_at/TestDeleteCharAt.java
@@ -0,0 +1,42 @@
+public class TestDeleteCharAt
+{
+   public static void testStringBuilderSuccess(boolean b)
+   {
+      String s = b ? "abc" : "xyz";
+      StringBuilder sb = new StringBuilder(s);
+      org.cprover.CProverString.deleteCharAt(sb, 1);
+      String result = sb.toString();
+      assert !b || result.equals("ac");
+      assert b || result.equals("xz");
+   }
+
+   public static void testStringBuilderFailure(boolean b)
+   {
+      String s = b ? "abc" : "xyz";
+      StringBuilder sb = new StringBuilder(s);
+      org.cprover.CProverString.deleteCharAt(sb, 1);
+      String result = sb.toString();
+      assert !b || result.equals("ab");
+      assert b || result.equals("yz");
+   }
+
+   public static void testStringBufferSuccess(boolean b)
+   {
+      String s = b ? "abc" : "xyz";
+      StringBuffer sb = new StringBuffer(s);
+      org.cprover.CProverString.deleteCharAt(sb, 1);
+      String result = sb.toString();
+      assert !b || result.equals("ac");
+      assert b || result.equals("xz");
+   }
+
+   public static void testStringBufferFailure(boolean b)
+   {
+      String s = b ? "abc" : "xyz";
+      StringBuffer sb = new StringBuffer(s);
+      org.cprover.CProverString.deleteCharAt(sb, 1);
+      String result = sb.toString();
+      assert !b || result.equals("ab");
+      assert b || result.equals("yz");
+   }
+}
diff --git a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test.desc b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test.desc
deleted file mode 100644
index 11fd2e5474f..00000000000
--- a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-CORE
-test_delete_char_at.class
---max-nondet-string-length 1000 --function test_delete_char_at.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-non equal types
diff --git a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.class b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.class
deleted file mode 100644
index d9148dfc2112f54814f3231a370326c490b626f8..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 923
zcmaJ<+int36kTVy%rFc>fwr`Y*Q!8mkxIR_F(PVW#7ly)u`gs8PH^gU24{wT3_swr
znowgCefOU<?lW|X2II@w=j^@DT5Df^{QCM0Kpl5gq*0V{R)vJ3f^)*2S8)Ls#qCl8
zDXb{Ctl|o;$|$KwiuAII3RY!YW5})Op2uC^bZqaT>FHgI_ZZkNLwwt`P5&N4q*Q**
z5N$d=&X8`IHh(_c?{fE*NT$HPZrTi~wyzuSp6P?YO_F4+F(})Hbqu4nouO;+$ENsH
z@VV!AdfehZ?-*}&x1;;(d-{Q{A&VTtqPSNr-R@W0zH8e32Sd~9ahKFIx`u{zRApS(
zP{W3X8>nl@V2(j*7(}aK6E}%tiqQybeB`<gf#m){FXNVm+qlD!nSOlH-Q$M;musSj
z`lAm9+@@x&m0Hseljv4?#&ul47Q>R`_N&Igbq=^&ZN3a_2&zq5(xi?wh<0-pI>dSM
zKMKWnLd1M&HjzZc`TL=6c?|P^QcTL-D%1GW)0&zV?Fhp{k9(%edne7LiTgte(1PsJ
z%B5%*0hTF<S<o#4CWc98o?b<=jBKoO2=-AVVxG=;;ABW(;Uv|e)s-l=aRlkjAtFyJ
z+2|Otol5iz;yaZw<klxBBji`Ji80g>l1E5VqV`?jN&)UNArl!CvT4ZVQ?N`dHK<sm
xND}NPYBCBkmV!{IvmOWn=CY|VPK_W(KOh?U3}uQPY8E&#NZNf-+3A4#%x~73%$WcH

diff --git a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.java b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.java
deleted file mode 100644
index 3121aab316c..00000000000
--- a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.java
+++ /dev/null
@@ -1,11 +0,0 @@
-public class test_delete_char_at
-{
-   public static void main()
-   {
-      StringBuilder s = new StringBuilder();
-      s.append("Abc");
-      org.cprover.CProverString.deleteCharAt(s, 1);
-      String str = s.toString();
-      assert(str.equals("Ac"));
-   }
-}
diff --git a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_buffer_failure.desc b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_buffer_failure.desc
new file mode 100644
index 00000000000..fe62837c839
--- /dev/null
+++ b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_buffer_failure.desc
@@ -0,0 +1,8 @@
+CORE
+TestDeleteCharAt.class
+--max-nondet-string-length 1000 --function TestDeleteCharAt.testStringBufferFailure --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+non equal types
diff --git a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_buffer_success.desc b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_buffer_success.desc
new file mode 100644
index 00000000000..42af49d8fa8
--- /dev/null
+++ b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_buffer_success.desc
@@ -0,0 +1,8 @@
+CORE
+TestDeleteCharAt.class
+--max-nondet-string-length 1000 --function TestDeleteCharAt.testStringBufferSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+non equal types
diff --git a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_builder_failure.desc b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_builder_failure.desc
new file mode 100644
index 00000000000..a7f3ccbfc5a
--- /dev/null
+++ b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_builder_failure.desc
@@ -0,0 +1,8 @@
+CORE
+TestDeleteCharAt.class
+--max-nondet-string-length 1000 --function TestDeleteCharAt.testStringBuilderFailure --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+non equal types
diff --git a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_builder_success.desc b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_builder_success.desc
new file mode 100644
index 00000000000..84e3d5ff739
--- /dev/null
+++ b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_builder_success.desc
@@ -0,0 +1,8 @@
+CORE
+TestDeleteCharAt.class
+--max-nondet-string-length 1000 --function TestDeleteCharAt.testStringBuilderSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+non equal types