Lightweight Verification of Separate Compilation
* Seoul National University & ** MPI-SWS
This is the artifact for the POPL 2016 paper: "Lightweight Verification of Separate Compilation".
Project Page: http://sf.snu.ac.kr/sepcompcert
Major compiler verification efforts, such as the CompCert project, have traditionally simplified the verification problem by restricting attention to the correctness of whole-program compilation, leaving open the question of how to verify the correctness of separate compilation. Recently, a number of sophisticated techniques have been proposed for proving more flexible, compositional notions of compiler correctness, but these approaches tend to be quite heavyweight compared to the simple "closed simulations" used in verifying whole-program compilation. Applying such techniques to a compiler like CompCert, as Stewart et.al. have done, involves major changes and extensions to its original verification.
In this paper, we show that if we aim somewhat lower --- to prove correctness of separate compilation, but only for a single compiler --- we can drastically simplify the proof effort. Toward this end, we develop several lightweight techniques that recast the compositional verification problem in terms of whole-program compilation, thereby enabling us to largely reuse the closed-simulation proofs from existing compiler verifications. We demonstrate the effectiveness of these techniques by applying them to CompCert 2.4, converting its verification of whole-program compilation into a verification of separate compilation in less than two person-months. This conversion only required a small number of changes to the original proofs, and uncovered two compiler bugs along the way. The result is SepCompCert, the first verification of separate compilation for the full CompCert compiler.
During the proof, we found two bugs in CompCert 2.4. Bug #1 is due to an analysis that is invalidated in the presence of linking and Bug #2 is due to an invalid axiom assumed. We reported these bugs and they are now fixed in CompCert 2.5.
ID / Password:
All contents are in
CompCert2.4/: CompCert 2.4 with the following four patches applied:
Two bug-fixes are back-ported (§4.1, §5.2):
RTL-level optimization flags are introduced:
levelA/: Level A compositional verification of CompCert (§2.2, §4.1, and §5).
The main theorem is
linker_correct: if the C programs in
ctreeare linked into
cprog, and the C programs in
ctreeare separately compiled into the ASM programs in
asmtree, then there exists an ASM program
asmtreeis linked into
The main theorem is equivalent to the claim in the paper.
In the paper, we claim that (§2.2):
For Level A, we aim to show that if we separately compile n different C modules (s1.c, ... , sn.c) using the same exact verified compiler C, producing n assembly modules (t1.asm, ... , tn.asm), then the assembly-level linking of the ti’s will refine the C-level linking of the si’s."
Note that we did not specify the order of the linkings among multiple modules.
In the development, we define only the linking of two modules, and used a tree data structure to specify the order of the linkings. For example, the following tree represents (m1 ◦ m2) ◦ m3:
◦ / \ ◦ m3 / \ m1 m2
Basically, the main theorem in the development proves the level A correctness, regardless of the order of the linkings.
levelB/: Level B compositional verification of CompCert (§2.3, §4.2).
The main theorem is
linker_correct_optd: similar to the level A correctness main theorem, but the C programs in
ctreeare separately compiled with possibly different optimization flags into the ASM programs in
The main theorem is equivalent to the claim in the paper, similarly to the level A correctness.
results.table.tex: Changes to lines of code when porting CompCert to SepCompCert LevelA and LevelB (§6, Fig. 10)
count_locs.pyis a script that counts differences between
level?/. The table in the paper (
results.table.tex) is automatically generated from this script.
We classify the changed lines into three categories: removed lines from the original CompCert 2.4 (Rm), added lines in our development which are derived from the original CompCert 2.4 (AddD), and added lines which are newly introduced in our development (AddN).
We classify the changed lines by the Unix
difftool. To further classify the added lines into two categories (AddD & AddN), we used the following criteria:
Added lines in the existing files are regarded as derived (AddD), except for those lines that begin with "(* new *)". Those lines are regarded as new (AddN).
Added lines in the newly created files are regarded as new (AddN), except for those lines that begin with "(* derived *)". Those lines are regarded as derived (AddD).
The only file that contains "(* derived *)" is
levelB/backend/RTLExtra.v. The contents are derived from the proofs of RTL optimizations, such as
We succeeded in compiling
levelB/directories with Coq 8.4pl5 for all Linux targets. You can reproduce it in the virtual machine with the following commands:
./configure arm-linux; make depend; make
./configure ia32-linux; make depend; make
./configure ppc-linux; make depend; make
In the virtual machine, you can run
build.shto build all architecture (
ppc) & directory (
We also succeeded in compiling our development in MAC OS X with:
./configure ia32-macosx; make depend; make
We recommend reviewers to use graphical diff tools, such as meld, for browsing our development. Meld is installed in the virtual machine.
Minor Technical Notes
- There are some files with a
.vpextension, which are turned by CompCert's preprocessor into generated
.vfiles. We have not touched these files, but in any case count the lines of code in the original
.vpfiles, not the generated