-
Notifications
You must be signed in to change notification settings - Fork 5
Home
-
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
andSpfCasesPass2Visitor
: 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.
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.