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 --- Changelog | 9 ++++----- doc/index.html | 63 +++++++++++++++------------------------------------------- 2 files changed, 20 insertions(+), 52 deletions(-) diff --git a/Changelog b/Changelog index c97fb1c..65e8e50 100644 --- a/Changelog +++ b/Changelog @@ -1,4 +1,4 @@ -Release 2.00, 2013-06-XX +Release 2.00, 2013-06-21 ======================== Major improvements: @@ -20,8 +20,7 @@ Major improvements: . two-address operations are treated more efficiently . no need to reserve processor registers for spilling and reloading. The improvements in quality of generated code is significant for - IA32 (because of its paucity of registers) and barely noticeable - for ARM and PowerPC. + IA32 (because of its paucity of registers) but less so for ARM and PowerPC. - Preliminary support for debugging information. The "-g" flag causes DWARF debugging information to be generated for line numbers @@ -49,7 +48,7 @@ Improvements in compiler usability: - Reduced memory requirements of constant propagation pass by forgetting compile-time approximations of dead variables. - More careful elaboration of C struct and union types into CompCert C - types, avoiding behaviors exponential in the nesting of structs. + types, avoiding behaviors exponential in the nesting of structs. Bug fixing: - Fixed parsing of labeled statements inside "switch" constructs, @@ -61,7 +60,7 @@ Bug fixing: Coq development: - Adapted the memory model to the needs of the VST project at Princeton: . Memory block identifiers are now of type "positive" instead of "Z" - . Strengthened preconditions in the definition of memory injections + . Strengthened invariants in the definition of memory injections and the specification of external calls. - The LTL intermediate language is now a CFG of basic blocks. - Suppressed the LTLin intermediate language, no longer used. 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