From 44cfa794dabe701959624c5cf2f0760c5827ccc0 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 9 Feb 2006 15:21:12 +0000 Subject: MAJ fichier ppal git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@3 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- doc/compcert.html | 250 ------------------------------------------------------ 1 file changed, 250 deletions(-) delete mode 100644 doc/compcert.html (limited to 'doc/compcert.html') diff --git a/doc/compcert.html b/doc/compcert.html deleted file mode 100644 index c778632d..00000000 --- a/doc/compcert.html +++ /dev/null @@ -1,250 +0,0 @@ - - - -The Compcert certified compiler back-end - - - - - - - - -

The Compcert certified compiler back-end

-

Commented Coq development

-

Version 0.2, 2006-01-07

- -

Introduction

- -

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.

- -

A high-level overview of the Compcert back-end and its proof of -correctness can be found in the following paper:

-Xavier Leroy, Formal -certification of a compiler back-end, or: programming a compiler with -a proof assistant. Proceedings of the POPL 2006 symposium. - -

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.

- -

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 GNU General Public -License version 2.

- -

Table of contents

- -

Libraries, algorithms, data structures

- - - -

Source, intermediate and target languages: syntax and semantics

- - - -

Compiler passes

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
PassSource & targetCompiler codeCorrectness proof
Recognition of operators and addressing modesCsharpminor to CminorCmconstrCmconstrproof
Stack allocation of local variables
whose address is taken		Csharpminor to CminorCminorgenCminorgenproof
Construction of the CFG,
3-address code generation		Cminor to RTLRTLgenRTLgenproof1
- RTLgenproof
Constant propagationRTL to RTLConstpropConstpropproof
Common subexpression eliminationRTL to RTLCSECSEproof
Register allocation by coloring
of an interference graph		RTL to LTLConventions
- InterfGraph
- Coloring
- Parallelmove
- Allocation
-
- Coloringproof
- Allocproof_aux
- Allocproof
Branch tunnelingLTL to LTLTunnelingTunnelingproof
Linearization of the CFGLTL to LinearLinearizeLinearizeproof
Laying out the activation recordsLinear to MachStackingStackingproof
Storing the activation records in memoryMach to Mach(none) - Machabstr2mach
Emission of PowerPC assemblyMach to PPCPPCgenPPCgenproof1
- PPCgenproof
- -

Type systems

- -Trivial type systems are used to statically capture well-formedness -conditions on the intermediate languages. - -Proofs that compiler passes are type-preserving: - - -

All together

- - - -
-
Xavier.Leroy@inria.fr
-
- - - -- cgit