From 4ce774750042043fca78f50575f154f68296ab18 Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Thu, 21 May 2009 16:28:43 +0000 Subject: Start basic Regexp.c example for klee. - A few other web page tweaks. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72215 91177308-0d34-0410-b5e6-96231b3b80d8 --- www/Examples.html | 114 +++++++++++++++++++++++++++++++++++++++++--- www/GetInvolved.html | 25 ++++++---- www/GetStarted.html | 10 ++-- www/menu.html.incl | 2 +- www/resources/Regexp.c.html | 78 ++++++++++++++++++++++++++++++ 5 files changed, 208 insertions(+), 21 deletions(-) create mode 100644 www/resources/Regexp.c.html diff --git a/www/Examples.html b/www/Examples.html index 23584053..25ee6fb0 100644 --- a/www/Examples.html +++ b/www/Examples.html @@ -15,19 +15,119 @@

KLEE Examples

-

FIXME: Intro.

+

Here is a basic example of using KLEE to test a simple regular expression matching function. You can find the basic example in the source tree under examples/regexp.

-

Basic Sort Example

+

Example: Regexp.c

-

FIXME: Write.

+

Regexp.c contains a simple regular expression matching function, and +the bare bones testing harness (in main) need to explore this code with +klee. You can see a version of the source +code here.

-

FIXME: More complicated example

+

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.

-

FIXME: Write: show the important klee.h functions.

+

We'll start by showing how to build and run the example, and then explain how +the test harness works in more detail.

+ +

Step 1: Building the example

-

FIXME: Write: show the important klee tools.

+

The first step is to compile the source code using a compiler which can +generate object files in LLVM bitcode format. Here we use llvm-gcc, +but Clang works just as well!

-

FIXME: Write: show the important klee options.

+

From within the examples/regexp directory: +

+ $ llvm-gcc -I ../../include -emit-llvm -c -g Regexp.c +
+which should create a Regexp.o file in LLVM bitcode +format. The -I argument is used so that the compiler can +find "klee/klee.h",which +contains definitions for the intrinsic functions used to interact with the KLEE +virtual machine. -c is used because we only want to compile the code to +an object file (not a native executable), and finally -g causes +additional debug information to be stored in the object file, which KLEE will +use to determine source line number information.

+ +

If you have the LLVM tools installed in your path, you can verify that this step +worked by running llvm-nm on the generated file:

+
+
+  $ llvm-nm Regexp.o
+         t matchstar
+         t matchhere
+         T match
+         T main
+         U klee_make_symbolic_name
+         d LC
+         d LC1
+
+
+ +

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 llvm-link +and llvm-ld 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.

+ +

Step 2: Executing the code with KLEE

+ + +

The next step is to execute the code with KLEE:

+
+
+$ klee --only-output-states-covering-new Regexp.o
+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
+
+
+ +

On startup, KLEE prints the directory used to store output (in this +case klee-out-1). By default klee will use the first +free klee-out-N directory and also create a klee-last +symlink which will point to the most recent created directory. You can specify a +directory to use for outputs using the -output-dir=path +command line argument.

+ +

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.

+ +

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.

+ +

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. klee gets +a SIGINT), but there are additional options to limit KLEE's runtime and memory +usage:

+

+

+ +

Step ?: Changing the test harness

+ +

FIXME: Step through & explain the test harness, and how we can modify it.

+ +

FIXME: Write: show the important klee.h functions.

diff --git a/www/GetInvolved.html b/www/GetInvolved.html index b8afcbb3..41c84e54 100644 --- a/www/GetInvolved.html +++ b/www/GetInvolved.html @@ -3,7 +3,7 @@ - klee - Get Involved + KLEE - Get Involved @@ -13,21 +13,30 @@
-

Getting Involved with the klee Project

+

Getting Involved with the KLEE Project

-

FIXME: Intro.

+

If you are interested in following development of KLEE, or would like to +contribute, here are some resources that may prove useful.

Mailing Lists

-

klee-dev

+

Currently the main list for KLEE discussion (both for users and developers) +is klee-dev.

-

klee-commits

+

Commit messages to the KLEE repository go to +klee-commits. This +is also the place to send patches if you are interested in contributing to +KLEE.

Working with the Code

-

FIXME: Point at pertinent LLVM docs.

- -

FIXME: Point at doxygen.

+

KLEE developer documentation is written in doxygen and you may have it online here: + doxygen + (this is updated nightly from the source tree).

+ +

Many parts of KLEE rely on the LLVM infrastructure, you can find more +information about programming for LLVM here: +LLVM's General Programming Documentation.

diff --git a/www/GetStarted.html b/www/GetStarted.html index 07083d4f..5f28b1d3 100644 --- a/www/GetStarted.html +++ b/www/GetStarted.html @@ -39,12 +39,12 @@ Started with the LLVM System for more information.
  • Checkout and build LLVM from SVN head: - - svn co http://llvm.org/svn/llvm-project/llvm/trunk llvm - cd llvm - ./configure --enable-optimized +
    + svn co http://llvm.org/svn/llvm-project/llvm/trunk llvm
    + cd llvm
    + ./configure --enable-optimized
    make -     +
    (the --enable-optimized configure argument is not necessary, but KLEE runs very slowly in Debug mode). diff --git a/www/menu.html.incl b/www/menu.html.incl index ef450ca7..58245138 100644 --- a/www/menu.html.incl +++ b/www/menu.html.incl @@ -4,7 +4,7 @@
    - + About Get Started Get Involved 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 @@ + + + +Enscript Output + + + + +

    Regexp.c

    + +
    +/* 
+ * Simple regular expression matching.
+ *
+ * From:
+ *   The Practice of Programming
+ *   Brian W. Kernighan, Rob Pike
+ *
+ */ 
+
+#include <klee/klee.h>
+
+static int matchhere(char*,char*);
+
+static int matchstar(int c, char *re, char *text) {
+  do {
+    if (matchhere(re, text))
+      return 1;
+  } while (*text != '\0' && (*text++ == c || c== '.'));
+  return 0;
+}
+
+static int matchhere(char *re, char *text) {
+  if (re[0] == '\0')
+     return 0;
+  if (re[1] == '*')
+    return matchstar(re[0], re+2, text);
+  if (re[0] == '$' && re[1]=='\0')
+    return *text == '\0';
+  if (*text!='\0' && (re[0]=='.' || re[0]==*text))
+    return matchhere(re+1, text+1);
+  return 0;
+}
+
+int match(char *re, char *text) {
+  if (re[0] == '^')
+    return matchhere(re+1, text);
+  do {
+    if (matchhere(re, text))
+      return 1;
+  } while (*text++ != '\0');
+  return 0;
+}
+
+/*
+ * Harness for testing with KLEE.
+ */
+
+// The size of the buffer to test with.
+#define SIZE 7
+
+int main() {
+  // The input regular expression.
+  char re[SIZE];
+  
+  // Make the input symbolic. 
+  klee_make_symbolic_name(re, sizeof re, "re");
+
+  // Try to match against a constant string "hello".
+  match(re, "hello");
+
+  return 0;
+}
+
    +
    +
    Generated by GNU enscript 1.6.4.
    + + -- cgit 1.4.1