diff options
| -rw-r--r-- | Changelog | 13 | ||||
| -rw-r--r-- | README | 30 | ||||
| -rw-r--r-- | doc/index.html | 17 |
3 files changed, 42 insertions, 18 deletions
@@ -1,15 +1,16 @@ -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 diff --git a/doc/index.html b/doc/index.html index 07ab0ff..67b821f 100644 --- a/doc/index.html +++ b/doc/index.html @@ -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> @@ -211,6 +211,13 @@ code. </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> <TD><A HREF="html/InterfGraph.html">InterfGraph</A><BR> |