Systematic abstraction of abstract machines

DOI10.1017/S0956796812000238MaRDI QIDQ3165529zbMATH OpenFDO

Authors David van Horn, Matthew Might

Publication date 29 October 2012

Published in Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1107.3539

zbMATH Keywords

abstract interpretationabstract machinehigher-order programming languagesimperative programming languages

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18)

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.

Recommendations

• Abstracting abstract machines
• Optimizing abstract abstract machines
• Abstract interpreters for free
• Deriving a lazy abstract machine
• From operational semantics to abstract machines

Cites work

• A call-by-name lambda-calculus machine
• A concrete framework for environment machines
• A functional correspondence between call-by-need evaluators and lazy abstract machines
• Abstracting abstract machines
• CFA2: a context-free approach to control-flow analysis
• Control-flow analysis of function calls and returns by abstract interpretation
• Control-flow analysis of functional programs
• Flow analysis of lazy higher-order functional programs
• Improving flow analyses via ΓCFA
• Modular set-based analysis from contracts
• Semantics engineering with PLT Redex
• The Mechanical Evaluation of Expressions
• Types and trace effects of higher order programs

Cited in

(13)

• A generative methodology for the design of abstract machines
• Distilling abstract machines
• scientific article; zbMATH DE number 5185574 (Why is no real title available?)
• The Vienna abstract machine
• Abstraction of hardware construction
• scientific article; zbMATH DE number 2090723 (Why is no real title available?)
• Abstract interpreters for free
• Introspective pushdown analysis of higher-order programs
• Abstracting abstract machines
• Optimizing abstract abstract machines
• Higher order symbolic execution for contract verification and refutation
• From Natural Semantics to Abstract Machines
• On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion

Describes a project that uses

Uses Software

• Haskell
• PLT Redex

This page was built for publication: Systematic abstraction of abstract machines

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3165529)