[llvm-commits] [klee] r72515 - in /klee/trunk: examples/islower/ examples/islower/islower.c www/GetStarted.html www/Tutorial-1.html www/Tutorials.html www/code-examples/demo.c www/menu.html.incl www/resources/islower.c.html www/tutorial-1.html www/tutorials.html
Cristian Cadar
cristic at cs.stanford.edu
Wed May 27 21:44:50 PDT 2009
Author: cristic
Date: Wed May 27 23:44:50 2009
New Revision: 72515
URL: http://llvm.org/viewvc/llvm-project?rev=72515&view=rev
Log:
Changes to webpage to make both tutorials use the same template.
Added:
klee/trunk/examples/islower/
klee/trunk/examples/islower/islower.c
- copied, changed from r72512, klee/trunk/www/code-examples/demo.c
klee/trunk/www/Tutorial-1.html
- copied, changed from r72512, klee/trunk/www/tutorial-1.html
klee/trunk/www/Tutorials.html
- copied, changed from r72512, klee/trunk/www/tutorials.html
klee/trunk/www/resources/islower.c.html
Removed:
klee/trunk/www/code-examples/demo.c
klee/trunk/www/tutorial-1.html
klee/trunk/www/tutorials.html
Modified:
klee/trunk/www/GetStarted.html
klee/trunk/www/menu.html.incl
Copied: klee/trunk/examples/islower/islower.c (from r72512, klee/trunk/www/code-examples/demo.c)
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/examples/islower/islower.c?p2=klee/trunk/examples/islower/islower.c&p1=klee/trunk/www/code-examples/demo.c&r1=72512&r2=72515&rev=72515&view=diff
==============================================================================
--- klee/trunk/www/code-examples/demo.c (original)
+++ klee/trunk/examples/islower/islower.c Wed May 27 23:44:50 2009
@@ -1,3 +1,9 @@
+/*
+ * First KLEE tutorial: testing a small function
+ */
+
+#include <klee/klee.h>
+
int my_islower(int x) {
if (x >= 'a' && x <= 'z')
return 1;
Modified: klee/trunk/www/GetStarted.html
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/www/GetStarted.html?rev=72515&r1=72514&r2=72515&view=diff
==============================================================================
--- klee/trunk/www/GetStarted.html (original)
+++ klee/trunk/www/GetStarted.html Wed May 27 23:44:50 2009
@@ -86,7 +86,7 @@
</div>
</li>
- <li>You're ready to go! Go to the <a href="tutorials.html">Tutorials</a> page
+ <li>You're ready to go! Go to the <a href="Tutorials.html">Tutorials</a> page
to try KLEE.</li>
</ol>
Copied: klee/trunk/www/Tutorial-1.html (from r72512, klee/trunk/www/tutorial-1.html)
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/www/Tutorial-1.html?p2=klee/trunk/www/Tutorial-1.html&p1=klee/trunk/www/tutorial-1.html&r1=72512&r2=72515&rev=72515&view=diff
==============================================================================
--- klee/trunk/www/tutorial-1.html (original)
+++ klee/trunk/www/Tutorial-1.html Wed May 27 23:44:50 2009
@@ -27,7 +27,9 @@
else return 0;
} </pre>
- You can find the entire code for this example <a href="code-examples/demo.c">here</a>.
+ You can find the entire code for this example in the source tree
+ under <tt>examples/islower</tt>. A version of the source code can
+ also be accessed <a href="resources/islower.c.html">here</a>.
<h2>Marking input as symbolic</h2>
Copied: klee/trunk/www/Tutorials.html (from r72512, klee/trunk/www/tutorials.html)
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/www/Tutorials.html?p2=klee/trunk/www/Tutorials.html&p1=klee/trunk/www/tutorials.html&r1=72512&r2=72515&rev=72515&view=diff
==============================================================================
--- klee/trunk/www/tutorials.html (original)
+++ klee/trunk/www/Tutorials.html Wed May 27 23:44:50 2009
@@ -16,8 +16,7 @@
<!--*********************************************************************-->
<ol>
- <li><a href="tutorial-1.html">Tutorial One</a>: Using KLEE on a toy
- example.</li>
+ <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>
Removed: klee/trunk/www/code-examples/demo.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/www/code-examples/demo.c?rev=72514&view=auto
==============================================================================
--- klee/trunk/www/code-examples/demo.c (original)
+++ klee/trunk/www/code-examples/demo.c (removed)
@@ -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);
-}
Modified: klee/trunk/www/menu.html.incl
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/www/menu.html.incl?rev=72515&r1=72514&r2=72515&view=diff
==============================================================================
--- klee/trunk/www/menu.html.incl (original)
+++ klee/trunk/www/menu.html.incl Wed May 27 23:44:50 2009
@@ -8,7 +8,7 @@
<a href="index.html">About</a>
<a href="GetStarted.html">Getting Started</a>
<a href="GetInvolved.html">Get Involved</a>
- <a href="tutorials.html">Tutorials</a>
+ <a href="Tutorials.html">Tutorials</a>
</div>
<div class="submenu">
Added: klee/trunk/www/resources/islower.c.html
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/www/resources/islower.c.html?rev=72515&view=auto
==============================================================================
--- klee/trunk/www/resources/islower.c.html (added)
+++ klee/trunk/www/resources/islower.c.html Wed May 27 23:44:50 2009
@@ -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>
Removed: klee/trunk/www/tutorial-1.html
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/www/tutorial-1.html?rev=72514&view=auto
==============================================================================
--- klee/trunk/www/tutorial-1.html (original)
+++ klee/trunk/www/tutorial-1.html (removed)
@@ -1,181 +0,0 @@
-<!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 my_islower(int x) {
- if (x >= 'a' && x <= 'z')
- return 1;
- else return 0;
- } </pre>
-
- You can find the entire code for this example <a href="code-examples/demo.c">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>c</tt> as symbolic and uses it to
- call <tt>my_islower()</tt>:
-
- <pre class="code">
- int main() {
- char c;
- klee_make_symbolic(&c, sizeof(c), "input");
- return my_islower(c);
- } </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>demo.c</tt>,
- we run:
-
- <div class="instr">
- llvm-gcc --emit-llvm -c -g demo.c
- </div>
-
- to generate the LLVM bitcode file <tt>demo.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 demo.o
- </div>
-
- You should see the following output:
- <pre class="output">
- KLEE: output directory = "klee-out-0"
- KLEE: done: total instructions = 69
- KLEE: done: completed paths = 3
- KLEE: done: generated tests = 3 </pre>
-
- There are three paths through our simple function, one
- where <tt>x</tt> is less than <tt>'a'</tt>, one where <tt>x</tt> is
- between <tt>'a'</tt> and <tt>'z'</tt> (so it's a lowercase letter),
- and one where <tt>x</tt> is greater than <tt>'z'</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 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' </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 ('input') and its size
- (1). The actual test itself is represented by the value of our
- input: <tt>'b'</tt> for the first test, <tt>'~'</tt> for the second
- and <tt>0</tt> for the last one. As expected, KLEE generated a
- character which is a lowercase letter (<tt>'b'</tt>), one which is
- less than <tt>'a'</tt> (<tt>0</tt>), and one which is greater
- than <tt>'z'</tt> (<tt>'~'</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">
- $ 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 </pre>
-
- As expected, our program returns 1 when running the first test case
- (which contains the lowercase letter <tt>'b'</tt>), and 0 when
- running the other two (which don't contain lowercase letters).
-
- <br/><br/>
-
-</div>
-</body>
-</html>
Removed: klee/trunk/www/tutorials.html
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/www/tutorials.html?rev=72514&view=auto
==============================================================================
--- klee/trunk/www/tutorials.html (original)
+++ klee/trunk/www/tutorials.html (removed)
@@ -1,29 +0,0 @@
-<!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>: Using KLEE on a toy
- example.</li>
-
- <li><a href="Tutorial-2.html">Tutorial Two</a>: Testing a simple regular
- expression library.</li>
- </ol>
-
-
-</div>
-</body>
-</html>
More information about the llvm-commits
mailing list