Verified Separate Compilation for C
Report ID: TR-980-15Author: Stewart, Gordon
Date: 2015-04-08
Pages: 155
Download Formats: |PDF|
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 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 Comp- Cert, a verified separate compiler for C. As additional validation, the dissertation demonstrates the connection of Compositional CompCert to the Verifiable C program logic.