+ +int my_islower(int x) { + if (x >= 'a' && x <= 'z') + return 1; + else return 0; +} + +int main() { + char c; + klee_make_symbolic(&c, sizeof(c), "input"); + return my_islower(c); +} diff --git a/www/GetStarted.html b/www/GetStarted.html index 890510ab..5c445059 100644 --- a/www/GetStarted.html +++ b/www/GetStarted.html @@ -86,7 +86,7 @@ necessary, but KLEE runs very slowly in Debug mode). -

You're ready to go! Go to the Tutorials page +

You're ready to go! Go to the Tutorials page to try KLEE.

diff --git a/www/Tutorial-1.html b/www/Tutorial-1.html new file mode 100644 index 00000000..833541d7 --- /dev/null +++ b/www/Tutorial-1.html @@ -0,0 +1,183 @@ + + + + + + KLEE - Tutorial One + + + + + +

+ +

Tutorial One: Testing a Small Function

+ + +

The demo code

+ + This tutorial walks you through the main steps needed to test a + simple function with KLEE. Here is our simple function: + +

+  int my_islower(int x) {
+      if (x >= 'a' && x <= 'z')  
+         return 1;
+      else return 0;
+  }

+ + You can find the entire code for this example in the source tree + under examples/islower. A version of the source code can + also be accessed here. + +

Marking input as symbolic

+ + In order to test this function with KLEE, we need to run it + on symbolic input. To mark a variable as symbolic, we use + the klee_make_symbolic() 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 main() function that marks a + variable c as symbolic and uses it to + call my_islower(): + +

+  int main() {
+      char c;
+      klee_make_symbolic(&c, sizeof(c), "input"); 
+      return my_islower(c);
+  }

+ + + +

Compiling to LLVM bitcode

+ + KLEE operates on LLVM bitcode. To run a program with KLEE, you + first compile it to LLVM bitcode using llvm-gcc + --emit-llvm. Assuming our code is stored in demo.c, + we run: + +

+ llvm-gcc --emit-llvm -c -g demo.c +

+ + to generate the LLVM bitcode file demo.o. + + It is useful to (1) build with -g 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 + --optimize command line option to run the optimizer + internally. + +

Running KLEE

+ + To run KLEE on the bitcode file simply execute: + +

+ klee demo.o +

+ + You should see the following output: +

+  KLEE: output directory = "klee-out-0"
+  KLEE: done: total instructions = 69  
+  KLEE: done: completed paths = 3      
+  KLEE: done: generated tests = 3

+ + There are three paths through our simple function, one + where x is less than 'a', one where x is + between 'a' and 'z' (so it's a lowercase letter), + and one where x is greater than 'z'. + + 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 klee-out-0) containing the test cases generated by + KLEE. KLEE names the output directory klee-out-N where N + is the lowest available number (so if we run KLEE again it will + create a directory called klee-out-1), and also generates a + symbolic link called klee-last to this directory for + convenience: + +

+  $ ls klee-last/
+  assembly.ll      run.istats       test000002.ktest
+  info             run.stats        test000003.ktest
+  messages.txt     test000001.ktest warnings.txt

+ + Please click here 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. + +

KLEE-generated test cases

The test cases generated by KLEE + are written in files with extension .ktest. These are + binary files, which can be read with the ktest-tool + utility. So let's examine each file: + +

+  $ ktest-tool klee-last/test000001.ktest 
+  ktest file : 'klee-last/test000001.ktest'
+  args       : ['demo.o']
+  num objects: 1
+  object    0: name: 'input'
+  object    0: size: 1
+  object    0: data: 'b'
+
+  $ ktest-tool klee-last/test000002.ktest 
+  ...
+  object    0: data: '~'
+
+  $ ktest-tool klee-last/test000003.ktest 
+  ..
+  object    0: data: '\x00'

+ + 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 ('input') and its size + (1). The actual test itself is represented by the value of our + input: 'b' for the first test, '~' for the second + and 0 for the last one. As expected, KLEE generated a + character which is a lowercase letter ('b'), one which is + less than 'a' (0), and one which is greater + than 'z' ('~'). We can now run these values on a + native version of our program, to exercise all paths through the + code! + + +

Replaying a test case

+ + 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 replay library, which simply replaces + the call to klee_make_symbolic with a call to a function + that assigns to our input the value stored in the .ktest + file. + + To use it, simply link your program with the libkleeRuntest + library and set the KTEST_FILE environment variable to + point to the name of the desired test case: + +

+  $ gcc ~/klee/Release/lib/libkleeRuntest.dylib demo.c
+  $ KTEST_FILE=klee-last/test000001.ktest ./a.out 
+  $ echo $?
+  1
+  $ KTEST_FILE=klee-last/test000002.ktest ./a.out 
+  $ echo $?
+  0
+  $ KTEST_FILE=klee-last/test000003.ktest ./a.out
+  $ echo $?
+  0

+ + As expected, our program returns 1 when running the first test case + (which contains the lowercase letter 'b'), and 0 when + running the other two (which don't contain lowercase letters). + +

+ +

+ + diff --git a/www/Tutorials.html b/www/Tutorials.html new file mode 100644 index 00000000..21ca3f29 --- /dev/null +++ b/www/Tutorials.html @@ -0,0 +1,28 @@ + + + + + + KLEE - Tutorials + + + + + +

+ +

KLEE Tutorials

+ + +

Tutorial One: Testing a small function.
Tutorial Two: Testing a simple regular + expression library.

+ + +

+ + diff --git a/www/code-examples/demo.c b/www/code-examples/demo.c deleted file mode 100644 index 2bf1c00d..00000000 --- a/www/code-examples/demo.c +++ /dev/null @@ -1,11 +0,0 @@ -int my_islower(int x) { - if (x >= 'a' && x <= 'z') - return 1; - else return 0; -} - -int main() { - char c; - klee_make_symbolic(&c, sizeof(c), "input"); - return my_islower(c); -} diff --git a/www/menu.html.incl b/www/menu.html.incl index 1c15ab44..22d6e578 100644 --- a/www/menu.html.incl +++ b/www/menu.html.incl @@ -8,7 +8,7 @@ About Getting Started Get Involved - Tutorials + Tutorials

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 @@ + + + +Enscript Output + + + + +

islower.c

+ +

+/*
+ * First KLEE tutorial: testing a small function
+ */
+
+#include <klee/klee.h>
+
+int my_islower(int x) {
+  if (x >= 'a' && x <= 'z')
+    return 1;
+  else return 0;
+}
+
+int main() {
+  char c;
+  klee_make_symbolic(&c, sizeof(c), "input");
+  return my_islower(c);
+}
+

Generated by GNU enscript 1.6.4.

+ + diff --git a/www/tutorial-1.html b/www/tutorial-1.html deleted file mode 100644 index 3f9bfc4e..00000000 --- a/www/tutorial-1.html +++ /dev/null @@ -1,181 +0,0 @@ - - - - - - KLEE - Tutorial One - - - - - -

- -

Tutorial One: Testing a Small Function

- - -

The demo code

- - This tutorial walks you through the main steps needed to test a - simple function with KLEE. Here is our simple function: - -

-  int my_islower(int x) {
-      if (x >= 'a' && x <= 'z')  
-         return 1;
-      else return 0;
-  }

- - You can find the entire code for this example here. - -

Marking input as symbolic

- - In order to test this function with KLEE, we need to run it - on symbolic input. To mark a variable as symbolic, we use - the klee_make_symbolic() 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 main() function that marks a - variable c as symbolic and uses it to - call my_islower(): - -

-  int main() {
-      char c;
-      klee_make_symbolic(&c, sizeof(c), "input"); 
-      return my_islower(c);
-  }

- - - -

Compiling to LLVM bitcode

- - KLEE operates on LLVM bitcode. To run a program with KLEE, you - first compile it to LLVM bitcode using llvm-gcc - --emit-llvm. Assuming our code is stored in demo.c, - we run: - -

- llvm-gcc --emit-llvm -c -g demo.c -

- - to generate the LLVM bitcode file demo.o. - - It is useful to (1) build with -g 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 - --optimize command line option to run the optimizer - internally. - -

Running KLEE

- - To run KLEE on the bitcode file simply execute: - -

- klee demo.o -

- - You should see the following output: -

-  KLEE: output directory = "klee-out-0"
-  KLEE: done: total instructions = 69  
-  KLEE: done: completed paths = 3      
-  KLEE: done: generated tests = 3

- - There are three paths through our simple function, one - where x is less than 'a', one where x is - between 'a' and 'z' (so it's a lowercase letter), - and one where x is greater than 'z'. - - 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 klee-out-0) containing the test cases generated by - KLEE. KLEE names the output directory klee-out-N where N - is the lowest available number (so if we run KLEE again it will - create a directory called klee-out-1), and also generates a - symbolic link called klee-last to this directory for - convenience: - -

-  $ ls klee-last/
-  assembly.ll      run.istats       test000002.ktest
-  info             run.stats        test000003.ktest
-  messages.txt     test000001.ktest warnings.txt

- - Please click here 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. - -

KLEE-generated test cases

The test cases generated by KLEE - are written in files with extension .ktest. These are - binary files, which can be read with the ktest-tool - utility. So let's examine each file: - -

-  $ ktest-tool klee-last/test000001.ktest 
-  ktest file : 'klee-last/test000001.ktest'
-  args       : ['demo.o']
-  num objects: 1
-  object    0: name: 'input'
-  object    0: size: 1
-  object    0: data: 'b'
-
-  $ ktest-tool klee-last/test000002.ktest 
-  ...
-  object    0: data: '~'
-
-  $ ktest-tool klee-last/test000003.ktest 
-  ..
-  object    0: data: '\x00'

- - 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 ('input') and its size - (1). The actual test itself is represented by the value of our - input: 'b' for the first test, '~' for the second - and 0 for the last one. As expected, KLEE generated a - character which is a lowercase letter ('b'), one which is - less than 'a' (0), and one which is greater - than 'z' ('~'). We can now run these values on a - native version of our program, to exercise all paths through the - code! - - -

Replaying a test case

- - 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 replay library, which simply replaces - the call to klee_make_symbolic with a call to a function - that assigns to our input the value stored in the .ktest - file. - - To use it, simply link your program with the libkleeRuntest - library and set the KTEST_FILE environment variable to - point to the name of the desired test case: - -

-  $ gcc ~/klee/Release/lib/libkleeRuntest.dylib demo.c
-  $ KTEST_FILE=klee-last/test000001.ktest ./a.out 
-  $ echo $?
-  1
-  $ KTEST_FILE=klee-last/test000002.ktest ./a.out 
-  $ echo $?
-  0
-  $ KTEST_FILE=klee-last/test000003.ktest ./a.out
-  $ echo $?
-  0

- - As expected, our program returns 1 when running the first test case - (which contains the lowercase letter 'b'), and 0 when - running the other two (which don't contain lowercase letters). - -

- -

- - diff --git a/www/tutorials.html b/www/tutorials.html deleted file mode 100644 index 795c629e..00000000 --- a/www/tutorials.html +++ /dev/null @@ -1,29 +0,0 @@ - - - - - - KLEE - Tutorials - - - - - -

- -

KLEE Tutorials

- - -

Tutorial One: Using KLEE on a toy - example.
Tutorial Two: Testing a simple regular - expression library.

- - -

- - -- cgit 1.4.1