aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-09-10 17:58:27 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-09-10 17:58:27 +0200
commit70cc8540ed308d26b4c211a291fef66f942b8431 (patch)
tree7a486af46be48b984d679dae628cc1a5be6cc096
parent61aefbc6413df9eaad1d1e93d8f4ea95ab8a0bcf (diff)
parent5b6c019a507688dfcf63b9ef54f7731137422ab5 (diff)
downloadcompcert-kvx-70cc8540ed308d26b4c211a291fef66f942b8431.tar.gz
compcert-kvx-70cc8540ed308d26b4c211a291fef66f942b8431.zip
Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
Diffstat
-rw-r--r--doc/index-mppa_k1c.html380
-rw-r--r--mppa_k1c/Asmvliw.v13
-rw-r--r--mppa_k1c/TargetPrinter.ml4
-rw-r--r--runtime/include/ccomp_k1c_fixes.h6
-rw-r--r--test/c/Makefile23
-rw-r--r--test/c/Results/binarytrees12
-rw-r--r--test/c/Results/fannkuch62
-rw-r--r--test/c/Results/fft2
-rw-r--r--test/c/Results/fftsp2
-rw-r--r--test/c/Results/fib2
-rw-r--r--test/c/Results/integr2
-rw-r--r--test/c/Results/knucleotide27
-rw-r--r--test/c/binarytrees.c4
-rw-r--r--test/c/fannkuch.c6
-rw-r--r--test/c/fft.c5
-rw-r--r--test/c/fftsp.c2
-rw-r--r--test/c/fftw.c2
-rw-r--r--test/c/fib.c4
-rw-r--r--test/c/integr.c2
-rw-r--r--test/c/knucleotide.c6
-rw-r--r--test/c/lists.c5
-rw-r--r--test/c/qsort.c2
-rw-r--r--test/mppa/coverage_helper.py2
-rw-r--r--test/mppa/instr/i32.c48
-rw-r--r--test/mppa/instr/i64.c43
25 files changed, 559 insertions, 107 deletions
diff --git a/doc/index-mppa_k1c.html b/doc/index-mppa_k1c.html
new file mode 100644
index 00000000..41a44a0d
--- /dev/null
+++ b/doc/index-mppa_k1c.html
@@ -0,0 +1,380 @@
+<!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>
+
+<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>
+
+<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>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>
+
+<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>
+
+<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.mppa_k1c.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.mppa_k1c.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.
+<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.
+<LI> <A HREF="html/compcert.mppa_k1c.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.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>
+
+<TABLE cellpadding="5%">
+<TR valign="top">
+ <TH>Pass</TH>
+ <TH>Source &amp; target</TH>
+ <TH>Compiler&nbsp;code</TH>
+ <TH>Correctness&nbsp;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.mppa_k1c.SelectOp.html"><I>SelectOp</I></A><br>
+ <A HREF="html/compcert.mppa_k1c.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.mppa_k1c.SelectOpproof.html"><I>SelectOpproof</I></A><br>
+ <A HREF="html/compcert.mppa_k1c.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.mppa_k1c.ConstpropOp.html"><I>ConstpropOp</I></A></TD>
+ <TD><A HREF="html/compcert.backend.Constpropproof.html">Constpropproof</A><br>
+ <A HREF="html/compcert.mppa_k1c.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.mppa_k1c.CombineOp.html"><I>CombineOp</I></A></TD>
+ <TD><A HREF="html/compcert.backend.CSEproof.html">CSEproof</A><BR>
+ <A HREF="html/compcert.mppa_k1c.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.mppa_k1c.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>
+
+<TR valign="top">
+ <TD>Reconstruction of basic-blocks at Mach level</TD>
+ <TD>Mach to Machblock</TD>
+ <TD><A HREF="html/compcert.mppa_k1c.lib.Machblockgen.html">Machblockgen</A></TD>
+ <TD><A HREF="html/compcert.mppa_k1c.lib.ForwardSimulationBlock.html">ForwardSimulationBlock</A><BR>
+ <A HREF="html/compcert.mppa_k1c.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.mppa_k1c.Asmblockgen.html"><I>Asmblockgen</I></A></TD>
+ <TD><A HREF="html/compcert.mppa_k1c.Asmblockgenproof0.html"><I>Asmblockgenproof0</I></A><BR>
+ <A HREF="html/compcert.mppa_k1c.Asmblockgenproof1.html"><I>Asmblockgenproof1</I></A><BR>
+ <A HREF="html/compcert.mppa_k1c.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.mppa_k1c.PostpassScheduling.html"><I>PostpassScheduling</I></A> using<BR>
+ <A HREF="html/compcert.mppa_k1c.Asmblockdeps.html"><I>Asmblockdeps</I></A> and the <tt>abstractbb</tt> library</TD>
+ <TD><A HREF="html/compcert.mppa_k1c.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.mppa_k1c.Asmgen.html"><I>Asmgen</I></A></TD>
+ <TD><A HREF="html/compcert.mppa_k1c.Asmgenproof.html"><I>Asmgenproof</I></A></TD>
+</TR>
+</TABLE>
+
+<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.mppa_k1c.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.mppa_k1c.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>
+
+<HR>
+<ADDRESS>Xavier.Leroy@inria.fr</ADDRESS>
+<HR>
+
+</BODY>
+</HTML>
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index 54654abb..54e9c847 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -203,11 +203,6 @@ Inductive itest: Type :=
| ITgeu (**r Greater Than or Equal Unsigned *)
| ITleu (**r Less Than or Equal Unsigned *)
| ITgtu (**r Greater Than Unsigned *)
- (* Not used yet *)
- | ITall (**r All Bits Set in Mask *)
- | ITnall (**r Not All Bits Set in Mask *)
- | ITany (**r Any Bits Set in Mask *)
- | ITnone (**r Not Any Bits Set in Mask *)
.
Inductive ftest: Type :=
@@ -909,10 +904,6 @@ Definition compare_int (t: itest) (v1 v2: val): val :=
| ITgeu => Val_cmpu Cge v1 v2
| ITleu => Val_cmpu Cle v1 v2
| ITgtu => Val_cmpu Cgt v1 v2
- | ITall
- | ITnall
- | ITany
- | ITnone => Vundef
end.
Definition compare_long (t: itest) (v1 v2: val): val :=
@@ -929,10 +920,6 @@ Definition compare_long (t: itest) (v1 v2: val): val :=
| ITgeu => Some (Val_cmplu Cge v1 v2)
| ITleu => Some (Val_cmplu Cle v1 v2)
| ITgtu => Some (Val_cmplu Cgt v1 v2)
- | ITall
- | ITnall
- | ITany
- | ITnone => Some Vundef
end in
match res with
| Some v => v
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 5618875f..0c179a07 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -262,10 +262,6 @@ module Target (*: TARGET*) =
| ITgeu -> "geu"
| ITleu -> "leu"
| ITgtu -> "gtu"
- | ITall -> "all"
- | ITnall -> "nall"
- | ITany -> "any"
- | ITnone -> "none"
let icond oc c = fprintf oc "%s" (icond_name c)
diff --git a/runtime/include/ccomp_k1c_fixes.h b/runtime/include/ccomp_k1c_fixes.h
index 5c543d8f..718ac3e5 100644
--- a/runtime/include/ccomp_k1c_fixes.h
+++ b/runtime/include/ccomp_k1c_fixes.h
@@ -17,6 +17,12 @@ extern __int128 __compcert_acswapd(void *address, unsigned long long new_value,
#define __builtin_k1_acswapw __compcert_acswapw
extern __int128 __compcert_acswapw(void *address, unsigned long long new_value, unsigned long long old_value);
+
+#define __builtin_k1_afaddd __compcert_afaddd
+extern long long __compcert_afaddd(void *address, unsigned long long incr);
+
+#define __builtin_k1_afaddw __compcert_afaddw
+extern int __compcert_afaddw(void *address, unsigned int incr);
#endif
#define __builtin_expect(x, y) (x)
diff --git a/test/c/Makefile b/test/c/Makefile
index 14c856ff..9580c8cc 100644
--- a/test/c/Makefile
+++ b/test/c/Makefile
@@ -3,18 +3,22 @@ include ../../Makefile.config
CCOMP=../../ccomp
CCOMPFLAGS=$(CCOMPOPTS) -stdlib ../../runtime -dc -dclight -dasm
-CFLAGS+=-O1 -Wall
+CFLAGS+=-O2 -Wall
+EXECUTE:=timeout --signal=SIGTERM 90s $(EXECUTE)
LIBS=$(LIBMATH)
#TIME=xtime -o /dev/null -mintime 2.0 # Xavier's hack
TIME=time >/dev/null # Otherwise
-PROGS?=fib qsort fftw sha1 sha3 aes \
- lists binarytrees fannkuch \
- nsieve nsievebits vmach \
- chomp perlin siphash24\
- integr fft fftsp almabench knucleotide mandelbrot nbody spectral bisect
+PROGS?=fib integr qsort fft fftsp fftw sha1 sha3 aes almabench \
+ lists binarytrees fannkuch mandelbrot nbody \
+ nsieve nsievebits spectral vmach \
+ bisect chomp perlin siphash24
+
+# Kalray NOTE : removed knucleotide from PROGS, it is hard to edit the input
+# to modify its size without resulting in a seg fault, and the base input
+# takes a too long time to complete in the simulator.
all: $(PROGS:%=%.compcert)
@@ -33,7 +37,8 @@ all_gcc: $(PROGS:%=%.gcc)
test: all
@for i in $(PROGS); do \
- if $(EXECUTE) ./$$i.compcert | cmp -s - Results/$$i; \
+ $(EXECUTE) ./$$i.compcert > $$i.compcert.out;\
+ if cmp -s $$i.compcert.out Results/$$i; \
then echo "$$i: passed"; \
else echo "$$i: FAILED"; exit 2; \
fi; \
@@ -41,7 +46,8 @@ test: all
test_gcc: all_gcc
@for i in $(PROGS); do \
- if $(EXECUTE) ./$$i.gcc | cmp -s - Results/$$i; \
+ $(EXECUTE) ./$$i.gcc > $$i.gcc.out;\
+ if cmp -s $$i.gcc.out Results/$$i; \
then echo "$$i: passed"; \
else echo "$$i: FAILED"; \
fi; \
@@ -60,3 +66,4 @@ bench: all
clean:
rm -f *.compcert *.gcc
rm -f *.compcert.c *.light.c *.parsed.c *.s *.o *.sdump *~
+ rm -f *.out
diff --git a/test/c/Results/binarytrees b/test/c/Results/binarytrees
index 9dfe1355..db0f0ef7 100644
--- a/test/c/Results/binarytrees
+++ b/test/c/Results/binarytrees
@@ -1,7 +1,5 @@
-stretch tree of depth 13 check: -1
-8192 trees of depth 4 check: -8192
-2048 trees of depth 6 check: -2048
-512 trees of depth 8 check: -512
-128 trees of depth 10 check: -128
-32 trees of depth 12 check: -32
-long lived tree of depth 12 check: -1
+stretch tree of depth 9 check: -1
+512 trees of depth 4 check: -512
+128 trees of depth 6 check: -128
+32 trees of depth 8 check: -32
+long lived tree of depth 8 check: -1
diff --git a/test/c/Results/fannkuch b/test/c/Results/fannkuch
index be1815d4..dac06137 100644
--- a/test/c/Results/fannkuch
+++ b/test/c/Results/fannkuch
@@ -1,31 +1,31 @@
-12345678910
-21345678910
-23145678910
-32145678910
-31245678910
-13245678910
-23415678910
-32415678910
-34215678910
-43215678910
-42315678910
-24315678910
-34125678910
-43125678910
-41325678910
-14325678910
-13425678910
-31425678910
-41235678910
-14235678910
-12435678910
-21435678910
-24135678910
-42135678910
-23451678910
-32451678910
-34251678910
-43251678910
-42351678910
-24351678910
-Pfannkuchen(10) = 38
+12345678
+21345678
+23145678
+32145678
+31245678
+13245678
+23415678
+32415678
+34215678
+43215678
+42315678
+24315678
+34125678
+43125678
+41325678
+14325678
+13425678
+31425678
+41235678
+14235678
+12435678
+21435678
+24135678
+42135678
+23451678
+32451678
+34251678
+43251678
+42351678
+24351678
+Pfannkuchen(8) = 22
diff --git a/test/c/Results/fft b/test/c/Results/fft
index a48608b0..cbeb0999 100644
--- a/test/c/Results/fft
+++ b/test/c/Results/fft
@@ -1 +1 @@
-262144 points, result OK
+4096 points, result OK
diff --git a/test/c/Results/fftsp b/test/c/Results/fftsp
index cbeb0999..36264416 100644
--- a/test/c/Results/fftsp
+++ b/test/c/Results/fftsp
@@ -1 +1 @@
-4096 points, result OK
+64 points, result OK
diff --git a/test/c/Results/fib b/test/c/Results/fib
index 84ce6474..d8beea8c 100644
--- a/test/c/Results/fib
+++ b/test/c/Results/fib
@@ -1 +1 @@
-fib(35) = 14930352
+fib(26) = 196418
diff --git a/test/c/Results/integr b/test/c/Results/integr
index 973806c9..bb755482 100644
--- a/test/c/Results/integr
+++ b/test/c/Results/integr
@@ -1 +1 @@
-integr(square, 0.0, 1.0, 10000000) = 0.333333
+integr(square, 0.0, 1.0, 1000000) = 0.333333
diff --git a/test/c/Results/knucleotide b/test/c/Results/knucleotide
index d13ae7dc..e69de29b 100644
--- a/test/c/Results/knucleotide
+++ b/test/c/Results/knucleotide
@@ -1,27 +0,0 @@
-A 30.284
-T 29.796
-C 20.312
-G 19.608
-
-AA 9.212
-AT 8.950
-TT 8.948
-TA 8.936
-CA 6.166
-CT 6.100
-AC 6.086
-TC 6.042
-AG 6.036
-GA 5.968
-TG 5.868
-GT 5.798
-CC 4.140
-GC 4.044
-CG 3.906
-GG 3.798
-
-562 GGT
-152 GGTA
-15 GGTATT
-0 GGTATTTTAATT
-0 GGTATTTTAATTTATAGT
diff --git a/test/c/binarytrees.c b/test/c/binarytrees.c
index b4b10232..f2921d9a 100644
--- a/test/c/binarytrees.c
+++ b/test/c/binarytrees.c
@@ -7,6 +7,7 @@
icc -O3 -ip -unroll -static binary-trees.c -lm
*/
+#include <assert.h>
#include <math.h>
#include <stdio.h>
#include <stdlib.h>
@@ -24,6 +25,7 @@ treeNode* NewTreeNode(treeNode* left, treeNode* right, long item)
treeNode* new;
new = (treeNode*)malloc(sizeof(treeNode));
+ assert(new != NULL && "NewTreeNode: new malloc failed");
new->left = left;
new->right = right;
@@ -73,7 +75,7 @@ int main(int argc, char* argv[])
unsigned N, depth, minDepth, maxDepth, stretchDepth;
treeNode *stretchTree, *longLivedTree, *tempTree;
- N = argc < 2 ? 12 : atol(argv[1]);
+ N = argc < 2 ? 8 : atol(argv[1]);
minDepth = 4;
diff --git a/test/c/fannkuch.c b/test/c/fannkuch.c
index 9cc7a693..ddaa7309 100644
--- a/test/c/fannkuch.c
+++ b/test/c/fannkuch.c
@@ -8,6 +8,7 @@
* $Id: fannkuch-gcc.code,v 1.33 2006/02/25 16:38:58 igouy-guest Exp $
*/
+#include <assert.h>
#include <stdio.h>
#include <stdlib.h>
@@ -31,8 +32,11 @@ fannkuch( int n )
if( n < 1 ) return 0;
perm = calloc(n, sizeof(*perm ));
+ assert(perm != NULL && "fannkuch: perm malloc failed");
perm1 = calloc(n, sizeof(*perm1));
+ assert(perm != NULL && "fannkuch: perm1 malloc failed");
count = calloc(n, sizeof(*count));
+ assert(perm != NULL && "fannkuch: count malloc failed");
for( i=0 ; i<n ; ++i ) perm1[i] = i; /* initial (trivial) permu */
@@ -98,7 +102,7 @@ fannkuch( int n )
int
main( int argc, char* argv[] )
{
- int n = (argc>1) ? atoi(argv[1]) : 10;
+ int n = (argc>1) ? atoi(argv[1]) : 8;
printf("Pfannkuchen(%d) = %ld\n", n, fannkuch(n));
return 0;
diff --git a/test/c/fft.c b/test/c/fft.c
index 2bd55a18..f91f5300 100644
--- a/test/c/fft.c
+++ b/test/c/fft.c
@@ -3,6 +3,7 @@
by: Dave Edelblute, edelblut@cod.nosc.mil, 05 Jan 1993
*/
+#include <assert.h>
#include <math.h>
#include <stdlib.h>
#include <stdio.h>
@@ -151,13 +152,15 @@ int main(int argc, char ** argv)
double enp, t, y, z, zr, zi, zm, a;
double * xr, * xi, * pxr, * pxi;
- if (argc >= 2) n = atoi(argv[1]); else n = 18;
+ if (argc >= 2) n = atoi(argv[1]); else n = 12;
np = 1 << n;
enp = np;
npm = np / 2 - 1;
t = PI / enp;
xr = calloc(np, sizeof(double));
+ assert(xr != NULL && "xr calloc failed");
xi = calloc(np, sizeof(double));
+ assert(xi != NULL && "xi calloc failed");
pxr = xr;
pxi = xi;
for (nruns = 0; nruns < NRUNS; nruns++) {
diff --git a/test/c/fftsp.c b/test/c/fftsp.c
index 26b18b62..316ef714 100644
--- a/test/c/fftsp.c
+++ b/test/c/fftsp.c
@@ -153,7 +153,7 @@ int main(int argc, char ** argv)
float enp, t, y, z, zr, zi, zm, a;
float * xr, * xi, * pxr, * pxi;
- if (argc >= 2) n = atoi(argv[1]); else n = 12;
+ if (argc >= 2) n = atoi(argv[1]); else n = 6;
np = 1 << n;
enp = np;
npm = np / 2 - 1;
diff --git a/test/c/fftw.c b/test/c/fftw.c
index 913091d9..1d5b6526 100644
--- a/test/c/fftw.c
+++ b/test/c/fftw.c
@@ -74,7 +74,7 @@ const E KP1_847759065 = ((E) +1.847759065022573512256366378793576573644833252);
/* Test harness */
-#define NRUNS (100 * 1000)
+#define NRUNS (100 * 10)
int main()
{
diff --git a/test/c/fib.c b/test/c/fib.c
index 19548415..77aa7bb9 100644
--- a/test/c/fib.c
+++ b/test/c/fib.c
@@ -12,11 +12,7 @@ int fib(int n)
int main(int argc, char ** argv)
{
int n, r;
-#ifdef __K1C_COS__
if (argc >= 2) n = atoi(argv[1]); else n = 26;
-#else
- if (argc >= 2) n = atoi(argv[1]); else n = 35;
-#endif
r = fib(n);
printf("fib(%d) = %d\n", n, r);
return 0;
diff --git a/test/c/integr.c b/test/c/integr.c
index 882325c3..9c762297 100644
--- a/test/c/integr.c
+++ b/test/c/integr.c
@@ -25,7 +25,7 @@ double test(int n)
int main(int argc, char ** argv)
{
int n; double r;
- if (argc >= 2) n = atoi(argv[1]); else n = 10000000;
+ if (argc >= 2) n = atoi(argv[1]); else n = 1000000;
r = test(n);
printf("integr(square, 0.0, 1.0, %d) = %g\n", n, r);
return 0;
diff --git a/test/c/knucleotide.c b/test/c/knucleotide.c
index 3ac469be..1982834e 100644
--- a/test/c/knucleotide.c
+++ b/test/c/knucleotide.c
@@ -8,6 +8,7 @@
http://cvs.alioth.debian.org/cgi-bin/cvsweb.cgi/shootout/bench/Include/?cvsroot=shootout
*/
+#include <assert.h>
#include <stdio.h>
#include <string.h>
#include <ctype.h>
@@ -76,9 +77,11 @@ struct ht_node *ht_node_create(char *key) {
struct ht_ht *ht_create(int size) {
int i = 0;
struct ht_ht *ht = (struct ht_ht *)malloc(sizeof(struct ht_ht));
+ assert (ht != NULL && "ht_create: ht malloc failed");
while (ht_prime_list[i] < size) { i++; }
ht->size = ht_prime_list[i];
ht->tbl = (struct ht_node **)calloc(ht->size, sizeof(struct ht_node *));
+ assert (ht->tbl != NULL && "ht_create: ht->tbl calloc failed");
ht->iter_index = 0;
ht->iter_next = 0;
ht->items = 0;
@@ -250,6 +253,7 @@ write_frequencies (int fl, char *buffer, long buflen)
size++;
}
s = calloc (size, sizeof (sorter));
+ assert(s != NULL && "write_frequencies: s alloc failed");
i = 0;
for (nd = ht_first (ht); nd != NULL; nd = ht_next (ht))
{
@@ -293,6 +297,7 @@ main ()
FILE * f;
line = malloc (256);
+ assert (line != NULL && "line alloc failed");
if (!line)
return 2;
seqlen = 0;
@@ -308,6 +313,7 @@ main ()
buflen = 10240;
buffer = malloc (buflen + 1);
+ assert (buffer != NULL && "buffer alloc failed");
if (!buffer)
return 2;
x = buffer;
diff --git a/test/c/lists.c b/test/c/lists.c
index ced384c0..d1c67954 100644
--- a/test/c/lists.c
+++ b/test/c/lists.c
@@ -1,5 +1,6 @@
/* List manipulations */
+#include <assert.h>
#include <stdio.h>
#include <stddef.h>
#include <stdlib.h>
@@ -11,6 +12,7 @@ struct list * buildlist(int n)
struct list * r;
if (n < 0) return NULL;
r = malloc(sizeof(struct list));
+ assert(r != NULL && "buildlist: r malloc failed");
r->hd = n;
r->tl = buildlist(n - 1);
return r;
@@ -21,6 +23,7 @@ struct list * reverselist (struct list * l)
struct list * r, * r2;
for (r = NULL; l != NULL; l = l->tl) {
r2 = malloc(sizeof(struct list));
+ assert(r2 != NULL && "reverselist: r2 malloc failed");
r2->hd = l->hd;
r2->tl = r;
r = r2;
@@ -58,7 +61,7 @@ int main(int argc, char ** argv)
int n, niter, i;
struct list * l;
- if (argc >= 2) n = atoi(argv[1]); else n = 1000;
+ if (argc >= 2) n = atoi(argv[1]); else n = 100;
if (argc >= 3) niter = atoi(argv[1]); else niter = 20000;
l = buildlist(n);
if (checklist(n, reverselist(l))) {
diff --git a/test/c/qsort.c b/test/c/qsort.c
index 66eef68d..a9d5757a 100644
--- a/test/c/qsort.c
+++ b/test/c/qsort.c
@@ -34,7 +34,7 @@ int main(int argc, char ** argv)
int n, i, j;
int * a, * b;
- if (argc >= 2) n = atoi(argv[1]); else n = 100000;
+ if (argc >= 2) n = atoi(argv[1]); else n = 10000;
a = malloc(n * sizeof(int));
b = malloc(n * sizeof(int));
for (j = 0; j < NITER; j++) {
diff --git a/test/mppa/coverage_helper.py b/test/mppa/coverage_helper.py
index cf7a84c9..e5b1907c 100644
--- a/test/mppa/coverage_helper.py
+++ b/test/mppa/coverage_helper.py
@@ -5,7 +5,7 @@ all_loads_stores = "lbs lbz lhz lo lq ld lhs lws sb sd sh so sq sw".split(" ")
all_bconds = "wnez weqz wltz wgez wlez wgtz dnez deqz dltz dgez dlez dgtz".split(" ")
-all_iconds = "ne eq lt ge le gt ltu geu leu gtu all nall any none".split(" ")
+all_iconds = "ne eq lt ge le gt ltu geu leu gtu".split(" ")
all_fconds = "one ueq oeq une olt uge oge ult".split(" ")
diff --git a/test/mppa/instr/i32.c b/test/mppa/instr/i32.c
index 4e389620..e350931c 100644
--- a/test/mppa/instr/i32.c
+++ b/test/mppa/instr/i32.c
@@ -28,6 +28,7 @@ BEGIN_TEST(int)
c = a+b;
c += a&b;
+ /* testing if, cb version */
if ((a & 0x1) == 1)
c += fact(1);
else
@@ -38,6 +39,11 @@ BEGIN_TEST(int)
else
c += fact(8);
+ if (a & 0x1 == 0)
+ c += fact(4);
+ else
+ c += fact(8);
+
b = !(a & 0x01);
if (!b)
c += fact(16);
@@ -67,6 +73,48 @@ BEGIN_TEST(int)
else
c += fact(8192);
+ /* cmoved version */
+ if ((a & 0x1) == 1)
+ c += 1;
+ else
+ c += 2;
+
+ if (a & 0x1 == 0)
+ c += 4;
+ else
+ c += 8;
+
+ if (a & 0x1 == 0)
+ c += 4;
+ else
+ c += 8;
+
+ b = !(a & 0x01);
+ if (!b)
+ c += 16;
+ else
+ c += 32;
+
+ if (0 > (a & 0x1) - 1)
+ c += 64;
+ else
+ c += 128;
+
+ if (0 >= (a & 0x1))
+ c += 256;
+ else
+ c += 512;
+
+ if ((a & 0x1) > 0)
+ c += 1024;
+ else
+ c += 2048;
+
+ if ((a & 0x1) - 1 >= 0)
+ c += 4096;
+ else
+ c += 8192;
+
c += ((a & 0x1) == (b & 0x1));
c += (a > b);
c += (a <= b);
diff --git a/test/mppa/instr/i64.c b/test/mppa/instr/i64.c
index dc5fa6ee..e869d93c 100644
--- a/test/mppa/instr/i64.c
+++ b/test/mppa/instr/i64.c
@@ -74,6 +74,7 @@ BEGIN_TEST(long long)
c += a^b;
c += (unsigned int) a;
+ /* Testing if, cb */
if (0 != (a & 0x1LL))
c += fact(1);
else
@@ -89,6 +90,12 @@ BEGIN_TEST(long long)
else
c += fact(32);
+ if ((unsigned long long)(a & 0x1LL) >= 1)
+ c += fact(18);
+ else
+ c += fact(31);
+
+
if (a-41414141 > 0)
c += fact(13);
else
@@ -109,6 +116,42 @@ BEGIN_TEST(long long)
else
c += fact(2048);
+ /* Testing if, cmoved */
+ if (0 != (a & 0x1LL))
+ c += 1;
+ else
+ c += 2;
+
+ if (0 > (a & 0x1LL))
+ c += 4;
+ else
+ c += 8;
+
+ if (0 >= (a & 0x1LL) - 1)
+ c += 16;
+ else
+ c += 32;
+
+ if (a-41414141 > 0)
+ c += 13;
+ else
+ c += 31;
+
+ if (a & 0x1LL > 0)
+ c += 64;
+ else
+ c += 128;
+
+ if ((a & 0x1LL) - 1 >= 0)
+ c += 256;
+ else
+ c += 512;
+
+ if (0 == (a & 0x1LL))
+ c += 1024;
+ else
+ c += 2048;
+
c += ((a & 0x1LL) == (b & 0x1LL));
c += (a >= b);
c += (a > b);
generated by cgit (git 2.34.1) at 2024-05-20 09:15:06 +0000