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 ++++++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 107 insertions(+), 7 deletions(-) (limited to 'www/Examples.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.

-- cgit 1.4.1