diff options
Diffstat (limited to 'www/tutorial-1.html')
| -rw-r--r-- | www/tutorial-1.html | 181 |
1 files changed, 0 insertions, 181 deletions
diff --git a/www/tutorial-1.html b/www/tutorial-1.html deleted file mode 100644 index 3f9bfc4e..00000000 --- a/www/tutorial-1.html +++ /dev/null @@ -1,181 +0,0 @@ -<!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 my_islower(int x) { - if (x >= 'a' && x <= 'z') - return 1; - else return 0; - } </pre> - - You can find the entire code for this example <a href="code-examples/demo.c">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>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 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 klee-last/test000001.ktest - ktest file : 'klee-last/test000001.ktest' - args : ['demo.o'] - num objects: 1 - object 0: name: 'input' - object 0: size: 1 - object 0: data: 'b' - - $ ktest-tool klee-last/test000002.ktest - ... - object 0: data: '~' - - $ ktest-tool klee-last/test000003.ktest - .. - 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 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"> - $ gcc ~/klee/Release/lib/libkleeRuntest.dylib demo.c - $ KTEST_FILE=klee-last/test000001.ktest ./a.out - $ echo $? - 1 - $ KTEST_FILE=klee-last/test000002.ktest ./a.out - $ echo $? - 0 - $ KTEST_FILE=klee-last/test000003.ktest ./a.out - $ echo $? - 0 </pre> - - As expected, our program returns 1 when running the first test case - (which contains the lowercase letter <tt>'b'</tt>), and 0 when - running the other two (which don't contain lowercase letters). - - <br/><br/> - -</div> -</body> -</html> |