Skip to content

Commit 6366a4b

Browse files
mergify[bot]mergify[bot]
authored
Merge pull request #1290 from GaloisInc/bh-jvm
JVM write permissions
2 parents 6c6fa3c + ed814c8 commit 6366a4b

File tree

15 files changed

+436
-45
lines changed

15 files changed

+436
-45
lines changed

‎deps/crucible

‎examples/java/get.saw

+1-1
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ jvm_verify c "get" [] false
99
j <- jvm_fresh_var "j" java_int;
1010
jvm_precond {{ j <= 3 }};
1111
jvm_execute_func [this, a, jvm_term j];
12-
// TODO: Update spec to say `a` is modified but not specified
12+
jvm_modifies_array a;
1313
jvm_return (jvm_term {{ j }});
1414
}
1515
abc;

‎intTests/test_jvm_modifies/Makefile

+2
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
%.class: %.java
2+
javac -g $<

‎intTests/test_jvm_modifies/Test.class

920 Bytes
Binary file not shown.

‎intTests/test_jvm_modifies/Test.java

+31
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
class Test
2+
{
3+
int a;
4+
static int b;
5+
int[] c;
6+
7+
int add1 (int x, int y) {
8+
a = x;
9+
return x + y;
10+
}
11+
12+
int add2 (int x, int y) {
13+
b = x;
14+
return x + y;
15+
}
16+
17+
int add3 (int x, int y) {
18+
c[1] = x;
19+
return x + y;
20+
}
21+
22+
int wrap1 (int x, int y) {
23+
return add1 (x, y);
24+
}
25+
int wrap2 (int x, int y) {
26+
return add2 (x, y);
27+
}
28+
int wrap3 (int x, int y) {
29+
return add3 (x, y);
30+
}
31+
}

‎intTests/test_jvm_modifies/test.saw

+170
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,170 @@
1+
enable_experimental;
2+
c <- java_load_class "Test";
3+
4+
////////////////////////////////////////////////////////////////////////////////
5+
// Specs with missing side effects
6+
7+
print "Verification fails for add1 spec with missing side effect.";
8+
fails (
9+
jvm_verify c "add1" [] false
10+
do {
11+
this <- jvm_alloc_object "Test";
12+
x <- jvm_fresh_var "x" java_int;
13+
y <- jvm_fresh_var "y" java_int;
14+
jvm_execute_func [this, jvm_term x, jvm_term y];
15+
jvm_return (jvm_term {{ x + y }});
16+
} z3
17+
);
18+
19+
print "Verification fails for add2 spec with missing side effect.";
20+
fails (
21+
jvm_verify c "add2" [] false
22+
do {
23+
this <- jvm_alloc_object "Test";
24+
x <- jvm_fresh_var "x" java_int;
25+
y <- jvm_fresh_var "y" java_int;
26+
jvm_execute_func [this, jvm_term x, jvm_term y];
27+
jvm_return (jvm_term {{ x + y }});
28+
} z3
29+
);
30+
31+
print "Verification fails for add3 spec with missing side effect.";
32+
fails (
33+
jvm_verify c "add3" [] false
34+
do {
35+
this <- jvm_alloc_object "Test";
36+
arr <- jvm_alloc_array 2 java_int;
37+
jvm_field_is this "c" arr;
38+
x <- jvm_fresh_var "x" java_int;
39+
y <- jvm_fresh_var "y" java_int;
40+
jvm_execute_func [this, jvm_term x, jvm_term y];
41+
jvm_return (jvm_term {{ x + y }});
42+
} z3
43+
);
44+
45+
////////////////////////////////////////////////////////////////////////////////
46+
// Full specifications with side effects
47+
48+
let spec1 =
49+
do {
50+
this <- jvm_alloc_object "Test";
51+
x <- jvm_fresh_var "x" java_int;
52+
y <- jvm_fresh_var "y" java_int;
53+
jvm_execute_func [this, jvm_term x, jvm_term y];
54+
jvm_field_is this "a" (jvm_term x);
55+
jvm_return (jvm_term {{ x + y }});
56+
};
57+
58+
let spec2 =
59+
do {
60+
this <- jvm_alloc_object "Test";
61+
x <- jvm_fresh_var "x" java_int;
62+
y <- jvm_fresh_var "y" java_int;
63+
jvm_execute_func [this, jvm_term x, jvm_term y];
64+
jvm_static_field_is "b" (jvm_term x);
65+
jvm_return (jvm_term {{ x + y }});
66+
};
67+
68+
let spec3 =
69+
do {
70+
this <- jvm_alloc_object "Test";
71+
arr <- jvm_alloc_array 2 java_int;
72+
jvm_field_is this "c" arr;
73+
x <- jvm_fresh_var "x" java_int;
74+
y <- jvm_fresh_var "y" java_int;
75+
jvm_execute_func [this, jvm_term x, jvm_term y];
76+
jvm_elem_is arr 1 (jvm_term x);
77+
jvm_return (jvm_term {{ x + y }});
78+
};
79+
80+
print "Verification succeeds for complete add1 spec.";
81+
add1_full <- jvm_verify c "add1" [] false spec1 z3;
82+
83+
print "Verification succeeds for complete add2 spec.";
84+
add2_full <- jvm_verify c "add2" [] false spec2 z3;
85+
86+
print "Verification succeeds for complete add3 spec.";
87+
add3_full <- jvm_verify c "add3" [] false spec3 z3;
88+
89+
////////////////////////////////////////////////////////////////////////////////
90+
// Partial specifications with jvm_modifies
91+
92+
print "Verification succeeds for partial add1 spec (jvm_modifies_field).";
93+
add1_part <-
94+
jvm_verify c "add1" [] false
95+
do {
96+
this <- jvm_alloc_object "Test";
97+
x <- jvm_fresh_var "x" java_int;
98+
y <- jvm_fresh_var "y" java_int;
99+
jvm_execute_func [this, jvm_term x, jvm_term y];
100+
jvm_modifies_field this "a";
101+
jvm_return (jvm_term {{ x + y }});
102+
} z3;
103+
104+
print "Verification succeeds for partial add2 spec (jvm_modifies_static_field).";
105+
add2_part <-
106+
jvm_verify c "add2" [] false
107+
do {
108+
this <- jvm_alloc_object "Test";
109+
x <- jvm_fresh_var "x" java_int;
110+
y <- jvm_fresh_var "y" java_int;
111+
jvm_execute_func [this, jvm_term x, jvm_term y];
112+
jvm_modifies_static_field "b";
113+
jvm_return (jvm_term {{ x + y }});
114+
} z3;
115+
116+
print "Verification succeeds for partial add3 spec (jvm_modifies_elem).";
117+
add3_part <-
118+
jvm_verify c "add3" [] false
119+
do {
120+
this <- jvm_alloc_object "Test";
121+
arr <- jvm_alloc_array 2 java_int;
122+
jvm_field_is this "c" arr;
123+
x <- jvm_fresh_var "x" java_int;
124+
y <- jvm_fresh_var "y" java_int;
125+
jvm_execute_func [this, jvm_term x, jvm_term y];
126+
jvm_modifies_elem arr 1;
127+
jvm_return (jvm_term {{ x + y }});
128+
} z3;
129+
130+
print "Verification succeeds for partial add3 spec (jvm_modifies_array).";
131+
add3_part_a <-
132+
jvm_verify c "add3" [] false
133+
do {
134+
this <- jvm_alloc_object "Test";
135+
arr <- jvm_alloc_array 2 java_int;
136+
jvm_field_is this "c" arr;
137+
x <- jvm_fresh_var "x" java_int;
138+
y <- jvm_fresh_var "y" java_int;
139+
jvm_execute_func [this, jvm_term x, jvm_term y];
140+
jvm_modifies_array arr;
141+
jvm_return (jvm_term {{ x + y }});
142+
} z3;
143+
144+
////////////////////////////////////////////////////////////////////////////////
145+
// Compositional verification with full specs
146+
147+
print "Compositional verification succeeds with full add1 spec.";
148+
wrap1_full <- jvm_verify c "wrap1" [add1_full] false spec1 z3;
149+
150+
print "Compositional verification succeeds with full add1 spec.";
151+
wrap2_full <- jvm_verify c "wrap2" [add2_full] false spec2 z3;
152+
153+
print "Compositional verification succeeds with full add1 spec.";
154+
wrap3_full <- jvm_verify c "wrap3" [add3_full] false spec3 z3;
155+
156+
////////////////////////////////////////////////////////////////////////////////
157+
// Compositional verification with partial specs
158+
159+
// TODO: Improve misleading "Ill-formed value for type int" error message.
160+
161+
print "Compositional verification fails with partial add1 spec.";
162+
fails (jvm_verify c "wrap1" [add1_part] false spec1 z3);
163+
164+
print "Compositional verification fails with partial add2 spec.";
165+
fails (jvm_verify c "wrap2" [add2_part] false spec2 z3);
166+
167+
print "Compositional verification fails with partial add3 spec.";
168+
fails (jvm_verify c "wrap3" [add3_part] false spec3 z3);
169+
170+
print "DONE!";

‎intTests/test_jvm_modifies/test.sh

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
$SAW test.saw

‎intTests/test_jvm_setup_errors/Test.class

89 Bytes
Binary file not shown.

‎intTests/test_jvm_setup_errors/Test.java

+5
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
class Test
22
{
33
long val;
4+
static long counter;
45

56
long get () {
67
return val;
@@ -14,4 +15,8 @@ boolean lessThan (Test t) {
1415
static long lookup (long arr[], int idx) {
1516
return arr[idx];
1617
}
18+
static long next () {
19+
counter = counter + 1;
20+
return counter;
21+
}
1722
}

‎intTests/test_jvm_setup_errors/test.saw

+110
Original file line numberDiff line numberDiff line change
@@ -120,6 +120,94 @@ check_fails test "get"
120120
jvm_return (jvm_term val);
121121
};
122122

123+
print "jvm_modifies_field in pre-state section";
124+
check_fails test "get"
125+
do {
126+
this <- jvm_alloc_object "Test";
127+
val <- jvm_fresh_var "val" java_long;
128+
jvm_modifies_field this "val";
129+
jvm_execute_func [this];
130+
jvm_return (jvm_term val);
131+
};
132+
133+
print "Working spec for method 'next'";
134+
jvm_verify test "next" [] false
135+
do {
136+
ctr <- jvm_fresh_var "ctr" java_long;
137+
jvm_static_field_is "counter" (jvm_term ctr);
138+
jvm_execute_func [];
139+
let ctr' = {{ ctr + 1 }};
140+
jvm_static_field_is "counter" (jvm_term ctr');
141+
jvm_return (jvm_term ctr');
142+
} z3;
143+
144+
print "jvm_static_field_is with non-monomorphic type";
145+
check_fails test "next"
146+
do {
147+
let ctr = {{ 0 }};
148+
jvm_static_field_is "counter" (jvm_term ctr);
149+
jvm_execute_func [];
150+
let ctr' = {{ 1 }};
151+
jvm_static_field_is "counter" (jvm_term ctr');
152+
jvm_return (jvm_term ctr');
153+
};
154+
155+
print "jvm_static_field_is with non-jvm type";
156+
check_fails test "next"
157+
do {
158+
let ctr = {{ 0 : Integer }};
159+
jvm_static_field_is "counter" (jvm_term ctr);
160+
jvm_execute_func [];
161+
let ctr' = {{ ctr + 1 }};
162+
jvm_static_field_is "counter" (jvm_term ctr');
163+
jvm_return (jvm_term ctr');
164+
};
165+
166+
print "jvm_static_field_is with wrong type";
167+
check_fails test "next"
168+
do {
169+
let ctr = {{ 0 : [32] }};
170+
jvm_static_field_is "counter" (jvm_term ctr);
171+
jvm_execute_func [];
172+
let ctr' = {{ ctr + 1 }};
173+
jvm_static_field_is "counter" (jvm_term ctr');
174+
jvm_return (jvm_term ctr');
175+
};
176+
177+
print "jvm_static_field_is with non-existent field name";
178+
check_fails test "next"
179+
do {
180+
ctr <- jvm_fresh_var "ctr" java_long;
181+
jvm_static_field_is "count" (jvm_term ctr);
182+
jvm_execute_func [];
183+
let ctr' = {{ ctr + 1 }};
184+
jvm_static_field_is "count" (jvm_term ctr');
185+
jvm_return (jvm_term ctr');
186+
};
187+
188+
print "jvm_static_field_is with previous jvm_static_field_is on same field";
189+
check_fails test "next"
190+
do {
191+
ctr <- jvm_fresh_var "ctr" java_long;
192+
jvm_static_field_is "counter" (jvm_term ctr);
193+
jvm_static_field_is "counter" (jvm_term ctr);
194+
jvm_execute_func [];
195+
let ctr' = {{ ctr + 1 }};
196+
jvm_static_field_is "counter" (jvm_term ctr');
197+
jvm_return (jvm_term ctr');
198+
};
199+
200+
print "jvm_modifies_static_field in pre-state section";
201+
check_fails test "next"
202+
do {
203+
ctr <- jvm_fresh_var "ctr" java_long;
204+
jvm_modifies_static_field "counter";
205+
jvm_execute_func [];
206+
let ctr' = {{ ctr + 1 }};
207+
jvm_static_field_is "counter" (jvm_term ctr');
208+
jvm_return (jvm_term ctr');
209+
};
210+
123211
print "Working spec for method 'lookup'";
124212
jvm_verify test "lookup" [] false
125213
do {
@@ -233,6 +321,17 @@ check_fails test "lookup"
233321
jvm_return (jvm_term x);
234322
};
235323

324+
print "jvm_modifies_elem in pre-state section";
325+
check_fails test "lookup"
326+
do {
327+
arr <- jvm_alloc_array 8 java_long;
328+
let idx = {{ 2 : [32] }};
329+
x <- jvm_fresh_var "x" java_long;
330+
jvm_modifies_elem arr 2;
331+
jvm_execute_func [arr, jvm_term idx];
332+
jvm_return (jvm_term x);
333+
};
334+
236335
print "Working spec for method 'lookup' (jvm_array_is)";
237336
jvm_verify test "lookup" [] false
238337
do {
@@ -356,6 +455,17 @@ check_fails test "lookup"
356455
jvm_return (jvm_term {{ xs @ idx }});
357456
};
358457

458+
print "jvm_modifies_array in pre-state section";
459+
check_fails test "lookup"
460+
do {
461+
arr <- jvm_alloc_array 8 java_long;
462+
let idx = {{ 2 : [32] }};
463+
x <- jvm_fresh_var "x" java_long;
464+
jvm_modifies_array arr;
465+
jvm_execute_func [arr, jvm_term idx];
466+
jvm_return (jvm_term x);
467+
};
468+
359469
print "Working spec for method 'set'";
360470
jvm_verify test "set" [] false
361471
do {

‎intTests/test_jvm_unsound/test.saw

+3-2
Original file line numberDiff line numberDiff line change
@@ -86,5 +86,6 @@ jvm_verify c "test_b" [set_ov_2] false
8686
fails (jvm_verify c "set" [] false set_spec_1 z3);
8787

8888
// It should be impossible to verify the bogus set_spec_2.
89-
// FIXME: this should fail
90-
jvm_verify c "set" [] false set_spec_2 z3;
89+
fails (jvm_verify c "set" [] false set_spec_2 z3);
90+
91+
print "Done.";

0 commit comments

Comments
 (0)