aboutsummaryrefslogtreecommitdiffhomepage
path: root/www/TestingCoreutils.html
diff options
context:
space:
mode:
Diffstat (limited to 'www/TestingCoreutils.html')
-rw-r--r--www/TestingCoreutils.html308
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>