Compositional CompCert

Overview

Compositional CompCert is a respecification and proof of CompCert 2.1 (http://compcert.inria.fr/) to support compositional separate compilation.

The files are distributed as a modification of standard CompCert 2.1: The compiler files are the same but there are two sets of proofs, one for standard CompCert and the second for Compositional CompCert. Both sets of proofs are buildable.

In general, files suffixed *_coop.v and *_eff.v are the compositional variants of standard CompCert intermediate language semantics (*_coop.v is the base interaction semantics of a given IL; *_eff.v is the effectful version). Files suffixed *_comp.v, for "compositional," are the compositional variants of the standard CompCert proofs. The compositional proofs can typically be found in the same directory as their standard CompCert counterparts.

Build

Compositional CompCert builds under:

• Coq 8.4pl4 (http://coq.inria.fr/),
• Ssreflect 1.5 (http://ssr.msr-inria.inria.fr/), and
• MathComp 1.5 (http://ssr.msr-inria.inria.fr/).

If you do not have Ssreflect+MathComp, you should be able to build everything but the files in the linking/ subdirectory (horizontal composition/proofs) but we make no guarantees.

To build, clone the repository, go to the root directory, and type:

  ./configure ia32-linux
  make

To install the ccomp binary and runtime libraries system-wide, type make install as root.

Using Custom Ssreflect Installation

If your Ssreflect or MathComp are installed in a nonstandard place (e.g., in your home directory rather than system-wide), edit variables SSREFLECT and MATHCOMP in the Makefile to point to the appropriate installation directories. Otherwise, leave both SSREFLECT and MATHCOMP equal the empty string "".

Files

An HTML rendering of the code is browsable at:

http://www.cs.princeton.edu/~jsseven/papers/compcomp/html.

In the cfrontend/ and backend/ directories, source and target language definitions used in each phase are generally suffixed *_eff.v (often importing files suffixed *_coop.v). The compositional compiler correctness proofs are suffixed *_comp.v, to distinguish from the standard CompCert proofs.

Toplevel Files

• driver/CompositionalCompiler.v

  Proves Theorem 3 (Section 6).

• linking/CompositionalComplements.v

  Proves Corollary 2 (Section 6).

cfrontend/

C frontend compiler phases and proofs:

• SimplLocals
  • Compiler Phase
  • Compositional Correctness
• Cshmgen
  • Compiler Phase
  • Compositional Correctness
• Cminorgen
  • Compiler Phase
  • Compositional Correctness

backend/

Backend compiler phases and proofs:

• Selection
  • Compiler Phase
  • Compositional Correctness
• RTLgen
  • Compiler Phase
  • Compositional Correctness
• Tailcall
  • Compiler Phase
  • Compositional Correctness
• Renumbering
  • Compiler Phase
  • Compositional Correctness
• Allocation
  • Compiler Phase
  • Compositional Correctness
• Tunneling
  • Compiler Phase
  • Compositional Correctness
• Linearize
  • Compiler Phase
  • Compositional Correctness
• CleanupLabels
  • Compiler Phase
  • Compositional Correctness
• Stacking
  • Compiler Phase
  • Compositional Correctness
• Asmgen
  • Compiler Phase
  • Compositional Correctness

Proof that CompCert IA32 Asm is a "nucular" semantics:

• Asm_nucular.v

Intermediate Language Semantics

Interaction Semantics of the intermediate languages used in Compositional CompCert.

• Clight
  • Interaction Semantics
  • Effectful Interaction Semantics
• Csharpminor
  • Interaction Semantics
  • Effectful Interaction Semantics
• Cminor
  • Interaction Semantics
  • Effectful Interaction Semantics
• CminorSel
  • Interaction Semantics
  • Effectful Interaction Semantics
• RTL
  • Interaction Semantics
  • Effectful Interaction Semantics
• LTL
  • Interaction Semantics
  • Effectful Interaction Semantics
• Linear
  • Interaction Semantics
  • Effectful Interaction Semantics
• Mach
  • Interaction Semantics
  • Effectful Interaction Semantics
• IA32 Asm
  • Interaction Semantics
  • Effectful Interaction Semantics

core/

• semantics.v

  Defines Interaction Semantics (Section 2).

• structured_injections.v

  Defines Structured Injections (Section 4).

• simulations.v

  Defines Structured Simulations (Section 4). Concordance for this file:

  • replace_locals is the function named export in the paper.
  • replace_externs is the function named import in the paper.

• simulations_lemmas.v

  Various derived structured simulations, specialized for particular use cases.

• simulations_trans.v

  Proves Theorem 1 (Section 5), that simulations compose vertically. The main subproofs are:

  • internal_diagram_trans.v proves transitivity of the internal step diagram.
  • interpolation_II.v proves the interpolation lemma required to prove transitivity of the external step diagram.

• closed_simulations.v

  Defines a variant of simulations suitable for closed programs.

• closed_simulations_lemmas.v

  Corollaries of closed program simulation.

• reach.v

  Defines the reach-closure operation used in Structured Simulations and Reach-Closed Semantics.

• relyguarantee_lemmas.v

  Proves a number of rely-guarantee compatibility lemmas used in the linking proof.

• nucular_semantics.v

  A notion of Interaction Semantics that never store invalid pointers in memory. Why "nucular"? We call the memory invariant that is preserved by such semantics the "WMD" condition, as defined in file mem_welldefined.v.

linking/

• compcert_linking.v

  Defines Linking Semantics (Section 3). The linking semantics (\mathcal{L}) is defined twice: First as a function (to Prop), and then as an inductive relation. The two versions are proved to coincide.

• compcert_linking_lemmas.v

  A few lemmas on linking semantics.

• linking_spec.v

  States Theorem 2 (Section 5).

• linking_inv.v

  States the main linking simulation invariant, used to prove Theorem 2. Subsidiary files include: linking/disjointness.v.

• linking_proof.v

  Proves Theorem 2 (Section 5). The two main subproofs (for the call and return cases, respectively) are:

  • linking/call_lemmas.v
  • linking/ret_lemmas.v

• rc_semantics.v

  Defines Reach-Closed Semantics (Section 5). The definition has been weakened slightly since the POPL submission, to facilitate the proof, in linking/safe_clight_rc.v, that all safe Clight programs are RC.

• rc_semantics_lemmas.v

  Lemmas on Reach-Closed Semantics.

• safe_clight_rc.v

  Proves that all safe Clight programs are RC (a new theorem not in the paper). This is a slightly counterintuitive result that relies on the fact that safe Clight programs cannot fabricate pointers (recall that even in C, casting integers to pointers is only implementation-defined).

• context_equiv.v

  Defines Reach-Closed Contextual Equivalence and proves Corollary 1 (Section 5).

• gallina_coresem.v

  Demonstrates one way in which to construct an interaction semantics that is just a mathematical relation in Gallina.

• reach_lemmas.v

  Lemmas concerning reachability.

• wf_lemmas.v

  Lemmas about well-founded orders.