[llvm-commits] [klee] r72215 - in /klee/trunk/www: Examples.html GetInvolved.html GetStarted.html menu.html.incl resources/ resources/Regexp.c.html
Daniel Dunbar
daniel at zuster.org
Thu May 21 09:28:55 PDT 2009
Author: ddunbar
Date: Thu May 21 11:28:43 2009
New Revision: 72215
URL: http://llvm.org/viewvc/llvm-project?rev=72215&view=rev
Log:
Start basic Regexp.c example for klee.
- A few other web page tweaks.
Added:
klee/trunk/www/resources/
klee/trunk/www/resources/Regexp.c.html
Modified:
klee/trunk/www/Examples.html
klee/trunk/www/GetInvolved.html
klee/trunk/www/GetStarted.html
klee/trunk/www/menu.html.incl
Modified: klee/trunk/www/Examples.html
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/www/Examples.html?rev=72215&r1=72214&r2=72215&view=diff
==============================================================================
--- klee/trunk/www/Examples.html (original)
+++ klee/trunk/www/Examples.html Thu May 21 11:28:43 2009
@@ -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>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 tools.</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>FIXME: Write: show the important klee options.</p>
+<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>
Modified: klee/trunk/www/GetInvolved.html
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/www/GetInvolved.html?rev=72215&r1=72214&r2=72215&view=diff
==============================================================================
--- klee/trunk/www/GetInvolved.html (original)
+++ klee/trunk/www/GetInvolved.html Thu May 21 11:28:43 2009
@@ -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>
Modified: klee/trunk/www/GetStarted.html
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/www/GetStarted.html?rev=72215&r1=72214&r2=72215&view=diff
==============================================================================
--- klee/trunk/www/GetStarted.html (original)
+++ klee/trunk/www/GetStarted.html Thu May 21 11:28:43 2009
@@ -39,12 +39,12 @@
<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).
Modified: klee/trunk/www/menu.html.incl
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/www/menu.html.incl?rev=72215&r1=72214&r2=72215&view=diff
==============================================================================
--- klee/trunk/www/menu.html.incl (original)
+++ klee/trunk/www/menu.html.incl Thu May 21 11:28:43 2009
@@ -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>
Added: klee/trunk/www/resources/Regexp.c.html
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/www/resources/Regexp.c.html?rev=72215&view=auto
==============================================================================
--- klee/trunk/www/resources/Regexp.c.html (added)
+++ klee/trunk/www/resources/Regexp.c.html Thu May 21 11:28:43 2009
@@ -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>
More information about the llvm-commits
mailing list