Skip to content

Documentation

Jump to bottom
Corina Pasareanu edited this page Dec 1, 2018 · 19 revisions

Symbolic PathFinder Documentation (under construction)

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

  • Input data structures, polymorphism -- using [http://ti.arc.nasa.gov//m/profile/pcorina/papers/paper149.ps "lazy initialization"]

  • Preconditions

  • Multi-threading

  • Mixed symbolic/concrete execution mode

  • Symbolic arrays

  • Inputs of type String -- work in progress

SPF uses the following constraint solvers/decision procedures:

  • Z3, Z3bitvector (both incremental and not incremental)

  • [http://www.emn.fr/z-info/choco-solver/ Choco] (pure Java) for linear/non-linear integer/real constraints.

  • [http://www.cs.brandeis.edu/~tim/Applets/IAsolver.html IASolver] (pure Java) the Brandeis Interval Arithmetic Constraint Solver.

  • [http://cs.nyu.edu/acsys/cvc3/ 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) and create .jpf/site.properties in home directory (see also documentation for jpf-core). Make sure that the site.properties file contains the following lines:

  • modify to point to the location of jpf-core and jpf-symbc on your computer

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

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

extensions=${jpf-core},${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).

Example configuration

Here is an example configuration that can be used to run the SPF tool

target=test.Main

classpath=/.. path to your class example: test.Main.class

sourcepath=/.. path to the source of your example: test/Main.java

  • specify the decision procedure to use

symbolic.dp=z3bitvector

symbolic.bvlength=64

  • specify various min max values

symbolic.min_int=-100

symbolic.max_int=100

symbolic.min_double=-100.0

symbolic.max_double=100.0

  • print some debug information

symbolic.debug=true

  • specify some search limit

search.depth_limit=15

  • handling symbolic arrays

symbolic.lazy=on

symbolic.arrays=true

  • specify string analysis

symbolic.strings = true

symbolic.string_dp=ABC

or

symbolic.string_dp=z3str

symbolic.string_dp_timeout_ms=3000

Example configuration for incremental solving

symbolic.dp=z3bitvectorinc

or

symbolic.dp=z3inc

The following two options are mandatory:

symbolic.optimizechoices=false

listener = gov.nasa.jpf.symbc.numeric.solvers.IncrementalListener

Options (old)

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=.Example

classpath=

symbolic.method= .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

  • 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, z3 is used as default):

symbolic.dp=choco

symbolic.dp=iasolver

symbolic.dp=cvc3

symbolic.dp=cvc3bitvec

symbolic.dp=z3

symbolic.dp=z3bitvec

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)

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

Clone this wiki locally