From 1d539296be5701036e8c48dac75add46eaf03a3f Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Wed, 5 Aug 2009 05:40:51 +0000 Subject: 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 --- www/TestingCoreutils.html | 308 +++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 305 insertions(+), 3 deletions(-) (limited to 'www/TestingCoreutils.html') 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 @@

First you will need to download and unpack the source for coreutils. 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).

@@ -87,7 +88,53 @@ There is NO WARRANTY, to the extent permitted by law. Written by Torbjorn Granlund and Richard M. Stallman. - + +

+ In addition, these executables should be built with gcov support, + so if you run one it will write a .gcda into the current + directory. That file contains information about exactly what code was + executed when the program ran. See + the Gcov + Documentation for more information. We can use the gcov tool + itself to produce a human readable form of the coverage information. For + example: +

+ +
+ 
+src$ rm -f *.gcda # Get rid of any stale gcov files
+src$ ./echo
+
+src$ ls -l echo.gcda
+-rw-r--r-- 1 ddunbar ddunbar 1832 2009-08-04 21:14 echo.gcda
+src$ gcov echo
+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'
+
+ +

+ By default gcov will show the number of lines executed in the + program (the .h files include code which was compiled + into echo.c). +

+

Step 2: Build coreutils with LLVM

@@ -572,7 +619,256 @@ Line 4: b = c;

Step 6: Replaying KLEE generated test cases

- To be written. +

+ Let's step away from KLEE for a bit and look at just the test cases KLEE + generated. If we look inside the klee-last we should see + 25 .ktest files. +

+ +
+ 
+src$ ls klee-last
+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
+
+ +

+ 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 ktest-tool: +

+ +
+ 
+$ ktest-tool klee-last/test000001.ktest
+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'
+
+ +

+ In this case, the test case indicates that values "@@@\x00" should be passed + as the first argument. However, .ktest files generally aren't + really meant to be looked at directly. For the POSIX runtime, we provide a + tool klee-replay which can be used to read the .ktest file + and invoke the native application, automatically passing it the data + necessary to reproduce the path that KLEE followed. +

+ +

+ To see how it works, go back to the directory where we built the native + executables: +

+ +
+ 
+src$ cd ..
+obj-llvm$ cd ..
+coreutils-6.11$ cd obj-gcov
+obj-gcov$ cd src
+src$ ls -l echo
+-rwxr-xr-x 1 ddunbar ddunbar 151051 2009-07-25 20:59 echo
+
+ +

+ To use the klee-replay tool, we just tell it the executable to run + and the .ktest file to use. The program arguments, input files, + etc. will all be constructed from the data in the .ktest file. +

+ +
+ 
+src$ klee-replay ./echo ../../obj-llvm/src/klee-last/test000001.ktest 
+klee-replay: TEST CASE: ../../obj-llvm/src/klee-last/test000001.ktest
+klee-replay: ARGS: "./echo" "@@@" 
+@@@
+klee-replay: EXIT STATUS: NORMAL (0 seconds)
+
+ +

+ The first two and last lines here come from the klee-replay 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 .ktest file earlier). The last line is + the exit status of the program and the elapsed time to run. +

+ +

+ We can also use the klee-replay tool to run a set of test cases at + once, one after the other. Let's do this and compare the gcov + coverage to the numbers we got from klee-stats: +

+ +
+ 
+src$ rm -f *.gcda # Get rid of any stale gcov files
+src$ klee-replay ./echo ../../obj-llvm/src/klee-last/*.ktest 
+klee-replay: TEST CASE: ../../obj-llvm/src/klee-last/test000001.ktest
+klee-replay: ARGS: "./echo" "@@@" 
+@@@
+klee-replay: EXIT STATUS: NORMAL (0 seconds)
+...
+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.
+...
+
+src$ gcov echo
+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'
+
+ +

+ The number for echo.c here significantly higher than + the klee-stats number because gcov is only considering + lines in that one file, not the entire application. As with kcachegrind, we can inspect the coverage file output by gcov to see exactly what lines were covered and which weren't. Here is a fragment from the output: +

+ +
+ 
+        -:  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;
+
+ +

+ The far left hand column is the number of times each line was + executed; - means the line has no executable code, and ##### + means the line was never covered. As you can see, the uncovered lines here + correspond exactly to the uncovered lines as reported + in kcachegrind. +

+ +

+ Before moving on to testing more complex applications, lets make sure we can + get decent coverage of the simple echo.c. 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 --sym-args option to pass multiple options. Here + are the steps, after switching back to the obj-llvm/src directory: +

+ +
+ 
+src$ klee --only-output-states-covering-new --optimize --libc=uclibc --posix-runtime --init-env ./echo.bc --sym-args 0 2 4
+ ... 
+KLEE: done: total instructions = 7437521
+KLEE: done: completed paths = 9963
+KLEE: done: generated tests = 55
+
+ +

+ The format of the --sym-args option actually specifies a minimum + and a maximum number of arguments to pass and the length to use for each + argument. In this case --sym-args 0 2 4 says to pass between 0 and + 2 arguments (inclusive), each with a maximum length of four characters. +

+ +

+ We also added the --only-output-states-covering-new option to the + KLEE command line. By default KLEE will write out test cases for every path + it explores. This becomes less useful 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. +

+ +

+ If we go back to the obj-gcov/src directory and rerun the latest + set of test cases, we finally have reasonable coverage of echo.c: +

+ +
+ 
+src$ rm -f *.gcda # Get rid of any stale gcov files
+src$ klee-replay ./echo ../../obj-llvm/src/klee-last/*.ktest 
+klee-replay: TEST CASE: ../../obj-llvm/src/klee-last/test000001.ktest
+klee-replay: ARGS: "./echo" 
+
+ ... 
+
+src$ gcov echo
+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'
+
+ +

+ The reasons for not getting perfect 100% line coverage are left as an + exercise to the reader. :) +

@@ -580,6 +876,12 @@ Line 4: b = c; To be written. + + +

Step 8: Using zcov to analyze coverage

+ + To be written. + -- cgit 1.4.1