Control-Flow Analysis of Function Calls and Returnsby Abstract Interpretation

摘要

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 ab-stract 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.