Verified Separate Compilation for C

Abstract

A separate compiler independently translates a program's components in

a way that preserves correctness of the program as a whole. This

dissertation develops techniques and tools for verified (mechanically

proved) separate compilation of programs in C.

Specifying and proving separate compilation for C is made challenging

by the coincidence of: compiler optimizations, such as register

spilling, that introduce compiler-managed (private) memory regions

into function stack frames, and C's stack-allocated addressable local

variables, which may \emph{leak} portions of stack frames to other

modules when their addresses are passed as arguments to external

function calls. The CompCert compiler, as built/proved by Leroy

et al. 2006--2015 and upon which this dissertation builds, has proofs

of correctness for whole programs, but its simulation relations are

too weak to specify or prove separately compiled modules.

The main contributions of the dissertation are:

(i) language-independent linking, a new operational model of multilanguage

module interaction that supports the statement and proof of

cross-language contextual equivalence;

(ii) structured simulations, a

program-equivalence proof method that enables expressive module-local

invariants on the state communicated between compilation units at

runtime;

(iii) the application of the above techniques to

Compositional CompCert, a verified separate compiler for C.

As additional validation, the dissertation demonstrates the connection

of Compositional CompCert to the Verifiable C program logic.