From 37447ffb3242d1d8ffa7c60eedeea848bd4ba956 Mon Sep 17 00:00:00 2001
From: xleroy
Date: Tue, 24 May 2011 13:28:41 +0000
Subject: Update for release 1.8.2
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1656 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
doc/index.html | 67 +++++++++++++++++++++++++++++++++-------------------------
1 file changed, 38 insertions(+), 29 deletions(-)
(limited to 'doc')
diff --git a/doc/index.html b/doc/index.html
index 9e2d79d..4c1d536 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -24,7 +24,7 @@ a:active {color : Red; text-decoration : underline; }
The Compcert verified compiler
Commented Coq development
-Version 1.8.1, 2011-03-14
+Version 1.8.2, 2011-05-24
Introduction
@@ -49,10 +49,15 @@ Journal of Automated Reasoning 43(4):363-446, 2009.
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 have substantially changed since the
-overview papers above were written.
+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 three supported target architectures. The
+PowerPC versions of these modules are shown below; the ARM and x86
+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.
@@ -97,7 +102,7 @@ See also: Memdata (in-memory representation of d
Globalenvs: global execution environments.
Smallstep: tools for small-step semantics.
Determinism: determinism properties of small-step semantics.
- Op: operators, addressing modes and their
+ Op: operators, addressing modes and their
semantics.
@@ -123,15 +128,15 @@ pseudo-registers).
code, control-flow graph, finitely many physical registers, infinitely
many stack slots).
See also: Locations (representation of
-locations).
+locations) and Machregs (description of processor registers).
LTLin: like LTL, but the CFG is
replaced by a linear list of instructions with explicit branches and labels.
Linear: like LTLin, with explicit
spilling, reloading and enforcement of calling conventions.
Mach: like Linear, with a more concrete
view of the activation record.
-See also: Machabstr operational semantics for Mach.
- Asm: abstract syntax for PowerPC assembly
+See also: Machsem operational semantics for Mach.
+ Asm: abstract syntax for PowerPC assembly
code.
@@ -173,14 +178,14 @@ code.
Recognition of operators and addressing modes |
Cminor to CminorSel |
Selection
- SelectOp |
+ SelectOp
Selectionproof
- SelectOpproof |
+ SelectOpproof
Construction of the CFG, 3-address code generation |
- Cminor to RTL |
+ CminorSel to RTL |
RTLgen |
RTLgenspec
RTLgenproof |
@@ -197,9 +202,9 @@ code.
Constant propagation |
RTL to RTL |
Constprop
- ConstpropOp |
+ ConstpropOp
Constpropproof
- ConstproppOproof |
+ ConstproppOproof
@@ -241,11 +246,19 @@ code.
Linearizeproof |
+
+ Removal of unreferenced labels |
+ LTLin to LTLin |
+ CleanupLabels |
+ CleanupLabelsproof |
+
+
Spilling, reloading, calling conventions |
LTLin to Linear |
- Conventions
- Reload |
+ Reload
+ Conventions
+ Conventions1
|
Parallelmove
Reloadproof |
@@ -253,24 +266,19 @@ code.
Laying out the activation records |
Linear to Mach |
- Bounds
- Stacking |
- Stackingproof |
+ Stacking
+ Bounds
+ Stacklayout |
+ Stackingproof
+ Asmgenretaddr |
-
- Storing the activation records in memory |
- Mach to Mach |
- (none)
- | Asmgenretaddr
- Machabstr2concr |
-
Emission of assembly code |
Mach to Asm |
- Asmgen |
- Asmgenproof1
- Asmgenproof |
+ Asmgen |
+ Asmgenproof1
+ Asmgenproof |
@@ -291,6 +299,7 @@ Proofs that compiler passes are type-preserving:
Alloctyping (register allocation).
Tunnelingtyping (branch tunneling).
Linearizetyping (code linearization).
+ CleanupLabelstyping (removal of unreferenced labels).
Reloadtyping (spilling and reloading).
Stackingtyping (layout of activation records).
--
cgit v1.2.3