STEP: Input-generation tool for Java

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.

Publications

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

People

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.

Install

It is easy to set up STEP for command line usage.

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.)

Or you can automatically setup STEP using this script: install-STEP.sh

For expert usage of STEP, please check the STEP source.

Run

NOTE: The released binary version of STEP supports only 64-bit Linux. If you want to run STEP using other (pipeline-based) solvers, please check the configuration file in STEP source. If you are interested, please contact us. We are pleased to give helps.

1. Run STEP on Rugrat benchmarks

Assume you already downloaded the rugrat benchmarks STEP-bin.zip and STEP utility script STEP-script.zip, and extract them into the sandbox folder. The script "step" already linked Z3 library and configured Java options. The usage is:

./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

Assume you already downloaded STEP utility script STEP-script.zip and toy example all-queries.smt2, and extract them into the sandbox folder. The usage is:

./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

Assume you already downloaded the rugrat benchmarks STEP-bin.zip and STEP utility script STEP-script.zip, and extract them into the sandbox folder. The usage is:

./step-preprocessing <approach> <class> <method> <unroll>

After execution of STEP, you will find time breakdown file "linearization_data.csv" in sandbox folder.

Experiment

5 approaches, Baseline, Caching, CachingOpt, StackNonSSA and StackSSA have been executed on 300 subjects with timeout 10 min. The result is STEP-rugrat-result.csv.

4 approaches, Baseline, Caching, CachingOpt and StackNonSSA have been executed on KLEE benchmark Coreutils-6.11, the experiment results is STEP-klee-result.csv.

We performed preprocessing evaluation on 60 subjects from unroll 1 to 30 times, without timeout. The experiment results is STEP-preprocessing-result.csv.