Merge pull request diffblue#5110 from danpoe/feature/string-constructors

Tests for constant propagation of string constructors

Author: danpoe

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

@@ -0,0 +1,43 @@
+public class Main {
+  public void testSuccess1() {
+    StringBuilder sb = new StringBuilder();
+    assert sb.toString().equals("");
+  }
+
+  public void testSuccess2() {
+    StringBuilder sb = new StringBuilder(0);
+    assert sb.toString().equals("");
+    sb = new StringBuilder(5);
+    assert sb.toString().equals("");
+  }
+
+  public void testSuccess3(int i) {
+    // The capacity argument of StringBuilder is ignored by the constant
+    // propagator, hence we can still constant propagate the two constructors
+    StringBuilder sb = new StringBuilder(i);
+    assert sb.toString().equals("");
+    sb = new StringBuilder(i);
+    assert sb.toString().equals("");
+  }
+
+  public void testSuccess4() {
+    StringBuilder sb = new StringBuilder("abc");
+    assert sb.toString().equals("abc");
+  }
+
+  public void testSuccess5() {
+    CharSequence cs = "abc";
+    StringBuilder sb = new StringBuilder(cs);
+    assert sb.toString().equals("abc");
+  }
+
+  public void testNoPropagation1(String s) {
+    StringBuilder sb = new StringBuilder(s);
+    assert sb.toString().equals("abc");
+  }
+
+  public void testNoPropagation2(CharSequence cs) {
+    StringBuilder sb = new StringBuilder(cs);
+    assert sb.toString().equals("abc");
+  }
+}

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

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

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

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

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

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

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

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.testSuccess3 --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/ConstantEvaluationStringBuilderConstructor/test_success3.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.testSuccess4 --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/ConstantEvaluationStringBuilderConstructor/test_success4.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.testSuccess5 --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/ConstantEvaluationStringBuilderConstructor/test_success5.desc

@@ -0,0 +1,38 @@
+public class Main {
+  public void testSuccess1() {
+    String s = new String();
+    assert s.equals("");
+  }
+
+  public void testSuccess2() {
+    String s = new String("abc");
+    assert s.equals("abc");
+  }
+
+  public void testSuccess3() {
+    StringBuilder sb = new StringBuilder("abc");
+    String s = new String(sb);
+    assert s.equals("abc");
+  }
+
+  public void testSuccess4() {
+    StringBuffer sb = new StringBuffer("abc");
+    String s = new String(sb);
+    assert s.equals("abc");
+  }
+
+  public void testNoPropagation1(String s1) {
+    String s2 = new String(s1);
+    assert s2.equals("abc");
+  }
+
+  public void testNoPropagation2(StringBuilder sb) {
+    String s = new String(sb);
+    assert s.equals("abc");
+  }
+
+  public void testNoPropagation3(StringBuffer sb) {
+    String s = new String(sb);
+    assert s.equals("abc");
+  }
+}

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

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

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

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

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

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

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

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.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/ConstantEvaluationStringConstructor/Main.java

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

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.testSuccess3 --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/ConstantEvaluationStringConstructor/test_no_propagation2.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.testSuccess4 --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/ConstantEvaluationStringConstructor/test_no_propagation3.desc

@@ -1679,9 +1679,21 @@ void java_string_library_preprocesst::initialize_conversion_table()
       std::placeholders::_2,
       std::placeholders::_3,
       std::placeholders::_4);
+  conversion_table
+    ["java::java.lang.StringBuilder.<init>:(Ljava/lang/CharSequence;)V"] =
+      std::bind(
+        &java_string_library_preprocesst::make_copy_constructor_code,
+        this,
+        std::placeholders::_1,
+        std::placeholders::_2,
+        std::placeholders::_3,
+        std::placeholders::_4);
   cprover_equivalent_to_java_constructor
     ["java::java.lang.StringBuilder.<init>:()V"]=
       ID_cprover_string_empty_string_func;
+  cprover_equivalent_to_java_constructor
+    ["java::java.lang.StringBuilder.<init>:(I)V"] =
+      ID_cprover_string_empty_string_func;
 
   cprover_equivalent_to_java_assign_and_return_function
     ["java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]=

jbmc/regression/jbmc-strings/ConstantEvaluationStringConstructor/test_success1.desc

@@ -359,8 +359,8 @@ void goto_symext::constant_propagate_empty_string(
   const array_typet char_array_type(char_type, length);
 
   DATA_INVARIANT(
-    f_l1.arguments().size() == 2,
-    "empty string primitive takes two output arguments");
+    f_l1.arguments().size() >= 2,
+    "empty string primitive requires two output arguments");
 
   const array_exprt char_array({}, char_array_type);