Verified compositional compilation (VCC) is a notion of modular verification of compilers that supports compilation of heterogeneous programs. The key to achieve VCC is to design a semantic interface that enables composition of correctness theorems for compiling individual modules. Most of the existing techniques for VCC fix a semantic interface from the very beginning and force it down to every single compiler pass. This requires significant changes to the existing framework and makes it difficult to understand the relationship between conditions enforced by the semantic interface and the actual requirements of compiler passes. A different approach is to design appropriate semantic interfaces for individual compiler passes and combine them into a unified interface which faithfully reflects the requirements of underlying compiler passes. However, this requires vertically composable simulation relations, which were traditionally considered very difficult to construct even with extensive changes to compiler verification frameworks. We propose a solution to construction of unified semantic interfaces for VCC with a bottom-up approach. Our starting point is CompCertO, an extension of CompCert -- the state-of-the-art verified compiler -- that supports VCC but lacks a unified interface. We discover that a CompCert Kripke Logical Relation (CKLR) in CompCertO provides a uniform notion of memory protection for evolving memory states across modules and is transitively composable. Based on this uniform and composable CKLR, we then merge the simulation relations for all the compiler pass in CompCertO (except for three value analysis passes) into a unified interface. We demonstrate the conciseness and effectiveness of this unified interface by applying it to verify the compositional compilation of a non-trivial heterogeneous program with mutual recursion.
翻译:校验组成汇编( VCC) 是编译者模块化校验的概念, 支持编译各种程序。 实现 VCC 的关键是设计一个语义界面, 使编译者能够组成正确性理论, 用于编辑各个模块。 VCC 的多数现有技术从一开始就固定一个语义界面, 并迫使它下至每个编译者通行证。 这要求对现有框架进行重大修改, 并使得难以理解语义界面执行的条件与编译者通行证的实际要求之间的关系。 一个不同的方法是设计一个适合个人编译者通行证的语义界面, 并将其合并成一个统一的界面, 从而忠实地反映对编译者简写者版本的要求。 然而, 这需要垂直的可拼写模拟关系, 即使在对编译者校验框架进行广泛修改后, 也被认为是非常困难的。 我们的起点是CervertiveLO, CompublicC 和 Comptraclationral 的扩展点, 支持VCC- 校验的校正 校正 校验的校正 校正 校验的校, 校验的校验中, 校验校验的校校校校验的校, 的校验的校, 校验的校, 校校校校校, 校, 校校校校, 校验的校验的校验, 校验的校, 校验, 校校。</s>