CompCert 3.14

ISO C conformance

• free has well-defined semantics on blocks of size 0 (#509).

Code generation and optimization

• More simplifications of comparison operations and selection operations during the CSE pass.
• Replace selection operations with moves if both branches are equal.
• ARM 32 bits: several minor improvements to the generated code (#503 and more).

Bug fixes

• x86 under Windows: the wrong sub instruction was generated for Pallocframe.
• ARM: fix PC displacement overflow involving floating-point constants.
• ARM: fix error on printing of "s17" register.
• RISC-V: do not use 64-bit FP registers for memcpy if option -fno-fpu is given.

Usability

• Added generation of CFI debugging directives for AArch64 and RISC-V.
• Removed the command-line option -fstruct-return, deprecated since release 2.6.

Formal semantics

• The big-step semantics for Clight now supports the two models for function arguments (either as stack-allocated variables or as register-like temporaries).

Coq development

• Support Coq 8.17, 8.18, and 8.19.
• Revised most uses of the intuition tactic (#496 and more).
• Address most other deprecation warnings from Coq 8.18 and 8.19.
• Updated local copy of MenhirLib to version 20231231.
• Updated local copy of Flocq to version 4.1.4.

Distribution

• The small test suite was moved to a separate Git repository. Use git submodule init && git submodule update to download it.

CompCert 3.13

Code generation and optimization:

• Slightly more precise value analysis, with a better distinction between "any integer value" and "any integer or pointer value". (#490)
• Recognize a few more nested conditional expressions that can be if-converted into a conditional move.
• Register allocation: better support for "preferred" registers, e.g. registers R0-R3 on ARM Thumb, which enable more compact instruction encodings.
• ARM Thumb: use more instructions that can be encoded in 16 bits, producing more compact code.
• x86: use a shorter instruction encoding for loading unsigned 32-bit constants. (#487)

Bug fixes:

• _Noreturn on function definitions (but not declarations) was ignored sometimes.
• The argument of __builtin_va_end was discarded, is now evaluated for its side effects.
• Tail call optimization must be disabled in variadic functions, otherwise a va_list structure can get out of scope.
• Nested compound initializers were elaborated in the wrong order, causing compile-time failures later in the compilation pipeline.
• The signedness of a bit field was determined differently when its type was an enum type and when it was a typedef to an enum type.

ABI conformance:

• Define wchar_t exactly like the ABI says. On most platforms, CompCert was defining wchar_t as signed int, but it must be unsigned int for AArch64-ELF and unsigned long for PowerPC-EABI.

Supported platforms:

• Removed support for Cygwin 32 bits, which has reached end of life. Cygwin 64 bits remains supported.

Coq development:

• Support Coq 8.16.0 and 8.16.1, addressing most of the new warnings in 8.16.
• When installing the Coq development, also install coq-native generated files.
• Tweak some proof scripts for compatibility with future Coq versions. (#465, #470, #491, #492)
• Updated the vendored copy of Flocq to version 4.1.1.

CompCert 3.12

New features:

• Support unstructured switch statements such as Duff's device. This is achieved via an optional, unverified code rewrite, activated by option -funstructured-switch. (#459)
• Support C11 Unicode string literals and character constants, such as u8"été" or u32'❎'.

Usability:

• Support the -std=c99, -std=c11 and -std=c18 option. These options are passed to the preprocessor, helping it select the
  correct version of the standard header files. It also controls CompCert's warning for uses of C11 features. (#456)
• The source character set of CompCert is now officially Unicode with UTF-8 encoding, A new warning invalid-utf8 is triggered if byte sequences that are not valid UTF-8 are found outside of comments. Other source character sets and stricter validation can be supported via the -finput-charset option, see next.
• If the GNU preprocessor is used, the source character set can be selected with the -finput-charset= option. In particular, -finput-charset=utf8 checks that the source file is correctly UTF-8 encoded, and -finput-charset=ascii that it contains no Unicode characters at all.
• Support mergeable sections for string literals and for numerical constants.
• AArch64, ARM, RISC-V and x86 ELF targets: use .data.rel.ro section for const data whose initializers contain relocatable addresses. This is required by the LLVM linker and simplifies the work of the GNU linker.
• configure script: add option -sharedir to specify where to put the compcert.ini configuration file (#450, #460)
• ARM 32 bits: emit appropriate Tag_ABI_VFP attribute (#461)

Optimizations:

• Recognize more if-else statements that can be if-converted into a conditional move. In particular, debug statements generated in -g mode no longer prevent this conversion.

Bug fixes:

• Revised simplification of nested conditional, ||, && expressions to make sure the generated Clight code is well typed and is not rejected later by ccomp (#458).
• In -g mode, when running under Windows, the ccomp executable could fail on an uncaught exception while inserting lines of the source C file as comments in the generated assembly file.
• Reintroduced DWARF debug information for bit fields in structs (it was missing since 3.10).

Coq development:

• RTLgen: use the state and error monad for reserving goto labels (#371) (by Pierre Nigron)
• Add Declare Scope statements where appropriate, and re-enable the undeclared-scope warning.

CompCert 3.11

New features

• Support _Generic expressions from ISO C11.

ISO C conformance

• Enumeration types are compatible only with int but not with other integer types.
• Fixed confusion between unprototyped function pointer types T (*)() and prototyped, zero-argument function pointer types T (*)(void) in type casts (#431).

Usability

• Improved control-flow analysis of calls to "noreturn" functions, resulting in more accurate warnings.
• More detailed warning for unprototyped function definitions, now shows the prototyped type that is given to the function.
• Extended the warning above to definitions of the form T f() { ... }, i.e. unprototyped but with no parameters. (Before, the warning would trigger only if parameters were declared.)
• Check (and warn if requested) for arguments of struct/union types passed to a variable-argument function.

Bug fixes

• RISC-V: fixed an error in the modeling of float32 <-> float64 conversions when the argument is a NaN (#428).
• x86: changed the compilation of __builtin_fmin and __builtin_fmax so that their NaN behavior is the one documented in the manual.
• Improved reproducibility of register allocation. (Before, compiling CompCert with two different OCaml versions could have resulted in correct but different allocations.)
• Hardened the configure script against Cygwin installations that produce \r\n for end-of-lines (#434).
• RISC-V: tail calls to far-away functions were causing link-time errors (#436, #437).

Coq development

• Updated the Flocq library to version 4.1.
• Support for Coq 8.14.1, 8.15.0, 8.15.1, 8.15.2.
• Minimal Coq version supported is now 8.12.0.

CompCert 3.10

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 constants L'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 to clightgen) (contributed by Bart Jacobs; #404, #413).

Coq development

• Added support for Coq 8.14 (#415).
• Added support for OCaml 4.13.
• Updated the Flocq library to version 3.4.2.
• Replaced Global Set Asymmetric Patterns by more local settings (#408).

CompCert 3.9

New features

• New port: AArch64 (ARM 64 bits, "Apple silicon") under macOS.
• Support bitfields of types other than int, provided they are no larger than 32 bits (#387)
• Support __builtin_unreachable and __builtin_expect (#394) (but these builtins are not used for optimization yet)

Optimizations

• Improved branch tunneling: optimized conditional branches can introduce further opportunities for tunneling, which are now taken into account.

Usability

• Pragmas within functions are now ignored (with a warning) instead of being lifted just before the function like in earlier versions.
• configure script: add -mandir option (#382)

Compiler internals

• Finer control of variable initialization in sections. Now we can put variables initialized with symbol addresses that need relocation in specific sections (e.g. const_data on macOS).
• Support re-normalization of function parameters at function entry, as required by the AArch64/ELF ABI.
• PowerPC 64 bits: remove Pfcfi, Pfcfiu, Pfctiu pseudo-instructions, expanding the corresponding int<->FP conversions during the selection pass instead.

Bug fixing

• PowerPC 64 bits: incorrect ld and std instructions were generated and rejected by the assembler.
• PowerPC: some variadic functions had the wrong position for their first variadic parameter.
• RISC-V: fix calling convention in the case of floating-point arguments that are passed in integer registers.
• AArch64: the default function alignment was incorrect, causing a warning from the LLVM assembler.
• Pick the correct archiver to build .a library archives (#380).
• x86 32 bits: make sure functions returning structs and unions return the correct pointer in register EAX (#377).
• PowerPC, ARM, AArch64: updated the registers destroyed by asm pseudo-instructions and built-in functions.
• Remove spurious error on initialization of a local struct containing a flexible array member.
• Fixed bug in emulation of assignment to a volatile bit-field (#395).

The clightgen tool

• Move the $ notation for Clight identifiers to scope clight_scope and submodule ClightNotations, to avoid clashes with Ltac2's use of $ (#392).

Coq development

• Compatibility with Coq 8.12.2, 8.13.0, 8.13.1, 8.13.2.
• Compatibility with Menhir 20210419 and up.
• Oldest Coq version supported is now 8.9.0.
• Use the lia tactic instead of omega.
• Updated the Flocq library to version 3.4.0.

Licensing and distribution

• Dual-licensed source files are now distributed under the LGPL version 2.1 (plus the Inria non-commercial license) instead of the GPL version 2 (plus the Inria non-commercial license).

CompCert 3.8

New features

• Support _Static_assert from ISO C11.
• Support __builtin_constant_p from GCC and Clang.
• New port: x86 64 bits Windows with the Cygwin 64 environment. (configure with target x86_64-cygwin).
• The following built-in functions are now available for all ports: __builtin_sqrt, __builtin_fabsf, and all variants of __builtin_clz and __builtin_ctz.
• Added __builtin_fmin and __builtin_fmax for AArch64.

Removed features

• The x86 32 bits port is no longer supported under macOS.

Compiler internals

• Simpler translation of CompCert C casts used for their effects but not for their values.
• Known builtins whose results are unused are eliminated earlier.
• Improved error reporting for ++ and -- applied to pointers to incomplete types.
• Improved error reporting for redefinitions and implicit definitions of built-in functions.
• Added formal semantics for some PowerPC built-ins.

The clightgen tool

• New -canonical-idents mode, selected by default, to change the way C identifiers are encoded as CompCert idents (positive numbers). In -canonical-idents mode, a fixed one-to-one encoding is used so that the same identifier occurring in different compilation units encodes to the same number.
• The -short-idents flag restores the previous encoding where C identifiers are consecutively numbered in order of appearance, causing the same identifier to have different numbers in different compilation units.
• Removed the automatic translation of annotation builtins to Coq logical assertions, which was never used and possibly confusing.

Coq and OCaml development

• Compatibility with Coq 8.12.1, 8.12.0, 8.11.2, 8.11.1.
• Can use already-installed Flocq and MenhirLib libraries instead of their local copies (options -use-external-Flocq and -use-external-MenhirLib to the configure script).
• Automatically build to OCaml bytecode on platforms where OCaml native-code compilation is not available.
• Install the compcert.config summary of configuration choices in the same directory as the Coq development.
• Updated the list of dual-licensed source files.

CompCert 3.7

ISO C conformance:

• Functions declared extern then implemented inline remain extern
• The type of a wide char constant is wchar_t, not int
• Support vertical tabs and treat them as whitespace
• Define the semantics of free(NULL)

Bug fixing:

• Take sign into account for conversions from 32-bit integers to 64-bit pointers
• PowerPC: more precise determination of small data accesses
• AArch64: when addressing global variables, check for correct alignment
• PowerPC, ARM: double rounding error in int64->float32 conversions

ABI conformance:

• x86, AArch64: re-normalize values of small integer types returned by function calls
• PowerPC: float arguments passed on stack are passed in 64-bit format
• RISC-V: use the new ELF psABI instead of the old ABI from ISA 2.1

Usability and diagnostics:

• Unknown builtin functions trigger a specific error message
• Improved error messages

Coq formalization:

• Revised modeling of the PowerPC/EREF isel instruction
• Weaker ec_readonly condition over external calls
  (permissions can be dropped on read-only locations)

Coq and OCaml development:

• Compatibility with Coq version 8.10.1, 8.10.2, 8.11.0
• Compatibility with OCaml 4.10 and up
• Compatibility with Menhir 20200123 and up
• Coq versions prior to 8.8.0 are no longer supported
• OCaml versions prior to 4.05.0 are no longer supported

CompCert 3.6

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 and a ? 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 to a ? b : c but b and c 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 and unsigned 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 type double.

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.

The clightgen tool:

• Fix normalization of Clight switch statements. (#285)
• Add more tracing options: -dprepro, -dall. (#298)
• Fix the output of -dclight. (#314)

CompCert 3.5

Release 3.5, 2019-02-27

Bug fixing:

• Modeling error in PowerPC ISA: how register 0 is interpreted when used as base register for indexed load/stores. The code generated by CompCert was correct, but was proved correct against the wrong specification.
• Modeling error in x86 ISA: how flag ZF is set by floating-point comparisons. Here as well, the code generated by CompCert was correct, but was proved correct against the wrong specification.
• Revised handling of attributes so that they behave more like in GCC and Clang. CompCert now distinguishes between attributes that attach to names (variables, fields, typedefs, structs and unions) and attributes that attach to objects (variables). In particular, the aligned(N) attribute now attaches to names, while the _Alignas(N) modifier still attaches to objects. This fixes issue #256.
• Issue with NULL as argument to a variadic function on 64-bit platforms (issue #265)
• Macro __bool_true_false_are_defined was missing from <stdbool.h> (issue #266)

Coq development:

• Can now be entirely rechecked using coqchk (contributed by Vincent Laporte)
• Support Coq version 8.9.0
• Avoid using "refine mode" when defining Instance (contributed by Maxime Dénès)
• Do not support Menhir versions more recent than 20181113, because they will introduce an incompatibility with this CompCert release.

New feature:

• PowerPC port: add __builtin_isel (conditional move) at types int64, uint64, and _Bool.