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
/
developers-guide.html
206 lines (171 loc) · 11.7 KB
/
developers-guide.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
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
<!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>
<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>KLEE Developer's Guide</h1>
<p>This guide covers several areas of KLEE that may not be imediately obvious to new developers.</p>
<h3>
<a href="#github"> 1. GitHub Environment</a> <br/>
<a href="#build"> 2. Build System</a> <br/>
<a href="#tests"> 3. Regression Testing Framework</a> <br/>
<a href="#misc"> 4. Miscellaneous</a> <br/>
</h3>
<h2 id="build">GitHub Environment</h2>
<p>
KLEE's codebase is currently hosted on <a href="https://github.com/ccadar/klee">GitHub</a>. For those unfamiliar with GitHub, a good starting point is <a href="https://help.github.com/categories/54/articles">here</a>.
</p>
<p>We are using a fork&pull model in KLEE, based on pull requests. For those of you unfamiliar with the process, you can find more information <a href="https://help.github.com/articles/using-pull-requests">here</a>.
</p>
<p>When submitting patches to KLEE, please open a separate pull request for each independent feature or bug fix. This makes it easier to review and approve patches.</p>
<h2 id="build">Build System</h2>
<p>KLEE uses LLVM's ability to build third-party projects, which is described <a href="http://llvm.org/docs/Projects.html">here</a>. The build system uses <a href="http://www.gnu.org/software/autoconf/">GNU Autoconf</a> and <a href="http://www.gnu.org/savannah-checkouts/gnu/autoconf/manual/autoconf-2.69/html_node/autoheader-Invocation.html">AutoHeader</a> to configure the build, but does not use the rest of GNU Autotools (e.g. automake).</p>
<p>LLVM's build system supports out-of-source builds and therefore so does KLEE. It is highly recommended you take advantage of this. For example, you could create three builds (Release, Release with debug symbols, Debug)
that all use the same source tree. This allows you keep your source tree clean and allows multiple configurations to be tested from a single source tree.</p>
<h3>Setting up a debug build of KLEE</h3>
<p>Setting up a debug build of KLEE (we'll assume it is an out-of-source build) is very similar to the build process described in <a href="GetStarted.html">Getting Started</a>, with the exception of steps 6 and 7.</p>
<ol start="6">
<li>Now we will configure KLEE. Notice that we are forcing the compiler to produce unoptimised code, this isn't the default behaviour.
<div class="instr">
$ mkdir path/to/build-dir <br/>
$ cd path/to/build-dir <br/>
$ CXXFLAGS="-g -O0" CFLAGS="-g -O0" path/to/source-dir/configure --with-llvm=<i>path/to/llvm</i> --with-stp=<i>path/to/stp/install</i> --with-uclibc=<i>path/to/klee-uclibc</i> --enable-posix-runtime --with-runtime=Debug+Asserts
</div>
Note if you're using an out-of-source build of LLVM you will need to use <tt>--with-llvmsrc=</tt> and <tt>--with-llvmobj=</tt> configure options instead of <tt>--with-llvm=</tt>
</li>
<li>Now we can build KLEE.
<div class="instr">
$ make -j
</div>
Note that we are using the <tt>-j</tt> option of make to speed up the compilation process.
</li>
</ol>
<p>Note that KLEE depends on LLVM and STP. If you need to debug KLEE's calls to that code, then you will need to build LLVM/STP with debug support too.</p>
<h3>Adding a class</h3>
<p>Because KLEE uses LLVM's makefile build system, adding a class to an existing library in KLEE is very simple. For example, to add a class to <tt>libkleaverExpr</tt>, the following steps would be followed:
<ol>
<li>Create the header file (<tt>.h</tt>) for the class and place it somewhere inside <tt>include/</tt> (the location isn't really important except that <tt>#include</tt> is relative to the <tt>include/</tt> directory).
</li>
<li>Create the source file (<tt>.cpp</tt>) for the class place it in <tt>lib/Expr/</tt>. You can confirm that the library in which your new class will be included is <tt>kleaverExpr</tt> by looking at the <tt>Makefile</tt> in <tt>lib/Expr</tt>.
</li>
</ol>
That's it! Now LLVM's build system will detect the new <tt>.cpp</tt> file and add it to the library that is generated when you run <tt>make</tt>.
</p>
<h3>Building code documentation</h3>
<p>KLEE uses <a href="http://www.doxygen.org">Doxygen</a> to generate code documentation. To generate it yourself you can run the following from KLEE's build directory root.
<div class="instr">
$ make doxygen
</div>
This will generate documentation in <tt>path/to/build-dir/docs/doxygen/</tt> folder. You can also find KLEE's latest official code documentation <a href="http://www.doc.ic.ac.uk/~dsl11/klee-doxygen/">here</a>
</p>
<h2 id="tests">Regression Testing Framework</h2>
<p>KLEE uses LLVM's testing infrastructure for its regression tests. In KLEE these are...
<ul>
<li>External tests executed by <a href="http://llvm.org/docs/CommandGuide/lit.html"><tt>llvm-lit</tt></a>. These are the tests that are executed by the <tt>make check</tt> command.
These test the KLEE tools externally.
</li>
<li>Internal tests that are driven using <a href="https://code.google.com/p/googletest/">GoogleTest</a>. These are the tests that are executed by the <tt>make unittests</tt> command.
These test KLEE's internal APIs.
</li>
</ul>
</p>
<h3>External tests</h3>
<tt>llvm-lit</tt> is used to test KLEE's tools by invoking them as shell commands.
<p>
KLEE's tests are currently divided into categories, each of which is a subdirectory in <tt>test/</tt> in the source tree (e.g. <tt>test/Feature</tt>).
<tt>llvm-lit</tt> is passed one or more paths to test files or directories which it will search recursively for tests. The <tt>llvm-lit</tt> tool needs to know
what test-suite the tests belong to and how to run them. This information is in the <tt>lit.site.cfg</tt> (generated by the <tt>Makefile</tt>). This file itself
refers to <tt>lit.cfg</tt> which tells <tt>llvm-lit</tt> how to run the test suite. At the time of writing the <tt>lit.cfg</tt> instructs <tt>llvm-lit</tt>
to treat files with the following file extensions as tests:<tt> .ll .c .cpp .pc </tt>.
</p>
<p>
It is desirable to disable some tests (e.g. disable klee-uclibc tests if support was not compiled in) or change which file extensions to look for. This
is done by adding a <tt>lit.local.cfg</tt> file to a directory which can be used to customise how tests in that directory are executed. For example
to change the file extensions searched for to <tt>.cxx</tt> and <tt>.txt</tt> the following could be used in a <tt>lit.local.cfg</tt> file:
<div class="instr">
config.suffixes = ['.cxx', '.txt' ]</br>
</div>
To disable execution of tests in a directory based on a condition you can mark them as unsupported by placing the following inside a <tt>lit.local.cfg</tt> file
in that directory (where <tt>some_condition</tt> is any Python expression):
<div class="instr">
if some_condition: config.unsupported = True
</div>
All <tt>llvm-lit</tt> configuration files are Python scripts loaded by <tt>llvm-lit</tt> so you have the full power of Python at your disposal.
</p>
<p>The actions performed in each test are specified by special comments in the file. For example, in <tt>test/Feature/ByteSwap.c</tt> the first two lines are
<div class="instr">
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc <br/>
// RUN: %klee --libc=klee --exit-on-error %t1.bc <br/>
</div>
This first runs <tt>llvm-gcc</tt> on the source file (<tt>%s</tt>) and generates a temporary file (<tt>%t1.bc</tt>). Then KLEE is executed on this generated temporary file. If either program returns a non-zero exit code (or crashes) then
test is considered to have failed. More information on the available substitution variables (such as <tt>%s</tt>) can be found
<a href="http://llvm.org/docs/TestingGuide.html#variables-and-substitutions">here</a>.
</p>
<p>To run the entire test suite run</p>
<div class="instr">
$ cd path/to/klee/build/test</br>
$ make check </br>
</div>
or you can use <tt>llvm-lit</tt> directy
<div class="instr">
$ cd path/to/klee/build/test</br>
$ llvm-lit -j1 . </br>
</div>
If you want to run a subset of the test suite simply pass the filenames of the tests or directories to search for tests to <tt>llvm-lit</tt>.
For example the commands below will execute the <tt>Feature/DoubleFree.c</tt> and <tt>CXX/ArrayNew.cpp</tt> test and all tests nested in the <tt>regression/</tt> folder.
<div class="instr">
$ cd path/to/klee/build/test</br>
$ llvm-lit -j1 Feature/DoubleFree.c CXX/ArrayNew.cpp regression/
</br>
</div>
<b>Note the test suite currently cannot be executed in parallel so the <tt>-j1</tt> flag must be passed to <tt>llvm-lit</tt> to prevent tests from being run in parallel.</b>
<p>
Sometimes it can be useful to pass extra command line options to <tt>klee</tt> or <tt>kleaver</tt> when running tests. This could be used for example to quickly see if changing
the default value for a command line option changes the passing/failing of a test. This is <b>not</b> a substitute for writing new tests for <tt>klee</tt> or <tt>kleaver</tt>!
If you add a new feature that is exposed by a new command line option a new test should be added that tests this behaviour.
</p>
<p>Here is an example:</p>
<div class="instr">
$ cd test/
$ llvm-lit --param klee_opts=-use-forked-solver=0 --param kleaver_opts="-use-forked-solver=0 -use-query-log=all:smt2" .</br>
</div>
In this example when running <tt>klee</tt> in tests an extra option <tt>-use-forked-solver=0</tt> is passed to <tt>klee</tt> and when running <tt>kleaver</tt> the <tt>-use-forked-solver=0</tt>
and <tt>-use-query-log=all:smt2</tt> options will be passed to <tt>kleaver</tt>. It is important to realise if the test already invokes <tt>klee</tt> or <tt>kleaver</tt>
with a particular option you will not be able to override that option because the <tt>klee_opts</tt> and <tt>kleaver_opts</tt> are substituted just after the tool name so subsequent options
used in the test will override these.
<p>
For more information on <tt>llvm-lit</tt> tests see <a href="http://llvm.org/docs/TestingGuide.html#id1">LLVM's testing infrastructure documentation</a> and the
<a href="http://llvm.org/docs/CommandGuide/lit.html"><tt>llvm-lit</tt> tool documentation</a>.
</p>
<h3>Internal tests</h3>
<p>
These tests are located in <tt>unittests/</tt> and can be executed by running:
<div class="instr">
$ cd path/to/klee/build/</br>
$ make unittests</br>
</div>
</p>
<p>
These test use <a href="https://code.google.com/p/googletest/">Google's C++ testing framework</a> and is well <a href="https://code.google.com/p/googletest/wiki/Documentation">documented here.</a>
</p>
<h2 id="misc">Miscellaneous</h2>
<h3>Writing messages to standard error</h3>
<p>The <tt>kleeCore</tt> library (<tt>lib/Core</tt>) provides several functions that can be used similarly to <tt>printf()</tt> in C. See <tt>lib/Core/Common.h</tt> for more information.
</p>
<h3>Adding a command line option to a tool</h3>
<p>KLEE uses LLVM's CommandLine library for adding options to tools in KLEE, which is well documented <a href="http://llvm.org/docs/CommandLine.html">here</a>. See <tt>lib/core/Executor.cpp</tt> for examples.</p>
<br/>
</div>
</body>
</html>