This repository has been archived by the owner on Mar 5, 2024. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Experimental.html
184 lines (147 loc) · 5.74 KB
/
Experimental.html
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
182
183
184
<!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 (Experimental)</title>
<link type="text/css" rel="stylesheet" href="menu.css" />
<link type="text/css" rel="stylesheet" href="content.css" />
</head>
<body>
<div id="menu">
<iframe src="menu.html" height="500" frameborder="0" scrolling="auto">
<a href="menu.html">Click here to load the iframe menu.</a>
</iframe>
</div>
<div id="content">
<h1>Getting Started: Building and Running KLEE (Experimental Version)</h1>
<h2 id="build_new">Building KLEE with LLVM 3.4</h2>
<p>The current procedure for building is outlined below.</p>
<ol>
<li><b>Install dependencies:</b>
<p>
KLEE requires all the dependencies of LLVM, which are discussed <a href="http://llvm.org/docs/GettingStarted.html#requirements">here</a>. In particular, you should install the following programs and libraries, listed below as Ubuntu packages:
<div class="instr">
$ sudo apt-get install git cmake bison flex libboost-program-options-dev libboost-system-dev libncurses5-dev libcap-dev g++ libgtest-dev <br/>
</div>
</p>
You will also need gcc 4.8 or later installed on your system. On
Ubuntu ≥ 12.04, you can follow the instructions
at <a href="http://ubuntuhandbook.org/index.php/2013/08/install-gcc-4-8-via-ppa-in-ubuntu-12-04-13-04/">here</a>
if you need to install it.
</li>
<li><b>Install LLVM:</b>
<p>
If you are using a recent Ubuntu (≥ 12.04, e.g. 14.04 LTS) or Debian, we recommend you to use the LLVM packages provided by LLVM itself.
Use <a href="http://www.llvm.org/apt/">LLVM Package Repository</a> to add the appropriate line to your /etc/apt/sources.list. As an example, for Ubuntu 14.04, the following lines should be added:
<div class="instr">
# 3.4 <br/>
deb http://llvm.org/apt/trusty/ llvm-toolchain-trusty-3.4 main <br/>
deb-src http://llvm.org/apt/trusty/ llvm-toolchain-trusty-3.4 main <br/>
</div>
<p>
Then add the repository key and install the 3.4 packages:
<div class="instr">
$ wget -O - http://llvm.org/apt/llvm-snapshot.gpg.key|sudo apt-key add - <br/>
$ sudo apt-get update <br/>
$ sudo apt-get install llvm-3.4-tools clang-3.4
</div>
Finally, make sure llvm-config is in your path:
<div class="instr">
$ mkdir -p ~/bin/ <br/>
$ ln -sf /usr/bin/llvm-config-3.4 ~/bin/llvm-config <br/>
$ echo "export PATH=\"\$PATH:\$HOME/bin\"" >> ~/.bashrc <br/>
$ source ~/.bashrc
</div>
That's it for LLVM. If you want to install it manually, please refer to the official <a href="http://www.llvm.org/docs/GettingStarted.html">LLVM Getting-Started documentation</a>.
</p>
</li>
<li> <b>Build STP:</b>
<p>KLEE is based on
the <a href="http://sites.google.com/site/stpfastprover/">STP</a>
constraint solver. 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
we have used successfully, but you can try a more recent revision by
changing or removing the <tt>-r</tt> argument to the <tt>svn co</tt>
command. (Please let us know if you have successfully and extensively
used KLEE with a more recent version of STP.)
</p>
<div class="instr">
$ git clone https://github.com/stp/stp.git<br/>
$ mkdir stp_build && cd stp_build <br/>
$ cmake -G 'Unix Makefiles' ../stp<br/>
$ make <br/>
$ cd ../
</div>
</li>
As documented on the STP website, it is essential to run the following
command before using STP (and thus KLEE):
<div class="instr">
$ ulimit -s unlimited
</div>
<li>[Optional] <b>Build uclibc and the POSIX environment model:</b>
<p>
By default, KLEE works 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>
<div class="instr">
$ git clone https://github.com/klee/klee-uclibc.git <br/>
$ cd klee-uclibc <br/>
$ ./configure --make-llvm-lib <br/>
$ make <br/>
$ cd ..
</div>
<p><b>NOTE:</b> If you are on a different target (i.e., not i386
or x64), you will need to run <tt>make config</tt> and select the
correct target. The defaults for the other uClibc configuration
variables should be fine.<p>
</li>
<li>[Optional] <b>Build libgtest:</b>
<p>
Build Google test libraries for unittests.
</p>
<div class="instr">
$ mkdir gtest <br/>
$ cd gtest <br/>
$ cmake /usr/src/gtest/ <br/>
$ make <br/>
$ pwd <br/>
$ cd ..
</div>
Note down the output of pwd it will be used later for KLEEs unittests.
</li>
<li><b>Checkout KLEE (to any path you like):</b>
<div class="instr">
$ git clone https://github.com/klee/klee.git
</div>
</li>
<li><b>Configure KLEE:</b>
<p>From the KLEE source directory, run:</p>
<div class="instr">
$ mkdir build </br>
$ cd build <br/>
$ ../configure --with-stp=<i>../stp_build</i> --with-uclibc=<i>../klee-uclibc</i> --enable-posix-runtime
</div>
<p><b>NOTE:</b> If you skipped step 4, simply remove the <tt>--with-uclibc</tt> and <tt>--enable-posix-runtime options</tt>. </p>
</li>
<li><b>Build KLEE:</b>
<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 LDFLAGS=-LPATH_TO_GTEST_DIRECTORY unittests<br/>
</div>
For the unittests, replace PATH_TO_GTEST_DIRECTORY with the absolute path to the build directory of Google tests.
</li>
<li>You're ready to go! Go to the <a href="Tutorials.html">Tutorials</a> page
to try KLEE.</li>
</ol>
</div>
</body>
</html>