Compiler Structure

The Vélus compiler is implemented in a mix of Coq and OCaml. A program is parsed from a source file and successively transformed through several intermediate languages. The final transformation produces a Clight program for CompCert to compile into one of its supported assembly languages.

The syntax and semantics of the intermediate languages are specified in Coq. The transformations are specified as functional programs that manipulate syntactic terms. Each is accompanied by a correctness proof showing the preservation of input/output traces in the semantic models.

Compilation Passes

↓parsing
Source files are parsed into raw syntax trees that the elaboration pass annotates with types and clocks.
Untyped Lustre
↓elaboration
Lustre is a dataflow formalism with arbitrary nesting of nodes, fbys, merges, etcetera.
Lustre⤸
unnesting and distribution
expression initialization
↓transcription
Normalized Lustre (NLustre) is a dataflow formalism with three forms of equations: basic equations, fby equations, and node instances.
NLustre
↓i-translation
Synchronous Transition Code (Stc) is based on composing state transitions that constrain state and output values, relative to input values, at an instant.
Stc⤸scheduling
↓s-translation
Object code (Obc) is a simple imperative language with encapsulated state and a fixed execution order.
Obc⤸
fusion optimization
argument initialization
↓generation

The CompCert verified C compiler

The generation pass produces a Clight program for compilation by CompCert into assembly code.

Clight
↓(dashed)compilation
Assembly
↓printing
Vélus