Calling context abstraction with shapes

ABSTRACT

Interprocedural program analysis is often performed by computing procedure summaries. While possible, computing adequate summaries is difficult, particularly in the presence of recursive procedures. In this paper, we propose a complementary framework for interprocedural analysis based on a direct abstraction of the calling context. Specifically, our approach exploits the inductive structure of a calling context by treating it directly as a stack of activation records. We then build an abstraction based on separation logic with inductive definitions. A key element of this abstract domain is the use of parameters to refine the meaning of such call stack summaries and thus express relations across activation records and with the heap. In essence, we define an abstract interpretation-based analysis framework for recursive programs that permits a fluid per call site abstraction of the call stack--much like how shape analyzers enable a fluid per program point abstraction of the heap.

References

1. Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. Symbolic execution with separation logic. In Asian Symposium on Programming Languages and Systems (APLAS), pages 52--68, 2005.
2. Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, and Hongseok Yang. Shape analysis for composite data structures. In Computer-Aided Verification (CAV), pages 178--192, 2007.
3. Bruno Blanchet, Patrick Cousot, Radhia Cousot, J´ erÆ ome Feret, Lau-rent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. A static analyzer for large safety-critical software. In Programming Language Design and Implementation (PLDI), pages 196--207, 2003.
4. Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, and Hongseok Yang. Compositional shape analysis by means of bi-abduction. In Principles of Programming Languages (POPL), pages 289--300, 2009.
5. Bor-Yuh Evan Chang and Xavier Rival. Relational inductive shape analysis. In Principles of Programming Languages (POPL), pages 247--260, 2008.
6. Bor-Yuh Evan Chang, Xavier Rival, and George C. Necula. Shape analysis with structural invariant checkers. In Static Analysis (SAS), pages 384--401, 2007.
7. Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Principles of Programming Languages (POPL), pages 238--252, 1977.
8. Patrick Cousot and Nicolas Halbwachs. Automatic discovery of linear restraints among variables of a program. In Principles of Program-ming Languages (POPL), pages 84--97, 1978.
9. Alain Deutsch. On determining lifetime and aliasing of dynamically allocated data in higher-order functional specifications. In Principles of Programming Languages (POPL), pages 157--168, 1990.
10. Dino Distefano, Peter W. O'Hearn, and Hongseok Yang. A local shape analysis based on separation logic. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 287--302, 2006.
11. Jérôme Feret. Static analysis of digital filters. In European Symposium on Programming (ESOP), pages 33--48, 2004.
12. Alexey Gotsman, Josh Berdine, and Byron Cook. Interprocedural shape analysis with separated heap abstractions. In Static Analysis (SAS), pages 240--260, 2006.
13. Bhargav S. Gulavani, Supratik Chakraborty, Ganesan Ramalingam, and Aditya V. Nori. Bottom-up shape analysis. In Static Analysis (SAS), pages 188--204, 2009.
14. Bolei Guo, Neil Vachharajani, and David I. August. Shape analysis with inductive recursion synthesis. In Programming Language Design and Implementation (PLDI), pages 256--265, 2007.
15. Bertrand Jeannet and Wendelin Serwe. Abstracting call-stacks for interprocedural verification of imperative programs. In Algebraic Methodology and Software Technology (AMAST), pages 258--273, 2004.
16. Bertrand Jeannet, Alexey Loginov, Thomas Reps, and Mooly Sagiv. A relational approach to interprocedural shape analysis. ACM Trans. Program. Lang. Syst., 32(2), 2010.
17. Jörg Kreiker, Thomas Reps, Noam Rinetzky, Mooly Sagiv, Reinhard Wilhelm, and Eran Yahav. Interprocedural shape analysis for effec-tively cutpoint-free programs. Technical report, Queen Mary Univer-sity of London, 2010.
18. Vincent Laviron, Bor-Yuh Evan Chang, and Xavier Rival. Separating shape graphs. In European Symposium on Programming (ESOP), pages 387--406, 2010.
19. Mark Marron, Manuel V. Hermenegildo, Deepak Kapur, and Darko Stefanovic. Efficient context-sensitive shape analysis with graph based heap models. In Compiler Construction (CC), pages 245--259, 2008.
20. Thomas Reps, Susan Horwitz, and Mooly Sagiv. Precise interproce-dural dataflow analysis via graph reachability. In Principles of Programming Languages (POPL), pages 49--61, 1995.
21. John C. Reynolds. Separation logic: A logic for shared mutable data structures. In Logic in Computer Science (LICS), pages 55--74, 2002.
22. Noam Rinetzky and Mooly Sagiv. Interprocedural shape analysis for recursive programs. In Compiler Construction (CC), pages 133--149, 2001.
23. Noam Rinetzky, Jörg Bauer, Thomas Reps, Mooly Sagiv, and Rein-hard Wilhelm. A semantics for procedure local heaps and its abstrac-tions. In Principles of Programming Languages (POPL), pages 296--309, 2005.
24. Noam Rinetzky, Mooly Sagiv, and Eran Yahav. Interprocedural shape analysis for cutpoint-free programs. In Static Analysis (SAS), pages 284--302, 2005.
25. Xavier Rival and Laurent Mauborgne. The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst., 29(5), 2007.
26. Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Solving shape-analysis problems in languages with destructive updating. ACM Trans. Program. Lang. Syst., 20(1):1--50, 1998.
27. Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst., 24(3): 217--298, 2002.
28. Micha Sharir and Amir Pnueli. Two approaches to interprocedural data flow analysis. In Steven S. Muchnick and Neil D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 7, pages 189--233. Prentice-Hall, 1981.
29. Arnaud Venet. Abstract cofibered domains: Application to the alias analysis of untyped programs. In Static Analysis (SAS), pages 366--382, 1996.

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

  • Logic

  • Semantics and reasoning

    • Program reasoning

      • Program analysis

      • Program verification

    • Program semantics