From afefcbe84bfe603a7954fc99688636e40bfd1c1f Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Sun, 10 May 2020 18:11:58 +0200 Subject: updating the html index for mppa-k1c NOTE: This file has been copied from the one of pldi-artefact branch. --- doc/index-mppa_k1c.html | 72 +++++++++++++++++++------------------------------ 1 file changed, 27 insertions(+), 45 deletions(-) (limited to 'doc') 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; } -

The CompCert verified compiler

+

The CompCert verified compiler

Commented Coq development

-

Version 3.5, 2019-02-27

-

PATCHED FOR MPPA-K1C

+

Version 3.7, 2020-03-31

 +

PATCHED for the Kalray MPPA-K1C VLIW CORE

Introduction

-

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.

+

This web page is a patched version of the table of contents of the official CompCert documentation, + as given on the CompCert Web site. + The unmodified parts of this table appear in gray. + -

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):

- - -

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 italics 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. -

- -

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.

- -

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 license. -

- -

Table of contents

+

Table of contents

General-purpose libraries, data structures and algorithms

@@ -83,8 +52,16 @@ semi-lattices. inequations by fixpoint iteration.
  • UnionFind: a persistent union-find data structure.
  • Postorder: postorder numbering of a directed graph. + + +

    The abstractbb library, introduced for MPPA-K1C

    + +

    Definitions and theorems used in many parts of the development

      @@ -136,6 +113,10 @@ locations) and Machregs Mach: like Linear, with a more concrete view of the activation record. +
    +     +

    Languages introduced for MPPA-K1C

    + -

    Compiler passes

    +

    Compiler passes

     - +
    @@ -305,7 +286,10 @@ This IR is generic over the processor, even if currently, only used for MPPA_K1C +
    Pass Source & targetStackingproof
    Separation
    +

    Compilation passes introduced for MPPA-K1C

    + @@ -339,6 +323,7 @@ This IR is generic over the processor, even if currently, only used for MPPA_K1C
    Reconstruction of basic-blocks at Mach level Mach to Machblock
    +

    All together

    - -
    -
    Xavier.Leroy@inria.fr
    -
    +     -- cgit