Abstracting Abstract Machines
David Van Horn, Matthew Might
We describe a derivational approach to abstract interpretation that yields
novel and transparently sound static analyses when applied to well-established
abstract machines. To demonstrate the technique and support our claim, we
transform the CEK machine of Felleisen and Friedman, a lazy variant of
Krivine's machine, and the stack-inspecting CM machine of Clements and
Felleisen into abstract interpretations of themselves. The resulting analyses
bound temporal ordering of program events; predict return-flow and
stack-inspection behavior; and approximate the flow and evaluation of by-need
parameters. For all of these machines, we find that a series of well-known
concrete machine refactorings, plus a technique we call store-allocated
continuations, leads to machines that abstract into static analyses simply by
bounding their stores. We demonstrate that the technique scales up uniformly to
allow static analysis of realistic language features, including tail calls,
conditionals, side effects, exceptions, first-class continuations, and even
garbage collection.