Revert "move website to separate repo"

This reverts commit 6ae711b1d900bffbca407fe97d5e5ce97745dff1.
author: Dominic Chen <d.c.ddcc@gmail.com> 2013-07-25 10:50:53 +0100
committer: Dominic Chen <d.c.ddcc@gmail.com> 2013-07-25 10:50:53 +0100
commit: 4df4cee1ef65b197020871095cc16d377c9a1996 (patch)
tree: 14578f9ce383f28becedd59d9f0a7d67f8641d7c /www/Tutorial-1.html
parent: 6ae711b1d900bffbca407fe97d5e5ce97745dff1 (diff)
download: klee-4df4cee1ef65b197020871095cc16d377c9a1996.tar.gz
1 files changed, 187 insertions, 0 deletions
diff --git a/www/Tutorial-1.html b/www/Tutorial-1.html
new file mode 100644
index 00000000..38c3b101
--- /dev/null
+++ b/www/Tutorial-1.html
@@ -0,0 +1,187 @@
+<!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>
author	Dominic Chen <d.c.ddcc@gmail.com>	2013-07-25 10:50:53 +0100
committer	Dominic Chen <d.c.ddcc@gmail.com>	2013-07-25 10:50:53 +0100
commit	4df4cee1ef65b197020871095cc16d377c9a1996 (patch)
tree	14578f9ce383f28becedd59d9f0a7d67f8641d7c /www/Tutorial-1.html
parent	6ae711b1d900bffbca407fe97d5e5ce97745dff1 (diff)
download	klee-4df4cee1ef65b197020871095cc16d377c9a1996.tar.gz