Docovery VM

Docovery is made available in a binary form, pre-installed in a virtual machine. For more details on Docovery and the benchmarks, please see the ASE’14 paper.

Virtual machine

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.

The VM was prepared under VirtualBox and is based on Ubuntu 12 (the same major version as used in our paper).

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 experiments with 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.

Directory structure

  • /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)

Re-running experiments

The results of re-run experiments can be found under /home/docovery/docovery/tests/results.

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

  • cd /home/docovery/docovery/tests

  • ./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 pr (please 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:

  • au-tom-ator.log_DATE_AND_TIME : the log of running all commands from the xml file
  • au-tom-ator.status_DATE_AND_TIME : the log of the cpu, disk and memory consumption over the execution of the test
  • au-tom-ator.stderr_DATE_AND_TIME : standard error of the commands executed in the test
  • au-tom-ator.stdout_DATE_AND_TIME : standard output of the commands executed in the test
  • au-tom-ator_prConcolicNativeCyclicConstrOptCexCache.xml_DATE_AND_TIME.tar.gz : compressed results of the test

The structure of the results directory at the example of prConcolicNativeCyclicConstrOptCexCache.xml:

  • a list of directories, named after the files under test; for out example these are 1p-end, 2p-end, 4p-end, 8p-end, 16p-end, 32p-end, 64p-end, 128p-end, 256p-end
    • inside each of these directories you will find klee-last directory containing the Docovery execution-related files and the recovery results
      • klee-last/doc-recov-data/recovery subdir 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
  • native directory storing native executable of the application and used to verify candidates
  • doc-recov directory containing a symbolic link to Docovery executable
  • log files for test, status, stdout and stderr
  • the xml test file itself
  • a *.bc file : an LLVM bit code for the tested application; in our example that is pr.bc
  • a bunch of helper information files

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)