Release 3.6, 2019-09-17
New features and optimizations:
- New port targeting the AArch64 architecture: ARMv8 in 64-bit mode.
- New optimization: if-conversion. Some
if
/else
statements anda ? b : c
conditional expressions are compiled to branchless conditional move instructions, when supported by the target processor - New optimization flag:
-Obranchless
, to favor the generation of branchless instruction sequences, even if probably slower than branches. - Built-in functions can now be given a formal semantics within CompCert, instead of being treated as I/O interactions. Currently,
__builtin_fsqrt
and__builtin_bswap*
have semantics. - Extend constant propagation and CSE optimizations to built-in functions that have known semantics.
- New "polymorphic" built-in function:
__builtin_sel(a,b,c)
. Similar toa ? b : c
butb
andc
are always evaluated, and a branchless conditional move instruction is produced if possible. - x86 64 bits: faster, branchless instruction sequences are produced for conversions between
double
andunsigned int
. __builtin_bswap64
is now available for all platforms.
Usability and diagnostics:
- Improved the DWARF debug information generated in -g mode.
- Added options -fcommon and -fno-common to control the generation of "common" declarations for uninitialized global.
- Check for reserved keywords
_Complex
and_Imaginary
. - Reject function declarations with multiple
void
parameters. - Define macros
__COMPCERT_MAJOR__
,__COMPCERT_MINOR__
, and__COMPCERT_VERSION__
with CompCert's version number. (#284) - Prepend
$(DESTDIR)
to the installation target. (#169) - Extended inline asm: print register names according to the types of the corresponding arguments (e.g. for x86_64,
%eax
if int and%rax
if long).
Bug fixing:
- Introduce distinct scopes for iteration and selection statements, as required by ISO C99.
- Handle dependencies in sequences of declarations (e.g.
int * x, sz = sizeof(x);
). (#267) - Corrected the check for overflow in integer literals.
- On x86, __builtin_fma was producing wrong code in some cases.
float
arguments to__builtin_annot
and__builtin_ais_annot
were uselessly promoted to typedouble
.
Coq formalization and development:
- Improved C parser based on Menhir version 20190626: fewer run-time checks, faster validation, no axioms. (#276)
- Compatibility with Coq versions 8.9.1 and 8.10.0.
- Compatibility with OCaml versions 4.08.0 and 4.08.1.
- Updated to Flocq version 3.1.
- Revised the construction of NaN payloads in processor descriptions so as to accommodate FMA.
- Removed some definitions and lemmas from lib/Coqlib.v, using Coq's standard library instead.