Java Ranger is a path-merging extension of Symbolic PathFinder (SPF). In this tool, we've extended the veritesting technique by Avgerinos et al. (see paper here) for symbolic execution of Java bytecode.
The setup of Java Ranger is very similar to the setup used by SPF. The only difference in setup is, since Java Ranger is simply an extension of SPF, the Java Ranger directory can be specified as a valid jpf-symbc extension of JPF. The example configuration required by Java Ranger is exactly the same as the configuration that is required by SPF with the following additions.
veritestingMode = <1-5>
veritestingMode specifies the path-merging features to be enabled with each higher number adding a new feature to the set of features enabled by the previous number. Setting veritestingMode to 1 runs vanilla SPF. Setting it to 2 enables path-merging for multi-path regions with no method calls and a single exit point. Setting it to 3 adds path-merging for multi-path regions that make method calls where the method can be summarized by Java Ranger. Setting it to 4 adds path-merging for multi-path regions with more than one exit point caused due to exceptional behavior and unsummarized method calls. Setting it to 5 adds path-merging for summarizing return instructions in multi-path regions by treating them as an additional exit point.
performanceMode = <true or false>
Setting performanceMode to true causes Java Ranger to minimize the number of solver calls to check the feasibility of the path condition when summarizing a multi-path region with multiple exit points.
TARGET_CLASSPATH_WALA=<classpath of target code>
Java Ranger needs this variable to be set up as environment variable. It is not part of the .jpf configuration file. This environment variable tells Java Ranger where it should be expecting to find code that needs to be statically summarized
More information on Java Ranger can be found in the following pages
- Understanding Java Ranger's source code
- Adding new transformations to Java Ranger
- Understanding Java Ranger's modes
Documentation for Java Ranger is available here: https://vaibhavbsharma.github.io/java-ranger/docs/index.html.
The following people have contributed to Java Ranger
- Soha Hussein
- Vaibhav Sharma
- Michael Whalen
- Stephen McCamant
- Willem Visser