CompCertELF: verified separate compilation of C programs into ELF object files
CompCertELF: verified separate compilation of C programs into ELF object files
复制标题
DOI：
10.1145/3428265
复制
发表时间：
2020-11
影响因子：
--
通讯作者：
Yuting Wang;Xiangzhe Xu;Pierre Wilke;Zhong Shao
中科院分区：
文献类型：
--
作者：
Yuting Wang;Xiangzhe Xu;Pierre Wilke;Zhong Shao
我们提出了CompCertelf，这是CompCert的第一个扩展程序，该扩展名支持了从C程序一直到标准二进制文件格式的经过验证的汇编，即ELF对象格式。以前的堆栈感知compcert的工作提供了经过验证的汇编链，从C程序到具有逼真的机器内存模型的组装程序。我们通过使用经过验证的汇编程序修改和扩展此编译链来构建compertelf，从而进一步将汇编程序转换为精灵对象文件。 CompCert通过经过验证的单独汇编支持大规模验证：C可以单独编写和编译C模块，然后将其链接在一起以获取一个目标程序，以优化从源模块链接的程序的语义。但是，CompCert中已验证的单独汇编仅适用于汇编程序，而不是对象文件。对于后者而言，主要的困难是桥接链接的两个不同视图：一个用于CompCert程序的程序，该程序允许通过链接而任意链接全局定义，而另一个则用于将编码定义块视为不可分割的单元的对象文件。我们提出了一种轻巧的方法，该方法可以解决上述问题，而没有任何修改来验证单独汇编的框架：通过引入程序之间的句法等价概念，并证明语法等效性与两种不同类型的链接之间的交换性，我们能够交通运输。从Compcert中更抽象的链接操作到精灵对象文件的更具体的操作。通过将此方法应用于CompCertelf，我们将获得第一个支持验证的C程序单独编译到ELF对象文件中的编译器。
We present CompCertELF, the first extension to CompCert that supports verified compilation from C programs all the way to a standard binary file format, i.e., the ELF object format. Previous work on Stack-Aware CompCert provides a verified compilation chain from C programs to assembly programs with a realistic machine memory model. We build CompCertELF by modifying and extending this compilation chain with a verified assembler which further transforms assembly programs into ELF object files. CompCert supports large-scale verification via verified separate compilation: C modules can be written and compiled separately, and then linked together to get a target program that refines the semantics of the program linked from the source modules. However, verified separate compilation in CompCert only works for compilation to assembly programs, not to object files. For the latter, the main difficulty is to bridge the two different views of linking: one for CompCert's programs that allows arbitrary shuffling of global definitions by linking and the other for object files that treats blocks of encoded definitions as indivisible units. We propose a lightweight approach that solves the above problem without any modification to CompCert's framework for verified separate compilation: by introducing a notion of syntactical equivalence between programs and proving the commutativity between syntactical equivalence and the two different kinds of linking, we are able to transit from the more abstract linking operation in CompCert to the more concrete one for ELF object files. By applying this approach to CompCertELF, we obtain the first compiler that supports verified separate compilation of C programs into ELF object files.