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
|
// RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --write-no-tests --output-dir=%t.klee-out %t.bc 2> %t.log
// RUN: %klee-stats --print-columns 'BrConditional,BrIndirect,BrSwitch,BrCall,BrMemOp,BrResolvePointer,BrAlloc,BrRealloc,BrFree,BrGetVal' --table-format=csv %t.klee-out > %t.stats
// RUN: FileCheck -check-prefix=CHECK-STATS -input-file=%t.stats %s
#include "klee/klee.h"
#include <stdlib.h>
void foo(void) {}
void bar(void) {}
int memop(void) {
int *p;
klee_make_symbolic(&p, sizeof(p), "p");
return *p;
}
int main(void) {
// alloc
size_t size0;
klee_make_symbolic(&size0, sizeof(size_t), "size0");
klee_assume(size0 < 10);
void *p;
// realloc
size_t size1;
klee_make_symbolic(&size1, sizeof(size_t), "size1");
klee_assume(size1 < 20);
// conditional
int cond;
klee_make_symbolic(&cond, sizeof(cond), "cond");
// switch
int sw_cond;
klee_make_symbolic(&sw_cond, sizeof(sw_cond), "sw_cond");
// call
void (*fptr)(void);
klee_make_symbolic(&fptr, sizeof(fptr), "fptr");
klee_assume((fptr == &foo) | (fptr == &bar));
// indirectbr
void *lptr;
klee_make_symbolic(&lptr, sizeof(lptr), "lptr");
klee_assume((lptr == &&one) | (lptr == &&two));
goto *lptr;
one:
p = malloc(size0);
if (p) {
p = realloc(p, size1);
if (p) {
// free
klee_make_symbolic(&p, sizeof(p), "p");
free(p);
}
}
return 1;
two:
switch (sw_cond) {
case 8: memop(); break; // memop
case 15: (*fptr)(); break;
default: {
int c = 42;
// conditional
if (cond) c++;
return c;
}
}
return 2;
}
// Check that we create branches
// CHECK-STATS: BrConditional,BrIndirect,BrSwitch,BrCall,BrMemOp,BrResolvePointer,BrAlloc,BrRealloc,BrFree,BrGetVal
// CHECK-STATS: 1,1,2,1,{{[1-9][0-9]*}},{{[1-9][0-9]*}},2,1,1,0
|
