diff options
Diffstat (limited to 'doc/backend.html')
| -rw-r--r-- | doc/backend.html | 250 |
1 files changed, 0 insertions, 250 deletions
diff --git a/doc/backend.html b/doc/backend.html deleted file mode 100644 index e33896c..0000000 --- a/doc/backend.html +++ /dev/null @@ -1,250 +0,0 @@ -<!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="lib.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="lib.Maps.html">Maps</A>: finite maps. - (Coq source file with proofs: - <A HREF="Maps.v"><code>Maps.v</code></a>.) -<LI> <A HREF="lib.Sets.html">Sets</A>: finite sets. -<LI> <A HREF="lib.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="lib.Inclusion.html">Inclusion</A>: tactics to prove list inclusions. -<LI> <A HREF="backend.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="lib.Integers.html">Integers</A>: machine integers. - (Coq source file with proofs: - <A HREF="Integers.v"><code>Integers.v</code></a>.) -<LI> <A HREF="lib.Floats.html">Floats</A>: machine floating-point numbers. -<LI> <A HREF="backend.Mem.html">Mem</A>: the memory model. -<LI> <A HREF="backend.Globalenvs.html">Globalenvs</A>: global execution environments. -<LI> <A HREF="backend.Op.html">Op</A>: operators, addressing modes and their -semantics. -<LI> <A HREF="lib.Ordered.html">Ordered</A>: construction of -ordered types. -<LI> <A HREF="lib.Lattice.html">Lattice</A>: construction of -semi-lattices. -<LI> <A HREF="backend.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="backend.Csharpminor.html">Csharpminor</A>: low-level structured language. -<LI> <A HREF="backend.Cminor.html">Cminor</A>: low-level structured -language, with explicit stack allocation of certain local variables. -<LI> <A HREF="backend.RTL.html">RTL</A>: register transfer language (3-address -code, control-flow graph, infinitely many pseudo-registers). <BR> -See also: <A HREF="backend.Registers.html">Registers</A> (representation of -pseudo-registers). -<LI> <A HREF="backend.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="backend.Locations.html">Locations</A> (representation of -locations). -<LI> <A HREF="backend.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="backend.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="backend.Machabstr.html">Machabstr</A>. <BR> -<LI> <A HREF="backend.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="backend.Cmconstr.html">Cmconstr</A></TD> - <TD><A HREF="backend.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="backend.Cminorgen.html">Cminorgen</A></TD> - <TD><A HREF="backend.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="backend.RTLgen.html">RTLgen</A></TD> - <TD><A HREF="backend.RTLgenproof1.html">RTLgenproof1</A><BR> - <A HREF="backend.RTLgenproof.html">RTLgenproof</A></TD> -</TR> - -<TR valign="top"> - <TD>Constant propagation</TD> - <TD>RTL to RTL</TD> - <TD><A HREF="backend.Constprop.html">Constprop</A></TD> - <TD><A HREF="backend.Constpropproof.html">Constpropproof</A></TD> -</TR> - -<TR valign="top"> - <TD>Common subexpression elimination</TD> - <TD>RTL to RTL</TD> - <TD><A HREF="backend.CSE.html">CSE</A></TD> - <TD><A HREF="backend.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="backend.Conventions.html">Conventions</A><BR> - <A HREF="backend.InterfGraph.html">InterfGraph</A><BR> - <A HREF="backend.Coloring.html">Coloring</A><BR> - <A HREF="backend.Parallelmove.html">Parallelmove</A><BR> - <A HREF="backend.Allocation.html">Allocation</A></TD> - <TD><BR> - <BR> - <A HREF="backend.Coloringproof.html">Coloringproof</A><BR> - <A HREF="backend.Allocproof_aux.html">Allocproof_aux</A><BR> - <A HREF="backend.Allocproof.html">Allocproof</A></TD> -</TR> - -<TR valign="top"> - <TD>Branch tunneling</TD> - <TD>LTL to LTL</TD> - <TD><A HREF="backend.Tunneling.html">Tunneling</A></TD> - <TD><A HREF="backend.Tunnelingproof.html">Tunnelingproof</A></TD> -</TR> - -<TR valign="top"> - <TD>Linearization of the CFG</TD> - <TD>LTL to Linear</TD> - <TD><A HREF="backend.Linearize.html">Linearize</A></TD> - <TD><A HREF="backend.Linearizeproof.html">Linearizeproof</A></TD> -</TR> - -<TR valign="top"> - <TD>Laying out the activation records</TD> - <TD>Linear to Mach</TD> - <TD><A HREF="backend.Stacking.html">Stacking</A></TD> - <TD><A HREF="backend.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="backend.Machabstr2mach.html">Machabstr2mach</A></TD> - -<TR valign="top"> - <TD>Emission of PowerPC assembly</TD> - <TD>Mach to PPC</TD> - <TD><A HREF="backend.PPCgen.html">PPCgen</A></TD> - <TD><A HREF="backend.PPCgenproof1.html">PPCgenproof1</A><BR> - <A HREF="backend.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="backend.RTLtyping.html">RTLtyping</A>: typing for RTL + type -reconstruction. -<LI> <A HREF="backend.LTLtyping.html">LTLtyping</A>: typing for LTL. -<LI> <A HREF="backend.Lineartyping.html">Lineartyping</A>: typing for Linear. -<LI> <A HREF="backend.Machtyping.html">Machtyping</A>: typing for Mach. -</UL> -Proofs that compiler passes are type-preserving: -<UL> -<LI> <A HREF="backend.Alloctyping_aux.html">Alloctyping_aux</A> and - <A HREF="backend.Alloctyping.html">Alloctyping</A> (register allocation). -<LI> <A HREF="backend.Tunnelingtyping.html">Tunnelingtyping</A> (branch tunneling). -<LI> <A HREF="backend.Lineartyping.html">Lineartyping</A> (branch tunneling). -<LI> <A HREF="backend.Stackingtyping.html">Stackingtyping</A> (layout of activation records). -</UL> - -<H3>All together</H3> - -<UL> -<LI> <A HREF="backend.Main.html">Main</A>: composing the passes together; the -final semantic preservation theorems. -</UL> - -<HR> -<ADDRESS>Xavier.Leroy@inria.fr</ADDRESS> -<HR> - -</BODY> -</HTML> |