Skip to content

Commit 8da81c5

Browse files
author
Joel Allred
authored
Merge pull request #4760 from allredj/feature/string-format-deps
String.format now uses dependency graph
2 parents c63c167 + 18fa75f commit 8da81c5

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

53 files changed

+1463
-303
lines changed

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

-1.8 KB
Binary file not shown.

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

1.63 KB
Binary file not shown.

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

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
public class Test {
2+
public static String testBool(boolean b) {
3+
String u = String.format("bool: %b", b);
4+
if (u.equals("bool: true"))
5+
assert(false);
6+
else if (u.equals("bool: false"))
7+
assert(false);
8+
else
9+
assert(false); // unreachable
10+
return u;
11+
}
12+
13+
public static String testBoolLength(boolean b) {
14+
String u = String.format("bool: %b", b);
15+
if (u.length() == 10)
16+
assert(false);
17+
else if (u.length() == 11)
18+
assert(false);
19+
else
20+
assert(false); // unreachable
21+
return u;
22+
}
23+
24+
public static String testBoolLengthTrue() {
25+
String u = String.format("bool: %b", true);
26+
if (u.length() == 10)
27+
assert(false);
28+
else
29+
assert(false); // unreachable
30+
return u;
31+
}
32+
33+
public static String testBoolLengthFalse() {
34+
String u = String.format("bool: %b", false);
35+
if (u.length() == 11)
36+
assert(false);
37+
else
38+
assert(false); // unreachable
39+
return u;
40+
}
41+
42+
public static String testBoolLengthNull() {
43+
Boolean b = null;
44+
String u = String.format("bool: %b", b);
45+
if (u.length() == 11)
46+
assert(false);
47+
else
48+
assert(false); // unreachable
49+
return u;
50+
}
51+
}

‎jbmc/regression/jbmc-strings/StringFormatBool/TestHex.java

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
public class TestHex {
2+
public static String testHex(int i) {
3+
String u = String.format("di%xlue", i);
4+
if (u.equals("diffblue"))
5+
assert(false);
6+
else if (u.startsWith("di"))
7+
assert(false);
8+
else
9+
assert(false);
10+
return u;
11+
}
12+
}

‎jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length-true-fail.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
Test.class
3+
--function Test.testBoolLengthTrue --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testBoolLengthTrue:()Ljava/lang/String;.assertion.1"
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
line 27 assertion at file Test.java .*: FAILURE

‎jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length-true-pass.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
KNOWNBUG
2+
Test.class
3+
--function Test.testBoolLengthTrue --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testBoolLengthTrue:()Ljava/lang/String;.assertion.2"
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
line 29 assertion at file Test.java .*: SUCCESS
7+
--
8+
--
9+
There seems to be some constraints missing, as the length of the 'true'
10+
boolean can be either 4 or 5.

‎jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length1.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
Test.class
3+
--function Test.testBoolLength --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testBoolLength:(Z)Ljava/lang/String;.assertion.1"
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
line 16 assertion at file Test.java .*: FAILURE

‎jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length2.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
Test.class
3+
--function Test.testBoolLength --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testBoolLength:(Z)Ljava/lang/String;.assertion.2"
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
line 18 assertion at file Test.java .*: FAILURE

‎jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length3.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE symex-driven-lazy-loading-expected-failure
2+
Test.class
3+
--function Test.testBoolLength --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testBoolLength:(Z)Ljava/lang/String;.assertion.3"
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
line 20 assertion at file Test.java .*: SUCCESS

‎jbmc/regression/jbmc-strings/StringFormatBool/test-bool1.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
Test.class
3+
--function Test.testBool --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testBool:(Z)Ljava/lang/String;.assertion.1"
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
line 5 assertion at file Test.java .*: FAILURE

‎jbmc/regression/jbmc-strings/StringFormatBool/test-bool2.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
Test.class
3+
--function Test.testBool --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testBool:(Z)Ljava/lang/String;.assertion.2"
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
line 7 assertion at file Test.java .*: FAILURE

‎jbmc/regression/jbmc-strings/StringFormatBool/test-bool3.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE symex-driven-lazy-loading-expected-failure
2+
Test.class
3+
--function Test.testBool --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testBool:(Z)Ljava/lang/String;.assertion.3"
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
line 9 assertion at file Test.java .*: SUCCESS

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

1.16 KB
Binary file not shown.

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

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
public class Test {
2+
public static String testHex(int i) {
3+
String u = String.format("di%xlue", i);
4+
if (u.equals("diffblue"))
5+
assert(false);
6+
else if (u.startsWith("di"))
7+
assert(false);
8+
else
9+
assert(false);
10+
return u;
11+
}
12+
13+
public static void testHexLengthConstPASS() {
14+
String u = String.format("di%xlue", 255);
15+
assert u.length() == 7;
16+
}
17+
18+
public static void testHexLengthConstFAIL() {
19+
String u = String.format("di%xlue", 255);
20+
assert u.length() != 7;
21+
}
22+
}

‎jbmc/regression/jbmc-strings/StringFormatHex/TestHex.java

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
public class TestHex {
2+
public static String testHex(int i) {
3+
String u = String.format("di%xlue", i);
4+
if (u.equals("diffblue"))
5+
assert(false);
6+
else if (u.startsWith("di"))
7+
assert(false);
8+
else
9+
assert(false);
10+
return u;
11+
}
12+
}

‎jbmc/regression/jbmc-strings/StringFormatHex/test-hex-length-const-fail.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
Test.class
3+
--function Test.testHexLengthConstFAIL --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testHexLengthConstFAIL:()V.assertion.1"
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
line 20 assertion at file Test.java .*: FAILURE

‎jbmc/regression/jbmc-strings/StringFormatHex/test-hex-length-const-pass.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
Test.class
3+
--function Test.testHexLengthConstPASS --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testHexLengthConstPASS:()V.assertion.1"
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
line 15 assertion at file Test.java .*: SUCCESS

‎jbmc/regression/jbmc-strings/StringFormat/test-hex1.desc renamed to ‎jbmc/regression/jbmc-strings/StringFormatHex/test-hex1.desc

File renamed without changes.

‎jbmc/regression/jbmc-strings/StringFormat/test-hex2.desc renamed to ‎jbmc/regression/jbmc-strings/StringFormatHex/test-hex2.desc

File renamed without changes.

‎jbmc/regression/jbmc-strings/StringFormat/test-hex3.desc renamed to ‎jbmc/regression/jbmc-strings/StringFormatHex/test-hex3.desc

File renamed without changes.

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

1.29 KB
Binary file not shown.

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

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
public class Test {
2+
public static String testInt(int i) {
3+
String u = String.format("Hello %d !", i);
4+
if (u.equals("Hello 10 !"))
5+
assert(false);
6+
else if (!u.startsWith("Hello"))
7+
assert(false);
8+
else
9+
assert(false);
10+
return u;
11+
}
12+
13+
public static void testIntLength(int i) {
14+
String u = String.format("Hello %d !", i);
15+
assert u.length() == 20;
16+
}
17+
18+
public static void testIntLengthConstPASS() {
19+
String u = String.format("Hello %d !", -12345);
20+
assert u.length() == 14;
21+
}
22+
23+
public static void testIntLengthConstFAIL() {
24+
String u = String.format("Hello %d !", -12345);
25+
assert u.length() != 14;
26+
}
27+
}

‎jbmc/regression/jbmc-strings/StringFormatInt/test-int-length-const-fail.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
Test.class
3+
--function Test.testIntLengthConstFAIL --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testIntLengthConstFAIL:()V.assertion.1"
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
line 25 assertion at file Test.java .*: FAILURE

‎jbmc/regression/jbmc-strings/StringFormatInt/test-int-length-const-pass.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
Test.class
3+
--function Test.testIntLengthConstPASS --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testIntLengthConstPASS:()V.assertion.1"
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
line 20 assertion at file Test.java .*: SUCCESS

‎jbmc/regression/jbmc-strings/StringFormatInt/test-int-length.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
Test.class
3+
--function Test.testIntLength --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testIntLength:(I)V.assertion.1"
4+
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
line 15 assertion at file Test.java .*: FAILURE

‎jbmc/regression/jbmc-strings/StringFormat/test-int1.desc renamed to ‎jbmc/regression/jbmc-strings/StringFormatInt/test-int1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,4 @@ Test.class
33
--function Test.testInt --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testInt:(I)Ljava/lang/String;.assertion.1"
44
^EXIT=10$
55
^SIGNAL=0$
6-
line 16 assertion at file Test.java .*: FAILURE
6+
line 5 assertion at file Test.java .*: FAILURE

‎jbmc/regression/jbmc-strings/StringFormat/test-int2.desc renamed to ‎jbmc/regression/jbmc-strings/StringFormatInt/test-int2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,4 @@ Test.class
33
--function Test.testInt --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testInt:(I)Ljava/lang/String;.assertion.2"
44
^EXIT=0$
55
^SIGNAL=0$
6-
line 18 assertion at file Test.java .*: SUCCESS
6+
line 7 assertion at file Test.java .*: SUCCESS

‎jbmc/regression/jbmc-strings/StringFormat/test-int3.desc renamed to ‎jbmc/regression/jbmc-strings/StringFormatInt/test-int3.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,4 @@ Test.class
33
--function Test.testInt --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testInt:(I)Ljava/lang/String;.assertion.3"
44
^EXIT=10$
55
^SIGNAL=0$
6-
line 20 assertion at file Test.java .*: FAILURE
6+
line 9 assertion at file Test.java .*: FAILURE

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

1.71 KB
Binary file not shown.

‎jbmc/regression/jbmc-strings/StringFormat/Test.java renamed to ‎jbmc/regression/jbmc-strings/StringFormatString/Test.java

Lines changed: 17 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -1,25 +1,4 @@
11
public class Test {
2-
public static String testHex(int i) {
3-
String u = String.format("di%xlue", i);
4-
if (u.equals("diffblue"))
5-
assert(false);
6-
else if (u.startsWith("di"))
7-
assert(false);
8-
else
9-
assert(false);
10-
return u;
11-
}
12-
13-
public static String testInt(int i) {
14-
String u = String.format("Hello %d !", i);
15-
if (u.equals("Hello 10 !"))
16-
assert(false);
17-
else if (!u.startsWith("Hello"))
18-
assert(false);
19-
else
20-
assert(false);
21-
return u;
22-
}
232

243
public static String string1(String s) {
254
if (s == null)
@@ -34,6 +13,23 @@ else if (u.startsWith("impossible!"))
3413
return u;
3514
}
3615

16+
public static void string1Length(String s) {
17+
if (s == null)
18+
return;
19+
String u = String.format("Hello %s !", s);
20+
assert u.length() == 10;
21+
}
22+
23+
public static void string1LengthConstPASS() {
24+
String u = String.format("Hello %s !", "world");
25+
assert u.length() == 13;
26+
}
27+
28+
public static void string1LengthConstFAIL() {
29+
String u = String.format("Hello %s !", "world");
30+
assert u.length() != 13;
31+
}
32+
3733
public static String string2(String s, String t) {
3834
if (s == null || t == null)
3935
return "null null";

‎jbmc/regression/jbmc-strings/StringFormatString/TestString.java

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
public class Test {
2+
public static String string1(String s) {
3+
if (s == null)
4+
return "null!";
5+
String u = String.format("Hello %s !", s);
6+
if (u.equals("Hello world !"))
7+
assert(false);
8+
else if (u.startsWith("impossible!"))
9+
assert(false);
10+
else
11+
assert(false);
12+
return u;
13+
}
14+
15+
public static void string1Length(String s) {
16+
if (s == null)
17+
return;
18+
String u = String.format("Hello %s !", s);
19+
assert u.length() == 10;
20+
return 1;
21+
}
22+
23+
public static void string1LengthConst() {
24+
String u = String.format("Hello %s !", "world");
25+
assert u.length() == 13;
26+
return 1;
27+
}
28+
}

‎jbmc/regression/jbmc-strings/StringFormatString/test-string1-length-const-FAIL.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
Test.class
3+
--function Test.string1LengthConstPASS --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
line 25 assertion at file Test.java .*: SUCCESS

‎jbmc/regression/jbmc-strings/StringFormatString/test-string1-length-const-PASS.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
Test.class
3+
--function Test.string1LengthConstPASS --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
line 25 assertion at file Test.java .*: SUCCESS

‎jbmc/regression/jbmc-strings/StringFormatString/test-string1-length.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
Test.class
3+
--function Test.string1Length --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
line 20 assertion at file Test.java .*: FAILURE

‎jbmc/regression/jbmc-strings/StringFormat/test-string1.desc renamed to ‎jbmc/regression/jbmc-strings/StringFormatString/test-string1.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ Test.class
33
--function Test.string1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
6-
line 29 assertion at file Test.java .*: FAILURE
7-
line 31 assertion at file Test.java .*: SUCCESS
8-
line 33 assertion at file Test.java .*: FAILURE
6+
line 8 assertion at file Test.java .*: FAILURE
7+
line 10 assertion at file Test.java .*: SUCCESS
8+
line 12 assertion at file Test.java .*: FAILURE

‎jbmc/regression/jbmc-strings/StringFormat/test-string2.desc renamed to ‎jbmc/regression/jbmc-strings/StringFormatString/test-string2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,4 @@ Test.class
33
--function Test.string2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --max-nondet-string-length 20 --property "java::Test.string2:(Ljava/lang/String;Ljava/lang/String;)Ljava/lang/String;.assertion.1"
44
^EXIT=0$
55
^SIGNAL=0$
6-
line 41 assertion at file Test.java .*: SUCCESS
6+
line 37 assertion at file Test.java .*: SUCCESS

‎jbmc/regression/jbmc-strings/StringFormat/test-string3.desc renamed to ‎jbmc/regression/jbmc-strings/StringFormatString/test-string3.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,4 @@ Test.class
33
--function Test.string3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --max-nondet-string-length 5 --property "java::Test.string3:(Ljava/lang/String;Ljava/lang/String;)Ljava/lang/String;.assertion.1"
44
^EXIT=0$
55
^SIGNAL=0$
6-
line 49 assertion at file Test.java .*: SUCCESS
6+
line 45 assertion at file Test.java .*: SUCCESS

‎src/solvers/Makefile

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -161,8 +161,10 @@ SRC = $(BOOLEFORCE_SRC) \
161161
refinement/refine_arrays.cpp \
162162
strings/array_pool.cpp \
163163
strings/equation_symbol_mapping.cpp \
164+
strings/format_specifier.cpp \
164165
strings/string_builtin_function.cpp \
165166
strings/string_dependencies.cpp \
167+
strings/string_format_builtin_function.cpp \
166168
strings/string_refinement.cpp \
167169
strings/string_refinement_util.cpp \
168170
strings/string_constraint.cpp \

0 commit comments

Comments
 (0)