concolic-walk

KO | EN

gitlite — search

#javascript #react #golang #deep-learning #docker #macos #awesome #cli #kubernetes #awesome-list #security #openai #mcp #ios

(★ 13)

Implementation and evaluation data of the Concolic Walk heuristic for solving complex arithmetic path conditions.

concolic-walk Latest Version Download

Download Latest Version (.zip)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

Concolic Walk Heuristic for Solving Complex Arithmetic Path Conditions
=====================================================================

This repository contains a modified version of the
[Symbolic PathFinder][jpf-symbc] 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][paper-fse14]
by Peter Dinges and Gul Agha, which was presented at the
[FSE conference 2014][fse14].  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][jpf-symbc] (SPF),
which is a symbolic execution engine built on top of the
[Java PathFinder][jpf-core] (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][jpf-symbc-base]) 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][paper-fse14].
  - The `experiments/build.xml` [Ant][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][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][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][python] 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][jpf-install] 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][junit], and [JaCoCo][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][jcute] and
  [Randoop][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][jcute-doc] 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][jpf-symbc-doc].  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][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][license-mit].  Copyright (c) 2014
the [University of Illinois][uiuc] Board of Trustees.  All Rights
Reserved.

The remaining components ([JaCoCo][jacoco],
[Java PathFinder][jpf-core], [jCUTE][jcute], [JUnit][junit],
[Randoop][randoop], [Sharpen][sharpen], and
[Symbolic PathFinder][jpf-symbc]), 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][uiuc].

[ant]: https://ant.apache.org/ "Apache Ant: Build Tool"
[fse14]: http://fse22.gatech.edu/ "22nd ACM SIGSOFT International Symposium on the Foundations of Software Engineering"
[jacoco]: http://eclemma.org/jacoco/ "JaCoCo Java Code Coverage Library"
[jcute]: http://osl.cs.illinois.edu/software/jcute/ "Java Concolic Unit Testing Engine"
[jcute-doc]: https://github.com/osl/jcute/blob/master/README.md "jCUTE README file"
[jpf-core]: http://babelfish.arc.nasa.gov/trac/jpf "Java PathFinder Verification Tool"
[jpf-install]: http://babelfish.arc.nasa.gov/trac/jpf/wiki/install/start "JPF Install Guide"
[jpf-symbc]: http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc "Symbolic PathFinder Symbolic Execution Engine for Java"
[jpf-symbc-base]: http://babelfish.arc.nasa.gov/hg/jpf/jpf-symbc/rev/2277b4d52b99 "JPF-Symbc v6, rev 2277b4d52b99"
[jpf-symbc-doc]: http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc/doc "Symbolic PathFinder Documentation"
[junit]: http://junit.org/ "JUnit: Programmer-Oriented Testing Framework for Java"
[license-mit]: http://opensource.org/licenses/MIT "MIT Open Source License"
[paper-fse14]: http://osl.cs.illinois.edu/
[python]: http://python.org/ "Homepage of the Python Programming Language"
[randoop]: https://code.google.com/p/randoop/ "Randoop Unit Test Generator"
[sharpen]: http://community.versant.com/Projects/html/projectspaces/db4o_product_design/sharpen.html "Sharpen Eclipse Plugin for Multi-Platform Development from One Codebase"
[uiuc]: http://www.illinois.edu "Homepage of the University of Illinois"

concolic-walk

concolic-walk Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

concolic-walk

concolic-walk Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

Download README