diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-02-09 14:55:48 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-02-09 14:55:48 +0000 |
commit | 2ae43be7b9d4118335c9d2cef6e098f9b9f807fe (patch) | |
tree | bbb5e49ccbf7e3614966571acc317f8d318fecad /doc/compcert.html | |
download | compcert-2ae43be7b9d4118335c9d2cef6e098f9b9f807fe.tar.gz compcert-2ae43be7b9d4118335c9d2cef6e098f9b9f807fe.zip |
Initial import of compcert
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'doc/compcert.html')
-rw-r--r-- | doc/compcert.html | 250 |
1 files changed, 250 insertions, 0 deletions
diff --git a/doc/compcert.html b/doc/compcert.html new file mode 100644 index 00000000..c778632d --- /dev/null +++ b/doc/compcert.html @@ -0,0 +1,250 @@ +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"> +<HTML> +<HEAD> +<TITLE>The Compcert certified compiler back-end</TITLE> +<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1"> + +<style type="text/css"> +body { + color: black; background: white; + margin-left: 5%; margin-right: 5%; +} +h2 { margin-left: -5%;} +h3,h4,h5,h6 { margin-left: -3%; } +hr { margin-left: -5%; margin-right:-5%; } +a:visited {color : #416DFF; text-decoration : none; } +a:link {color : #416DFF; text-decoration : none; font-weight : bold} +a:hover {color : Red; text-decoration : underline; } +a:active {color : Red; text-decoration : underline; } +</style> + +<LINK type="text/css" rel="stylesheet" href="style.css"> +</HEAD> +<BODY> + +<H1 align="center">The Compcert certified compiler back-end</H1> +<H2 align="center">Commented Coq development</H2> +<H3 align="center">Version 0.2, 2006-01-07</H3> + +<H2>Introduction</H2> + +<P>The Compcert back-end is a compiler that generates PowerPC assembly +code from a low-level intermediate language called Cminor and a +slightly more expressive intermediate language called Csharpminor. +The particularity of this compiler is that it is written mostly within +the specification language of the Coq proof assistant, and its +correctness --- the fact that the generated assembly code is +semantically equivalent to its source program --- was entirely proved +within the Coq proof assistant.</P> + +<P>A high-level overview of the Compcert back-end and its proof of +correctness can be found in the following paper:</P> +<CITE>Xavier Leroy, <A +HREF="http://pauillac.inria.fr/~xleroy/publi/compiler-certif.pdf">Formal +certification of a compiler back-end, or: programming a compiler with +a proof assistant</A>. Proceedings of the POPL 2006 symposium.</CITE> + +<P>This Web site gives a commented listing of the underlying Coq +specifications and proofs. Proof scripts and the parts of the +compiler written directly in Caml are omitted. This development is a +work in progress; some parts may have changed since the overview paper +above was written.</P> + +<P>This document and all Coq source files referenced from it are +copyright 2005, 2006 Institut National de Recherche en Informatique et +en Automatique (INRIA) and distributed under the terms of the <A +HREF="http://www.gnu.org/licenses/gpl.html">GNU General Public +License</A> version 2.</P> + +<H2>Table of contents</H2> + +<H3>Libraries, algorithms, data structures</H3> + +<UL> +<LI> <A HREF="Coqlib.html">Coqlib</A>: addendum to the Coq standard library. + (Coq source file with proofs: + <A HREF="Coqlib.v"><code>Coqlib.v</code></a>.) +<LI> <A HREF="Maps.html">Maps</A>: finite maps. + (Coq source file with proofs: + <A HREF="Maps.v"><code>Maps.v</code></a>.) +<LI> <A HREF="Sets.html">Sets</A>: finite sets. +<LI> <A HREF="union_find.html">Union-find</A>: representation of +equivalence classes. + (Coq source file with proofs: + <A HREF="union_find.v"><code>union_find.v</code></a>.) +<LI> <A HREF="Inclusion.html">Inclusion</A>: tactics to prove list inclusions. +<LI> <A HREF="AST.html">AST</A>: identifiers, whole programs and other +common elements of abstract syntaxes. + (Coq source file with proofs: + <A HREF="AST.v"><code>AST.v</code></a>.) +<LI> <A HREF="Integers.html">Integers</A>: machine integers. + (Coq source file with proofs: + <A HREF="Integers.v"><code>Integers.v</code></a>.) +<LI> <A HREF="Floats.html">Floats</A>: machine floating-point numbers. +<LI> <A HREF="Mem.html">Mem</A>: the memory model. +<LI> <A HREF="Globalenvs.html">Globalenvs</A>: global execution environments. +<LI> <A HREF="Op.html">Op</A>: operators, addressing modes and their +semantics. +<LI> <A HREF="Ordered.html">Ordered</A>: construction of +ordered types. +<LI> <A HREF="Lattice.html">Lattice</A>: construction of +semi-lattices. +<LI> <A HREF="Kildall.html">Kildall</A>: resolution of dataflow +inequations by fixpoint iteration. +</UL> + +<H3>Source, intermediate and target languages: syntax and semantics</H3> + +<UL> +<LI> <A HREF="Csharpminor.html">Csharpminor</A>: low-level structured language. +<LI> <A HREF="Cminor.html">Cminor</A>: low-level structured +language, with explicit stack allocation of certain local variables. +<LI> <A HREF="RTL.html">RTL</A>: register transfer language (3-address +code, control-flow graph, infinitely many pseudo-registers). <BR> +See also: <A HREF="Registers.html">Registers</A> (representation of +pseudo-registers). +<LI> <A HREF="LTL.html">LTL</A>: location transfer language (3-address +code, control-flow graph, finitely many physical registers, infinitely +many stack slots). <BR> +See also: <A HREF="Locations.html">Locations</A> (representation of +locations). +<LI> <A HREF="Linear.html">Linear</A>: like LTL, but the CFG is +replaced by a linear list of instructions with explicit branches and labels. +<LI> <A HREF="Mach.html">Mach</A>: like Linear, with a more concrete +view of the activation record. <BR> +See also: an alternate semantics for the same +syntax is given in <A HREF="Machabstr.html">Machabstr</A>. <BR> +<LI> <A HREF="PPC.html">PPC</A>: abstract syntax for PowerPC assembly +code. +</UL> + +<H3>Compiler passes</H3> + +<TABLE cellpadding="5%"> +<TR valign="top"> + <TH>Pass</TH> + <TH>Source & target</TH> + <TH>Compiler code</TH> + <TH>Correctness proof</TH> +</TR> + +<TR valign="top"> + <TD>Recognition of operators and addressing modes</TD> + <TD>Csharpminor to Cminor</TD> + <TD><A HREF="Cmconstr.html">Cmconstr</A></TD> + <TD><A HREF="Cmconstrproof.html">Cmconstrproof</A></TD> +</TR> + +<TR valign="top"> + <TD>Stack allocation of local variables<br>whose address is taken</TD> + <TD>Csharpminor to Cminor</TD> + <TD><A HREF="Cminorgen.html">Cminorgen</A></TD> + <TD><A HREF="Cminorgenproof.html">Cminorgenproof</A></TD> +</TR> + +<TR valign="top"> + <TD>Construction of the CFG, <br>3-address code generation</TD> + <TD>Cminor to RTL</TD> + <TD><A HREF="RTLgen.html">RTLgen</A></TD> + <TD><A HREF="RTLgenproof1.html">RTLgenproof1</A><BR> + <A HREF="RTLgenproof.html">RTLgenproof</A></TD> +</TR> + +<TR valign="top"> + <TD>Constant propagation</TD> + <TD>RTL to RTL</TD> + <TD><A HREF="Constprop.html">Constprop</A></TD> + <TD><A HREF="Constpropproof.html">Constpropproof</A></TD> +</TR> + +<TR valign="top"> + <TD>Common subexpression elimination</TD> + <TD>RTL to RTL</TD> + <TD><A HREF="CSE.html">CSE</A></TD> + <TD><A HREF="CSEproof.html">CSEproof</A></TD> +</TR> + +<TR valign="top"> + <TD>Register allocation by coloring<br>of an interference graph</TD> + <TD>RTL to LTL</TD> + <TD><A HREF="Conventions.html">Conventions</A><BR> + <A HREF="InterfGraph.html">InterfGraph</A><BR> + <A HREF="Coloring.html">Coloring</A><BR> + <A HREF="Parallelmove.html">Parallelmove</A><BR> + <A HREF="Allocation.html">Allocation</A></TD> + <TD><BR> + <BR> + <A HREF="Coloringproof.html">Coloringproof</A><BR> + <A HREF="Allocproof_aux.html">Allocproof_aux</A><BR> + <A HREF="Allocproof.html">Allocproof</A></TD> +</TR> + +<TR valign="top"> + <TD>Branch tunneling</TD> + <TD>LTL to LTL</TD> + <TD><A HREF="Tunneling.html">Tunneling</A></TD> + <TD><A HREF="Tunnelingproof.html">Tunnelingproof</A></TD> +</TR> + +<TR valign="top"> + <TD>Linearization of the CFG</TD> + <TD>LTL to Linear</TD> + <TD><A HREF="Linearize.html">Linearize</A></TD> + <TD><A HREF="Linearizeproof.html">Linearizeproof</A></TD> +</TR> + +<TR valign="top"> + <TD>Laying out the activation records</TD> + <TD>Linear to Mach</TD> + <TD><A HREF="Stacking.html">Stacking</A></TD> + <TD><A HREF="Stackingroof.html">Stackingproof</A></TD> +</TR> + +<TR valign="top"> + <TD>Storing the activation records in memory</TD> + <TD>Mach to Mach</TD> + <TD>(none) + <TD><A HREF="Machabstr2mach.html">Machabstr2mach</A></TD> + +<TR valign="top"> + <TD>Emission of PowerPC assembly</TD> + <TD>Mach to PPC</TD> + <TD><A HREF="PPCgen.html">PPCgen</A></TD> + <TD><A HREF="PPCgenproof1.html">PPCgenproof1</A><BR> + <A HREF="PPCgenproof.html">PPCgenproof</A></TD> +</TR> +</TABLE> + +<H3>Type systems</H3> + +Trivial type systems are used to statically capture well-formedness +conditions on the intermediate languages. +<UL> +<LI> <A HREF="RTLtyping.html">RTLtyping</A>: typing for RTL + type +reconstruction. +<LI> <A HREF="LTLtyping.html">LTLtyping</A>: typing for LTL. +<LI> <A HREF="Lineartyping.html">Lineartyping</A>: typing for Linear. +<LI> <A HREF="Machtyping.html">Machtyping</A>: typing for Mach. +</UL> +Proofs that compiler passes are type-preserving: +<UL> +<LI> <A HREF="Alloctyping_aux.html">Alloctyping_aux</A> and + <A HREF="Alloctyping.html">Alloctyping</A> (register allocation). +<LI> <A HREF="Tunnelingtyping.html">Tunnelingtyping</A> (branch tunneling). +<LI> <A HREF="Lineartyping.html">Lineartyping</A> (branch tunneling). +<LI> <A HREF="Stackingtyping.html">Stackingtyping</A> (layout of activation records). +</UL> + +<H3>All together</H3> + +<UL> +<LI> <A HREF="Main.html">Main</A>: composing the passes together; the +final semantic preservation theorems. +</UL> + +<HR> +<ADDRESS>Xavier.Leroy@inria.fr</ADDRESS> +<HR> + +</BODY> +</HTML> |