Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Thomas Ball, Rupak Majumdar, Todd Millstein, and Sriram K. Rajamani. Automatic predicate abstraction of c programs. In Proceedings of the ACM SIGPLAN’ 01 Conference on Programming Language Design and Implementation (PLDI-01), volume 35, pages 203–213, 2001.
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.
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.
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.
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.
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.
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.
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.
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.
Jeffrey S. Foster, Tachio Terauchi, and Alex Aiken. Flow-Sensitive Type Qualifiers. Technical Report UCB//CSD-01-1162, University of California, Berkeley, November 2001.
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.
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.
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.
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.
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.
E. Ruf. Partitioning dataflow analyses using types. In Conference Record of the Twenty-Fourth ACM Symposium on Principles of Programming Languages, 1997.
R. Strom and S. Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering, 12(1):157–171, 1986.
F. Tip. A survey of program slicing techniques. Journal of Programming Languages, 3(3):121–189, 1995.
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.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Adams, S. et al. (2002). Speeding Up Dataflow Analysis Using Flow-Insensitive Pointer Analysis. In: Hermenegildo, M.V., Puebla, G. (eds) Static Analysis. SAS 2002. Lecture Notes in Computer Science, vol 2477. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45789-5_18
Download citation
DOI: https://doi.org/10.1007/3-540-45789-5_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44235-6
Online ISBN: 978-3-540-45789-3
eBook Packages: Springer Book Archive