Staged abstract interpreters: fast and modular whole-program analysis via meta-programming
Staged abstract interpreters: fast and modular whole-program analysis via meta-programming
复制标题
分阶段抽象解释器：通过元编程进行快速、模块化的整个程序分析
DOI：
10.1145/3360552
复制
发表时间：
2019
影响因子：
--
通讯作者：
Tiark Rompf
中科院分区：
文献类型：
--
作者：
Guannan Wei;Yuxuan Chen;Tiark Rompf
众所周知，阶段式解释器就是编译器：将解释器专门化到给定程序会产生运行速度更快的等价可执行文件。这种连接被称为第一个Futamura投影。更广为人知的是，抽象解释器是程序分析器：调整解释器以在抽象域上运行会产生合理的静态分析。当我们将这两个想法结合起来，并将专门化应用于抽象的解释器时，会发生什么？在这篇文章中，我们提出了一个统一的框架，它自然地将第一个Futamura投影从具体的解释器扩展到抽象的解释器。我们的方法基于类型级绑定时间抽象和一元抽象的泛型解释器，得到了一个完善的阶段式抽象解释器。通过使用这些抽象的不同实例化，通用解释器可以以四种模式之一灵活地行为：作为非阶段性的具体解释器、阶段性的具体解释器、非阶段性的抽象解释器或阶段性的抽象解释器。作为无遗憾抽象的一个例子，这些抽象层的开销在升级后生成的代码中被消除了。我们展示了阶段化抽象解释器对于优化静态分析是实用和有用的，所有这些都需要较少的工程工作，并且不会影响可靠性。我们进行了三个案例研究，包括与Boucher和Feeley的抽象编译的比较，在各种控制流分析中的应用，以及模块分析的演示。我们还实证评估了阶段性对执行时间的影响。实验表明，对于控制流分析，阶段性加速可达数量级。
It is well known that a staged interpreter is a compiler: specializing an interpreter to a given program produces an equivalent executable that runs faster. This connection is known as the first Futamura projection. It is even more widely known that an abstract interpreter is a program analyzer: tweaking an interpreter to run on abstract domains produces a sound static analysis. What happens when we combine these two ideas, and apply specialization to an abstract interpreter? In this paper, we present a unifying framework that naturally extends the first Futamura projection from concrete interpreters to abstract interpreters. Our approach derives a sound staged abstract interpreter based on a generic interpreter with type-level binding-time abstractions and monadic abstractions. By using different instantiations of these abstractions, the generic interpreter can flexibly behave in one of four modes: as an unstaged concrete interpreter, a staged concrete interpreter, an unstaged abstract interpreter, or a staged abstract interpreter. As an example of abstraction without regret, the overhead of these abstraction layers is eliminated in the generated code after staging. We show that staging abstract interpreters is practical and useful to optimize static analysis, all while requiring less engineering effort and without compromising soundness. We conduct three case studies, including a comparison with Boucher and Feeley’s abstract compilation, applications to various control-flow analyses, and a demonstration for modular analysis. We also empirically evaluate the effect of staging on the execution time. The experiment shows an order of magnitude speedup with staging for control-flow analyses.
抽象解释器的组合健全性证明
影响因子：
--
作者：
S. Keidel;C. Bach Poulsen;S. Erdweg
通讯作者：
S. Erdweg