SynergiSE: Using Test Ranges to Improve Symbolic Execution

SynergiSE is a novel two-fold approach that (1) it integrates distributed analysis and constraint re-use to enhance symbolic execution using feasible ranges, which allow sharing of constraint solving results among different workers without communicating or sharing potentially large constraint databases (as required traditionally); (2) it integrates complementary techniques for test input generation, e.g., search-based generation and symbolic execution, for creating higher quality tests using unexplored ranges, which allows symbolic execution to re-use tests created by another technique for effective distribution of exploration of previously unexplored paths.

SynergiSE builds on previous work on ranged symbolic execution, which introduced the idea of bounding a run of symbolic execution using a range defined by a pair of two ordered tests (T1, T2) such that symbolic execution is restricted to program paths that are lexicographically between the path executed by T1 and the path executed by T2. The key novelty of SynergiSE is to introduce two special kinds of ranges, i.e., feasible ranges and unexplored ranges for laying the foundation of a two-fold synergistic approach.

Publications

Using Test Ranges to Improve Symbolic Execution

By Rui Qiu, Sarfraz Khurshid, Corina S. Pasareanu, Junye Wen, and Guowei Yang
10th NASA Formal Methods Symposium
(NFM 2018), Newport News, VA, USA, April 2018.

A Synergistic Approach for Distributed Symbolic Execution Using Test Ranges

By Rui Qiu, Sarfraz Khurshid, Corina S. Pasareanu, and Guowei Yang
39th International Conference on Software Engineering, Poster
(ICSE 2017), Buenos Aires, Argentina, May 2017.

Download

Run

To run SynergiSE, simply use the provided script run.sh. The script takes multiple arguments. The first argument is the target Java class file for executing. The second argument is the target subject. The third argument is the number of ranges generated. The fourth argument is the initial search depth for the target subject. One use case for SynergiSE is that we can run distributed symbolic execution for a subject WBS (initial depth 10) using 6 feasible ranges will be:

cd ~/synergise; ./run.sh DSE WBS 6 10 

Refer the script run.sh for details on arguments and settings. You may need to change the executed command (variable COMMAND) based on your distributed setting (e.g., using command mpirun instead of ibrun).

A more detailed usage of mpj-express can be found here. A full reference of SynergiSE will be released soon.

Example Programs

The following five example programs are used in the experiments we conducted to evaluate our proposed approach. The corresponding mutated methods or statements (if used) are comment out in the source code.

1. JDK1.5 Sorting Algorithms and RedBlack Tree Data Structure

download

We evaluated SynergiSE on three commonly used sorting algorithms and one data structure from Sun's JDK 1.5. These algorithms are MergeSort, QuickSort, and HeapInsert. The data structure is Red-Black Tree. They were used as benchmarks in previous symbolic execution studies. For the sorting algorithms, we use an array of 6 symbolic inputs. Red-Black Tree contains 7 symbolic elements.

2. WBS

download

Wheel Brake System (WBS) is a synchronous reactive component from the automotive domain. This method determines how much braking pressure to apply based on the environment. The Java model is based on a Simulink model derived from the WBS case example found in ARP 4761. The Simulink model was translated to C using tools developed at Rockwell Collins and manually translated to Java. It consists of one class and 231 lines of code. The version of the program we used performs three iterations of analysis.

3. TCAS

download

Traffic Anti-Collision Avoidance System (TCAS) is a system to avoid air collisions. Its code in C together with 41 mutants are available at SIR repository. We manually converted the code to Java. The Java version has 143 lines of code.

4. Rational

download

Program Rational is a case study for computing greatest common divisor and its related operations on rational numbers. It contains 96 lines of code in one class.

5. MerArbiter

download

MerArbiter models a component of the flight software for NASA JPL’s Mars Exploration Rovers (MER). The analyzed software consists of a Resource Arbiter and several user components. Each user serves one specific application, such as imaging, controlling the robot arm, communicating with earth, and driving. The arbiter module moderates access to several shared resources. It prevents potential conflicts between resource requests coming from different users and it enforces priorities. For example, it does not make sense to start a communication session with Earth while the rover is driving.

MerArbiter has been modeled in Simulink/Stateflow and it was automatically translated into Java using the Polyglot framework. The configuration for our analysis involved two users and five resources. The example has 268 classes, 553 methods, 4697 lines of code (including the Java Polyglot execution framework).

6. Dijkstra

download

Program Dijkstra is a benchmark developed by Jacob Burnim from University of California, Berkeley. It is an algorithm for finding the shortest paths between nodes in a graph, which may represent road networks for instance. It contains 109 lines of code in one class and 25 symbolic variables.

7. TSP

download

Program TSP is a benchmark solution for Traveling Salesman Problem. This subject is developed by Sudeep Juvekar and Jacob Burnim from California, Berkeley. It contains 124 lines of code in one class and 25 symbolic variables.

Raw Data

Green Databases and Feasible Ranges

download

For WBS and JDK1.5 Sorting Algorithms and RedBlack Tree, we evaluated the size of Green databases generated by symbolic execution and their corresponding feasible ranges.

Green uses a Redis in-memory database (*.rdb) to store all path constraints of symbolic execution into a key-value store, in which keys are path constraint strings and values are boolean results of satisfiability (either satisfiable or unsatisfiable). To inspect a Green database, you need to install Redis. A complete reference on how to use Redis to load an existing database can be found here.

We also compared the size of the compressed Green databases and the size of the compressed feasible ranges. To obtain a zipped file, please use the following sample command:

zip wbsGreen.rdb zipDB.zip

Test Inputs Generated by Complementary Test Generation Tools

download

We run two complementary test generation tools Randoop and EvoSuite to generate an initial test inputs for SynergiSE. Then SynergiSE generates a set of unexplored ranges to speed up symbolic execution.

We provide these generated tests as part of the raw data of our experiments. All the tests are organized into folders named by the test subject. Each subject folder contains several sub-folders named as "t*" representing the execution time of the complementary tool.