Test Cases Manually Added and Generated by KLEE's Shadow Symbolic Execution

This dataset contains test cases that were manually designed and automatically generated using KLEE's shadow symbolic execution (see Shadow ICSE2016) and employed in the empirical study: An Empirical Study on Mutation, Statement and Branch Coverage Fault Revelation that Avoids the Unreliable Clean Program Assumption (ICSE2017).

These tests were designed to run on the version pre/post bux fixing commit of 68 of the 70 CoreBEnch subjects. Users just need integrate these tests with CoreBEnch, for compilation of OLD and NEW verions (see bellow), and run the tests.

OLD version represents the version pre bug fixing commit NEW version represents the version post bug fixing commit

These tests use the NEW version's output as oracle to test OLD version, therefore requires both OLD version and NEW version to be compiled.

Integration with Corebench

Insert the call to the CoreBEnch script for building respectively the version pre bug fix commit (OLD) and post bug fix commit (NEW) into the script corebenchBuild.sh. The executables generated after compilation will be copied into the directory build-versions described bellow.

Directory structure

1. klee-replay contain the executable of the program klee-replay (version used by shadow version of KLEE) necessary to execute KLEE's generated tests.
2. subjects contain 68 directory of the 70 bugs of corebench (except IDs 64 and 65). each directory name represent the corresponding CoreBEnch bug ID. Each subject contain:
   • testscripts which contains the modified version of the tests scripts of the programs.
   • genktests which contains the .ktest files generated by KLEE's Shadow and and based on the tests in testscripts
   • build-versions where the executables are store and used in a wrapper duringtest execution
   • test-verdict-output contains the result of test execution in a file <bugID>-ktestPassFail.txt (automatically created during test execution). in the file, 0 means test pass and 1 means test fail. Note: the list of test generated and manually added are found in <bugID>-ktestlist.txt

Run the tests

call the script run.sh with the corebench bug ID, the repo root directory and the keyword tests in order to execute all the tests. for example, assume that the subject bugID 1 have the repo directory path/to/repo/1. the test execution will be:

   ./run.sh 1 path/to/repo/1 tests

This command will first copy the tests from testscripts into the repository, then execute the tests and store the results into test-verdict-output , and finaly restore the original test of the repo.

---

By Thierry Titcheu Chekam University of Luxembourg (SnT)

Email: thierry.titcheu-chekam@uni.lu

please contact me if you have questions about this.

---