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

Jan Midtgaard, Thomas P. Jensen

    Publikation: Bog/antologi/afhandling/rapportRapportForskning


    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.

    StatusUdgivet - 2009

    Bibliografisk note

    Udvidet version af artikel accepteret til International Conference on Functional Programming (ICFP'09), Edinburgh, august-september 2009.

    Citer dette