updating the html index for mppa-k1c

NOTE: This file has been copied from the one of pldi-artefact branch.
author: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> 2020-05-10 18:11:58 +0200
committer: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> 2020-05-10 18:11:58 +0200
commit: afefcbe84bfe603a7954fc99688636e40bfd1c1f (patch)
tree: 96bcfaf1d310d896c60dc42509af709ea166a82e /doc
parent: 6171f6a0880acbf0d007a7715cc37984ac25d851 (diff)
download: compcert-kvx-afefcbe84bfe603a7954fc99688636e40bfd1c1f.tar.gz
compcert-kvx-afefcbe84bfe603a7954fc99688636e40bfd1c1f.zip
1 files changed, 27 insertions, 45 deletions
diff --git a/doc/index-mppa_k1c.html b/doc/index-mppa_k1c.html
index 41a44a0d..50e11def 100644
--- a/doc/index-mppa_k1c.html
+++ b/doc/index-mppa_k1c.html
@@ -22,50 +22,19 @@ a:active {color : Red; text-decoration : underline; }
 </HEAD>
 <BODY>
 
-<H1 align="center">The CompCert verified compiler</H1>
+<font color=gray><H1 align="center">The CompCert verified compiler</H1>
 <H2 align="center">Commented Coq development</H2>
-<H3 align="center">Version 3.5, 2019-02-27</H3>
-<H3 align="center">PATCHED FOR MPPA-K1C</H3>
+<H3 align="center">Version 3.7, 2020-03-31</H3></font>
+<H3 align="center">PATCHED for the Kalray MPPA-K1C VLIW CORE</H3>
 
 <H2>Introduction</H2>
 
-<P>CompCert is a compiler that generates PowerPC, ARM, RISC-V and x86 assembly
-code from CompCert C, a large subset of the C programming language.
-The particularity of this compiler is that it is written mostly within
-the specification language of the Coq proof assistant, and its
-correctness --- the fact that the generated assembly code is
-semantically equivalent to its source program --- was entirely proved
-within the Coq proof assistant.</P>
+<p>This web page is a patched version of the table of contents of the official CompCert documentation,
+  as given on <A HREF="http://compcert.inria.fr/doc/index.html">the CompCert Web site</A>.
+  The unmodified parts of this table appear in <font color=gray>gray</font>.
+</font>
 
-<P>High-level descriptions of the CompCert compiler and its proof of 
-correctness can be found in the following papers (in increasing order of technical details):</P>
-<UL>
-<LI>Xavier Leroy, <A HREF="https://xavierleroy.org/publi/compcert-CACM.pdf">Formal verification of a realistic compiler</A>.  Communications of the ACM 52(7), July 2009.
-<LI>Xavier Leroy, <A HREF="https://xavierleroy.org/publi/compcert-backend.pdf">A formally verified compiler back-end</A>. 
-Journal of Automated Reasoning 43(4):363-446, 2009.
-</UL>
-
-<P>This Web site gives a commented listing of the underlying Coq
-specifications and proofs.  Proof scripts are folded by default, but
-can be viewed by clicking on "Proof".  Some modules (written in <I>italics</I> below) differ between the four target architectures.  The
-PowerPC versions of these modules are shown below; the ARM, x86 and RISC-V
-versions can be found in the source distribution.
-</P>
-
-<P> This development is a work in progress; some parts have
-substantially changed since the overview papers above were
-written.</P>
-
-<P>The complete sources for CompCert can be downloaded from
-<A HREF="http://compcert.inria.fr/">the CompCert Web site</A>.</P>
-
-<P>This document and the CompCert sources are copyright Institut
-National de Recherche en Informatique et en Automatique (INRIA) and
-AbsInt Angewandte Informatik GmbH, and are distributed under the terms of the
-following <A HREF="LICENSE">license</A>.
-</P>
-
-<H2>Table of contents</H2>
+<font color=gray><H2>Table of contents</H2>
 
 <H3>General-purpose libraries, data structures and algorithms</H3>
 
@@ -83,8 +52,16 @@ semi-lattices.
 inequations by fixpoint iteration.
 <LI> <A HREF="html/compcert.lib.UnionFind.html">UnionFind</A>: a persistent union-find data structure.
 <LI> <A HREF="html/compcert.lib.Postorder.html">Postorder</A>: postorder numbering of a directed graph.
+</UL></font>
+
+<H4>The <tt>abstractbb</tt> library, introduced for MPPA-K1C</H4>
+<UL>
+<LI> <A HREF="html/compcert.mppa_k1c.abstractbb.AbstractBasicBlocksDef.html">AbstractBasicBlocksDef</A>: an IR for verifying some semantic properties on basic-blocks.
+<LI> <A HREF="html/compcert.mppa_k1c.abstractbb.Parallelizability.html">Parallelizability</A>: verifying that sequential and parallel semantics are equivalent for a given abstract basic-block.
+<LI> <A HREF="html/compcert.mppa_k1c.abstractbb.ImpSimuTest.html">ImpSimuTest</A>: verifying that a given abstract basic-block is simulated by another one for sequential semantics. This module refines <A HREF="html/compcert.mppa_k1c.abstractbb.SeqSimuTheory.html">SeqSimuTheory</A> with hash-consing. 
 </UL>
 
+<font color=gray>
 <H3>Definitions and theorems used in many parts of the development</H3>
 
 <UL>
@@ -136,6 +113,10 @@ locations) and <A HREF="html/compcert.mppa_k1c.Machregs.html"><I>Machregs</I></A
 replaced by a linear list of instructions with explicit branches and labels.
 <LI> <A HREF="html/compcert.backend.Mach.html">Mach</A>: like Linear, with a more concrete
 view of the activation record.  
+</UL>
+</font>
+<H4>Languages introduced for MPPA-K1C</H4>
+<UL>
 <LI> <A HREF="html/compcert.mppa_k1c.lib.Machblock.html">Machblock</A>: a variant of Mach, with a syntax for basic-blocks, and a block-step semantics (execute one basic-block in one step).
 This IR is generic over the processor, even if currently, only used for MPPA_K1C.
 <LI> <A HREF="html/compcert.mppa_k1c.Asmvliw.html"><I>Asmvliw</I></A>: abstract syntax and semantics for Mppa_K1c VLIW assembly: atomic instructions are grouped by "bundles". These bundles are executed sequentially, but execution is parallel within bundles.
@@ -144,9 +125,9 @@ This IR is generic over the processor, even if currently, only used for MPPA_K1C
 <LI> <A HREF="html/compcert.mppa_k1c.Asm.html"><I>Asm</I></A>: a variant of Asmvliw with a flat syntax for bundles, instead of a structured one (bundle termination is encoded as a pseudo-instruction). This IR is mainly a wrapper of <I>Asmvliw</I> for a smooth integration in CompCert (and an easier pretty-printing of the abstract syntax).
 </UL>
 
-<H3>Compiler passes</H3>
+<font color=gray><H3>Compiler passes</H3></font>
 
-<TABLE cellpadding="5%">
+<TABLE cellpadding="5%" style="color:#808080">
 <TR valign="top">
   <TH>Pass</TH>
   <TH>Source &amp; target</TH>
@@ -305,7 +286,10 @@ This IR is generic over the processor, even if currently, only used for MPPA_K1C
   <TD><A HREF="html/compcert.backend.Stackingproof.html">Stackingproof</A><br>
       <A HREF="html/compcert.common.Separation.html">Separation</A></TD>
 </TR>
+</TABLE>
 
+<H4>Compilation passes introduced for MPPA-K1C</H4>
+<TABLE cellpadding="5%">
 <TR valign="top">
   <TD>Reconstruction of basic-blocks at Mach level</TD>
   <TD>Mach to Machblock</TD>
@@ -339,6 +323,7 @@ This IR is generic over the processor, even if currently, only used for MPPA_K1C
 </TR>
 </TABLE>
 
+<font color=gray>
 <H3>All together</H3>
 
 <UL>
@@ -371,10 +356,7 @@ The <A HREF="html/compcert.cfrontend.Ctyping.html">type system of CompCert C</A>
 reconstruction.
 <LI> <A HREF="html/compcert.backend.Lineartyping.html">Lineartyping</A>: typing for Linear.
 </UL>
-
-<HR>
-<ADDRESS>Xavier.Leroy@inria.fr</ADDRESS>
-<HR>
+</font>
 
 </BODY>
 </HTML>
author	Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>	2020-05-10 18:11:58 +0200
committer	Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>	2020-05-10 18:11:58 +0200
commit	afefcbe84bfe603a7954fc99688636e40bfd1c1f (patch)
tree	96bcfaf1d310d896c60dc42509af709ea166a82e /doc
parent	6171f6a0880acbf0d007a7715cc37984ac25d851 (diff)
download	compcert-kvx-afefcbe84bfe603a7954fc99688636e40bfd1c1f.tar.gz compcert-kvx-afefcbe84bfe603a7954fc99688636e40bfd1c1f.zip