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
149
150
151
152
153
154
155
156
157
158
159
160
|
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN"
"http://www.w3.org/TR/html4/strict.dtd">
<!-- Material used from: HTML 4.01 specs: http://www.w3.org/TR/html401/ -->
<html>
<head>
<META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
<title>The KLEE Symbolic Virtual Machine</title>
<link type="text/css" rel="stylesheet" href="menu.css">
<link type="text/css" rel="stylesheet" href="content.css">
</head>
<body>
<!--#include virtual="menu.html.incl"-->
<div id="content">
<!--*********************************************************************-->
<h1>Tutorial One: Testing a Small Function</h1>
<!--*********************************************************************-->
<h2>The demo code</h2>
This tutorial walks you through the main steps needed to test a
simple function with KLEE. Here is our simple function:
<pre class="code">
int my_islower(int x) {
if (x >= 'a' && x <= 'z')
return 1;
else return 0;
} </pre>
<h2>Marking input as symbolic</h2>
In order to test this function with KLEE, we need to run it
on <i>symbolic</i> input. To mark a variable as symbolic, we use
the <tt>klee_make_symbolic()</tt> function, which takes three
arguments: the address of the variable (memory location) that we
want to treat as symbolic, its size, and a name (which can be
anything). Here is a simple <tt>main()</tt> function that marks a
variable <tt>c</tt> as symbolic and uses it to
call <tt>my_islower()</tt>:
<pre class="code">
int main() {
char c;
klee_make_symbolic(&c, sizeof(c), "input");
return my_islower(c);
} </pre>
<h2>Compiling to LLVM bitcode</h2>
KLEE operates on LLVM bitcode. To run a program with KLEE, you
first compile it to LLVM bitcode using <tt>llvm-gcc
--emit-llvm</tt>. Assuming our code is stored in <tt>demo.c</tt>,
we run:
<div class="instr">
llvm-gcc --emit-llvm -c -g demo.c
</div>
to generate the LLVM bitcode file <tt>demo.o</tt>.
It is useful to (1) build with <tt>-g</tt> to add debug information
to the bitcode file, which we use to generate source line level
statistics information, and (2) not use any optimization flags. The
code can be optimized later, as KLEE provides the
<tt>--optimize</tt> command line option to run the optimizer
internally.
<h2>Running KLEE</h2>
To run KLEE on the bitcode file simply execute:
<div class="instr">
klee demo.o
</div>
You should see the following output:
<pre class="output">
KLEE: output directory = "klee-out-0"
KLEE: done: total instructions = 69
KLEE: done: completed paths = 3
KLEE: done: generated tests = 3 </pre>
There are three paths through our simple function, one
where <tt>x</tt> is less than <tt>'a'</tt>, one where <tt>x</tt> is
between <tt>'a'</tt> and <tt>'z'</tt> (so it's a lowercase letter),
and one where <tt>x</tt> is greater than <tt>'z'</tt>.
As expected, KLEE informs us that it explored three paths in the
program and generated one test case for each path explored. The
output of a KLEE execution is a directory (in our
case <tt>klee-out-0</tt>) containing the test cases generated by
KLEE. KLEE names the output directory <tt>klee-out-N</tt> where N
is the lowest available number (so if we run KLEE again it will
create a directory called <tt>klee-out-1</tt>), and also generates a
symbolic link called <tt>klee-last</tt> to this directory for
convenience:
<pre class="output">
$ ls klee-last/
assembly.ll messages.txt run.stats test000002.bout warnings.txt
info run.istats test000001.bout test000003.bout </pre>
Please click <a href="klee-files.html">here</a> if you would like an
overview of the files generated by KLEE. In this tutorial, we only
focus on the actual test files generated by KLEE.
<h2>KLEE-generated test cases</h2> The test cases generated by KLEE
are written in files with extension <tt>.bout</tt>. These are
binary files, which can be read with the <tt>klee-bout-tool</tt>
utility. So let's examine each file:
<pre class="output">
$ klee-bout-tool klee-last/test000001.bout
bout file : 'klee-last/test000001.bout'
args : ['demo.o']
num objects: 1
object 0: name: 'input'
object 0: size: 1
object 0: data: 'b'
$ klee-bout-tool klee-last/test000002.bout
...
object 0: data: '~'
$ klee-bout-tool klee-last/test000003.bout
...
object 0: data: '\x00' </pre>
In each test file, KLEE reports the arguments with which the program
was invoked (in our case no arguments other than the program name
itself), the number of symbolic objects on that path (only one in
our case), the name of our symbolic object ('input') and its size
(1). The actual test itself is represented by the value of our
input: <tt>'b'</tt> for the first test, <tt>'~'</tt> for the second
and <tt>0</tt> for the last one. As expected, KLEE generated a
character which is a lowercase letter (<tt>'b'</tt>), one which is
less than <tt>'a'</tt> (<tt>0</tt>), and one which is greater
than <tt>'z'</tt> (<tt>'~'</tt>). We can now run these values on a
native version of our program, to exercise all paths through the
code!
<h2>Replaying a test case</h2>
While we can run the test cases generated by KLEE on our program by
hand, (or with the help of an existing test infrastructure), KLEE
provides a convenient <i>replay driver</i>, which simply replaces
the call to <tt>klee_make_symbolic</tt> with a call to a function
that assigns to our input the value stored in the .bout file:
<pre class="output">
$ gcc ... </pre>
</div>
</body>
</html>
|
