diff options
| -rw-r--r-- | Changelog | 34 | ||||
| -rw-r--r-- | README | 21 |
2 files changed, 43 insertions, 12 deletions
@@ -1,6 +1,21 @@ 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 |