Start basic Regexp.c example for klee.

 - A few other web page tweaks.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72215 91177308-0d34-0410-b5e6-96231b3b80d8

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">&lt;klee/klee.h&gt;</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> &amp;&amp; (*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> &amp;&amp; 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> &amp;&amp; (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">&quot;re&quot;</FONT></B>);
+
+  <I><FONT COLOR="#B22222">// Try to match against a constant string &quot;hello&quot;.
+</FONT></I>  match(re, <B><FONT COLOR="#BC8F8F">&quot;hello&quot;</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>