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

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

The CompCert verified C compiler

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