[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.)
David
Pushdown Flow Analysis of First-Class Control
Dimitrios Vardoulakis and Olin Shivers (Northeastern University)
To appear, ICFP 2011
http://www.ccs.neu.edu/home/dimvar/papers/callcc-cfa2.pdf
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