GitLab

This reverts commit 9370eee7.

starting a new index-verimag.html on BTL doc

Mostly changes in PTree

Add one more `Local Transparent Node` to ensure compatibility with Coq < 8.12

This PR replaces the "PTree" data structure used in lib/Maps.v by the
canonical binary tries data structure proposed by A. W. Appel and
described in the paper "Efficient Extensional Binary Tries",
https://arxiv.org/abs/2110.05063

The new implementation is more memory-efficient and a bit faster,
resulting in reduced compilation times (-5% on typical C programs, up
to -10% on very large C functions).

It also enjoys the extensionality property (two tries mapping equal
keys to equal data are equal), which simplifies some proofs.

The previous code for elaborating character constants has a small bug:
the value of a wide character constant consisting of several characters
was normalized to type `int`, while, statically, it has type `wchar_t`.
If `wchar_t` is `unsigned short`, for example, the constant `L'ab'`
would elaborate to 6357090, which is not of type `unsigned short`.

This commit fixes the bug by normalizing wide character constants to type
`wchar_t`, regardless of how many characters they contain.

The previous code was odd in another respect: leading `\0` characters
in multi-character constants were ignored.  Hence, `'\0bcde'` was accepted
while `'abcde'` caused a warning.

This commit implements a more predictable behavior: the number of characters
in a character literal is limited a priori to
      sizeof(type of result) / sizeof(type of each character)

So, for non-wide character constants we can typically have up to 4
characters (sizeof(int) / sizeof(char)), while for wide character
constants we can only have one character.

In effect, multiple-character wide character literals are not supported.
This is allowed by the ISO C99 standard and seems consistent with GCC
and Clang.

Finally, a multi-character constant with too many characters was
reported either as an error (if the computation overflowed the 64-bit
accumulator) or as a warning (otherwise).  Here, we make this an error
in all cases.

GCC and Clang only produce warnings, and truncate the value of the
character constant, but an error feels safer.

Earlier CompCert versions would warn if a bit field of width N and
type enum E was too small for the values of the enumeration: whether
the field is interpreted as a N-bit signed integer or a N-bit unsigned
integer, some values of the enumeration are not representable.

This warning was performed in the Bitfields emulation pass, which went
away during the reimplementation of bit fields within the verified
part of CompCert.

In this commit, we resurrect the warning and perform it during the Elab pass.

In passing, some of the code that elaborates bit fields was moved to a
separate function "check_bitfield".

In Op.v, the definitions of is_rldl_mask and is_rldr_mask mask were
swapped:
- rldl is for [00001111] masks that clear on the left,
  hence start with 1s and finish with 0s;
- rldr is for [11110000] masks that clear on the right,
  hence start with 0s and finish with 1s.

In Asmgen.v, the case for masks of the form [00011111100] that can
generate a rldic instruction was incorrectly detected.

CompCert does not support 128-bit integers, but the gcc and clang preprocessors do include support as part of its 'built-in'.

A common way of testing for 128-bit integer support is to check to see if `__SIZEOF_INT128__` is defined.

Eliminating this macro prevents software from believing that 128-bit integers are supported.

Improved compatibility with Coq 8.14