From b42f6baf4358a81683cd0ab1a8529683a6819ab5 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Tue, 22 Jan 2013 20:47:10 +0000 Subject: Some information about the Coreutils experiments presented in the KLEE OSDI paper. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@173191 91177308-0d34-0410-b5e6-96231b3b80d8 --- www/CoreutilsExperiments.html | 145 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 145 insertions(+) create mode 100644 www/CoreutilsExperiments.html (limited to 'www/CoreutilsExperiments.html') diff --git a/www/CoreutilsExperiments.html b/www/CoreutilsExperiments.html new file mode 100644 index 00000000..bd48e823 --- /dev/null +++ b/www/CoreutilsExperiments.html @@ -0,0 +1,145 @@ + + + + + + KLEE - Coreutils Experiments + + + + + +
+ +

Coreutils Experiments

+ +

+ This document is meant to give additional information regarding + the Coreutils experiments discussed in + our KLEE + OSDI'08 paper. However, please note that in the last several + years, KLEE and its dependencies (particularly LLVM and STP), have + undergone major changes, which have resulted in considerable + different behavior on several benchmarks, including Coreutils.

+ +

+ This document is structured as a series of FAQs: +

+ +
    +
  1. How did you build Coreutils?
    + Please follow the instructions in the Coreutils Tutorial. +
    2. + +
  2. What version of LLVM was used in the OSDI paper?
    + We generally kept in sync with the LLVM top-of-tree, which at the time + was somewhere around LLVM 2.2 and 2.3.
    3. + + +
  3. What version of STP was used in the OSDI paper?
    + An old version of STP, which is still available as part of KLEE's + repository, in revisions up to r161056. +
    4. + +
  4. What options did you run KLEE with?
    + We used the following options (the command below is for paste): +
    +$ klee --simplify-sym-indices --write-cvcs --write-cov --output-module \
    + --max-memory=1000 --disable-inlining --optimize --use-forked-stp \
    + --use-cex-cache --with-libc --with-file-model=release \
    + --allow-external-sym-calls --only-output-states-covering-new \
    + --exclude-libc-cov --exclude-cov-file=./../lib/functions.txt \
    + --environ=test.env --run-in=/tmp/sandbox --output-dir=paste-data-1h \
    + --max-sym-array-size=4096 --max-instruction-time=10. --max-time=3600. \
    + --watchdog --max-memory-inhibit=false --max-static-fork-pct=1 \
    + --max-static-solve-pct=1 --max-static-cpfork-pct=1 --switch-type=internal \
    + --randomize-fork --use-random-path --use-interleaved-covnew-NURS \
    + --use-batching-search --batch-instructions 10000 --init-env \
    + ./paste.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdout +
    + + Some of these options have been renamed or removed in the current + version of KLEE. Most notably, the options "--exclude-libc-cov" + and "--exclude-cov-file" were implemented in a fragile way and we + decided to remove them from KLEE. The idea was to treat the + functions in libc or specified in a text file as "covered". (For + the Coreutils experiments, we were interested in covering the + code in the tools themselves, as opposed to library code, see the + paper for more details). If you plan to reimplement these + options in a clean way, please consider contributing your code to the mainline. +
    5. + +
  5. What are the options closest to the ones above that + work with the current version KLEE?
    + Try the following: + +
    +$ klee --simplify-sym-indices --write-cvcs --write-cov --output-module \
    + --max-memory=1000 --disable-inlining --optimize --use-forked-stp \
    + --use-cex-cache --libc=uclibc --posix-runtime \
    + --allow-external-sym-calls --only-output-states-covering-new \
    + --environ=test.env --run-in=/tmp/sandbox \
    + --max-sym-array-size=4096 --max-instruction-time=30. --max-time=3600. \
    + --watchdog --max-memory-inhibit=false --max-static-fork-pct=1 \
    + --max-static-solve-pct=1 --max-static-cpfork-pct=1 --switch-type=internal \
    + --randomize-fork --search=random-path --search=nurs:covnew \
    + --use-batching-search --batch-instructions=10000 \
    + ./paste.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdout +
    + +
    6. + +
  6. How do I generate test.env and /tmp/sandbox?
    + We used a simple environment and a "sandbox" directory to make + our experiments more deterministic. To recreate them, follow + these steps: +
      +
    1. Download testing-env.sh by clicking here, and place it in the current directory.
      2. +
    2. Create test.env by running: +
      + $ env -i /bin/bash -c '(source testing-env.sh; env >test.env)' +
      +
      3. +
    3. Download sandbox.tgz by clicking here, place it in /tmp, and run: +
      + $ cd /tmp + $ tar xzfv sandbox.tgz +
      +
      4. +
    +
    7. +
  7. + What symbolic arguments did you use in your experiments?
    + We ran most utilities using the arguments below. Our choice was + based on a high-level understanding of the Coreutils + applications: most behavior can be triggered with no more than two + short options, one long option, and two small input streams (stdin and one file). +
    + --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdout +
    + + + + For eight tools where the coverage results were unsatisfactory, +we consulted the man page and increased the number and size of +arguments and files as follows: +
    + dd: --sym-args 0 3 10 --sym-files 1 8 --sym-stdout
    + dircolors: --sym-args 0 3 10 --sym-files 2 12 --sym-stdout
    + echo: --sym-args 0 4 300 --sym-files 2 30 --sym-stdout
    + expr: --sym-args 0 1 10 --sym-args 0 3 2 --sym-stdout
    + mknod: --sym-args 0 1 10 --sym-args 0 3 2 --sym-files 1 8 --sym-stdout
    + od: --sym-args 0 3 10 --sym-files 2 12 --sym-stdout
    + pathchk: --sym-args 0 1 2 --sym-args 0 1 300 --sym-files 1 8 --sym-stdout
    + printf: --sym-args 0 3 10 --sym-files 2 12 --sym-stdout +
    + +
    8. + +
+ + +
+ + -- cgit 1.4.1