抽象机器Abstract Machines
Abstracting Abstract Machines
摘要：
我们描述了一种推导的方法，抽象的解释，产生新颖的和透明的声音静态分析时，适用于完善的抽象机器。为了证明的技术和支持我们的要求，我们转换的CEK机Felleisen和弗里德曼，Krivine的机器的懒惰的变种，和堆栈检查CM机克莱门茨和Felleisen到抽象的解释自己。由此产生的分析约束时序的程序事件，预测返回流和堆栈检查行为，并近似的流量和评估的需要参数。对于所有这些机器，我们发现，一系列众所周知的具体的机器重构，加上我们称之为存储分配延续的技术，导致机器抽象到静态分析简单地通过绑定其存储。我们证明了该技术的规模统一，允许静态分析现实的语言功能，包括尾部调用，条件，副作用，异常，一流的延续，甚至垃圾回收。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
