diff options
Diffstat (limited to 'doc/index-kvx.html')
-rw-r--r-- | doc/index-kvx.html | 368 |
1 files changed, 368 insertions, 0 deletions
diff --git a/doc/index-kvx.html b/doc/index-kvx.html new file mode 100644 index 00000000..b8850727 --- /dev/null +++ b/doc/index-kvx.html @@ -0,0 +1,368 @@ +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"> +<HTML> +<HEAD> +<TITLE>The CompCert verified compiler</TITLE> +<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1"> + +<style type="text/css"> +body { + color: black; background: white; + margin-left: 5%; margin-right: 5%; +} +h2 { margin-left: -5%;} +h3 { margin-left: -3%; } +h1,h2,h3 { font-family: sans-serif; } +hr { margin-left: -5%; margin-right:-5%; } +a:visited {color : #416DFF; text-decoration : none; font-weight : bold} +a:link {color : #416DFF; text-decoration : none; font-weight : bold} +a:hover {color : Red; text-decoration : underline; } +a:active {color : Red; text-decoration : underline; } +</style> + +</HEAD> +<BODY> + +<font color=gray><H1 align="center">The CompCert verified compiler</H1> +<H2 align="center">Commented Coq development</H2> +<H3 align="center">Version 3.7, 2020-03-31</H3></font> +<H3 align="center">PATCHED for the Kalray MPPA-KVX VLIW CORE<!--@DATE@--></H3> + +<H2>Introduction</H2> + +<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>. + <br> + <br> + A high-level view of this CompCert backend is provided by this OOPSLA'20 paper (of Six, Boulmé and Monniaux): + <div><a href=https://hal.archives-ouvertes.fr/hal-02185883>Certified and Efficient Instruction Scheduling. Application to Interlocked VLIW Processors.</a></div> + <br> + See also the <tt>README.md</tt> of our <a href=https://gricad-gitlab.univ-grenoble-alpes.fr/certicompil/compcert-kvx>GitLab public repository</a>. +</p> + +<font color=gray><H2>Table of contents</H2> + +<H3>General-purpose libraries, data structures and algorithms</H3> + +<UL> +<LI> <A HREF="html/compcert.lib.Coqlib.html">Coqlib</A>: addendum to the Coq standard library. +<LI> <A HREF="html/compcert.lib.Maps.html">Maps</A>: finite maps. +<LI> <A HREF="html/compcert.lib.Integers.html">Integers</A>: machine integers. +<LI> <A HREF="html/compcert.lib.Floats.html">Floats</A>: machine floating-point numbers. +<LI> <A HREF="html/compcert.lib.Iteration.html">Iteration</A>: various forms of "while" loops. +<LI> <A HREF="html/compcert.lib.Ordered.html">Ordered</A>: construction of +ordered types. +<LI> <A HREF="html/compcert.lib.Lattice.html">Lattice</A>: construction of +semi-lattices. +<LI> <A HREF="html/compcert.backend.Kildall.html">Kildall</A>: resolution of dataflow +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 KVX core</H4> +<UL> +<LI> <A HREF="html/compcert.kvx.abstractbb.AbstractBasicBlocksDef.html">AbstractBasicBlocksDef</A>: an IR for verifying some semantic properties on basic-blocks. +<LI> <A HREF="html/compcert.kvx.abstractbb.Parallelizability.html">Parallelizability</A>: verifying that sequential and parallel semantics are equivalent for a given abstract basic-block. +<LI> <A HREF="html/compcert.kvx.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.kvx.abstractbb.SeqSimuTheory.html">SeqSimuTheory</A> with hash-consing and uses <A HREF=https://github.com/boulme/ImpureDemo>the Impure library</A> to reason on physical equality and handling of imperative code in Coq. +</UL> + +<font color=gray> +<H3>Definitions and theorems used in many parts of the development</H3> + +<UL> +<LI> <A HREF="html/compcert.common.Errors.html">Errors</A>: the Error monad. +<LI> <A HREF="html/compcert.common.AST.html">AST</A>: identifiers, whole programs and other +common elements of abstract syntaxes. +<LI> <A HREF="html/compcert.common.Linking.html">Linking</A>: generic framework to define syntactic linking over the CompCert languages. +<LI> <A HREF="html/compcert.common.Values.html">Values</A>: run-time values. +<LI> <A HREF="html/compcert.common.Events.html">Events</A>: observable events and traces. +<LI> <A HREF="html/compcert.common.Memory.html">Memory</A>: memory model. <BR> +See also: <A HREF="html/compcert.common.Memdata.html">Memdata</A> (in-memory representation of data). +<LI> <A HREF="html/compcert.common.Globalenvs.html">Globalenvs</A>: global execution environments. +<LI> <A HREF="html/compcert.common.Smallstep.html">Smallstep</A>: tools for small-step semantics. +<LI> <A HREF="html/compcert.common.Behaviors.html">Behaviors</A>: from small-step semantics to observable behaviors of programs. +<LI> <A HREF="html/compcert.common.Determinism.html">Determinism</A>: determinism properties of small-step semantics. +<LI> <A HREF="html/compcert.kvx.Op.html"><I>Op</I></A>: operators, addressing modes and their +semantics. +<LI> <A HREF="html/compcert.common.Unityping.html">Unityping</A>: a solver for atomic unification constraints. +</UL> + +<H3>Source, intermediate and target languages: syntax and semantics</H3> + +<UL> +<LI> The CompCert C source language: +<A HREF="html/compcert.cfrontend.Csyntax.html">syntax</A> and +<A HREF="html/compcert.cfrontend.Csem.html">semantics</A> and +<A HREF="html/compcert.cfrontend.Cstrategy.html">determinized semantics</A> and +<A HREF="html/compcert.cfrontend.Ctyping.html">type system</A>.<BR> +See also: <A HREF="html/compcert.cfrontend.Ctypes.html">type expressions</A> and +<A HREF="html/compcert.cfrontend.Cop.html">operators (syntax and semantics)</A>.<BR> +See also: <A HREF="html/compcert.cfrontend.Cexec.html">reference interpreter</A>. +<LI> <A HREF="html/compcert.cfrontend.Clight.html">Clight</A>: a simpler version of CompCert C where expressions contain no side-effects. +<LI> <A HREF="html/compcert.cfrontend.Csharpminor.html">Csharpminor</A>: low-level + structured language. +<LI> <A HREF="html/compcert.backend.Cminor.html">Cminor</A>: low-level structured +language, with explicit stack allocation of certain local variables. +<LI> <A HREF="html/compcert.backend.CminorSel.html">CminorSel</A>: like Cminor, +with machine-specific operators and addressing modes. +<LI> <A HREF="html/compcert.backend.RTL.html">RTL</A>: register transfer language (3-address +code, control-flow graph, infinitely many pseudo-registers). <BR> +See also: <A HREF="html/compcert.backend.Registers.html">Registers</A> (representation of +pseudo-registers). +<LI> <A HREF="html/compcert.backend.LTL.html">LTL</A>: location transfer language (3-address +code, control-flow graph of basic blocks, finitely many physical registers, infinitely +many stack slots). <BR> +See also: <A HREF="html/compcert.backend.Locations.html">Locations</A> (representation of +locations) and <A HREF="html/compcert.kvx.Machregs.html"><I>Machregs</I></A> (description of processor registers). +<LI> <A HREF="html/compcert.backend.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/compcert.backend.Mach.html">Mach</A>: like Linear, with a more concrete +view of the activation record. +</UL> +</font> +<H4>Languages introduced for KVX core</H4> +<UL> +<LI> <A HREF="html/compcert.kvx.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 KVX. +<LI> <A HREF="html/compcert.kvx.Asmvliw.html"><I>Asmvliw</I></A>: abstract syntax and semantics for KVX VLIW assembly: atomic instructions are grouped by "bundles". These bundles are executed sequentially, but execution is parallel within bundles. +<LI> <A HREF="html/compcert.kvx.Asmblock.html"><I>Asmblock</I></A>: a variant of Asmvliw, with a sequential semantics within bundles, which make them corresponds here to usual basic-blocks. + This IR is an intermediate step between Machblock and Asmvliw. +<LI> <A HREF="html/compcert.kvx.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> + +<font color=gray><H3>Compiler passes</H3></font> + +<TABLE cellpadding="5%" style="color:#808080"> +<TR valign="top"> + <TH>Pass</TH> + <TH>Source & target</TH> + <TH>Compiler code</TH> + <TH>Correctness proof</TH> +</TR> + +<TR valign="top"> + <TD>Pulling side-effects out of expressions;<br> + fixing an evaluation order</TD> + <TD>CompCert C to Clight</TD> + <TD><A HREF="html/compcert.cfrontend.SimplExpr.html">SimplExpr</A></TD> + <TD><A HREF="html/compcert.cfrontend.SimplExprspec.html">SimplExprspec</A><br> + <A HREF="html/compcert.cfrontend.SimplExprproof.html">SimplExprproof</A></TD> +</TR> +<TR valign="top"> + <TD>Pulling non-adressable scalar local variables out of memory</TD> + <TD>Clight to Clight</TD> + <TD><A HREF="html/compcert.cfrontend.SimplLocals.html">SimplLocals</A></TD> + <TD><A HREF="html/compcert.cfrontend.SimplLocalsproof.html">SimplLocalsproof</A></TD> +</TR> +<TR valign="top"> + <TD>Simplification of control structures; <br> + explication of type-dependent computations</TD> + <TD>Clight to Csharpminor</TD> + <TD><A HREF="html/compcert.cfrontend.Cshmgen.html">Cshmgen</A></TD> + <TD><A HREF="html/compcert.cfrontend.Cshmgenproof.html">Cshmgenproof</A></TD> +</TR> +<TR valign="top"> + <TD>Stack allocation of local variables<br> + whose address is taken;<br> + simplification of switch statements</TD> + <TD>Csharpminor to Cminor</TD> + <TD><A HREF="html/compcert.cfrontend.Cminorgen.html">Cminorgen</A></TD> + <TD><A HREF="html/compcert.cfrontend.Cminorgenproof.html">Cminorgenproof</A></TD> +</TR> + +<TR valign="top"> + <TD>Recognition of operators<br>and addressing modes</TD> + <TD>Cminor to CminorSel</TD> + <TD><A HREF="html/compcert.backend.Selection.html">Selection</A><br> + <A HREF="html/compcert.kvx.SelectOp.html"><I>SelectOp</I></A><br> + <A HREF="html/compcert.kvx.SelectLong.html"><I>SelectLong</I></A><br> + <A HREF="html/compcert.backend.SelectDiv.html">SelectDiv</A><br> + <A HREF="html/compcert.backend.SplitLong.html">SplitLong</A></TD> + <TD><A HREF="html/compcert.backend.Selectionproof.html">Selectionproof</A><br> + <A HREF="html/compcert.kvx.SelectOpproof.html"><I>SelectOpproof</I></A><br> + <A HREF="html/compcert.kvx.SelectLongproof.html"><I>SelectLongproof</I></A><br> + <A HREF="html/compcert.backend.SelectDivproof.html">SelectDivproof</A><br> + <A HREF="html/compcert.backend.SplitLongproof.html">SplitLongproof</A></TD> +</TR> + +<TR valign="top"> + <TD>Construction of the CFG, <br>3-address code generation</TD> + <TD>CminorSel to RTL</TD> + <TD><A HREF="html/compcert.backend.RTLgen.html">RTLgen</A></TD> + <TD><A HREF="html/compcert.backend.RTLgenspec.html">RTLgenspec</A><BR> + <A HREF="html/compcert.backend.RTLgenproof.html">RTLgenproof</A></TD> +</TR> + +<TR valign="top"> + <TD>Recognition of tail calls</TD> + <TD>RTL to RTL</TD> + <TD><A HREF="html/compcert.backend.Tailcall.html">Tailcall</A></TD> + <TD><A HREF="html/compcert.backend.Tailcallproof.html">Tailcallproof</A></TD> +</TR> + +<TR valign="top"> + <TD>Function inlining</TD> + <TD>RTL to RTL</TD> + <TD><A HREF="html/compcert.backend.Inlining.html">Inlining</A></TD> + <TD><A HREF="html/compcert.backend.Inliningspec.html">Inliningspec</A><BR> + <A HREF="html/compcert.backend.Inliningproof.html">Inliningproof</A></TD> +</TR> + +<TR valign="top"> + <TD>Postorder renumbering of the CFG</TD> + <TD>RTL to RTL</TD> + <TD><A HREF="html/compcert.backend.Renumber.html">Renumber</A></TD> + <TD><A HREF="html/compcert.backend.Renumberproof.html">Renumberproof</A></TD> +</TR> + +<TR valign="top"> + <TD>Constant propagation</TD> + <TD>RTL to RTL</TD> + <TD><A HREF="html/compcert.backend.Constprop.html">Constprop</A><br> + <A HREF="html/compcert.kvx.ConstpropOp.html"><I>ConstpropOp</I></A></TD> + <TD><A HREF="html/compcert.backend.Constpropproof.html">Constpropproof</A><br> + <A HREF="html/compcert.kvx.ConstpropOpproof.html"><I>ConstproppOproof</I></A></TD> +</TR> + +<TR valign="top"> + <TD>Common subexpression elimination</TD> + <TD>RTL to RTL</TD> + <TD><A HREF="html/compcert.backend.CSE.html">CSE</A><BR> + <A HREF="html/compcert.kvx.CombineOp.html"><I>CombineOp</I></A></TD> + <TD><A HREF="html/compcert.backend.CSEproof.html">CSEproof</A><BR> + <A HREF="html/compcert.kvx.CombineOpproof.html"><I>CombineOpproof</I></A></TD> +</TR> + +<TR valign="top"> + <TD>Redundancy elimination</TD> + <TD>RTL to RTL</TD> + <TD><A HREF="html/compcert.backend.Deadcode.html">Deadcode</A></TD> + <TD><A HREF="html/compcert.backend.Deadcodeproof.html">Deadcodeproof</A></TD> +</TR> + +<TR valign="top"> + <TD>Removal of unused static globals</TD> + <TD>RTL to RTL</TD> + <TD><A HREF="html/compcert.backend.Unusedglob.html">Unusedglob</A></TD> + <TD><A HREF="html/compcert.backend.Unusedglobproof.html">Unusedglobproof</A></TD> +</TR> + +<TR valign="top"> + <TD>Register allocation (validation a posteriori)</TD> + <TD>RTL to LTL</TD> + <TD><A HREF="html/compcert.backend.Allocation.html">Allocation</A></TD> + <TD><A HREF="html/compcert.backend.Allocproof.html">Allocproof</A></TD> +</TR> + +<TR valign="top"> + <TD>Branch tunneling</TD> + <TD>LTL to LTL</TD> + <TD><A HREF="html/compcert.backend.Tunneling.html">Tunneling</A></TD> + <TD><A HREF="html/compcert.backend.Tunnelingproof.html">Tunnelingproof</A></TD> +</TR> + +<TR valign="top"> + <TD>Linearization of the CFG</TD> + <TD>LTL to Linear</TD> + <TD><A HREF="html/compcert.backend.Linearize.html">Linearize</A></TD> + <TD><A HREF="html/compcert.backend.Linearizeproof.html">Linearizeproof</A></TD> +</TR> + +<TR valign="top"> + <TD>Removal of unreferenced labels</TD> + <TD>Linear to Linear</TD> + <TD><A HREF="html/compcert.backend.CleanupLabels.html">CleanupLabels</A></TD> + <TD><A HREF="html/compcert.backend.CleanupLabelsproof.html">CleanupLabelsproof</A></TD> +</TR> + +<TR valign="top"> + <TD>Synthesis of debugging information</TD> + <TD>Linear to Linear</TD> + <TD><A HREF="html/compcert.backend.Debugvar.html">Debugvar</A></TD> + <TD><A HREF="html/compcert.backend.Debugvarproof.html">Debugvarproof</A></TD> +</TR> + +<TR valign="top"> + <TD>Laying out the activation records</TD> + <TD>Linear to Mach</TD> + <TD><A HREF="html/compcert.backend.Stacking.html">Stacking</A><BR> + <A HREF="html/compcert.backend.Bounds.html">Bounds</A><BR> + <A HREF="html/compcert.kvx.Stacklayout.html"><I>Stacklayout</I></A></TD> + <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 KVX VLIW</H4> +<TABLE cellpadding="5%"> +<TR valign="top"> + <TD>Reconstruction of basic-blocks at Mach level</TD> + <TD>Mach to Machblock</TD> + <TD><A HREF="html/compcert.kvx.lib.Machblockgen.html">Machblockgen</A></TD> + <TD><A HREF="html/compcert.kvx.lib.ForwardSimulationBlock.html">ForwardSimulationBlock</A><BR> + <A HREF="html/compcert.kvx.lib.Machblockgenproof.html">Machblockgenproof</A></TD> +</TR> + +<TR valign="top"> + <TD>Emission of purely sequential assembly code</TD> + <TD>Machblock to Asmblock</TD> + <TD><A HREF="html/compcert.kvx.Asmblockgen.html"><I>Asmblockgen</I></A></TD> + <TD><A HREF="html/compcert.kvx.lib.Asmblockgenproof0.html"><I>Asmblockgenproof0</I></A><BR> + <A HREF="html/compcert.kvx.Asmblockgenproof1.html"><I>Asmblockgenproof1</I></A><BR> + <A HREF="html/compcert.kvx.Asmblockgenproof.html"><I>Asmblockgenproof</I></A></TD> +</TR> + +<TR valign="top"> + <TD>Bundling (and basic-block scheduling)</TD> + <TD>Asmblock to Asmvliw</TD> + <TD><A HREF="html/compcert.kvx.PostpassScheduling.html"><I>PostpassScheduling</I></A> using<BR> + <A HREF="html/compcert.kvx.Asmblockdeps.html"><I>Asmblockdeps</I></A> and the <tt>abstractbb</tt> library</TD> + <TD><A HREF="html/compcert.kvx.PostpassSchedulingproof.html"><I>PostpassSchedulingproof</I></A></TD> +</TR> + +<TR valign="top"> + <TD>Flattening bundles (only a bureaucratic operation)</TD> + <TD>Asmvliw to Asm</TD> + <TD><A HREF="html/compcert.kvx.Asmgen.html"><I>Asmgen</I></A></TD> + <TD><A HREF="html/compcert.kvx.Asmgenproof.html"><I>Asmgenproof</I></A> (whole simulation proof from <tt>Mach</tt> to <tt>Asm</tt>)</TD> +</TR> +</TABLE> + +<font color=gray> +<H3>All together</H3> + +<UL> +<LI> <A HREF="html/compcert.driver.Compiler.html">Compiler</A>: composing the passes together; +whole-compiler semantic preservation theorems. +<LI> <A HREF="html/compcert.driver.Complements.html">Complements</A>: interesting consequences of the semantic preservation theorems. +</UL> + +<H3>Static analyses</H3> + +The following static analyses are performed over the RTL intermediate +representation to support optimizations such as constant propagation, +CSE, and dead code elimination. +<UL> +<LI> <A HREF="html/compcert.backend.Liveness.html">Liveness</A>: liveness analysis</A>. +<LI> <A HREF="html/compcert.backend.ValueAnalysis.html">ValueAnalysis</A>: value and alias analysis</A> <BR> +See also: <A HREF="html/compcert.backend.ValueDomain.html">ValueDomain</A>: the abstract domain for value analysis.<BR> +See also: <A HREF="html/compcert.kvx.ValueAOp.html"><I>ValueAOp</I></A>: processor-dependent parts of value analysis. +<LI> <A HREF="html/compcert.backend.Deadcode.html">Deadcode</A>: neededness analysis</A> <BR> +See also: <A HREF="html/compcert.backend.NeedDomain.html">NeedDomain</A>: the abstract domain for neededness analysis.<BR> +See also: <A HREF="html/compcert.kvx.NeedOp.html"><I>NeedOp</I></A>: processor-dependent parts of neededness analysis. +</UL> + +<H3>Type systems</H3> + +The <A HREF="html/compcert.cfrontend.Ctyping.html">type system of CompCert C</A> is fully formalized. For some intermediate languages of the back-end, simpler type systems are used to statically capture well-formedness conditions. +<UL> +<LI> <A HREF="html/compcert.cfrontend.Ctyping.html">Ctyping</A>: typing for CompCert C + type-checking functions. +<LI> <A HREF="html/compcert.backend.RTLtyping.html">RTLtyping</A>: typing for RTL + type +reconstruction. +<LI> <A HREF="html/compcert.backend.Lineartyping.html">Lineartyping</A>: typing for Linear. +</UL> +</font> + +</BODY> +</HTML> |