From c3ff165355e49114364bd45cd7c145ccb248ca8f Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 19 Jun 2013 07:38:24 +0000 Subject: Updates in preparation for release 2.00 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2283 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- doc/index.html | 63 +++++++++++++++------------------------------------------- 1 file changed, 16 insertions(+), 47 deletions(-) (limited to 'doc') diff --git a/doc/index.html b/doc/index.html index 1f5d3ed..adad156 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.13, 2013-03-12

+

Version 2.00, 2013-06-21

Introduction

@@ -85,7 +85,6 @@ ordered types. semi-lattices.
  • Kildall: resolution of dataflow inequations by fixpoint iteration. -
  • Parmov: compilation of parallel assignments.
  • UnionFind: a persistent union-find data structure.
  • Postorder: postorder numbering of a directed graph. @@ -107,6 +106,7 @@ See also: Memdata (in-memory representation of d
  • Determinism: determinism properties of small-step semantics.
  • Op: operators, addressing modes and their semantics. +
  • Subtyping: a solver for atomic subtyping constraints.

    Source, intermediate and target languages: syntax and semantics

    @@ -131,14 +131,12 @@ code, control-flow graph, infinitely many pseudo-registers).
    See also: Registers (representation of pseudo-registers).
  • LTL: location transfer language (3-address -code, control-flow graph, finitely many physical registers, infinitely +code, control-flow graph of basic blocks, finitely many physical registers, infinitely many stack slots).
    See also: Locations (representation of locations) and Machregs (description of processor registers). -
  • LTLin: like LTL, but the CFG is +
  • Linear: 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.
  • Asm: abstract syntax for PowerPC assembly @@ -189,9 +187,11 @@ code. Recognition of operators
    and addressing modes Cminor to CminorSel Selection
    - SelectOp + SelectOp
    + SelectLong Selectionproof
    - SelectOpproof + SelectOpproof
    + SelectLongproof @@ -228,7 +228,8 @@ code. Constant propagation RTL to RTL Constprop
    - ConstpropOp + ConstpropOp
    + Liveness Constpropproof
    ConstproppOproof @@ -243,14 +244,10 @@ code. - Register allocation by coloring
    of an interference graph + Register allocation (validation a posteriori) RTL to LTL - InterfGraph
    - Coloring
    - Allocation -
    - Coloringproof
    - Allocproof + Allocation + Allocproof @@ -262,35 +259,18 @@ code. Linearization of the CFG - LTL to LTLin + LTL to Linear Linearize Linearizeproof Removal of unreferenced labels - LTLin to LTLin + Linear to Linear CleanupLabels CleanupLabelsproof - - Spilling, reloading, calling conventions - LTLin to Linear - Reload
    - Conventions
    - Conventions1
    - Parallelmove
    - Reloadproof - - - - Redundant reload elimination - Linear to Linear - RRE - RREproof - - Laying out the activation records Linear to Mach @@ -313,23 +293,12 @@ code.

    Type systems

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

    All together

    -- cgit v1.2.3