Advertisement

Speeding Up Dataflow Analysis Using Flow-Insensitive Pointer Analysis

  • Stephen Adams
  • Thomas Ball
  • Manuvir Das
  • Sorin Lerner
  • Sriram K. Rajamani
  • Mark Seigle
  • Westley Weimer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2477)

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.

Keywords

Will Emit Large Program Device Driver Ground Term Program Point 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [BMMR01]
    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.CrossRefGoogle Scholar
  2. [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
  3. [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
  4. [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
  5. [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
  6. [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
  7. [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
  8. [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
  9. [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
  10. [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
  11. [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
  12. [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
  13. [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
  14. [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
  15. [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
  16. [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
  17. [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
  18. [Tip95]
    F. Tip. A survey of program slicing techniques. Journal of Programming Languages, 3(3):121–189, 1995.Google Scholar
  19. [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
  20. [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

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Stephen Adams
    • 1
  • Thomas Ball
    • 1
  • Manuvir Das
    • 1
  • Sorin Lerner
    • 2
  • Sriram K. Rajamani
    • 1
  • Mark Seigle
    • 2
  • Westley Weimer
    • 3
  1. 1.Microsoft ResearchUSA
  2. 2.University of WashingtonUSA
  3. 3.UC BerkeleyUSA

Personalised recommendations