Calling Context Abstraction with Shapes

Xavier Rival 1, 2 Bor-Yuh Evan Chang 3
2 ABSTRACTION - Abstract Interpretation and Static Analysis
DI-ENS - Département d'informatique de l'École normale supérieure, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
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.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [29 references]  Display  Hide  Download

https://hal.inria.fr/hal-00760421
Contributor : Xavier Rival <>
Submitted on : Monday, December 3, 2012 - 8:03:53 PM
Last modification on : Friday, May 25, 2018 - 12:02:05 PM
Document(s) archivé(s) le : Monday, March 4, 2013 - 3:54:23 AM

File

popl11-stack.pdf
Publisher files allowed on an open archive

Identifiers

Collections

Citation

Xavier Rival, Bor-Yuh Evan Chang. Calling Context Abstraction with Shapes. POPL'11 - 38th annual ACM SIGPLAN-SIGACT symposium on Principles Of Programming Languages 2011, Jan 2011, Austin, United States. pp.173-186, ⟨10.1145/1925844.1926406⟩. ⟨hal-00760421⟩

Share

Metrics

Record views

264

Files downloads

196