aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* andn / orn long complete I thinkDavid Monniaux2019-03-182-0/+19
|
* selection of andn/orn on longDavid Monniaux2019-03-182-0/+10
|
* some more andn / ornDavid Monniaux2019-03-183-0/+28
|
* andn/orn start being generatedDavid Monniaux2019-03-183-8/+22
|
* andn / orn suiteDavid Monniaux2019-03-186-7/+34
|
* orn / andn in asmDavid Monniaux2019-03-184-4/+50
|
* some more about andn/ornDavid Monniaux2019-03-182-0/+24
|
* begin andn ornDavid Monniaux2019-03-183-0/+87
|
* stats on chunks etc.David Monniaux2019-03-171-3/+5
|
* isolate the slow partDavid Monniaux2019-03-172-3/+4
|
* experiments on what's slowDavid Monniaux2019-03-171-136/+12
|
* longer testsDavid Monniaux2019-03-171-1/+5
|
* compactify unrolled codeDavid Monniaux2019-03-171-143/+26
|
* expand hDavid Monniaux2019-03-171-17/+33
|
* expand hDavid Monniaux2019-03-171-17/+33
|
* the inliner is rottenDavid Monniaux2019-03-161-26/+44
|
* long nand, nor, nxorDavid Monniaux2019-03-1612-12/+151
|
* nxorDavid Monniaux2019-03-1613-4/+64
|
* nor implementeDavid Monniaux2019-03-168-1/+44
|
* partial norwDavid Monniaux2019-03-165-9/+26
|
* nand is implementedDavid Monniaux2019-03-167-2/+39
|
* some more nandDavid Monniaux2019-03-164-3/+48
|
* nand debutDavid Monniaux2019-03-163-0/+18
|
* fix problem with ALU reservation tablesDavid Monniaux2019-03-161-1/+3
|
* 32-bit rotate finishedDavid Monniaux2019-03-167-6/+27
|
* select rotate ops 32-bitDavid Monniaux2019-03-163-2/+74
|
* some more progress on rotateDavid Monniaux2019-03-162-0/+6
|
* ValueAOp rotate 32-bitDavid Monniaux2019-03-161-0/+1
|
* instruction rotateDavid Monniaux2019-03-162-0/+3
|
* Removing SelectLong.v from the git repo (compiled from SelectLong.vp)Cyril SIX2019-03-152-800/+1
|
* better robustness wrt exceptionsDavid Monniaux2019-03-141-5/+9
|
* le Makefile passeDavid Monniaux2019-03-141-2/+11
|
* test for memcpy builtinDavid Monniaux2019-03-131-0/+15
|
* Merge branch 'mppa_postpass' of ↵David Monniaux2019-03-131-4/+3
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * Corrigé certaines latences (Store -> 1 i/o 3, Set -> 4 i/o 3)Cyril SIX2019-03-131-4/+3
| |
* | with timingDavid Monniaux2019-03-132-2/+7
|/
* Fix for CompCert 3.5Cyril SIX2019-03-131-0/+1
|
* Merge branch 'master' into mppa_postpassCyril SIX2019-03-1329-290/+564
|\ | | | | | | | | | | Conflicts: .gitignore runtime/include/stdbool.h
| * 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
generated by cgit (git 2.34.1) at 2024-07-12 05:18:39 +0000