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