| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
What's new:
1. A rewrite of the Coq interpreter of Menhir automaton, with
dependent types removing the need for runtime checks for the
well-formedness of the LR stack. This seem to cause some speedup on
the parsing time (~10% for lexing + parsing).
2. Thanks to 1., it is now possible to avoid the use of int31 for
comparing symbols: Since this is only used for validation,
positives are enough.
3. Speedup of Validation: on my machine, the time needed for compiling
Parser.v goes from about 2 minutes to about 1 minute. This seem to
be related to a performance bug in the completeness validator and
to the use of positive instead of int31.
3. Menhir now generates a dedicated inductive type for
(semantic-value-carrying) tokens (in addition to the already
existing inductive type for (non-semantic-value-carrying)
terminals. The end result is that the OCaml support code for the
parser no longer contain calls to Obj.magic. The bad side of this
change is that the formal specification of the parser is perhaps
harder to read.
4. The parser and its library are now free of axioms (I used to use
axiom K and proof irrelevance for easing proofs involving dependent
types).
5. Use of a dedicated custom negative coinductive type for the input
stream of tokens, instead of Coq stdlib's `Stream`. `Stream` is a
positive coinductive type, which are now deprecated by Coq.
6. The fuel of the parser is now specified using its logarithm instead
of its actual value. This makes it possible to give large fuel
values instead of using the `let rec fuel = S fuel` hack.
7. Some refactoring in the lexer, the parser and the Cabs syntax tree.
The corresponding changes in Menhir have been released as part of
version 20190626. The `MenhirLib` directory is identical to the
content of the `src` directory of the corresponding `coq-menhirlib`
opam package except that:
- In order to try to make CompCert compatible with several Menhir
versions without updates, we do not check the version of menhir
is compatible with the version of coq-menhirlib. Hence the
`Version.v` file is not present in CompCert's copy.
- Build-system related files have been removed.
|
|
|
|
| |
The `_Alignas(expr)` construct is not C11, only `_Alignas(type)` is.
|
| |
|
|
|
|
|
|
| |
This only means that there must be one identifier at the begining
and then a designator.
Bug 20765
|
|
|
|
|
|
|
|
|
| |
The c standard allows member designators for offsetof. The current
implementation works by recursively combining the offset of each
of the member designators. For array access the size of the
subtypes is multiplied by the index and for members the offset of
the member is calculated.
Bug 20765
|
|
|
|
|
|
|
|
|
|
|
|
| |
The implementation of offsetof as macro in the form
((size_t) &((ty*) NULL)->member) has the problem that it cannot be
used everywhere were an integer constant expression is allowed,
for example in initiliazers of global variables and there is also
no check for the case that member is of bitifield type.
The new implementation adds a builtin function for this which is
replaced by an integer constant during elaboration.
Bug 20765
|
|\
| |
| | |
Added the _Noreturn keyword.
|
| |
| |
| |
| |
| |
| |
| |
| | |
CompCert now recognizes the C11 _Noreturn function specifier and
emits a simple warning for functions declared _Noreturn containing
a return statement. Also the stdnoreturn header and additionally
the stdalign header are added.
Bug 18541
|
|/ |
|
| |
|
|
|
|
| |
and merging two error states into one. There should be no observable change.
|
| |
|
|
|
|
| |
handcrafted.messages
|
|\ |
|
| | |
|
| |
| |
| |
| |
| | |
This affects in which states errors are detected,
but does not change the language that is accepted.
|
| |
| |
| |
| | |
This allows us to give a better error message in one state.
|
| |
| |
| |
| |
| |
| |
| | |
For the first one, this is fine; the error is caught by a type check later on.
For the second one, it is temporary. More thought is needed about the syntax
of K&R functions anyway, as Jacques-Henri and I discovered that it is currently
broken (it mis-interprets some function definitions).
|
| | |
|
| |
| |
| |
| |
| |
| | |
list.
This saves 7 states and 4 error states.
|
| |
| |
| |
| |
| | |
This creates more states and does not change the number of error states.
It should make it easier to give a good error message in at least 2 states.
|
| |
| |
| |
| |
| |
| |
| | |
[declaration_specifier_no_typedef_name*].
This replaces a right-recursive list with a left-recursive list.
This saves 2 states and 6 error states.
|
| |
| |
| |
| | |
This results in slightly fewer states.
|
| |
| |
| |
| | |
elegant manner.
|
| |
| |
| |
| |
| |
| | |
a left-recursive list.
This further reduces the number of states (and error states).
|
| |
| |
| |
| | |
This saves a few states.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This parameter is passed down in [declaration_specifiers(declaration(phantom))].
This allows us to distinguish between three calling contexts for [declaration_specifiers]:
- we are definitely in a parameter declaration;
- we are definitely in a declaration (e.g., in a block);
- we are in a declaration or in a function definition (i.e., at the top level).
This allows us to give better error messages.
For instance, when inside a block, we know that this cannot be the beginning
of a function definition.
|
| |
| |
| |
| |
| |
| |
| |
| | |
This does not change the automaton at all.
It allows us to distinguish more easily between two contexts:
- the beginning of a declaration or function definition;
- the beginning of a parameter declaration.
This leads to better error messages.
|
| |
| |
| |
| |
| |
| |
| | |
This allows distinguishing two uses of abstract_declarator, within a type_name
and within a parameter_declaration. This provides more static context and
allows giving a better syntax error message, as this allows us know what is
expected next: a closing parenthesis or a comma.
|
| | |
|
| | |
|
| |
| |
| |
| |
| | |
These productions were used to give better error messages in some situations.
They are no longer useful, since we are building a whole new system for reporting errors.
|
| |
| |
| |
| |
| |
| |
| | |
[declaration_specifiers_no_type?].
Inlining these options was not necessary.
This reduces the number of states in the automaton.
|
| | |
|
| | |
|
| |
| |
| |
| | |
This leads to a smaller automaton.
|
| |
| |
| |
| |
| |
| | |
declarators and FOR loops.
This leads to fewer automaton states, and potentially better error messages.
|
| |
| |
| |
| |
| |
| |
| | |
This leads to a small savings in the number of states (which could
become greater in the future if we decide to parameterize expressions).
If desired, the old automaton could be recovered by marking the binary
operators as %inline.
|
| |
| |
| |
| | |
This is analogous to the previous commit.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
[struct_or_union_specifier].
The old version was strictly equivalent to using [ioption(other_identifier)].
The new version uses [option(other_identifier)] instead, that is, [other_identifier?].
Technically, this means that [set_id_type i OtherId] is called slightly earlier (at
the opening brace, instead of at the closing brace), but this does not make any
difference, since the re-classification of identifiers affects only the second
parsing phase.
|
| |
| |
| |
| |
| |
| |
| | |
A TYPEDEF_NAME is already classified as a [TypedefId] by the lexer,
and similarly, a VAR_NAME is already classified as a [VarId].
Thus, the removed calls had no effect.
The remaining calls to [set_id_type] are useful, as they can re-classify a token.
|
| |
| |
| |
| |
| |
| | |
i OtherId].
This causes no change in the automaton.
|
| |
| |
| |
| | |
I missed this opportunity in the previous commit.
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The existing [option(X)] was marked %inline, and has been renamed [ioption(X)].
A new [option(X)], which is not marked %inline, has been introduced.
The grammar now uses [option] everywhere, except where [ioption] is necessary
in order to avoid conflicts.
This reduces the number of states in the automaton. The number of LR(0) cores
drops from 857 to 712.
|
| |
| |
| |
| | |
This violates the 80-column width limit, but is really important.
|
| |
| |
| |
| |
| |
| | |
- Added a Cabs.PROTO_OLD constructor to Cabs.decl_type
- Refactored the Parser.vy and pre_parser.mly grammars
- Rewritten the conversion of old function definitions to new-style
|
|/ |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
was not parsed correctly:
typedef int a;
int f() {
for(int a; ;)
if(1);
a * x;
}
Additionnaly, I tried to add some comments in the pre-parser code,
especially for the different hacks used to solve various conflicts.
|
| |
|
|
|
|
| |
The CompCert back-end already treats "asm" inserts as "volatile" in GCC's sense (performing unpredictable side-effects), so no change is required outside of the parser.
|