Skip to content

Commit 7b9d728

Browse files
author
Joel Allred
committed
Test String.compareTo more systematically and use nondet strings
Using nondet strings ensures that the string solver is invoked, and the string operation is not replaced during constant propagation.
1 parent 4a06254 commit 7b9d728

File tree

14 files changed

+167
-0
lines changed

14 files changed

+167
-0
lines changed

‎jbmc/regression/jbmc-strings/StringCompareTo/Main.class

1.3 KB
Binary file not shown.

‎jbmc/regression/jbmc-strings/StringCompareTo/Main.java

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
class Main {
2+
3+
public static void nondetPass(String s1, String s2) {
4+
if (s1.startsWith("abc") && s2.startsWith("cde")) {
5+
assert s1.compareTo(s2) == -2; // assertion.1 true
6+
assert s2.compareTo(s1) == 2; // assertion.2 true
7+
} else if (s1.startsWith("abc") && s1.length() == 3 && s2.startsWith("abc") && s2.length() > 3) {
8+
assert s1.compareTo(s2) < 0; // assertion.3 true
9+
assert s2.compareTo(s1) > 0; // assertion.4 true
10+
} else if (s1.startsWith("abc") && s1.length() == 3 && s2.startsWith("abc") && s2.length() == 3) {
11+
assert s1.compareTo(s2) == 0; // assertion.5 true
12+
assert s2.compareTo(s1) == 0; // assertion.6 true
13+
}
14+
}
15+
16+
public static void nondetFail(boolean b, String s1, String s2) {
17+
if (s1.startsWith("abc") && s2.startsWith("cde")) {
18+
if (b)
19+
assert s1.compareTo(s2) != -2; // assertion.1 false
20+
else
21+
assert s2.compareTo(s1) != 2; // assertion.2 false
22+
} else if (s1.startsWith("abc") && s1.length() == 3 && s2.startsWith("abc") && s2.length() > 3) {
23+
if (b)
24+
assert s1.compareTo(s2) >= 0; // assertion.3 false
25+
else
26+
assert s2.compareTo(s1) <= 0; // assertion.4 false
27+
} else if (s1.startsWith("abc") && s1.length() == 3 && s2.startsWith("abc") && s2.length() == 3) {
28+
if (b)
29+
assert s1.compareTo(s2) != 0; // assertion.5 false
30+
else
31+
assert s2.compareTo(s1) != 0; // assertion.6 false
32+
}
33+
}
34+
35+
}

‎jbmc/regression/jbmc-strings/StringCompareTo/testFail1.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE symex-driven-lazy-loading-expected-failure
2+
Main.class
3+
--function Main.nondetFail --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.nondetFail:(ZLjava/lang/String;Ljava/lang/String;)V.assertion.1"
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
Checks that String.compareTo is implemented in the string solver.
10+
Nondeterministic strings are used to make sure the operation is not replaced
11+
by constant propagation.

‎jbmc/regression/jbmc-strings/StringCompareTo/testFail2.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE symex-driven-lazy-loading-expected-failure
2+
Main.class
3+
--function Main.nondetFail --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.nondetFail:(ZLjava/lang/String;Ljava/lang/String;)V.assertion.2"
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
Checks that String.compareTo is implemented in the string solver.
10+
Nondeterministic strings are used to make sure the operation is not replaced
11+
by constant propagation.

‎jbmc/regression/jbmc-strings/StringCompareTo/testFail3.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE symex-driven-lazy-loading-expected-failure
2+
Main.class
3+
--function Main.nondetFail --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.nondetFail:(ZLjava/lang/String;Ljava/lang/String;)V.assertion.3"
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
Checks that String.compareTo is implemented in the string solver.
10+
Nondeterministic strings are used to make sure the operation is not replaced
11+
by constant propagation.

‎jbmc/regression/jbmc-strings/StringCompareTo/testFail4.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE symex-driven-lazy-loading-expected-failure
2+
Main.class
3+
--function Main.nondetFail --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.nondetFail:(ZLjava/lang/String;Ljava/lang/String;)V.assertion.4"
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
Checks that String.compareTo is implemented in the string solver.
10+
Nondeterministic strings are used to make sure the operation is not replaced
11+
by constant propagation.

‎jbmc/regression/jbmc-strings/StringCompareTo/testFail5.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE symex-driven-lazy-loading-expected-failure
2+
Main.class
3+
--function Main.nondetFail --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.nondetFail:(ZLjava/lang/String;Ljava/lang/String;)V.assertion.5"
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
Checks that String.compareTo is implemented in the string solver.
10+
Nondeterministic strings are used to make sure the operation is not replaced
11+
by constant propagation.

‎jbmc/regression/jbmc-strings/StringCompareTo/testFail6.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE symex-driven-lazy-loading-expected-failure
2+
Main.class
3+
--function Main.nondetFail --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.nondetFail:(ZLjava/lang/String;Ljava/lang/String;)V.assertion.6"
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
Checks that String.compareTo is implemented in the string solver.
10+
Nondeterministic strings are used to make sure the operation is not replaced
11+
by constant propagation.

‎jbmc/regression/jbmc-strings/StringCompareTo/testPass1.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE symex-driven-lazy-loading-expected-failure
2+
Main.class
3+
--function Main.nondetPass --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.nondetPass:(Ljava/lang/String;Ljava/lang/String;)V.assertion.1"
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Checks that String.compareTo is implemented in the string solver.
10+
Nondeterministic strings are used to make sure the operation is not replaced
11+
by constant propagation.

‎jbmc/regression/jbmc-strings/StringCompareTo/testPass2.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE symex-driven-lazy-loading-expected-failure
2+
Main.class
3+
--function Main.nondetPass --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.nondetPass:(Ljava/lang/String;Ljava/lang/String;)V.assertion.2"
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Checks that String.compareTo is implemented in the string solver.
10+
Nondeterministic strings are used to make sure the operation is not replaced
11+
by constant propagation.

‎jbmc/regression/jbmc-strings/StringCompareTo/testPass3.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE symex-driven-lazy-loading-expected-failure
2+
Main.class
3+
--function Main.nondetPass --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.nondetPass:(Ljava/lang/String;Ljava/lang/String;)V.assertion.3"
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Checks that String.compareTo is implemented in the string solver.
10+
Nondeterministic strings are used to make sure the operation is not replaced
11+
by constant propagation.

‎jbmc/regression/jbmc-strings/StringCompareTo/testPass4.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE symex-driven-lazy-loading-expected-failure
2+
Main.class
3+
--function Main.nondetPass --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.nondetPass:(Ljava/lang/String;Ljava/lang/String;)V.assertion.4"
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Checks that String.compareTo is implemented in the string solver.
10+
Nondeterministic strings are used to make sure the operation is not replaced
11+
by constant propagation.

‎jbmc/regression/jbmc-strings/StringCompareTo/testPass5.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE symex-driven-lazy-loading-expected-failure
2+
Main.class
3+
--function Main.nondetPass --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.nondetPass:(Ljava/lang/String;Ljava/lang/String;)V.assertion.5"
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Checks that String.compareTo is implemented in the string solver.
10+
Nondeterministic strings are used to make sure the operation is not replaced
11+
by constant propagation.

‎jbmc/regression/jbmc-strings/StringCompareTo/testPass6.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE symex-driven-lazy-loading-expected-failure
2+
Main.class
3+
--function Main.nondetPass --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.nondetPass:(Ljava/lang/String;Ljava/lang/String;)V.assertion.6"
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Checks that String.compareTo is implemented in the string solver.
10+
Nondeterministic strings are used to make sure the operation is not replaced
11+
by constant propagation.

0 commit comments

Comments
 (0)