Merge pull request #5134 from danpoe/feature/constant-propagation-of-string-operations

Constant propagation of CProverString.setLength() and CProverString.setCharAt()

Author: danpoe

jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetCharAt/Test.class

@@ -0,0 +1,45 @@
+import org.cprover.CProverString;
+
+public class Test
+{
+  public void testSuccess1()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    CProverString.setCharAt(sb, 0, 'd');
+    assert sb.toString().equals("dbc");
+  }
+
+  public void testSuccess2()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    CProverString.setCharAt(sb, 2, 'd');
+    assert sb.toString().equals("abd");
+  }
+
+  public void testNoPropagation1()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    CProverString.setCharAt(sb, -1, 'd');
+    assert sb.toString().equals("dbc");
+  }
+
+  public void testNoPropagation2()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    CProverString.setCharAt(sb, 3, 'd');
+    assert sb.toString().equals("dbc");
+  }
+
+  public void testNoPropagation3(StringBuffer sb)
+  {
+    CProverString.setCharAt(sb, 1, 'd');
+    assert sb.toString().equals("dbc");
+  }
+
+  public void testNoPropagation4(int index)
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    CProverString.setCharAt(sb, index, 'd');
+    assert sb.toString().equals("dbc");
+  }
+}

jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetCharAt/Test.java

@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.testNoPropagation1 --show-vcc --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testNoPropagation1:()V.assertion.1'
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetCharAt/test_no_propagation1.desc

@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.testNoPropagation2 --show-vcc --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testNoPropagation2:()V.assertion.1'
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetCharAt/test_no_propagation2.desc

@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.testNoPropagation3 --show-vcc --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testNoPropagation3:(Ljava/lang/StringBuffer;)V.assertion.1'
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetCharAt/test_no_propagation3.desc

@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.testNoPropagation4 --show-vcc --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testNoPropagation4:(I)V.assertion.1'
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetCharAt/test_no_propagation4.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testSuccess1 --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/ConstantEvaluationCProverStringSetCharAt/test_success1.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testSuccess2 --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/ConstantEvaluationCProverStringSetCharAt/test_success2.desc

@@ -0,0 +1,65 @@
+import org.cprover.CProverString;
+
+public class Test
+{
+  public void testSuccess1()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    CProverString.setLength(sb, 0);
+    assert sb.toString().equals("");
+  }
+
+  public void testSuccess2()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    CProverString.setLength(sb, 2);
+    assert sb.toString().equals("ab");
+  }
+
+  public void testSuccess3()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    CProverString.setLength(sb, 3);
+    assert sb.toString().equals("abc");
+  }
+
+  public void testSuccess4()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    CProverString.setLength(sb, 4);
+    assert sb.toString().equals("abc\u0000");
+  }
+
+  public void testSuccess5()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    CProverString.setLength(sb, 5);
+    assert sb.toString().equals("abc\u0000\u0000");
+  }
+
+  public void testSuccess6(StringBuffer sb)
+  {
+    CProverString.setLength(sb, 0);
+    assert sb.toString().equals("");
+  }
+
+  public void testNoPropagation1()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    CProverString.setLength(sb, -1);
+    assert sb.toString().equals("abc");
+  }
+
+  public void testNoPropagation2(StringBuffer sb)
+  {
+    CProverString.setLength(sb, 3);
+    assert sb.toString().equals("abc");
+  }
+
+  public void testNoPropagation3(int newLength)
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    CProverString.setLength(sb, newLength);
+    assert sb.toString().equals("abc");
+  }
+}