Abstract
We derive a control-flow analysis that 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 across optimized tail calls. 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 continuation-passing style (CPS) transformation
followed by an abstract interpretation of a stack-less CPS machine,
and 2) extract an equivalent constraint-based analysis formulation,
thereby providing a rational reconstruction of a constraint-based
control-flow analysis from abstract interpretation principles.
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 across optimized tail calls. 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 continuation-passing style (CPS) transformation
followed by an abstract interpretation of a stack-less CPS machine,
and 2) extract an equivalent constraint-based analysis formulation,
thereby providing a rational reconstruction of a constraint-based
control-flow analysis from abstract interpretation principles.
| Originalsprog | Engelsk |
|---|
| Forlag | INRIA |
|---|---|
| Status | Udgivet - 2009 |