1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
|
// RUN: rm -f %t4.out %t4.err %t4.log
// RUN: %llvmgcc %s -emit-llvm -O2 -c -o %t1.bc
// RUN: %llvmas -f ../_utils._ll -o %t2.bc
// RUN: %llvm-ld --optimize=false -link-as-library %t1.bc %t2.bc -o %t3.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --log-file %t4.log --debug-check-for-implied-values %t3.bc > %t4.out 2> %t4.err
// RUN: ls %t.klee-out | not grep .err
// RUN: not grep "(missed)" %t4.log
#include <assert.h>
#include "utils.h"
int main() {
unsigned char which;
volatile unsigned char a,b,c,d,e,f,g,h;
klee_make_symbolic(&which, sizeof which, "which");
klee_make_symbolic(&a, sizeof a, "a");
klee_make_symbolic(&b, sizeof b, "b");
klee_make_symbolic(&c, sizeof c, "c");
klee_make_symbolic(&d, sizeof d, "d");
klee_make_symbolic(&e, sizeof e, "e");
klee_make_symbolic(&f, sizeof f, "f");
klee_make_symbolic(&g, sizeof g, "g");
klee_make_symbolic(&h, sizeof h, "h");
switch (which) {
// RUN: grep "simple read(2) = value case" %t4.out
case 0:
if (a == 2) {
assert(!klee_is_symbolic(a));
printf("simple read(%d) = value case\n", a);
}
break;
// RUN: grep "select(0) has distinct constant result case (false)" %t4.out
case 1:
if (util_make_select(a, 12, 14) == 14) {
assert(!klee_is_symbolic(a));
printf("select(%d) has distinct constant result case (false)\n", a);
}
break;
// RUN: grep "select(0) has distinct constant result case (true)" %t4.out
case 2:
if (util_make_select(!a, 12, 14) == 12) {
assert(!klee_is_symbolic(a));
printf("select(%d) has distinct constant result case (true)\n", a);
}
break;
// RUN: grep "concat2(0xBE,0xEF) = value case" %t4.out
case 3:
if (util_make_concat2(a,b) == 0xBEEF) {
assert(!klee_is_symbolic(a));
assert(!klee_is_symbolic(b));
printf("concat2(0x%X,0x%X) = value case\n",
a, b);
}
break;
// RUN: grep "concat4(0xDE,0xAD,0xBE,0xEF) = value case" %t4.out
case 4:
if (util_make_concat4(a,b,c,d) == 0xDEADBEEF) {
assert(!klee_is_symbolic(a));
assert(!klee_is_symbolic(b));
assert(!klee_is_symbolic(c));
assert(!klee_is_symbolic(d));
printf("concat4(0x%X,0x%X,0x%X,0x%X) = value case\n",
a, b, c, d);
}
break;
// RUN: grep "concat8(0xDE,0xAD,0xBE,0xEF,0xAB,0xCD,0xAB,0xCD) = value case" %t4.out
case 5:
if (util_make_concat8(a,b,c,d,e,f,g,h) == 0xDEADBEEFABCDABCDLL) {
assert(!klee_is_symbolic(a));
assert(!klee_is_symbolic(b));
assert(!klee_is_symbolic(c));
assert(!klee_is_symbolic(d));
assert(!klee_is_symbolic(e));
assert(!klee_is_symbolic(f));
assert(!klee_is_symbolic(g));
assert(!klee_is_symbolic(h));
printf("concat8(0x%X,0x%X,0x%X,0x%X,0x%X,0x%X,0x%X,0x%X) = value case\n",
a, b, c, d, e, f, g, h);
}
break;
// RUN: grep "and(0,0) = true case" %t4.out
case 6:
if (util_make_and_i1(!a, !b)) {
assert(!klee_is_symbolic(a));
assert(!klee_is_symbolic(b));
printf("and(%d,%d) = true case\n", a, b);
}
break;
// RUN: grep "or(0,0) = false case" %t4.out
case 7:
if (!util_make_or_i1(a, b)) {
assert(!klee_is_symbolic(a));
assert(!klee_is_symbolic(b));
printf("or(%d,%d) = false case\n", a, b);
}
break;
// we use concat to prevent folding, will need to fix if that gets
// partial evaluated
// RUN: grep "add constant case: 0xDE" %t4.out
case 8:
if (util_make_concat2(a+0xCD,0xCD) == 0xABCD) {
assert(!klee_is_symbolic(a));
printf("add constant case: 0x%X\n", a);
}
break;
// RUN: grep "sub constant case: 0x60" %t4.out
case 9:
if (util_make_concat2(0x0B-a,0xCD) == 0xABCD) {
assert(!klee_is_symbolic(a));
printf("sub constant case: 0x%X\n", a);
}
break;
// RUN: grep "xor constant case: 0xA0" %t4.out
case 10:
if (util_make_concat2(0x0B ^ a,0xCD) == 0xABCD) {
assert(!klee_is_symbolic(a));
printf("xor constant case: 0x%X\n", a);
}
break;
// RUN: grep "sext constant case: 244" %t4.out
case 11:
if (! util_make_or_i1(((short) (signed char) a) + 12,b)) {
assert(!klee_is_symbolic(a));
printf("sext constant case: %d\n", a);
}
break;
default:
break;
}
return 0;
}
|
