Similarly, in the abstract semantics, continuations are
deallocated as soon as they become unreachable, which
often corresponds to when they would be popped. We say
often, because due to the finiteness of the store, this correspondence cannot always hold. However, this approach
gives a good finite approximation to infinitary stack analyses that can always match calls and returns.
5. ReLateD WoRK
The study of abstract machines for the λ-calculus began
with Landin’s SECD machine,
11 the systematic construction of machines from semantics with Reynolds’s
20 the theory of abstract interpretation with the seminal work of Cousot and Cousot,
static analysis of the λ-calculus with Jones’s coupling of
abstract machines and abstract interpretation.
9 All have
been active areas of research since their inception, but
only recently have well-known abstract machines been
connected with abstract interpretation by Midtgaard and
14, 15 We strengthen the connection by demonstrating a general technique for abstracting abstract machines.
The approximation of abstract machine states for the
analysis of higher-order languages goes back to Jones,
who argued abstractions of regular tree automata
could solve the problem of recursive structure in environments. We reinvoked that wisdom to eliminate the
recursive structure of continuations by allocating them
in the store.
Midtgaard and Jensen present a 0CFA for a CPS language.
14 The approach is based on Cousot-style calculational abstract interpretation,
3 applied to a functional
language. Like the present work, Midtgaard and Jensen
start with a known abstract machine for the concrete
semantics, the CE machine of Flanagan et al.,
8 and employ
a reachable-states model. They then compose well-known
Galois connections to reveal a 0CFA with reachability in
the style of Ayers.
1 The CE machine is not sufficient to
interpret direct-style programs, so the analysis is specialized to programs in continuation-passing style.
Although our approach is not calculational like
Midtgaard and Jensen’s, it continues in their vein by
applying abstract interpretation to well-known machines,
extending the application to direct-style machines to
obtain a parameterized family of analyses that accounts
Static analyzers typically hemorrhage precision in the
presence of exceptions and first-class continuations: they
jump to the top of the lattice of approximation when these
features are encountered. Conversion to continuation- and
exception-passing style can handle these features without
forcing a dramatic ascent of the lattice of approximation.
The cost of this conversion, however, is lost knowledge—
both approaches obscure static knowledge of stack structure, by desugaring it into syntax.
Might and Shivers introduced the idea of using abstract
garbage collection to improve precision and efficiency in
16 They develop a garbage collecting abstract
machine for a CPS language and prove it correct. We extend
abstract garbage collection to direct-style languages
interpreted on the CESK machine.
6. ConCLUsions anD PeRsPeCtiVe
We have demonstrated a derivational approach to program
analysis that yields novel abstract interpretations of languages with higher-order functions, control, state, and garbage collection. These abstract interpreters are obtained
by a straightforward pointer refinement and structural
abstraction that bounds the address space, making the
abstract semantics safe and computable. The technique
allows concrete implementation technology, such as garbage collection, to be imported straightforwardly into that
of static analysis, bearing immediate benefits. More generally, an abstract machine based approach to analysis shifts
the focus of engineering efforts from the design of complex
analytic models such as involved constraint languages back
to the design of programming languages and machines,
from which analysis can be derived. Finally, our approach
uniformly scales up to richer language features such as laziness, stack-inspection, exceptions, and object-orientation.
We speculate that store-allocating bindings and continuations is sufficient for a straightforward abstraction of most
Looking forward, a semantics-based approach opens
new possibilities for design. Context-sensitive analysis can
have daunting complexity,
24 which we have made efforts
17 but modular program analysis is crucial to overcome the significant cost of precise abstract interpretation. Modularity can be achieved without needing to design
clever approximations, but rather by designing modular
semantics from which modular analyses follow systematically.
23 Likewise, push-down analyses offer infinite state
space abstractions with perfect call-return matching while
retaining decidability. Our approach expresses this form of
abstraction naturally: the store remains bounded, but continuations stay on the stack.
We thank Matthias Felleisen, Jan Midtgaard, Sam Tobin-Hochstadt, and Mitchell Wand for discussions, and the
anonymous reviewers of ICFP¢
10 for their close reading and
helpful critiques; their comments have improved this paper.
Van Horn’s work is supported by the National Science
Foundation under grant 0937060 to the Computing Research Association for the CIFellow Project. Might’s
research is based upon work supported by the National
Science Foundation under Grant No. 1035658.
1. ayers, a.e. abstract analysis and
optimization of scheme. PhD
thesis, Massachusetts institute of
2. biernacka, M., Danvy, o. a concrete
framework for environment machines.
ACM Trans. Comput. Logic 9, 1 (2007)
3. Cousot, P. the calculational design of a
generic abstract interpreter. in M. broy
and r. steinbrüggen. eds. Calculational
System Design. nato asi series F.
ios Press, amsterdam (1999).
4. Cousot, P., Cousot, r. abstract
interpretation: a unified lattice
model for static analysis of
programs by construction or
approximation of fixpoints.
in POPL ´77: Proceedings of the
4th ACM SIGACT-SIGPLAN
Symposium on Principles of
Programming Languages (new york,
1977), aCM, 238–252.