Implement constant propagation of string concatenation

This implements constant propagation of ID_cprover_string_concat_func and
ID_cprover_string_empty_string_func which are the primitives used by
StringBuilder.append(), which in turn is used to implement String concatenation
using +.

Author: danpoe

jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation1/Main.class

@@ -0,0 +1,9 @@
+public class Main {
+  public void test() {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.append("xyz");
+    String s = sb.toString();
+    assert s.length() == 6;
+    assert s.startsWith("abcxyz");
+  }
+}

jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation1/Main.java

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.test --property "java::Main.test:()V.assertion.1" --property "java::Main.test:()V.assertion.2"
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

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

@@ -0,0 +1,25 @@
+public class Main {
+  public void test1() {
+    StringBuilder sb1 = new StringBuilder("abc");
+    String s2 = "";
+    sb1.append(s2);
+    assert sb1.length() == 3;
+    assert sb1.toString().startsWith("abc");
+  }
+
+  public void test2() {
+    StringBuilder sb1 = new StringBuilder();
+    String s2 = "abc";
+    sb1.append(s2);
+    assert sb1.length() == 3;
+    assert sb1.toString().startsWith("abc");
+  }
+
+  public void test3() {
+    StringBuilder sb1 = new StringBuilder();
+    String s2 = "";
+    sb1.append(s2);
+    assert sb1.length() == 0;
+    assert sb1.toString().startsWith("");
+  }
+}

jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/Main.class

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.test1 --property "java::Main.test1:()V.assertion.1" --property "java::Main.test1:()V.assertion.2"
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/Main.java

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.test2 --property "java::Main.test2:()V.assertion.1" --property "java::Main.test2:()V.assertion.2"
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/test1.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.test3 --property "java::Main.test3:()V.assertion.1" --property "java::Main.test3:()V.assertion.2"
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/test2.desc

@@ -0,0 +1,8 @@
+public class Main {
+  public void test() {
+    StringBuilder sb = new StringBuilder();
+    String s = sb.toString();
+    assert s.isEmpty();
+    assert s.length() == 0;
+  }
+}

jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/test3.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.test
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

jbmc/regression/jbmc-strings/StringBuilderDefaultConstructorConstantEvaluation/Main.class

@@ -0,0 +1,9 @@
+public class Main {
+  public void test() {
+    String s1 = "abc";
+    String s2 = "xyz";
+    String s3 = s1 + s2;
+    assert s3.length() == 6;
+    assert s3.startsWith("abcxyz");
+  }
+}

jbmc/regression/jbmc-strings/StringBuilderDefaultConstructorConstantEvaluation/Main.java

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.test --property "java::Main.test:()V.assertion.1" --property "java::Main.test:()V.assertion.2"
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

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

@@ -0,0 +1,25 @@
+public class Main {
+  public void test1() {
+    String s1 = "abc";
+    String s2 = "";
+    String s3 = s1 + s2;
+    assert s3.length() == 3;
+    assert s3.startsWith("abc");
+  }
+
+  public void test2() {
+    String s1 = "";
+    String s2 = "abc";
+    String s3 = s1 + s2;
+    assert s3.length() == 3;
+    assert s3.startsWith("abc");
+  }
+
+  public void test3() {
+    String s1 = "";
+    String s2 = "";
+    String s3 = s1 + s2;
+    assert s3.length() == 0;
+    assert s3.startsWith("");
+  }
+}

jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation1/Main.class

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.test1 --property "java::Main.test1:()V.assertion.1" --property "java::Main.test1:()V.assertion.2"
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation1/Main.java

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.test2 --property "java::Main.test2:()V.assertion.1" --property "java::Main.test2:()V.assertion.2"
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

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

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.test3 --property "java::Main.test3:()V.assertion.1" --property "java::Main.test3:()V.assertion.2"
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/Main.class

@@ -0,0 +1,10 @@
+public class Main {
+  public void test1(String s1) {
+    String s2 = "abc";
+    assert (s1 + s2).startsWith("abc");
+  }
+
+  public void test2(String s) { assert ("" + s).startsWith("abc"); }
+
+  public void test3(String s) { assert (s + s).startsWith("abc"); }
+}

jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/Main.java

@@ -0,0 +1,11 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.test1 --property "java::Main.test1:(Ljava/lang/String;)V.assertion.1"
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that constant propagation does not happen, since a constant
+result cannot be determined from the arguments to `+`.

jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/test1.desc

@@ -0,0 +1,11 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.test2 --property "java::Main.test2:(Ljava/lang/String;)V.assertion.1"
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that constant propagation does not happen, since a constant
+result cannot be determined from the arguments to `+`.

jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/test2.desc

@@ -0,0 +1,11 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.test3 --property "java::Main.test3:(Ljava/lang/String;)V.assertion.1"
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that constant propagation does not happen, since a constant
+result cannot be determined from the arguments to `+`.

jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/test3.desc

@@ -0,0 +1,7 @@
+public class Main {
+  public void test() {
+    String s = new String();
+    assert s.isEmpty();
+    assert s.startsWith("");
+  }
+}

jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation3/Main.class

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.test
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--