Speeding Up Dataflow Analysis Using Flow-Insensitive Pointer Analysis
In recent years, static analysis has increasingly been applied to the problem of program verification. Systems for program verification typically use precise and expensive interprocedural dataflow algorithms that are difficult to scale to large programs. An attractive way to scale these analyses is to use a preprocessing step to reduce the number of dataflow facts propagated by the analysis and/or the number of statements to be processed, before the dataflow analysis is run. This paper describes an approach that achieves this effect. We first run a scalable, control-flow-insensitive pointer analysis to produce a conservative representation of value flow in the program. We query the value flow representation at the program points where a dataflow solution is required, in order to obtain a conservative over-approximation of the dataflow facts and the statements that must be processed by the analysis. We then run the dataflow analysis on this “slice” of the program.
We present experimental evidence in support of our approach by considering two client dataflow analyses for program verification: typestate analysis, and software model checking. We show that in both cases, our approach leads to dramatic speedups.
KeywordsWill Emit Large Program Device Driver Ground Term Program Point
Unable to display preview. Download preview PDF.
- [BR01a]Thomas Ball and Sriram K. Rajamani. Automatically validating temporal safety properties of interfaces. In Proceedings of SPIN’ 01, 8th Annual SPIN Workshop on Model Checking of Software, May 2001.Google Scholar
- [BR01b]Thomas Ball and Sriram K. Rajamani. Bebop: A path-sensitive interprocedural dataflow engine. In Proceedings of PASTE’ 01, ACM SIGPLANSIGSOFT Workshop on Program Analysis for Software Tools and Engineering, June 2001.Google Scholar
- [CFR+91]Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark N. Wegman, and F. Kenneth Zadeck. Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems, 13(4):451–490, October 1991.Google Scholar
- [CRL99]R. Chatterjee, B. Ryder, and W. Landi. Relevant context inference. In Proceedings of POPL’ 99, 26st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1999.Google Scholar
- [Das00]Manuvir Das. Unification-based pointer analysis with directional assignments. In Proceedings of the ACM SIGPLAN’ 00 Conference on Programming Language Design and Implementation (PLDI-00), 2000.Google Scholar
- [DGS95]Evelyn Duesterwald, Rajiv Gupta, and Mary Lou Soffa. Demand-driven computation of interprocedural data flow. In Symposium on Principles of Programming Languages, pages 37–48, 1995.Google Scholar
- [DLFR01]Manuvir Das, Ben Liblit, Manuel Fahndrich, and Jakob Rehof. Estimating the impact of scalable pointer analysis on optimization. In Proceedings of the 8th International Symposium on Static Analysis, 2001.Google Scholar
- [DLS02]M. Das, S. Lerner, and M. Seigle. ESP: Path sensitive program verification in polynomial time. In Proceedings of the ACM SIGPLAN’ 02 Conference on Programming Language Design and Implementation (PLDI-02), June 2002.Google Scholar
- [FTA01]Jeffrey S. Foster, Tachio Terauchi, and Alex Aiken. Flow-Sensitive Type Qualifiers. Technical Report UCB//CSD-01-1162, University of California, Berkeley, November 2001.Google Scholar
- [HRB90]Susan Horwitz, Thomas Reps, and David Binkley. Interprocedural slicing using dependence graphs. ACM Transactions on Programming Languages and Systems, 12(1):26–60, January 1990.Google Scholar
- [HRS95]Susan Horwitz, Thomas Reps, and Mooly Sagiv. Demand-driven inter-procedural dataflow analysis. In Proceedings of the ACM SIGSOFT Symposium on Foundations of Software Engineering Notes, volume 20, 1995.Google Scholar
- [HT01]Nevin Heintze and O. Tardeau. Ultra fast aliasing analysis using CLA: a million lines in a second. In Proceedings of the ACM SIGPLAN’ 01 Conference on Programming Language Design and Implementation (PLDI-01), 2001.Google Scholar
- [OJ97]R. O’Callahan and D. Jackson. Lackwit: A program understanding tool based on type inference. In Proceedings of the 1997 International Conference on Software Engineering, 1997.Google Scholar
- [RRL99]Atanas Rountev, Barbara G. Ryder, and William Landi. Data-flow analysis of program fragments. In Proceedings of the ACM SIGSOFT Symposium on Foundations of Software Engineering, pages 235–252, 1999.Google Scholar
- [Ruf97]E. Ruf. Partitioning dataflow analyses using types. In Conference Record of the Twenty-Fourth ACM Symposium on Principles of Programming Languages, 1997.Google Scholar
- [SY86]R. Strom and S. Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering, 12(1):157–171, 1986.Google Scholar
- [Tip95]F. Tip. A survey of program slicing techniques. Journal of Programming Languages, 3(3):121–189, 1995.Google Scholar
- [WL95]R. Wilson and Monica Lam. Efficient context-sensitive pointer analysis for C progams. In Proceedings of the ACM SIGPLAN’ 95 Conference on Programming Language Design and Implementation (PLDI-95), 1995.Google Scholar
- [ZRL96]S. Zhang, B. Ryder, and W. Landi. Program Decomposition for Pointer Aliasing: A Step toward Practical Analyses. In Fourth Symposium on the Foundations of Software Engineering (FSE4), 1996.Google Scholar