Home

Java Ranger Source Code Navigation

• Java Ranger (JR) avoids path explosion by summarizing fragment of code into a constraint that can be added on the path condition.

• The primary entry point to Java Ranger's instantiation is the VeritestingListener. It writes the region's outputs to local variables, fields, array entries, and the stack out. It also updates the path condition and advances SPF to the end of the region.

• Main JR transformations happen in FixedPointWrapper Class, which iterates through different transformations until a fixed point on the summary is reached. These transformations are implemented using the visitor pattern. They are implemented in the following classes inside the gov.nasa.jpf.symbc.veritesting package except for the first class:

  • gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.CreateStaticRegions: This is the class that, given a class' WALA IR representation, recovers the Java Ranger IR representation of the same static region. It essentially runs a topological sort on the CFG of the method.
  • SubstitutionVisitor: substitutes local variables in the region's JR IR representation with the actual values that the local variables have in the SPF context
  • FieldSSAVisitor: creates JR IR in Static Single Assignment (SSA) form for all field accesses in the region's JR IR representation. Field read operations with no prior write operations are substituted with the corresponding value in the field.
  • ArraySSAVisitor: creates JR IR in SSA form for all array accesses in the region's JR IR representation. Array read operations with no prior write operations to the same array entry are substitution with the corresponding value in the array entry.
  • SimplifyStmtVisitor: performs constant propagation, copy propagation, and if-then-else statement and expression simplification on the region's JR IR representation.
  • TypePropagationVisitor: performs type propagation across operators in the region's JR IR representation
  • ExpUniqueVisitor: performs alpha-renaming on all variables in the region's JR IR representation
  • SpfCasesPass1Visitor and SpfCasesPass2Visitor: identifies all exceptional statements in the region's JR IR representation and constructs conditions to explore each of the SPF cases using SPF, the baseline symbolic executor for Java Ranger
  • LinearizationTransformation: removes all if-then-else statements from the region's JR IR representation
  • AstToGreenVisitor: transforms the region's JR IR representation to a Green formula so that it can be written to the path condition

• JR also implements the single-path cases (called SPFCases in the implementation) through StaticChoiceGenerator, which allows JR to explore unsummarized behaviors of the region.

• JR has two instances of the region, a StaticRegion and a DynamicRegion. StaticRegion includes no runtime information and DynamicRegion is where instantiation-time information is found. Initially, JR creates the StaticRegion representing the fragment of the code that is about to be executed, this is done through the JITAnalysis. All Static Regions encounter are cached into VeritestingMain.veriRegions HashMap.

• JR then applies different transformations on it using the FixedPointWrapper, to turn the static region into a dynamic one, and finally to turn the dynamic region into a constraint.

• Finally, JR decides which parts have not completely been summarized and creates a choice for them using StaticBranchChoiceGenerator.

• For more information please refer to the Java documentation of JR found here: https://vaibhavbsharma.github.io/java-ranger/docs/index.html.

Adding new transformations to Java Ranger

When considering a new transformation to be added to Java Ranger, you should first ask yourself if this transformation needs to be done exactly once or multiple times as part of a fixed-point computation. If it is a former kind of transformation, then call it from VeritestingListener.runVeritesting. If it is the latter kind of transformation, then call it from FixedPointWrapper.executeFixedPointTransformations. In either case, you will want to add it to the gov.nasa.jpf.symbc.veritesting.ast.transformations package. If the transformation is a static one (changes only the static representation of a region in JR IR), you will want to ensure you call it inside the StaticRegion constructor.

One important point to note for all JR transformations is that every region summary (represented as a Stmt inside StaticRegion or DynamicRegion) is immutable. Please try to maintain this design in new transformations because it helps examine the effect of each transformation on a region summary.

Understanding Java Ranger's modes

Java Ranger can be run in 5 different modes as set up the veritestingMode. 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.