Added a first KLEE tutorial.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72207 91177308-0d34-0410-b5e6-96231b3b80d8
author: Cristian Cadar <cristic@cs.stanford.edu> 2009-05-21 06:55:54 +0000
committer: Cristian Cadar <cristic@cs.stanford.edu> 2009-05-21 06:55:54 +0000
commit: 467108ce9b81a4f57f2fb52d1a35759d4bd053a1 (patch)
tree: 0855e04be2e0125e9d64cfe441c166906faf544d
parent: cd95368ea4f74b09e30725ba04cc84ede6b24fcf (diff)
download: klee-467108ce9b81a4f57f2fb52d1a35759d4bd053a1.tar.gz
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>
author	Cristian Cadar <cristic@cs.stanford.edu>	2009-05-21 06:55:54 +0000
committer	Cristian Cadar <cristic@cs.stanford.edu>	2009-05-21 06:55:54 +0000
commit	467108ce9b81a4f57f2fb52d1a35759d4bd053a1 (patch)
tree	0855e04be2e0125e9d64cfe441c166906faf544d
parent	cd95368ea4f74b09e30725ba04cc84ede6b24fcf (diff)
download	klee-467108ce9b81a4f57f2fb52d1a35759d4bd053a1.tar.gz