diff options
| -rw-r--r-- | www/TestingCoreutils.html | 308 |
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> |