Language-parametric compiler validation with application to LLVM
Language-parametric compiler validation with application to LLVM
复制标题
语言参数编译器验证及其应用于 LLVM
DOI：
--
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Grigore Roşu
中科院分区：
文献类型：
--
作者：
T. Kasampalis;D. Park;Zhengyao Lin;Vikram S. Adve;Grigore Roşu
我们提出了一种新的翻译验证（TV）系统设计，旨在与现代优化编译器（例如 LLVM）实际使用。现有的电视系统是针对特定的转换序列以及输入和输出程序的特定通用语言定制的，与此不同的是，我们的设计明确地将特定于转换的组件与系统的其余部分分开，并概括了与转换无关的组件。具体来说，我们提出了 Keq，第一个程序等价检查器，它对输入和输出语言语义进行参数化，并且不依赖于输入和输出程序之间的转换。 Keq 算法基于严格的形式化，即剪切互模拟，并被证明是正确的。我们为 LLVM 的指令选择过程设计了一个 TV 系统原型，能够自动证明从 LLVM IR 到用于编译 x86-64 的 MachineIR 的转换的等效性。这种转换使用不同的输入和输出语言，因此现有技术先前尚未解决。实验评估表明，Keq 成功证明了 SPEC 2006 中 GCC 支持的 4732 个函数中 90% 以上的正确翻译。
We propose a new design for a Translation Validation (TV) system geared towards practical use with modern optimizing compilers, such as LLVM. Unlike existing TV systems, which are custom-tailored for a particular sequence of transformations and a specific, common language for input and output programs, our design clearly separates the transformation-specific components from the rest of the system, and generalizes the transformation-independent components. Specifically, we present Keq, the first program equivalence checker that is parametric to the input and output language semantics and has no dependence on the transformation between the input and output programs. The Keq algorithm is based on a rigorous formalization, namely cut-bisimulation, and is proven correct. We have prototyped a TV system for the Instruction Selection pass of LLVM, being able to automatically prove equivalence for translations from LLVM IR to the MachineIR used in compiling to x86-64. This transformation uses different input and output languages, and as such has not been previously addressed by the state of the art. An experimental evaluation shows that Keq successfully proves correct the translation of over 90% of 4732 supported functions in GCC from SPEC 2006.