Release 3.10, 2021-11-19
Major improvement
- Bit fields in structs and unions are now handled in the formally-verified part of CompCert. (Before, they were being implemented through an unverified source-to-source translation.)
The CompCert C and Clight languages provide abstract syntax for bit-field declarations and formal semantics for bit-field accesses.
The translation of bit-field accesses to bit manipulations is performed in the Cshmgen pass and proved correct.
Usability
- The layout of bit-fields in memory now follows the ELF ABI algorithm, improving ABI compatibility for the CompCert target platforms that use ELF.
- Handle the
# 0
line directive generated by some C preprocessors (#398). - Un-define the
__SIZEOF_INT128__
macro that is predefined by some C preprocessors (#419). - macOS assembler: use
##
instead of#
to delimit comments (#399).
ISO C conformance
- Stricter checking of multi-character constants
'abc'
.
Multi-wide-character constantsL'ab'
are now rejected, like GCC and Clang do. - Ignore (but still warn about) unnamed plain members of structs and unions (#411).
- Ignore unnamed bit fields when initializing unions.
Bug fixing
- x86 64 bits: overflow in offset of
leaq
instructions (#407). - AArch64, ARM, PowerPC, RISC-V: wrong expansion of
__builtin_memcpy_aligned
in cases involving arguments that are stack addresses (#410, #412) - PowerPC 64 bits: wrong selection of 64-bit rotate-and-mask instructions (
rldic
,rldicl
,rldicr
), resulting in assertion failures later in the compiler. - RISC-V: update the Asm semantics to reflect the fact that register X1 is destroyed by some builtins.
Compiler internals
- The "PTree" data structure (binary tries) was reimplemented, using a canonical representation that guarantees extensionality and improves performance.
- Add the ability to give formal semantics to numerical builtins with small integer return types.
- PowerPC: share code for memory accesses between Asmgen and Asmexpand.
- Declare
__compcert_i64*
helper runtime functions during the C2C pass, so that they are not visible during source elaboration.
The clightgen
tool
- Add support for producing Csyntax abstract syntax instead of Clight abstract syntax (option
-csyntax
toclightgen
) (contributed by Bart Jacobs; #404, #413).