The VM comes with “docovery” user, for whom the password is the same as the user name. All the benchmark applications and the necessary infrastructure have been pre-installed under the VM.
Click here to download the virtual machine (name: Docovery-VM_clean.ova, size: 5.8GB, md5: 6491d7c63783e07e50a3a0e3aea841fc).
You can reproduce the experiments under the provided VM. The experiments were re-run and the results are stored under the VM.
Caveat: Unfortunately, since a real mailbox file was used for the original
Pine, we cannot make it available. As a replacement, we provide a “dummy”
mailboxes containing the same number of e-mails as the ones used in the original experiments.
If you have any further questions about the VM or you spot an issue, please contact Tomasz Kuchta.
/home/docovery : the home directory for the “docovery” user
/home/docovery/docovery : the main directory of interest
/home/docovery/docovery/benchmarks : this is where the files and the associated applications are stored
./FILES : files (for libdwarf and binutils also the original files provided)
./benchmarks : directory, where all the applications used for experiments were built
./bin : a helper directory to store application binaries and LLVM bytecode files
./specfiles : xml definitions of tests (they are interpreted by an automation infrastructure)
The results of re-run experiments can be found under
If you would like to reproduce the experiments, please follow these instructions:
Download the VM (it is the best to set the RAM amount of the virtual machine to 8GB, if possible)
Login as the “docovery” user
Open the terminal window
./run_tests_main.sh : this will run the main batch of tests
./run_tests_extended.sh : this will run extended tests (no
taints, collecting all the constraints, checking branch feasibility non-lazily)
Tests are run using Python-based infrastructure that executes commands defined in xml files. Once each xml file is processed and executed, the infrastructure creates a directory named after the file.
As an example, let’s consider running tests for
remember, that you can conveniently run all the tests using the
scripts mentioned above).
In the /home/docovery/docovery/tests you can
find all the necessary xml definition files. The file needed in our example is
prConcolicNativeCyclicConstrOptCexCache.xml. We can run the test by invoking:
au-tom-ator --compress=True --break-on-error=True --report-usage=5 prConcolicNativeCyclicConstrOptCexCache.xml
As a result, the following files will appear in the current directory:
The structure of the results directory at the example of prConcolicNativeCyclicConstrOptCexCache.xml:
klee-last/doc-recov-data/recoverysubdir contains all the recovery candidates in directories named ConstraintSet_NUMBER; each such directory corresponds to one execution path; ConstraintSet_00001_fail always corresponds to the original execution path taken by the application when processing the broken file
nativedirectory storing native executable of the application and used to verify candidates
doc-recovdirectory containing a symbolic link to Docovery executable
Tip: If you have an access to an SMTP server, you may find smtp-server and email options of the au-tom-ator infrastructure useful (see au-tom-ator help for details)