diff options
| -rw-r--r-- | www/Examples.html | 114 | ||||
| -rw-r--r-- | www/GetInvolved.html | 25 | ||||
| -rw-r--r-- | www/GetStarted.html | 10 | ||||
| -rw-r--r-- | www/menu.html.incl | 2 | ||||
| -rw-r--r-- | www/resources/Regexp.c.html | 78 |
5 files changed, 208 insertions, 21 deletions
diff --git a/www/Examples.html b/www/Examples.html index 23584053..25ee6fb0 100644 --- a/www/Examples.html +++ b/www/Examples.html @@ -15,19 +15,119 @@ <h1>KLEE Examples</h1> -<p>FIXME: Intro.</p> +<p>Here is a basic example of using KLEE to test a simple regular expression matching function. You can find the basic example in the source tree under <tt>examples/regexp</tt>.</p> -<h2>Basic Sort Example</h2> +<h2>Example: <tt>Regexp.c</tt></h2> -<p>FIXME: Write.</p> +<p><tt>Regexp.c</tt> contains a simple regular expression matching function, and +the bare bones testing harness (in <tt>main</tt>) need to explore this code with +klee. You can see a version of the source +code <a href="resources/Regexp.c.html">here</a>.</p> -<h2>FIXME: More complicated example</h2> +<p>This example will show to build and run the example using KLEE, as well as +how to interpret the output, and some additional KLEE features that can be used +when writing a test driver by hand.</p> -<p>FIXME: Write: show the important klee.h functions.</p> +<p>We'll start by showing how to build and run the example, and then explain how +the test harness works in more detail.</p> + +<h3>Step 1: Building the example</h3> -<p>FIXME: Write: show the important klee tools.</p> +<p>The first step is to compile the source code using a compiler which can +generate object files in LLVM bitcode format. Here we use <tt>llvm-gcc</tt>, +but <a href="http://clang.llvm.org">Clang</a> works just as well!</p> -<p>FIXME: Write: show the important klee options.</p> +<p>From within the <tt>examples/regexp</tt> directory: +<div class="instr"> + <b>$ llvm-gcc -I ../../include -emit-llvm -c -g Regexp.c</b> +</div> +which should create a <tt>Regexp.o</tt> file in LLVM bitcode +format. The <tt>-I</tt> argument is used so that the compiler can +find <a href="http://t1.minormatter.com/~ddunbar/klee-doxygen/klee_8h-source.html">"klee/klee.h"</a>,which +contains definitions for the intrinsic functions used to interact with the KLEE +virtual machine. <tt>-c</tt> is used because we only want to compile the code to +an object file (not a native executable), and finally <tt>-g</tt> causes +additional debug information to be stored in the object file, which KLEE will +use to determine source line number information.</p> + +<p>If you have the LLVM tools installed in your path, you can verify that this step +worked by running <tt>llvm-nm</tt> on the generated file:</p> +<div class="instr"> +<pre> + <b>$ llvm-nm Regexp.o</b> + t matchstar + t matchhere + T match + T main + U klee_make_symbolic_name + d LC + d LC1 +</pre> +</div> + +<p>Normally before running this program we would need to link it to create a +native executable. However, KLEE runs directly on LLVM bitcode files -- since +this program only has a single file there is no need to link. For "real" +programs with multiple inputs, +the <a href="http://llvm.org/cmds/llvm-link.html"><tt>llvm-link</tt></a> +and <a href="http://llvm.org/cmds/llvm-ld.html"><tt>llvm-ld</tt></a> tools can +be used in place of the regular link step to merge multiple LLVM bitcode files +into a single module which can be executed by KLEE.</p> + +<h3>Step 2: Executing the code with KLEE</h3> + +<!-- FIXME: Make only-output-states-covering-new default --> +<p>The next step is to execute the code with KLEE:</p> +<div class="instr"> +<pre> +<b>$ klee --only-output-states-covering-new Regexp.o</b> +KLEE: output directory = "klee-out-1" +KLEE: ERROR: .../klee/examples/regexp/Regexp.c:23: memory error: out of bound pointer +KLEE: NOTE: now ignoring this error at this location +KLEE: ERROR: .../klee/examples/regexp/Regexp.c:25: memory error: out of bound pointer +KLEE: NOTE: now ignoring this error at this location +KLEE: done: total instructions = 6334861 +KLEE: done: completed paths = 7692 +KLEE: done: generated tests = 22 +</pre> +</div> + +<p>On startup, KLEE prints the directory used to store output (in this +case <tt>klee-out-1</tt>). By default klee will use the first +free <tt>klee-out-<em>N</em></tt> directory and also create a <tt>klee-last</tt> +symlink which will point to the most recent created directory. You can specify a +directory to use for outputs using the <tt>-output-dir=<em>path</em></tt> +command line argument.</p> + +<p>While KLEE is running, it will print status messages for "important" events, +for example when it finds an error in the program. In this case, KLEE detected +to invalid memory accesses on lines 23 and 25 of our test program. We'll look +more at this in a moment.</p> + +<p>Finally, when KLEE finishes execution it prints out a few statistics about +the run. Here we see that KLEE executed a total of ~6 million instructions, +explored 7,692 paths, and generated 22 test cases.</p> + +<p>Note that many realistic programs have an infinite (or extremely large) +number of paths through them, and it is common that KLEE will not terminate. By +default KLEE will run until the user presses Control-C (i.e. <tt>klee</tt> gets +a SIGINT), but there are additional options to limit KLEE's runtime and memory +usage:<p> +<ul> + <li><tt>-max-time=<em>seconds</em></tt>: Halt execution after the given number + of seconds.</li> + <li><tt>-max-forks=<em>N</em></tt>: Stop forking after <em>N</em> symbolic + branches, and run the remaining paths to termination.</li> + <li><tt>-max-memory=<em>N</em></tt>: Try to limit memory consumption + to <em>N</em> megabytes.</li> +</ul> +</p> + +<h3>Step ?: Changing the test harness</h3> + +<p>FIXME: Step through & explain the test harness, and how we can modify it.</p> + +<p>FIXME: Write: show the important klee.h functions.</p> </div> </body> diff --git a/www/GetInvolved.html b/www/GetInvolved.html index b8afcbb3..41c84e54 100644 --- a/www/GetInvolved.html +++ b/www/GetInvolved.html @@ -3,7 +3,7 @@ <html> <head> <META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1" /> - <title>klee - Get Involved</title> + <title>KLEE - Get Involved</title> <link type="text/css" rel="stylesheet" href="menu.css" /> <link type="text/css" rel="stylesheet" href="content.css" /> </head> @@ -13,21 +13,30 @@ <div id="content"> -<h1>Getting Involved with the klee Project</h1> +<h1>Getting Involved with the KLEE Project</h1> -<p>FIXME: Intro.</p> +<p>If you are interested in following development of KLEE, or would like to +contribute, here are some resources that may prove useful.</p> <h2>Mailing Lists</h2> -<p>klee-dev</p> +<p>Currently the main list for KLEE discussion (both for users and developers) +is <a href="http://keeda.stanford.edu/mailman/listinfo/klee-dev">klee-dev</a>.</p> -<p>klee-commits</p> +<p>Commit messages to the KLEE repository go to +<a href="http://keeda.stanford.edu/mailman/listinfo/klee-commits">klee-commits</a>. This +is also the place to send patches if you are interested in contributing to +KLEE.</p> <h2>Working with the Code</h2> -<p>FIXME: Point at pertinent LLVM docs.</p> - -<p>FIXME: Point at doxygen.</p> +<p>KLEE developer documentation is written in doxygen and you may have it online here: + <a href="http://t1.minormatter.com/~ddunbar/klee-doxygen/index.html">doxygen</a> + (this is updated nightly from the source tree).</p> + +<p>Many parts of KLEE rely on the LLVM infrastructure, you can find more +information about programming for LLVM here: +<a href="http://llvm.org/docs/#llvmprog">LLVM's General Programming Documentation</a>.</p> </div> </body> diff --git a/www/GetStarted.html b/www/GetStarted.html index 07083d4f..5f28b1d3 100644 --- a/www/GetStarted.html +++ b/www/GetStarted.html @@ -39,12 +39,12 @@ Started with the LLVM System</a> for more information. <li><a href="http://www.llvm.org/docs/GettingStarted.html#checkout">Checkout and build LLVM</a> from SVN head: - <code class="instr"> <code> - svn co http://llvm.org/svn/llvm-project/llvm/trunk llvm - cd llvm - ./configure --enable-optimized + <div class="instr"> + svn co http://llvm.org/svn/llvm-project/llvm/trunk llvm <br> + cd llvm <br> + ./configure --enable-optimized <br> make - </code></code> + </div> (the <tt>--enable-optimized</tt> configure argument is not necessary, but KLEE runs very slowly in Debug mode). diff --git a/www/menu.html.incl b/www/menu.html.incl index ef450ca7..58245138 100644 --- a/www/menu.html.incl +++ b/www/menu.html.incl @@ -4,7 +4,7 @@ </div> <div class="submenu"> - <label>klee Info</label> + <label>KLEE Info</label> <a href="index.html">About</a> <a href="GetStarted.html">Get Started</a> <a href="GetInvolved.html">Get Involved</a> diff --git a/www/resources/Regexp.c.html b/www/resources/Regexp.c.html new file mode 100644 index 00000000..cb3e3d75 --- /dev/null +++ b/www/resources/Regexp.c.html @@ -0,0 +1,78 @@ +<!DOCTYPE html PUBLIC "-//IETF//DTD HTML 2.0//EN"> +<HTML> +<HEAD> +<TITLE>Enscript Output</TITLE> +</HEAD> +<BODY BGCOLOR="#FFFFFF" TEXT="#000000" LINK="#1F00FF" ALINK="#FF0000" VLINK="#9900DD"> +<A NAME="top"> +<A NAME="file1"> +<H1>Regexp.c</H1> + +<PRE> +<I><FONT COLOR="#B22222">/* + * Simple regular expression matching. + * + * From: + * The Practice of Programming + * Brian W. Kernighan, Rob Pike + * + */</FONT></I> + +#<B><FONT COLOR="#5F9EA0">include</FONT></B> <B><FONT COLOR="#BC8F8F"><klee/klee.h></FONT></B> + +<B><FONT COLOR="#228B22">static</FONT></B> <B><FONT COLOR="#228B22">int</FONT></B> <B><FONT COLOR="#0000FF">matchhere</FONT></B>(<B><FONT COLOR="#228B22">char</FONT></B>*,<B><FONT COLOR="#228B22">char</FONT></B>*); + +<B><FONT COLOR="#228B22">static</FONT></B> <B><FONT COLOR="#228B22">int</FONT></B> <B><FONT COLOR="#0000FF">matchstar</FONT></B>(<B><FONT COLOR="#228B22">int</FONT></B> c, <B><FONT COLOR="#228B22">char</FONT></B> *re, <B><FONT COLOR="#228B22">char</FONT></B> *text) { + <B><FONT COLOR="#A020F0">do</FONT></B> { + <B><FONT COLOR="#A020F0">if</FONT></B> (matchhere(re, text)) + <B><FONT COLOR="#A020F0">return</FONT></B> 1; + } <B><FONT COLOR="#A020F0">while</FONT></B> (*text != <B><FONT COLOR="#BC8F8F">'\0'</FONT></B> && (*text++ == c || c== <B><FONT COLOR="#BC8F8F">'.'</FONT></B>)); + <B><FONT COLOR="#A020F0">return</FONT></B> 0; +} + +<B><FONT COLOR="#228B22">static</FONT></B> <B><FONT COLOR="#228B22">int</FONT></B> <B><FONT COLOR="#0000FF">matchhere</FONT></B>(<B><FONT COLOR="#228B22">char</FONT></B> *re, <B><FONT COLOR="#228B22">char</FONT></B> *text) { + <B><FONT COLOR="#A020F0">if</FONT></B> (re[0] == <B><FONT COLOR="#BC8F8F">'\0'</FONT></B>) + <B><FONT COLOR="#A020F0">return</FONT></B> 0; + <B><FONT COLOR="#A020F0">if</FONT></B> (re[1] == <B><FONT COLOR="#BC8F8F">'*'</FONT></B>) + <B><FONT COLOR="#A020F0">return</FONT></B> matchstar(re[0], re+2, text); + <B><FONT COLOR="#A020F0">if</FONT></B> (re[0] == <B><FONT COLOR="#BC8F8F">'$'</FONT></B> && re[1]==<B><FONT COLOR="#BC8F8F">'\0'</FONT></B>) + <B><FONT COLOR="#A020F0">return</FONT></B> *text == <B><FONT COLOR="#BC8F8F">'\0'</FONT></B>; + <B><FONT COLOR="#A020F0">if</FONT></B> (*text!=<B><FONT COLOR="#BC8F8F">'\0'</FONT></B> && (re[0]==<B><FONT COLOR="#BC8F8F">'.'</FONT></B> || re[0]==*text)) + <B><FONT COLOR="#A020F0">return</FONT></B> matchhere(re+1, text+1); + <B><FONT COLOR="#A020F0">return</FONT></B> 0; +} + +<B><FONT COLOR="#228B22">int</FONT></B> <B><FONT COLOR="#0000FF">match</FONT></B>(<B><FONT COLOR="#228B22">char</FONT></B> *re, <B><FONT COLOR="#228B22">char</FONT></B> *text) { + <B><FONT COLOR="#A020F0">if</FONT></B> (re[0] == <B><FONT COLOR="#BC8F8F">'^'</FONT></B>) + <B><FONT COLOR="#A020F0">return</FONT></B> matchhere(re+1, text); + <B><FONT COLOR="#A020F0">do</FONT></B> { + <B><FONT COLOR="#A020F0">if</FONT></B> (matchhere(re, text)) + <B><FONT COLOR="#A020F0">return</FONT></B> 1; + } <B><FONT COLOR="#A020F0">while</FONT></B> (*text++ != <B><FONT COLOR="#BC8F8F">'\0'</FONT></B>); + <B><FONT COLOR="#A020F0">return</FONT></B> 0; +} + +<I><FONT COLOR="#B22222">/* + * Harness for testing with KLEE. + */</FONT></I> + +<I><FONT COLOR="#B22222">// The size of the buffer to test with. +</FONT></I>#<B><FONT COLOR="#5F9EA0">define</FONT></B> <FONT COLOR="#B8860B">SIZE</FONT> 7 + +<B><FONT COLOR="#228B22">int</FONT></B> <B><FONT COLOR="#0000FF">main</FONT></B>() { + <I><FONT COLOR="#B22222">// The input regular expression. +</FONT></I> <B><FONT COLOR="#228B22">char</FONT></B> re[SIZE]; + + <I><FONT COLOR="#B22222">// Make the input symbolic. +</FONT></I> klee_make_symbolic_name(re, <B><FONT COLOR="#A020F0">sizeof</FONT></B> re, <B><FONT COLOR="#BC8F8F">"re"</FONT></B>); + + <I><FONT COLOR="#B22222">// Try to match against a constant string "hello". +</FONT></I> match(re, <B><FONT COLOR="#BC8F8F">"hello"</FONT></B>); + + <B><FONT COLOR="#A020F0">return</FONT></B> 0; +} +</PRE> +<HR> +<ADDRESS>Generated by <A HREF="http://www.iki.fi/~mtr/genscript/">GNU enscript 1.6.4</A>.</ADDRESS> +</BODY> +</HTML> |