Concolic Walk Heuristic for Solving Complex Arithmetic Path Conditions

This repository contains a modified version of the Symbolic PathFinder symbolic execution engine for Java. The modified version implements the heuristic described in the paper Solving Complex Path Conditions through Heuristic Search on Induced Polytopes by Peter Dinges and Gul Agha, which was presented at the FSE conference 2014. The repository furthermore contains the scripts for running experiments, as well as the data collected during the evaluation of the heuristic.

Abstract

Test input generators using symbolic and concolic execution must solve path conditions to systematically explore a program and generate high coverage tests. However, programs may contain complex arithmetic path conditions, which are undecidable in general. Existing test generators either simplify such constraints with concrete values to make them decidable, or rely on strong but incomplete constraint solvers. Unfortunately, simplification yields coarse approximations whose solutions rarely satisfy the original constraint; and constraint solvers cannot handle calls to native library methods. We show how a simple combination of linear constraint solving and heuristic search can overcome these limitations. On a corpus of 11 programs, our Concolic Walk algorithm generates tests with two- to three-times higher coverage than simplification-based tools while being up to five-times as efficient. Furthermore, our algorithm improves the coverage of two state-of-the-art test generators by 21% and 32%. Other concolic and symbolic testing tools could integrate our algorithm to solve complex path conditions without having to sacrifice any of their own capabilities, leading to higher overall coverage.

Overview

The implementation of the Concolic Walk (CW) algorithm in this repository is an extension of Symbolic PathFinder (SPF), which is a symbolic execution engine built on top of the Java PathFinder (JPF) verification framework. The extension works with existing SPF test-drivers; the only change required is setting a configuration flag to enable the extension.

The evaluation scripts measure how effective and efficient the CW algorithm and competing approaches are in solving path conditions with non-linear arithmetic constraints. To make numbers comparable, the effectiveness is measured as the coverage of generated test cases on a focused program corpus. The corpus consists of programs whose path conditions contain mostly non-linear constraints.

Directory Structure

• The tools/jpf/jpf-symbc/ directory contains the modified version of SPF (rev 2277b4d52b99) that includes the Concolic Walk implementation. All relevant classes can be found in the gov.nasa.jpf.symbc.concolic.walk package. The ConcolicWalkSolver class implements the actual algorithm; reading should start there.
• The tools/ directory furthermore contains the test generators competing with the CW implementation, as well as the programs used to measure the coverage of the generated tests. Because most of them are third-party tools, they have to be installed first (see the instructions below). For convenience, the snapshots/ directory contains archives of most of the required programs.
• The experiments/ directory contains the evaluation scripts, the corpus of target programs, and archives with the data used in the evaluation section of the paper.
  • The experiments/build.xml Ant build file manages the evaluation with the help of sub-build files and shell scripts.
  • The src/programs/ sub-directory of experiments/ contains the corpus of target programs, both in the original Java version, and in the auto-converted C# version (see tools/sharpen/README.md).
  • The src/drivers/ sub-directory contains the drivers and configuration files required by the test generators participating in the evaluation. However, since [Pex][pex] requires a Windows environment and is therefore hard to integrate directly into the evaluation setup, it has been executed manually and the resulting output has been stored in the res/ sub-directory. The src/drivers/pex/make-pex-test.py script converts the output into JUnit tests for the target programs.
  • Compiled programs and execution traces are written to the build/ sub-directory.
  • Generated test cases are stored in the gen/ sub-directory because they constitute the raw data and must be preserved.
  • Coverage reports generated by JaCoCo are stored in the coverage/ sub-directory.

Setup

Using the Concolic Walk version of Symbolic PathFinder (SPF) requires a Java Development Kit (JDK) supporting at least Java 1.6. Oracle's JDK 6u31 is known to work. The evaluation scripts assume a Linux environment that provides bash, m4, (GNU) sed, and Python 2.7 or later.

In the instructions given below, a leading dollar sign ($) symbolizes the shell prompt.

Installing the Java PathFinder Core

Because SPF itself is an extension of Java PathFinder (JPF), it requires a working installation of the JPF Core. The following steps summarize the installation; see the installation documentation on the JPF homepage for detailed instructions.

• Inflate the JPF Core snapshot.

  $ unzip snapshots/jpf-core-archived_from_5e5512919713.zip -d tools/jpf
  

• Tell JPF where its components are located by creating (or editing) the ~/.jpf/site.properties file. The file should contain the following lines, where ${user.home]/CONCOLIC_WALK_PROJECT/ should be replaced by the actual path to the root of this repository:

  jpf.home = ${user.home}/CONCOLIC_WALK_PROJECT_DIR/tools/jpf
  jpf-core = ${jpf.home}/jpf-core
  extensions=${jpf-core}
  

• Build and test the JPF Core module by executing bin/ant clean test in the tools/jpf/jpf-core/ directory. The process should end with a BUILD SUCCESSFUL message.

Building Symbolic PathFinder with Concolic Walk Support

• Add the following line to the site.properties file:

  jpf-symbc = ${jpf.home}/jpf-symbc
  extensions+=,${jpf-symbc}
  

• Build the Symbolic PathFinder module for JPF by executing bin/ant clean test in the tools/jpf/jpf-symbc/ directory. The process should end with a BUILD SUCCESSFUL message.

Installing Tools for Running Experiments

• Unpack the snapshots of the tools required for running experiments (JUnit, and JaCoCo) into the tools/ directory. For example, execute the following commands in the project root directory:

  $ unzip snapshots/junit-4.11.zip -d tools/
  $ unzip snapshots/jacoco-0.6.5.20131211-0329.zip -d tools/
  

• Install the competing test generators (jCUTE and Randoop) by unpacking their snapshots into the tools/ directory:

  $ unzip snapshots/jcute-packaged_from_3b2105b34a.zip -d tools/
  $ unzip snapshots/randoop-1.3.3.zip -d tools/
  

  Because jCUTE calls methods in native libraries, the snapshot version may not work on your system. Please see the jCUTE documentation for instructions on how to recompile these libraries.

If you decide to use different versions of the tools, adjust the paths and JAR names in the experiments/build.xml file accordingly.

Usage

Symbolic PathFinder with Concolic Walk Support

Given a .jpf configuration file for running SPF on a target program, the Concolic Walk heuristic can be enabled by adding the lines

symbolic.concolic=true
symbolic.heuristic_walk=true

to the file. More information about configuration files can be found in the SPF documentation. Examples are available in the SPF distribution (in the src/examples/ directory; in particular, src/examples/concolic/), and in the experiments/src/drivers/jpf/ directory. To run the classic DART example included in the SPF distribution, execute bin/jpf src/examples/concolic/DART.jpf in the tools/jpf/jpf-symbc/ directory. Modify the file as described above to enable the CW heuristic.

A set of additional configuration keys allows setting the parameters of the CW heuristic:

• symbolic.heuristic_walk.iterations = POSITIVE_INT (default: 150). Number of algorithm iterations added for each constraint in the path condition. The paper speaks of steps instead of iterations and denotes this constant as I.
• symbolic.heuristic_walk.neighbors = POSITIVE_INT (default: 10). Number of random neighbors to generate per iteration. The paper denotes this constant as R.
• symbolic.heuristic_walk.tabu_multiplier = NON_NEGATIVE_FLOAT (default: 0.5). Multiplier for computing how many iterations a variable is tabu if changing it failed to yield a better point. The paper uses this constant and the tabu_min value to compute the number of tabu iterations T.
• symbolic.heuristic_walk.tabu_min = NON_NEGATIVE_INT (default: 3). Minimum number of iterations that a variable is tabu if changing it failed to yield a better point. See the tabu_multiplier key above.
• symbolic.heuristic_walk.bisect = BOOLEAN (default: true). Toggle estimating additional neighbors that should satisfy one of the constraints violated by the current variable if the constraint was linear. See the discussion of Finding Neighbors in section 3.3 of the paper.

Generating Unit Tests from SPF Output

The experiments/src/drivers/filter-jpf-tests.sh script converts the Method Summaries section from SPF's output into JUnit tests. The script uses simple string-matching and replacement, which results in at least two limitations:

• The script only works with driver methods that accept primitive inputs; driver methods with object arguments are unsupported.
• The script cannot detect cases in which SPF produces faulty summaries, for example ones that differ from the driver method's signature. In these cases, the resulting test class must be cleaned up before it will compile. See the disableNonCompilingTests() function in the experiments/run-experiments.sh script for a method of automating this task.

Running a Single Experiment

The Ant build file experiments/build.xml controls how a single experiment for evaluating the Concolic Walk heuristic is run. A full experiment collects the coverage of all unit tests that each test generation tool generates for every target program.

To run one full experiment, invoke Ant on the rebuild target:

$ ant rebuild

or, falling back on JPF's Ant installation if Ant is not installed,

$ ../tools/jpf/jpf-core/bin/ant rebuild

The rebuild target is a short-hand for

$ ant clean-all compile-programs generate-tests run-tests report

It is also possible to collect the coverage of a specific test generation tool by using tool-specific sub-targets of generate-tests and run-tests such as generate-tests-jcute. For historic reasons, the tool name of SPF with the CW heuristic is jpf-gradient.

Note that the run-tests-* targets do not depend on the generate-tests-* targets to allow for some fiddling with the generated tests before running them. This allows, for example, to fix the non-compiling tests generated by the filter-jpf-tests.sh (see above).

Running a Series of Experiments

The experiments/run-experiments.sh script runs a series of full experiments and archives the results.

License

The implementation of the Concolic Walk algorithm and its unit tests, the BruteFuzz tool, and the evaluation scripts in this repository are available under the MIT license. Copyright (c) 2014 the University of Illinois Board of Trustees. All Rights Reserved.

The remaining components (JaCoCo, Java PathFinder, jCUTE, JUnit, Randoop, Sharpen, and Symbolic PathFinder), are works of their respective authors and their included LICENSE files apply.

Acknowledgments

This work was made possible in part by sponsorship from the Army Research Office under award W911NF-09-1-0273, as well as a fellowship from the Graduate College of the University of Illinois at Urbana-Champaign.