aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
Commit message (Collapse)AuthorAgeFilesLines
* Distinguish object-related and name-related attributesXavier Leroy2019-02-251-2/+3
| | | | | | | | | | | | | | | | | 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.
* Use `Program Instance` instead of `Instance` + refine mode (#261)Maxime Dénès2018-12-271-23/+33
| | | | | | | | | | | | | 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`.
* Improved diagnostics: spelling, wording, etc (#138)Michael Schmidt2018-09-141-8/+8
| | | | | | | | | | | | | | | | | | * 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"
* Attach _Alignas to names and refactor _Alignas checks (#133)Bernhard Schommer2018-09-101-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * 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.
* Import prim token notations before using themJason Gross2018-08-273-1/+3
| | | | | | | | | This is required for compatibility with https://github.com/coq/coq/pull/8064, where prim token notations no longer follow `Require`, but instead follow `Import`. Closes #246 Closes #250
* Issue with packed structs and sizeof, alignof, offsetof in cparser/Xavier Leroy2018-08-171-1/+3
| | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Compatibility with OCaml 4.07 (#241) continuedXavier Leroy2018-07-101-1/+1
| | | | | This is a follow-up to commit 6e1a5ce. Another `open! Floats` is needed.
* String literals are l-values and have array types (#116)Bernhard Schommer2018-05-271-6/+7
| | | | | | | | | | | | | | | | | * Allow strings literals as lvalues. Strings and WStrings literals are lvalues, thus it is allowed to take their addresses. Bug 23356. * String literals have types "array of (wide) char", not "pointer to (wide) char" The pointer types were a leftover from the early, CIL-based C frontend. * Remove special case for sizeof("string literal") during elaboration No longer needed now that literals have array types.
* Record value of constant expression in C.Scase constructorXavier Leroy2018-04-271-1/+1
| | | | | | | | | | | | The Elab pass checks that the argument of 'case' is a compile-time constant expression. This commit records the value of this expression in the C.Scase AST generated by Elab, so that it can be used for further diagnostics, i.e. checking (in Elab) for duplicate cases. Note that C2C ignores the recorded value and recomputes the value of the expression using Ceval.integer_expr. This is intentional: Ceval.integer_expr is more trustworthy, as it is formally verified against the CompCert C semantics.
* Warn when volatile struct is assigned to a normal structBernhard Schommer2018-04-191-0/+3
| | | | | | | | | | | | | | Adds a warning when a volatile struct is assigned to another struct, that the volatile qualifier is ignored in this context. Example: ``` volatile struct S s; struct S t; t = s; // did not warn before; now it warns s = t; // did warn already ``` Bug 23489
* Print size argument of Init_space as Z not as int32Xavier Leroy2018-03-131-1/+1
| | | | | Init_space has an argument of type Z and it can exceed the range of a 32-bit integer. Reported by Frédéric Besson.
* Do not use "Require" inside sections (#224)Xavier Leroy2018-03-121-2/+1
| | | | | | This will soon be deprecated by Coq. Manual merge of pull request #224 by vbgl. Closes: #224
* Improve and simplify error messages.Bernhard Schommer2018-03-071-5/+1
| | | | | | | | The checks on the argument and format arguments are now performed during C2C translation by calling the validate_ais_annotations function and result in an error instead of a warning in the backend to be more consistent with the rest of the builtin functions.
* Reactivated and improved ais annotations.Bernhard Schommer2018-03-061-24/+35
| | | | | | | | | | | | | | | | | | The ais annotations are now handled in a separate file shared between all architectures. Also two different variants of replacements are supported, %e which expands to ais expressions and %l which also expands to an ais expression but is guaranted to be usable as l-value in the ais annotation. Otherwise the new warning is Wrong_is_parameter is generated. Also an error message is generated if floating point variables are used in ais annotations since a3 does not support them at the moment. Additionally an error message is generated for plain volatile variables used, since they will enforce a volatile load and result in the value being passed to the annotation instead of the address as other global variables.
* Truncation of array sizes when converting them to Coq's Z typeXavier Leroy2018-02-081-6/+8
| | | | | | | | | | The size (number of elements) of an array type is represented as an OCaml int64 in the parse tree, and as a Coq Z in the CompCert C AST. However, the C2C.convertInt function used to do this conversion produces a Coq int (32 bits) type, taking the array size modulo 2^32. This is not correct, esp. on a 64-bit target. This commit refactors C2C around three integer conversion functions: convertInt32 producing a Coq "int" (32 bit) convertInt64 producing a Coq "int64" (64 bit) convertIntZ producing a Coq "Z" (arbitrary precision)
* Refactor the handling of errors and warnings (#44)Bernhard Schommer2018-02-082-17/+20
| | | | | | | | | | | | | | | | | * Module Cerrors is now called Diagnostic and can be used in parts of CompCert other than cparser/ * Replaced eprintf error. Instead of having eprintf msg; exit 2 use the functions from the Diagnostics module. * Raise on error before calling external tools. * Added diagnostics to clightgen. * Fix error handling of AsmToJson. * Cleanup error handling of Elab and C2C. *The implementation of location printing (file & line) is simplified and correctly prints valid filenames with invalid lines.
* Deactivate ais_annotations again.Bernhard Schommer2017-12-121-24/+25
|
* Correct test for noinline. Bug 22642Bernhard Schommer2017-12-111-1/+1
|
* Introduce and use C2C.atom_inline function with 3-valued resultXavier Leroy2017-12-081-11/+5
| | | | | | Instead of two Boolean tests C2C.atom_is_{no,}inline, have a single C2C.atom_inline function that returns one of the three possible values stored in the the a_inline field.
* Store the different inlining cases.Bernhard Schommer2017-12-081-7/+25
| | | | | | | In order to correctly support the noinline attribute we must store whether the function was specified with an inline specifer, had a noinline attribute or nothing. Bug 22642
* Pull request #192: improve the printing of Clight intermediate codeXavier Leroy2017-11-221-10/+26
| | | | So that it looks more like valid C source.
* Remove ais_annot_intval.Bernhard Schommer2017-10-241-13/+0
|
* Prefix ais annotations with location.Bernhard Schommer2017-10-241-2/+4
| | | | | | The file and line information are now stored as comment string at the start of each annotation. Bug 22462
* Merge pull request #191 from sigurdschneider/masterXavier Leroy2017-10-202-0/+2
|\ | | | | | | Ensure FunInd or Recdef is imported if functional induction is used. This is necessary for Coq 8.7.0.
| * Ensure FunInd or Recdef is imported if functional induction is usedSigurd Schneider2017-07-202-0/+2
| | | | | | | | | | | | Coq 8.7 does not load FunInd in prelude anymore, so this is necessary. Recdef exports FunInd, so if Recdef is imported, importing FunInd is not required.
* | New support for inserting ais-annotations.Bernhard Schommer2017-10-193-7/+44
| | | | | | | | | | | | | | | | | | | | | | | | The ais annotations can be inserted via the new ais variants of the builtin annotation. They mainly differe in that they have an address format specifier '%addr' which will be replaced by the adress in the binary. The implementation simply prints a label for the builtin call alongside a the text of the annotation as comment and inserts the annotation together as acii string in a separate section 'ais_annotations' and replaces the usages of the address format specifiers by the address of the label of the builtin call.
* | Moved common buitlins to C2C gernic_builtins.Bernhard Schommer2017-09-261-1/+11
| |
* | Remove coq warnings (#28)Bernhard Schommer2017-09-228-50/+50
| | | | | | | | Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
* | Prefixed runtime functions.Bernhard Schommer2017-08-251-16/+16
|/ | | | | | | The runtime functions are prefixed with compcert in order to avoid potential clashes with runtime/builtin functions of other compilers. Bug 22062
* SimlLocals.Sdebug_var: wrong type for 64-bit platformsXavier Leroy2017-07-091-1/+1
| | | | | | Fixes: Github issue #190. Tint was used instead of the correct Tptr.
* Early optimization of redundant *& and &* addressingsXavier Leroy2017-05-293-8/+59
| | | | | | Particularly annoying was the `*&x` sequence where `x` is a local variable, which would force stack-allocation of `x` early, generating extra loads and stores that could not always be optimized later (in CSE and Deadcode). The `*&` sequences and, by symmetry, the `&*` sequences are now eliminated early during Clight generation, via smart constructors.
* Do not generate code for "inline definitions"Bernhard Schommer2017-04-071-8/+15
| | | | | | | | | ISO C99 states that "inline defintions", functions with inline specifier that are not extern, does not provide an external definition and another compilation unit can contain an external definition. Thus in the case of non-static inline functions no code should be generated. Bug 21343
* attempt to optimize empty if/then/else statementsMichael Schmidt2017-04-063-7/+32
|
* Added gcc noinline attribute.Bernhard Schommer2017-02-191-0/+1
| | | | The noinline attribute prevents functions from inlining.
* Added unused attribute and simplified checks.Bernhard Schommer2017-02-171-1/+2
| | | | | | | | | The attribute unused can be used to indicate if a variable or parameter is unused and no warning should be emitted for it. Furthermore this commit simplifies the check by adding a generic function to traverse the program. Bug 19872
* Replace "Implicit Arguments" with "Arguments"Xavier Leroy2017-02-131-2/+2
| | | | | This silences a warning of Coq 8.6. Some "Implicit Arguments" remain in flocq/ but I'd rather not diverge from the released version of flocq if at all possible.
* Use "Local" as prefixXavier Leroy2017-02-132-3/+3
| | | | | Open Local becomes Local Open. This silences Coq 8.6's warning. Also: remove one useless Require-inside-a-module that caused another warning.
* Merge branch 'coq-8.6' of https://github.com/maximedenes/CompCert into ↵Xavier Leroy2017-02-132-7/+9
|\ | | | | | | maximedenes-coq-8.6
| * Some backward compatible Ltac fixes, necessary for 8.6.Maxime Dénès2017-01-091-5/+7
| |
| * An hypothesis has changed name.Maxime Dénès2017-01-091-1/+1
| | | | | | | | Not sure why, but it would be safer not to rely on automatic naming.
| * The subst tactic has become more powerful.Maxime Dénès2017-01-091-1/+1
| |
* | More tweaking of module 'open'Xavier Leroy2017-02-091-8/+10
| | | | | | | | I really like to have Floats and Values opened. The other opens I can live without, but Floats.Float.zero is just wrong.
* | Merge branch 'elaboration-of-attributes'Xavier Leroy2017-02-061-1/+15
|\ \
| * | Preliminary support for the "noreturn" attributeXavier Leroy2017-02-061-1/+2
| | | | | | | | | | | | | | | - Mark the "noreturn" attribute as related to function types, so that it is correctly attached to the nearest enclosing function type. - Add this attribute on functions declared / defined _Noreturn (with the C2011 keyword). The information is not used presently but could be useful later.
| * | Refactor the classification of attributesXavier Leroy2017-02-031-0/+13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Introduce Cutil.class_of_attribute to return the class of the given attribute: one among Attr_type attribute related to types (e.g. "aligned") Attr_struct attribute related to struct/union/enum types (e.g. "packed") Attr_function attribute related to function types (e.g. "noreturn") Attr_name attribute related to variable and function declarations (e.g. "section") Attr_unknown attribute was not declared Cutil.declare_attribute is used to associate a class to a custom attribute. Standard attributes (const, volatile, _Alignas, etc) are Attr_type. cfronted/C2C.ml: declare the few attributes that CompCert honors currently. cparser/GCC.ml: a bigger list of attributes taken from GCC, for reference only.
| * | Revised elaboration of attributesXavier Leroy2017-01-311-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The treatment of attributes in the current CompCert is often surprising. For example, attribute(xxx) char * x; is parsed as "x is a pointer to a (char modified by attribute "xxx")", while for most attributes (e.g. section attributes) the expected meaning is "x, modified by attribute "xxx", has type pointer to char". CompCert's current treatment comes from the fact that attributes are processed very much like the standard type modifiers `const` and `volatile`, i.e. const char * x; is really "x is a pointer to a const char", not "x is a const pointer to char". This experiment introduces a distinction between type-related attributes (which include the standard modifiers `const` and `volatile`) and other attributes. The other, non-type-related attributes are "floated up" during elaboration so that they apply to the variable or function being declared or defined. In the examples above, attribute(xxx) char * x; // "attribute(xxx)" applies to "x" const char * x; // "const" applies to "char" This may be a step in the right direction but is not the final story. In particular, the `packed` attribute is special-cased when applied to `struct`, like it was before, and future attributes concerning calling conventions would need to be floated up to function types but not higher than that.
* | | Cleanup opensBernhard Schommer2017-02-061-69/+62
| | |
* | | Removed shadowing problems.Bernhard Schommer2017-02-061-9/+9
| | | | | | | | | | | | The clashing identifiers are now referenced explicitly.
* | | Inlined open of ASTBernhard Schommer2017-02-061-7/+6
|/ /
* / Simplified C2C.error.Bernhard Schommer2017-01-182-19/+16
|/ | | | | | | Instead of just accepting a string the function is changed to accept a format string. This removes a lot of artificial sprintfs in calls to the functions. Bug 19872
generated by cgit (git 2.34.1) at 2024-06-26 18:18:22 +0000