aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
* Completely avoid line breaks in types when printing error messagesXavier Leroy2022-05-071-6/+10
| | | | | The `pp_indication` optional argument that governs formatting boxes in types was not propagated recursively, causing boxes to appear.
* Enum is only compatible with IInt.Xavier Leroy2022-05-061-4/+4
| | | | | | Enum types should only be compatible with the underlying integer type, not all integer types. Bug 33212
* Merge pull request #368 from silene/flocq-3.4Xavier Leroy2022-04-2938-2934/+5149
|\ | | | | Upgrade to Flocq 4.1.
| * Upgrade to Flocq 4.1.Guillaume Melquiond2022-04-2611-285/+737
| |
| * Support Coq 8.15.1Xavier Leroy2022-04-251-2/+2
| |
| * Make Coq 8.12.0 the minimal version.Guillaume Melquiond2022-04-251-2/+2
| | | | | | | | Otherwise, BinarySingleNaN.Bleb_correct cannot be proved.
| * Ignore .coq-native directories.Guillaume Melquiond2022-04-251-0/+1
| |
| * Upgrade to Flocq 4.0.Guillaume Melquiond2022-04-2536-2875/+4637
|/
* Fix a typo in a comment in Clight.v (#427)Hanzhi Liu2022-04-251-1/+1
| | | | `Kloop1` should have been `Kloop2`.
* Introduce float_conversion_default_nan parameter for float-float conversionsBernhard Schommer2022-04-257-9/+31
| | | | | | | | | | | | | 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
* Check for arguments of struct/union type passed to a vararg functionXavier Leroy2022-02-111-13/+16
| | | | | | | 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.
* Add op for float max and min for x86.Bernhard Schommer2022-02-0710-23/+66
| | | | | | | | | | 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
* Return second arg for float min/max on x86.Bernhard Schommer2022-02-071-4/+4
| | | | | | If both arguments are zero the second argument is returned independ from their sign. Bug 32640
* Support Coq 8.15.0Xavier Leroy2022-01-311-2/+2
|
* Adapt w.r.t. coq/coq#15442 (#425)Pierre-Marie Pédrot2022-01-103-6/+6
| | | | | | | 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>
* Fix pattern for github-linguist.Bernhard Schommer2021-12-141-2/+2
|
* Enforce evaluation order in IRC.add_interf and IRC.add_prefXavier Leroy2021-12-071-2/+2
| | | | | | | | | | 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.
* Support Coq 8.14.1Xavier Leroy2021-11-261-2/+2
|
* Second update for release 3.10v3.10Xavier Leroy2021-11-191-4/+6
|
* mention AArch64 in man-pageMichael Schmidt2021-11-171-1/+1
|
* Remove documentation of bitfield language support option.Michael Schmidt2021-11-171-5/+0
|
* First update for release 3.10Xavier Leroy2021-11-163-2/+57
|
* Maps.v: transparency of NodeXavier Leroy2021-11-161-1/+3
| | | | Add one more `Local Transparent Node` to ensure compatibility with Coq < 8.12
* An improved PTree data structure (#420)Xavier Leroy2021-11-169-668/+908
| | | | | | | | | | | | | | 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.
* Revised checks for multi-character constants 'xyz'Xavier Leroy2021-11-161-24/+19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Resurrect a warning for bit fields of enum typesXavier Leroy2021-11-121-15/+33
| | | | | | | | | | | | | | | | 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".
* PPC64: revised generation of rldic* instructionsXavier Leroy2021-10-284-20/+31
| | | | | | | | | | | | 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.
* Explicitly remove __SIZEOF_INT128__ macro definition. (#419)roconnor-blockstream2021-10-161-4/+4
| | | | | | | | 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.
* Merge pull request #415 from AbsInt/coq-8.14-compatXavier Leroy2021-10-1618-58/+68
|\ | | | | Improved compatibility with Coq 8.14
| * Add Coq 8.14.0 to the supported versions of CoqXavier Leroy2021-10-031-3/+3
| |
| * Selectively turn some Coq 8.14 warnings offXavier Leroy2021-10-031-1/+11
| | | | | | | | | | | | | | | | | | | | | | | | 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.
| * Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-0315-53/+53
| | | | | | | | This avoids a new warning of Coq 8.14.
| * Vendored Flocq library: address Coq 8.14 warningXavier Leroy2021-10-031-1/+1
|/
* Synchronize vendored MenhirLib with upstream (#416)Jacques-Henri Jourdan2021-10-037-36/+47
| | | | It remains compatible with earlier Menhir versions.
* Adapt to coq/coq#13837 ("apply with" does not rename arguments) (#417)Gaëtan Gilbert2021-10-032-4/+4
| | | | The change is backward compatible with Coq 8.9 to 8.13 (at least).
* Typo in expand_builtin_memcpy_smallXavier Leroy2021-10-011-1/+1
| | | | Follow-up to c34d25e01
* Ignore unnamed bit fields for initialization of unionsBernhard Schommer2021-09-282-7/+16
| | | | | | | | | | | | 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
* Ignore unnamed plain members of structs and unionsXavier Leroy2021-09-281-10/+15
| | | | | | | | | | | | | | | | | | | 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
* Merge pull request #413 from AbsInt/new-exportXavier Leroy2021-09-2727-694/+1098
|\ | | | | Add support to clightgen for generating Csyntax AST as .v files
| * Update export/README.mdXavier Leroy2021-09-221-18/+18
| |
| * Add support to clightgen for generating Csyntax AST as .v filesXavier Leroy2021-09-2221-271/+625
| | | | | | | | | | | | | | | | | | 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.
| * Refactor clightgenXavier Leroy2021-09-2213-594/+644
| | | | | | | | | | | | | | Split reusable parts of ExportClight.ml off, into ExportBase.ml and ExportCtypes.ml. Rename exportclight/ directory to export/
* | Vendored MenhirLib: replace Require Omega with Require ZArithXavier Leroy2021-09-251-1/+1
| | | | | | | | | | | | For compatibility with Coq 8.14. Cherry-picked from upstream commit 2e3c2441
* | Update the vendored Flocq library to version 3.4.2Xavier Leroy2021-09-255-38/+24
| | | | | | | | For compatibility with the upcoming Coq 8.14.
* | Fix wrong expansion of __builtin_memcpy_alignedXavier Leroy2021-09-234-8/+8
| | | | | | | | | | | | | | | | | | 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
* | For __builtin_memcpy_aligned, watch out for alignment of stack offsetsXavier Leroy2021-09-231-0/+1
|/ | | | | | | | | | 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
* Fix the type and the semantics of BI_bselXavier Leroy2021-09-221-4/+17
| | | | The return type is Tint8unsigned (i.e. _Bool), not Tint.
* For numerical builtins, support return types that are small integer typesXavier Leroy2021-09-221-25/+47
|
* Avoid `Global Set Asymmetric Patterns` (#408)Xavier Leroy2021-09-158-5/+13
| | | | | | 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
* clightgen: handle empty names given to padding bit fieldsXavier Leroy2021-09-152-16/+28
| | | | | | | | | | | | 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 `_`.
generated by cgit (git 2.34.1) at 2024-05-20 11:19:03 +0000