Abstracting Abstract Machines

TL;DR

This paper introduces a derivational approach to abstract interpretation that transforms well-known abstract machines into sound static analyses, effectively handling complex language features and scaling to realistic programming languages.

Contribution

It presents a novel derivational technique that simplifies deriving static analyses from concrete machines by bounding their stores, enabling scalable analysis of advanced language features.

Findings

Transformations produce sound static analyses for various abstract machines.

The approach scales to realistic language features like tail calls, exceptions, and garbage collection.

The method provides a uniform framework for deriving analyses from concrete semantics.

Abstract

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.