blob: 76e741c88b8ead94c9e9f5eb5c02da89de719050 (
plain) (
blame)
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
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
|
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN"
"http://www.w3.org/TR/html4/strict.dtd">
<html>
<head>
<META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1" />
<title>KLEE - Getting Started</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>Getting Started: Building and Running KLEE</h1>
<!-- <p>FIXME: Intro and disclaimer.</p> -->
<h2 id="build">Building KLEE</h2>
<p>If you would like to try KLEE, the current procedure for building is
below.</p>
KLEE is built on LLVM; the first steps are to get a working LLVM
installation. See <a href="http://llvm.org/docs/GettingStarted.html">Getting
Started with the LLVM System</a> for more information.
<p><b>NOTE:</b> KLEE is only currently tested on Linux and Darwin x86-32
targets, using LLVM top-of-tree. KLEE will not work with an older LLVM (e.g.,
2.5). We are currently working on full support for Linux and Darwin x86-64
targets.<p>
<ol>
<li>Install llvm-gcc:
<ul>
<li>Download and install the LLVM 2.7 release of <tt>llvm-gcc</tt>
from <a href="http://llvm.org/releases/download.html">here</a>. Add
<tt>llvm-gcc</tt> to your <tt>PATH</tt>. It is important to do this first
so that <tt>llvm-gcc</tt> is found in subsequent <tt>configure</tt>
steps. <tt>llvm-gcc</tt> will be used later to compile programs that KLEE
can execute.</li>
</ul>
</li>
<li><a href="http://llvm.org/releases/download.html#2.7">Download and build
LLVM 2.7</a> (you may also use SVN head, but klee may not always be
up-to-date with LLVM API changes).
<div class="instr">
$ curl -O http://llvm.org/releases/2.7/llvm-2.7.tgz <br>
$ tar zxvf llvm-2.7.tgz <br>
$ cd llvm-2.7 <br>
$ ./configure --enable-optimized <br>
$ make
</div>
(the <tt>--enable-optimized</tt> configure argument is not necessary, but
KLEE runs very slowly in Debug mode).
</li>
<li>Checkout KLEE (to any path you like):
<div class="instr">
$ svn co http://llvm.org/svn/llvm-project/klee/trunk klee
</div>
</li>
<li>Configure KLEE (from the KLEE source directory):
<div class="instr">
$ ./configure --with-llvm=<i>path/to/llvm</i>
</div>
<p>This assumes that you compiled LLVM in-place. If you used a
different directory for the object files then use:
<div class="instr">
$ ./configure --with-llvmsrc=<i>path/to/llvm/src</i> --with-llvmobj=<i>path/to/llvm/obj</i>
</div>
</li>
<li>Build KLEE (from the KLEE source directory):
<div class="instr">
$ make ENABLE_OPTIMIZED=1
</div>
</li>
<li>Run the regression suite to verify your build:
<div class="instr">
$ make check<br>
$ make unittests<br>
</div>
</li>
<li>You're ready to go! Go to the <a href="Tutorials.html">Tutorials</a> page
to try KLEE.</li>
</ol>
<h2 id="uclib">Building KLEE with POSIX runtime support</h2>
<p>The steps above are enough for building and testing KLEE on closed programs
(programs that don't use any external code such as C library
functions). However, if you want to use KLEE to run real programs you will want
to enable the KLEE POSIX runtime, which is built on top of the uClibc C
library.</p>
<ol>
<li>Download KLEE's uClibc:
<ul>
<li>
KLEE uses a version of <a href="http://uclibc.org">uClibc</a>
which has been modified slightly for use with KLEE.
<ul>
<li>A version that works on 32-bit Linux can be found
here: <a href="http://t1.minormatter.com/~ddunbar/klee-uclibc-0.01.tgz">klee-uclibc-0.01.tgz</a></li>
<li>A version that works on 64-bit Linux can be found
here: <a href="http://www.doc.ic.ac.uk/~cristic/klee-uclibc-0.01-x64.tgz">klee-uclibc-0.01-x64.tgz</a>
</li>
</ul>
</li>
</ul>
</li>
<li>Build uClibc with <tt>llvm-gcc</tt>:
<div class="instr">
$ tar zxvf klee-uclibc-0.01.tgz <br>
$ ./configure --with-llvm=<i>path/to/llvm</i> <br>
$ make <br>
</div>
<p><b>NOTE:</b> KLEE's uClibc is shipped in a pre-configured for x86-32. If
you are on a different target (e.g. x86-64), you will need to run 'make
config' and select the correct target. The defaults for the other uClibc
configuration variables should be fine.<p>
</li>
<li>Configure KLEE with uClibc/POSIX support:
<div class="instr">
$ ./configure --with-llvm=<i>path/to/llvm</i> --with-uclibc=<i>path/to/klee-uclibc</i> --enable-posix-runtime
</div>
</li>
<li>Rebuild KLEE and run <tt>make check</tt> and verify that the POSIX tests
run correctly.
</li>
</ol>
<h2 id="stp">Building KLEE with a more recent version of STP</h2>
<p>If your benchmarks are running slowly or not terminating it may
be worth trying a more recent version of KLEE's constraint solver
<a href="http://sites.google.com/site/stpfastprover/">STP</a>,
which offers performance improvements over the version supplied
with KLEE.</p>
<p>STP does not make frequent releases, and its Subversion repository
is under constant development and may be unstable. The instructions
below are for a particular revision which is known to pass the KLEE
test suite, but you can try a more recent revision (at your own risk)
by changing or removing the <tt>-r</tt> argument to the <tt>svn
co</tt> command.</p>
<ol>
<li>Download and build STP.
<div class="instr">
$ svn co -r 940 https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp stp <br>
$ cd stp <br>
$ scripts/configure --with-prefix=<i>path/to/stp/inst</i> --with-cryptominisat2 <br>
$ make OPTIMIZE=-O2 CFLAGS_M32= install
</div>
</li>
<li>Configure KLEE:
<div class="instr">
$ ./configure --with-llvm=<i>path/to/llvm</i> --with-stp=<i>path/to/stp/inst</i>
</div>
</li>
<li>Rebuild KLEE.</li>
</ol>
</div>
</body>
</html>
|
