During summer of 2017, I worked on a Google Summer of Code project for implementing a technique called Veritesting in Symbolic PathFinder. For the static analysis part of veritesting, I created a Soot extension which automatically generates the main listener function of Symbolic PathFinder.
Veritesting requires static symbolic execution to be performed, when possible, to exponentially reduce the number of execution paths required for complete path exploration in symbolic execution. To integrate veritesting with Symbolic PathFinder, I created a Soot extension which needs to be run as a prior step to a symbolic execution with SPF. Running this step will produce a collection of executeInstruction functions that SPF can run. My veritesting implementation currently causes symbolic execution of the following code to have one execution path instead of 4, when x and y are marked as symbolic integers.
if (x <= 800 ) a = -1;
else a = 1;
if (y <= 1200 ) b = -1;
else b = 1;This integration also required SPF to have complex constraints involving multiple comparison operators. I implemented these changes to allow SPF to solve such complex constraints (see ComplexNonLinearIntegerConstraints.java). To solve such constraints, I implemented support for SPF to communicate these constraints with the Z3BitVector solver.
The project was maintained here. The project is in usable state. The complete example for which my veritesting implementation works is here. My Soot extension can be found in jpf-symbc/src/examples/MyMain.java and my auto-generated listener functions can be found in jpf-symbc/src/main/gov/nasa/jpf/symbc/VeritestingListener.java.