Precise Data-flow Summaries with Synchronized Pushdown Systems

Abstract: Static data-flow analysis is a method of reasoning about program values without executing the program. A data-flow analysis that is context-sensitive, field-sensitive, flow-sensitive, and alias-aware can precisely and soundly answer points-to queries (e.g. what heap objects can variable v reference at line n?). For large modern software systems, answering these queries is time- and resource-intensive due to the size and complexity of library code. If an application is heavily library-dependent, a typical data-flow analysis spends the majority of its computation time analyzing library code. However, library code does not change each time an application is compiled, so library data-flow can be summarized and re-used to efficiently analyze application code. This work details a novel method of computing precise data-flow summaries for libraries using Synchronized Pushdown Systems (SPDS) and heap graphs, which we implement in a tool called BluJ. To construct the summaries, BluJ instantiates an SPDS instance at every point that an object may enter the library. BluJ then computes forward data-flow reachability information for each SPDS instance and uses a heap graph to model the heap relationships between the respective objects tracked by each SPDS instance. The resulting data-flow summaries take into account any aliasing that occurs in the library, they are context- and field-sensitive, and they are flow-sensitive with the exception of a few rare cases. The generated summaries are bi-directional and can be consumed by either a forward or backward client analysis. We implement our summaries within the Boomerang points-to analysis framework and compare the relative performance and precision of Boomerang with and without our generated summaries.