Skip to content

Commit 6667118

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: test::1::unconditionally_reachable_1[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_1[^\s]+\)$ [FAILED] test::1::unconditionally_reachable_6[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_6[^\s]+\)$ [FAILED] test::1::unconditionally_reachable_7[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_7[^\s]+\)$ [FAILED] test::1::unconditionally_reachable_8[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_8[^\s]+\)$ [FAILED] test::1::unconditionally_reachable_9[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_9[^\s]+\)$ [FAILED] test::1::unconditionally_reachable_10[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_10[^\s]+\)$ [FAILED] test::1::unconditionally_reachable_11[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_11[^\s]+\)$ [FAILED] test::1::unconditionally_reachable_12[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_12[^\s]+\)$ [FAILED] test::1::unreachable_1[^\s]+ = 7$ [FAILED] test::1::unreachable_6[^\s]+ = 7$ [FAILED] test::1::unreachable_7[^\s]+ = 7$ [FAILED] test::1::unreachable_8[^\s]+ = 7$ [FAILED] test::1::unreachable_9[^\s]+ = 7$ [FAILED] test::1::unreachable_10[^\s]+ = 7$ [FAILED] test::1::unreachable_11[^\s]+ = 7$ [FAILED] test::1::unreachable_12[^\s]+ = 7$ [FAILED]
1 parent e3872ea commit 6667118

File tree

2 files changed

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

2 files changed

+249
-0
lines changed

‎regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.c

Lines changed: 189 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,189 @@
1+
#include <assert.h>
2+
3+
static void noop() { }
4+
5+
int test(int nondet_int_array[]) {
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 a matching value
15+
int unconditionally_reachable_1;
16+
if(ptr_to_a == &a)
17+
unconditionally_reachable_1 = 7;
18+
19+
// A non-null pointer and a non-matching 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 a non-matching 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 a matching value
31+
int unconditionally_reachable_2;
32+
if(ptr_to_null == 0)
33+
unconditionally_reachable_2 = 7;
34+
35+
// A null pointer and a non-matching 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 a matching value
44+
int unreachable_4;
45+
if(ptr_to_a != &a)
46+
unreachable_4 = 7;
47+
48+
// A non-null pointer and a non-matching 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 a non-matching 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 a matching value
60+
int unreachable_5;
61+
if(ptr_to_null != 0)
62+
unreachable_5 = 7;
63+
64+
// A null pointer and a non-matching 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_array[0] == 0 ? &a : &b;
75+
int *ptr_to_a_or_b_or_null =
76+
nondet_int_array[1] == 0 ? &a : nondet_int_array[1] == 1 ? &b : 0;
77+
78+
// Equality "=="
79+
80+
// A non-null pointer and a matching value
81+
int possibly_reachable_1;
82+
if(ptr_to_a_or_b == &a)
83+
possibly_reachable_1 = 7;
84+
85+
// A non-null pointer and a non-matching value (not a null pointer)
86+
int unreachable_6;
87+
if(ptr_to_a_or_b == &c)
88+
unreachable_6 = 7;
89+
90+
// A non-null pointer and a non-matching value (a null pointer)
91+
int unreachable_7;
92+
if(ptr_to_a_or_b == 0)
93+
unreachable_7 = 7;
94+
95+
96+
// A possibly-null pointer and a matching value (not a null pointer)
97+
int possibly_reachable_2;
98+
if(ptr_to_a_or_b_or_null == &a)
99+
possibly_reachable_2 = 7;
100+
101+
// A possibly-null pointer and a matching value (a null pointer)
102+
int possibly_reachable_3;
103+
if(ptr_to_a_or_b_or_null == 0)
104+
possibly_reachable_3 = 7;
105+
106+
// A possibly-null pointer and a non-matching value
107+
int unreachable_8;
108+
if(ptr_to_a_or_b_or_null == &c)
109+
unreachable_8 = 7;
110+
111+
112+
// Disequality "!="
113+
114+
// A non-null pointer and a matching value
115+
int possibly_reachable_4;
116+
if(ptr_to_a_or_b != &a)
117+
possibly_reachable_4 = 7;
118+
119+
// A non-null pointer and a non-matching value (not a null pointer)
120+
int unconditionally_reachable_6;
121+
if(ptr_to_a_or_b != &c)
122+
unconditionally_reachable_6 = 7;
123+
124+
// A non-null pointer and a non-matching value (a null pointer)
125+
int unconditionally_reachable_7;
126+
if(ptr_to_a_or_b != 0)
127+
unconditionally_reachable_7 = 7;
128+
129+
130+
// A possibly-null pointer and a matching value (not a null pointer)
131+
int possibly_reachable_5;
132+
if(ptr_to_a_or_b_or_null != &a)
133+
possibly_reachable_5 = 7;
134+
135+
// A possibly-null pointer and a matching value (a null pointer)
136+
int possibly_reachable_6;
137+
if(ptr_to_a_or_b_or_null != 0)
138+
possibly_reachable_6 = 7;
139+
140+
// A possibly-null pointer and a non-matching value
141+
int unconditionally_reachable_8;
142+
if(ptr_to_a_or_b_or_null != &c)
143+
unconditionally_reachable_8 = 7;
144+
145+
146+
// We should also be able to do all of the above in compound expressions which
147+
// use logical operators like AND, OR and NOT, or even ternary expressions.
148+
149+
int unconditionally_reachable_9;
150+
if(!(ptr_to_a == &c) && ptr_to_a_or_b != 0)
151+
unconditionally_reachable_9 = 7;
152+
153+
int unreachable_9;
154+
if(!(ptr_to_null == 0) || ptr_to_a_or_b == 0)
155+
unreachable_9 = 7;
156+
157+
int unconditionally_reachable_10;
158+
if((ptr_to_a == &a && !(ptr_to_a_or_b == 0)) || ptr_to_a_or_b_or_null == &c)
159+
unconditionally_reachable_10 = 7;
160+
161+
int unreachable_10;
162+
if(ptr_to_a_or_b_or_null != 0 ? ptr_to_null != 0 : ptr_to_a_or_b == &c)
163+
unreachable_10 = 7;
164+
165+
166+
// And everything should work with the symbol on the left or the right
167+
168+
int unconditionally_reachable_11;
169+
if(!(&c == ptr_to_a) && 0 != ptr_to_a_or_b)
170+
unconditionally_reachable_11 = 7;
171+
172+
int unreachable_11;
173+
if(!(0 == ptr_to_null) || 0 == ptr_to_a_or_b)
174+
unreachable_11 = 7;
175+
176+
int unconditionally_reachable_12;
177+
if((&a == ptr_to_a && !(0 == ptr_to_a_or_b)) || &c == ptr_to_a_or_b_or_null)
178+
unconditionally_reachable_12 = 7;
179+
180+
int unreachable_12;
181+
if(0 != ptr_to_a_or_b_or_null ? 0 != ptr_to_null : &c == ptr_to_a_or_b)
182+
unreachable_12 = 7;
183+
184+
int possibly_reachable_7;
185+
if(0 != ptr_to_a_or_b_or_null)
186+
possibly_reachable_7 = 7;
187+
188+
assert(0);
189+
}

‎regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc

Lines changed: 60 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
CORE paths-lifo-expected-failure
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+
unreachable_1[3-9]
50+
unreachable[2-9][0-9]
51+
unconditionally_reachable_1[3-9]
52+
unconditionally_reachable[2-9][0-9]
53+
possibly_reachable_[8-9]
54+
possibly_reachable_[1-9][0-9]
55+
--
56+
Pointer comparisons will be resolved in symex by a mixture of constant
57+
propagation and value-set filtering in try_evaluate_pointer_comparisons.
58+
59+
The expected failure for path-symex is because the lines we check for
60+
possibly_reachable_* would only appear when there is convergence behaviour.

0 commit comments

Comments
 (0)