Redesigning Soot’s Data-Flow Analysis Framework for Abstract Interpretation

The goal of a program analysis framework is to decrease the effort required of a program analysis developer to implement a new analysis. The Soot Java optimization framework provides analysis developers with several types of abstract analyses, which depending on the developers’ needs, can be further extended. Unfortunately, the applicability of the available abstract analyses in Soot is limited to analyses with finite ascending chains abstract domains, which are sufficient for the majority of program optimization tasks. This limitation hinders the use of Soot for program verification that requires reasoning about a program’s semantic over infinite abstract domains, i.e., abstract interpretation.

In this work we re-design Soot’s forward flow analysis framework to provide basic support for abstract interpretation. To accomplish this goal, we first extend the definition of a data-flow analysis to include additional parameters required for efficient and precise computation of abstract interpretation analyses. Next, we re-factor the current Soot’s implementation of a data-flow analysis to represent the extended definition. Finally, we demonstrate the flexibility and the applicability of the refactored implementation by instantiating several essential data-flow analyses used in abstract interpretation research.