Merge pull request #4885 from danpoe/feature/constant-propagate-string-concatenation

[TG-8293] Constant propagation for empty strings and string concatenation [blocks: #4941]

Author: danpoe

jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/Main.class

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

jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/Main.java

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.test --property "java::Main.test:()V.assertion.1" --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/test.desc

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

jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation05-VerificationFailure/Main.class

@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.test1
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation05-VerificationFailure/Main.java

@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.test2
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation05-VerificationFailure/test1.desc

@@ -0,0 +1,9 @@
+public class Main {
+  public void test() {
+    String s1 = "ディフ";
+    String s2 = "ブルー";
+    String s3 = s1 + s2;
+    assert s3.length() == 6;
+    assert s3.startsWith("ディフブルー");
+  }
+}

jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation05-VerificationFailure/test2.desc

@@ -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/ConstantEvaluationStringConcatenation06-2byteChar/Main.class

@@ -0,0 +1,9 @@
+public class Main {
+  public void test() {
+    String s1 = "\t";
+    String s2 = "\\";
+    String s3 = s1 + s2;
+    assert s3.length() == 2;
+    assert s3.startsWith("\t\\");
+  }
+}

jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/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/ConstantEvaluationStringConcatenation06-2byteChar/test.desc

@@ -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/ConstantEvaluationStringConcatenation07-NonPrintableChar/Main.class

@@ -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/ConstantEvaluationStringConcatenation07-NonPrintableChar/Main.java

@@ -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/ConstantEvaluationStringConcatenation07-NonPrintableChar/test.desc

@@ -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/StringBuilderAppendConstantEvaluation1/Main.class

@@ -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/StringBuilderAppendConstantEvaluation1/Main.java

@@ -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/StringBuilderAppendConstantEvaluation1/test.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/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$
+--
+--

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

@@ -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/StringBuilderAppendConstantEvaluation2/test1.desc

@@ -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/StringBuilderAppendConstantEvaluation2/test2.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/StringBuilderAppendConstantEvaluation2/test3.desc

@@ -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/StringBuilderDefaultConstructorConstantEvaluation/Main.class

@@ -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/StringBuilderDefaultConstructorConstantEvaluation/Main.java

@@ -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/StringBuilderDefaultConstructorConstantEvaluation/test.desc

@@ -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/StringConcatenationConstantEvaluation1/Main.class

@@ -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/StringConcatenationConstantEvaluation1/Main.java

@@ -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/StringConcatenationConstantEvaluation1/test.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/Main.class

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

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

@@ -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/StringConcatenationConstantEvaluation2/test1.desc

@@ -15,34 +15,12 @@ Author: Chris Smowton, [email protected]
 #include <util/arith_tools.h>
 #include <util/expr_initializer.h>
 #include <util/namespace.h>
+#include <util/string_utils.h>
 #include <util/unicode.h>
 
 #include <iomanip>
 #include <sstream>
 
-/// Replace non-alphanumeric characters with `_xx` escapes, where xx are hex
-/// digits. Underscores are replaced by `__`.
-/// \param to_escape: string to escape
-/// \return string with non-alphanumeric characters escaped
-static std::string escape_non_alnum(const std::string &to_escape)
-{
-  std::ostringstream escaped;
-  for(auto &ch : to_escape)
-  {
-    if(ch=='_')
-      escaped << "__";
-    else if(isalnum(ch))
-      escaped << ch;
-    else
-      escaped << '_'
-              << std::hex
-              << std::setfill('0')
-              << std::setw(2)
-              << (unsigned int)ch;
-  }
-  return escaped.str();
-}
-
 /// Convert UCS-2 or UTF-16 to an array expression.
 /// \par parameters: `in`: wide string to convert
 /// \return Returns a Java char array containing the same wchars.