Skip to content

Commit a8bdb09

Browse files
author
Joel Allred
authored
Merge pull request diffblue#1817 from allredj/string-primitives-for-exceptions
TG-2153 Add more String primitives to JBMC
2 parents bf9b2c1 + 2b92cd3 commit a8bdb09

Some content is hidden

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

41 files changed

+319
-74
lines changed

‎regression/jbmc-strings/cprover/CProverString.class

3.28 KB
Binary file not shown.

‎regression/jbmc-strings/cprover/CProverString.java

+121
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,29 @@ public static char charAt(String s, int i) {
88
return '\u0000';
99
}
1010

11+
public static int codePointAt(String s, int index) {
12+
return s.codePointAt(index);
13+
}
14+
15+
public static int codePointBefore(String s, int index) {
16+
return s.codePointBefore(index);
17+
}
18+
19+
public static int codePointCount(
20+
String s, int beginIndex, int endIndex) {
21+
return s.codePointCount(beginIndex, endIndex);
22+
}
23+
24+
public static int offsetByCodePoints(
25+
String s, int index, int codePointOffset) {
26+
return s.offsetByCodePoints(index, codePointOffset);
27+
}
28+
29+
public static CharSequence subSequence(
30+
String s, int beginIndex, int endIndex) {
31+
return s.subSequence(beginIndex, endIndex);
32+
}
33+
1134
public static String substring(String s, int i) {
1235
if (i <= 0)
1336
return s;
@@ -26,4 +49,102 @@ public static String substring(String s, int i, int j) {
2649
return "";
2750
return s.substring(i, j);
2851
}
52+
53+
public static StringBuilder append(
54+
StringBuilder sb, CharSequence cs, int i, int j) {
55+
return sb.append(cs, i, j);
56+
}
57+
58+
public static StringBuilder delete(StringBuilder sb, int start, int end) {
59+
return sb.delete(start, end);
60+
}
61+
62+
public static StringBuilder deleteCharAt(StringBuilder sb, int index) {
63+
return sb.deleteCharAt(index);
64+
}
65+
66+
public static StringBuilder insert(
67+
StringBuilder sb, int offset, String str) {
68+
return sb.insert(offset, str);
69+
}
70+
71+
public static StringBuilder insert(
72+
StringBuilder sb, int offset, boolean b) {
73+
return sb.insert(offset, b);
74+
}
75+
76+
public static StringBuilder insert(
77+
StringBuilder sb, int offset, char c) {
78+
return sb.insert(offset, c);
79+
}
80+
81+
public static StringBuilder insert(
82+
StringBuilder sb, int offset, int i) {
83+
return sb.insert(offset, i);
84+
}
85+
86+
public static StringBuilder insert(
87+
StringBuilder sb, int offset, long l) {
88+
return sb.insert(offset, l);
89+
}
90+
91+
public static StringBuilder insert(
92+
StringBuilder sb, int offset, float f) {
93+
return sb.insert(offset, f);
94+
}
95+
96+
public static StringBuilder insert(
97+
StringBuilder sb, int offset, double d) {
98+
return sb.insert(offset, d);
99+
}
100+
101+
public static void setLength(StringBuffer sb, int newLength) {
102+
sb.setLength(newLength);
103+
}
104+
105+
public static char charAt(StringBuffer sb, int index) {
106+
return sb.charAt(index);
107+
}
108+
109+
public static void setCharAt(StringBuffer sb, int index, char c) {
110+
sb.setCharAt(index, c);
111+
}
112+
113+
public static StringBuffer delete(
114+
StringBuffer sb, int start, int end) {
115+
return sb.delete(start, end);
116+
}
117+
118+
public static StringBuffer deleteCharAt(StringBuffer sb, int index) {
119+
return sb.deleteCharAt(index);
120+
}
121+
122+
public static String substring(StringBuffer sb, int start, int end) {
123+
return sb.substring(start, end);
124+
}
125+
126+
public static StringBuffer insert(
127+
StringBuffer sb, int offset, String str) {
128+
return sb.insert(offset, str);
129+
}
130+
131+
public static StringBuffer insert(
132+
StringBuffer sb, int offset, boolean b) {
133+
return sb.insert(offset, b);
134+
}
135+
136+
public static StringBuffer insert(
137+
StringBuffer sb, int offset, char c) {
138+
return sb.insert(offset, c);
139+
}
140+
141+
public static StringBuffer insert(
142+
StringBuffer sb, int offset, int i) {
143+
return sb.insert(offset, i);
144+
}
145+
146+
public static StringBuffer insert(
147+
StringBuffer sb, int offset, long l) {
148+
return sb.insert(offset, l);
149+
}
29150
}

‎regression/jbmc-strings/java_delete/test_delete.class

56 Bytes
Binary file not shown.

‎regression/jbmc-strings/java_delete/test_delete.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ public class test_delete
33
public static void main(/*String[] argv*/)
44
{
55
StringBuilder s = new StringBuilder("Abc");
6-
s.delete(1,2);
6+
org.cprover.CProverString.delete(s,1,2);
77
String str = s.toString();
88
assert(!str.equals("Ac"));
99
}

‎regression/jbmc-strings/java_delete_char_at/test_delete_char_at.class

56 Bytes
Binary file not shown.

‎regression/jbmc-strings/java_delete_char_at/test_delete_char_at.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ public static void main(/*String[] argv*/)
44
{
55
StringBuilder s = new StringBuilder();
66
s.append("Abc");
7-
s.deleteCharAt(1);
7+
org.cprover.CProverString.deleteCharAt(s, 1);
88
String str = s.toString();
99
assert(!str.equals("Ac"));
1010
}

‎regression/jbmc-strings/java_insert_char/test_insert_char.class

56 Bytes
Binary file not shown.

‎regression/jbmc-strings/java_insert_char/test_insert_char.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ public class test_insert_char
33
public static void main(/*String[] argv*/)
44
{
55
StringBuilder sb = new StringBuilder("ac");
6-
sb.insert(1, 'b');
6+
org.cprover.CProverString.insert(sb, 1, 'b');
77
String s = sb.toString();
88
assert(!s.equals("abc"));
99
}

‎regression/jbmc-strings/java_insert_char_array/test.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ test_insert_char_array.class
33
--refine-strings --string-max-length 1000 --function test_insert_char_array.main
44
^EXIT=10$
55
^SIGNAL=0$
6-
assertion.* line 28.* SUCCESS$
7-
assertion.* line 30.* FAILURE$
6+
assertion.* line 26.* SUCCESS$
7+
assertion.* line 28.* FAILURE$
88
--

‎regression/jbmc-strings/java_insert_char_array/test_insert_char_array.class

56 Bytes
Binary file not shown.

‎regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ public static String stringOfCharArray(char arr[])
1111
public static void insert(StringBuilder sb, int pos, char arr[])
1212
{
1313
String s=stringOfCharArray(arr);
14-
sb.insert(pos, s);
14+
org.cprover.CProverString.insert(sb, pos, s);
1515
}
1616
public static void main(int i)
1717
{

‎regression/jbmc-strings/java_insert_int/test_insert_int.class

56 Bytes
Binary file not shown.

‎regression/jbmc-strings/java_insert_int/test_insert_int.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ public class test_insert_int
33
public static void main(/*String[] argv*/)
44
{
55
StringBuilder sb = new StringBuilder("ac");
6-
sb.insert(1, 42);
6+
org.cprover.CProverString.insert(sb, 1, 42);
77
String s = sb.toString();
88
assert(!s.equals("a42c"));
99
}

‎regression/jbmc-strings/java_insert_multiple/test_insert_multiple.class

81 Bytes
Binary file not shown.

‎regression/jbmc-strings/java_insert_multiple/test_insert_multiple.java

+2-2
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ public class test_insert_multiple
33
public static void main(/*String[] argv*/)
44
{
55
StringBuilder sb = new StringBuilder("ad");
6-
sb.insert(1, 'c');
7-
sb.insert(1, "b");
6+
org.cprover.CProverString.insert(sb, 1, 'c');
7+
org.cprover.CProverString.insert(sb, 1, "b");
88
String s = sb.toString();
99
assert(!s.equals("abcd"));
1010
}

‎regression/jbmc-strings/java_insert_string/test_insert_string.class

56 Bytes
Binary file not shown.

‎regression/jbmc-strings/java_insert_string/test_insert_string.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ public class test_insert_string
33
public static void main(/*String[] argv*/)
44
{
55
StringBuilder sb = new StringBuilder("ad");
6-
sb.insert(1, "bc");
6+
org.cprover.CProverString.insert(sb, 1, "bc");
77
String s = sb.toString();
88
assert(!s.equals("abcd"));
99
}

‎regression/strings-smoke-tests/cprover/CProverString.class

3.28 KB
Binary file not shown.

‎regression/strings-smoke-tests/cprover/CProverString.java

+121
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,29 @@ public static char charAt(String s, int i) {
88
return '\u0000';
99
}
1010

11+
public static int codePointAt(String s, int index) {
12+
return s.codePointAt(index);
13+
}
14+
15+
public static int codePointBefore(String s, int index) {
16+
return s.codePointBefore(index);
17+
}
18+
19+
public static int codePointCount(
20+
String s, int beginIndex, int endIndex) {
21+
return s.codePointCount(beginIndex, endIndex);
22+
}
23+
24+
public static int offsetByCodePoints(
25+
String s, int index, int codePointOffset) {
26+
return s.offsetByCodePoints(index, codePointOffset);
27+
}
28+
29+
public static CharSequence subSequence(
30+
String s, int beginIndex, int endIndex) {
31+
return s.subSequence(beginIndex, endIndex);
32+
}
33+
1134
public static String substring(String s, int i) {
1235
if (i <= 0)
1336
return s;
@@ -26,4 +49,102 @@ public static String substring(String s, int i, int j) {
2649
return "";
2750
return s.substring(i, j);
2851
}
52+
53+
public static StringBuilder append(
54+
StringBuilder sb, CharSequence cs, int i, int j) {
55+
return sb.append(cs, i, j);
56+
}
57+
58+
public static StringBuilder delete(StringBuilder sb, int start, int end) {
59+
return sb.delete(start, end);
60+
}
61+
62+
public static StringBuilder deleteCharAt(StringBuilder sb, int index) {
63+
return sb.deleteCharAt(index);
64+
}
65+
66+
public static StringBuilder insert(
67+
StringBuilder sb, int offset, String str) {
68+
return sb.insert(offset, str);
69+
}
70+
71+
public static StringBuilder insert(
72+
StringBuilder sb, int offset, boolean b) {
73+
return sb.insert(offset, b);
74+
}
75+
76+
public static StringBuilder insert(
77+
StringBuilder sb, int offset, char c) {
78+
return sb.insert(offset, c);
79+
}
80+
81+
public static StringBuilder insert(
82+
StringBuilder sb, int offset, int i) {
83+
return sb.insert(offset, i);
84+
}
85+
86+
public static StringBuilder insert(
87+
StringBuilder sb, int offset, long l) {
88+
return sb.insert(offset, l);
89+
}
90+
91+
public static StringBuilder insert(
92+
StringBuilder sb, int offset, float f) {
93+
return sb.insert(offset, f);
94+
}
95+
96+
public static StringBuilder insert(
97+
StringBuilder sb, int offset, double d) {
98+
return sb.insert(offset, d);
99+
}
100+
101+
public static void setLength(StringBuffer sb, int newLength) {
102+
sb.setLength(newLength);
103+
}
104+
105+
public static char charAt(StringBuffer sb, int index) {
106+
return sb.charAt(index);
107+
}
108+
109+
public static void setCharAt(StringBuffer sb, int index, char c) {
110+
sb.setCharAt(index, c);
111+
}
112+
113+
public static StringBuffer delete(
114+
StringBuffer sb, int start, int end) {
115+
return sb.delete(start, end);
116+
}
117+
118+
public static StringBuffer deleteCharAt(StringBuffer sb, int index) {
119+
return sb.deleteCharAt(index);
120+
}
121+
122+
public static String substring(StringBuffer sb, int start, int end) {
123+
return sb.substring(start, end);
124+
}
125+
126+
public static StringBuffer insert(
127+
StringBuffer sb, int offset, String str) {
128+
return sb.insert(offset, str);
129+
}
130+
131+
public static StringBuffer insert(
132+
StringBuffer sb, int offset, boolean b) {
133+
return sb.insert(offset, b);
134+
}
135+
136+
public static StringBuffer insert(
137+
StringBuffer sb, int offset, char c) {
138+
return sb.insert(offset, c);
139+
}
140+
141+
public static StringBuffer insert(
142+
StringBuffer sb, int offset, int i) {
143+
return sb.insert(offset, i);
144+
}
145+
146+
public static StringBuffer insert(
147+
StringBuffer sb, int offset, long l) {
148+
return sb.insert(offset, l);
149+
}
29150
}

‎regression/strings-smoke-tests/java_append_string/test_append_string.class

25 Bytes
Binary file not shown.

‎regression/strings-smoke-tests/java_append_string/test_append_string.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ public static void check(StringBuilder sb, String str)
1717
String init = sb.toString();
1818
if(str.length() >= 4)
1919
{
20-
sb.append(str, 2, 4);
20+
org.cprover.CProverString.append(sb, str, 2, 4);
2121
String res = sb.toString();
2222
assert(res.startsWith(init));
2323
assert(res.endsWith(org.cprover.CProverString.substring(str, 2, 4)));

‎regression/strings-smoke-tests/java_append_string/test_substring.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
test_append_string.class
3-
--refine-strings --verbosity 10 --string-max-length 10 --function test_append_string.check --java-assume-inputs-non-null
3+
--refine-strings --string-max-length 10 --function test_append_string.check --java-assume-inputs-non-null
44
^EXIT=10$
55
^SIGNAL=0$
66
^\[.*assertion.*\].* line 22.* SUCCESS$

‎regression/strings-smoke-tests/java_code_point/test_code_point.class

33 Bytes
Binary file not shown.

‎regression/strings-smoke-tests/java_code_point/test_code_point.java

+4-4
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ public class test_code_point
33
public static void main(/*String[] argv*/)
44
{
55
String s = "!𐤇𐤄𐤋𐤋𐤅";
6-
assert(s.codePointAt(1) == 67847);
7-
assert(s.codePointBefore(3) == 67847);
8-
assert(s.codePointCount(1,5) >= 2);
9-
assert(s.offsetByCodePoints(1,2) >= 3);
6+
assert(org.cprover.CProverString.codePointAt(s, 1) == 67847);
7+
assert(org.cprover.CProverString.codePointBefore(s, 3) == 67847);
8+
assert(org.cprover.CProverString.codePointCount(s,1,5) >= 2);
9+
assert(org.cprover.CProverString.offsetByCodePoints(s,1,2) >= 3);
1010
StringBuilder sb = new StringBuilder();
1111
sb.appendCodePoint(0x10907);
1212
assert(org.cprover.CProverString.charAt(s, 1) == org.cprover.CProverString.charAt(sb.toString(), 0));

‎regression/strings-smoke-tests/java_delete/test_delete.class

-87 Bytes
Binary file not shown.

‎regression/strings-smoke-tests/java_delete/test_delete.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ public class test_delete
33
public static void main(/*String[] argv*/)
44
{
55
StringBuilder s = new StringBuilder("Abc");
6-
s.delete(1,2);
6+
org.cprover.CProverString.delete(s,1,2);
77
String str = s.toString();
88
assert(str.equals("Ac"));
99
}

‎regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.class

56 Bytes
Binary file not shown.

‎regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ public static void main(/*String[] argv*/)
44
{
55
StringBuilder s = new StringBuilder();
66
s.append("Abc");
7-
s.deleteCharAt(1);
7+
org.cprover.CProverString.deleteCharAt(s, 1);
88
String str = s.toString();
99
assert(str.equals("Ac"));
1010
}

‎regression/strings-smoke-tests/java_insert_char/test_insert_char.class

56 Bytes
Binary file not shown.

‎regression/strings-smoke-tests/java_insert_char/test_insert_char.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ public class test_insert_char
33
public static void main(/*String[] argv*/)
44
{
55
StringBuilder sb = new StringBuilder("ac");
6-
sb.insert(1, 'b');
6+
org.cprover.CProverString.insert(sb, 1, 'b');
77
String s = sb.toString();
88
assert(s.equals("abc"));
99
}

‎regression/strings-smoke-tests/java_insert_char_array/test_insert_char_array.class

56 Bytes
Binary file not shown.

0 commit comments

Comments
 (0)