Black-Box Equivalence Checking Across Compiler Optimizations
Black-Box Equivalence Checking Across Compiler Optimizations
复制标题
跨编译器优化的黑盒等效性检查
DOI：
10.1007/978-3-319-71237-6_7
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Sorav Bansal
中科院分区：
文献类型：
--
作者：
Manjeet Dahiya;Sorav Bansal
等效检查是程序合成和验证的重要组成部分。为了与现代编译器竞争合成工具，其等效检查器应能够验证这些编译器产生的转换。我们发现，编译器产生的转换多种多样，并且不确定的行为的存在使他们能够产生更具侵略性的优化。在翻译验证的背景下，已经完成了对等效检查的先前工作，在这种情况下，采用了基于通行证的方法，或者证明了一组精心挑选的优化。这些设置不适用于需要黑框方法的合成工具。
Equivalence checking is an important building block for program synthesis and verification. For a synthesis tool to compete with modern compilers, its equivalence checker should be able to verify the transformations produced by these compilers. We find that the transformations produced by compilers are much varied and the presence of undefined behaviour allows them to produce even more aggressive optimizations. Previous work on equivalence checking has been done in the context of translation validation, where either a pass-by-pass based approach was employed or a set of handpicked optimizations were proven. These settings are not suitable for a synthesis tool where a black-box approach is required.