1 Verification Approach

Symbolic Pathfinder (SPF) is a program analysis tool for Java bytecode; the tool is based on symbolic execution. In this approach, programs are executed on symbolic inputs representing multiple concrete inputs. Values of variables are represented as numeric constraints, generated from the analysis of the code structure, i.e. conditionals and other statements in the program. These constraints are then solved using different constraint solvers (both off-the-shelf and built-in-house) to generate test inputs that are guaranteed to reach those parts of the code.

The current implementation handles the following:

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

  • Input data structures, using lazy initialization [5]

  • Preconditions [5]

  • Multi-threading (via Java PathFinder exploration)

  • Mixed symbolic/concrete execution mode [9]

  • Symbolic arrays [3]

  • Inputs of type String – work in progress [1].

SPF can also be used for probabilistic analysis by leveraging model counting over symbolic constraints [2, 4], and for automated program repair [6, 7]. Most recent work explores combinations of SPF with AFL-style fuzzing [8] and further differential analysis for regression problems.

2 Software Architecture

SPF is described in detail in a journal article [10] (however, as it is an active project, it is being updated with new features all the time). We depict the current tool architecture in Fig. 1. The input to the tool is a Java bytecode program and a configuration file that specifies different options for analysis (as discussed below). The output is a set of test sequences that execute different paths through the code. The output also lists the errors that were found (e.g. exceptions, assert violations) together with various statistics about the analysis.

Fig. 1.
figure 1

Symbolic PathFinder overview.

Full size image

Symbolic execution is implemented by a “non-standard” interpretation of bytecodes. The symbolic information is propagated via attributes associated with program variables, operands, etc. The analysis can start from any point in the program and it can perform mixed concrete/symbolic execution. SPF relies on jpf-core’s search engine to explore different paths through the code. The default search strategy is depth-first search. State matching (as implemented in jpf-core) is usually turned off during symbolic execution.

SPF uses several constraint solvers and decision procedures, most notably Z3 and Z3bitvector, which are available from https://github.com/Z3Prover/z3. SPF implements both incremental and non-incremental constraint solving.

3 Discussion of Strengths and Weaknesses of the Approach

The competition results are provided on the SV-COMP website. The results indicate that SPF outperforms the other tools in terms of correct answers (337), cpu time (1300 s) and energy (13000 J). However, SPF also reported 6 incorrect results, which penalized the overall final score. While the incorrect true results are due to the bounded nature of the analysis, the incorrect false results are due mainly to the string analysis, with the exception of one result which was due to an error in jpf-core which has since been corrected. The string solver was incorrectly specified and tested (i.e. the path to the string solver is hard coded in the current implementation but we provided no string solver for the competition).

In the future we plan to test SPF on the competition string examples using either ABC or Z3str and to robustify the implementation. We also plan to contribute to the competition by adding more interesting benchmarks, particularly related to input data structures.

4 Tool Setup and Configuration

Symbolic PathFinder is available at https://github.com/SymbolicPathFinder/jpf-symbc. It requires Java 8 and Java PathFinder, which available at https://github.com/javapathfinder/jpf-core.

For this competition we used the version with the timestamp Mon Nov 19 09:51:16 CET 2018, which refers to the date when we pulled the artifacts from the GitHub repository and generated the jpf-symbc jar archive.

To run SPF, the user needs to download Symbolic PathFinder and Java PathFinder (default branches) and create a file .jpf/site.properties in the home directory. The site.properties file should contain the following lines (the users should modify to point to the location of jpf-core and jpf-symbc on their computer):

figure a

The user then creates a *.jpf configuration file (described in detail below). For the competition we modified the SPF tool to handle the non-deterministic constructs required by the competition.

4.1 Example Configuration

We give here an example configuration that can be used to run the SPF tool; this is the default configuration, that we used in the competition. The explanation for the different options is given in parenthesis.

  • (specify the target application)

  • (path to your class example)

  • (path to the source of your example)

  • (specify the decision procedure)

  • (specify the bitvector length)

  • (specify various min max values)

  • (print debug information)

  • (specify search limit)

  • (handling symbolic arrays)

  • (specify string analysis)

  • (specify string solver).

SPF also has the option of running the constraint solving incrementally. Note however that we did not use the string solving and the incremental solving options in the competition as we did not have enough time to prepare and test those features, as we were entered late in the competition.

5 Software Project and Contributors

Information about the project and contributors can be found at the project webpage: https://github.com/SymbolicPathFinder/jpf-symbc. For more information please contact the authors of this paper.