Skip to content

Home

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

Understanding Java Ranger's source code

This wiki is a supplemental resource to understanding Java Ranger's source code. The primary resource to understanding all things Java Ranger is here: https://vaibhavbsharma.github.io/java-ranger/

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.

Most of Java Ranger's transformations happen in FixedPointWrapper, 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 StaticPCChoiceGenerator, 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.

Clone this wiki locally