Skip to content

Commit 461b3a5

Browse files
romainbrenguierromainbrenguier
authored
Merge pull request #1922 from romainbrenguier/dependency-graph/get-model#TG-2607
Use string dependencies in the get method of the solver [TG-2607]
2 parents 05a3426 + 1a874b3 commit 461b3a5

19 files changed

+919
-151
lines changed

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

5.12 KB
Binary file not shown.

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

+315
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,315 @@
1+
public class Test {
2+
3+
public String stringDet() {
4+
String s = "a";
5+
s += "b";
6+
s += "c";
7+
s += "d";
8+
s += "e";
9+
s += "f";
10+
s += "g";
11+
s += "h";
12+
s += "i";
13+
s += "j";
14+
s += "k";
15+
s += "l";
16+
s += "m";
17+
18+
assert(false);
19+
return s;
20+
}
21+
22+
public String stringNonDet(String arg) {
23+
String s = arg;
24+
s += "b";
25+
s += "c";
26+
s += "d";
27+
s += "e";
28+
s += "f";
29+
s += arg;
30+
s += "h";
31+
s += "i";
32+
s += "j";
33+
s += "k";
34+
s += "l";
35+
s += arg;
36+
37+
assert(false);
38+
return s;
39+
}
40+
41+
public String bufferDet() {
42+
StringBuffer s = new StringBuffer();
43+
s.append("a");
44+
s.append("b");
45+
s.append("c");
46+
s.append("d");
47+
s.append("e");
48+
49+
s.append("a");
50+
s.append("b");
51+
s.append("c");
52+
s.append("d");
53+
s.append("e");
54+
55+
s.append("a");
56+
s.append("b");
57+
s.append("c");
58+
s.append("d");
59+
s.append("e");
60+
61+
s.append("a");
62+
s.append("b");
63+
s.append("c");
64+
s.append("d");
65+
s.append("e");
66+
67+
s.append("a");
68+
s.append("b");
69+
s.append("c");
70+
s.append("d");
71+
s.append("e");
72+
73+
s.append("a");
74+
s.append("b");
75+
assert(false);
76+
return s.toString();
77+
}
78+
79+
public String charBufferDet() {
80+
StringBuffer s = new StringBuffer();
81+
s.append('a');
82+
s.append('b');
83+
s.append('c');
84+
s.append('d');
85+
s.append('e');
86+
87+
s.append('a');
88+
s.append('b');
89+
s.append('c');
90+
s.append('d');
91+
s.append('e');
92+
93+
s.append('a');
94+
s.append('b');
95+
s.append('c');
96+
s.append('d');
97+
s.append('e');
98+
99+
s.append('a');
100+
s.append('b');
101+
s.append('c');
102+
s.append('d');
103+
s.append('e');
104+
105+
s.append('a');
106+
s.append('b');
107+
s.append('c');
108+
s.append('d');
109+
s.append('e');
110+
111+
s.append('a');
112+
s.append('b');
113+
114+
assert(false);
115+
return s.toString();
116+
}
117+
118+
public String charBufferDetLoop(int width) {
119+
if(width <= 5)
120+
return "";
121+
StringBuffer sb = new StringBuffer();
122+
sb.append('+');
123+
for(int i=1; i < width-1; ++i)
124+
sb.append('-');
125+
sb.append('+');
126+
sb.append('\n');
127+
sb.append('|');
128+
129+
sb.append(' ');
130+
sb.append('c');
131+
int padding = width - 2;
132+
while(padding-- > 0)
133+
sb.append(' ');
134+
135+
sb.append(' ');
136+
sb.append('|');
137+
sb.append('\n');
138+
assert(false);
139+
return sb.toString();
140+
}
141+
142+
public String charBufferDetLoop2(int width, int height) {
143+
if(width <= 0 || height <= 0)
144+
return "";
145+
StringBuffer sb = new StringBuffer();
146+
sb.append('+');
147+
for(int i=1; i < width-1; ++i)
148+
sb.append('-');
149+
sb.append('+');
150+
sb.append('\n');
151+
sb.append('|');
152+
153+
sb.append(' ');
154+
sb.append('c');
155+
int padding = width - 2;
156+
while(padding-- > 0)
157+
sb.append(' ');
158+
sb.append(' ');
159+
sb.append('|');
160+
sb.append('\n');
161+
162+
sb.append('+');
163+
for(int i=1; i<width; ++i)
164+
sb.append('-');
165+
sb.append('+');
166+
sb.append('\n');
167+
168+
for(int i = 0; i < height; ++i) {
169+
sb.append('|');
170+
sb.append(' ');
171+
sb.append('d');
172+
padding = width - 3;
173+
while(padding-- > 0)
174+
sb.append(' ');
175+
sb.append(' ');
176+
sb.append('|');
177+
sb.append('\n');
178+
}
179+
180+
sb.append('+');
181+
for(int i=1; i<width-1; ++i)
182+
sb.append('-');
183+
sb.append('+');
184+
sb.append('\n');
185+
186+
assert(false);
187+
return sb.toString();
188+
}
189+
190+
public String bufferNonDetLoop(int width, String s) {
191+
if(width <= 5 || s.length() >= width || s.length() == 0)
192+
return "";
193+
StringBuffer sb = new StringBuffer();
194+
sb.append('+');
195+
for(int i=1; i < width-1; ++i)
196+
sb.append('-');
197+
sb.append('+');
198+
sb.append('\n');
199+
sb.append('|');
200+
201+
sb.append(' ');
202+
sb.append(s);
203+
int padding = width - s.length();
204+
while(padding-- > 0)
205+
sb.append(' ');
206+
sb.append(' ');
207+
sb.append('|');
208+
sb.append('\n');
209+
210+
assert(false);
211+
return sb.toString();
212+
}
213+
214+
public String bufferNonDetLoop2(int width, String c) {
215+
if(width < 5 || c.length() > width)
216+
return "";
217+
218+
StringBuffer sb = new StringBuffer();
219+
sb.append('+');
220+
221+
for(int i=1; i<width-1; ++i)
222+
sb.append('-');
223+
sb.append('+');
224+
sb.append('\n');
225+
sb.append('|');
226+
for(int i = 0; i < width; ++i) {
227+
sb.append(' ');
228+
sb.append(c);
229+
int padding = width - c.length();
230+
while(padding-- > 0)
231+
sb.append(' ');
232+
sb.append(' ');
233+
sb.append('|');
234+
}
235+
sb.append('\n');
236+
237+
assert(false);
238+
return sb.toString();
239+
}
240+
241+
public String bufferNonDetLoop3(int cols, int columnWidth, String c) {
242+
StringBuffer sb = new StringBuffer();
243+
sb.append('-');
244+
for(int i = 0; i < cols; ++i)
245+
sb.append(c);
246+
247+
assert(false);
248+
return sb.toString();
249+
}
250+
public String bufferNonDetLoop4(int cols, int columnWidth, String c) {
251+
StringBuffer sb = new StringBuffer();
252+
for(int i=1; i < columnWidth-1; ++i)
253+
sb.append('-');
254+
for(int i = 0; i < cols; ++i) {
255+
sb.append(c);
256+
}
257+
258+
assert(false);
259+
return sb.toString();
260+
}
261+
262+
public String bufferNonDetLoop5(int cols, int columnWidth, String c, String data[]) {
263+
if(cols<1)
264+
return "";
265+
266+
StringBuffer sb = new StringBuffer();
267+
sb.append('+');
268+
int totalWidth = columnWidth * cols;
269+
for(int i=1; i<totalWidth-1; ++i)
270+
sb.append('-');
271+
sb.append('+');
272+
sb.append('\n');
273+
sb.append('|');
274+
for(int i = 0; i < cols; ++i) {
275+
sb.append(' ');
276+
sb.append(c);
277+
int padding = columnWidth - c.length();
278+
while(padding-- > 0)
279+
sb.append(' ');
280+
sb.append(' ');
281+
sb.append('|');
282+
}
283+
sb.append('\n');
284+
285+
sb.append('+');
286+
for(int i=1; i<totalWidth-1; ++i)
287+
sb.append('-');
288+
sb.append('+');
289+
sb.append('\n');
290+
291+
for(int i = 0; i < data.length; ++i) {
292+
sb.append('|');
293+
String d = data[i];
294+
sb.append(' ');
295+
sb.append(d);
296+
int padding = columnWidth - d.length();
297+
while(padding-- > 0)
298+
sb.append(' ');
299+
sb.append(' ');
300+
sb.append('|');
301+
302+
if(i % cols == 0)
303+
sb.append('\n');
304+
}
305+
306+
sb.append('+');
307+
for(int i=1; i<totalWidth-1; ++i)
308+
sb.append('-');
309+
sb.append('+');
310+
sb.append('\n');
311+
312+
assert(false);
313+
return sb.toString();
314+
}
315+
}

‎regression/jbmc-strings/StringConcat/test_buffer_det.desc

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
Test.class
3+
--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferDet --depth 10000 --verbosity 10
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
check_SAT: got SAT but the model is not correct
9+
--
10+
Using the string dependences information to compute the model, refinement
11+
should not be needed when the execution is deterministic.

‎regression/jbmc-strings/StringConcat/test_buffer_nondet_loop.desc

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
FUTURE
2+
Test.class
3+
--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop --depth 10000 --unwind 5 --verbosity 10 --property "java::Test.bufferNonDetLoop:(ILjava/lang/String;)Ljava/lang/String;.assertion.1"
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
check_SAT: got SAT but the model is not correct
9+
--
10+
Using the string dependences information to compute the model, refinement
11+
should not be needed when the execution is deterministic.
12+
13+
This test seems to fail with AppVeyor, we should make sure it works
14+
once TG-2608 is done.

‎regression/jbmc-strings/StringConcat/test_buffer_nondet_loop2.desc

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
FUTURE
2+
Test.class
3+
--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop2 --depth 10000 --unwind 5 --verbosity 10
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
check_SAT: got SAT but the model is not correct
9+
--
10+
Using the string dependences information to compute the model, refinement
11+
should not be needed when the execution is deterministic.

‎regression/jbmc-strings/StringConcat/test_buffer_nondet_loop3.desc

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
Test.class
3+
--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop3 --depth 10000 --unwind 5 --verbosity 10
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
check_SAT: got SAT but the model is not correct
9+
--
10+
Using the string dependences information to compute the model, refinement
11+
should not be needed when the execution is deterministic.

‎regression/jbmc-strings/StringConcat/test_buffer_nondet_loop4.desc

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
FUTURE
2+
Test.class
3+
--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop4 --depth 10000 --unwind 5 --verbosity 10 --property "java::Test.bufferNonDetLoop4:(IILjava/lang/String;)Ljava/lang/String;.assertion.1"
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
check_SAT: got SAT but the model is not correct
9+
--
10+
Using the string dependences information to compute the model, refinement
11+
should not be needed when the execution is deterministic.
12+
13+
This test seems to fail with AppVeyor, we should make sure it works
14+
once TG-2608 is done.

‎regression/jbmc-strings/StringConcat/test_buffer_nondet_loop5.desc

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
FUTURE
2+
Test.class
3+
--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop5 --depth 10000 --unwind 5 --verbosity 10
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
check_SAT: got SAT but the model is not correct
9+
--
10+
Using the string dependences information to compute the model, refinement
11+
should not be needed when the execution is deterministic.

0 commit comments

Comments
 (0)