Commit 28c04de6 authored by xleroy's avatar xleroy
Browse files

Updated

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1505 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
parent 812e142e
Release 1.8
===========
- 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.
- 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.
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.
(About 75% of the performance of gcc -O1 for x86, compared with
> 90% for PowerPC.)
- More faithful semantics for volatile accesses:
. volatile reads and writes from a volatile global variable are treated
like input and output system calls (respectively), bypassing
......@@ -8,13 +23,11 @@ Release 1.8
. volatile reads and writes from other locations are treated like
regular loads and stores.
- Added "fabs" (floating-point absolute value) unary operator to Clight;
map __builtin_fabs() to this operator.
- Introduced __builtin_memcpy() and __builtin_memcpy_words, use them
- Introduced __builtin_memcpy() and __builtin_memcpy_words(), use them
instead of memcpy() to compile struct and union assignments.
- Better instruction selection for "globvar[expr + cst]" memory accesses.
- Introduced __builtin_annotation() to transmit assertions from
the source program all the way to the generated assembly code.
- Elimination of some useless casts around "&", "|" and "^" bitwise operators.
......@@ -22,11 +35,14 @@ Release 1.8
rest of compilation and slightly improves the result of register
allocation when register pressure is high.
- Implemented a spilling heuristic during register allocation.
This heuristic reduces significantly the amount of spill code
generated when register pressure is high.
- Improvements in register allocation:
. Implemented a spilling heuristic during register allocation.
This heuristic reduces significantly the amount of spill code
generated when register pressure is high.
. More coalescing between low-pressure and high-pressure variables.
. Aggressive coalescing between pairs of spilled variables.
- Implemented aggressive coalescing between pairs of spilled variables.
- Fixed some bugs in the emulation of bit fields.
Release 1.7.1, 2010-04-13
......
......@@ -39,6 +39,9 @@ SUPPORTED PLATFORMS:
- 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:
......@@ -46,7 +49,7 @@ PREREQUISITES:
the search path. For MacOS X, you can get them by installing the
XCode development tools, as found on the installation DVDs.
* The Coq proof assistant, version 8.2-1 or later.
* The Coq proof assistant, version 8.2pl1 or 8.2pl2.
Coq is free software, available from http://coq.inria.fr/
* The Caml functional language, version 3.10 or later.
......@@ -64,6 +67,9 @@ where <target> is one of:
ppc-macosx (PowerPC, MacOS X)
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)
This generates the Makefile.config file in the top directory.
......@@ -74,6 +80,7 @@ The "configure" script accepts the following options:
-libdir <dir> (default: /usr/local/lib/compcert)
Directory where the Compcert support library will be installed
(needed only under MacOS X)
-prefix <dir> (default: /usr/local)
Set bindir and libdir to
......@@ -143,7 +150,7 @@ Preprocessing options:
-U<symb> Undefine preprocessor symbol
Language support options (use -fno-<opt> to turn off -f<opt>) :
-fbitfields Emulate bit fields in structs [off]
-flonglong Treat 'long long' as 'long' and 'long double' as 'double' [off]
-flonglong Partial emulation of 'long long' types [on]
-fstruct-passing Emulate passing structs and unions by value [off]
-fstruct-assign Emulate assignment between structs or unions [off]
-fvararg-calls Emulate calls to variable-argument functions [on]
......@@ -153,14 +160,22 @@ Code generation options:
-fsmall-const <n> Set maximal size <n> for allocation in small constant area
Tracing options:
-dparse Save C file after parsing and elaboration in <file>.parse.c
-dc Save generated Compcert C in <file>.compcert.c
-dclight Save generated Clight in <file>.light.c
-dcminor Save generated Cminor in <file>.cm
-drtl Save unoptimized generated RTL in <file>.rtl
-dtailcall Save RTL after tail call optimization in <file>.tailcall.rtl
-dcastopt Save RTL after cast optimization in <file>.castopt.rtl
-dconstprop Save RTL after constant propagation in <file>.constprop.rtl
-dcse Save RTL after CSE optimization in <file>.cse.rtl
-dalloc Save LTL after register allocation in <file>.alloc.ltl
-dasm Save generated assembly in <file>.s
Linking options:
-l<lib> Link library <lib>
-L<dir> Add <dir> to search path for libraries
-o <file> Generate executable in <file> (default: a.out)
General options:
-stdlib <dir> Set the path of the Compcert run-time library
-stdlib <dir> Set the path of the Compcert stdlib wrappers
-v Print external commands before invoking them
......
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