Skip to content

Commit 54a9369

Browse files
Owensmowton
Owen
authored and
smowton
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 9c516d7 commit 54a9369

File tree

2 files changed

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

2 files changed

+241
-0
lines changed

‎regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.c

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

‎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)