Control-Flow Analysis of Function Calls and Returns by Abstract Interpretation

Jan Midtgaard and Thomas P. Jensen

The 14th ACM SIGPLAN International Conference on Functional Programming (ICFP 2009)
Edinburgh, Scotland, 31st August - 2nd September 2009


Abstract

We derive a control-flow analysis for a simple higher-order functional language. Contrary to existing direct-style analyses, our analysis approximates the interprocedural 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 function calls return. The analysis is systematically 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 CPS-transformation followed by an abstract interpretation of a stack-less CPS machine, and 2) extract an equivalent constraint-based formulation, thereby providing a rational reconstruction of a constraint-based CFA from abstract interpretation principles.


START Conference Manager (V2.56.8 - Rev. 748M)