-
Notifications
You must be signed in to change notification settings - Fork 5
Home
-
Java Ranger avoids path explosion by summarizing fragment of code into a constraint that can be added on the path condition.
-
VeritestingListner Class is the entry point of Java Ranger. Through this listener JR intercept symbolic branch instructions and attempt to path-merge them by summarizing them as a constraint to be added on the path condition.
-
Main JR transformations happen in FixedPointWrapper Classs, which iterates different transformations until a fixed point is reached.
-
JR also implements the single-path cases (called in the implementation SPFCases) through StaticChoiceGenerator, which allows JR to explore unsummarized behaviors of the region.
-
JR has two instances of the region, a StaticRegion, and a DynamicRegion, where the static one has no runtime information included, whereas the dynamic one is where instantiation time information is found. Initially, JR creates the Static Region 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.