xavierleroy
released this
Release 3.8, 2020-11-16
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 theconfigure
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.
Assets
2
xavierleroy
released this
Release 3.7, 2020-03-31
ISO C conformance:
- Functions declared
extern
then implementedinline
remainextern
- The type of a wide char constant is
wchar_t
, notint
- 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
Assets
2
xavierleroy
released this
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.
The clightgen tool:
Assets
2
xavierleroy
released this
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.
Assets
2
xavierleroy
released this
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 asint * const t
in the function body, notint * t
like before. - Reject
__builtin_offsetof(struct s, f)
iff
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. intypedef
.__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:
Assets
2
xavierleroy
released this
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 ife2
has array type.- x86 64 bits: in
symbol + ofs
addressing modes, the offsetofs
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)
wheree
designates a bit-field member of a struct or union. e1, e2
is not a compile-time constant expression even ife1
ande2
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).
Assets
2
xavierleroy
released this
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.
Assets
2
xavierleroy
released this
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.
Assets
2
xavierleroy
released this
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.
Assets
2
xavierleroy
released this
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
orx86_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
-W
xxx 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 typeint
, while the "section" attribute is attached to namep
.
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.