CompCert 3.4

Release 3.4, 2018-09-17

Bug fixing:

• Redefinition of a typedef in a different scope was wrongly rejected.
• Attach _Alignas(N) and __attribute((aligned(N))) to names instead of types, so that _Alignas(16) int * p means "16-aligned pointer to int", not "pointer to 16-aligned int".
• For packed structs, fix a discrepancy between the size and alignment computed during elaboration and those computed by the verified front-end after expansion.
• Honor qualified array types in function parameters: if a parameter is declared as e.g. int t[const 4], it is now treated as int * const t in the function body, not int * t like before.
• Reject __builtin_offsetof(struct s, f) if f is a bit-field.
• Wrong parsing of attributes having multiple arguments such as __attribute((packed(A,B,C))).
• If __builtin_ais_annot is followed immediately by a label (e.g. a loop head), add a nop instruction to separate the annotation from the label.
• Wrong parsing of the command-line options -u <symbol> and -iquote.
• PowerPC in hybrid 32/64 bit mode: reject %Q and %R register specifications in inline assembly code, since 64-bit integer arguments are not split in two registers.
• x86 64-bit mode: wrong expansion of __builtin_clzl and __builtin_ctzl (issue #127).

New checks for ISO C conformance:

• Removed support for _Alignof(expr), which is not C11; only _Alignof(ty) is part of C11.
• Reject occurrences of _Alignas in places that are not allowed by C11, e.g. in typedef. __attribute((aligned(N))) can be used instead.
• Reject occurrences of restrict in places that are not allowed by C99 and C11.
• Reject structs composed of a single flexible array struct { ty []; }.
• Check that qualified array types such as int t[const 4] occur only as function parameters, but nowhere else.
• In function definitions, reject function parameters that have no names.

New warnings:

• Warn for flexible array types ty[] in places where they do not make sense.
• Warn for inline (not static inline) functions that declare non-constant static variables.
• Optionally warn if the alignment of an object is reduced below its natural alignment because of a _Alignas qualifier or an aligned attribute, or a packed attribute.
• Warn for tentative static definitions with an incomplete type, e.g. static int x[];.
• The warning about uses of C11 features is now off by default.

Semantic preservation proof:

• Model the fact that external functions can destroy caller-save registers and Outgoing stack slots; adapt the proofs accordingly.

Coq and OCaml development:

• Support Coq versions 8.8.1 and 8.8.2.
• Support OCaml versions 4.7.0 and up.
• Support Menhir versions 20180530 and up.

Others:

• Improved error handling in "configure" script (issue #244)
• clightgen adds configuration information to the generated .v file (issue #226)

CompCert 3.3

Release 3.3, 2018-05-30

New features

• Introduced the __builtin_ais_annot built-in function to communicate source-level annotations to AbsInt's a3 tool suite via a special section in object and executable files.
• Improved C11 support: define the C11 conditional feature macros; define the max_align_t type in stddef.h.
• PowerPC 64-bit port: new built-in functions for 64-bit load-store with byte reversal and for 64-bit integer multiply high.
• x86 64 bits: add support for BSD.

Bug fixing

• Wrong code generated for unions containing several bit fields.
• Internal compiler errors for some initializers for structs and unions containing bit-fields, and for anonymous members of unions.
• Missing error reporting for <integer> - <ptr> subtraction, causing an internal retyping error later during compilation.
• String literals are l-values.
• String literals have array types, not pointer types.
• Array sizes >= 2^32 were handled incorrectly on 64-bit platforms.
• Wrong code generated for global variables of size 2^31 bytes or more.
• struct and union arguments to annotation builtins must be passed by reference, regardless of the ABI calling conventions.
• e1, e2 has pointer type if e2 has array type.
• x86 64 bits: in symbol + ofs addressing modes, the offset ofs must be limited to [-2^24, 2^24) otherwise linking can fail.

New or improved diagnostics (errors and warnings)

• Warn for comparison of a pointer to a complete type and a pointer to an incomplete type.
• More checks on variables declared in "for" loops: not static, not extern, not function types.
• Reject empty declarations in K&R functions.
• Reject arrays of incomplete types.
• Reject duplicate 'case' or 'default' statements within a 'switch'.
• Reject 'case' and 'default' statements outside a 'switch'.
• Check that 'typedef' declares a name and doesn't contain '_Noreturn'.
• Function parameters are in the same scope as function local variables.
• More comprehensive constant-ness checks for initializers of global or static local variables.
• Make sure an enum cannot have the same tag as a struct or an union.
• More checks on where the 'auto' storage class can be used.
• Accept empty enum declaration after nonempty enum definition.
• Reject pointers to incomplete types in ptr - ptr subtraction.
• When defining a function, take attributes (_Noreturn, etc) from earlier declarations of the function into account.
• Better check for multiple definitions of functions or global variables.
• Reject illegal initializations of aggregates such as char c[4] = 42;.
• Reject designated initializers where a member of a composite type is
  re-initialized after the composite has been initialized as a whole.
• Reject casts to struct/union types.
• Reject sizeof(e) where e designates a bit-field member of a struct or union.
• e1, e2 is not a compile-time constant expression even if e1 and e2 are.
• "main" function must not be "inline"
• Warn for functions declared extern after having been defined.
• Warn for function declarations after function definitions when the
  declaration has more attributes than the definition.
• Warn for assignment of a volatile struct to a non-volatile struct.
• Warn for "main" function if declared _Noreturn.

Coq development

• Added support for Coq versions 8.7.2 and 8.8.0.
• Rewrote "Implicit Arguments" and "Require" inside sections, these are obsolete in 8.8.0.
• Upgraded Flocq to version 2.6.1.
• Optionally install the .vo files for reuse by other projects (options -install-coqdev and -coqdevdir to configure script; automatically selected if option -clightgen is given).

CompCert 3.2

Release 3.2, 2018-01-15

Code generation and optimization

• Inline static functions that are called only once. Can be turned off by setting the "noinline" attribute on the function.
• More consistent detection and elimination of divisions by 1.
• ARM in Thumb mode: simpler instruction sequence for branch through jump table.
• ARM: support and use the "cmn" instruction.
• Issue #208: make value analysis of comparisons more conservative for dubious comparisons such as (uintptr_t) &global == 0x1234 which are undefined behavior in CompCert.

Usability

• Resurrected support for the Cygwin x86-32 port, which got lost at release 3.0.
• Support the noinline attribute on C function definitions.
• PowerPC port with Diab toolchain: support -t <target processor> option and pass it to the Diab tools.
• Clightgen tool: add -o option to specify output file.
• Pull request #192: improve the printing of Clight intermediate code so that it looks more like valid C source. (Frédéric Besson)

Bug fixing

• Issue #P25: make sure sizeof(long double) = sizeof(double) in all contexts.
• Issue #211: wrong scoping for C99 declarations within a "for" statement.
• Issues #215 and #216: updates to clightgen.

Coq and Caml development

• Pull request #191: Support Coq version 8.7.0 and 8.7.1 in addition to Coq 8.6.1. Coq 8.6 (.0) is no longer supported owing to an incompatibility with 8.7.0. (Sigurd Schneider)
• ARM code generator: refactoring of constant expansions and EABI fixups.
• Resynchronized the list of dual-licensed files given in file LICENSE and the copyright headers of the dual-licensed files.

CompCert 3.1

Release 3.1, 2017-08-18

Major improvements

• New port targeting the RISC-V architecture, in 32- and 64-bit modes.

• Improved support for PowerPC 64 processors: use 64-bit registers and
  instructions for 64-bit integer arithmetic. Pointers remain 32 bits
  and the 32-bit ABI is still used.

Code generation and optimization

• Optimize leaf functions in the PowerPC back-end.
  (Avoid reloading the return address from the stack.)
• Avoid generating useless conditional branches for empty if/else statements.
• Earlier elimination of redundant &*expr and *&expr addressings.
• Improve utilization of addressing modes for volatile loads and stores.

Usability

• Add options -finline / -fno-inline to control function inlining.
• Removed the compilation of '.cm' files written in Cminor concrete syntax.
• More precise warnings about missing function returns.
• clightgen: add option "-normalize" to avoid memory loads deep inside
  expressions.

Bug fixing

• Issue #179: clightgen produces wrong output for "switch" statements.
• Issue #196: excessive proof times in .v files produced by clightgen.
• Do not generate code for functions with "inline" specifier that are
  neither static nor extern, as per ISO C99.
• Some line number information was missing for some goto labels and
  switch cases.
• Issue #P16: illegal PowerPC asm generated for unsigned division after
  constant propagation.
• Issue #P18: ARM addressing overflows caused by 1- underestimation of
  code size, causing mismanagement of constant pool, and 2- large stack
  frames where return address and back link are at offsets >= 4Kb.
• Pass -no-pie flag to the x86 linker when -pie is the default.

Coq and Caml development

• Support Coq 8.6.1.
• Improve compatibility with Coq working version.
• Always generate .merlin and _CoqProject files.

CompCert 3.0.1

Release 3.0.1, 2017-02-14

This release is functionally identical to release 3.0, but uses Coq version 8.6 instead of version 8.5.

CompCert 3.0

Release 3.0, 2017-02-10

Major improvements:

• Added support for 64-bit target platforms, including pointers that are 64-bit wide, and the ability to use 64-bit integer registers and arithmetic operations. This support does not replace but comes in addition to CompCert's original support for 32-bit target platforms, with 32-bit pointers and emulation of 64-bit integer arithmetic using pairs of 32-bit integers. In terms of C data models, CompCert used to be restricted to the ILP32LL64 model; now it also supports I32LP64 and IL32LLP64.
• The x86 port of CompCert was extended to produce x86-64 bit code in addition to the original x86-32 bit (IA32) code. (This is the first instantiation of the new support for 64-bit targets described above.) Support for x86-64 is currently available for Linux and MacOS X. (Run the configure script with x86_64-linux or x86_64-macosx.) This is an early port: several ABI incompatibilities remain.

Language features:

• Support for anonymous structures and unions as members of structures or unions. (ISO C11, section 6.7.2.1, para 13 and 19.)
• New built-in functions for ARM and PowerPC: __builtin_ctz, __builtin_ctzl, __builtin_ctzll (count trailing zeros, 32 and 64 bits).

Usability:

• Added options -Wxxx and -Wno-xxx (for various values of "xxx") to control which warnings are emitted.
• Added options -Werror=xxx and -Wno-error=xxx (for various values of "xxx") to control which warnings are treated as errors.
• Support response files where additional command-line arguments can be passed (syntax: @file).
• Improved wording of warning and error messages.
• Improved handling of attributes, distinguishing attributes that apply to types from attributes that apply to names. For example, in __attribute((aligned(8),section("foo"))) int * p; the "aligned" attribute is attached to type int, while the "section" attribute is attached to name p.

Code generation:

• Support for ARM target processors in big-endian mode.
• Optimize 64-bit integer division by constants.

Bug fixing:

• Issue #155: on ARM, assembly errors caused by large jump tables for "switch" statements and overflow in accessing constant pools.
• Issue #151: large inductive definition causes a fatal error in 32-bit versions of Coq.
• Issue #143: handle %lf printf() format in the reference interpreter
• Issue #138: struct declarations in K&R function parameters were ignored.
• Issues #110, #111, #113, #114, #115, #119, #120, #121, #122, #123, #124, #125, #126, #127, #128, #129, #130, #133, #138, #144: various cases of internal errors and failed assertions that should have been proper errors instead.
• For __builtin_memcpy_aligned, size and alignment arguments of 64-bit integer type were causing a fatal error on a 32-bit target.
• ARM and x86 ports: wrong register allocation for some calls to function pointers.

CompCert 2.7.1

Release 2.7.1, 2016-07-18

The CompCert Coq sources were ported to Coq 8.5pl2. There are no new functionalities compared with 2.7.

Bug fixing

• Fixed a compile-time assertion failure involving builtins taking a 64-bit integer parameter and given an signed 32-bit integer argument.
• The Cminor parser was updated.

CompCert 2.7

Release 2.7, 2016-06-30

Major improvement:

The proof of semantic preservation now accounts for separate compilation and linking, following the approach of Kang, Kim, Hur, Dreyer and Vafeiadis, "Lightweight verification of separate compilation", POPL 2016. Namely, the proof considers a set of C compilation units, separately compiled to assembly then linked, and shows that the resulting assembly program preserves the semantics of the C program that would be obtained by syntactic linking of the source C compilation units.

Language features:

• Parse the _Noreturn function attribute from ISO C11.
• New standard includes files: <iso646.h> and <stdnoreturn.h> from ISO C11.
• New built-in functions: __builtin_clzl, __builtin_clzll (count leading zeros, 32 and 64 bits) for ARM, IA32 and PowerPC; __builtin_ctz, __builtin_ctzl, __builtin_ctzll (count trailing zeros, 32 and 64 bits) for IA32.

Formal C semantics:

• The semantics of conversions from pointer types to _Bool is fully defined (again).

Usability:

• The generation of DWARF debugging information in -g mode is now supported for ARM and IA32 (in addition to PowerPC).

Coq development:

• Revised the Stacking pass and its proof to make it more extensible later to e.g. 64-bit integer registers.
• Use register pairs in function calling conventions to control more precisely the splitting of 64-bit integer arguments and results into pairs of 32-bit quantities
• Revised the way register conventions are described in Machregs and Conventions.
• Simulation diagrams now live in Prop instead of Type.

OCaml development:

• Code cleanup to remove warnings, support "safe strings" mode, and be fully compatible with OCaml 4.02 and 4.03.
• Cminor parser: support for single-precision FP numbers and operators.

Bug fixing:

• Some declarations within C expressions were incorrectly ignored (e.g. sizeof(enum e {A})).
• ARM in Thumb mode: incorrect movs instructions involving the stack pointer register were generated.

CompCert 2.6

Release 2.6, 2015-12-21

Usability:

• Generation of full DWARF v2 debugging information in "-g" mode,
  including function-local variables. This is fully supported
  for the PowerPC target with GNU tools or Diab tools. Support
  for IA32 and ARM is nearly there.
• Production of detailed explanations for syntax errors during parsing.
  (Exploiting recent work by F. Pottier on the Menhir parser generator.)
• PowerPC port: added many new builtin functions.

Code generation and optimization:

• Support for PowerPC 64-bits (pointers are still 32-bit wide)
  and Freescale's E5500 variant.
• More prudent alias analysis for operations over pointers that are
  formally undefined, such as bit masking.
• New pass: Debugvar, to associate debug information to local variables.

Coq development:

• Richer representation of arguments and results to builtin operations.
• As a consequence, annotation builtins no longer need special handling.
• Added EF_debug builtins to transport debugging information throughout
  the compiler back-end.
• Upgraded the Flocq library to version 2.5.0.

Bug fixing:

• Issue #71: incorrect initialization of an array of wchar_t
• Corrected the handling of bit-fields of type _Bool and width > 1
• Removed copy optimization when returning a struct from a function.
• Full parsing of unprototyped (K&R-style) function definitions.
  (Before, the parsing was incomplete and would reject some definitions.)

Miscellaneous:

• The cchecklink tool (for a posteriori validation of assembly
  and linking) was removed. It is replaced by the Valex tool,
  available from AbsInt.
• Added a command-line option -conf to select
  a different compcert.ini configuration file.
• Removed the command-line options fstruct-passing=
  and -fstruct-return=, more confusing than useful.
• Added a command-line option -fstruct-passing that activates
  ABI-conformant by-value passing of structs and unions as
  function arguments or results. If this option is not set,
  passing a struct/union as function argument is now rejected.
• The -fstruct-return command-line option is deprecated and
  becomes a synonymous for -fstruct-passing.
• The return type of __builtin_clz() is int, as documented,
  and not unsigned int, as previously implemented.

CompCert 2.5

Release 2.5, 2015-06-12

Language features:

• Extended inline assembly in the style of GCC. (See section 6.5
  of the user's manual.) The implementation is not as complete
  as that of GCC or Clang. In particular, the only constraints
  supported over operands are "r" (register), "m" (memory), and
  "i" (integer immediate).

Code generation and optimization:

• Revised translation of '||' and '&&' to Clight so as to
  produce well-typed Clight code.
• More prudent value analysis of uninitialized declarations of
  "const" global variables.
• Revised handling of "common" global declarations, fixes an issue
  with uninitialized declarations of "const" global variables.

Improvements in confidence:

• Formalized the typing rules for CompCert C in Coq and verified
  a type-checker, which is used to produce the type annotations
  in CompCert C ASTs, rather than trusting the types produced by
  the Elab pass.
• Coq proof of correctness for the Unusedglob pass (elimination
  of unreferenced static global definitions). The Coq AST for
  compilation units now records which globals are static.
• More careful semantics of comparisons between a non-null pointer
  and the null pointer. The comparison is undefined if the non-null
  pointer is out of bounds.

Usability:

• Generation of DWARF v2 debugging information in "-g" mode.
  The information describes C types, global variables, functions,
  but not yet function-local variables. This is currently available
  only for the PowerPC/Diab target.
• Added command-line options to turn individual optimizations on or off,
  and a "-O0" option to turn them all off.
• Revised handling of arguments to __builtin_annot so that no code
  is generated for an argument that is a global variable or a local
  variable whose address is taken.
• In string and character literals, treat illegal escape sequences
  (e.g. "%" or "\0") as an error instead of a warning.
• Warn if floating-point literals overflow or underflow when converted
  to FP numbers.
• In "-g -S" mode, annotate the generated .s file with comments
  containing the C source code.
• Recognize and accept more of GCC's alternate keywords, e.g. signed,
  __volatile, etc.
• cchecklink: added option "-files-from" to read .sdump file names
  from a file or from standard input.

ABI conformance:

• Improved ABI conformance for passing values of struct or union types
  as function arguments or results. Full conformance is achieved on
  IA32/ELF, IA32/MacOSX, PowerPC/EABI, PowerPC/Linux, and ARM/EABI.
• Support the "va_arg" macro from <stdarg.h> in the case of arguments
  of struct or union types.

Coq development:

• In the CompCert C and Clight ASTs, struct and union types are now
  represented by name instead of by structure. A separate environment
  maps these names to struct/union definitions. This avoids
  bad algorithmic complexity of operations over structural types.
• Introduce symbol environments (type Senv.t) as a restricted view on
  global environments (type Genv.t).
• Upgraded the Flocq library to version 2.4.0.

Bug fixing:

• Issue #4: exponential behaviors with deeply-nested struct types.
• Issue #6: mismatch on the definition of wchar_t
• Issue #10: definition of composite type missing from the environment.
• Issue #13: improved handling of wide string literals
• Issue #15: variable-argument functions are not eligible for inlining.
• Issue #19: support empty "switch" statements
• Issue #20: ABI incompatibility wrt struct passing on IA32.
• Issue #28: missing type decay in __builtin_memcpy_aligned applied to arrays.
• Issue #42: emit error if "static" definition follows non-"static" declaration.
• Issue #44: OSX assembler does not recognize ".global" directive.
• Protect against redefinition of the __i64_xxx helper library functions.
• Revised handling of nonstandard attributes in C type compatibility check.
• Emit an error on "preprocessing numbers" that are invalid numerical literals.
• Added missing check for static redefinition following a non-static
  declaration.
• Added missing check for redefinition of a typedef as an ordinary
  identifier within the same scope.

Miscellaneous:

• When preprocessing with gcc or clang, use "-std=c99" mode to force
  C99 conformance.
• Use a Makefile instead of ocamlbuild to compile the OCaml code.