diff options
| -rw-r--r-- | www/CoreutilsExperiments.html | 158 | ||||
| -rw-r--r-- | www/Documentation.html | 57 | ||||
| -rw-r--r-- | www/GetInvolved.html | 53 | ||||
| -rw-r--r-- | www/GetStarted.html | 244 | ||||
| -rw-r--r-- | www/KQuery.html | 620 | ||||
| -rw-r--r-- | www/OpenProjects.html | 91 | ||||
| -rw-r--r-- | www/Publications.html | 402 | ||||
| -rw-r--r-- | www/TestingCoreutils.html | 893 | ||||
| -rw-r--r-- | www/Tutorial-1.html | 187 | ||||
| -rw-r--r-- | www/Tutorial-2.html | 287 | ||||
| -rw-r--r-- | www/Tutorials.html | 38 | ||||
| -rw-r--r-- | www/bugs.html | 24 | ||||
| -rw-r--r-- | www/content.css | 75 | ||||
| -rw-r--r-- | www/content/coreutils_kc_0.png | bin | 0 -> 277141 bytes | |||
| -rw-r--r-- | www/content/coreutils_kc_1.png | bin | 0 -> 232377 bytes | |||
| -rw-r--r-- | www/developers-guide.html | 114 | ||||
| -rw-r--r-- | www/index.html | 36 | ||||
| -rw-r--r-- | www/klee-dev.html | 31 | ||||
| -rw-r--r-- | www/klee-files.html | 137 | ||||
| -rw-r--r-- | www/klee-options.html | 99 | ||||
| -rw-r--r-- | www/klee-tools.html | 84 | ||||
| -rw-r--r-- | www/menu.css | 39 | ||||
| -rw-r--r-- | www/menu.html.incl | 31 | ||||
| -rw-r--r-- | www/resources/Regexp.c.html | 78 | ||||
| -rw-r--r-- | www/resources/get_sign.c.html | 37 | ||||
| -rw-r--r-- | www/resources/islower.c.html | 33 |
26 files changed, 3848 insertions, 0 deletions
diff --git a/www/CoreutilsExperiments.html b/www/CoreutilsExperiments.html new file mode 100644 index 00000000..c0f0829c --- /dev/null +++ b/www/CoreutilsExperiments.html @@ -0,0 +1,158 @@ +<!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 - Coreutils Experiments</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>Coreutils Experiments</h1> + + <p> + This document is meant to give additional information regarding + the Coreutils experiments discussed in + our <a href="http://llvm.org/pubs/2008-12-OSDI-KLEE.html">KLEE + OSDI'08 paper</a>. However, please note that in the last several + years, KLEE and its dependencies (particularly LLVM and STP), have + undergone major changes, which have resulted in considerable + different behavior on several benchmarks, including Coreutils.</p> + + <p> + This document is structured as a series of FAQs: + </p> + + <ol> + <li>How did you build Coreutils?<br/> + Please follow the instructions in the <a href="TestingCoreutils.html">Coreutils Tutorial</a>. + </li> + + <li>What version of LLVM was used in the OSDI paper?<br/> + We generally kept in sync with the LLVM top-of-tree, which at the time + was somewhere around LLVM 2.2 and 2.3.</li> + </li> + + <li>What version of STP was used in the OSDI paper?<br/> + An old version of STP, which is still available as part of KLEE's + repository, in revisions up to r161056. + </li> + + <li>On what OS did you run your experiments?<br/> + We ran most experiments on a 32-bit Fedora machine with SELinux + support. The most important aspect is that this was a 32-bit + system: the constraints generated on a 64-bit system are typically + more complex and memory consumption might also increase. + </li> + + <li>What are the 89 Coreutils applications that you tested? <br/> + <div class="instr"> + [ base64 basename cat chcon chgrp chmod chown chroot cksum comm cp csplit cut date dd df dircolors dirname du echo env expand expr factor false fmt fold head hostid hostname id ginstall join kill link ln logname ls md5sum mkdir mkfifo mknod mktemp mv nice nl nohup od paste pathchk pinky pr printenv printf ptx pwd readlink rm rmdir runcon seq setuidgid shred shuf sleep sort split stat stty sum sync tac tail tee touch tr tsort tty uname unexpand uniq unlink uptime users wc whoami who yes + </div> + </li> + + <li>What options did you run KLEE with? <br/> + We used the following options (the command below is for paste): + <div class="instr"> +$ klee --simplify-sym-indices --write-cvcs --write-cov --output-module \ <br/> + --max-memory=1000 --disable-inlining --optimize --use-forked-stp \ <br/> + --use-cex-cache --with-libc --with-file-model=release \ <br/> + --allow-external-sym-calls --only-output-states-covering-new \ <br/> + --exclude-libc-cov --exclude-cov-file=./../lib/functions.txt \ <br/> + --environ=test.env --run-in=/tmp/sandbox --output-dir=paste-data-1h \ <br/> + --max-sym-array-size=4096 --max-instruction-time=10. --max-time=3600. \ <br/> + --watchdog --max-memory-inhibit=false --max-static-fork-pct=1 \ <br/> + --max-static-solve-pct=1 --max-static-cpfork-pct=1 --switch-type=internal \ <br/> + --randomize-fork --use-random-path --use-interleaved-covnew-NURS \ <br/> + --use-batching-search --batch-instructions 10000 --init-env \ <br/> + ./paste.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdout + </div> + + Some of these options have been renamed or removed in the current + version of KLEE. Most notably, the options "--exclude-libc-cov" + and "--exclude-cov-file" were implemented in a fragile way and we + decided to remove them from KLEE. The idea was to treat the + functions in libc or specified in a text file as "covered". (For + the Coreutils experiments, we were interested in covering the + code in the tools themselves, as opposed to library code, see the + paper for more details). If you plan to reimplement these + options in a clean way, please consider contributing your code to the mainline. + </li> + + <li>What are the options closest to the ones above that + work with the current version KLEE? </br> + Try the following: + + <div class="instr"> +$ klee --simplify-sym-indices --write-cvcs --write-cov --output-module \ <br/> + --max-memory=1000 --disable-inlining --optimize --use-forked-stp \ <br/> + --use-cex-cache --libc=uclibc --posix-runtime \ <br/> + --allow-external-sym-calls --only-output-states-covering-new \ <br/> + --environ=test.env --run-in=/tmp/sandbox \ <br/> + --max-sym-array-size=4096 --max-instruction-time=30. --max-time=3600. \ <br/> + --watchdog --max-memory-inhibit=false --max-static-fork-pct=1 \ <br/> + --max-static-solve-pct=1 --max-static-cpfork-pct=1 --switch-type=internal \ <br/> + --randomize-fork --search=random-path --search=nurs:covnew \ <br/> + --use-batching-search --batch-instructions=10000 \ <br/> + ./paste.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdout + </div> + + </li> + + <li>How do I generate test.env and /tmp/sandbox? <br/> + We used a simple environment and a "sandbox" directory to make + our experiments more deterministic. To recreate them, follow + these steps: + <ol type="a"> + <li>Download <tt>testing-env.sh</tt> by clicking <a href="http://www.doc.ic.ac.uk/~cristic/klee/klee-cu-testing-env.html">here</a>, and place it in the current directory.</li> + <li>Create <tt>test.env</tt> by running: + <div class="instr"> + $ env -i /bin/bash -c '(source testing-env.sh; env >test.env)' + </div> + </li> + <li>Download <tt>sandbox.tgz</tt> by clicking <a href="http://www.doc.ic.ac.uk/~cristic/klee/klee-cu-sandbox.html">here</a>, place it in <tt>/tmp</tt>, and run: + <div class="instr"> + $ cd /tmp + $ tar xzfv sandbox.tgz + </div> + </li> + </ol> + </li> + <li> + What symbolic arguments did you use in your experiments? <br/> + We ran most utilities using the arguments below. Our choice was + based on a high-level understanding of the Coreutils + applications: most behavior can be triggered with no more than two + short options, one long option, and two small input streams (stdin and one file). + <div class="instr"> + --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdout + </div> + + + + For eight tools where the coverage results were unsatisfactory, +we consulted the man page and increased the number and size of +arguments and files as follows: + <div class="instr"> + <b>dd:</b> --sym-args 0 3 10 --sym-files 1 8 --sym-stdout <br/> + <b>dircolors:</b> --sym-args 0 3 10 --sym-files 2 12 --sym-stdout <br/> + <b>echo:</b> --sym-args 0 4 300 --sym-files 2 30 --sym-stdout <br/> + <b>expr:</b> --sym-args 0 1 10 --sym-args 0 3 2 --sym-stdout <br/> + <b>mknod:</b> --sym-args 0 1 10 --sym-args 0 3 2 --sym-files 1 8 --sym-stdout <br/> + <b>od:</b> --sym-args 0 3 10 --sym-files 2 12 --sym-stdout <br/> + <b>pathchk:</b> --sym-args 0 1 2 --sym-args 0 1 300 --sym-files 1 8 --sym-stdout <br/> + <b>printf:</b> --sym-args 0 3 10 --sym-files 2 12 --sym-stdout + </div> + + </li> + + </ol> + + +</div> +</body> +</html> diff --git a/www/Documentation.html b/www/Documentation.html new file mode 100644 index 00000000..538cada7 --- /dev/null +++ b/www/Documentation.html @@ -0,0 +1,57 @@ +<!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 - Documentation</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 Documentation</h1> + <!--*********************************************************************--> + + <ol> + <li> + <a href="Tutorials.html">KLEE Tutorials</a>: + Simple examples of how to use KLEE to test programs. + </li> + + <li> + <a href="klee-options.html">KLEE Options</a>: + Overview of KLEE's main command-line options. + </li> + + <li> + <a href="klee-files.html">KLEE Generated Files</a>: + Overview of the main files generated by KLEE. + </li> + + <li> + <a href="klee-tools.html">KLEE Tools</a>: + Overview of the main auxiliary tools provided by KLEE. + </li> + + <li> + <a href="KQuery.html">KQuery Language Reference Manual</a>: + The reference manual for the KQuery language, used for interacting with + the KLEE solver (kleaver). + </li> + + <li> + <a href="CoreutilsExperiments.html">OSDI'08 Coreutils Experiments</a>: + 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> +</html> diff --git a/www/GetInvolved.html b/www/GetInvolved.html new file mode 100644 index 00000000..2ff2b5ee --- /dev/null +++ b/www/GetInvolved.html @@ -0,0 +1,53 @@ +<!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 - Get Involved</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>Getting Involved with the KLEE Project</h1> + +<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>Currently the main list for KLEE discussion (both for users and developers) +is <a href="klee-dev.html">klee-dev</a>.</p> + +<p>Commit messages to the KLEE repository go to +<a href="https://mailman.ic.ac.uk/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><a name="BugReports">Bug Reports</a></h2> + +<p>If you find a bug in KLEE, please report it on <a href="klee-dev.html">klee-dev</a> +and also fill a bug report on <a href="http://llvm.org/bugs/">Bugzilla</a></a> under the <b>klee</b> product.</p> + + +<h2>Working with the Code</h2> + +<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, so you might also want to look at +<a href="http://llvm.org/docs/#llvmprog">LLVM's General Programming Documentation</a>.</p> + +</div> +</body> +</html> diff --git a/www/GetStarted.html b/www/GetStarted.html new file mode 100644 index 00000000..7f6199dc --- /dev/null +++ b/www/GetStarted.html @@ -0,0 +1,244 @@ +<!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>Getting Started: Building and Running KLEE</h1> + +<!-- <p>FIXME: Intro and disclaimer.</p> --> + +<h3> +<a href="#cde">1. Trying out KLEE without installing any dependencies</a> <br/> +<a href="#build">2. Building KLEE</a> <br/> +</h3> + + +<h2 id="cde">Trying out KLEE without installing any dependencies</h2> + +<p> +If you would like to try out KLEE without the hassle of compiling or installing dependencies, <a href="http://keeda.stanford.edu/~pgbovine/klee-cde-package.v2.tar.bz2">download the self-contained package</a> (200MB), and follow the instructions in <tt>klee-cde-package/README</tt> to get up-and-running! +</p> + +<p> +This package contains a self-contained source+binary distribution of KLEE and all of its associated dependencies (e.g., llvm-2.7, llvm-gcc, uClibc, svn). Using this package, you can: +</p> + +<ol> +<li/> Compile target programs using llvm-gcc +<li/> Run KLEE on target programs compiled with llvm-gcc +<li/> Modify KLEE's source code, re-compile it to build a new KLEE binary, and then run the test suite using the new binary +<li/> Pull the latest KLEE source code updates from SVN +<li/> Run the entire <a href="TestingCoreutils.html">Coreutils case study</a> +</ol> + +<p> +... all without compiling or installing anything else on your Linux machine! +</p> + +<p> +The only requirement is that you are running a reasonably-modern x86-Linux distro that can execute 32-bit ELF binaries. This package was created using the <a href="http://www.pgbovine.net/cde.html">CDE auto-packaging tool</a>. +</p> + +<p> +<b>NOTE:</b> The CDE package is mainly meant for trying out KLEE on +some simple examples and the Coreutils case study. It is likely that +you will run into errors when testing other applications, in which +case you will need to follow the full installation instructions below. +</p> + + +<h2 id="build">Building KLEE</h2> + + +<p>The current procedure for building is outlined below.</p> + +<ol> + +<li><b>Install dependencies:</b> + +KLEE requires all the dependencies of LLVM, which are discussed <a href="http://llvm.org/docs/GettingStarted.html#requirements">here</a>. In particular, you should have the following packages (the list is likely not complete): g++, curl, dejagnu, subversion, bison, flex: + <div class="instr"> + $ sudo apt-get install g++ curl dejagnu subversion bison flex (Ubuntu) <br/> + $ sudo yum install g++ curl dejagnu subversion bison flex (Fedora) + </div> +</p> + +On some architectures, you might also need to set the following environment variables (best to put them in a config file like <b>.bashrc</b>): + <div class="instr"> + $ export C_INCLUDE_PATH=/usr/include/x86_64-linux-gnu <br/> + $ export CPLUS_INCLUDE_PATH=/usr/include/x86_64-linux-gnu + </div> + +<li><b>Build LLVM 2.9:</b> + +<p> +KLEE is built on top of <a href="http://llvm.org">LLVM</a>; the first +steps are to get a working LLVM installation. +See <a href="http://llvm.org/docs/GettingStarted.html">Getting Started +with the LLVM System</a> for more information. +</p> + +<p> +<b>NOTE:</b> KLEE is currently tested only on Linux x86-32 and x86-64 +targets, using <b>LLVM 2.9</b>. KLEE will not work with older LLVM +versions (e.g., 2.5), and might not work with newer versions (e.g., +3.0). +</p> + + +<ol type="a"> + <li>Install llvm-gcc: + <ul> + <li>Download and install the LLVM 2.9 release of <tt>llvm-gcc</tt> + from <a href="http://llvm.org/releases/download.html">here</a>. + + <br/>Add <tt>llvm-gcc</tt> to your <tt>PATH</tt>. It + is important to do this first so that <tt>llvm-gcc</tt> is + found in subsequent <tt>configure</tt> + steps. <tt>llvm-gcc</tt> will be used later to compile + programs that KLEE can execute. + </li> + + <li><b>Forgetting to add llvm-gcc to your PATH at this point is + by far the most common source of build errors reported by new + users.</b></li> + </ul> + </li> + + <li>Download and build LLVM 2.9: + <div class="instr"> + $ curl -O http://llvm.org/releases/2.9/llvm-2.9.tgz <br/> + $ tar zxvf llvm-2.9.tgz <br/> + $ cd llvm-2.9 <br/> + $ ./configure --enable-optimized --enable-assertions<br/> + $ make + </div> + + (the <tt>--enable-optimized</tt> configure argument is not necessary, but + KLEE runs very slowly in Debug mode). + </li> +</li> +</ol> + + +<li> <b>Build STP:</b> + +<p>KLEE is based on +the <a href="http://sites.google.com/site/stpfastprover/">STP</a> +constraint solver. STP does not make frequent releases, and its +Subversion repository is under constant development and may be +unstable. The instructions below are for a particular revision which +we have used successfully, but you can try a more recent revision by +changing or removing the <tt>-r</tt> argument to the <tt>svn co</tt> +command. (Please let us know if you have successfully and extensively +used KLEE with a more recent version of STP.) +</p> + +<div class="instr"> + $ svn co -r 940 https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp stp <br/> + $ cd stp <br/> + $ ./scripts/configure --with-prefix=<i>path/to/stp/install</i> --with-cryptominisat2 <br/> + $ make OPTIMIZE=-O2 CFLAGS_M32= install +</div> +</li> + +As documented on the STP website, it is essential to run the following +command before using STP (and thus KLEE): +<div class="instr"> + $ ulimit -s unlimited +</div> + + +<li>[Optional] <b>Build uclibc and the POSIX environment model:</b> + +<p> +By default, KLEE works on closed programs (programs that don't use any +external code such as C library functions). However, if you want to +use KLEE to run real programs you will want to enable the KLEE POSIX +runtime, which is built on top of the uClibc C library. +</p> + +<ol type="a"> + <li>Download KLEE's uClibc. KLEE uses a version + of <a href="http://uclibc.org">uClibc</a> which has been + modified slightly for our purposes. + <ul> + <li>A version that works on 32-bit Linux can be found + <a href="http://www.doc.ic.ac.uk/~cristic/klee/klee-uclibc-i386.html">here</a> + </li> + <li>A version that works on 64-bit Linux can be found + <a href="http://www.doc.ic.ac.uk/~cristic/klee/klee-uclibc-x64.html">here</a> + </li> + </ul> + </li> + + <li>Build uClibc with <tt>llvm-gcc</tt>: + <div class="instr"> + $ tar zxvf klee-uclibc-0.02.tgz <br/> + $ ./configure --with-llvm=<i>path/to/llvm</i> <br/> + $ make <br/> + </div> + + <p><b>NOTE:</b> If you are on a different target (i.e., not i386 + or x64), you will need to run <tt>make config</tt> and select the + correct target. The defaults for the other uClibc configuration + variables should be fine.<p> + </li> + + </ol> + + + <li><b>Checkout KLEE (to any path you like):</b> + <div class="instr"> + $ svn co http://llvm.org/svn/llvm-project/klee/trunk klee + </div> + Alternatively, if you prefer to use git there is also a + read-only git mirror, which syncs automatically with each + Subversion commit. You can do a git clone of KLEE via: + <div class="instr"> + $ git clone http://llvm.org/git/klee.git + </div> + </li> + + <li><b>Configure KLEE:</b> + <p>From the KLEE source directory, run:</p> + <div class="instr"> + $ ./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 + </div> + + <p><b>NOTE:</b> If you skipped step 4, simply remove the <tt>--with-uclibc</tt> and <tt>--enable-posix-runtime options</tt>. </p> + </li> + + <li><b>Build KLEE:</b> + <div class="instr"> + $ make ENABLE_OPTIMIZED=1 + </div> + </li> + + <li>Run the regression suite to verify your build: + <div class="instr"> + $ make check<br/> + $ make unittests<br/> + </div> + </li> + + <li>You're ready to go! Go to the <a href="Tutorials.html">Tutorials</a> page + to try KLEE.</li> +</ol> + +<p><b>NOTE:</b> If you are installing the system of Ubuntu 12.04 (or similar), you might want to take a look at this <a href="http://thread.gmane.org/gmane.comp.compilers.llvm.klee/923">message</a>.</p> +<br/> + +</div> +</body> +</html> diff --git a/www/KQuery.html b/www/KQuery.html new file mode 100644 index 00000000..a40f4435 --- /dev/null +++ b/www/KQuery.html @@ -0,0 +1,620 @@ +<!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 - KQuery Language Reference Manul</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>KQuery Language Reference Manual</h1> + + <h2>Table Of Contents</h2> + <ol> + <li><a href="#intro">Introduction</a></li> + <li><a href="#notation">Notation</a></li> + <li><a href="#structure">Structure</a></li> + <ol type="a"> + <li><a href="#expr_labels">Expression and Version Labels</a> + </ol> + <li><a href="#literals">Literals</a> + <ol type="a"> + <li><a href="#ident_literal">Identifiers</a></li> + <li><a href="#ident_number">Numbers</a></li> + <li><a href="#ident_types">Types</a></li> + </ol> + </li> + <li><a href="#decls">Declarations</a> + <ol type="a"> + <li><a href="#array_decls">Arrays</a></li> + <li><a href="#query_commands">Query Commands</a></li> + </ol> + </li> + <li><a href="#versions">Versions</a></li> + <li><a href="#exprs">Expressions</a> + <ol type="a"> + <li><a href="#primitive_expr">Primitive Expressions</a> + <ol type="i"> + <li><a href="#ref_primitive_expr">Expression References</a></li> + <li><a href="#const_primitive_expr">Constants</a></li> + </ol> + </li> + <li><a href="#arith_expr">Arithmetic Operations</a> + <ol type="i"> + <li><a href="#Add_expr">Add</a></li> + <li><a href="#Sub_expr">Sub</a></li> + <li><a href="#Mul_expr">Mul</a></li> + <li><a href="#UDiv_expr">UDiv</a></li> + <li><a href="#URem_expr">URem</a></li> + <li><a href="#SDiv_expr">SDiv</a></li> + <li><a href="#SRem_expr">SRem</a></li> + </ol> + </li> + <li><a href="#bit_expr">Bitwise Operations</a> + <ol type="i"> + <li><a href="#Not_expr">Not</a></li> + <li><a href="#And_expr">And</a></li> + <li><a href="#Or_expr">Or</a></li> + <li><a href="#Xor_expr">Xor</a></li> + <li><a href="#Shl_expr">Shl</a></li> + <li><a href="#LShr_expr">LShr</a></li> + <li><a href="#AShr_expr">AShr</a></li> + </ol> + </li> + <li><a href="#comp_expr">Comparisons</a> + <ol type="i"> + <li><a href="#Eq_expr">Eq</a></li> + <li><a href="#Ne_expr">Ne</a></li> + <li><a href="#Ult_expr">Ult</a></li> + <li><a href="#Ule_expr">Ule</a></li> + <li><a href="#Ugt_expr">Ugt</a></li> + <li><a href="#Uge_expr">Uge</a></li> + <li><a href="#Slt_expr">Slt</a></li> + <li><a href="#Sle_expr">Sle</a></li> + <li><a href="#Sgt_expr">Sgt</a></li> + <li><a href="#Sge_expr">Sge</a></li> + </ol> + </li> + <li><a href="#bv_expr">Bitvector Manipulation</a> + <ol type="i"> + <li><a href="#Concat_expr">Concat</a></li> + <li><a href="#Extract_expr">Extract</a></li> + <li><a href="#ZExt_expr">ZExt</a></li> + <li><a href="#SExt_expr">SExt</a></li> + </ol> + </li> + <li><a href="#special_expr">Special Expressions</a> + <ol type="i"> + <li><a href="#Read_expr">Read</a></li> + <li><a href="#Select_expr">Select</a></li> + </ol> + </li> + <li><a href="#macro_expr">Macro Expressions</a> + <ol type="i"> + <li><a href="#Neg_expr">Neg</a></li> + <li><a href="#ReadLSB_expr">ReadLSB</a></li> + <li><a href="#ReadMSB_expr">ReadMSB</a></li> + </ol> + </li> + </ol> + </li> + </ol> + + <h2><a name="intro">Introduction</a></h2> + + <p>The KQuery language is the textual representation of constraint + expressions and queries which is used as input to the Kleaver + constraint solver.</p> + + <p>Currently the language is capable of representing quantifier free + formulas over bitvectors and arrays, with direct support for all + standard operations on bitvectors. The language has been designed to + be compact and easy to read and write.</p> + + <p>The KQuery language is closely related to the C++ API for Exprs, see + also the + doxygen <a href="http://t1.minormatter.com/~ddunbar/klee-doxygen/classklee_1_1Expr.html">Expr</a> + documentation.</p> + + <h2><a name="notation">Notation</a></h2> + + <p>In this document, syntax is given in Extended Backus-Naur Form and appears as:</p> + <div class="syntax"> + "(" "Eq" [ type ] LHS RHS ")" + </div> + <p>Unless noted, the rules are described in terms of tokens not characters, + and tokens can be separate by white space and comments.</p> + + <p>In some case, a production like <i>child-expression</i> is used as an alias + for the <i>expression</i> production, when subsequent text needs to + differentiate the expression.</p> + + <p>Examples are shown using:</p> + <div class="example"> + (Eq w32 a b) + </div> + + <h2><a name="structure">Structure</a></h2> + + <p>A KQuery source file consists of a sequence of declarations.</p> + + <p><b>Syntax:</b></p> + <div class="syntax"> + kquery = { array-declaration | query-command } + </div> + + <p>Currently, the language supports two kinds of declarations:</p> + <ul> + <li><i><a href="#array_decls">Array Declarations</a></i>: Use to + declare an array of bitvectors for use in subsequent + expressions.</li> + + <li><i><a href="#query_commands">Query Commands</a></i>: Used to + define queries which should be executed by the constraint solver. A + query consists of a set of constraints (assumptions), a query + expression, and optionally expressions and arrays to compute values + for if the query expression is invalid.</li> + </ul> + + <p>Comments begin with "#" and continue until the end of line. For example:</p> + <div class="example"> + (Add w32 1 1) <font color="Red"># Two, hopefully</font> + </div> + + <h3><a name="expr_labels">Expression and Version Labels</a></h3> + + <p>Expressions are frequently shared among constraints and query + expressions. In order to keep the output succinct and readable, expression + labels can be used to introduce a lexical binding which can be used in + subsequent expressions. Expression labels are globally scoped through the + entire source file, and a definition must preceed any use in the source + file.</p> + + <p><b>Syntax:</b></p> + <div class="syntax"> + expression = identifier ":" expression<br> + </div> + + <p>Likewise, versions are frequently shared among reads and can be labelled in + the same fashion.</p> + + <p><b>Examples:</b></p> + <div class="example"> + (Add w32 N0:(Add w32 1 1) N0) <font color="Red"># Four</font><br><br> + array const_array[] : w32 -> w8 = [5,6]<br> + (Read w8 0 U0:[0=255] @ const_array) <font color="Red"># U0 now refers to an array [255,6]</font><br> + (Read w8 1 U0) <font color="Red"># Read from byte offset 1 of [255,6]</font><br> + </div> + + <h2><a name="literals">Literals</a></h2> + + <h3><a name="ident_literal">Identifiers</a></h3> + + <p>Identifiers are used for specifying array names and + for <a href="#expr_labels">expression labels</a>.</p> + + <p><b>Syntax:</b></p> + <div class="syntax"> + identifier = "[a-zA-Z_][a-zA-Z0-9._]*"<br> + </div> + + <p><b>Examples:</b></p> + <div class="example"> + _foo<br> + arr10_20<br> + </div> + + <p>Note that in order to keep open the possibility to introduce explicit + integral and floating-point types, the following identifiers are treated + as reserved keywords:</p> + <div class="syntax"> + floating-point-type = "fp[0-9]+([.].*)?"<br> + integer-type = "i[0-9]+"<br> + </div> + + <h3><a name="ident_number">Numbers</a></h3> + + <p>Numeric constants can be specified as follows.</p> + + <p><b>Syntax:</b></p> + <div class="syntax"> + number = "true" | "false" | signed-constant<br> + signed-constant = [ "+" | "-" ] ( dec-constant | bin-constant | oct-constant | hex-constant )<br> + dec-constant = "[0-9_]+"<br> + bin-constant = "0b[01_]+"<br> + oct-constant = "0o[0-7_]+"<br> + hex-constant = "0x[0-9a-fA-F_]+"<br> + </div> + + <p><b>Examples:</b></p> + <div class="example"> + false<br> + -10<br> + 0b1000_0001 <font color="Red"># 129 </font><br> + </div> + + <p>Non-decimal constants can be signed. The '_' character is ignored when + evaluating constants, but is available for use as a separator.</p> + + <h3><a name="ident_type">Types</a></h3> + + <p>Types are explicit operands to most expressions, and indicate the + bit-width of the type.</p> + + <p><b>Syntax:</b></p> + <div class="syntax"> + type = "w[0-9]+"<br> + </div> + + <p><b>Example:</b></p> + <div class="example"> + w32<br> + </div> + + <p>The numeric portion of the token is taken to be a decimal integer + specifying the bit-width of the type.</p> + + <h2><a name="decls">Declarations</a></h2> + + <h3><a name="array_decls">Arrays</a></h3> + + <p>Arrays are the basic type for defining symbolic variables (the + language does not currently support simple variables).</p> + + <p><b>Syntax:</b></p> + <div class="syntax"> + array-declaration = "array" name "[" [ size ] "]" ":" domain "->" range "=" array-initializer<br> + array-initializer = "symbolic" | "[" number-list "]"<br> + number-list = number | number "," number-list<br> + </div> + + <p>Arrays can be initialized to be either symbolic, or to have a given list of + constant values. For constant arrays, the initializer list must exactly match + the size of the array (if the size was unspecified, it will be the number of + constant values).</p> + + <p><b>Examples:</b></p> + <div class="example"> + array foo[10] : w32 -> w8 = symbolic <font color="Red"># A ten element symbolic array</font><br> + array foo[] : w8 -> w1 = [ true, false, false, true ] <font color="Red"># A constant array of four booleans</font><br> + </div> + + <h3><a name="query_commands">Query Commands</a></h3> + + <p>Query declarations describe the queries that the constraint solver + should run, along with optional additional arguments to specify + expressions and arrays for which counterexamples should be provided.</p> + + <p><b>Syntax:</b></p> + <div class="syntax"> + query-command = "(" "query" constraint-list query-expression [ eval-expr-list [ eval-array-list ] ] ")" <br> + query-expression = expression<br> + constraint-list = "[" { expression } "]" <br> + eval-expr-list = "[" { expression } "]" <br> + eval-array-list = "[" { identifier } "]" <br> + </div> + + <p><b>Examples:</b></p> + <div class="example"> + (query [] false)<br> + (query [(Eq w8 (Read w8 0 mem) 10)] false [] [ mem ])<br> + </div> + + <p>A query command consists a query, consisting of a constraint list and + a query expression, and two optional lists for use when a counterexample is desired.</p> + + <p>The <i>constraint-list</i> is a list of expressions (with boolean + type) which are assumed to hold. Although not required in the language, + many solvers require that this set of constraints be + consistent. The <i>query-expression</i> is the expression to determine + the validity of.</p> + + <p>If a counterexample is desired for invalid + queries, <i>eval-expr-list</i> is a list of expressions for which a + possible value should be constructed, and <i>eval-array-list</i> is a + list of arrays for which values for the entire array should be + provided. All counterexamples results must be simultaneously + feasible.</p> + + <h2><a name="versions">Versions</a></h2> + + <p>Versions are used to refer to an array with an ordered sequence of writes to it.</p> + + <p><b>Syntax:</b></p> + <div class="syntax"> + version = identifier | "[" [ update-list ] "]" "@" version<br> + update-list = lhs-expression "=" rhs-expression [ "," update-list ]<br> + </div> + + <p><b>Examples:</b></p> + <div class="example"> + array small_array[2] : w32 -> w8 = symbolic <font color="Red"># The array we will read from</font><br> + <br> + (Read w8 0 thing) <font color="Red"># No Updates to small_array</font><br> + (Read w8 1 [1=0xff] @ small_array) <font color="Red"># Read from small_array at byte offset 1 with update where byte 1 set to decimal 255</font><br> + </div> + <p>A version can be specified either by an identifier, which can refer to an + array or a <a href="#expr_labels">labelled version</a>, or by an explicit list + of writes which are to be concatenated to another version (the most recent + writes are first).</p> + + <h2><a name="exprs">Expressions</a></h2> + + <p>Expressions are strongly typed, and have the following general + form:</p> + <div class="syntax"> + "(" EXPR_NAME EXPR_TYPE ... arguments ... ")" + </div> + <p>where <i>EXPR_NAME</i> is the expression name, <i>EXPR_TYPE</i> is the + expression type (which may be optional), followed by any additional + arguments.</p> + + <h3><a name="primitive_expr">Primitive Expressions</a></h3> + + <h4><a name="ref_primitive_expr">Expression References</a></h4> + + <p>An expression reference can be used to refer to a + previously <a href="#expr_labels">labelled expression</a>.</p> + + <p><b>Syntax:</b></p> + <div class="syntax"> + expression = identifier<br> + </div> + + <p>Expression and version labels are in separate namespaces, it is the users + responsibility to use separate labels to preserve readability.</p> + + <h4><a name="const_primitive_expr">Constants</a></h4> + + <p>Constants are specified by a numeric token or a type and numeric + token.</p> + + <p><b>Syntax:</b></p> + <div class="syntax"> + expression = number | "(" type number ")"<br> + </div> + + <p>When a constant is specified without a type, the resulting expression + is only well-formed if its type can be inferred from the enclosing + context. The <b>true</b> and <b>false</b> constants always have + type <b>w1</b>. + + <p><b>Examples:</b></p> + <div class="example"> + true<br> + (w32 0)<br> + (Add w32 10 20) <font color="Red"># The type for 10 and 20 is inferred to be w32.</font><br> + </div> + + <h3><a name="arith_expr">Arithmetic Operations</a></h3> + + <h4><a name="Add_expr">Add</a>, + <a name="Sub_expr">Sub</a>, + <a name="Mul_expr">Mul</a>, + UDiv, SDiv, URem, SRem</h4> + + <p><b>Syntax:</b></p> + <div class="syntax"> + arithmetic-expr-kind = ( "Add" | "Sub" | "Mul" | "UDiv" | "URem" | "SDiv" | "SRem" )<br> + expression = "(" arithmetic-expr-kind type expression expression ")"<br> + </div> + + <p>Arithmetic operations are always binary and the types of the left- + and right-hand side expressions must match the expression type.</p> + + <h4><a name="UDiv_expr">UDiv</a></h4> + <p>Truncated unsigned division. Undefined if divisor is 0.</p> + + <h4><a name="URem_expr">URem</a></h4> + <p>Unsigned remainder. Undefined if divisor is 0.</p> + + <h4><a name="SDiv_expr">SDiv</a></h4> + <p>Signed division. Undefined if divisor is 0.</p> + + <h4><a name="SRem_expr">SRem</a></h4> + <p>Signed remainder. Undefined if divisor is 0. Sign of the + remainder is the same as that of the dividend.</p> + + + <h3><a name="bit_expr">Bitwise Operations</a></h3> + + <h4><a name="Not_expr">Not</a></h4> + + <p><b>Syntax:</b></p> + <div class="syntax"> + expression = "(" "Not" [ type ] expression ")" + </div> + + <p>Bitwise negation. The result is the bitwise negation (one's complement) of + the input expression. If the type is specified, it must match the expression + type.</p> + + <h4><a name="And_expr">And</a>, + <a name="Or_expr">Or</a>, + <a name="Xor_expr">Xor</a>, + <a name="Shl_expr">Shl</a>, + <a name="LShr_expr">LShr</a>, + <a name="AShr_expr">AShr</a></h4> + + <p><b>Syntax:</b></p> + <div class="syntax"> + bitwise-expr-kind = ( "And" | "Or" | "Xor" | "Shl" | "LShr" | "AShr" )<br> + expression = "(" bitwise-expr-kind type expression expression ")"<br> + </div> + + <p>These bitwise operations are always binary and the types of the left- and + right-hand side expressions must match the expression type.</p> + + <h4><a name="Shl">Shl</a></h4> + + <div class="syntax"> + expression = "(" "Shl" type X Y ")" + </div> + + <p>Logical shift left. Moves each bit of <b>X</b> to the left + by <b>Y</b> positions. The <b>Y</b> right-most bits of <b>X</b> are + replaced with zero, and the left-most bits discarded.</p> + + <h4><a name="LShr">LShr</a></h4> + + <div class="syntax"> + expression = "(" "LShr" type X Y ")" + </div> + + <p>Logical shift right. Moves each bit of <b>X</b> to the right + by <b>Y</b> positions. The <b>Y</b> left-most bits of <b>X</b> are + replaced with zero, and the right-most bits discarded.</p> + + + <h4><a name="AShr">AShr</a></h4> + + <div class="syntax"> + expression = "(" "AShr" type X Y ")" + </div> + + <p>Arithmetic shift right. Behaves as <b>LShr</b> except that the + left-most bits of <b>X</b> copy the initial left-most bit (the sign + bit) of <b>X</b>. + + <h3><a name="comp_expr">Comparisons</a></h3> + + <h4><a name="Eq_expr">Eq</a>, + <a name="Ne_expr">Ne</a>, + <a name="Ult_expr">Ult</a>, + <a name="Ule_expr">Ule</a>, + <a name="Ugt_expr">Ugt</a>, + <a name="Uge_expr">Uge</a>, + <a name="Slt_expr">Slt</a>, + <a name="Sle_expr">Sle</a>, + <a name="Sgt_expr">Sgt</a>, + <a name="Sge_expr">Sge</a></h4> + + <p><b>Syntax:</b></p> + <div class="syntax"> + comparison-expr-kind = ( "Eq" | "Ne" | "Ult" | "Ule" | "Ugt" | "Uge" | "Slt" | "Sle" | "Sgt" | "Sge" )<br> + expression = "(" comparison-expr-kind [ type ] expression expression ")"<br> + </div> + + <p>Comparison operations are always binary and the types of the left- + and right-hand side expression must match. If the type is specified, it + must be <b>w1</b>.</p> + + <h3><a name="bv_expr">Bitvector Manipulation</a></h3> + + <h4><a name="Concat_expr">Concat</a></h4> + + <p><b>Syntax:</b></p> + <div class="syntax"> + expression = "(" "Concat" [type] msb-expression lsb-expression ")" + </div> + + <p><b>Concat</b> evaluates to a <i>type</i> bits formed by + concatenating <i>lsb-expression</i> to <i>msb-expression</i>.</p> + + <h4><a name="Extract_expr">Extract</a></h4> + + <p><b>Syntax:</b></p> + <div class="syntax"> + expression = "(" "Extract" type offset-number child-expression ")" + </div> + + <p><b>Extract</b> evaluates to <i>type</i> bits from <i>child-expression</i> + taken from <i>offset-number</i>, where <i>offset-number</i> is the index of + the least-significant bit in <i>child-expression</i> which should be + extracted. + + <h4><a name="ZExt_expr">ZExt</a></h4> + + <p><b>Syntax:</b></p> + <div class="syntax"> + expression = "(" "ZExt" type child-expression ")" + </div> + + <p><b>ZExt</b> evaluates to the lowest <i>type</i> bits + of <i>child-expression</i>, with undefined bits set to zero.</p> + + <h4><a name="SExt_expr">SExt</a></h4> + + <p><b>Syntax:</b></p> + <div class="syntax"> + expression = "(" "SExt" type input-expression ")" + </div> + + <p><b>SExt</b> evaluates to the lowest <i>type</i> bits + of <i>child-expression</i>, with undefined bits set to the most-significant + bit of <i>input-expression</i>.</p> + + <h3><a name="special_expr">Special Expressions</a></h3> + + <h4><a name="Read_expr">Read</a></h4> + + <p><b>Syntax:</b></p> + <div class="syntax"> + expression = "(" "Read" type index-expression version ")"<br> + </div> + + <p>The <b>Read</b> expression evaluates to the first write + in <i>version</i> for which <i>index-expression</i> is equivalent to + the index in the write. The type of the expression must match the range of the + root array in <i>version</i>, and the type + of <i>index-expression</i> must match the domain.</p> + + <h4><a name="Select_expr">Select</a></h4> + + <p><b>Syntax:</b></p> + <div class="syntax"> + expression = "(" "Select" type cond-expression true-expression false-expression ")"<br> + </div> + + <p>The <b>Select</b> expression evalues to <i>true-expression</i> if the + condition evaluates to true, and to <i>false-expression</i> if the condition + evaluates to false. The <i>cond-expression</i> must have type <b>w1</b>.</p> + + <p>Both the true and false expressions must be well-formed, regardless of the + condition expression. In particular, it is not legal for one of the + expressions to cause a division-by-zero during evaluation, even if + the <b>Select</b> expression will never evaluate to that expression.</p> + + <h3><a name="macro_expr">Macro Expressions</a></h3> + + <p>Several common expressions are not implemented directly in the Expr + library, but can be expressed in terms of other operations. A number of these + are implemented as "macros". The pretty printer recognizes and prints the + appropriate Expr forms as the macro, and the parser recognizes them and turns + them into the underlying representation.</p> + + <h4><a name="Neg_expr">Neg</a></h4> + + <p><b>Syntax:</b></p> + <div class="syntax"> + expression = "(" "Neg" [ type ] expression ")" + </div> + + <p>This macro form can be used to generate a <b>Sub</b> from zero.</p> + + <h4><a name="ReadLSB_expr">ReadLSB</a>, + <a name="ReadMSB_expr">ReadMSB</a></h4> + + <p><b>Syntax:</b></p> + <div class="syntax"> + expression = "(" "ReadLSB" type index-expression version ")"<br> + expression = "(" "ReadMSB" type index-expression version ")"<br> + </div> + + <p><b>ReadLSB</b> and <b>ReadMSB</b> can be used to simplify contiguous array + accesses. The type of the expression must be a multiple <i>N</i> of the array + range type. The expression expands to a concatenation of <i>N</i> read + expressions, where each read is done at a subsequent offset from + the <i>index-expression</i>. For <b>ReadLSB</b> (<b>ReadMSB</b>), the + concatentation is done such that the read at <i>index-expression</i> forms the + least- (most-) significant bits.</p> +</div> + +</body> +</html> diff --git a/www/OpenProjects.html b/www/OpenProjects.html new file mode 100644 index 00000000..d4a01964 --- /dev/null +++ b/www/OpenProjects.html @@ -0,0 +1,91 @@ +<!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 - Open Projects</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 Open Projects</h1> + <!--*********************************************************************--> + + This page lists a variety of open projects that are natural (and tractable) + extensions of KLEE and things that we would love to see people work on. If + you are interested in tackling any of the projects, please mail + <a href="klee-dev.html">klee-dev</a> + with your ideas -- or even better, your patches!.</a> + + <ul> + <li> + <em>Implement SMT support for Kleaver:</em> + + <p>We would like to make Kleaver (KLEE's constraint solver) a more viable + standalone product. One of the steps in this direction is to implement SMT + support. This would also allow us to enter Kleaver into + the <a href="http://www.smtcomp.org/2011/">SMT-COMP</a> theorem prover + competition, which would be a good proving ground for our optimizations + and benchmarking our underlying constraint solver (STP, currently) against + other implementations.</p> + </li> + + <li> + <em>Distributed Constraint Solving:</em> + + <p>Much of the execution time of KLEE is spent inside the constraint + solver. A natural extension would be to implement support for a + distributed constraint solver, which would run KLEE on a single machine, + but would farm out the constraints to be solved on a network of + machines.</p> + </li> + + <li> + <em>Improve User Interface:</em> + + <p>This is not a very glamorous project, but it is still + important. Currently, KLEE has a myriad of command line options and flags, + most of which are left over from its research project roots. In order to + promote KLEE's use as a user tool, we would like to clean up most of the + UI so that the default behavior matches best practice, and so that more + arcane or research-only options are hidden by default.</p> + </li> + + <li> + <em>Experiment With Other Constraint Solvers:</em> + + <p>For the most part, KLEE has been written so that it is possible to swap + in other constraint solvers, but we have never tried anything other than + STP. We would love to see the results of using other contraint solvers + (like Yices or Z3) with KLEE.</p> + </li> + + <li> + <em>Implement Expression Level Constraint Optimization:</em> + + <p>KLEE does not currently do much optimization of constraint expressions + before sending them to the constraint solver. We would like to have an + internal framework for doing optimization of constraint expressions (e.g., + (A & ~A) => 0) so that these optimizations are only done once instead of + on every solver query.</p> + + <p>In general, because KLEE is dealing with expressions which result from + dynamic execution traces, many expressions end up having constant + components. This means we can frequently apply the same optimizations a + compiler would do, but to much greater effect because we are more likely + to see constant values. For reference, see the kinds of optimizations done + by LLVM's InstCombine + pass <a href="http://llvm.org/viewvc/llvm-project/llvm/trunk/lib/Transforms/InstCombine/">here</a>.</p> + + <p>The bulk of this project involves defining a good framework for us to + apply optimizations to expressions, and for deciding when to attempt to + optimization expressions.</p> + </li> + </ul> +</div> +</body> +</html> diff --git a/www/Publications.html b/www/Publications.html new file mode 100644 index 00000000..2a2dd313 --- /dev/null +++ b/www/Publications.html @@ -0,0 +1,402 @@ +<!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 - Publications</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-related Publications and Systems</h1> + <!--*********************************************************************--> + + <p>Below you can find a list of papers that use or extend KLEE. + Papers are listed in chronological order. <br/>If you have used and + extended KLEE, please share your experience by having your paper + listed here (email klee-dev-owner or c.cadar AT imperial.ac.uk).</p> + + <ol start="0"> + <li> + <a href="http://www.doc.ic.ac.uk/~cristic/papers/klee-osdi-08.pdf"> + <em> + KLEE: Unassisted and Automatic Generation of High-Coverage Tests for + Complex Systems Programs + </em> + </a> + <br> + Cristian Cadar, Daniel Dunbar, Dawson Engler + <br> + USENIX Symposium on Operating Systems Design and Implementation (OSDI 2008) + <br> + December 8-10, 2008, San Diego, CA, USA + <br><br> + </li> + + <li> + <a href="http://www.isoc.org/isoc/conferences/ndss/10/pdf/01.pdf"> + <em> + Server-side Verification of Client Behavior in Online Games + </em> + </a> + <br> + Darrell Bethea, Robert Cochran, Michael Reiter + <br> + Network and Distributed System Security Symposium (NDSS 2010) + <br> + February 28 - March 3, San Diego, CA, USA + <br><br> + </li> + + <li> + <a href="http://www.comsys.rwth-aachen.de/fileadmin/papers/2010/2010-04-ipsn-sasnauskas-KleeNet.pdf"> + <em> + KleeNet: Discovering Insidious Interaction Bugs in Wireless Sensor Networks Before Deployment + </em> + </a> + <br> + Raimondas Sasnauskas, Olaf Landsiedel, Muhammad Hamad Alizai, + Carsten Weise, Stefan Kowalewski, Klaus Wehrle + <br> + ACM/IEEE International Conference on Information Processing in Sensor Networks (IPSN 2010) + <br> + April 12-16, 2010, Stockholm, Sweden + <br> + <b>KleeNet is available <a href="https://www.comsys.rwth-aachen.de/research/projects/kleenet/">here</a>.</b> + <br><br> + </li> + + <li> + <a href="http://dslab.epfl.ch/pubs/esd.pdf"> + <em> + Execution Synthesis: A Technique for Automated Software Debugging + </em> + </a> + <br> + Cristian Zamfir, George Candea + <br> + ACM SIGOPS/EuroSys European Conference on Computer Systems (EuroSys 2010) + <br> + April 13-16, 2010, Paris, France + <br><br> + </li> + + <li> + <a href="http://dslab.epfl.ch/pubs/revnic.pdf"> + <em> + Reverse Engineering of Binary Device Drivers with RevNIC + </em> + </a> + <br> + Vitaly Chipounov, George Candea + <br> + ACM SIGOPS/EuroSys European Conference on Computer Systems (EuroSys 2010) + <br> + April 13-16, 2010, Paris, France + <br><br> + </li> + + <li> + <a href="http://dslab.epfl.ch/pubs/ddt.pdf"> + <em> + Testing Closed-Source Binary Device Drivers with DDT + </em> + </a> + <br> + Volodymyr Kuznetsov, Vitaly Chipounov, George Candea + <br> + USENIX Annual Technical Conference (USENIX ATC 2010) + <br> + June 22-25, 2010, Boston, MA, USA + <br><br> + </li> + + <li> + <a href="http://rcs.cs.columbia.edu/papers/cui-tern-osdi10.pdf"> + <em> + Stable Deterministic Multithreading through Schedule Memoization + </em> + </a> + <br> + Heming Cui, Jingyue Wu, Chia-che Tsai, Junfeng Yang + <br> + USENIX Symposium on Operating Systems Design and Implementation (OSDI 2010) + <br> + October 4-6, 2010, Vancouver, BC, Canada + <br><br> + </li> + + <li> + <a href="http://security.ece.cmu.edu/aeg/aeg-ndss-2011.pdf"> + <em> + AEG: Automatic Exploit Generation + </em> + </a> + <br> + Thanassis Avgerinos, Sang Kil Cha, Brent Lim Tze Hao, David Brumley + <br> + Network and Distributed System Security Symposium (NDSS 2011) + <br> + February 6-9, 2011, San Diego, CA, USA + <br><br> + </li> + + <li> + <a href="http://www.cs.vu.nl/%7Eherbertb/papers/dde_ndss11-preprint.pdf"> + <em> + Howard: A Dynamic Excavator for Reverse Engineering Data Structures + </em> + </a> + <br> + Asia Slowinska, Traian Stancescu, Herbert Bos + <br> + Network and Distributed System Security Symposium (NDSS 2011) + <br> + February 6-9, 2011, San Diego, CA, USA + <br><br> + </li> + + <li> + <a href="http://dslab.epfl.ch/pubs/s2e.pdf?attredirects=0"> + <em> + S2E: A Platform for In Vivo Multi-Path Analysis of Software Systems + </em> + </a> + <br> + Vitaly Chipounov, Volodymyr Kuznetsov, George Candea + <br> + International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2011) + <br> + March 5-11, 2011, Newport Beach, CA + <br/> + <b>S2E is available <a href="http://s2e.epfl.ch/">here</a>.</b> + <br><br> + </li> + + <li> + <a href="http://dslab.epfl.ch/pubs/cloud9.pdf?attredirects=0"> + <em> + Parallel Symbolic Execution for Automated Real-World Software Testing + </em> + </a> + <br> + ACM SIGOPS/EuroSys European Conference on Computer Systems (EuroSys 2011) + <br/> + Stefan Bucur, Vlad Ureche, Cristian Zamfir, George Candea + <br/> + April 10-13, 2011, Salzburg, Austria + <br/> + <b>Cloud9 is available <a href="http://cloud9.epfl.ch/">here</a>.</b> + <br/><br/> + </li> + + <li> + <a href="http://www.doc.ic.ac.uk/~pcc03/eurosys11klee.pdf"> + <em> + Symbolic Crosschecking of Floating-Point and SIMD Code + </em> + </a> + <br/> + Peter Collingbourne, Cristian Cadar, Paul H. J. Kelly + <br/> + ACM SIGOPS/EuroSys European Conference on Computer Systems (EuroSys 2011) + <br/> + April 10-13, 2011, Salzburg, Austria + <br/><br/> + </li> + + <li> + <a href="http://keeda.stanford.edu/~daramos/papers/ucklee-cav-2011.pdf"> + <em> + Practical, Low-Effort Equivalence Verification of Real Code + </em> + </a> + <br/> + David Ramos, Dawson Engler + <br > + Computer Aided Verification (CAV 2011) + <br/> + July 16-20, 2011, Snowbird, UT, USA + <br/><br/> + </li> + + <li> + <a href="http://www.comsys.rwth-aachen.de/fileadmin/papers/2011/2011-06-icdcs-sasnauskas-sde.pdf"> + <em> + Scalable Symbolic Execution of Distributed Systems + </em> + </a> + <br> + Raimondas Sasnauskas, Oscar Soria Dustmann, Benjamin Lucien Kaminski, + Carsten Weise, Stefan Kowalewski, Klaus Wehrle + <br> + IEEE International Conference on Distributed Computing Systems (ICDCS 2011) + <br> + June 20-24, 2011, Minneapolis, MN, USA + <br><br> + </li> + + <li> + <a href="http://rcs.cs.columbia.edu/papers/peregrine-sosp11.pdf"> + <em> + Efficient Deterministic Multithreading through Schedule Relaxation + </em> + </a> + <br> + Heming Cui, Jingyue Wu, John Gallagher, Huayang Guo, Junfeng Yang + <br> + ACM Symposium on Operating Systems Principles (SOSP 2011) + <br> + October 23-26, 2011, Cascais, Portugal + <br><br> + </li> + + <li> + <a href="http://www.cs.utah.edu/~ligd/publications/KLOVER-CAV11.pdf"> + <em> + KLOVER: A Symbolic Execution and Automatic Test Generation Tool for C++ Programs + </em> + </a> + <br> + Guodong Li, Indradeep Ghosh and Sreeranga Rajan + <br> + International Conference on Computer Aided Verification (CAV 2011) + <br> + July 14-20, 2011, Cliff Lodge, Snowbird, UT, USA + <br><br> + </li> + + <li> + <a href="http://www.doc.ic.ac.uk/~cristic/papers/kleecl-hvc-11.pdf"> + <em> + Symbolic Testing of OpenCL Code + </em> + </a> + <br> + Peter Collingbourne, Cristian Cadar, Paul H. J. Kelly + <br> + Haifa Verification Conference (HVC 2011) + <br> + December 6-8, 2011, Haifa, Israel + <br><br> + </li> + + <li> + <a href="http://www.cs.utah.edu/formal_verification/GKLEE/ppopp12-gklee-accepted-version.pdf"> + <em> + GKLEE: Concolic Verification and Test Generation for GPUs + </em> + </a> + <br> + Guodong Li, Peng Li, Geof Sawaya, Ganesh Gopalakrishnan, Indradeep Ghosh, and Sreeranga P. Rajan + <br> + ACM Symposium on Principles and Practice of Parallel Programming (PPoPP 2012) + <br> + February 25-29, 2012, New Orleans, LA, USA + <br> + <b>GKLEE is available <a href="http://www.cs.utah.edu/formal_verification/GKLEE">here</a>.</b> + <br><br> + </li> + + <li> + <a href="http://www.doc.ic.ac.uk/~cristic/papers/zesti-icse-12.pdf"> + <em> + make test-zesti: A Symbolic Execution Solution for Improving Regression Testing + </em> + </a> + <br> + Paul Dan Marinescu, Cristian Cadar + <br> + International Conference on Software Engineering (ICSE 2012) + <br> + June 2-9, 2012, Zurich, Switzerland + <br> + <b>ZESTI is available <a href="http://srg.doc.ic.ac.uk/projects/zesti/">here</a>.</b> + <br><br> + </li> + + <li> + <a href="http://www.cc.gatech.edu/~orso/papers/jin.orso.ICSE12.pdf"> + <em> + BugRedux: Reproducing Field Failures for In-House Debugging + </em> + </a> + <br> + Wei Jin, Alessandro Orso + <br> + International Conference on Software Engineering (ICSE 2012) + <br> + June 2-9, 2012, Zurich, Switzerland + <br> + <b>BugRedux is available <a href="http://www.cc.gatech.edu/~wjin6/mypage/bugredux.html">here</a>.</b> + <br><br> + </li> + + <li> + <a href="http://dslab.epfl.ch/pubs/stateMerging.pdf"> + <em> + Efficient State Merging in Symbolic Execution + </em> + </a> + <br> + Volodymyr Kuznetsov, Johannes Kinder, Stefan Bucur, George Candea + <br> + Programming Language Design and Implementation (PLDI) + <br> + June 11-16, 2012, Beijing, China + <br><br> + </li> + + <li> + <a href="http://www.doc.ic.ac.uk/~cristic/papers/highcovpatch-spin-12.pdf"> + <em> + High-Coverage Symbolic Patch Testing + </em> + </a> + <br> + Paul Dan Marinescu, Cristian Cadar + <br> + SPIN Workshop on Model Checking of Software (SPIN 2012) + <br> + July 23-24, 2012, Oxford, UK + <br><br> + </li> + + <li> + <a href="http://earlbarr.com/publications/ariadne.pdf"> + <em> + Automatic Detection of Floating-Point Exceptions + </em> + </a> + <br> + Peter C. Rigby, Earl T. Barr, Christian Bird, Premkumar Devanbu, Daniel M. German + <br> + Principles of Programming Languages (POPL) + <br> + January 23-25, 2013, Rome, Italy + <br><br> + </li> + + <li> + <a href="http://www.stanford.edu/~suhabe/atc13-bugrara.pdf"> + <em> + Redundant State Detection for Dynamic Symbolic Execution + </em> + </a> + <br> + Suhabe Bugrara, Dawson Engler + <br> + USENIX Annual Technical Conference (USENIX ATC 2013) + <br> + June 26-28, 2013, San Jose, California. + <br><br> + </li> + + </ol> +</div> +</body> +</html> diff --git a/www/TestingCoreutils.html b/www/TestingCoreutils.html new file mode 100644 index 00000000..7ae49302 --- /dev/null +++ b/www/TestingCoreutils.html @@ -0,0 +1,893 @@ +<!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 - Coreutils Case Study</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>Coreutils Case Study</h1> + + <p> + As a more detailed explanation of using KLEE, we will look at how we did our + testing of <a href="http://www.gnu.org/software/coreutils/">GNU + Coreutils</a> using KLEE. + </p> + + <p>This tutorial assumes that you have configured and built KLEE + with <tt>uclibc</tt> and <tt>POSIX</tt> runtime support. + <p> + + <p>These tests were done on a 32-bit Linux machine. On a 64-bit + machine, we needed to also set the <tt>LD_LIBRARY_PATH</tt> environment + variable: + <pre> + export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/usr/lib64 (Fedora) + export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/usr/lib/x86_64-linux-gnu (Ubuntu) + </pre> + </p> + + <!--*********************************************************************--> + + <h2>Step 1: Build coreutils with gcov</h2> + + <p> + First you will need to download and unpack the source + for <a href="http://www.gnu.org/software/coreutils/">coreutils</a>. In this + example we use version 6.11 (one version later than what was used for our + OSDI paper). + </p> + + <p> + Before we build with LLVM, let's build a version of <i>coreutils</i> + with <em>gcov</em> support. We will use this later to get coverage + information on the test cases produced by KLEE. + </p> + + <p> + From inside the <i>coreutils</i> directory, we'll do the usual + configure/make steps inside a subdirectory (<tt>obj-gcov</tt>). Here are the + steps: + </p> + + <div class="instr"> + <pre> +<b>coreutils-6.11$ mkdir obj-gcov</b> +<b>coreutils-6.11$ cd obj-gcov</b> +<b>obj-gcov$ ../configure --disable-nls CFLAGS="-g -fprofile-arcs -ftest-coverage"</b> +<i>... verify that configure worked ...</i> +<b>obj-gcov$ make</b> +<b>obj-gcov$ make -C src arch hostname</b> +<i>... verify that make worked ...</i> </pre> + </div> + + <p> + We build with <tt>--disable-nls</tt> because this adds a lot of extra + initialization in the C library which we are not interested in testing. Even + though these aren't the executables that KLEE will be running on, we want to + use the same compiler flags so that the test cases KLEE generates are most + likely to work correctly when run on the uninstrumented binaries. + </p> + + <p> + You should now have a set of <tt>coreutils</tt> in + the <tt>objc-gcov/src</tt> directory. For example: + </p> + + <div class="instr"> + <pre> +<b>obj-gcov$ cd src</b> +src$ ls -l ls echo cat +-rwxr-xr-x 1 ddunbar ddunbar 164841 2009-07-25 20:58 cat +-rwxr-xr-x 1 ddunbar ddunbar 151051 2009-07-25 20:59 echo +-rwxr-xr-x 1 ddunbar ddunbar 439712 2009-07-25 20:58 ls +<b>src$ ./cat --version</b> +cat (GNU coreutils) 6.11 +Copyright (C) 2008 Free Software Foundation, Inc. +License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html> +This is free software: you are free to change and redistribute it. +There is NO WARRANTY, to the extent permitted by law. + +Written by Torbjorn Granlund and Richard M. Stallman.</pre> + </div> + + <p> + In addition, these executables should be built with <tt>gcov</tt> support, + so if you run one it will write a <tt>.gcda</tt> into the current + directory. That file contains information about exactly what code was + executed when the program ran. See + the <a href="http://gcc.gnu.org/onlinedocs/gcc/Gcov.html">Gcov + Documentation</a> for more information. We can use the <tt>gcov</tt> tool + itself to produce a human readable form of the coverage information. For + example: + </p> + + <div class="instr"> + <pre> +<b>src$ rm -f *.gcda</b> <i># Get rid of any stale gcov files</i> +<b>src$ ./echo</b> + +<b>src$ ls -l echo.gcda</b> +-rw-r--r-- 1 ddunbar ddunbar 1832 2009-08-04 21:14 echo.gcda +<b>src$ gcov echo</b> +File '../../src/system.h' +Lines executed:0.00% of 47 +../../src/system.h:creating 'system.h.gcov' + +File '../../lib/timespec.h' +Lines executed:0.00% of 2 +../../lib/timespec.h:creating 'timespec.h.gcov' + +File '../../lib/gettext.h' +Lines executed:0.00% of 32 +../../lib/gettext.h:creating 'gettext.h.gcov' + +File '../../lib/openat.h' +Lines executed:0.00% of 8 +../../lib/openat.h:creating 'openat.h.gcov' + +File '../../src/echo.c' +Lines executed:18.81% of 101 +../../src/echo.c:creating 'echo.c.gcov' </pre> + </div> + + <p> + By default <tt>gcov</tt> will show the number of lines executed in the + program (the <tt>.h</tt> files include code which was compiled + into <tt>echo.c</tt>). + </p> + + <!--*********************************************************************--> + + <h2>Step 2: Build <tt>coreutils</tt> with LLVM</h2> + + <p> + One of the difficult parts of testing real software using KLEE is that it + must be first compiled so that the final program is an LLVM bitcode file and + not a linked executable. The software's build system may be set up to use + tools such as 'ar', 'libtool', and 'ld', which do not in general understand + LLVM bitcode files. + </p> + + <p> + It depends on the actual project what the best way to do this is. For + coreutils, we use a helper script <tt>klee-gcc</tt>, which acts + like <tt>llvm-gcc</tt> but adds additional arguments to cause it to emit + LLVM bitcode files and to call <tt>llvm-ld</tt> to link executables. This + is <b>not</b> a general solution, and your mileage may vary. + </p> + + <!-- Discuss building other projects, the ./configure CC=llvm-gcc; make + LD=llvm-ld CFLAGS="-emit-llvm" trick works frequently. --> + + <p> + As before, we will build in a separate directory so we can easily access + both the native executables and the LLVM versions. Here are the steps: + </p> + + <div class="instr"> + <pre> +<b>coreutils-6.11$ mkdir obj-llvm</b> +<b>coreutils-6.11$ cd obj-llvm</b> +<b>obj-llvm$ ../configure --disable-nls CFLAGS="-g"</b> +<i>... verify that configure worked ...</i> +<b>obj-llvm$ make CC=/full/path/to/klee/scripts/klee-gcc</b> +<b>obj-llvm$ make -C src arch hostname CC=/full/path/to/klee/scripts/klee-gcc</b> +<i>... verify that make worked ...</i> </pre> + </div> + + <p> + Notice that we made two changes. First, we don't want to add <em>gcov</em> + instrumentation in the binary we are going to test using KLEE, so we left of + the <tt>-fprofile-arcs -ftest-coverage</tt> flags. Second, when running + make, we set the <tt>CC</tt> variable to point to our <tt>klee-gcc</tt> + wrapper script. + </p> + + <p> + If all went well, you should now have LLVM bitcode versions of coreutils! For + example: + </p> + + <div class="instr"> + <pre> +<b>obj-llvm$ cd src</b> +src$ ls -l ls echo cat +-rwxr-xr-x 1 ddunbar ddunbar 65 2009-07-25 23:40 cat +-rwxr-xr-x 1 ddunbar ddunbar 66 2009-07-25 23:43 echo +-rwxr-xr-x 1 ddunbar ddunbar 94 2009-07-25 23:38 ls +<b>src$ ./cat --version</b> +cat (GNU coreutils) 6.11 +Copyright (C) 2008 Free Software Foundation, Inc. +License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html> +This is free software: you are free to change and redistribute it. +There is NO WARRANTY, to the extent permitted by law. + +LLVM ERROR: JIT does not support inline asm! </pre> + </div> + + <p> + You may notice some funny things going on. To start with, the files are way + too small! Since we are actually producing LLVM bitcode files, the operating + system can't run them directly. What <tt>llvm-ld</tt> does to make it so we + can still run the resulting outputs is write a little shell script which + uses the LLVM interpreter to run the binaries; the actual LLVM bitcode + files have <tt>.bc</tt> appended. If we look a little closer: + </p> + + <div class="instr"> + <pre> +<b>src$ cat ls</b> +#!/bin/sh +lli=${LLVMINTERP-lli} +exec $lli \ + -load=/usr/lib/librt.so \ + ls.bc ${1+"$@"} +<b>src$ ls -l ls.bc</b> +-rwxr-xr-x 1 ddunbar ddunbar 643640 2009-07-25 23:38 ls.bc </pre> + </div> + + <p> + The other funny thing is that the version message doesn't all print out, the + LLVM interpreter emits a message about not supporting inline assembly. The + problem here is that <tt>glibc</tt> occasionally implements certain + operations using inline assembly, which the LLVM interpreter (<tt>lli</tt>) + doesn't understand. KLEE works around this problem by specially recognizing + certain common inline assembly sequences and turning them back into the + appropriate LLVM instructions before executing the binary. + </p> + + <!--*********************************************************************--> + + <h2>Step 3: Using KLEE as an interpreter</h2> + + <p> + At its core, KLEE is just an interpreter for LLVM bitcode. For example, here + is how to run the same <tt>cat</tt> command we did before, using KLEE. Note, + this step requires that you configured and built KLEE with <tt>uclibc</tt> + and <tt>POSIX</tt> runtime support (if you didn't, you'll need to go do that + now). + </p> + + <div class="instr"> + <pre> +<b>src$ klee --libc=uclibc --posix-runtime ./cat.bc --version</b> +KLEE: NOTE: Using model: /home/ddunbar/public/klee/Release/lib/libkleeRuntimePOSIX.bca +KLEE: output directory = "klee-out-3" +KLEE: WARNING: undefined reference to function: __signbitl +KLEE: WARNING: executable has module level assembly (ignoring) +KLEE: WARNING: calling external: syscall(54, 0, 21505, 177325672) +KLEE: WARNING: calling __user_main with extra arguments. +KLEE: WARNING: calling external: getpagesize() +KLEE: WARNING: calling external: vprintf(177640072, 183340048) +cat (GNU coreutils) 6.11 + +License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html> +This is free software: you are free to change and redistribute it. +There is NO WARRANTY, to the extent permitted by law. + +Written by Torbjorn Granlund and Richard M. Stallman. +KLEE: WARNING: calling close_stdout with extra arguments. +Copyright (C) 2008 Free Software Foundation, Inc. +KLEE: done: total instructions = 259357 +KLEE: done: completed paths = 1 +KLEE: done: generated tests = 1 + </div> + + <p> + We got a lot more output this time! Let's step through it, starting with the + KLEE command itself. The general form of a KLEE command line is first the + arguments for KLEE itself, then the LLVM bitcode file to execute + (<tt>cat.bc</tt>), and then any arguments to pass to the application + (<tt>--version</tt> in this case, as before). + </p> + + <p> + If we were running a normal native application, it would have been linked + with the C library, but in this case KLEE is running the LLVM bitcode file + directly. In order for KLEE to work effectively, it needs to have + definitions for all the external functions the program may call. We have + modified the <a href="http://www.uclibc.org">uClibc</a> C library + implementation for use with KLEE; the <tt>--libc=uclibc</tt> KLEE argument + tells KLEE to load that library and link it with the application before it + starts execution. + </p> + + <p> + Similarly, a native application would be running on top of an operating + system that provides lower level facilities like <tt>write()</tt>, which the + C library uses in its implementation. As before, KLEE needs definitions for + these functions in order to fully understand the program. We provide a POSIX + runtime which is designed to work with KLEE and the uClibc library to + provide the majority of operating system facilities used by command line + applications -- the <tt>--posix-runtime</tt> argument tells KLEE to link + this library in as well. + </p> + + <p> + As before, <tt>cat</tt> prints out its version information (note that this + time all the text is written out), but we now have a number of additional + information output by KLEE. In this case, most of these warnings are + innocuous, but for completeness here is what they mean: + </p> + + <ul> + <li><i>undefined reference to function: __signbitl</i>: This warning means + that the program contains a call to the function <tt>__signbitl</tt>, + but that function isn't defined anywhere (we would have seen a lot more + of these if we had not linked with uClibc and the POSIX runtime). If the + program actually ends up making a call to this function while it is + executing, KLEE won't be able to interpret it and may terminate the + program.</li> + + <li><i>executable has module level assembly (ignoring)</i>: Some file + compiled in to the application had file level inline-assembly, which KLEE + can't understand. In this case this comes from uClibc and is unused, so + this is safe.</li> + + <li><i>calling __user_main with extra arguments</i>: This indicates that + the function was called with more arguments than it expected, it is + almost always innocuous. In this case <tt>__user_main</tt> is actually + the <tt>main()</tt> function for <tt>cat</tt>, which KLEE has renamed it + when linking with uClibc. <tt>main()</tt> is being called with + additional arguments by uClibc itself during startup, for example the + environment pointer.</li> + + <li><i>calling external: getpagesize()</i>: This is an example of KLEE + calling a function which is used in the program but is never + defined. What KLEE actually does in such cases is try to call the native + version of the function, if it exists. This is sometimes safe, as long + as that function does write to any of the programs memory or attempt to + manipulate symbolic values. <tt>getpagesize()</tt>, for example, just + returns a constant.</li> + </ul> + + <p> + In general, KLEE will only emit a given warning once. The warnings are also + logged to <tt>warnings.txt</tt> in the KLEE output directory. + </p> + + <!--*********************************************************************--> + + <h2>Step 4: Introducing symbolic data to an application </h2> + + <p> + We've seen that KLEE can interpret a program normally, but the real purpose + of KLEE is to explore programs more exhaustively by making parts of their + input symbolic. For example, lets look at running KLEE on the <tt>echo</tt> + application. + </p> + + <p> + When using uClibc and the POSIX runtime, KLEE replaces the + program's <tt>main()</tt> function with a special function + (<tt>klee_init_env</tt>) provided inside the runtime library. This + function alters the normal command line processing of the + application, in particular to support construction of symbolic + arguments. For example, passing <tt>--help</tt> yields: + </p> + + <div class="instr"> + <pre> +<b>src$ klee --libc=uclibc --posix-runtime ./echo.bc --help</b> +<i>...</i> + +usage: (klee_init_env) [options] [program arguments] + -sym-arg <N> - Replace by a symbolic argument with length N + -sym-args <MIN> <MAX> <N> - Replace by at least MIN arguments and at most + MAX arguments, each with maximum length N + -sym-files <NUM> <N> - Make stdin and up to NUM symbolic files, each + with maximum size N. + -sym-stdout - Make stdout symbolic. + -max-fail <N> - Allow up to <N> injected failures + -fd-fail - Shortcut for '-max-fail 1' +<i>...</i> + </div> + + <p> + As an example, lets run <tt>echo</tt> with a symbolic argument of 3 + characters. + </p> + + <div class="instr"> + <pre> +<b>src$ klee --libc=uclibc --posix-runtime ./echo.bc --sym-arg 3</b> +KLEE: NOTE: Using model: /home/ddunbar/public/klee/Release/lib/libkleeRuntimePOSIX.bca +KLEE: output directory = "klee-out-16" +KLEE: WARNING: undefined reference to function: __signbitl +KLEE: WARNING: executable has module level assembly (ignoring) +KLEE: WARNING: calling external: syscall(54, 0, 21505, 189414856) +KLEE: WARNING: calling __user_main with extra arguments. +.. +KLEE: WARNING: calling close_stdout with extra arguments. +... +KLEE: WARNING: calling external: printf(183664896, 183580400) +Usage: ./echo.bc [OPTION]... [STRING]... +Echo the STRING(s) to standard output. + + -n do not output the trailing newline + -e enable interpretation of backslash escapes + -E disable interpretation of backslash escapes (default) + --help display this help and exit + --version output version information and exit + +If -e is in effect, the following sequences are recognized: + + \0NNN the character whose ASCII code is NNN (octal) + \\ backslash + \a alert (BEL) + \b backspace + \c suppress trailing newline + \f form feed + \n new line + \r carriage return + \t horizontal tab + \v vertical tab + +NOTE: your shell may have its own version of echo, which usually supersedes +the version described here. Please refer to your shell's documentation +for details about the options it supports. + +Report bugs to <bug-coreutils@gnu.org>. +KLEE: WARNING: calling external: vprintf(183956664, 190534360) +echo (GNU coreutils) 6.11 + +License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html> +This is free software: you are free to change and redistribute it. +There is NO WARRANTY, to the extent permitted by law. + +Written by FIXME unknown. +... +... +... + + + + +.. + + +. + +. +.. +... +Copyright (C) 2008 Free Software Foundation, Inc. +KLEE: done: total instructions = 300193 +KLEE: done: completed paths = 25 +KLEE: done: generated tests = 25<pre> + </div> + + <p> + The results here are slightly more interesting, KLEE has explored 25 paths + through the program. The output from all the paths is intermingled, but you + can see that in addition to echoing various random characters, some blocks + of text also were output. You may be suprised to learn that + coreutils' <tt>echo</tt> takes some arguments, in this case the + options <tt>--v</tt> (short for <tt>--version</tt>) and <tt>--h</tt> (short + for <tt>--help</tt>) were explored. We can get a short summary of KLEE's + internal statistics by running <tt>klee-stats</tt> on the output directory + (remember, KLEE always makes a symlink called <tt>klee-last</tt> to the most + recent output directory). + </p> + + <div class="instr"> + <pre> +<b>src$ klee-stats klee-last</b> +------------------------------------------------------------------------- +| Path | Instrs | Time(s) | ICov(%) | BCov(%) | ICount | Solver(%) | +------------------------------------------------------------------------- +| klee-last | 300673 | 1.47 | 28.18 | 17.37 | 28635 | 5.65 | +-------------------------------------------------------------------------</pre> + </div> + + <p> + Here <em>ICov</em> is the percentage of LLVM instructions which were + covered, and <em>BCov</em> is the percentage of branches that were + covered. You may be wondering why the percentages are so low -- how much + more code can echo have! The main reason is that these numbers are computed + using all the instructions or branches in the bitcode files; that includes a + lot of library code which may not even be executable. We can help with that + problem (and others) by passing the <tt>--optimize</tt> option to KLEE. This + will cause KLEE to run the LLVM optimization passes on the bitcode module + before executing it; in particular they will remove any dead code. When + working with non-trivial applications, it is almost always a good idea to + use this flag. Here are the results from running again + with <tt>--optimze</tt> enabled: + </p> + + <div class="instr"> + <pre> +<b>src$ klee --optimize --libc=uclibc --posix-runtime ./echo.bc --sym-arg 3</b> +<i>...</i> +KLEE: done: total instructions = 123251 +KLEE: done: completed paths = 25 +KLEE: done: generated tests = 25 +src$ klee-stats klee-last +------------------------------------------------------------------------- +| Path | Instrs | Time(s) | ICov(%) | BCov(%) | ICount | Solver(%) | +------------------------------------------------------------------------- +| klee-last | 123251 | 0.32 | 38.02 | 25.43 | 9531 | 29.66 | +-------------------------------------------------------------------------</pre> + </div> + + <p> + This time the instruction coverage went up by about ten percent, and you can + see that KLEE also ran faster and executed less instructions. Most of the + remaining code is still in library functions, just in places that the + optimizers aren't smart enough to remove. We can verify this -- and look for + uncovered code inside <tt>echo</tt> -- by using KCachegrind to visualize the + results of a KLEE run. + </p> + + <!--*********************************************************************--> + + <h2>Step 5: Visualizing KLEE's progress with <tt>kcachegrind</tt> </h2> + + <p> + <a href="http://kcachegrind.sourceforge.net">KCachegrind</a> is an excellent + profiling visualization tool, originally written for use with the callgrind + plugin for valgrind. If you don't have it already, it is usually easily + available on a modern Linux distribution via your platforms' software + installation tool (e.g., <tt>apt-get</tt> or <tt>yum</tt>). + </p> + + <p> + KLEE by default writes out a <tt>run.istats</tt> file into the test output + directory which is actually a KCachegrind file. In this example, + the <tt>run.istats</tt> is from a run without <tt>--optimize</tt>, so the + results are easier to understand. Assuming you have KCachegrind installed, + just run: + </p> + + <div class="instr"> + <pre> <b>src$ kcachegrind klee-last/run.istats</b> </pre> + </div> + + <p> + After KCachegrind opens, you should see a window that looks something like + the one below. You should make sure that the "Instructions" statistic is + selected by choosing "View" > "Primary Event Type" > "Instructions" + from the menu, and make sure the "Source Code" view is selected (the right + hand pane in the screenshot below). + </p> + + <a href="content/coreutils_kc_0.png"> + <img src="content/coreutils_kc_0.png" height=500></a> + + <p> + KCachegrind is a complex application in itself, and interested users should + see the KCachegrind website for more information and documentation. However, + the basics are that the one pane shows the "Flat Profile"; this is a list of + which how many instructions were executed in each function. The "Self" + column is the number of instructions which were executed in the function + itself, and the "Incl" (inclusive) column is the number of instructions + which were executed in the function, or any of the functions it called (or + its callees called, and so on). + </p> + + <p> + KLEE includes quite a few statistics about execution. The one we are + interested in now is "Uncovered Instructions", which will show which + functions have instructions which were never executed. If you select that + statistic and resort the list of functions, you should see something like + this: + </p> + + <a href="content/coreutils_kc_1.png"> + <img src="content/coreutils_kc_1.png" height=500></a> + + <p> + Notice that most of the uncovered instructions are in library code as we + would expect. However, if we select the <tt>__user_main</tt> function, we + can look for code inside <tt>echo</tt> itself that was uncovered. In this + case, most of the uncovered instructions are inside a large <tt>if</tt> + statement guarded by the variable <tt>do_v9</tt>. If you look a bit more, + you can see that this is a flag set to true when <tt>-e</tt> is passed. The + reason that KLEE never explored this code is because we only passed one + symbolic argument -- hitting this code requires a command line like <tt>$ + echo -e \a</tt>. + </p> + + <p> + One subtle thing to understand if you are trying to actually make sense of + the KCachegrind numbers is that they include events accumulated across all + states. For example, consider the following code: + </p> + + <div class="instr"> + <pre> +Line 1: a = 1; +Line 2: if (...) +Line 3: printf("hello\n"); +Line 4: b = c; </pre> + </div> + + <p> + In a normal application, if the statement on Line 1 was only executed once, + then the statement on Line 4 could be (at most) executed once. When KLEE is + running an application, however, it could fork and generate separate + processes at Line 2. In that case, Line 4 may be executed more times than + Line 1! + </p> + + <p> + Another useful tidbit: KLEE actually writes the <tt>run.istats</tt> file + periodically as the application is running. This provides one way to monitor + the status of long running applications (another way is to use the + klee-stats tool). + </p> + + <!--*********************************************************************--> + + <h2>Step 6: Replaying KLEE generated test cases </h2> + + <p> + Let's step away from KLEE for a bit and look at just the test cases KLEE + generated. If we look inside the <tt>klee-last</tt> we should see + 25 <tt>.ktest</tt> files. + </p> + + <div class="instr"> + <pre> +<b>src$ ls klee-last</b> +assembly.ll test000004.ktest test000012.ktest test000020.ktest +info test000005.ktest test000013.ktest test000021.ktest +messages.txt test000006.ktest test000014.ktest test000022.ktest +run.istats test000007.ktest test000015.ktest test000023.ktest +run.stats test000008.ktest test000016.ktest test000024.ktest +test000001.ktest test000009.ktest test000017.ktest test000025.ktest +test000002.ktest test000010.ktest test000018.ktest warnings.txt +test000003.ktest test000011.ktest test000019.ktest </pre> + </div> + + <p> + These files contain the actual values to use for the symbolic data in order + to reproduce the path that KLEE followed (either for obtaining code + coverage, or for reproducing a bug). They also contain additional metadata + generated by the POSIX runtime in order to track what the values correspond + to and the version of the runtime. We can look at the individual contents of + one file using <tt>ktest-tool</tt>: + </p> + + <div class="instr"> + <pre> +<b>$ ktest-tool klee-last/test000001.ktest</b> +ktest file : 'klee-last/test000001.ktest' +args : ['./echo.bc', '--sym-arg', '3'] +num objects: 2 +object 0: name: 'arg0' +object 0: size: 4 +object 0: data: '@@@\x00' +object 1: name: 'model_version' +object 1: size: 4 +object 1: data: '\x01\x00\x00\x00' </pre> + </div> + + <p> + In this case, the test case indicates that values "@@@\x00" should be passed + as the first argument. However, <tt>.ktest</tt> files generally aren't + really meant to be looked at directly. For the POSIX runtime, we provide a + tool <tt>klee-replay</tt> which can be used to read the <tt>.ktest</tt> file + and invoke the native application, automatically passing it the data + necessary to reproduce the path that KLEE followed. + </p> + + <p> + To see how it works, go back to the directory where we built the native + executables: + </p> + + <div class="instr"> + <pre> +<b>src$ cd ..</b> +<b>obj-llvm$ cd ..</b> +<b>coreutils-6.11$ cd obj-gcov</b> +<b>obj-gcov$ cd src</b> +<b>src$ ls -l echo</b> +-rwxr-xr-x 1 ddunbar ddunbar 151051 2009-07-25 20:59 echo </pre> + </div> + + <p> + To use the <tt>klee-replay</tt> tool, we just tell it the executable to run + and the <tt>.ktest</tt> file to use. The program arguments, input files, + etc. will all be constructed from the data in the <tt>.ktest</tt> file. + </p> + + <div class="instr"> + <pre> +<b>src$ klee-replay ./echo ../../obj-llvm/src/klee-last/test000001.ktest </b> +klee-replay: TEST CASE: ../../obj-llvm/src/klee-last/test000001.ktest +klee-replay: ARGS: "./echo" "@@@" +@@@ +klee-replay: EXIT STATUS: NORMAL (0 seconds) </pre> + </div> + + <p> + The first two and last lines here come from the <tt>klee-replay</tt> tool + itself. The first two lines list the test case being run, and the concrete + values for arguments that are being passed to the application (notice this + matches what we saw in the <tt>.ktest</tt> file earlier). The last line is + the exit status of the program and the elapsed time to run. + </p> + + <p> + We can also use the <tt>klee-replay</tt> tool to run a set of test cases at + once, one after the other. Let's do this and compare the <tt>gcov</tt> + coverage to the numbers we got from <tt>klee-stats</tt>: + </p> + + <div class="instr"> + <pre> +<b>src$ rm -f *.gcda</b> <i># Get rid of any stale gcov files</i> +<b>src$ klee-replay ./echo ../../obj-llvm/src/klee-last/*.ktest </b> +klee-replay: TEST CASE: ../../obj-llvm/src/klee-last/test000001.ktest +klee-replay: ARGS: "./echo" "@@@" +@@@ +klee-replay: EXIT STATUS: NORMAL (0 seconds) +<i>...</i> +klee-replay: TEST CASE: ../../obj-llvm/src/klee-last/test000022.ktest +klee-replay: ARGS: "./echo" "--v" +echo (GNU coreutils) 6.11 +Copyright (C) 2008 Free Software Foundation, Inc. +<i>...</i> + +<b>src$ gcov echo</b> +File '../../src/system.h' +Lines executed:6.38% of 47 +../../src/system.h:creating 'system.h.gcov' + +File '../../lib/timespec.h' +Lines executed:0.00% of 2 +../../lib/timespec.h:creating 'timespec.h.gcov' + +File '../../lib/gettext.h' +Lines executed:0.00% of 32 +../../lib/gettext.h:creating 'gettext.h.gcov' + +File '../../lib/openat.h' +Lines executed:0.00% of 8 +../../lib/openat.h:creating 'openat.h.gcov' + +File '../../src/echo.c' +Lines executed:50.50% of 101 +../../src/echo.c:creating 'echo.c.gcov' </pre> + </div> + + <p> + The number for <tt>echo.c</tt> here significantly higher than + the <tt>klee-stats</tt> number because <tt>gcov</tt> is only considering + lines in that one file, not the entire application. As with <tt>kcachegrind</tt>, we can inspect the coverage file output by <tt>gcov</tt> to see exactly what lines were covered and which weren't. Here is a fragment from the output: + </p> + + <div class="instr"> + <pre> + -: 193: } + -: 194: + 23: 195:just_echo: + -: 196: + 23: 197: if (do_v9) + -: 198: { + 10: 199: while (argc > 0) + -: 200: { + #####: 201: char const *s = argv[0]; + -: 202: unsigned char c; + -: 203: + #####: 204: while ((c = *s++)) + -: 205: { + #####: 206: if (c == '\\' && *s) + -: 207: { + #####: 208: switch (c = *s++) + -: 209: { + #####: 210: case 'a': c = '\a'; break; + #####: 211: case 'b': c = '\b'; break; + #####: 212: case 'c': exit (EXIT_SUCCESS); + #####: 213: case 'f': c = '\f'; break; + #####: 214: case 'n': c = '\n'; break; </pre> + </div> + + <p> + The far left hand column is the number of times each line was + executed; <b>-</b> means the line has no executable code, and <b>#####</b> + means the line was never covered. As you can see, the uncovered lines here + correspond exactly to the uncovered lines as reported + in <tt>kcachegrind</tt>. + </p> + + <p> + Before moving on to testing more complex applications, lets make sure we can + get decent coverage of the simple <tt>echo.c</tt>. The problem before was + that we weren't making enough data symbolic, providing echo with two + symbolic arguments should be plenty to cover the entire program. We can use + the POSIX runtime <tt>--sym-args</tt> option to pass multiple options. Here + are the steps, after switching back to the <tt>obj-llvm/src</tt> directory: + </p> + + <div class="instr"> + <pre> +<b>src$ klee --only-output-states-covering-new --optimize --libc=uclibc --posix-runtime ./echo.bc --sym-args 0 2 4</b> +<i> ... </i> +KLEE: done: total instructions = 7437521 +KLEE: done: completed paths = 9963 +KLEE: done: generated tests = 55 </pre> +</div> + + <p> + The format of the <tt>--sym-args</tt> option actually specifies a minimum + and a maximum number of arguments to pass and the length to use for each + argument. In this case <tt>--sym-args 0 2 4</tt> says to pass between 0 and + 2 arguments (inclusive), each with a maximum length of four characters. + </p> + + <p> + We also added the <tt>--only-output-states-covering-new</tt> option to the + KLEE command line. By default KLEE will write out test cases for every path + it explores. This becomes less useful <!-- and should become not the default + --> once the program becomes larger, because many test cases will end up + exercise the same paths, and computing (or even reexecuting) each one wastes + time. Using this option tells KLEE to only output test cases for paths which + covered some new instruction in the code (or hit an error). The final lines + of the output show that even though KLEE explored almost ten thousand paths + through the code, it only needed to write 55 test cases. + </p> + + <p> + If we go back to the <tt>obj-gcov/src</tt> directory and rerun the latest + set of test cases, we finally have reasonable coverage of <tt>echo.c</tt>: + </p> + + <div class="instr"> + <pre> +<b>src$ rm -f *.gcda</b> <i># Get rid of any stale gcov files</i> +<b>src$ klee-replay ./echo ../../obj-llvm/src/klee-last/*.ktest </b> +klee-replay: TEST CASE: ../../obj-llvm/src/klee-last/test000001.ktest +klee-replay: ARGS: "./echo" + +<i> ... </i> + +<b>src$ gcov echo</b> +File '../../src/system.h' +Lines executed:6.38% of 47 +../../src/system.h:creating 'system.h.gcov' + +File '../../lib/timespec.h' +Lines executed:0.00% of 2 +../../lib/timespec.h:creating 'timespec.h.gcov' + +File '../../lib/gettext.h' +Lines executed:0.00% of 32 +../../lib/gettext.h:creating 'gettext.h.gcov' + +File '../../lib/openat.h' +Lines executed:0.00% of 8 +../../lib/openat.h:creating 'openat.h.gcov' + +File '../../src/echo.c' +Lines executed:97.03% of 101 +../../src/echo.c:creating 'echo.c.gcov' </pre> +</div> + + <p> + The reasons for not getting perfect 100% line coverage are left as an + exercise to the reader. :) <!-- FIXME: Technically, it's just cause I haven't + bothered to figure it out... figure it out! --> + </p> + + <!--*********************************************************************--> + + <h2>Step 7: Using <tt>zcov</tt> to analyze coverage </h2> + + <p> + For visualizing the coverage results, you might want to use the <a href="http://minormatter.com/zcov/">zcov</a> tool. + </p> + <br/> + +</div> +</body> +</html> 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> diff --git a/www/Tutorial-2.html b/www/Tutorial-2.html new file mode 100644 index 00000000..47187a45 --- /dev/null +++ b/www/Tutorial-2.html @@ -0,0 +1,287 @@ +<!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 - Tutorial Two</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 Two: Testing a Simple Regular Expression Library</h1> + +<p>This is an 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> + +<p><tt>Regexp.c</tt> contains a simple regular expression matching function, and +the bare bones testing harness (in <tt>main</tt>) needed to explore this code +with klee. You can see a version of the source +code <a href="resources/Regexp.c.html">here</a>.</p> + +<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>We'll start by showing how to build and run the example, and then explain how +the test harness works in more detail.</p> + +<h2>Building the example</h2> + +<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>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> + +<h2>Executing the code with KLEE</h2> + +<!-- 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> + +<h2>KLEE error reports</h2> + +<p>When KLEE detects an error in the program being executed it will generate a +test case which exhibits the error, and write some additional information about +the error into a file <tt>test<i>N</i>.<i>TYPE</i>.err</tt>, where <i>N</i> is +the test case number, and <i>TYPE</i> identifies the kind of error. Some +types of errors KLEE detects include:</p> + +<ul> + <li><b>ptr</b>: Stores or loads of invalid memory locations.</li> + + <li><b>free</b>: Double or invalid <tt>free()</tt>.</li> + + <li><b>abort</b>: The program called <tt>abort()</tt>.</li> + + <li><b>assert</b>: An assertion failed.</li> + + <li><b>div</b>: A division or modulus by zero was detected.</li> + + <li><b>user</b>: There is a problem with the input (invalid <tt>klee</tt> + intrinsic calls) or the way KLEE is being used.</li> + + <li><b>exec</b>: There was a problem which prevented KLEE from executing the + program; for example an unknown instruction, a call to an invalid function + pointer, or inline assembly.</li> + + <li><b>model</b>: KLEE was unable to keep full precision and is only exploring + parts of the program state. For example, symbolic sizes to <tt>malloc</tt> are + not currently supported, in such cases KLEE will concretize the argument.</li> +</ul> + +<p>KLEE will print a message to the console when it detects an error, in the +test run above we can see that KLEE detected two memory errors. For all program +errors, KLEE will write a simple backtrace into the <tt>.err</tt> file. This is +what one of the errors above looks like:</p> +<div class="instr"> +<pre> +Error: memory error: out of bound pointer +File: .../klee/examples/regexp/Regexp.c +Line: 23 +Stack: + #0 00000146 in matchhere (re=14816471, text=14815301) at .../klee/examples/regexp/Regexp.c:23 + #1 00000074 in matchstar (c, re=14816471, text=14815301) at .../klee/examples/regexp/Regexp.c:16 + #2 00000172 in matchhere (re=14816469, text=14815301) at .../klee/examples/regexp/Regexp.c:26 + #3 00000074 in matchstar (c, re=14816469, text=14815301) at .../klee/examples/regexp/Regexp.c:16 + #4 00000172 in matchhere (re=14816467, text=14815301) at .../klee/examples/regexp/Regexp.c:26 + #5 00000074 in matchstar (c, re=14816467, text=14815301) at .../klee/examples/regexp/Regexp.c:16 + #6 00000172 in matchhere (re=14816465, text=14815301) at .../klee/examples/regexp/Regexp.c:26 + #7 00000231 in matchhere (re=14816464, text=14815300) at .../klee/examples/regexp/Regexp.c:30 + #8 00000280 in match (re=14816464, text=14815296) at .../klee/examples/regexp/Regexp.c:38 + #9 00000327 in main () at .../klee/examples/regexp/Regexp.c:59 +Info: + address: 14816471 + next: object at 14816624 of size 4 + prev: object at 14816464 of size 7 +</pre> +</div> + +<p>Each line of the backtrace lists the frame number, the instruction line (this +is the line number in the <tt>assembly.ll</tt> file found along with the run +output), the function and arguments (including values for the concrete +parameters), and the source information.</p> + +<p>Particular error reports may also include additional information. For memory +errors, KLEE will show the invalid address, and what objects are on the heap +both before and after that address. In this case, we can see that the address +happens to be exactly one byte past the end of the previous object.</p> + +<h2>Changing the test harness</h2> + +<p>The reason KLEE is finding memory errors in this program isn't because the +regular expression functions have a bug, rather it indicates a problem in our +test driver. The problem is that we are making the input regular expression +buffer completely symbolic, but the <tt>match</tt> function expects it to be a +null terminated string. Let's look at two ways we can fix this.</p> + +<p>The simplest way to fix this problem is to store <tt>'\0'</tt> at the end of +the buffer, after making it symbolic. This makes our driver look like this:</p> +<div class="instr"> +<pre> +int main() { + // The input regular expression. + char re[SIZE]; + + // Make the input symbolic. + klee_make_symbolic(re, sizeof re, "re"); + re[SIZE - 1] = '\0'; + + // Try to match against a constant string "hello". + match(re, "hello"); + + return 0; +} +</pre> +</div> +<p>Making a buffer symbolic just initializes the contents to refer to symbolic +variables, we are still free to modify the memory as we wish. If you recompile +and run <tt>klee</tt> on this test program, the memory errors should now be +gone.</p> + +<p>Another way to accomplish the same effect is to use the <tt>klee_assume</tt> +intrinsic function. <tt>klee_assume</tt> takes a single argument (an unsigned +integer) which generally should some kind of conditional expression, and +"assumes" that expression to be true on the current path (if that can never +happen, i.e. the expression is provably false, KLEE will report an error).</pp> + +<p>We can use <tt>klee_assume</tt> to cause KLEE to only explore states where +the string is null terminated by writing the driver like this:</p> +<div class="instr"> +<pre> +int main() { + // The input regular expression. + char re[SIZE]; + + // Make the input symbolic. + klee_make_symbolic(re, sizeof re, "re"); + klee_assume(re[SIZE - 1] == '\0'); + + // Try to match against a constant string "hello". + match(re, "hello"); + + return 0; +} +</pre> +</div> +<p>In this particular example, both solutions work fine, but in +general <tt>klee_assume</tt> is more flexible:</p> +<ul> + <li>By explicitly declaring the constraint, this will force test cases to have + the <tt>'\0'</tt> in them. In the first example where we write the terminating + null explicitly, it doesn't matter what the last byte of the symbolic input is + and KLEE is free to generate any value. In some cases where you want to + inspect the test cases by hand, it is more convenient for the test case to + show all the values that matter.</li> + + <li><tt>klee_assume</tt> can be used to encode more complicated + constraints. For example, we could use <tt>klee_assume(re[0] != '^')</tt> to + cause KLEE to only explore states where the first byte is + not <tt>'^'</tt>.</li> +</ul> + +<p><b>NOTE</b>: One important caveat when using <tt>klee_assume</tt> with +multiple conditions; remember that boolean conditionals like '&&' and '||' may +be compiled into code which branches before computing the result of the +expression. In such situations KLEE will branch the process *before* it reaches +the call to <tt>klee_assume</tt>, which may result in exploring unnecessary +additional states. For this reason it is good to use as simple expressions as +possible to <tt>klee_assume</tt> (for example splitting a single call into +multiple ones), and to use the '&' and '|' operators instead of the +short-circuiting ones.</p> + +<!-- +<h2>Visualizing what KLEE explored<h2> + +<p>For large or long running programs, it is frequently useful to know exactly +what code KLEE explored, where it spent its time, where branches were taken, +and so on.</p> +--> + +</div> +</body> +</html> diff --git a/www/Tutorials.html b/www/Tutorials.html new file mode 100644 index 00000000..e063a9a8 --- /dev/null +++ b/www/Tutorials.html @@ -0,0 +1,38 @@ +<!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 - Tutorials</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 Tutorials</h1> + <!--*********************************************************************--> + + <ol> + <li><a href="Tutorial-1.html">Tutorial One</a>: Testing a small function.</li> + + <li><a href="Tutorial-2.html">Tutorial Two</a>: Testing a simple regular + expression library.</li> + + <li><a href="http://feliam.wordpress.com/2010/10/07/the-symbolic-maze/"> + Solving a maze with KLEE</a>: A nice explanation of how symbolic + execution can be used to generate interesting program + inputs. The example shows how to use KLEE to find all the + solutions to a maze game. + </li> + + <li><a href="TestingCoreutils.html">Testing Coreutils</a>: In-depth + description of how to use KLEE to test GNU Coreutils.</li> + </ol> + + +</div> +</body> +</html> diff --git a/www/bugs.html b/www/bugs.html new file mode 100644 index 00000000..1ac9421a --- /dev/null +++ b/www/bugs.html @@ -0,0 +1,24 @@ +<!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>The KLEE Symbolic Virtual Machine</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 Bug Reports</h1> + <!--*********************************************************************--> + + Please report any bugs in KLEE to + the <a href="klee-dev.html">klee-dev mailing list</a>. You need to + be subscribe to the list in order to send your report. + +</div> +</body> +</html> diff --git a/www/content.css b/www/content.css new file mode 100644 index 00000000..50835ec3 --- /dev/null +++ b/www/content.css @@ -0,0 +1,75 @@ +html, body { + padding:0px; + font-size:small; + font-family:"Lucida Grande", "Lucida Sans Unicode", Arial, Verdana, Helvetica, sans-serif; + background-color: #fff; color: #222; + line-height:1.5; +} + +h1, h2, h3, tt { color: #000 } + +h1 { color:#000000; padding-top: 0px; margin-top:0px;} +h2 { color:#333333; padding-top: 0.5em; } +h3 { color:#2d58b7; padding-top: 0.5em; margin-bottom: -0.25em; } +h4 { color:#2d58b7; } +li { padding-bottom: 0.5em; } +ul { padding-left:1.5em; } + +/* Slides */ +IMG.img_slide { + display: block; + margin-left: auto; + margin-right: auto +} + +.itemTitle { color:#2d58b7 } + +/* Tables */ +tr { vertical-align:top } + +/* Syntax */ +div.syntax { + border: 1px solid LightSteelBlue ; + font-family: Courier New; + background-color: SeaShell; + padding: 7px; + margin: 7px; +} + +/* Examples */ +div.example { + border: 1px solid LightSteelBlue ; + font-family: Courier New; + background-color: #E3E3E3; + padding: 7px; + margin: 7px; +} + +/* Instructions */ +div.instr { + border: 1px solid LightSteelBlue ; + font-family: Courier New; + background-color: #E3E3E3; + padding: 7px; + margin: 7px; +} + +/* Output */ +pre.output { + border: 1px solid LightSteelBlue ; + font-family: Courier New; + background-color: #E3E3E3; + padding: 7px; + margin: 7px; +} + +/* Code */ +pre.code{ + display:table; + border: 1px solid LightSteelBlue ; + font-family: Courier New; + background-color: #E3E3E3; + margin: 10px; + padding: 10px; +} + diff --git a/www/content/coreutils_kc_0.png b/www/content/coreutils_kc_0.png new file mode 100644 index 00000000..3f72dc49 --- /dev/null +++ b/www/content/coreutils_kc_0.png Binary files differdiff --git a/www/content/coreutils_kc_1.png b/www/content/coreutils_kc_1.png new file mode 100644 index 00000000..d4372f26 --- /dev/null +++ b/www/content/coreutils_kc_1.png Binary files differdiff --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> diff --git a/www/index.html b/www/index.html new file mode 100644 index 00000000..b76a42bc --- /dev/null +++ b/www/index.html @@ -0,0 +1,36 @@ +<!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>The KLEE Symbolic Virtual Machine</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>The KLEE Symbolic Virtual Machine</h1> + <!--*********************************************************************--> + + <p>KLEE is a symbolic virtual machine built on top of + the <a href="http://llvm.org">LLVM</a> compiler infrastructure, and available + under the UIUC open source license.</p> + + <p>For more information on what KLEE is and what it can do, see + the <a href="http://llvm.org/pubs/2008-12-OSDI-KLEE.html">OSDI + 2008</a> paper.</p> + + <p>If you are interested in trying it yourself, please + see <a href="GetStarted.html">Getting Started</a>.</p> + +<!-- <p>FIXME: Somewhere need to describe what KLEE can do well and what + is more "experimental" or research level. This should also address + how KLEE could be used by outside groups (i.e. kleaver).</p> --> + +</div> +</body> +</html> diff --git a/www/klee-dev.html b/www/klee-dev.html new file mode 100644 index 00000000..5434ce57 --- /dev/null +++ b/www/klee-dev.html @@ -0,0 +1,31 @@ +<!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-dev mailing list</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-dev mailing list</h1> + <!--*********************************************************************--> + + <p>If you have questions about KLEE that are not answered on this + website, please send a message to + the <a href="https://mailman.ic.ac.uk/mailman/listinfo/klee-dev">klee-dev</a> + mailing list.</p> + + + <p>However, before doing so, please + check <a href="http://www.mail-archive.com/klee-dev@imperial.ac.uk/">klee-dev's + searchable archive<a/> to see if your question has already been + answered.</p> + +</div> +</body> +</html> diff --git a/www/klee-files.html b/www/klee-files.html new file mode 100644 index 00000000..299f593b --- /dev/null +++ b/www/klee-files.html @@ -0,0 +1,137 @@ +<!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>The KLEE Symbolic Virtual Machine</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>Files generated by KLEE</h1> + <!--*********************************************************************--> + + <h2>Standard Global Files</h2> + + These are global files are always generated on a KLEE execution: + <ol> + <li><b>info</b>: This is a text file containing various information + related to a KLEE run. In particular, it records the exact + command-line with which KLEE was run, and the total time taken by + the execution. E.g.: + <pre class="output"> + $ cat info + klee --write-pcs demo.o + PID: 12460 + Started: 2009-05-20 22:31:41 + BEGIN searcher description + DFSSearcher + END searcher description + Finished: 2009-05-20 22:31:41 + Elapsed: 00:00:00 + KLEE: done: explored paths = 3 + KLEE: done: avg. constructs per query = 6 + KLEE: done: total queries = 3 + KLEE: done: valid queries = 0 + KLEE: done: invalid queriers = 3 + KLEE: done: query cex = 3 + KLEE: done: total instructions = 67 + KLEE: done: completed paths = 3 + KLEE: done: generated tests = 3 </pre> + </li> + + <li><b>warnings.txt</b>: This is a text file containing all warnings emitted by KLEE. + </li> + + <li><b>messages.txt</b>: This is a text file containing all other messages emitted by KLEE. + </li> + + <li><b>assembly.ll</b>: This file contains a human readable version + of the LLVM bitcode executed by KLEE + + <li><b>run.stats</b>: This is a text file containing various + statistics emitted by KLEE. While this file can be inspected + manually, you should use the <a href="klee-tools.html">klee-stats</a> + tool for that.</li> + + <li><b>run.istats</b>: This is a binary file containing global + statistics emitted by KLEE for each line of code in the program. + </li> + + </ol> + + + <h2>Other Global Files</h2> + + <ol> + <li><b>all-queries.pc:</b> This file contains all the queries KLEE + made during execution in the <a href="KQuery.html">KQuery</a> + format. Note these are the queries before any optimisation + (e.g. caching, constraint independence) so it is possible that + some of the queries logged are never executed by KLEE's underlying + solver or are modified before being executed by KLEE's underlying + solver. The generation of this file can be enabled by specifying + the option <tt>--use-query-log=all:pc</tt> to KLEE.</li> + <li><b>all-queries.smt2:</b> This file contains all the queries KLEE made during execution in the <a href="http://www.smtlib.org">SMT-LIBv2</a> + .It contains the same information as <tt>all-queries.pc</tt>. + The generation of this file can be enabled by specifying the option <tt>--use-query-log=all:smt2</tt> to KLEE.</li> + <li><b>solver-queries.pc:</b> This file contains all the queries passed to KLEE's underlying solver during execution in the + <a href="KQuery.html">KQuery</a> format. Note these are the + queries after all optimisations (e.g. caching, constraint + independence) are performed. The generation of this file can be + enabled by specifying the + option <tt>--use-query-log=solver:pc</tt> to KLEE.</li> + <li><b>solver-queries.smt2:</b> This file contains all the queries passed to KLEE's underlying solver during execution in the + <a href="http://www.smtlib.org">SMT-LIBv2</a> + format. It contains the same information as <tt>solver-queries.pc</tt>. + The generation of this file can be enabled by specifying the option <tt>--use-query-log=solver:smt2</tt> to KLEE.</li> + </ol> + + + <h2> Per-path files</h2> + + <ol> + <li> + <b>test<N>.ktest</b>: Contains the test case generated by + KLEE on that path. Use <a href="klee-tools.html">ktest-tool</a> + to read the contents. The generation of <tt>.ktest</tt> files + can be disabled using the <tt>--no-output</tt> option. + </li> + + <li> + <b>test<N>.<error-type>.err</b>: Generated for paths + where KLEE found an error. Contains information about the error + in textual form. + </li> + + <li><b>test<N>.pc:</b> Contains the constraints associated with the given + path, in <a href="KQuery.html">KQuery</a> format. The generation + of these files can be enabled via the <tt>--write-cvcs</tt> flag. + </li> + + <li> + <b>test<N>.cvc:</b> Contains the constraints associated + with the given path, + in <a href="https://sites.google.com/site/stpfastprover/stp-documentation#TOC-The-CVC-language">CVC</a> + format. The generation of these files can be enabled via + the <tt>--write-pcs</tt> flag. (This is the same information as + in the corresponding <tt>.pc</tt> file.) + </li> + <li> + <b>test<N>.smt2:</b> Contains the constraints associated + with the given path, + in <a href="http://www.smtlib.org/">SMT-LIBv2</a> + format. The generation of these files can be enabled via + the <tt>--write-smt2s</tt> flag. (This is the same information as + in the corresponding <tt>.pc</tt> file.) + </li> + </ol> + + +</div> +</body> +</html> diff --git a/www/klee-options.html b/www/klee-options.html new file mode 100644 index 00000000..be997ec4 --- /dev/null +++ b/www/klee-options.html @@ -0,0 +1,99 @@ +<!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>The KLEE Symbolic Virtual Machine</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 Options</h1> + <!--*********************************************************************--> + + <h3> + <a href="#search"> 1. Search Heuristics</a> <br/> + <a href="#logging"> 2. Query Logging</a> <br/> + </h3> + + <h2 id="search">Search Heuristics</h2> + + <h3>Main search heuristics</h3> + + <p> + KLEE provides four main search heuristics: + <ol> + <li><b>Depth-First Search (DFS):</b> Traverses states in depth-first order.</li> + <li><b>Random State Search:</b>Randomly selects a state to explore.</li> + <li><b>Random Path Selection:</b> Described in our <a href="http://www.doc.ic.ac.uk/~cristic/papers/klee-osdi-08.pdf">KLEE OSDI'08</a> paper.</li> + <li><b>Non Uniform Random Search (NURS):</b> Selects a state randomly according to a given distribution. The distribution can be based on the minimum distance to an uncovered instruction (MD2U), the query cost, etc. + </ol> + + To select a search heuristic, use the <b>--search</b> option provided by KLEE. For example: + <pre class="output"> + $ klee --search=dfs demo.o</pre> + + runs <i>demo.o</i> using DFS, while + <pre class="output"> + $ klee --search=random-path demo.o </pre> + runs it using the random path selection strategy. + + The full list of options is shown in KLEE's help message: + <pre class="output"> + $ klee --help + -search - Specify the search heuristic (default=random-path interleaved with nurs:covnew) + =dfs - use Depth First Search (DFS) + =random-state - randomly select a state to explore + =random-path - use Random Path Selection (see OSDI'08 paper) + =nurs:covnew - use Non Uniform Random Search (NURS) with Coverage-New heuristic + =nurs:md2u - use NURS with Min-Dist-to-Uncovered heuristic + =nurs:depth - use NURS with 2^depth heuristic + =nurs:icnt - use NURS with Instr-Count heuristic + =nurs:cpicnt - use NURS with CallPath-Instr-Count heuristic + =nurs:qc - use NURS with Query-Cost heuristic </pre> + + + <h3>Interleaving search heuristics</h3> + <p> + Search heuristics in KLEE can be interleaved in a round-robin + fashion. To interleave several search heuristics to be interleaved, use the <b>--search</b> multiple times. For example: + <pre class="output"> + $ klee --search=random-state --search=nurs:md2u demo.o </pre> + interleaves the Random State and the NURS:MD2U heuristics in a round robin fashion. + <br/> + </p> + + + <h3>Default search heuristics</h3> + <p> + The default heuristics used by KLEE are <i>random-path</i> interleaved with <i>nurs:covnew</i>. + </p> + + <h2 id="logging">Query Logging</h2> + + To log the queries issued by KLEE during symbolic execution, you can use the following options: + <ol> + <li> + <b>--use-query-log=TYPE:FORMAT</b>, where: + <ul> + <li><b>TYPE</b> is either <b>all</b> to log all the queries KLEE made during execution before any optimisation (e.g. caching, constraint independence) is performed, or <b>solver</b> to log only the queries passed to KLEE's underlying solver. Note that it is possible that some of the unoptimized queries are never executed or are modified before being executed by KLEE's underlying solver.</li> + <li><b>FORMAT</b> is the format in which queries are logged and can be either <b>pc</b> for the <a href="KQuery.html">KQuery</a> format, or <b>smt2</b> for the <a href="http://www.smtlib.org">SMT-LIBv2</a> format. + </ul> + <li> + <b>--min-query-time-to-log=TIME</b> (in ms) is used to log only queries that exceed a certain time limit. <b>TIME</b> can be: + <ul> + <li><b>0</b> (default): to log all queries</li> + <li><b><0</b>: a negative value specifies that only queries that timed out should be logged. The timeout value is specified via the <b>--max-stp-time</b> option.</li> + <li><b>>0</b>: only queries that took more that <b>TIME</b> milliseconds should be logged. + </ul> + </li> + </li> + </ol> + +</div> +</body> +</html> diff --git a/www/klee-tools.html b/www/klee-tools.html new file mode 100644 index 00000000..80ae5d35 --- /dev/null +++ b/www/klee-tools.html @@ -0,0 +1,84 @@ +<!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>The KLEE Symbolic Virtual Machine</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 Tools</h1> + <!--*********************************************************************--> + + <h3> + <a href="#ktest-tool"> 1. ktest-tool</a> <br/> + <a href="#klee-stats"> 2. klee-stats</a> <br/> + </h3> + + <h2 id="ktest-tool">ktest-tool</h2> + + <h2 id="klee-stats">klee-stats</h2> + <b><i>klee-stats</i></b> is a Python script used to extract and present in a + tabular form runtime statistics for a KLEE execution. The runtime statistics include: + <ul> + <li>The number of executed instructions</li> + <li>Instruction coverage in the LLVM bitcode (%)</li> + <li>Branch coverage in the LLVM bitcode (%)</li> + <li>Total static instructions in the LLVM bitcode</li> + <li>The number of currently active states</li> + <li>Megabytes of memory currently used</li> + <li>The number of queries issued to STP</li> + <li>The average number of query constructs per query</li> + <li>Various time statistics: + <ul> + <li>Total user time</li> + <li>Total wall time</li> + <li>Time spent in the constraint solver</li> + <li>Time spent in the counterexample caching code</li> + <li>Time spent forking</li> + <li>Time spent in object resolution</li> + </ul></li> + </ul> + + + <i>klee-stats</i> extracts statistics information from the <i>run.stats</i> file + present in the <i>klee-out-*</i> directory created during a KLEE execution. + The exact usage of <i>klee-stats</i> is as follows: + <pre>klee-stats [options] directories</pre> + The <i>directories</i> parameter is a list of <i>klee-out-*</i> directories + created by KLEE. A common scenario is to simply run <i>klee-stats</i> on <i>klee-last</i>. + + <p> + In order to limit printed information only to the values of measured times, + the following options can be used: + + <ul> + <li><i>--print-rel-times</i>—display time values relative + to measured execution time</li> + + <li><i>--print-abs-times</i>—display absolute time values</li> + </ul> + + The <i>--precision</i> option can be used to configure the number of fractional + digits displayed in floating point values. By default, 2 fractional digits + are displayed, but in some cases that might be not sufficient—if the value + is very small, e.g. 0.0001, with 2-digits precision it will be printed as 0.00. + </p> + + <p> Various other options can be used to specify what values are + displayed and how they are displayed. Options for comparison of + statistics are also provided. More information about available + options can be obtained using the command: + <pre>klee-stats --help</pre> + </p> + + <br/> + +</div> +</body> +</html> diff --git a/www/menu.css b/www/menu.css new file mode 100644 index 00000000..6e96a457 --- /dev/null +++ b/www/menu.css @@ -0,0 +1,39 @@ +/***************/ +/* page layout */ +/***************/ + +[id=menu] { + position:fixed; + width:25ex; +} +[id=content] { + /* ***** EDIT THIS VALUE IF CONTENT OVERLAPS MENU ***** */ + position:absolute; + left:29ex; + padding-right:4ex; +} + +/**************/ +/* menu style */ +/**************/ + +#menu .submenu { + padding-top:1em; + display:block; +} + +#menu label { + display:block; + font-weight: bold; + text-align: center; + background-color: rgb(192,192,192); +} +#menu a { + padding:0 .2em; + display:block; + text-align: center; + background-color: rgb(235,235,235); +} +#menu a:visited { + color:rgb(100,50,100); +} \ No newline at end of file diff --git a/www/menu.html.incl b/www/menu.html.incl new file mode 100644 index 00000000..7f2e4e33 --- /dev/null +++ b/www/menu.html.incl @@ -0,0 +1,31 @@ +<div id="menu"> + <div> + <a href="http://klee.llvm.org/">KLEE Home</a> + </div> + + <div class="submenu"> + <label>KLEE Info</label> + <a href="GetStarted.html">Getting Started</a> + <a href="GetInvolved.html">Get Involved</a> + <a href="Documentation.html">Documentation</a> + <a href="Tutorials.html">Tutorials</a> + <a href="Publications.html">Publications</a> + <a href="OpenProjects.html">Open Projects</a> + </div> + + <div class="submenu"> + <label>Quick Links</label> + <a href="klee-dev.html">klee-dev (mailing list)</a> + <a href="GetInvolved.html#BugReports">Bug Reports</a> + <a href="http://llvm.org/">LLVM Home</a> + </div> + + <div class="submenu"> + <label>Development & Code</label> + <a href="http://klee.minormatter.com:8010/">Buildbot</a> + <a href="http://llvm.org/svn/llvm-project/klee/trunk/">Browse SVN</a> + <a href="http://llvm.org/viewvc/llvm-project/klee/trunk/">Browse ViewVC</a> + <a href="http://test.minormatter.com/~ddunbar/klee-doxygen/index.html">Browse Doxygen</a> + <a href="http://test.minormatter.com/~ddunbar/klee-cov/index.html">Testing Coverage</a> + </div> +</div> 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> diff --git a/www/resources/get_sign.c.html b/www/resources/get_sign.c.html new file mode 100644 index 00000000..58c28d01 --- /dev/null +++ b/www/resources/get_sign.c.html @@ -0,0 +1,37 @@ +<!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>get_sign.c</H1> + +<PRE> +<I><FONT COLOR="#B22222">/* + * First KLEE tutorial: testing a small function + */</FONT></I> + + +<B><FONT COLOR="#228B22">int</FONT></B> <B><FONT COLOR="#0000FF">get_sign</FONT></B>(<B><FONT COLOR="#228B22">int</FONT></B> x) { + <B><FONT COLOR="#A020F0">if</FONT></B> (x == 0) + <B><FONT COLOR="#A020F0">return</FONT></B> 0; + + <B><FONT COLOR="#A020F0">if</FONT></B> (x < 0) + <B><FONT COLOR="#A020F0">return</FONT></B> -1; + <B><FONT COLOR="#A020F0">else</FONT></B> + <B><FONT COLOR="#A020F0">return</FONT></B> 1; +} + +<B><FONT COLOR="#228B22">int</FONT></B> <B><FONT COLOR="#0000FF">main</FONT></B>() { + <B><FONT COLOR="#228B22">int</FONT></B> a; + klee_make_symbolic(&a, <B><FONT COLOR="#A020F0">sizeof</FONT></B>(a), <B><FONT COLOR="#BC8F8F">"a"</FONT></B>); + <B><FONT COLOR="#A020F0">return</FONT></B> get_sign(a); +} +</PRE> +<HR> +<ADDRESS>Generated by <A HREF="http://www.iki.fi/~mtr/genscript/">GNU Enscript 1.6.5.2</A>.</ADDRESS> +<I>enscript -Ec --color -w html get_sign.c -o get_sign.c.html</I> +</BODY> +</HTML> diff --git a/www/resources/islower.c.html b/www/resources/islower.c.html new file mode 100644 index 00000000..524f2093 --- /dev/null +++ b/www/resources/islower.c.html @@ -0,0 +1,33 @@ +<!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>islower.c</H1> + +<PRE> +<I><FONT COLOR="#B22222">/* + * First KLEE tutorial: testing a small function + */</FONT></I> + +#<B><FONT COLOR="#5F9EA0">include</FONT></B> <B><FONT COLOR="#BC8F8F"><klee/klee.h></FONT></B> + +<B><FONT COLOR="#228B22">int</FONT></B> <B><FONT COLOR="#0000FF">my_islower</FONT></B>(<B><FONT COLOR="#228B22">int</FONT></B> x) { + <B><FONT COLOR="#A020F0">if</FONT></B> (x >= <B><FONT COLOR="#BC8F8F">'a'</FONT></B> && x <= <B><FONT COLOR="#BC8F8F">'z'</FONT></B>) + <B><FONT COLOR="#A020F0">return</FONT></B> 1; + <B><FONT COLOR="#A020F0">else</FONT></B> <B><FONT COLOR="#A020F0">return</FONT></B> 0; +} + +<B><FONT COLOR="#228B22">int</FONT></B> <B><FONT COLOR="#0000FF">main</FONT></B>() { + <B><FONT COLOR="#228B22">char</FONT></B> c; + klee_make_symbolic(&c, <B><FONT COLOR="#A020F0">sizeof</FONT></B>(c), <B><FONT COLOR="#BC8F8F">"input"</FONT></B>); + <B><FONT COLOR="#A020F0">return</FONT></B> my_islower(c); +} +</PRE> +<HR> +<ADDRESS>Generated by <A HREF="http://www.iki.fi/~mtr/genscript/">GNU enscript 1.6.4</A>.</ADDRESS> +</BODY> +</HTML> |
