From 28c04de64220be15c589c4dbe1662b212b6d25b1 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Sep 2010 10:14:37 +0000 Subject: Updated git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1505 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- Changelog | 34 +++++++++++++++++++++++++--------- 1 file changed, 25 insertions(+), 9 deletions(-) (limited to 'Changelog') diff --git a/Changelog b/Changelog index 7a49998f..2842d3bb 100644 --- a/Changelog +++ b/Changelog @@ -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 -- cgit