Implement constant propagation for substring operations

This implements constant propagation of ID_cprover_string_substring_func
function application expressions. These are in turn used by the various
substring operations of String and StringBuilder.

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,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");
+  }
+}