Skip to content

Commit 0784f77

Browse files
smowtonsmowton
authored
Merge pull request #2125 from smowton/smowton/feature/symex-ignore-null-derefs
Symex: ignore null dereferences when targeting Java
2 parents 001fca0 + 9fd3434 commit 0784f77

File tree

20 files changed

+651
-13
lines changed

20 files changed

+651
-13
lines changed

‎jbmc/regression/jbmc/symex_should_exclude_null_pointers/test.class‎

776 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/symex_should_exclude_null_pointers/test.desc‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
test.class
3+
--function test.main
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
Null pointer check: FAILURE$
8+
assertion at file test\.java line 21 .*: SUCCESS$
9+
--
10+
^warning: ignoring
11+
--
12+
JBMC should reports failure, as it might dereference a null pointer, but as Java
13+
is a safe language we should statically determine that if we reach the assertion
14+
it cannot be violated.

‎jbmc/regression/jbmc/symex_should_exclude_null_pointers/test.java‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
public class test {
2+
3+
public int field;
4+
5+
public test(int value) {
6+
7+
field = value;
8+
9+
}
10+
11+
public static void main(boolean unknown) {
12+
13+
test t = new test(12345);
14+
test maybe_t = unknown ? null : t;
15+
16+
// t could still be null, but symex ought to notice that as the Java frontend introduces
17+
// checks before all pointer dereference operations, it can statically eliminate
18+
// the assertion below.
19+
20+
int field_value = maybe_t.field;
21+
assert field_value == 12345;
22+
23+
}
24+
25+
}

‎jbmc/regression/jbmc/symex_should_exclude_null_pointers/test_vccs.desc‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
test.class
3+
--show-vcc --function test.main
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
assertion at file test\.java line 22
9+
--
10+
Because symex should statically determine the assertion can't be violated there should not be a goal for it
11+
by the time --show-vccs prints the equation.

‎regression/cbmc/symex_should_exclude_null_pointers/main.c‎

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
static void noop() { }
2+
3+
int main(int argc, char **argv) {
4+
5+
int x;
6+
int *maybe_null = argc & 1 ? &x : 0;
7+
8+
// Should work (guarded by assume):
9+
int *ptr1 = maybe_null;
10+
__CPROVER_assume(ptr1 != 0);
11+
int deref1 = *ptr1;
12+
13+
// Should work (guarded by else):
14+
int *ptr2 = maybe_null;
15+
if(ptr2 == 0)
16+
{
17+
}
18+
else
19+
{
20+
int deref2 = *ptr2;
21+
}
22+
23+
// Should work (guarded by if):
24+
int *ptr3 = maybe_null;
25+
if(ptr3 != 0)
26+
{
27+
int deref3 = *ptr3;
28+
}
29+
30+
// Shouldn't work yet despite being safe (guarded by backward goto):
31+
int *ptr4 = maybe_null;
32+
goto check;
33+
34+
deref:
35+
int deref4 = *ptr4;
36+
goto end_test4;
37+
38+
check:
39+
__CPROVER_assume(ptr4 != 0);
40+
goto deref;
41+
42+
end_test4:
43+
44+
// Shouldn't work yet despite being safe (guarded by confluence):
45+
int *ptr5 = maybe_null;
46+
if(argc == 5)
47+
__CPROVER_assume(ptr5 != 0);
48+
else
49+
__CPROVER_assume(ptr5 != 0);
50+
int deref5 = *ptr5;
51+
52+
// Shouldn't work (unsafe as only guarded on one branch):
53+
int *ptr6 = maybe_null;
54+
if(argc == 6)
55+
__CPROVER_assume(ptr6 != 0);
56+
else
57+
{
58+
}
59+
int deref6 = *ptr6;
60+
61+
// Shouldn't work due to suspicion write to ptr6 might alter ptr7:
62+
int *ptr7 = maybe_null;
63+
__CPROVER_assume(ptr7 != 0);
64+
ptr6 = 0;
65+
int deref7 = *ptr7;
66+
67+
// Shouldn't work due to suspicion noop() call might alter ptr8:
68+
int *ptr8 = maybe_null;
69+
__CPROVER_assume(ptr8 != 0);
70+
noop();
71+
int deref8 = *ptr8;
72+
73+
assert(0);
74+
}

‎regression/cbmc/symex_should_exclude_null_pointers/test.desc‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE
2+
main.c
3+
--show-vcc
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
ptr4\$object
7+
ptr5\$object
8+
ptr6\$object
9+
ptr7\$object
10+
ptr8\$object
11+
--
12+
ptr[1-3]\$object
13+
^warning: ignoring
14+
--
15+
ptrX\$object appearing in the VCCs indicates symex was unsure whether the pointer had a valid
16+
target, and uses the $object symbol as a referred object of last resort. ptr1-3 should be judged
17+
not-null by symex, so their $object symbols do not occur.

‎regression/goto-instrument/safe-dereferences/main.c‎

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
static void noop() { }
2+
3+
int main(int argc, char **argv) {
4+
5+
int x;
6+
7+
// Should work (guarded by assume):
8+
int *ptr1 = &x;
9+
__CPROVER_assume(ptr1 != 0);
10+
int deref1 = *ptr1;
11+
12+
// Should work (guarded by else):
13+
int *ptr2 = &x;
14+
if(ptr2 == 0)
15+
{
16+
}
17+
else
18+
{
19+
int deref2 = *ptr2;
20+
}
21+
22+
// Should work (guarded by if):
23+
int *ptr3 = &x;
24+
if(ptr3 != 0)
25+
{
26+
int deref3 = *ptr3;
27+
}
28+
29+
// Shouldn't work yet despite being safe (guarded by backward goto):
30+
int *ptr4 = &x;
31+
goto check;
32+
33+
deref:
34+
int deref4 = *ptr4;
35+
goto end_test4;
36+
37+
check:
38+
__CPROVER_assume(ptr4 != 0);
39+
goto deref;
40+
41+
end_test4:
42+
43+
// Shouldn't work yet despite being safe (guarded by confluence):
44+
int *ptr5 = &x;
45+
if(argc == 5)
46+
__CPROVER_assume(ptr5 != 0);
47+
else
48+
__CPROVER_assume(ptr5 != 0);
49+
int deref5 = *ptr5;
50+
51+
// Shouldn't work (unsafe as only guarded on one branch):
52+
int *ptr6 = &x;
53+
if(argc == 6)
54+
__CPROVER_assume(ptr6 != 0);
55+
else
56+
{
57+
}
58+
int deref6 = *ptr6;
59+
60+
// Shouldn't work due to suspicion *ptr6 might alter ptr7:
61+
int *ptr7 = &x;
62+
__CPROVER_assume(ptr7 != 0);
63+
ptr6 = 0;
64+
int deref7 = *ptr7;
65+
66+
// Shouldn't work due to suspicion noop() call might alter ptr8:
67+
int *ptr8 = &x;
68+
__CPROVER_assume(ptr8 != 0);
69+
noop();
70+
int deref8 = *ptr8;
71+
}

‎regression/goto-instrument/safe-dereferences/test.desc‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
main.c
3+
--show-safe-dereferences
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
Safe \(known-not-null\) dereferences: \{main::[0-9]+::ptr1\}
7+
Safe \(known-not-null\) dereferences: \{main::[0-9]+::ptr2\}
8+
Safe \(known-not-null\) dereferences: \{main::[0-9]+::ptr3\}
9+
--
10+
Safe \(known-not-null\) dereferences: \{main::[0-9]+::ptr[4-8]\}
11+
^warning: ignoring
12+
--
13+
See comments in main.c for details about what each ptr variable is testing, and why they
14+
should or shouldn't be seen as safe accesses.

‎src/analyses/Makefile‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ SRC = ai.cpp \
2020
local_bitvector_analysis.cpp \
2121
local_cfg.cpp \
2222
local_may_alias.cpp \
23+
local_safe_pointers.cpp \
2324
locals.cpp \
2425
natural_loops.cpp \
2526
reaching_definitions.cpp \

0 commit comments

Comments
 (0)