| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
| |
| |
| |
| | |
Otherwise, BinarySingleNaN.Bleb_correct cannot be proved.
|
| | |
|
|/ |
|
|
|
|
| |
`Kloop1` should have been `Kloop2`.
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
For RISC-V we need to return the canonical NaN value if the argument of
a float32->float64 or float64->float32 conversion is any NaN.
This is in line with 11.3 from the RISC-V manual, the description of
the conversion operations as well as what the spike ISA simulator and
qemu do.
Other platforms convert the NaN payload (by truncation or expansion)
in float32->float64 and float64->float32 conversions.
Fixes: #428
|
|
|
|
|
|
|
| |
If any are found, make sure that `-fstruct-passing` was given.
Previously, we used to check the fixed arguments (as part of a call to
`checkFunctionType`) but not the variable arguments.
|
|
|
|
|
|
|
|
|
|
| |
The ops `Omaxf` and `Ominf` have the same semantics as `minsd` and
`maxsd` instruction, i.e. if both arguments are equal the second
argument is returned as well as for NaN.
The operations are the used in SelectOp to implement the built-in
function `__builtin_fmax` and `__builtin_fmin`.
Bug 32640
|
|
|
|
|
|
| |
If both arguments are zero the second argument is returned independ from
their sign.
Bug 32640
|
| |
|
|
|
|
|
|
|
| |
coq/coq#15442 changes the way `Program` names things, to make it uniform w.r.t. the standard naming schema.
This commit removes dependencies on the names chosen by `Program`. Should be backwards compatible.
Co-authored-by: Xavier Leroy <xavier.leroy@college-de-france.fr>
|
| |
|
|
|
|
|
|
|
|
|
|
| |
As written previously, OCaml can evaluate `nodeOfVar g v1` and
`nodeOfVar g v2` in any order. Consequently, `v1` and `v2` can be
entered in the `varTable` hash table in different order. This can
result in different (but equally valid) register allocations.
It's better to enforce one evaluation order for the sake of
reproducible compilations when the OCaml version changes.
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
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
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Warning "deprecated hint rewrite without locality" cannot be addressed:
the suggested fix (qualify with Global or Local or [#export])
is not supported by Coq 8.11 to 8.13 !
Warning "deprecated instance without locality" is turned off
for generated file cparser/Parser.v only.
Menhir needs to be changed so as to generate the `Global` modifier
that would silence this warning.
|
| |
| |
| |
| | |
This avoids a new warning of Coq 8.14.
|
|/ |
|
|
|
|
| |
It remains compatible with earlier Menhir versions.
|
|
|
|
| |
The change is backward compatible with Coq 8.9 to 8.13 (at least).
|
|
|
|
| |
Follow-up to c34d25e01
|
|
|
|
|
|
|
|
|
|
|
|
| |
When a union is initialized with an initializer without designator the
first named member should be initialized. This commit skips members
without names during the elaboration of union initializers.
Note that anonymous members (unnamed members of struct or union type)
should not be skipped, and are not skipped since elaboration give names
to these members.
Bug 31982
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
E.g. `struct { int; int x; };`. The `int;` declaration provides no name,
is not a bit field, and is not a C11 anonymous struct/union member.
Such declarations are not allowed by the C99 grammar, even though GCC,
Clang and CompCert tolerate them. The C11 grammar allows these
declarations but the standard text gives them no meaning.
CompCert used to warn about such declarations, yet include them in the
struct or union as unnamed members, similar to an unnamed bit field.
This is incorrect and inconsistent with what GCC and Clang do.
With this commit, CompCert still warns, then ignores the declaration
and does not create an unnamed member. This is consistent with GCC
and Clang.
Fixes: #411
|
|\
| |
| | |
Add support to clightgen for generating Csyntax AST as .v files
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
As proposed in #404.
This is presented as a new option `-clight` to the existing `clightgen` tool.
Revise clightgen testing to test the Csyntax output in addition to
the Clight output.
|
| |
| |
| |
| |
| |
| |
| | |
Split reusable parts of ExportClight.ml off, into
ExportBase.ml and ExportCtypes.ml.
Rename exportclight/ directory to export/
|
| |
| |
| |
| |
| |
| | |
For compatibility with Coq 8.14.
Cherry-picked from upstream commit 2e3c2441
|
| |
| |
| |
| | |
For compatibility with the upcoming Coq 8.14.
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
In the "small" case, there was an error in the choice of temporary
registers to use when one argument is a stack location and the other
is a register. The chosen temporary could conflict with the argument
that resides in a register.
Fixes: #412
|
|/
|
|
|
|
|
|
|
|
| |
Stack offsets must be multiple of 8 when using ldp/stp instructions
and multiple of the transferred size when using other load/store
instructions with offsets greater than 256.
For simplicity, always require that the offset is multiple of 8.
Fixes: #410
|
|
|
|
| |
The return type is Tint8unsigned (i.e. _Bool), not Tint.
|
| |
|
|
|
|
|
|
| |
Instead, add `Set Asymmetric Patterns` to the files that need it,
or use `Arguments` to make inductive types work better with symmetric patterns.
Closes: #403
|
|
|
|
|
|
|
|
|
|
|
|
| |
In the Clight AST, padding bit fields (such as `int : 6;`) in composite
declarations are given an ident that corresponds to the empty string.
Previously, clightgen would give name `_` to this ident, but this is
not valid Coq.
This commit gives name `empty_ident` to the empty ident. This name
does not start with an underscore, so it cannot conflict with the
names for regular idents, which all start with `_`.
|
|
|
|
|
|
|
|
|
|
|
| |
Warning 69 "mutable record field is never mutated":
3 occurrences in backend/IRC.ml
removed the "mutable" qualifier on these fields
Warning 70 "cannot find interface file"
many .ml files have no .mli
no strong motivation to add the .mli files
turned off the warning in Makefile.extr
|
|
|
|
|
|
| |
Instead of duplicating the memory access code in `Asmexpand.ml` we move
the code for each of the different addressings in `Asmgen.v` into
separate functions that then can be reused in `Asmexpand.ml`.
|
|
|
|
|
|
|
|
| |
leaq's offsets can overflow (not fit in 32 bits) in other cases than
those fixed in 4daebb7a0, e.g. in the expansion of __builtin_memcpy_aligned.
This commit implements full normalization of the `leaq` instructions
produced in Asmexpand, following the same method used in Asmgen.
|
|
|
|
|
|
|
|
|
|
|
|
| |
If N does not fit in signed 32 bits, `leaq` cannot be used and
`mov; addq` must be used instead.
This was already the case for `leaq` instructions produced by the Asmgen
pass, but not for some `leaq` instructions produced by Asmexpand.
Normally, assemblers should fail if the `leaq` offset is not representable,
but this is not always the case (see issue #406).
Fixes: #406
|
|\ |
|