- 85 views
- 141 downloads
Precise Data-flow Summaries with Synchronized Pushdown Systems
-
- Author / Creator
- Seekatz, David
-
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.
-
- Subjects / Keywords
-
- Graduation date
- Fall 2022
-
- Type of Item
- Thesis
-
- Degree
- Master of Science
-
- License
- This thesis is made available by the University of Alberta Library with permission of the copyright owner solely for non-commercial purposes. This thesis, or any portion thereof, may not otherwise be copied or reproduced without the written consent of the copyright owner, except to the extent permitted by Canadian copyright law.