wiki:projects/jpf-symbc/doc

Symbolic PathFinder -- Tool Documentation

Symbolic PathFinder (SPF) performs symbolic execution of Java bytecode programs. One of the main applications is automated generation of test inputs that obtain high coverage (e.g. path coverage) of code. Other applications include error detection in concurrent programs that take inputs from unbounded domains and lightweight theorem proving.

SPF combines symbolic execution with model checking and constraint solving for test input generation. In this tool, programs are executed on symbolic inputs that cover all possible concrete inputs. Values of variables are represented as numeric expressions and constraints, generated from analysis of the code structure. These constraints are then solved to generate test inputs guaranteed to reach that part of code.

For example, in the figure, the path condition (PC) is initially true. If the program takes the if statement's then branch, the path condition will be X<Y. If the program takes the if statement's else branch, the path condition will be X≥Y.

Implementation

Symbolic execution is implemented by a "non-standard" interpretation of bytecodes. The symbolic information is propagated via attributes associated with program variables, operands, etc. Symbolic execution can start from any point in the program and it can perform mixed concrete/symbolic execution. State matching is usually turned off during symbolic execution.

The current implementation handles the following:

  • Inputs of type boolean, int, long, float, double

  • Preconditions
  • Multi-threading
  • Mixed symbolic/concrete execution mode
  • Inputs of type String -- work in progress

SPF uses the following constraint solvers/decision procedures:

  • Choco (pure Java) for linear/non-linear integer/real constraints.
  • IASolver (pure Java) the Brandeis Interval Arithmetic Constraint Solver.
  • CVC3 for real and integer linear arithmetic and also for bit vector operations.

Instructions

To run SPF, the user needs to download jpf-core and jpf-symbc (default branches, or v6 branches for both) and set-up .jpf/site.properties (see main documentation). Make sure that the site.properties file contains the following lines:

# modify to point to the location of jpf-symbc on your computer

jpf-symbc = ${user.home}/workspace/jpf-symbc

extensions+=,${jpf-symbc}

The user then creates a *.jpf configuration file which specifies, among other things, which method to execute symbolically and which method arguments are symbolic/concrete. Globals (i.e. fields) can also be specified to be symbolic, via special annotations; annotations are also used to specify preconditions (see src/tests/ExSymExePrecondAndMath.java).

  • Here is an example of a JPF run configuration (Example.jpf). It enables symbolic execution of method "test" in main class Example.java, where first argument is symbolic, and second argument is concrete.

Options

We explain now in more detail the various options that can be used in a .jpf configuration file. Below, the fully qualified name specifies the package, class, inner class etc., e.g. "package_name.class_name$inner_class_name.method_name"

target=<your package>.Example

classpath=<your class path>

symbolic.method= <fully qualified name>.test(sym#con)

# peer packages used by SPF; not mandatory: already set-up in jpf-symbc

peer_packages= gov.nasa.jpf.symbc,${peer_packages}

# replace standard execution with symbolic execution; not mandatory: already set-up in jpf-symbc

vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory

# listener to print information (PCs, test cases) about symbolic run

listener = gov.nasa.jpf.symbc.SymbolicListener

# listener to print test sequences

listener = gov.nasa.jpf.symbc.sequences.SymbolicSequenceListener

# The following JPF options are usually used for SPF as well:

# no state matching; not mandatory: already set-up in jpf-symbc

vm.storage.class=nil

# instruct jpf to not stop at first error

search.multiple_errors=true

# specify the search strategy (default is DFS)

search.class = .search.heuristic.BFSHeuristic

# limit the search depth (number of choices along the path)

search.depth_limit = 10

  • You can specify multiple methods to be executed symbolically as follows:

symbolic.method=<list of methods to be executed symbolically separated by ",">

  • You can pick which decision procedure to choose (if unspecified, choco is used as default):

symbolic.dp=choco

symbolic.dp=iasolver

symbolic.dp=cvc3

symbolic.dp=cvc3bitvec

symbolic.dp=no_solver (explores an over-approximation of program paths; similar to a CFG traversal)

  • A new option was added to implement lazy initialization (see [TACAS'03] paper)

symbolic.lazy=on

(default is off) -- for now it is incompatible with Strings

  • New options have been added, to specify min/max values for symbolic variables and also to give the default for don't care values.

symbolic.min_int=-100

symbolic.max_int=100

symbolic.min_double=-1000.0

symbolic.max_double=1000.0

symbolic.undefined=0

  • An option to increase the time limit until which choco tries to solve a particular constraint

choco.time_bound=30000 # default value is 30000

  • Print debug information

symbolic.debug=on

See also examples in src/tests and src/examples. If you run SPF outside eclipse, you should compile your class under test with debug option on ("javac -g").

Last modified 16 months ago Last modified on 09/03/2013 02:32:11 PM

Attachments (3)

Download all attachments as: .zip