Hybrid top-down and bottom-up interprocedural analysis

ABSTRACT

Interprocedural static analyses are broadly classified into top-down and bottom-up, depending upon how they compute, instantiate, and reuse procedure summaries. Both kinds of analyses are challenging to scale: top-down analyses are hindered by ineffective reuse of summaries whereas bottom-up analyses are hindered by inefficient computation and instantiation of summaries. This paper presents a hybrid approach Swift that combines top-down and bottom-up analyses in a manner that gains their benefits without suffering their drawbacks. Swift is general in that it is parametrized by the top-down and bottom-up analyses it combines. We show an instantiation of Swift on a type-state analysis and evaluate it on a suite of 12 Java programs of size 60-250 KLOC each. Swift outperforms both conventional approaches, finishing on all the programs while both of those approaches fail on the larger programs.

References

1. A. Albarghouthi, R. Kumar, A. Nori, and S. Rajamani. Parallelizing top-down interprocedural analyses. In PLDI, 2012.
2. T. Ball and S. Rajamani. Bebop: a path-sensitive interprocedural dataflow engine. In PASTE, 2001.
3. C. Calcagno, D. Distefano, P. O'Hearn, and H. Yang. Compositional shape analysis by means of bi-abduction. J. ACM, 58(6), 2011.
4. R. Chatterjee, B. Ryder, and W. Landi. Relevant context inference. In POPL, 1999.
5. P. Cousot and R. Cousot. Static determination of dynamic properties of recursive procedures. In E. Neuhold, editor, Formal Descriptions of Programming Concepts. North-Holland, 1978.
6. P. Cousot and R. Cousot. Modular static program analysis. In CC, 2002.
7. I. Dillig, T. Dillig, A. Aiken, and M. Sagiv. Precise and compact modular procedure summaries for heap manipulating programs. In PLDI, 2011.
8. S. Fink, E. Yahav, N. Dor, G. Ramalingam, and E. Geay. Effective typestate verification in the presence of aliasing. ACM TOSEM, 17(2), 2008.
9. R. Ghiya and L. Hendren. Connection analysis: A practical interprocedural heap analysis for C. IJPP, 24(6), 1996.
10. B. Gulavani, S. Chakraborty, G. Ramalingam, and A. Nori. Bottom-up shape analysis using lisf. ACM TOPLAS, 33(5), 2011.
11. S. Gulwani and A. Tiwari. Computing procedure summaries for interprocedural analysis. In ESOP, 2007.
12. B. Jeannet, A. Loginov, T. Reps, and M. Sagiv. A relational approach to interprocedural shape analysis. ACM TOPLAS, 32(2), 2010.
13. R. Madhavan, G. Ramalingam, and K. Vaswani. Modular heap analysis for higher-order programs. In SAS, 2012.
14. T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In POPL, 1995.
15. N. Rinetzky, J. Bauer, T. Reps, S. Sagiv, and R. Wilhelm. A semantics for procedure local heaps and its abstractions. In POPL, 2005.
16. N. Rinetzky, M. Sagiv, and E. Yahav. Interprocedural shape analysis for cutpoint-free programs. In SAS, 2005.
17. S. Sagiv, T. W. Reps, and S. Horwitz. Precise interprocedural dataflow analysis with applications to constant propagation. Theor. Comput. Sci., 167(1&2), 1996.
18. A. Salcianu and M. Rinard. Purity and side effect analysis for Java programs. In VMCAI, 2005.
19. M. Sharir and A. Pnueli. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications, chapter 7. Prentice-Hall, 1981.
20. J. Whaley and M. Rinard. Compositional pointer and escape analysis for Java programs. In OOPSLA, 1999.
21. Y. Xie and A. Aiken. Saturn: A scalable framework for error detection using boolean satisfiability. ACM TOPLAS, 29(3), 2007.
22. G. Yorsh, E. Rabinovich, M. Sagiv, A. Meyer, and A. Bouajjani. A logic of reachable patterns in linked data-structures. In FOSSACS, 2006.
23. G. Yorsh, E. Yahav, and S. Chandra. Generating precise and concise procedure summaries. In POPL, 2008.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification