aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
Commit message (Collapse)AuthorAgeFilesLines
* AArch64 portXavier Leroy2019-08-082-0/+6
| | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
* Make __builtin_sel available from C source codeXavier Leroy2019-07-171-0/+36
| | | | | It is type-checked like a conditional expression then translated to a call to the known builtin function.
* Remove the cparser/Builtins moduleXavier Leroy2019-07-1712-87/+62
| | | | | | | | | Move its definitions to modules C (the type `builtins`) and Env (the operations that deal with the initial environment). Reasons for the refactoring: 1- The name "Builtins" will soon be reused for a Coq module 2- `Env.initial()` makes more sense than `Builtins.environment()`.
* Change condition for warning of conditional exprBernhard Schommer2019-07-101-1/+1
| | | | | | The warning should only be active if the optimization is active, so the check is only performed when the warning is active and additionally the command line flag -Obranchless is specified.
* Compatibility with OCaml 4.08 (#302)Xavier Leroy2019-07-081-1/+1
| | | | | | | | | | | | | | | | * Do not use `Pervasives.xxx` qualified names Starting with OCaml 4.08, `Pervasives` is deprecated in favor of `Stdlib`, and uses of `Pervasives` cause fatal warnings. This commit uses unqualified names instead, as no ambiguity occurs. * Clarify "open" statements OCaml 4.08.0 has stricter warnings concerning open statements that shadow module names. Closes: #300
* New parser based on new version of the Coq backend of Menhir (#276)Jacques-Henri Jourdan2019-07-0519-3635/+472
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Deref is not safe.Bernhard Schommer2019-07-041-1/+1
|
* Added new diagnostic for non-linear conditionalsBernhard Schommer2019-07-046-1/+179
| | | | | | | | | | | | | | The new diagnostics is triggered if a conditional is used that may not be transformed into linear code by the later by the if conversion. The new diagnostic is emitted if a conditional may contain an unsafe expression or is contained within another conditional, logical and or logical or expression. An expression is unsafe if it contains a call, changes memory or if its evaluation leads to undefined behavior, for example division and modulo. Also fixes a small typo in a comment in Cutil.
* Added helper function for array types.Bernhard Schommer2019-07-042-0/+7
| | | | | The function determines whether the given type is an array type or not.
* Added statement traversal functions.Bernhard Schommer2019-07-041-107/+90
| | | | | | Refactored the checks functions by using higher order traversal functions for statements. Also introduce helper functions for the traversal of initializers.
* New additional check for void parameters. (#174)Bernhard Schommer2019-06-031-3/+5
| | | | There should only be one unnamed parameter of type void in the parameter list.
* Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-315-9/+9
| | | | | | This is a manual, partial merge of Github pull request #296 by @Fourchaux. flocq/, cparser/MenhirLib/ and parts of test/ have not been changed because these are local copies and the fixes should be performed upstream.
* Add a check for the args of unprototyped calls.Bernhard Schommer2019-05-201-3/+8
| | | | | | The arguments that are passed to an unprototyped function must also be checked to be valid types passed to a function, i.e. they must be complete types after argument conversion.
* Reworked elaboration of declarations/definitions.Bernhard Schommer2019-05-101-140/+138
| | | | | | | | | | | | Since a definition/declaration is completed with after the separator to the next init group member it is also possible to use it for example in the next init group member: char s[]="miaou", buf[sizeof s]; In order to ensure that this works the declarations are added to the environment directly during the elaboration of the init member group instead of later.
* Change to AbsInt version string.Bernhard Schommer2019-05-101-1/+1
| | | | | The AbsInt build number no longer contains "release", so it must be printed additionally.
* Check for reserved keywords.Bernhard Schommer2019-05-101-1/+8
| | | | | | `_Complex` and `_Imaginary` are reserved keywords. Since CompCert does not support these types they could be used as identifiers. However the standard requires to reject this.
* Fix various scoping issues (#163)Bernhard Schommer2019-05-101-51/+56
| | | | | | | | | Pass the environment to all expr eval functions since the functions themselve may be called recursively and modify the environment. The other change introduces new scopes that are strict subsets of their surrounding scopes for if, switch, while, do and for statement, as prescribed by ISO C standards.
* Ensure flushing of the error formatter.Bernhard Schommer2019-05-101-0/+4
| | | | | Since the error formatter is not automatically flushed at program exit we need to ensure that it is flushed at exit.
* Reset scope ids later.Bernhard Schommer2019-04-161-1/+1
| | | | | | | In order to avoid adding ranges to the wrong scopes due to inlining they are numbered consecutively for the whole compilation unit. Bug 26234
* 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
* Revised attachment of name attributes to structs, unions, enumsXavier Leroy2019-02-251-6/+21
| | | | | | | | | | | | | | | | | | 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.
* Distinguish object-related and name-related attributesXavier Leroy2019-02-253-11/+21
| | | | | | | | | | | | | | | | | 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.
* 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
* 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
* Improved diagnostics: spelling, wording, etc (#138)Michael Schmidt2018-09-143-6/+6
| | | | | | | | | | | | | | | | | | * 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"
* 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-103-12/+16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * 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.
* Typo in commentXavier Leroy2018-09-031-1/+1
|
* Move parameter check.Bernhard Schommer2018-09-031-2/+6
| | | | | | Instead of performing the check only for parameters of function definitions also perform it for function declarations. Bug 23393
* New diagnostic for reduced alignment (#117)Bernhard Schommer2018-08-293-3/+38
| | | | | | | The new diagnostic triggers if an `_Alignas` or an `aligned` attribute or a `packed` attribute requests an alignment smaller than the natural alignment. Bug 23389
* Edit documentation comments for [alignas_attribute] and [has_std_alignas]Xavier Leroy2018-08-241-2/+3
|
* More standard compliant handling of _Alignas.Bernhard Schommer2018-08-241-0/+11
| | | | | | | | | | | The C11 standard disallows the usage of _Alignas for: - Bit-field members of struct or union types - Typedefs - Function Defintions - Parameters of functions It is still allowed to use the gcc attribute for these constructs. Bug 23391
* Add check for _Alignas attribute.Bernhard Schommer2018-08-242-0/+6
| | | | | | The check tests whether the standard _Alignas is contained within a given attribute list. Bug 23391
* Reimplement attr_array_applicable in terms of class_of_attributeXavier Leroy2018-08-241-3/+2
| | | | | | | | | | | | | Since commit 5963ac4, "aligned" attributes and _Alignas qualifiers are represented differently, causing them to be treated differently by the previous implementation of Cutil.attr_array_applicable. This is incorrect and inconsistent with what happens during elaboration of array types in Elab. This PR reimplements attr_array_applicable in terms of class_of_attribute. Just like during elaboration, attributes of the Attr_type class are applied to the type of array elements, other attributes stay attached to the array type.
* Preserve attribute(("aligned")) in the AST, don't map it to _AlignasXavier Leroy2018-08-242-2/+3
| | | | | | | | | | | | | | We used to recognize attribute(("aligned"(N))) and map it to _Alignas(N) during elaboration. However, we want to restrict the places where _Alignas can occur, as standardized in ISO C11, while leaving more freedom for the placement of the "aligned" attribute. As a first step in this direction, this commit keeps the "aligned" attribute unchanged in the AST, and distinct from _Alignas attributes. Both attributes are honored when it comes to determining the actual alignment of a type.
* Diagnostic for wrong application of restrict (#119)Bernhard Schommer2018-08-213-7/+33
| | | | | | Restrict is only allowed for pointers whose referenced type is an object type or incomplete type, but not a function type. Bug 23397
* Improve support and diagnostic for type qualified arrays (#118)Bernhard Schommer2018-08-203-1/+18
| | | | | | | | | | | | | | | | * Add diagnostic for type qualified arrays that occur in the wrong place Arrays with type qualifiers (e.g. int t[const 5]) are only allowed as function parameters and for them only the outermost array type derivation. Bug 23400 * Keep attributes from array for argument conversion Type qualifiers of arrays in function parameters are just syntactic sugar to allow adding them to the resulting pointer type. Hence, when a qualified array type such as `int t[const 5]` decays into a pointer type during argument conversion, the pointer type should be qualified, e.g. `int * const t`.
* Added warning for incomplete tentative static defs (#114)Bernhard Schommer2018-08-203-4/+11
| | | | | | Tentative static definitions with incomplete type are not allowed in C99. However most popular compilers support them and warn about them. Bug 23377
* Additional checks for flex arrays in structs (#93)Bernhard Schommer2018-08-205-5/+30
| | | | | | | | | | | | | | | * Error for structs with only flex array member Flexible array members are only allowed if another member exists. Bug 23324 * Added checks for nesting of structs with flex array members Warn if a struct with a flex array member is used as array element or member of another struct. Such usage is dubious. Bug 23324 Don't warn if the struct-with-flex-array is a member of an union.
* Add sizeof_reg and new Machine configurations (#129)Bernhard Schommer2018-08-203-1/+19
| | | | | | | | | | | | | Since the size of integer registers is not identical to the size of pointers for the ppc64 and e5500 model the check for register pairs in ExtendedAsm does not work correctly. In order to avoid this a new field sizeof_intreg is introduced in the Machine configuration which describes the size of integer registers. New configurations for the ppc64 and e5500 model are added and used. Bug 24273
* Turn error into fatal error for unnamed parameter.Bernhard Schommer2018-08-201-2/+4
| | | | | | Since the parameter name gets used in other error messages it results in messages without names. Bug 24283
* For "packed" attribute, check that 3rd parameter is 0 or 1Xavier Leroy2018-08-171-1/+1
| | | | | | | It's meant as a Boolean (byte-swap or not), so any other value is dangerous. The error message is the generic "ill-formed 'packed' attribute". Maybe we don't need a custom error message.
* Wrong AST for GCC-style attributesXavier Leroy2018-08-171-1/+1
| | | | | The list of arguments to the attribute was missing a reverse, hence attribute(("foo"(1,2,3))) was actually read as attribute(("foo"(3,2,1))).
* Check for bit-fields in __builtin_offsetofXavier Leroy2018-08-171-1/+4
| | | | __builtin_offsetof(struct s, f) is an error if f is a bit-field.
* Issue with packed structs and sizeof, alignof, offsetof in cparser/Xavier Leroy2018-08-174-95/+139
| | | | | | | | | | | | | | | | | | | | | | | | | | | CompCert has two implementations of sizeof, alignof and offsetof (byte offset of a struct field): - the reference implementation, in Coq, from cfrontend/Ctypes.v - the implementation used during elaboration, in OCaml, from cparser/Cutil.ml The reference Coq implementation is used as much as possible, but sometimes during elaboration the size of a type must be computed (e.g. to compute array sizes), or the offset of a field (e.g. to evaluate __builtin_offsetof), in which case the OCaml implementation is used. This causes issues with packed structs. Currently, the cparser/Cutil.ml functions ignore the "packed" attribute on structs. Their results disagree with the "true" sizes, alignments and offsets computed by the cfrontend/Ctypes.v functions after source-to-source transformation of packed structs as done in cparser/PackedStruct.ml. For example: ``` struct __packed__(1) s { char c; short s; int i; }; assert (__builtin_offsetof(struct s, i) == 3); assert (sizeof(struct s) = sizeof(char[sizeof(struct s)])); ``` The two assertions fail. In the first assertion, __builtin_offsetof is elaborated to 4, because the packed attribute is ignored during elaboration. In the second assertion, the type `char[sizeof(struct s)]` is elaborated to `char[8]`, again because the packed attribute is ignored during elaboration, while the other `sizeof(struct s)` is computed as 7 after the source-to-source transformation of packed structs. This commit changes the cparser/Cutil.ml functions so that they take the packed attribute into account when computing sizeof, alignof, offsetof, and struct_layout. Related changes: * cparser/Cutil: add `packing_parameters` function to extract packing info from attributes * cparser/Cutil: refactor and share more code between sizeof_struct, offsetof, and struct_layout * cparser/Elab: check the alignment parameters given in packed attributes. (The check was previously done in cparser/PackedStruct.ml but now it would come too late.) * cparser/Elab: refactor the checking of alignment parameters between _Alignas, attribute((aligned)), __packed__, and attribute((packed)). * cparser/PackedStructs: simplify the code, some functionality was moved to cparser/Cutil, other to cparser/Elab * cfrontend/C2C: raise an "unsupported" error if a packed struct is defined and -fpacked-structs is not given. Before, the packed attribute would be silently ignored, but now doing so would cause inconsistencies between cfrontend/ and cparser/. * test/regression/packedstruct1.c: add tests to compare the sizes and the offsets produced by the elaborator with those obtained after elaboration.
* Added a check for parameters without identifiers. (#128)Bernhard Schommer2018-08-171-5/+7
| | | | | It is not allowed in C to have a parameter in a parameter list without an identifier. Bug 24283
* Earlier check for invalid asm outputs. (#130)Bernhard Schommer2018-08-172-2/+5
| | | | | | Since a non modifiable lvalue is an invalid asm output it should be checked earlier, otherwise this leads to a retyping error later. Bug 24285
* Also check parameters for unknown attributes.Bernhard Schommer2018-08-161-0/+1
| | | | | | Parameters also need to be checkd for unknown attributes, like all other declarations. Bug 24277
generated by cgit (git 2.34.1) at 2024-06-26 18:26:49 +0000