[hofa] Pushdown Flow Analysis of First-Class Control

David Van Horn dvanhorn at ccs.neu.edu
Wed Jun 22 13:38:59 PDT 2011

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.

More information about the HOFA mailing list