Commit fd6bc311 authored by xleroy's avatar xleroy
Browse files

Update for release 1.8

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1512 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
parent 771e05d4
Release 1.8
===========
Release 1.8, 2010-09-21
=======================
- The input language to the proved part of the compiler is no longer
Clight but CompCert C: a larger subset of the C language supporting
in particular side-effects within expressions. The transformation
that pulls side effects out of expressions, formerly performed by
untrusted Caml code, is now fully proved in Coq.
in particular side-effects within expressions. The transformations
that pull side effects out of expressions and materialize implicit
casts, formerly performed by untrusted Caml code, are now fully
proved in Coq.
- New port targeting Intel/AMD x86 processors. Generates 32-bit x86 code
using SSE2 extensions for floating-point arithmetic. Works under
Linux, *BSD, MacOS X, and the Cygwin environment for Windows.
Linux, MacOS X, and the Cygwin environment for Windows.
CompCert's compilation strategy is not a very good match for the
x86 architecture, therefore the performance of the generated code
is not as good as for the PowerPC port, but still usable.
......
......@@ -3,7 +3,7 @@
OVERVIEW:
The Compcert verified compiler is a compiler for a large subset of the
C programming language that generates code for the PowerPC and ARM
C programming language that generates code for the PowerPC, ARM and x86
processors.
The distinguishing feature of Compcert is that it has been formally
......@@ -36,12 +36,14 @@ SUPPORTED PLATFORMS:
- PowerPC / Linux [somewhat experimental]
For PowerPC machines running the Linux operating system.
- IA32 / Linux or MacOS or Windows+Cygwin [experimental]
For Intel/AMD x86 processors with SSE2 extensions
(i.e. Pentium 4 and later), running either Linux, MacOS 10.6,
or Windows with the Cygwin environment (http://www.cygwin.com/).
- ARM / Linux [experimental]
For ARM machines running the Linux operating system.
- IA32 / Linux, BSD, MacOS [experimental]
For Intel/AMD x86 processors with SSE2 extensions
(i.e. Pentium 4 and later).
PREREQUISITES:
......@@ -55,6 +57,19 @@ PREREQUISITES:
* The Caml functional language, version 3.10 or later.
Caml is free software, available from http://caml.inria.fr/
* Under MacOS 10.5 and 10.6, some standard C include files in /usr/include/
contain gcc-isms that cause errors when compiling with CompCert.
Symptoms include:
- references to undefined types uint16_t and uint32_t
- a type error when using the "assert" macro.
These issues have been reported through Apple Developer's Connection.
Until Apple fixes them, you can apply the patch available from
http://compcert.inria.fr/release/MacOSX-includes.patch
Download this file, then do:
sudo /bin/bash
cd /
patch -p0 < ..../MacOSX-includes.patch
INSTALLATION:
......@@ -68,8 +83,8 @@ where <target> is one of:
ppc-linux (PowerPC, Linux)
arm-linux (ARM, Linux)
ia32-linux (x86 SSE2 32 bits, Linux)
ia32-bsd (x86 SSE2 32 bits, BSD)
ia32-macosx (x86 SSE2 32 bits, MacOS X)
ia32-cygwin (x86 SSE2 32 bits, Cygwin environment for Windows)
This generates the Makefile.config file in the top directory.
......@@ -92,8 +107,9 @@ The "configure" script accepts the following options:
This re-checks all the Coq proofs, then extracts Caml code from the
Coq specification and combines it with supporting hand-written Caml
code to generate the executable for Compcert. This step takes 10 to
15 minutes on a recent Mac computer; be patient.
code to generate the executable for Compcert. This step takes 20
minutes or so on a recent machine; be patient.
3- You can now install Compcert. This will create the "ccomp" command
in the binary directory selected during configuration, and install
......
......@@ -24,12 +24,12 @@ 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.7, 2010-03-31</H3>
<H3 align="center">Version 1.8, 2010-09-21</H3>
<H2>Introduction</H2>
<P>Compcert is a compiler that generates PowerPC and ARM assembly
code from Clight, a large subset of the C programming language.
<P>Compcert is a compiler that generates PowerPC, ARM 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
......@@ -104,7 +104,7 @@ semantics.
<H3>Source, intermediate and target languages: syntax and semantics</H3>
<UL>
<LI> The Cmedium source language:
<LI> The Compcert C source language:
<A HREF="html/Csyntax.html">syntax</A> and
<A HREF="html/Csem.html">semantics</A> and
<A HREF="html/Cstrategy.html">determinized semantics</A>.
......@@ -149,7 +149,7 @@ code.
<TR valign="top">
<TD>Pulling side-effects out of expressions;<br>
fixing an evaluation order</TD>
<TD>Cmedium to Clight</TD>
<TD>Compcert C to Clight</TD>
<TD><A HREF="html/SimplExpr.html">SimplExpr</A></TD>
<TD><A HREF="html/SimplExprspec.html">SimplExprspec</A><br>
<A HREF="html/SimplExprproof.html">SimplExprproof</A></TD>
......@@ -210,6 +210,13 @@ code.
<TD><A HREF="html/CSEproof.html">CSEproof</A></TD>
</TR>
<TR valign="top">
<TD>Elimination of redundant casts</TD>
<TD>RTL to RTL</TD>
<TD><A HREF="html/CastOptim.html">CastOptim</A></TD>
<TD><A HREF="html/CastOptimproof.html">CastOptimproof</A></TD>
</TR>
<TR valign="top">
<TD>Register allocation by coloring<br>of an interference graph</TD>
<TD>RTL to LTL</TD>
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment