Skip to Main content Skip to Navigation
Conference papers

Control-flow analysis of function call and returns by abstract interpretation

Jan Midtgaard 1, * Thomas Jensen 2 
* Corresponding author
2 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : We derive a control-flow analysis that approximates the interproce- dural control-flow of both function calls and returns in the presence of first-class functions and tail-call optimization. In addition to an abstract environment, our analysis computes for each expression an abstract control stack, effectively approximating where func- tion calls return across optimized tail calls. The analysis is sys- tematically calculated by abstract interpretation of the stack-based CaEK abstract machine of Flanagan et al. using a series of Galois connections. Abstract interpretation provides a unifying setting in which we 1) prove the analysis equivalent to the composition of a continuation-passing style (CPS) transformation followed by an abstract interpretation of a stack-less CPS machine, and 2) extract an equivalent constraint-based formulation, thereby providing a ratio- nal reconstruction of a constraint-based control-flow analysis from abstract interpretation principles.
Document type :
Conference papers
Complete list of metadata

Cited literature [37 references]  Display  Hide  Download
Contributor : Thomas Jensen Connect in order to contact the contributor
Submitted on : Wednesday, March 9, 2011 - 10:40:13 AM
Last modification on : Wednesday, February 2, 2022 - 3:50:47 PM
Long-term archiving on: : Friday, June 10, 2011 - 2:26:27 AM


Files produced by the author(s)



Jan Midtgaard, Thomas Jensen. Control-flow analysis of function call and returns by abstract interpretation. ACM International Conference on Functional Programming, Sep 2009, Edinburgh, United Kingdom. ⟨10.1145/1596550.1596592⟩. ⟨inria-00574944⟩



Record views


Files downloads