Systematic Abstraction of Abstract Machines

TL;DR

This paper presents a systematic derivational approach to abstract interpretation that transforms well-known abstract machines into sound static analyses, capable of handling complex language features and scalable to realistic programming languages.

Contribution

It introduces a unified method to derive static analyses from concrete abstract machines using store bounding and refactorings, bridging formalism and implementation.

Findings

Transformations of CEK, Krivine, and CM machines into static analyses

Analysis bounds temporal ordering, return-flow, and stack-inspection

Scales to realistic language features like tail calls, exceptions, and garbage collection

Abstract

We describe a derivational approach to abstract interpretation that yields novel and transparently sound static analyses when applied to well-established abstract machines for higher-order and imperative programming languages. 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 of 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. In order to close the gap between formalism and implementation, we provide translations of the mathematics as running Haskell code for the initial development of our method.