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 definitional interpreters, 20 the theory of abstract interpretation with the seminal work of Cousot and Cousot, 4 and 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 Jensen. 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, 9 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 for polyvariance.

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. 21 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 flow analysis. 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 existing machines.

Looking forward, a semantics-based approach opens new possibilities for design. Context-sensitive analysis can have daunting complexity, 24 which we have made efforts to tame, 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.

acknowledgments

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.

References

1. ayers, a.e. abstract analysis and optimization of scheme. PhD thesis, Massachusetts institute of technology (1993).

2. biernacka, M., Danvy, o. a concrete framework for environment machines. ACM Trans. Comput. Logic 9, 1 (2007) 1–30.

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.