Overview

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.

Examining Output

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:

1. If start == 0, the bug was found at distance 0
2. If start != 0, the bug was found at distance current - start + 1

The current format is slightly cumbersome and may change in the future.

Command Line Reference

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.