Lightweight Verification of Separate Compilation

Jeehoon Kang*, Yoonseung Kim*, Chung-Kil Hur*, Derek Dreyer**, Viktor Vafeiadis**
Seoul National University & ** MPI-SWS


Our technique has been applied to CompCert 2.7!
Here is a quote from the change log:

Release 2.7, 2016-06-29

Major improvement:
- The proof of semantic preservation now accounts for separate compilation
  and linking, following the approach of Kang, Kim, Hur, Dreyer and
  Vafeiadis, "Lightweight verification of separate compilation", POPL 2016.
  Namely, the proof considers a set of C compilation units, separately
  compiled to assembly then linked, and shows that the resulting
  assembly program preserves the semantics of the C program that would
  be obtained by syntactic linking of the source C compilation units.

Project Description

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 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.