diff options
| -rw-r--r-- | www/code-examples/demo.c | 11 | ||||
| -rw-r--r-- | www/tutorial-1.html | 160 |
2 files changed, 171 insertions, 0 deletions
diff --git a/www/code-examples/demo.c b/www/code-examples/demo.c new file mode 100644 index 00000000..69e0715a --- /dev/null +++ b/www/code-examples/demo.c @@ -0,0 +1,11 @@ +int my_islower(int x) { + if (x >= 'a' && x <= 'z') + return 1; + else return 0; +} + +int main() { + char c; + klee_make_symbolic_name(&c, sizeof(c), "input"); + return my_islower(c); +} diff --git a/www/tutorial-1.html b/www/tutorial-1.html new file mode 100644 index 00000000..8307e69c --- /dev/null +++ b/www/tutorial-1.html @@ -0,0 +1,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> |