Developer's guide by Dan Liew, with a few changes from me.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@185351 91177308-0d34-0410-b5e6-96231b3b80d8
author: Cristian Cadar <cristic@cs.stanford.edu> 2013-07-01 18:01:01 +0000
committer: Cristian Cadar <cristic@cs.stanford.edu> 2013-07-01 18:01:01 +0000
commit: e4ce97b38411de5d972ee4cf89cede342b7f82f0 (patch)
tree: ef6f5e1f7c9b023f544eb451d79b50341b9cac3f
parent: 8e7a137e640823dae8364e1fc928dfb34f7271bb (diff)
download: klee-e4ce97b38411de5d972ee4cf89cede342b7f82f0.tar.gz
3 files changed, 127 insertions, 5 deletions
diff --git a/www/Documentation.html b/www/Documentation.html
index 8c19b36e..538cada7 100644
--- a/www/Documentation.html
+++ b/www/Documentation.html
@@ -47,6 +47,10 @@
       Some information about the Coreutils experiments presented in our <a href="http://www.doc.ic.ac.uk/~cristic/papers/klee-osdi-08.pdf">KLEE OSDI'08 paper</a>.
     </li>
 
+    <li>
+      <a href="developers-guide.html">Developer's Guide</a>: 
+      A brief guide on working with the KLEE source code.
+    </li>
   </ol>
 </div>
 </body>
diff --git a/www/GetInvolved.html b/www/GetInvolved.html
index 0cde1299..2ff2b5ee 100644
--- a/www/GetInvolved.html
+++ b/www/GetInvolved.html
@@ -36,12 +36,16 @@ and also fill a bug report on <a href="http://llvm.org/bugs/">Bugzilla</a></a> u
   
 <h2>Working with the Code</h2>
 
-<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> You should first check <a href="developers-guide.html">KLEE's developer's guide</a>.</p>  
+  
+<p>Developer documentation is written in 
+ <a href="http://t1.minormatter.com/~ddunbar/klee-doxygen/index.html">doxygen</a>.
+<!-- (this page is updated nightly from the source tree).-->
+</p>
+
+</p>
 
-<p>Many parts of KLEE rely on the LLVM infrastructure, you can find more
-information about programming for LLVM here:
+<p>Many parts of KLEE rely on the LLVM infrastructure, so you might also want to look at 
 <a href="http://llvm.org/docs/#llvmprog">LLVM's General Programming Documentation</a>.</p>
 
 </div>
diff --git a/www/developers-guide.html b/www/developers-guide.html
new file mode 100644
index 00000000..9c0ff719
--- /dev/null
+++ b/www/developers-guide.html
@@ -0,0 +1,114 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN"
+          "http://www.w3.org/TR/html4/strict.dtd">
+<html>
+<head>
+  <META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1" />
+  <title>KLEE - Getting Started</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>KLEE Developer's Guide</h1>
+ 
+<p>This guide covers several areas of KLEE that may not be imediately obvious to new developers.</p>
+
+ <h3>
+  <a href="#build"> 1. KLEE's Build System</a> <br/>
+  <a href="#tests"> 2. KLEE's Test Framework</a> <br/>
+  <a href="#misc"> 3. Miscellaneous</a> <br/>
+</h3>
+
+<h2 id="build">KLEE's Build System</h2>
+<p>KLEE uses LLVM's ability to build third-party projects, which is described <a href="http://llvm.org/docs/Projects.html">here</a>. The build system uses <a href="http://www.gnu.org/software/autoconf/">GNU Autoconf</a> and <a href="http://www.gnu.org/savannah-checkouts/gnu/autoconf/manual/autoconf-2.69/html_node/autoheader-Invocation.html">AutoHeader</a> to configure the build, but does not use the rest of GNU Autotools (e.g. automake).</p>
+
+<p>LLVM's build system supports out-of-source builds and therefore so does KLEE. It is highly recommended you take advantage of this. For example, you could create three builds (Release, Release with debug symbols, Debug) 
+   that all use the same source tree. This allows you keep your source tree clean and allows multiple configurations to be tested from a single source tree.</p>
+
+<h3>Setting up a debug build of KLEE</h3>
+<p>Setting up a debug build of KLEE (we'll assume it is an out-of-source build) is very similar to the build process described in <a href="GetStarted.html">Getting Started</a>, with the exception of steps 6 and 7.</p>
+
+  <ol start="6">
+	<li>Now we will configure KLEE. Notice that we are forcing the compiler to produce unoptimised code, this isn't the default behaviour.
+	    <div class="instr">
+	      $ mkdir path/to/build-dir <br/>
+	      $ cd path/to/build-dir <br/>
+	      $ CXXFLAGS="-g -O0" CFLAGS="-g -O0" path/to/source-dir/configure --with-llvm=<i>path/to/llvm</i>  --with-stp=<i>path/to/stp/install</i> --with-uclibc=<i>path/to/klee-uclibc</i> --enable-posix-runtime --with-runtime=Debug+Asserts
+	    </div>
+	Note if you're using an out-of-source build of LLVM you will need to use <tt>--with-llvmsrc=</tt> and <tt>--with-llvmobj=</tt> configure options instead of <tt>--with-llvm=</tt>
+	</li>
+	<li>Now we can build KLEE.
+	    <div class="instr">
+	      $ make -j
+	    </div>
+	    Note that we are using the <tt>-j</tt> option of make to speed up the compilation process.
+	</li>
+  </ol>
+
+<p>Note that KLEE depends on LLVM and STP.  If you need to debug KLEE's calls to that code, then you will need to build LLVM/STP with debug support too.</p>
+
+<h3>Adding a class</h3>
+  <p>Because KLEE uses LLVM's build system, adding a class to an existing library in KLEE is very simple. For example, to add a class to <tt>libkleaverExpr</tt>, the following steps would be followed:
+    <ol>
+       <li>Create the header file (<tt>.h</tt>) for the class and place it somewhere inside <tt>include/</tt> (the location isn't really important except that <tt>#include</tt> is relative to the <tt>include/</tt> directory).
+       </li>
+       <li>Create the source file (<tt>.cpp</tt>) for the class place it in <tt>lib/Expr/</tt>. You can confirm that the library in which your new class will be included is <tt>kleaverExpr</tt> by looking at the <tt>Makefile</tt> in <tt>lib/Expr</tt>.
+       </li>
+    </ol>
+    That's it! Now LLVM's build system will detect the new <tt>.cpp</tt> file and add it to the library that is generated when you run <tt>make</tt>.
+  </p>
+
+<h3>Building code documentation</h3>
+  <p>KLEE uses <a href="http://www.doxygen.org">Doxygen</a> to generate code documentation. To generate it yourself you can run the following from KLEE's build directory root.
+    <div class="instr">
+      $ make doxygen
+    </div>
+  This will generate documentation in <tt>path/to/build-dir/docs/doxygen/</tt> folder. You can also find KLEE's latest official code documentation <a href="http://test.minormatter.com/~ddunbar/klee-doxygen/index.html">here</a>
+  </p>
+
+
+<h2 id="tests">KLEE's Test Framework</h2>
+<p>KLEE uses LLVM's testing infrastructure for its tests, which itself uses <a href="http://www.gnu.org/software/dejagnu/">DejaGnu</a>. These are the tests that are executed by the <tt>make check</tt> command. Some documentation on LLVM's testing infrastructure can be found <a href="http://llvm.org/docs/TestingGuide.html#rtcustom">here</a>.
+ </p>    
+ <p>KLEE's tests are currently divided into categories, each of which is a subdirectory in <tt>test/</tt> in the source tree (e.g. <tt>test/Feature</tt>) . The <tt>dg.exp</tt> file in each subdirectory instructs the LLVM testing infrastructure which files in the subdirectory are to be used as tests. For example, <tt>test/Expr/dg.exp</tt> contains:
+    <div class="instr">
+	load_lib llvm.exp <br/><br/>
+
+	RunLLVMTests [lsort [glob -nocomplain $srcdir/$subdir/*.{pc}]]
+   </div>
+   This instructs the testing infrastructure that every <tt>.pc</tt> file in <tt>test/Expr</tt> should be used as a test.
+ </p>
+ <p>The actions performed in each test are specified by special comments in the file. For example, in <tt>test/Feature/ByteSwap.c</tt> the first two lines are
+    <div class="instr">
+     // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc <br/>
+     // RUN: %klee --libc=klee --exit-on-error %t1.bc <br/>
+   </div>
+   This first runs <tt>llvm-gcc</tt> on the source file (<tt>%s</tt>) and generates a temporary file (<tt>%t1.bc</tt>). Then KLEE is executed on this generated temporary file. If either program returns a non-zero exit code (or crashes) then 
+   test is considered to have failed. More information on the available substitution variables (such as <tt>%s</tt>) can be found <a href="http://llvm.org/releases/3.1/docs/TestingGuide.html#rtvars">here</a>.
+ </p>
+
+ <p>It is useful to be able to execute just a single test rather than all of them. KLEE provides a makefile target for doing so which can used as shown below. Note that <i>category/test-name</i> should be the test that one would like to execute, e.g. <tt>Feature/ByteSwap.c</tt>.
+    <div class="instr">
+    $ cd path/to/build-dir/test <br/>
+    $ make check-one TESTONE=path/to/source-dir/test/<i>category/test-name</i>
+    </div>
+ </p>
+
+    
+<h2 id="misc">Miscellaneous</h2>
+<h3>Writing messages to standard error</h3>
+<p>The <tt>kleeCore</tt> library (<tt>lib/Core</tt>) provides several functions that can be used similarly to <tt>printf()</tt> in C. See <tt>lib/Core/Common.h</tt> for more information.
+</p>
+
+<h3>Adding a command line option to a tool</h3>
+  <p>KLEE uses LLVM's CommandLine library for adding options to tools in KLEE, which is well documented <a href="http://llvm.org/docs/CommandLine.html">here</a>. See <tt>lib/core/Executor.cpp</tt> for examples.</p>
+
+<br/>
+    
+</div>
+</body>
+</html>
author	Cristian Cadar <cristic@cs.stanford.edu>	2013-07-01 18:01:01 +0000
committer	Cristian Cadar <cristic@cs.stanford.edu>	2013-07-01 18:01:01 +0000
commit	e4ce97b38411de5d972ee4cf89cede342b7f82f0 (patch)
tree	ef6f5e1f7c9b023f544eb451d79b50341b9cac3f
parent	8e7a137e640823dae8364e1fc928dfb34f7271bb (diff)
download	klee-e4ce97b38411de5d972ee4cf89cede342b7f82f0.tar.gz