STEP (STate space ExPlorer) is a systematic test-input generation tool for Java programs. it is based on Symbolic Execution (SE) and reduces the overall cost of SE. It reduces the costs of path exploration and path execution by building on a linearized, Static Single Assignment (SSA) representation of the program under test, and exploiting incremental constraint solving.
- A Comparative Study of Incremental Constraint Solving Approaches in Symbolic Execution, Tianhai Liu, Mateus Borges, Marcelo d'Amorim and Mana Taghdiri. 10th Haifa Verification Conference (HVC), 2014
Tool and Benchmarks
- STEP binary: step.tar.xz. It is compiled in OpenJDK 1.7.
- STEP source: please contact us.
- Third-party software: STEP-ext-lib.zip. It consists of some libraries obtained from Z3, Soot. Guava, Jung, Jacoco and Apache Collections.
- Solver: STEP-Z3JNI.zip. It contains two Z3 compiled library files for 64-bit Linux. For additional platform supports, please compile Z3 following the instructions from Leonardo de Moura.
- Scripts: STEP-script.zip. It contains several scripts to facilitate STEP usage in command line, e.g., encapsulate Java options and link Z3 library files.
- Rugrat benchmark: STEP-bin.zip (binary) and STEP-rugrat-benchmark.zip (source). They were generated from Rugrat using the configuration files STEP-rugrat-config.zip. You can find the list of analyzed method here.
- KLEE benchmark: Due to the large file size (~50GB) of path conditions that continuously generated by KLEE in 30 seconds, it is impractical to put them online. You can reproduce them using this script with a successfully installed KLEE. Here is the list of GNU programs we have checked: Klee-benchmark. You can find part of the path condition file for program "rm" in all-queries.smt2.
- make a folder: mkdir sandbox
- download and extract following files into sandbox folder: STEP.jar, STEP-ext-lib.zip, STEP-Z3JNI.zip, STEP-script.zip, STEP-bin.zip, and all-queries.smt2. (The last two files are optional, download them to let you have something to test immediately.)
1. Run STEP on Rugrat benchmarks
./step <approach> <class> <method> <unroll> <timeout>
- <approach>: one of case-insensitive words: "Baseline", "Caching", "CachingOpt", "StackNonSSA" and "StackSSA".
- <class>: fully qualified name of the class under test.
- <method>: the name of entry method in the analyzed class. (NOTE: the method should only accept primitive inputs)
- <unroll>: maximum loop unrolling allowed in the analysis. Constant loops (a loop always terminates after constant number of iterations) take no effects of this option. (default 1)
- <timeout>: set up timeout. (second. default 0)
Depending on the size of analyzed methods, the heap size and stack size should be sufficiently set. With our experience, 8G memory and 50m stack is enough for Rugrat benchmarks.
For example, with following command "./step StackSSA rugrat.bench1.linear.fivek.exp1.FiveKLOCStart entryMethod 3 60", STEP explored 207 paths and 102383 states in 60 seconds using 1210 MB memory. It also generates time breakdown file "<approach>_data.csv" and tests folder "unittests" in sandbox.
2. Run STEP on KLEE benchmarks
./step-pc <approach> <PCFile> <method>
- <approach>: one of case-insensitive words: "Baseline", "Caching", "CachingOpt", "StackNonSSA".
- <PCFile>: the file "all-queries.smt2" generated from KLEE.
- <method>: the GNU program corresponding to the <PCFile>. e.g. "rm" in the following example.
STEP will load the <PCFile> and construct decision graph after analyzing the constraints, then explore the graph in the way according to the <approach>. For example, with the following command "./step-pc Baseline all-queries.smt2 rm", STEP finds no valid paths, which is correct to the original constraints. STEP will generate time breakdown file "klee.csv" and tests file "klee-test" in sandbox folder.
3. Run STEP for Linearization and SSA transformation
./step-preprocessing <approach> <class> <method> <unroll>
After execution of STEP, you will find time breakdown file "linearization_data.csv" in sandbox folder.
We performed preprocessing evaluation on 60 subjects from unroll 1 to 30 times, without timeout. The experiment results is STEP-preprocessing-result.csv.