From bdc51567080a00a83c5d8d1ded8091a78ee7f50b Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Sun, 26 Jul 2009 11:35:07 +0000 Subject: A quick editing pass. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77157 91177308-0d34-0410-b5e6-96231b3b80d8 --- www/TestingCoreutils.html | 69 ++++++++++++++++++++++++----------------------- 1 file changed, 36 insertions(+), 33 deletions(-) (limited to 'www/TestingCoreutils.html') diff --git a/www/TestingCoreutils.html b/www/TestingCoreutils.html index 7dc95cda..c4dc6c49 100644 --- a/www/TestingCoreutils.html +++ b/www/TestingCoreutils.html @@ -38,7 +38,7 @@

Before we build with LLVM, let's build a version of coreutils - with gcov suppory. We will use this later to get coverage + with gcov support. We will use this later to get coverage information on the test cases produced by KLEE.

@@ -60,11 +60,10 @@

We build with --disable-nls because this adds a lot of extra - initialization in the C library which we were not interested in - testing. Even though these aren't the executables that KLEE will be running - on, we want to use the same compiler flags so that the test cases KLEE - generates are most likely to work correctly when run on the uninstrumented - binaries. + initialization in the C library which we are not interested in testing. Even + though these aren't the executables that KLEE will be running on, we want to + use the same compiler flags so that the test cases KLEE generates are most + likely to work correctly when run on the uninstrumented binaries.

@@ -94,17 +93,18 @@ Written by Torbjorn Granlund and Richard M. Stallman.

Step 2: Build coreutils with LLVM

- One of the difficult parts of testing real software using KLEE is that it must - be first compiled so that the final progress is an LLVM bitcode file and not a - linked executable. The software's build system may be set up to use tools such - as 'ar', 'libtool', and 'ld', which do not understand LLVM bitcode files. + One of the difficult parts of testing real software using KLEE is that it + must be first compiled so that the final program is an LLVM bitcode file and + not a linked executable. The software's build system may be set up to use + tools such as 'ar', 'libtool', and 'ld', which do not in general understand + LLVM bitcode files.

It depends on the actual project what the best way to do this is. For coreutils, we use a helper script klee-gcc, which acts like llvm-gcc but adds additional arguments to cause it to emit - LLVM bitcode files, and to call llvm-ld to link executables. This + LLVM bitcode files and to call llvm-ld to link executables. This is not a general solution, and your mileage may vary.

@@ -113,7 +113,7 @@ Written by Torbjorn Granlund and Richard M. Stallman.

As before, we will build in a separate directory so we can easily access - both the native executables, and the LLVM versions. Here are the steps: + both the native executables and the LLVM versions. Here are the steps:

@@ -135,7 +135,7 @@ Written by Torbjorn Granlund and Richard M. Stallman.

- If all went well, you should now how LLVM bitcode versions of coreutils! For + If all went well, you should now have LLVM bitcode versions of coreutils! For example:

@@ -161,8 +161,8 @@ LLVM ERROR: JIT does not support inline asm! too small! Since we are actually producing LLVM bitcode files, the operating system can't run them directly. What llvm-ld does to make it so we can still run the resulting outputs is write a little shell script which - just uses the LLVM interpreter to run the binaries, the actual LLVM bitcode - files have .bc appended. For example: + uses the LLVM interpreter to run the binaries; the actual LLVM bitcode + files have .bc appended. If we look a little closer:

@@ -181,10 +181,10 @@ exec $lli \ The other funny thing is that the version message doesn't all print out, the LLVM interpreter emits a message about not supporting inline assembly. The problem here is that glibc occasionally implements certain - operations using inline assembly, which lli doesn't - understand. KLEE works around this problem by specifically turning certain - inline assembly sequences back into the appropriate LLVM instructions before - executing the binary. + operations using inline assembly, which the LLVM interpreter (lli) + doesn't understand. KLEE works around this problem by specially recognizing + certain common inline assembly sequences and turning them back into the + appropriate LLVM instructions before executing the binary.

@@ -416,7 +416,7 @@ KLEE: done: generated tests = 25
     coreutils' echo takes some arguments, in this case the
     options --v (short for --version) and --h (short
     for --help) were explored. We can get a short summary of KLEE's
-    internal statistics be running klee-stats on the output directory
+    internal statistics by running klee-stats on the output directory
     (remember, KLEE always makes a symlink called klee-last to the most
     recent output directory).
   

@@ -435,7 +435,7 @@ KLEE: done: generated tests = 25
     Here ICov is the percentage of LLVM instructions which were
     covered, and BCov is the percentage of branches that were
     covered. You may be wondering why the percentages are so low -- how much
-    more code can echo have! The first reason is that these numbers are computed
+    more code can echo have! The main reason is that these numbers are computed
     using all the instructions or branches in the bitcode files; that includes a
     lot of library code which may not even be executable. We can help with that
     problem (and others) by passing the --optimize option to KLEE. This
@@ -463,9 +463,11 @@ src$ klee-stats klee-last
 
   

This time the instruction coverage went up by about ten percent, and you can - see that KLEE also ran faster and executed less instructions. To understand - why we still haven't gotten more coverage of the program, let's take a look - at using kcachegrind to visualize the results of a KLEE run. + see that KLEE also ran faster and executed less instructions. Most of the + remaining code is still in library functions, just in places that the + optimizers aren't smart enough to remove. We can verify this -- and look for + uncovered code inside echo -- by using KCachegrind to visualize the + results of a KLEE run.

@@ -476,15 +478,15 @@ src$ klee-stats klee-last KCachegrind is an excellent profiling visualization tool, originally written for use with the callgrind plugin for valgrind. If you don't have it already, it is usually easily - available on a modern Linux distribution via your platforms usual software + available on a modern Linux distribution via your platforms' software installation tool (e.g., apt-get or yum).

KLEE by default writes out a run.istats file into the test output - directory which is actually a kcachegrind file. In this example, + directory which is actually a KCachegrind file. In this example, the run.istats is from a run without --optimize, so the - results are easier to understand. Assuming you have kcachegrind installed, + results are easier to understand. Assuming you have KCachegrind installed, just run:

@@ -505,12 +507,13 @@ src$ klee-stats klee-last

KCachegrind is a complex application in itself, and interested users should - see the KCachegrind website. However, the basics are that the one pane shows - the "Flat Profile"; this is a list of which how many instructions were - executed in each function. The "Self" column is the number of instructions - which were executed in the function itself, and the "Incl" (inclusive) - column is the number of instructions which were executed in the function, or - any of the functions it called (and so on). + see the KCachegrind website for more information and documentation. However, + the basics are that the one pane shows the "Flat Profile"; this is a list of + which how many instructions were executed in each function. The "Self" + column is the number of instructions which were executed in the function + itself, and the "Incl" (inclusive) column is the number of instructions + which were executed in the function, or any of the functions it called (or + its callees called, and so on).

-- cgit 1.4.1