From 43c67c98877feeb2e91cb4be3835e70834379d5a Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Tue, 3 Sep 2019 15:50:17 +0200 Subject: a dedicated entry-point to the doc of Coq sources --- doc/index-mppa_k1c.html | 380 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 380 insertions(+) create mode 100644 doc/index-mppa_k1c.html (limited to 'doc') diff --git a/doc/index-mppa_k1c.html b/doc/index-mppa_k1c.html new file mode 100644 index 00000000..41a44a0d --- /dev/null +++ b/doc/index-mppa_k1c.html @@ -0,0 +1,380 @@ + + + +The CompCert verified compiler + + + + + + + +

The CompCert verified compiler

+

Commented Coq development

+

Version 3.5, 2019-02-27

+

PATCHED FOR MPPA-K1C

+ +

Introduction

+ +

CompCert is a compiler that generates PowerPC, ARM, RISC-V and x86 assembly +code from CompCert C, a large subset of the C programming language. +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.

+ +

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):

+ + +

This Web site gives a commented listing of the underlying Coq +specifications and proofs. Proof scripts are folded by default, but +can be viewed by clicking on "Proof". Some modules (written in italics below) differ between the four target architectures. The +PowerPC versions of these modules are shown below; the ARM, x86 and RISC-V +versions can be found in the source distribution. +

+ +

This development is a work in progress; some parts have +substantially changed since the overview papers above were +written.

+ +

The complete sources for CompCert can be downloaded from +the CompCert Web site.

+ +

This document and the CompCert sources are copyright Institut +National de Recherche en Informatique et en Automatique (INRIA) and +AbsInt Angewandte Informatik GmbH, and are distributed under the terms of the +following license. +

+ +

Table of contents

+ +

General-purpose libraries, data structures and algorithms

+ + + +

Definitions and theorems used in many parts of the development

+ + + +

Source, intermediate and target languages: syntax and semantics

+ + + +

Compiler passes

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
PassSource & targetCompiler codeCorrectness proof
Pulling side-effects out of expressions;
+ fixing an evaluation order		CompCert C to ClightSimplExprSimplExprspec
+ SimplExprproof
Pulling non-adressable scalar local variables out of memoryClight to ClightSimplLocalsSimplLocalsproof
Simplification of control structures;
+ explication of type-dependent computations		Clight to CsharpminorCshmgenCshmgenproof
Stack allocation of local variables
+ whose address is taken;
+ simplification of switch statements		Csharpminor to CminorCminorgenCminorgenproof
Recognition of operators
and addressing modes		Cminor to CminorSelSelection
+ SelectOp
+ SelectLong
+ SelectDiv
+ SplitLong		Selectionproof
+ SelectOpproof
+ SelectLongproof
+ SelectDivproof
+ SplitLongproof
Construction of the CFG,
3-address code generation		CminorSel to RTLRTLgenRTLgenspec
+ RTLgenproof
Recognition of tail callsRTL to RTLTailcallTailcallproof
Function inliningRTL to RTLInliningInliningspec
+ Inliningproof
Postorder renumbering of the CFGRTL to RTLRenumberRenumberproof
Constant propagationRTL to RTLConstprop
+ ConstpropOp		Constpropproof
+ ConstproppOproof
Common subexpression eliminationRTL to RTLCSE
+ CombineOp		CSEproof
+ CombineOpproof
Redundancy eliminationRTL to RTLDeadcodeDeadcodeproof
Removal of unused static globalsRTL to RTLUnusedglobUnusedglobproof
Register allocation (validation a posteriori)RTL to LTLAllocationAllocproof
Branch tunnelingLTL to LTLTunnelingTunnelingproof
Linearization of the CFGLTL to LinearLinearizeLinearizeproof
Removal of unreferenced labelsLinear to LinearCleanupLabelsCleanupLabelsproof
Synthesis of debugging informationLinear to LinearDebugvarDebugvarproof
Laying out the activation recordsLinear to MachStacking
+ Bounds
+ Stacklayout		Stackingproof
+ Separation
Reconstruction of basic-blocks at Mach levelMach to MachblockMachblockgenForwardSimulationBlock
+ Machblockgenproof
Emission of purely sequential assembly codeMachblock to AsmblockAsmblockgenAsmblockgenproof0
+ Asmblockgenproof1
+ Asmblockgenproof
Bundling (and basic-block scheduling)Asmblock to AsmvliwPostpassScheduling using
+ Asmblockdeps and the abstractbb library		PostpassSchedulingproof
Flattening bundles (only a bureaucratic operation)Asmvliw to AsmAsmgenAsmgenproof
+ +

All together

+ + + +

Static analyses

+ +The following static analyses are performed over the RTL intermediate +representation to support optimizations such as constant propagation, +CSE, and dead code elimination. + + +

Type systems

+ +The type system of CompCert C is fully formalized. For some intermediate languages of the back-end, simpler type systems are used to statically capture well-formedness conditions. + + +
+
Xavier.Leroy@inria.fr
+
+ + + -- cgit