From WalaWiki

Jump to: navigation, search

wala.core technical overview

WALA's demand-driven pointer analysis, exposed through the DemandRefinementPointsTo class, implements the analysis presented in the paper "Refinement-Based Context-Sensitive Points-To Analysis for Java" and in Manu Sridharan's dissertation.



There are several parameters that must be set during initialization of the DemandRefinementPointsTo object, documented below. Basic initialization code can be seen in the AbstractPtrTest.makeDemandPointerAnalysis() method in the trunk.tests.demandpa project.

Call Graph

The analysis requires a pre-computed call graph (though it can be configured to refine virtual call targets on-the-fly). Most testing has been done with a 0-CFA call graph (see UserGuide:PointerAnalysis), but more precise call graphs should work fine. Using a call graph built by rapid type analysis is not supported and may lead to unsoundness or crashes (see note in UserGuide:CallGraph).

Heap Model

The analysis also requires a HeapModel to determine how to abstract pointers and heap locations (see UserGuide:PointerAnalysis). The analysis has mostly been tested with a HeapModel obtained from calling Util.makeVanillaZeroOneCFABuilder(), but other heap models should work.

State Machine

The analysis can be extended to have more precision or to track other properties using a StateMachine. For example, context sensitivity is implemented through the use of a ContextSensitiveStateMachine. The DemandRefinementPointsTo constructor takes a StateMachineFactory as a parameter; the factory is used to create a new StateMachine object for each query and for each refinement pass. For context-insensitive analysis, pass in a DummyStateMachine.Factory object.

Refinement Policy

A RefinementPolicy dictates how the analysis handles field accesses and method calls, and also specifies the budgets for each refinement pass. By default, the analysis uses a SinglePassRefinementPolicy that leads to a single analysis pass with no field sensitivity or on-the-fly call graph refinement. Other useful refinement policies include the ManualRefinementPolicy, which refines for certain hand-specified fields (mostly java.util collections classes), and the TunedRefinementPolicy, which attempts to discover which fields and method calls are important to treat precisely.

Similar to state machines, the refinement policy is changed through setting a RefinementPolicyFactory with a call to DemandRefinementPointsTo.setRefinementPolicyFactory().

Running The Analysis

The most straightforward way to run the analysis is to call the getPointsTo() method that just takes a PointerKey as an argument. (The PointerKey should be obtained from the same HeapModel used to initialize the analysis.) If the analysis is able to compute a result in the budget specified by the RefinementPolicy, that result is returned; otherwise, the analysis returns null.

For more control over the analysis, call the getPointsTo() method that takes both a PointerKey and a Predicate as arguments. The Predicate specifies the condition that the result points-to set should ideally satisfy. (For example, if the points-to set is used for checking downcast safety, the predicate would check that no instance key in the set would cause a downcast failure.) The method returns both the points-to set (again possibly null) and a PointsToResult indicating whether the (1) predicate was satisfied, (2) no more refinement was possible, or (3) the analysis budget was exceeded.

Personal tools
project information