[llvm-commits] [klee] r72207 - in /klee/trunk/www: code-examples/ code-examples/demo.c tutorial-1.html
Cristian Cadar
cristic at cs.stanford.edu
Wed May 20 23:55:58 PDT 2009
Author: cristic
Date: Thu May 21 01:55:54 2009
New Revision: 72207
URL: http://llvm.org/viewvc/llvm-project?rev=72207&view=rev
Log:
Added a first KLEE tutorial.
Added:
klee/trunk/www/code-examples/
klee/trunk/www/code-examples/demo.c
klee/trunk/www/tutorial-1.html
Added: klee/trunk/www/code-examples/demo.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/www/code-examples/demo.c?rev=72207&view=auto
==============================================================================
--- klee/trunk/www/code-examples/demo.c (added)
+++ klee/trunk/www/code-examples/demo.c Thu May 21 01:55:54 2009
@@ -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);
+}
Added: klee/trunk/www/tutorial-1.html
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/www/tutorial-1.html?rev=72207&view=auto
==============================================================================
--- klee/trunk/www/tutorial-1.html (added)
+++ klee/trunk/www/tutorial-1.html Thu May 21 01:55:54 2009
@@ -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>
More information about the llvm-commits
mailing list