[hofa] Pushdown Flow Analysis of First-Class Control
shivers at ccs.neu.edu
Wed Jun 22 13:43:24 PDT 2011
On Jun 22, 2011, at 4:41 PM, David Van Horn <dvanhorn at ccs.neu.edu> wrote:
> Here's another interesting paper. This one shows how to do pushdown analysis of a language with call/cc, which is difficult since first-class control destroys call/return matching. It will appear at this year's ICFP. (The link below is to a draft, not the final version.)
> Pushdown Flow Analysis of First-Class Control
> Dimitrios Vardoulakis and Olin Shivers (Northeastern University)
> To appear, ICFP 2011
> Pushdown models are better than control-flow graphs for higher- order flow analysis. They faithfully model the call/return structure of a program, which results in fewer spurious flows and increased precision. However, pushdown models require that calls and returns in the analyzed program nest properly. As a result, they cannot be used to analyze language constructs that break call/return nesting such as generators, coroutines, call/cc, etc.
> In this paper, we extend the CFA2 flow analysis to create the first pushdown flow analysis for languages with first-class control. We modify the abstract semantics of CFA2 to allow continuations to escape to, and be restored from, the heap. We then present a summarization algorithm that handles escaping continuations via a new kind of summary edges. We prove that the algorithm is sound with respect to the abstract semantics.
> HOFA mailing list
> HOFA at lists.lambda-calcul.us
More information about the HOFA