Skip to content

Commit d8ed6fe

Browse files
danpoedanpoe
authored
Merge pull request #5134 from danpoe/feature/constant-propagation-of-string-operations
Constant propagation of CProverString.setLength() and CProverString.setCharAt()
2 parents fd4a8ec + 4bb03aa commit d8ed6fe

22 files changed

+437
-3
lines changed

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

1.44 KB
Binary file not shown.

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

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
import org.cprover.CProverString;
2+
3+
public class Test
4+
{
5+
public void testSuccess1()
6+
{
7+
StringBuffer sb = new StringBuffer("abc");
8+
CProverString.setCharAt(sb, 0, 'd');
9+
assert sb.toString().equals("dbc");
10+
}
11+
12+
public void testSuccess2()
13+
{
14+
StringBuffer sb = new StringBuffer("abc");
15+
CProverString.setCharAt(sb, 2, 'd');
16+
assert sb.toString().equals("abd");
17+
}
18+
19+
public void testNoPropagation1()
20+
{
21+
StringBuffer sb = new StringBuffer("abc");
22+
CProverString.setCharAt(sb, -1, 'd');
23+
assert sb.toString().equals("dbc");
24+
}
25+
26+
public void testNoPropagation2()
27+
{
28+
StringBuffer sb = new StringBuffer("abc");
29+
CProverString.setCharAt(sb, 3, 'd');
30+
assert sb.toString().equals("dbc");
31+
}
32+
33+
public void testNoPropagation3(StringBuffer sb)
34+
{
35+
CProverString.setCharAt(sb, 1, 'd');
36+
assert sb.toString().equals("dbc");
37+
}
38+
39+
public void testNoPropagation4(int index)
40+
{
41+
StringBuffer sb = new StringBuffer("abc");
42+
CProverString.setCharAt(sb, index, 'd');
43+
assert sb.toString().equals("dbc");
44+
}
45+
}

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE symex-driven-lazy-loading-expected-failure
2+
Test.class
3+
--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'
4+
^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
--

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE symex-driven-lazy-loading-expected-failure
2+
Test.class
3+
--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'
4+
^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
--

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE symex-driven-lazy-loading-expected-failure
2+
Test.class
3+
--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'
4+
^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
--

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE symex-driven-lazy-loading-expected-failure
2+
Test.class
3+
--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'
4+
^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
--

‎jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetCharAt/test_success1.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
Test.class
3+
--function Test.testSuccess1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
^VERIFICATION SUCCESSFUL$
8+
--
9+
--

‎jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetCharAt/test_success2.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
Test.class
3+
--function Test.testSuccess2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
^VERIFICATION SUCCESSFUL$
8+
--
9+
--

‎jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/Test.class

1.78 KB
Binary file not shown.

‎jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/Test.java

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
import org.cprover.CProverString;
2+
3+
public class Test
4+
{
5+
public void testSuccess1()
6+
{
7+
StringBuffer sb = new StringBuffer("abc");
8+
CProverString.setLength(sb, 0);
9+
assert sb.toString().equals("");
10+
}
11+
12+
public void testSuccess2()
13+
{
14+
StringBuffer sb = new StringBuffer("abc");
15+
CProverString.setLength(sb, 2);
16+
assert sb.toString().equals("ab");
17+
}
18+
19+
public void testSuccess3()
20+
{
21+
StringBuffer sb = new StringBuffer("abc");
22+
CProverString.setLength(sb, 3);
23+
assert sb.toString().equals("abc");
24+
}
25+
26+
public void testSuccess4()
27+
{
28+
StringBuffer sb = new StringBuffer("abc");
29+
CProverString.setLength(sb, 4);
30+
assert sb.toString().equals("abc\u0000");
31+
}
32+
33+
public void testSuccess5()
34+
{
35+
StringBuffer sb = new StringBuffer("abc");
36+
CProverString.setLength(sb, 5);
37+
assert sb.toString().equals("abc\u0000\u0000");
38+
}
39+
40+
public void testSuccess6(StringBuffer sb)
41+
{
42+
CProverString.setLength(sb, 0);
43+
assert sb.toString().equals("");
44+
}
45+
46+
public void testNoPropagation1()
47+
{
48+
StringBuffer sb = new StringBuffer("abc");
49+
CProverString.setLength(sb, -1);
50+
assert sb.toString().equals("abc");
51+
}
52+
53+
public void testNoPropagation2(StringBuffer sb)
54+
{
55+
CProverString.setLength(sb, 3);
56+
assert sb.toString().equals("abc");
57+
}
58+
59+
public void testNoPropagation3(int newLength)
60+
{
61+
StringBuffer sb = new StringBuffer("abc");
62+
CProverString.setLength(sb, newLength);
63+
assert sb.toString().equals("abc");
64+
}
65+
}

‎jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/test_no_propagation1.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE symex-driven-lazy-loading-expected-failure
2+
Test.class
3+
--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'
4+
^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
--

‎jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/test_no_propagation2.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE symex-driven-lazy-loading-expected-failure
2+
Test.class
3+
--function Test.testNoPropagation2 --show-vcc --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testNoPropagation2:(Ljava/lang/StringBuffer;)V.assertion.1'
4+
^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
--

‎jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/test_no_propagation3.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE symex-driven-lazy-loading-expected-failure
2+
Test.class
3+
--function Test.testNoPropagation3 --show-vcc --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testNoPropagation3:(I)V.assertion.1'
4+
^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
--

‎jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/test_success1.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
Test.class
3+
--function Test.testSuccess1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
^VERIFICATION SUCCESSFUL$
8+
--
9+
--

‎jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/test_success2.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
Test.class
3+
--function Test.testSuccess2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
^VERIFICATION SUCCESSFUL$
8+
--
9+
--

‎jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/test_success3.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
Test.class
3+
--function Test.testSuccess3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
^VERIFICATION SUCCESSFUL$
8+
--
9+
--

‎jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/test_success4.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
Test.class
3+
--function Test.testSuccess4 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
^VERIFICATION SUCCESSFUL$
8+
--
9+
--

‎jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/test_success5.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
Test.class
3+
--function Test.testSuccess5 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
^VERIFICATION SUCCESSFUL$
8+
--
9+
--

‎jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/test_success6.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
Test.class
3+
--function Test.testSuccess5 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
^VERIFICATION SUCCESSFUL$
8+
--
9+
--

‎jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1528,11 +1528,17 @@ void java_string_library_preprocesst::initialize_conversion_table()
15281528
["java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/"
15291529
"String;II)I"] = ID_cprover_string_offset_by_code_point_func;
15301530
cprover_equivalent_to_java_assign_function
1531-
["java::org.cprover.CProverString.setCharAt:(Ljava/lang/String;IC)V"] =
1532-
ID_cprover_string_char_set_func;
1531+
["java::org.cprover.CProverString.setCharAt:(Ljava/lang/"
1532+
"StringBuffer;IC)V"] = ID_cprover_string_char_set_func;
1533+
cprover_equivalent_to_java_assign_function
1534+
["java::org.cprover.CProverString.setCharAt:(Ljava/lang/"
1535+
"StringBuilder;IC)V"] = ID_cprover_string_char_set_func;
15331536
cprover_equivalent_to_java_assign_function
1534-
["java::org.cprover.CProverString.setLength:(Ljava/lang/String;I)V"] =
1537+
["java::org.cprover.CProverString.setLength:(Ljava/lang/StringBuffer;I)V"] =
15351538
ID_cprover_string_set_length_func;
1539+
cprover_equivalent_to_java_assign_function
1540+
["java::org.cprover.CProverString.setLength:(Ljava/lang/"
1541+
"StringBuilder;I)V"] = ID_cprover_string_set_length_func;
15361542
cprover_equivalent_to_java_string_returning_function
15371543
["java::org.cprover.CProverString.subSequence:(Ljava/lang/String;II)Ljava/"
15381544
"lang/CharSequence;"] = ID_cprover_string_substring_func;

0 commit comments

Comments
 (0)