diff options
Diffstat (limited to 'www/Tutorial-1.html')
| -rw-r--r-- | www/Tutorial-1.html | 187 |
1 files changed, 187 insertions, 0 deletions
diff --git a/www/Tutorial-1.html b/www/Tutorial-1.html new file mode 100644 index 00000000..38c3b101 --- /dev/null +++ b/www/Tutorial-1.html @@ -0,0 +1,187 @@ +<!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>KLEE - Tutorial One</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 get_sign(int x) { + if (x == 0) + return 0; + + if (x < 0) + return -1; + else + return 1; + } </pre> + + You can find the entire code for this example in the source tree + under <tt>examples/get_sign</tt>. A version of the source code can + also be accessed <a href="resources/get_sign.c.html">here</a>. + + <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>a</tt> as symbolic and uses it to + call <tt>get_sign()</tt>: + + <pre class="code"> + int main() { + int a; + klee_make_symbolic(&a, sizeof(a), "a"); + return get_sign(a); + } </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>get_sign.c</tt>, + we run: + + <div class="instr"> + llvm-gcc --emit-llvm -c -g get_sign.c + </div> + + to generate the LLVM bitcode file <tt>get_sign.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 get_sign.o + </div> + + You should see the following output (assumes LLVM 2.8): + <pre class="output"> + KLEE: output directory = "klee-out-0" + + KLEE: done: total instructions = 51 + KLEE: done: completed paths = 3 + KLEE: done: generated tests = 3 </pre> + + There are three paths through our simple function, one + where <tt>a</tt> is <tt>0</tt>, one where it is less than <tt>0</tt> + and one where it is greater than <tt>0</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 run.istats test000002.ktest + info run.stats test000003.ktest + messages.txt test000001.ktest warnings.txt </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>.ktest</tt>. These are + binary files, which can be read with the <tt>ktest-tool</tt> + utility. So let's examine each file: + + <pre class="output"> + $ ktest-tool --write-ints klee-last/test000001.ktest + ktest file : 'klee-last/test000001.ktest' + args : ['get_sign.o'] + num objects: 1 + object 0: name: 'a' + object 0: size: 4 + object 0: data: 1 + + $ ktest-tool --write-ints klee-last/test000002.ktest + ... + object 0: data: -2147483648 + + $ ktest-tool --write-ints klee-last/test000003.ktest + ... + object 0: data: 0 </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 ('a') and its size (4). + The actual test itself is represented by the value of our + input: <tt>1</tt> for the first test, <tt>-2147483648</tt> for the + second and <tt>0</tt> for the last one. As expected, KLEE generated + value <tt>0</tt>, one negative value (<tt>-2147483648</tt>), and one + positive value (<tt>1</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 library</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 <tt>.ktest</tt> + file. + + To use it, simply link your program with the <tt>libkleeRuntest</tt> + library and set the <tt>KTEST_FILE</tt> environment variable to + point to the name of the desired test case: + + <pre class="output"> + $ export LD_LIBRARY_PATH=path-to-klee-root/Release+Asserts/lib/:$LD_LIBRARY_PATH + $ gcc -L path-to-klee-root/Release+Asserts/lib/ get_sign.c -lkleeRuntest + $ KTEST_FILE=klee-last/test000001.ktest ./a.out + $ echo $? + 1 + $ KTEST_FILE=klee-last/test000002.ktest ./a.out + $ echo $? + 255 + $ KTEST_FILE=klee-last/test000003.ktest ./a.out + $ echo $? + 0 </pre> + + As expected, our program returns 1 when running the first test case, + 255 (-1 converted to a valid exit code value in the 0-255 range) + when running the second one, and 0 when running the last one. + + <br/><br/> + +</div> +</body> +</html> |