aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Update the proofs after rebaseFPcompXavier Leroy2019-03-261-84/+19
|
* Update proof of transl_condXavier Leroy2019-03-261-4/+2
|
* Introduce and use the type fp_comparison for floating-point comparisonsXavier Leroy2019-03-2646-761/+556
| | | | | | | | | | | With FP arithmetic, the negation of "x < y" is not "x >= y". For this reason, the back-end intermediate languages of CompCert used to have both "Ccompf c" and "Cnotcompf c" comparison operators, where "c" is of type Integers.comparison and "Cnotcompf c" denotes the negation of FP comparison c. There are some problems with this approach: - Beyond Cnotcompf we also need Cnotcompfs (for single precision FP) and, in case of ARM, special forms for not-comparison against 0.0. This duplication of comparison constructors inevitably causes some code and proof duplication. - Cnotcompf Ceq is really Ccompf Cne, and likewise Cnotcompf Cne is really Ccompf Ceq, hence the representation of FP comparisons is not canonical, adding to the code and proof duplication mentioned above. - Cnotcompf is introduced in CminorSel, but in Cminor we don't have it, making it impossible to express some transformations over comparisons at the machine-independent Cminor level. This commit develops an alternate approach, whereas FP comparisons have their own type, defined as Floats.fp_comparison, and which includes constructors for "not <", "not <=", "not >" and "not >=". Hence this type is closed under boolean negation, so to speak, and there is no longer a need for "Cnotcompf", given that "Ccompf" takes a fp_comparison and can therefore express all FP comparisons of interest.
* Harden configure against weird Menhir installationsXavier Leroy2019-03-251-2/+8
| | | | | | | | | | | As reported in #281, the Menhir packages in Fedora 29 and perhaps in other distributions can cause `menhir --suggest-menhirLib` to fail and return an empty path. This commit detects this situation and aborts configurations. Also, it hardens the generated Makefile against spaces and special characters in the path returned by `menhir --suggest-menhirLib`.
* RTLgenproof: destruct too deepXavier Leroy2019-03-251-2/+2
| | | | | | | `external_call_mem_extends` returns a conjunction of 4 properties, but the destruct pattern was 5 level deep. (Reported by Jeremie Koenig in pull request #278.)
* Integers.v: add modulus_gt_one (#259)Xavier Leroy2019-03-251-1/+7
| | | | | | | Since the number of bits is > 0, it is guaranteed that modulus > 1, not just that modulus > 0. (Suggested by Jake Waksbaum @jbaum.)
* Update the comment of the free operation (#277)chaomaer2019-03-251-1/+1
| | | | The comment says "writable" but it should be "freeable".
* Minor simplifications in two proofs. (#280)Vincent Laporte2019-03-252-3/+3
| | | Preparation for Coq PR 9725 that may make `eauto` stronger.
* Improve overflow check for integer literals (#157)Michael Schmidt2019-03-201-2/+4
| | | | | | The previous check was incomplete for integer literals in base 10. Bug 26119
* Update version number for 3.5v3.5Xavier Leroy2019-02-281-1/+1
|
* Update HTML doc for release 3.5Xavier Leroy2019-02-271-1/+1
|
* Update Changelog in preparation for release 3.5Xavier Leroy2019-02-261-1/+1
|
* Maximum supported Menhir version (#275)Xavier Leroy2019-02-261-1/+1
| | | | | Follow-up to commit fc9bc643. The latest Menhir version compatible with the current code base is actually 20181113.
* Update Changelog in preparation for release 3.5Xavier Leroy2019-02-251-0/+35
|
* Maximum supported Menhir version (#275)Jacques-Henri Jourdan2019-02-251-2/+3
| | | The Coq backend of Menhir will soon enjoy a large refactoring, making it incompatible with the version of MenhirLib currently in CompCert. This commit adds a check in configure to make sure that the version of Menhir is not more modern than the current one (20181026).
* Revised attachment of name attributes to structs, unions, enumsXavier Leroy2019-02-253-6/+29
| | | | | | | | | | | | | | | | | | Consider: ``` struct s { ... } __attribute((aligned(N))); struct t { ... } __attribute((aligned(N))) struct t x; ``` In the first case, the aligned attribute should be attached to struct s, so that further references to struct s are aligned. In the second case, the aligned attribute should be attached to the variable x, because if we attach it to struct t, it will be ignored and cause a warning. This commit changes the attachment rule so that it treats both cases right. Extend regression test for "aligned" attribute accordingly, by testing aligned attribute applied to a name of struct type.
* Reject object-related and struct-related attributes on typedefsXavier Leroy2019-02-254-8/+19
| | | | | | | | | | | | | | | | | | | | This commit adds a check to reject type definitions such as ``` typedef __attribute((section "foo")) int fooint; ``` GCC and Clang also reject this as an error. Without the check, the behavior is somewhat surprising: ``` fooint x; // placed in section "foo" fooint * x; // placed in default section, attribute "foo" is ignored ``` Note that the following must be accepted: ``` typedef struct { ... } __attribute((packed)) t; ``` The "packed" attribute is correctly attached to the struct type and should not be checked. This is achieved by using `attribute_of_type_no_expand` to get the attributes of the typedef-ed type, excluding the attributes carried by a struct/union or another typedef.
* Add regression test for "aligned" attributeXavier Leroy2019-02-253-1/+120
| | | | Expected results were obtained with GCC 5.4 and Clang 8.0
* Distinguish object-related and name-related attributesXavier Leroy2019-02-254-13/+24
| | | | | | | | | | | | | | | | | This is a second step towards mimicking GCC/Clang's handling of attributes. This commit introduces a distinction between - Object-related attributes, such as "section", which apply to the object (function, variable) being defined; - Name-related attributes, such as "aligned", which apply to the name (object, struct/union member, struct/union/enum tag) being defined. In particular, "aligned" is now attached to "struct" and "union" definitions, while it used to be "floated up" before. The C11 _Alignas modifier is treated like an object-related attribute, so that ``` struct s { ... }; _Alignas(64) struct s x; ``` correctly associates the alignment with "x" and not with "struct s", where it would be ignored because it was not part of the original definition of s.
* Do not expand type names when floating attributes "up" a declarationXavier Leroy2019-02-253-2/+24
| | | | | | | | | | | | | | | | | | | | | During elaboration of type declarators, non-type-related attributes such as "aligned" or "section" are "floated up" so that they apply to the thing being declared. For example, consider: ``` __attribute((aligned(16))) int * p; ``` The attribute is first attached to type `int`, then floated up to type `int *`, so that it finally applies to `p`, giving a 16-aligned pointer to int, and not a naturally-aligned pointer to 16-aligned int. What happens when the non-type-related attribute comes from a typedef? ``` typedef __attribute((aligned(16))) int i16; i16 * p; ``` CompCert used to expand the typedef then float up the attribute, resulting in `p` being a 16-aligned pointer to int. GCC and Clang produce a naturally-aligned pointer, so they do not expand the typedef before floating. The old CompCert behavior is somewhat surprising, and potentially less useful than the GCC/Clang behavior. This commit changes the floating up of non-type-related attributes so that typedefs and struct/union/enum definitions are not expanded when determining which attributes to float up. This is a first step towards mimicking the GCC/Clang behavior.
* Ignore and clean file .lia.cacheXavier Leroy2019-02-122-1/+4
| | | | This file is created by Coq when running some tactics
* Make the checker happy (#272)Vincent Laporte2019-02-123-19/+17
| | | Previously, the coqchk type- and proof-checker would take forever on some of CompCert's modules. This commit makes minimal changes to the problematic proofs so that all of CompCert can be checked with coqchk. Tested with Coq versions 8.8.2 and 8.9.0.
* Add support for Coq 8.9.0Xavier Leroy2019-02-041-3/+3
| | | | No other changes are needed to support 8.9.0.
* <stddef.h>: define NULL with type void *Xavier Leroy2019-02-041-1/+1
| | | | | | | | | | | | | | ISO C2011 7.19 para 3 says "NULL, which expands to an implementation-defined null pointer constant" ISO C2011 6.3.2.3 para 3 says "An integer constant expression with the value 0, or such an expression cast to type void *, is called a null pointer constant." So, it seems NULL can be defined either as "0" or as "(void *) 0". However, the two definitions are not equivalent in the context of a call to a variadic or unprototyped function: passing 0 when the function expects a pointer value can go wrong if sizeof(int) != sizeof(void *). This commit changes the definition of NULL to the safer one: This is what GCC and Clang do in C mode; they use "#define NULL 0" for C++ only. Fixes issue #265
* Test for NULL in variable argument listsXavier Leroy2019-02-042-1/+53
| | | | | Sometimes a vararg function receives a NULL-terminated list of pointers. This can fail if sizeof(NULL) < sizeof(void *), as this test illustrates.
* <stdbool.h>: add missing macro __bool_true_false_are_definedXavier Leroy2019-02-041-0/+1
| | | | | | As specified in ISO C99 section 7.16 and C11 section 7.18. Fixes issue #266
* Fix some URLs in the first page of the Coq HTML documentation (#263)Andre2019-01-221-5/+5
| | | | Links to machine-specific modules were garbled during editing.
* Use `Program Instance` instead of `Instance` + refine mode (#261)Maxime Dénès2018-12-272-64/+86
| | | | | | | | | | | | | CompCert currently uses `Instance` in so-called "refine" mode, where Coq drops automatically in proof mode if some members of the instance are missing. This mode is soon going to be turned off by default, see https://github.com/coq/coq/pull/9270. In order to make CompCert robust against this change, this commit replaces those occurrences of `Instance` that use "refine" mode with `Program Instance`.
* x86: wrong modeling of ZF flag for FP comparisonsXavier Leroy2018-12-202-130/+66
| | | | | | | | | | | | | | As written in the comment, ZF should be set if the two floats are equal or unordered. The "or unordered" case was missing in the original modeling of FP comparisons. - Set ZF flag correctly in the Asm.compare_floats and Asm.compare_floats32 functions. - Update the proofs in Asmgenproof1 accordingly. No change required to the code generated for FP comparisons: this code already anticipated the "or unordered" case. Problem reported by Alix Trieu.
* Add functions "ordered" and "compare" to Float and Float32Xavier Leroy2018-12-201-9/+20
| | | | | | | "compare" returns the 4 possible results w/ type "option comparison". "ordered" returns a Boolean. These functions will be used soon in the x86 port.
* Fix fixme in PackedStructs.Bernhard Schommer2018-11-201-4/+4
| | | | | | | | Instead of relying testing that the size of pointers is 64bit the size of registers should be tested. Also it should be a fatal error to reverse a long long on an architecture that does not support reverse 64bit read/writes. Bug 24982
* Fix typo in asmexpand. Bug 24953Bernhard Schommer2018-11-071-1/+1
|
* Use 'gpr_or_zero' for base register of indexed load/stores, bug 24776Michael Schmidt2018-10-202-5/+10
|
* Catch exception from elab_attr_arg.Bernhard Schommer2018-10-181-1/+4
| | | | | | Catch the exception from a non constant argument of a packed attribute and print an error. Bug 24748
* Switch conditions for eref plattforms.Bernhard Schommer2018-09-191-4/+4
| | | | | Otherwise an isel is generated if no isel is needed at all. Bug 24516
* Support __builtin_isel64 for non-EREF PPC64 platforms (#141)Xavier Leroy2018-09-181-22/+28
| | | | | | If the isel instruction is missing, it can be emulated just like we do in the 32-bit case (__builtin_isel). Follow-up to commit 51d32b92. Bug 24516
* Add builtin isel (conditional move) for int64, uint64 and _Bool (#140)Bernhard Schommer2018-09-182-1/+16
| | | | | New builtin isel variants to support conditional moves for 64bit integers and _Bool values. Bug 24516
* Bug 24518Bernhard Schommer2018-09-170-0/+0
|
* Updates for release 3.4v3.4Xavier Leroy2018-09-172-2/+2
|
* Bug 24510Bernhard Schommer2018-09-140-0/+0
|
* flocq: minor cleaning (#257)Vincent Laporte2018-09-141-3/+2
| | | | | | This change avoids relying on generated names, making the proof script compatible with ongoing evolutions of the `zify` tactic. A similar cleanup was already performed in Flocq's master sources.
* Update change log for 3.4, continuedXavier Leroy2018-09-141-2/+5
|
* Improved diagnostics: spelling, wording, etc (#138)Michael Schmidt2018-09-145-15/+15
| | | | | | | | | | | | | | | | | | * bug 24268: avoid assertion after reporting error for invalid call to builtin_debug * bug 24268, remove duplicated warning tag in lexer messages * bug 24268, fix spelling in array element designator message * bug 24268, unify 'consider adding option ...' messages * bug 24268, add spacing for icbi operands * bug 24268, uniform use of Ignored_attributes class for identical warnings * bug 24268, unify message for 'assignment to const type' to error from error/fatal error * bug 24268, in handcrafted.messages, "a xxx have been recognized" -> "a xxx has been recognized"
* Simplified code. Bug 24067Bernhard Schommer2018-09-121-8/+8
|
* Tentatively support Coq 8.8.2Xavier Leroy2018-09-121-2/+2
| | | | | It's not out yet, but based on the state of the v8.8 branch of Coq, it is very likely to be compatible with CompCert.
* Typo in OCaml version numberXavier Leroy2018-09-121-1/+1
|
* Update version and change log in preparation for public release 3.4Xavier Leroy2018-09-122-1/+63
|
* Generate a nop instruction after some ais annotations (#137)Bernhard Schommer2018-09-1214-28/+64
| | | | | | | | | | | | | | | | | | | | | | | | | | * Generate a nop instruction after ais annotations. In order to prevent the merging of ais annotations with following Labels a nop instruction is inserted, but only if the annotation is followed immediately by a label. The insertion of nop instructions is performed during the expansion of builtin and pseudo assembler instructions and is processor independent, by inserting a __builtin_nop built-in. * Add Pnop instruction to ARM, RISC-V, and x86 ARM as well as RISC-V don't have nop instructions that can be easily encoded by for example add with zero instructions. For x86 we used to use `mov X0, X0` for nop but this may not be as efficient as the true nop instruction. * Implement __builtin_nop on all supported target architectures. This builtin is not yet made available on the C side for all architectures. Bug 24067
* Fatal error instead of error for bit-fields.Bernhard Schommer2018-09-121-1/+1
| | | | | | Since the following offsetof cannot handle bit-fields we should stop earlier. Bug 24480
* Attach _Alignas to names and refactor _Alignas checks (#133)Bernhard Schommer2018-09-106-20/+22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Refactor common code of alignas. Instead of working on attributes the function now works directly on the type since the check always performed an extraction of attributes from a type. Bug 23393 * Attach _Alignas to the name. Bug 23393 * Attach "aligned" attributes to names So that __attribute((aligned(N))) remains consistent with _Alignas(N). gcc and clang apply "aligned" attributes to names, with a special case for typedefs: typedef __attribute((aligned(16))) int int_al_16; int_al_16 * p; __attribute((aligned(16))) int * q; For gcc, p is naturally-aligned pointer to 16-aligned int and q is 16-aligned pointer to naturally-aligned int. For CompCert with this commit, both p and q are 16-aligned pointers to naturally-aligned int. * Resurrect the alignment test involving typedef The test was removed because it involved an _Alignas in a typedef, which is no longer supported. However the same effect can be achieved with an "aligned" attribute, which is still supported in typedef.
generated by cgit (git 2.34.1) at 2024-05-19 01:05:26 +0000