Skip to content

Home

Jump to bottom
Vaibhav Sharma edited this page Jun 25, 2020 · 25 revisions

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 VeritestingListener class is the primarty entry point to understanding Java Ranger's implementation. Through this listener, JR intercepts symbolic branch instructions and attempts to merge paths by summarizing them as a constraint to be added on the path condition.

  • 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
    • VeritestingListener.setupSPF: 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.

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

Clone this wiki locally