Write "Step 6: Replaying KLEE generated test cases", using klee-replay.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@78168 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 305 insertions, 3 deletions

diff --git a/www/TestingCoreutils.html b/www/TestingCoreutils.html
index c4dc6c49..07169efe 100644
--- a/www/TestingCoreutils.html
+++ b/www/TestingCoreutils.html
@@ -33,7 +33,8 @@
   <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, which is what was used for our OSDI paper.
+    example we use version 6.11 (one version later than what was used for our
+    OSDI paper).
   </p>
 
   <p>
@@ -87,7 +88,53 @@ 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>
@@ -572,7 +619,256 @@ Line 4:      b = c; </pre>
   
   <h2>Step 6: Replaying KLEE generated test cases </h2>
 
-  To be written.
+  <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 --init-env ./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>
 
   <!--*********************************************************************-->
   
@@ -580,6 +876,12 @@ Line 4:      b = c; </pre>
 
   To be written.
 
+  <!--*********************************************************************-->
+  
+  <h2>Step 8: Using <tt>zcov</tt> to analyze coverage </h2>
+
+  To be written.
+
 </div>
 </body>
 </html>