diff options
| author | Dominic Chen <d.c.ddcc@gmail.com> | 2013-07-25 10:58:00 +0100 |
|---|---|---|
| committer | Dominic Chen <d.c.ddcc@gmail.com> | 2013-07-25 10:58:00 +0100 |
| commit | 032a2dedd1d3d033bcc410c3de07e6ed0f701ac0 (patch) | |
| tree | da6a64772f9440601c7b0efd816b06c40bdf90d8 /www/Tutorial-1.html | |
| parent | 4df4cee1ef65b197020871095cc16d377c9a1996 (diff) | |
| download | klee-032a2dedd1d3d033bcc410c3de07e6ed0f701ac0.tar.gz | |
remove www from master branch
Diffstat (limited to 'www/Tutorial-1.html')
| -rw-r--r-- | www/Tutorial-1.html | 187 |
1 files changed, 0 insertions, 187 deletions
diff --git a/www/Tutorial-1.html b/www/Tutorial-1.html deleted file mode 100644 index 38c3b101..00000000 --- a/www/Tutorial-1.html +++ /dev/null @@ -1,187 +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 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> |