Merge pull request #4941 from danpoe/feature/constant-propagate-string-substring

[TG-7648] Constant propagation of substring operations

Author: danpoe

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

@@ -0,0 +1,25 @@
+public class Main {
+  public void test() {
+    StringBuilder sb = new StringBuilder("abc");
+
+    String s1 = sb.substring(0);
+    assert s1.length() == 3;
+    assert s1.startsWith("abc");
+
+    String s2 = sb.substring(1);
+    assert s2.length() == 2;
+    assert s2.startsWith("bc");
+
+    String s3 = sb.substring(0, 3);
+    assert s3.length() == 3;
+    assert s3.startsWith("abc");
+
+    String s4 = sb.substring(0, 0);
+    assert s4.length() == 0;
+    assert s4.startsWith("");
+
+    String s5 = sb.substring(0, 1);
+    assert s5.length() == 1;
+    assert s5.startsWith("a");
+  }
+}

jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation1/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/StringBuilderSubstringConstantEvaluation1/test.desc

@@ -0,0 +1,18 @@
+public class Main {
+  public void test1(StringBuilder sb) {
+    String s = sb.substring(0);
+    assert s.startsWith("xyz");
+  }
+
+  public void test2(int i) {
+    StringBuilder sb = new StringBuilder("abc");
+
+    String s = sb.substring(i);
+    assert s.startsWith("xyz");
+  }
+
+  public void test3(StringBuilder sb, int i) {
+    String s = sb.substring(i);
+    assert s.startsWith("xyz");
+  }
+}

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

@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.test1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.test1:(Ljava/lang/StringBuilder;)V.assertion.1"
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

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

@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.test2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.test2:(I)V.assertion.1"
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

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

@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.test3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.test3:(Ljava/lang/StringBuilder;I)V.assertion.1"
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

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

@@ -0,0 +1,16 @@
+public class Main {
+  public void test1() {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.substring(-1);
+  }
+
+  public void test2() {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.substring(4);
+  }
+
+  public void test3() {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.substring(-1, 4);
+  }
+}

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

@@ -0,0 +1,13 @@
+FUTURE
+Main.class
+--function Main.test1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [1-9][0-9]* VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+no uncaught exception: FAILURE
+^VERIFICATION FAILED$
+--
+--
+This test will pass once a model for StringBuilder.substring() exists that
+throws an exception when the index is greater or equal to the length of the
+string.

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

@@ -0,0 +1,13 @@
+FUTURE
+Main.class
+--function Main.test2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [1-9][0-9]* VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+no uncaught exception: FAILURE
+^VERIFICATION FAILED$
+--
+--
+This test will pass once a model for StringBuilder.substring() exists that
+throws an exception when the index is greater or equal to the length of the
+string.

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

@@ -0,0 +1,13 @@
+FUTURE
+Main.class
+--function Main.test3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [1-9][0-9]* VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+no uncaught exception: FAILURE
+^VERIFICATION FAILED$
+--
+--
+This test will pass once a model for StringBuilder.substring() exists that
+throws an exception when the index is greater or equal to the length of the
+string.

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

@@ -0,0 +1,20 @@
+public class Main {
+  public void test() {
+    String s = "abc";
+
+    String s1 = s.substring(0);
+    assert s1.equals("abc");
+
+    String s2 = s.substring(1);
+    assert s2.equals("bc");
+
+    String s3 = s.substring(0, 3);
+    assert s3.equals("abc");
+
+    String s4 = s.substring(0, 0);
+    assert s4.equals("");
+
+    String s5 = s.substring(0, 1);
+    assert s5.equals("a");
+  }
+}

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

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.test --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/StringBuilderSubstringConstantEvaluation3/test3.desc

@@ -0,0 +1,18 @@
+public class Main {
+  public void test1(String s1) {
+    String s2 = s1.substring(0);
+    assert s2.startsWith("xyz");
+  }
+
+  public void test2(int i) {
+    String s1 = "abc";
+
+    String s2 = s1.substring(i);
+    assert s2.startsWith("xyz");
+  }
+
+  public void test3(String s1, int i) {
+    String s2 = s1.substring(i);
+    assert s2.startsWith("xyz");
+  }
+}

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

@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.test1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.test1:(Ljava/lang/String;)V.assertion.1"
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

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

@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.test2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.test2:(I)V.assertion.1"
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

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

@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.test3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.test3:(Ljava/lang/String;I)V.assertion.1"
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

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

@@ -0,0 +1,16 @@
+public class Main {
+  public void test1() {
+    String s1 = "abc";
+    s1.substring(-1);
+  }
+
+  public void test2() {
+    String s1 = "abc";
+    s1.substring(4);
+  }
+
+  public void test3() {
+    String s1 = "abc";
+    s1.substring(-1, 4);
+  }
+}

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

@@ -0,0 +1,10 @@
+CORE
+Main.class
+--function Main.test1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [1-9][0-9]* VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+no uncaught exception: FAILURE
+^VERIFICATION FAILED$
+--
+--

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

@@ -0,0 +1,10 @@
+CORE
+Main.class
+--function Main.test2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [1-9][0-9]* VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+no uncaught exception: FAILURE
+^VERIFICATION FAILED$
+--
+--

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

@@ -0,0 +1,10 @@
+CORE
+Main.class
+--function Main.test3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [1-9][0-9]* VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+no uncaught exception: FAILURE
+^VERIFICATION FAILED$
+--
+--