This is a step-by-step walkthrough for reproducing our Coreutils results using ZESTI. See the main project page for a high-level overview and download details.
The first step is to retrieve and compile Coreutils 6.10. Follow the instructions at http://klee.github.io/klee/TestingCoreutils.html for this purpose. For simplicity, we assume that Coreutils are compiled in-place i.e. the src/ folder contains all bitcode files. Export the location of the Coreutils folder to a global variable such as
$ export CU=/data/coreutils-6.10
Coreutils is different than most other software packages because it has many (89) programs. To transparently
have make test invoke ZESTI we first need to create wrappers for these programs. Create a file named $CU/zesti.tmpl
containing
the ZESTI invocation to be used:
#!/bin/sh
klee --zest --use-symbex=1 --symbex-for=10 --search=zest --zest-search-heuristic=br --watchdog --max-time=30 --optimize --max-cex-size=0 --zest-continue-after-error=true --output-source=false --no-std-out --output-level=error --use-cex-cache=false ---dump-states-on-halt=false -use-forked-stp --max-stp-time=10 --posix-runtime --libc=uclibc $CU/src/TEMPLATE-EXE.bc ${1+"$@"}
See the command line reference for details about the arguments used.
Create a script in $CU/run-test.sh
to setup the wrapper for a particular program and run the tests
#!/bin/bash
if [ "X$1" == X ]; then
echo "Usage: $0 <executable> [test folder] [tests]"
else
if [ "X$2" == X ]; then
TDIR=$1
else
TDIR=$2
fi
fi
cd src
for f in *.bc; do
fsimple=${f%.*}
rm -f $fsimple
if [ -x /bin/$fsimple ]; then
ln -s /bin/$fsimple
elif [ -x /usr/bin/$fsimple ]; then
ln -s /usr/bin/$fsimple
fi
done
rm -f $1
cd ..
sed "s/TEMPLATE-EXE/$1/g" zesti.tmpl > src/$1
chmod 755 src/$1
if [ "X$3" == "X" ]; then
make check -C tests/$TDIR/
else
make check -C tests/$TDIR/ "TESTS=$3"
fi
You can now directly invoke this script to test a program, for example $ ./run-test.sh cut
. Note that the command
will take roughly 90 minutes to execute, since cut has a large number of regression tests.
Some Coreutils programs have their tests structured differently, bundled together with other programs in the misc-tests folder.
You can run them using an additional wrapper shown below ($CU/run-misc.sh
)
#!/bin/bash
if [ "X$1" == X ]; then
echo "Usage: $0 <program>"
else
f=$1
TESTS=$(find tests/tests-misc/ -maxdepth 1 -executable \( -name "$f-*" -o -name $f \) -type f -printf "%f ")
if [ "X$TESTS" == X ]; then
echo No tests available for $f
else
echo Running tests for $f: $TESTS
./run-test.sh $f tests-misc "$TESTS"
fi
fi
Note: if using Coreutils 6.11, replace tests-misc
with misc
in the above script.
Testing the printf program for example, is done using $ ./run-misc.sh printf
Combining the two scripts to test all Coreutils programs automatically is straightforward.
ZESTI outputs information regarding the sensitive instructions found in the messages.txt file found in the klee-out-* folders. The messages have the self-explanatory format
KLEE: Sensitive instruction (depth 45) @ /data/coreutils-6.10/src/cut.c:375
The depth refers to the number of symbolic branches zesti followed until reaching the sensitive instruction. Note that only one sensitive instruction per depth is listed even if more exist; multiple sensitive instructions have the same effect as a single one on the search strategy and are not recorded for efficiency reasons.
Whenever ZESTI finds a bug, it logs in the associated .ptr.err
file details regarding the bug depth. The most
important lines are
SE started at depth/instruction <start> Current depth <current>
The algorithm for determining the distance at which the bug was found in this particular instance is:
The current format is slightly cumbersome and may change in the future.
ZESTI is implemented on top of KLEE and supports all options available for KLEE. In addition, it introduces several other command line arguments described below, along with their default option.
--zest
This option enables ZESTI. Without it, the system will behave as KLEE. Default false.--enable-symbex
This instructs ZESTI to search beyond distance 0. Default 0 (false).--search=zest
This instructs ZESTI to use its own iterative deepening algorithm for state selection instead of the default KLEE algorithm.--zest-search-heuristic
The metric to be used by the ZESTI searcher for distance computation.
By default, symbolic branches are used. You should not modify this.--zest-search-until
The maximum distance to search for. Default 500; you should almost always use a time limit when setting this to a large value.