Skip to content

Commit 6bb621a

Browse files
author
Owen
committed
Add tests for symex evaluating simple pointer comparisons
At time of writing, develop fails on the following lines of the test:
1 parent 15d83a9 commit 6bb621a

File tree

2 files changed

+239
-0
lines changed
  • regression/cbmc/symex_should_evaluate_simple_pointer_conditions

2 files changed

+239
-0
lines changed

‎regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.c

Lines changed: 188 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,188 @@
1+
#include <assert.h>
2+
3+
static void noop() { }
4+
5+
int test(int nondet_int) {
6+
int a = 1, b = 2, c = 3;
7+
int *ptr_to_a = &a, *ptr_to_b = &b, *ptr_to_c = &c, *ptr_to_null = 0;
8+
9+
// Symex knows the value of ptr_to_a, ptr_to_b, ptr_to_c and ptr_to_null, so
10+
// it should be able to evaluate simple conditions involving them.
11+
12+
// Equality "=="
13+
14+
// A non-null pointer and the correct value
15+
int unconditionally_reachable_1;
16+
if(ptr_to_a == &a)
17+
unconditionally_reachable_1 = 7;
18+
19+
// A non-null pointer and an incorrect value (not a null pointer)
20+
int unreachable_1;
21+
if(ptr_to_a == &c)
22+
unreachable_1 = 7;
23+
24+
// A non-null pointer and an incorrect value (a null pointer)
25+
int unreachable_2;
26+
if(ptr_to_a == 0)
27+
unreachable_2 = 7;
28+
29+
30+
// A null pointer and the correct value
31+
int unconditionally_reachable_2;
32+
if(ptr_to_null == 0)
33+
unconditionally_reachable_2 = 7;
34+
35+
// A null pointer and an incorrect value
36+
int unreachable_3;
37+
if(ptr_to_null == &a)
38+
unreachable_3 = 7;
39+
40+
41+
// Disequality "!="
42+
43+
// A non-null pointer and the correct value
44+
int unreachable_4;
45+
if(ptr_to_a != &a)
46+
unreachable_4 = 7;
47+
48+
// A non-null pointer and an incorrect value (not a null pointer)
49+
int unconditionally_reachable_3;
50+
if(ptr_to_a != &c)
51+
unconditionally_reachable_3 = 7;
52+
53+
// A non-null pointer and an incorrect value (a null pointer)
54+
int unconditionally_reachable_4;
55+
if(ptr_to_a != 0)
56+
unconditionally_reachable_4 = 7;
57+
58+
59+
// A null pointer and the correct value
60+
int unreachable_5;
61+
if(ptr_to_null != 0)
62+
unreachable_5 = 7;
63+
64+
// A null pointer and an incorrect value
65+
int unconditionally_reachable_5;
66+
if(ptr_to_null != &a)
67+
unconditionally_reachable_5 = 7;
68+
69+
70+
71+
72+
// Symex can't tell what ptr_to_a_or_b points to, but we can tell that it
73+
// doesn't point to some things
74+
int *ptr_to_a_or_b = nondet_int == 0 ? &a : &b;
75+
int *ptr_to_a_or_b_or_null = nondet_int == 0 ? &a : nondet_int == 1 ? &b : 0;
76+
77+
// Equality "=="
78+
79+
// A non-null pointer and a correct value
80+
int possibly_reachable_1;
81+
if(ptr_to_a_or_b == &a)
82+
possibly_reachable_1 = 7;
83+
84+
// A non-null pointer and an incorrect value (not a null pointer)
85+
int unreachable_6;
86+
if(ptr_to_a_or_b == &c)
87+
unreachable_6 = 7;
88+
89+
// A non-null pointer and an incorrect value (a null pointer)
90+
int unreachable_7;
91+
if(ptr_to_a_or_b == 0)
92+
unreachable_7 = 7;
93+
94+
95+
// A possibly-null pointer and a correct value (not a null pointer)
96+
int possibly_reachable_2;
97+
if(ptr_to_a_or_b_or_null == &a)
98+
possibly_reachable_2 = 7;
99+
100+
// A possibly-null pointer and a correct value (a null pointer)
101+
int possibly_reachable_3;
102+
if(ptr_to_a_or_b_or_null == 0)
103+
possibly_reachable_3 = 7;
104+
105+
// A possibly-null pointer and an incorrect value
106+
int unreachable_8;
107+
if(ptr_to_a_or_b_or_null == &c)
108+
unreachable_8 = 7;
109+
110+
111+
// Disequality "!="
112+
113+
// A non-null pointer and the correct value
114+
int possibly_reachable_4;
115+
if(ptr_to_a_or_b != &a)
116+
possibly_reachable_4 = 7;
117+
118+
// A non-null pointer and an incorrect value (not a null pointer)
119+
int unconditionally_reachable_6;
120+
if(ptr_to_a_or_b != &c)
121+
unconditionally_reachable_6 = 7;
122+
123+
// A non-null pointer and an incorrect value (a null pointer)
124+
int unconditionally_reachable_7;
125+
if(ptr_to_a_or_b != 0)
126+
unconditionally_reachable_7 = 7;
127+
128+
129+
// A possibly-null pointer and a correct value (not a null pointer)
130+
int possibly_reachable_5;
131+
if(ptr_to_a_or_b_or_null != &a)
132+
possibly_reachable_5 = 7;
133+
134+
// A possibly-null pointer and a correct value (a null pointer)
135+
int possibly_reachable_6;
136+
if(ptr_to_a_or_b_or_null != 0)
137+
possibly_reachable_6 = 7;
138+
139+
// A possibly-null pointer and an incorrect value
140+
int unconditionally_reachable_8;
141+
if(ptr_to_a_or_b_or_null != &c)
142+
unconditionally_reachable_8 = 7;
143+
144+
145+
// We should also be able to do all of the above in compound expressions which
146+
// use logical operators like AND, OR and NOT, or even ternary expressions.
147+
148+
int unconditionally_reachable_9;
149+
if(!(ptr_to_a == &c) && ptr_to_a_or_b != 0)
150+
unconditionally_reachable_9 = 7;
151+
152+
int unreachable_9;
153+
if(!(ptr_to_null == 0) || ptr_to_a_or_b == 0)
154+
unreachable_9 = 7;
155+
156+
int unconditionally_reachable_10;
157+
if((ptr_to_a == &a && !(ptr_to_a_or_b == 0)) || ptr_to_a_or_b_or_null == &c)
158+
unconditionally_reachable_10 = 7;
159+
160+
int unreachable_10;
161+
if(ptr_to_a_or_b_or_null != 0 ? ptr_to_null != 0 : ptr_to_a_or_b == &c)
162+
unreachable_10 = 7;
163+
164+
165+
// And everything should work with the symbol on the left or the right
166+
167+
int unconditionally_reachable_11;
168+
if(!(&c == ptr_to_a) && 0 != ptr_to_a_or_b)
169+
unconditionally_reachable_11 = 7;
170+
171+
int unreachable_11;
172+
if(!(0 == ptr_to_null) || 0 == ptr_to_a_or_b)
173+
unreachable_11 = 7;
174+
175+
int unconditionally_reachable_12;
176+
if((&a == ptr_to_a && !(0 == ptr_to_a_or_b)) || &c == ptr_to_a_or_b_or_null)
177+
unconditionally_reachable_12 = 7;
178+
179+
int unreachable_12;
180+
if(0 != ptr_to_a_or_b_or_null ? 0 != ptr_to_null : &c == ptr_to_a_or_b)
181+
unreachable_12 = 7;
182+
183+
int possibly_reachable_7;
184+
if(0 != ptr_to_a_or_b_or_null)
185+
possibly_reachable_7 = 7;
186+
187+
assert(0);
188+
}

‎regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
CORE
2+
test.c
3+
--function test --show-vcc
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
test::1::unconditionally_reachable_1[^\s]+ = 7$
7+
test::1::unconditionally_reachable_2[^\s]+ = 7$
8+
test::1::unconditionally_reachable_3[^\s]+ = 7$
9+
test::1::unconditionally_reachable_4[^\s]+ = 7$
10+
test::1::unconditionally_reachable_5[^\s]+ = 7$
11+
test::1::unconditionally_reachable_6[^\s]+ = 7$
12+
test::1::unconditionally_reachable_7[^\s]+ = 7$
13+
test::1::unconditionally_reachable_8[^\s]+ = 7$
14+
test::1::unconditionally_reachable_9[^\s]+ = 7$
15+
test::1::unconditionally_reachable_10[^\s]+ = 7$
16+
test::1::possibly_reachable_1[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_1[^\s]+\)$
17+
test::1::possibly_reachable_2[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_2[^\s]+\)$
18+
test::1::possibly_reachable_3[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_3[^\s]+\)$
19+
test::1::possibly_reachable_4[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_4[^\s]+\)$
20+
test::1::possibly_reachable_5[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_5[^\s]+\)$
21+
test::1::possibly_reachable_6[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_6[^\s]+\)$
22+
test::1::possibly_reachable_7[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_7[^\s]+\)$
23+
--
24+
test::1::unconditionally_reachable_1[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_1[^\s]+\)$
25+
test::1::unconditionally_reachable_2[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_2[^\s]+\)$
26+
test::1::unconditionally_reachable_3[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_3[^\s]+\)$
27+
test::1::unconditionally_reachable_4[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_4[^\s]+\)$
28+
test::1::unconditionally_reachable_5[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_5[^\s]+\)$
29+
test::1::unconditionally_reachable_6[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_6[^\s]+\)$
30+
test::1::unconditionally_reachable_7[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_7[^\s]+\)$
31+
test::1::unconditionally_reachable_8[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_8[^\s]+\)$
32+
test::1::unconditionally_reachable_9[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_9[^\s]+\)$
33+
test::1::unconditionally_reachable_10[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_10[^\s]+\)$
34+
test::1::unconditionally_reachable_11[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_11[^\s]+\)$
35+
test::1::unconditionally_reachable_12[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_12[^\s]+\)$
36+
test::1::unreachable_1[^\s]+ = 7$
37+
test::1::unreachable_2[^\s]+ = 7$
38+
test::1::unreachable_3[^\s]+ = 7$
39+
test::1::unreachable_4[^\s]+ = 7$
40+
test::1::unreachable_5[^\s]+ = 7$
41+
test::1::unreachable_6[^\s]+ = 7$
42+
test::1::unreachable_7[^\s]+ = 7$
43+
test::1::unreachable_8[^\s]+ = 7$
44+
test::1::unreachable_9[^\s]+ = 7$
45+
test::1::unreachable_10[^\s]+ = 7$
46+
test::1::unreachable_11[^\s]+ = 7$
47+
test::1::unreachable_12[^\s]+ = 7$
48+
^warning: ignoring
49+
--
50+
Pointer comparisons will be resolved in symex by a mixture of constant
51+
propagation and value-set filtering in try_evaluate_pointer_comparisons

0 commit comments

Comments
 (0)