diff options
-rw-r--r-- | Changelog | 9 | ||||
-rw-r--r-- | doc/index.html | 63 |
2 files changed, 20 insertions, 52 deletions
@@ -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 1f5d3ed5..adad1564 100644 --- a/doc/index.html +++ b/doc/index.html @@ -24,7 +24,7 @@ a:active {color : Red; text-decoration : underline; } <H1 align="center">The CompCert verified compiler</H1> <H2 align="center">Commented Coq development</H2> -<H3 align="center">Version 1.13, 2013-03-12</H3> +<H3 align="center">Version 2.00, 2013-06-21</H3> <H2>Introduction</H2> @@ -85,7 +85,6 @@ ordered types. semi-lattices. <LI> <A HREF="html/Kildall.html">Kildall</A>: resolution of dataflow inequations by fixpoint iteration. -<LI> <A HREF="html/Parmov.html">Parmov</A>: compilation of parallel assignments. <LI> <A HREF="html/UnionFind.html">UnionFind</A>: a persistent union-find data structure. <LI> <A HREF="html/Postorder.html">Postorder</A>: postorder numbering of a directed graph. </UL> @@ -107,6 +106,7 @@ See also: <A HREF="html/Memdata.html">Memdata</A> (in-memory representation of d <LI> <A HREF="html/Determinism.html">Determinism</A>: determinism properties of small-step semantics. <LI> <A HREF="html/Op.html"><I>Op</I></A>: operators, addressing modes and their semantics. +<LI> <A HREF="html/Subtyping.html">Subtyping</A>: a solver for atomic subtyping constraints. </UL> <H3>Source, intermediate and target languages: syntax and semantics</H3> @@ -131,14 +131,12 @@ code, control-flow graph, infinitely many pseudo-registers). <BR> See also: <A HREF="html/Registers.html">Registers</A> (representation of pseudo-registers). <LI> <A HREF="html/LTL.html">LTL</A>: 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). <BR> See also: <A HREF="html/Locations.html">Locations</A> (representation of locations) and <A HREF="html/Machregs.html"><I>Machregs</I></A> (description of processor registers). -<LI> <A HREF="html/LTLin.html">LTLin</A>: like LTL, but the CFG is +<LI> <A HREF="html/Linear.html">Linear</A>: like LTL, but the CFG is replaced by a linear list of instructions with explicit branches and labels. -<LI> <A HREF="html/Linear.html">Linear</A>: like LTLin, with explicit -spilling, reloading and enforcement of calling conventions. <LI> <A HREF="html/Mach.html">Mach</A>: like Linear, with a more concrete view of the activation record. <LI> <A HREF="html/Asm.html"><I>Asm</I></A>: abstract syntax for PowerPC assembly @@ -189,9 +187,11 @@ code. <TD>Recognition of operators<br>and addressing modes</TD> <TD>Cminor to CminorSel</TD> <TD><A HREF="html/Selection.html">Selection</A><br> - <A HREF="html/SelectOp.html"><I>SelectOp</I></A></TD> + <A HREF="html/SelectOp.html"><I>SelectOp</I></A><br> + <A HREF="html/SelectLong.html">SelectLong</A></TD> <TD><A HREF="html/Selectionproof.html">Selectionproof</A><br> - <A HREF="html/SelectOpproof.html"><I>SelectOpproof</I></A></TD> + <A HREF="html/SelectOpproof.html"><I>SelectOpproof</I></A><br> + <A HREF="html/SelectLongproof.html">SelectLongproof</A></TD> </TR> <TR valign="top"> @@ -228,7 +228,8 @@ code. <TD>Constant propagation</TD> <TD>RTL to RTL</TD> <TD><A HREF="html/Constprop.html">Constprop</A><br> - <A HREF="html/ConstpropOp.html"><I>ConstpropOp</I></A></TD> + <A HREF="html/ConstpropOp.html"><I>ConstpropOp</I></A><br> + <A HREF="html/Liveness.html">Liveness</A></TD> <TD><A HREF="html/Constpropproof.html">Constpropproof</A><br> <A HREF="html/ConstpropOpproof.html"><I>ConstproppOproof</I></A></TD> </TR> @@ -243,14 +244,10 @@ code. </TR> <TR valign="top"> - <TD>Register allocation by coloring<br>of an interference graph</TD> + <TD>Register allocation (validation a posteriori)</TD> <TD>RTL to LTL</TD> - <TD><A HREF="html/InterfGraph.html">InterfGraph</A><BR> - <A HREF="html/Coloring.html">Coloring</A><BR> - <A HREF="html/Allocation.html">Allocation</A></TD> - <TD><BR> - <A HREF="html/Coloringproof.html">Coloringproof</A><BR> - <A HREF="html/Allocproof.html">Allocproof</A></TD> + <TD><A HREF="html/Allocation.html">Allocation</A></TD> + <TD><A HREF="html/Allocproof.html">Allocproof</A></TD> </TR> <TR valign="top"> @@ -262,36 +259,19 @@ code. <TR valign="top"> <TD>Linearization of the CFG</TD> - <TD>LTL to LTLin</TD> + <TD>LTL to Linear</TD> <TD><A HREF="html/Linearize.html">Linearize</A></TD> <TD><A HREF="html/Linearizeproof.html">Linearizeproof</A></TD> </TR> <TR valign="top"> <TD>Removal of unreferenced labels</TD> - <TD>LTLin to LTLin</TD> + <TD>Linear to Linear</TD> <TD><A HREF="html/CleanupLabels.html">CleanupLabels</A></TD> <TD><A HREF="html/CleanupLabelsproof.html">CleanupLabelsproof</A></TD> </TR> <TR valign="top"> - <TD>Spilling, reloading, calling conventions</TD> - <TD>LTLin to Linear</TD> - <TD><A HREF="html/Reload.html">Reload</A><BR> - <A HREF="html/Conventions.html">Conventions</A><BR> - <A HREF="html/Conventions1.html"><I>Conventions1</I></A><BR></TD> - <TD><A HREF="html/Parallelmove.html">Parallelmove</A><BR> - <A HREF="html/Reloadproof.html">Reloadproof</A></TD> -</TR> - -<TR valign="top"> - <TD>Redundant reload elimination</TD> - <TD>Linear to Linear</TD> - <TD><A HREF="html/RRE.html">RRE</A></TD> - <TD><A HREF="html/RREproof.html">RREproof</A></TD> -</TR> - -<TR valign="top"> <TD>Laying out the activation records</TD> <TD>Linear to Mach</TD> <TD><A HREF="html/Stacking.html">Stacking</A><BR> @@ -313,23 +293,12 @@ code. <H3>Type systems</H3> Trivial type systems are used to statically capture well-formedness -conditions on the source and intermediate languages. +conditions on some intermediate languages. <UL> <LI> <A HREF="html/RTLtyping.html">RTLtyping</A>: typing for RTL + type reconstruction. -<LI> <A HREF="html/LTLtyping.html">LTLtyping</A>: typing for LTL. -<LI> <A HREF="html/LTLintyping.html">LTLintyping</A>: typing for LTLin. <LI> <A HREF="html/Lineartyping.html">Lineartyping</A>: typing for Linear. </UL> -Proofs that compiler passes are type-preserving: -<UL> -<LI> <A HREF="html/Alloctyping.html">Alloctyping</A> (register allocation). -<LI> <A HREF="html/Tunnelingtyping.html">Tunnelingtyping</A> (branch tunneling). -<LI> <A HREF="html/Linearizetyping.html">Linearizetyping</A> (code linearization). -<LI> <A HREF="html/CleanupLabelstyping.html">CleanupLabelstyping</A> (removal of unreferenced labels). -<LI> <A HREF="html/Reloadtyping.html">Reloadtyping</A> (spilling and reloading). -<LI> <A HREF="html/RREtyping.html">RREtyping</A> (redundant reload elimination). -</UL> <H3>All together</H3> |