index.html 12.1 KB
Newer Older
1
2
3
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<HTML>
<HEAD>
xleroy's avatar
MAJ    
xleroy committed
4
<TITLE>The Compcert verified compiler</TITLE>
5
<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1">
xleroy's avatar
xleroy committed
6

7
8
9
10
11
12
<style type="text/css">
body {
  color: black; background: white;
  margin-left: 5%; margin-right: 5%;
}
h2 { margin-left: -5%;}
xleroy's avatar
xleroy committed
13
14
h3 { margin-left: -3%; }
h1,h2,h3 { font-family: sans-serif; }
15
16
17
18
19
20
hr { margin-left: -5%; margin-right:-5%; }
a:visited {color : #416DFF; text-decoration : none; font-weight : bold}
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>
xleroy's avatar
xleroy committed
21

22
23
24
</HEAD>
<BODY>

xleroy's avatar
MAJ    
xleroy committed
25
<H1 align="center">The Compcert verified compiler</H1>
26
<H2 align="center">Commented Coq development</H2>
xleroy's avatar
xleroy committed
27
<H3 align="center">Version 1.8, 2010-09-21</H3>
28
29
30

<H2>Introduction</H2>

xleroy's avatar
xleroy committed
31
32
<P>Compcert is a compiler that generates PowerPC, ARM and x86 assembly
code from Compcert C, a large subset of the C programming language.
33
34
35
36
37
38
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>

xleroy's avatar
MAJ    
xleroy committed
39
40
<P>High-level descriptions of the Compcert compiler and its proof of 
correctness can be found in the following papers (in increasing order of technical details):</P>
xleroy's avatar
xleroy committed
41
<UL>
xleroy's avatar
MAJ    
xleroy committed
42
<LI>Xavier Leroy, <A HREF="http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf">Formal verification of a realistic compiler</A>.  Communications of the ACM 52(7), July 2009.
xleroy's avatar
xleroy committed
43
44
45
46
<LI>Sandrine Blazy, Zaynah Dargaye and Xavier Leroy,
<A HREF="http://gallium.inria.fr/~xleroy/publi/cfront.pdf">Formal
verification of a C compiler front-end</A>. 
Proceedings of Formal Methods 2006, LNCS 4085.
xleroy's avatar
xleroy committed
47
48
<LI>Xavier Leroy, <A HREF="http://gallium.inria.fr/~xleroy/publi/compcert-backend.pdf">A formally verified compiler back-end</A>. 
Journal of Automated Reasoning 43(4):363-446, 2009.
xleroy's avatar
xleroy committed
49
</UL>
50
51
52
53

<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
xleroy's avatar
xleroy committed
54
55
work in progress; some parts have substantially changed since the
overview papers above were written.</P>
56

xleroy's avatar
xleroy committed
57
58
59
60
<P>The complete sources for Compcert can be downloaded from
<A HREF="http://compcert.inria.fr/">the Compcert Web site</A>.</P>

<P>This document and the Compcert sources are
xleroy's avatar
xleroy committed
61
copyright 2005, 2006, 2007, 2008, 2009, 2010 Institut National de Recherche en
xleroy's avatar
xleroy committed
62
63
64
Informatique et en Automatique (INRIA) and distributed under the terms
of the following <A HREF="LICENSE">license</A>.
</P>
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82

<H2>Table of contents</H2>

<H3>General-purpose libraries, data structures and algorithms</H3>

<UL>
<LI> <A HREF="html/Coqlib.html">Coqlib</A>: addendum to the Coq standard library.
<LI> <A HREF="html/Maps.html">Maps</A>: finite maps.
<LI> <A HREF="html/Integers.html">Integers</A>: machine integers.
<LI> <A HREF="html/Floats.html">Floats</A>: machine floating-point numbers.
<LI> <A HREF="html/Iteration.html">Iteration</A>: various forms of "while" loops.
<LI> <A HREF="html/Ordered.html">Ordered</A>: construction of
ordered types.
<LI> <A HREF="html/Lattice.html">Lattice</A>: construction of
semi-lattices.
<LI> <A HREF="html/Kildall.html">Kildall</A>: resolution of dataflow
inequations by fixpoint iteration.
<LI> <A HREF="html/Parmov.html">Parmov</A>: compilation of parallel assignments.
xleroy's avatar
xleroy committed
83
<LI> <A HREF="html/UnionFind.html">UnionFind</A>: a persistent union-find data structure.
84
85
</UL>

xleroy's avatar
xleroy committed
86
<H3>Definitions and theorems used in many parts of the development</H3>
87
88
89
90
91
92
93

<UL>
<LI> <A HREF="html/Errors.html">Errors</A>: the Error monad.
<LI> <A HREF="html/AST.html">AST</A>: identifiers, whole programs and other
common elements of abstract syntaxes.
<LI> <A HREF="html/Values.html">Values</A>: run-time values.
<LI> <A HREF="html/Events.html">Events</A>: observable events and traces.
xleroy's avatar
xleroy committed
94
95
96
<LI> <A HREF="html/Memtype.html">Memtype</A>: memory model (interface). <BR>
See also: <A HREF="html/Memory.html">Memory</A> (implementation of the memory model). <BR>
See also: <A HREF="html/Memdata.html">Memdata</A> (in-memory representation of data).
97
98
<LI> <A HREF="html/Globalenvs.html">Globalenvs</A>: global execution environments.
<LI> <A HREF="html/Smallstep.html">Smallstep</A>: tools for small-step semantics.
xleroy's avatar
xleroy committed
99
<LI> <A HREF="html/Determinism.html">Determinism</A>: determinism properties of small-step semantics.
100
101
102
103
104
105
106
<LI> <A HREF="html/Op.html">Op</A>: operators, addressing modes and their
semantics.
</UL>

<H3>Source, intermediate and target languages: syntax and semantics</H3>

<UL>
xleroy's avatar
xleroy committed
107
<LI> The Compcert C source language:
xleroy's avatar
xleroy committed
108
109
110
111
<A HREF="html/Csyntax.html">syntax</A> and
<A HREF="html/Csem.html">semantics</A> and
<A HREF="html/Cstrategy.html">determinized semantics</A>.
<LI> <A HREF="html/Clight.html">Clight</A>: a simpler version of Cmedium where expressions contain no side-effects.
xleroy's avatar
xleroy committed
112
113
<LI> <A HREF="html/Csharpminor.html">Csharpminor</A>: low-level
 structured language.
114
115
116
117
118
119
120
121
122
123
124
125
126
<LI> <A HREF="html/Cminor.html">Cminor</A>: low-level structured
language, with explicit stack allocation of certain local variables.
<LI> <A HREF="html/CminorSel.html">CminorSel</A>: like Cminor,
with machine-specific operators and addressing modes.
<LI> <A HREF="html/RTL.html">RTL</A>: register transfer language (3-address
code, control-flow graph, infinitely many pseudo-registers). <BR>
See also: <A HREF="html/Registers.html">Registers</A> (representation of
pseudo-registers).
<LI> <A HREF="html/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="html/Locations.html">Locations</A> (representation of
locations).
xleroy's avatar
xleroy committed
127
<LI> <A HREF="html/LTLin.html">LTLin</A>: like LTL, but the CFG is
128
129
130
131
132
133
134
replaced by a linear list of instructions with explicit branches and labels.
<LI> <A HREF="html/Linear.html">Linear</A>: like LTLin, with explicit
spilling, reloading and enforcement of calling conventions.
<LI> <A HREF="html/Mach.html">Mach</A>: like Linear, with a more concrete
view of the activation record.  <BR>
See also: <A HREF="html/Machabstr.html">Machabstr</A> abstract semantics for Mach. <BR>
See also: <A HREF="html/Machconcr.html">Machconcr</A> concrete semantics for Mach.
xleroy's avatar
MAJ    
xleroy committed
135
<LI> <A HREF="html/Asm.html">Asm</A>: abstract syntax for PowerPC assembly
136
137
138
139
140
141
142
143
144
145
146
147
148
code.
</UL>

<H3>Compiler passes</H3>

<TABLE cellpadding="5%">
<TR valign="top">
  <TH>Pass</TH>
  <TH>Source &amp; target</TH>
  <TH>Compiler&nbsp;code</TH>
  <TH>Correctness&nbsp;proof</TH>
</TR>

xleroy's avatar
xleroy committed
149
150
151
<TR valign="top">
  <TD>Pulling side-effects out of expressions;<br>
      fixing an evaluation order</TD>
xleroy's avatar
xleroy committed
152
  <TD>Compcert C to Clight</TD>
xleroy's avatar
xleroy committed
153
154
155
156
  <TD><A HREF="html/SimplExpr.html">SimplExpr</A></TD>
  <TD><A HREF="html/SimplExprspec.html">SimplExprspec</A><br>
      <A HREF="html/SimplExprproof.html">SimplExprproof</A></TD>
</TR>
xleroy's avatar
xleroy committed
157
158
159
160
161
<TR valign="top">
  <TD>Simplification of control structures; <br>
      explication of type-dependent computations</TD>
  <TD>Clight to Csharpminor</TD>
  <TD><A HREF="html/Cshmgen.html">Cshmgen</A></TD>
xleroy's avatar
xleroy committed
162
163
  <TD><A HREF="html/Cshmgenproof.html">Cshmgenproof</A></TD>
</TR>
164
<TR valign="top">
xleroy's avatar
xleroy committed
165
166
167
  <TD>Stack allocation of local variables<br>
      whose address is taken;<br>
      simplification of switch statements</TD>
168
169
170
171
172
173
174
175
  <TD>Csharpminor to Cminor</TD>
  <TD><A HREF="html/Cminorgen.html">Cminorgen</A></TD>
  <TD><A HREF="html/Cminorgenproof.html">Cminorgenproof</A></TD>
</TR>

<TR valign="top">
  <TD>Recognition of operators<br>and addressing modes</TD>
  <TD>Cminor to CminorSel</TD>
xleroy's avatar
xleroy committed
176
177
178
179
  <TD><A HREF="html/Selection.html">Selection</A><br>
      <A HREF="html/SelectOp.html">SelectOp</A></TD>
  <TD><A HREF="html/Selectionproof.html">Selectionproof</A><br>
      <A HREF="html/SelectOpproof.html">SelectOpproof</A></TD>
180
181
182
183
184
185
186
187
188
189
</TR>

<TR valign="top">
  <TD>Construction of the CFG, <br>3-address code generation</TD>
  <TD>Cminor to RTL</TD>
  <TD><A HREF="html/RTLgen.html">RTLgen</A></TD>
  <TD><A HREF="html/RTLgenspec.html">RTLgenspec</A><BR>
      <A HREF="html/RTLgenproof.html">RTLgenproof</A></TD>
</TR>

xleroy's avatar
xleroy committed
190
191
192
193
194
195
196
<TR valign="top">
  <TD>Recognition of tail calls</TD>
  <TD>RTL to RTL</TD>
  <TD><A HREF="html/Tailcall.html">Tailcall</A></TD>
  <TD><A HREF="html/Tailcallproof.html">Tailcallproof</A></TD>
</TR>

197
198
199
<TR valign="top">
  <TD>Constant propagation</TD>
  <TD>RTL to RTL</TD>
xleroy's avatar
xleroy committed
200
201
202
203
  <TD><A HREF="html/Constprop.html">Constprop</A><br>
      <A HREF="html/ConstpropOp.html">ConstpropOp</A></TD>
  <TD><A HREF="html/Constpropproof.html">Constpropproof</A><br>
      <A HREF="html/ConstpropOpproof.html">ConstproppOproof</A></TD>
204
205
206
207
208
209
210
211
212
</TR>

<TR valign="top">
  <TD>Common subexpression elimination</TD>
  <TD>RTL to RTL</TD>
  <TD><A HREF="html/CSE.html">CSE</A></TD>
  <TD><A HREF="html/CSEproof.html">CSEproof</A></TD>
</TR>

xleroy's avatar
xleroy committed
213
214
215
216
217
218
219
<TR valign="top">
  <TD>Elimination of redundant casts</TD>
  <TD>RTL to RTL</TD>
  <TD><A HREF="html/CastOptim.html">CastOptim</A></TD>
  <TD><A HREF="html/CastOptimproof.html">CastOptimproof</A></TD>
</TR>

220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
<TR valign="top">
  <TD>Register allocation by coloring<br>of an interference graph</TD>
  <TD>RTL to LTL</TD>
  <TD><A HREF="html/InterfGraph.html">InterfGraph</A><BR>
      <A HREF="html/Coloring.html">Coloring</A><BR>
      <A HREF="html/Allocation.html">Allocation</A></TD>
  <TD><BR>
      <A HREF="html/Coloringproof.html">Coloringproof</A><BR>
      <A HREF="html/Allocproof.html">Allocproof</A></TD>
</TR>

<TR valign="top">
  <TD>Branch tunneling</TD>
  <TD>LTL to LTL</TD>
  <TD><A HREF="html/Tunneling.html">Tunneling</A></TD>
  <TD><A HREF="html/Tunnelingproof.html">Tunnelingproof</A></TD>
</TR>

<TR valign="top">
  <TD>Linearization of the CFG</TD>
  <TD>LTL to LTLin</TD>
  <TD><A HREF="html/Linearize.html">Linearize</A></TD>
  <TD><A HREF="html/Linearizeproof.html">Linearizeproof</A></TD>
</TR>

<TR valign="top">
  <TD>Spilling, reloading, calling conventions</TD>
  <TD>LTLin to Linear</TD>
  <TD><A HREF="html/Conventions.html">Conventions</A><BR>
      <A HREF="html/Reload.html">Reload</A></TD>
  <TD><A HREF="html/Parallelmove.html">Parallelmove</A><BR>
      <A HREF="html/Reloadproof.html">Reloadproof</A></TD>
</TR>

<TR valign="top">
  <TD>Laying out the activation records</TD>
  <TD>Linear to Mach</TD>
  <TD><A HREF="html/Bounds.html">Bounds</A><BR>
      <A HREF="html/Stacking.html">Stacking</A></TD>
  <TD><A HREF="html/Stackingproof.html">Stackingproof</A></TD>
</TR>

<TR valign="top">
  <TD>Storing the activation records in memory</TD>
  <TD>Mach to Mach</TD>
  <TD>(none)
xleroy's avatar
MAJ    
xleroy committed
266
  <TD><A HREF="html/Asmgenretaddr.html">Asmgenretaddr</A><BR>
xleroy's avatar
MAJ    
xleroy committed
267
      <A HREF="html/Machabstr2concr.html">Machabstr2concr</A></TD>
268
269

<TR valign="top">
xleroy's avatar
MAJ    
xleroy committed
270
271
272
273
274
  <TD>Emission of assembly code</TD>
  <TD>Mach to Asm</TD>
  <TD><A HREF="html/Asmgen.html">Asmgen</A></TD>
  <TD><A HREF="html/Asmgenproof1.html">Asmgenproof1</A><BR>
      <A HREF="html/Asmgenproof.html">Asmgenproof</A></TD>
275
276
277
278
279
280
</TR>
</TABLE>

<H3>Type systems</H3>

Trivial type systems are used to statically capture well-formedness
xleroy's avatar
xleroy committed
281
conditions on the source and intermediate languages.
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
<UL>
<LI> <A HREF="html/RTLtyping.html">RTLtyping</A>: typing for RTL + type
reconstruction.
<LI> <A HREF="html/LTLtyping.html">LTLtyping</A>: typing for LTL.
<LI> <A HREF="html/LTLintyping.html">LTLintyping</A>: typing for LTLin.
<LI> <A HREF="html/Lineartyping.html">Lineartyping</A>: typing for Linear.
<LI> <A HREF="html/Machtyping.html">Machtyping</A>: typing for Mach.
</UL>
Proofs that compiler passes are type-preserving:
<UL>
<LI> <A HREF="html/Alloctyping.html">Alloctyping</A> (register allocation).
<LI> <A HREF="html/Tunnelingtyping.html">Tunnelingtyping</A> (branch tunneling).
<LI> <A HREF="html/Linearizetyping.html">Linearizetyping</A> (code linearization).
<LI> <A HREF="html/Reloadtyping.html">Reloadtyping</A> (spilling and reloading).
<LI> <A HREF="html/Stackingtyping.html">Stackingtyping</A> (layout of activation records).
</UL>

<H3>All together</H3>

<UL>
xleroy's avatar
xleroy committed
302
303
<LI> <A HREF="html/Compiler.html">Compiler</A>: composing the passes together;
whole-compiler semantic preservation theorems.
304
<LI> <A HREF="html/Complements.html">Complements</A>: interesting consequences of the semantic preservation theorems.
305
306
307
308
309
310
311
312
</UL>

<HR>
<ADDRESS>Xavier.Leroy@inria.fr</ADDRESS>
<HR>

</BODY>
</HTML>