aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
Commit message (Collapse)AuthorAgeFilesLines
...
| * | | Merge branch 'mppa-cse2' of ↵David Monniaux2020-03-031-4/+36
| |\ \ \ | | |/ / | |/| | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
* | | | Merge branch 'mppa-work' into mppa-threadCyril SIX2020-02-259-76/+232
|\ \ \ \
| * | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2020-02-248-74/+229
| |\| | | | | | | | | | | | | | | | | | mppa-work-upstream-merge
| | * | | Support re-normalization of values returned by function callsXavier Leroy2020-02-212-33/+137
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Some ABIs leave more flexibility concerning function return values than CompCert expects. For example, the x86 ABI says that a function result of type "char" is returned in register AL, leaving the top 24 bits of register EAX unspecified, while CompCert expects EAX to contain 32 valid bits, namely the zero- or sign-extension of the 8-bit result. This commits adds a general mechanism to insert "re-normalization" conversions on the results of function calls. Currently, it only deals with results of small integer types, and inserts zero- or sign-extensions if so instructed by a platform-dependent function, Convention1.return_value_needs_normalization. The conversions in question are inserted early in the front-end, so that they can be optimized away in the back-end. The semantic preservation proof is still conducted against the CompCert model, where the return values of functions are already normalized. What the proof shows is that the extra conversions have no effect in this case. In future work we could relax the CompCert model, allowing functions to return values that are not normalized.
| | * | | Refine the type of function results in AST.signatureXavier Leroy2020-02-216-39/+78
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Before it was "option typ". Now it is a proper inductive type that can also express small integer types (8/16-bit unsigned/signed integers). One benefit is that external functions get more precise types that control better their return values. As a consequence, the CompCert C type preservation property now holds unconditionally, without extra typing hypotheses on external functions.
| | * | | More precise determination of small data accesses (#220)Bernhard Schommer2020-02-201-3/+15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We can get linker errors for addresses of the form "symbol + offset" where "symbol" is in the small data area and "offset" is large enough to overflow the relative displacement from the SDA base register. To avoid this, this commit enriches `C2C.atom_is_small_data`, which is the implementation of `Asm.symbol_is_small_data` in the PPC port, with a check that the offset is within the bounds of the symbol. If it is not, `Asm.symbol_is_small_data` returns `false` and Asmgen produces an absolute addressing instead of a SDA-relative addressing. To implement the check, we record the sizes of symbols in the atom table, just like we already record their alignments.
| * | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2020-02-132-2/+3
| |\| | | | | |/ / | |/| | | | | | mppa-work-upstream-merge
| | * | Take the sign into account for int to ptr cast.Bernhard Schommer2020-02-122-2/+3
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Casting from an integer constant to pointer on 64 bit architectures did not take the signedness into account and always interpreted the integer as unsigned which causes some incompatibility with libc implementations.
* | | | thread local declarations now workDavid Monniaux2020-02-241-1/+5
| | | |
* | | | it now works, no more ugly hack to access thread local dataDavid Monniaux2020-02-241-0/+9
| | | |
* | | | seems to process _Thread_local but not till backendDavid Monniaux2020-02-241-7/+14
|/ / /
* | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-12-091-0/+5
|\| | | | | | | | | | | mppa-work-upstream-merge
| * | Fix for AArch64 alignment problem (#206)Bernhard Schommer2019-11-281-0/+5
| | | | | | | | | | | | | | | | | | | | | | | | | | | In addressing modes for load and store instructions, the offset must be a multiple of the memory size being accessed. When accessing global variables, this may not be the case if the alignment of the variable is less than its size. Errors occur at link time. This PR extends the check for a representable offset for the addressing of global variables to also check whether the variable is correctly aligned. Only if both conditions are met can we generate the short sequence Padrp / ADadr. Otherwise we go through the generic loadsymbol sequence.
* | | Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-09-202-17/+45
|\| | | |/ |/| | | mppa-work-upstream-merge
| * -dclight output: use nicer names for temporary variablesXavier Leroy2019-09-161-2/+11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The temporary variables introduced by SimplLocals reuse the same integer identifiers as the local variables they come from. This commit ensures that these variables are printed as "$var", where "var" is the original variable name, instead of "$NNN" as before. The "$NNN" form is retained for temporary variables that do not correspond to a source-level local variable, such as the temporary variables introduced by SimplExpr. This commit should make no difference for "ccomp -dclight", because the Clight that is printed is the Clight version 1 produced by SimplExpr, where every temporary is fresh and does not correspond to a source-level local variable. This commit does change the output of "clightgen -dclight", because the Clight that is printed is the Clight version 2 produced by SimplLocals. The printed Clight is much more legible thanks to the more meaningful temporary variable names.
| * clightgen -dclight: print function parameters correctlyXavier Leroy2019-09-162-15/+34
| | | | | | | | | | | | | | | | | | | | | | | | | | The Clight output of clightgen is Clight version 2, after SimplLocals conversion, where function parameters are temporary variables, not variables. This commit makes sure the function parameters are printed as temporary variables and not as variables. In passing, it generalizes the Clight pretty-printer so that it can print both Clight version 1 and Clight version 2. Closes: #314
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-08-285-14/+17
|\| | | | | | | mppa-work-upstream-merge
| * bswap builtins: give semantics to them, support bswap64 on all targetsBernhard Schommer2019-08-121-1/+3
| | | | | | | | | | | | | | | | | | | | | | | | * Added semantic for byte swap builtins The `__builtin_bswap`, `__builtin_bswap16`, `__builtin_bswap32`, `__builtin_bswap64` builtin function are now standard builtin functions with a defined semantics. The semantics is given in terms of the decode/encode functions used for the memory model. * Added bswap64 expansion to PowerPC 32 bits. * Added bswap64 expansion for ARM.
| * Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-054-13/+14
| | | | | | | | | | "Hint Resolve foo." becomes "Hint Resolve foo : core", or "Local Hint Resolve foo : core".
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-07-196-65/+227
|\| | | | | | | mppa-work-upstream-merge
| * Make __builtin_sel available from C source codeXavier Leroy2019-07-175-31/+157
| | | | | | | | | | It is type-checked like a conditional expression then translated to a call to the known builtin function.
| * Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-171-9/+34
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit adds mechanisms to - recognize certain built-in and run-time functions by name and signature; - associate semantics to these functions, as a partial function from list of values to values; - interpret external calls to these functions according to this semantics (pure function from values to values, memory unchanged, no observable events in the trace); - external calls to unknown built-in and run-time functions remain interpreted as generating observable events and possibly changing memory, like before. The description of the built-ins is split into a target-independent part (in common/Builtins0.v) and a target-specific part (in $ARCH/Builtins1.v). Instruction selection uses the new mechanism in order to - recognize some built-in functions and turn them into operations of the target processor. Currently, this is done for __builtin_sel and __builtin_fabs; more to come. - remove the axioms about int64 helper functions from the standard library. More precisely, the behavior of these functions is still axiomatized, but now it is specified using the more general machinery introduced in this commit, rather than ad-hoc axioms in backend/SplitLongproof. The only built-ins currently described are __builtin_fsqrt (for all platforms) and __builtin_fmin / __builtin_fmax (for x86). More built-ins will be added later.
| * Remove the cparser/Builtins moduleXavier Leroy2019-07-171-7/+10
| | | | | | | | | | | | | | | | | | 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 the expected types for arguments to __builtin_annot, and extended asmXavier Leroy2019-06-191-5/+25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Currently, the arguments to __builtin_annot, __builtin_ais_annot, __builtin_debug, and extended asm statements are treated like arguments to an unprototyped or vararg function call. In particular, arguments of type "float" are converted to "double", generating useless code. To avoid this extra, useless conversion, this commit changes the types expected for the arguments to these built-ins and to extended asm statements. Now they are the types of the arguments themselves, after performing the usual unary conversions (e.g. char -> int), but without the problematic float -> double conversion. This ensures that no code is generated to change the representation of the arguments.
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-06-036-10/+9
|\| | | | | | | mppa-if-conversion
| * Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-312-2/+2
| | | | | | | | | | | | 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.
| * Csyntax.v: Fix a typo in a documentation comment (#292)Bart Jacobs2019-05-211-1/+1
| |
| * lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-232-2/+1
| | | | | | | | | | Instead, use definitions and lemmas from the Coq standard library (ZArith, Znumtheory).
| * Replace nat_of_Z with Z.to_natXavier Leroy2019-04-231-1/+1
| | | | | | | | | | | | | | Use Z.to_nat theorems from the standard Coq library in preference to our theorems in lib/Coqlib.v. Simplify lib/Coqlib.v accordingly.
| * Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-271-4/+4
| | | | | | | | | | | | | | | | | | | | | | | | Main changes to CompCert outside of Flocq are as follows: - Minimal supported version of Coq is now 8.7, due to Flocq requirements. - Most modifications are due to Z2R being dropped in favor of IZR and to the way Flocq now handles NaNs. - CompCert now correctly handles NaNs for the Risc-V architecture (hopefully).
* | ternary ops for float/doubleDavid Monniaux2019-04-031-0/+4
| |
* | problem in ValueAOpDavid Monniaux2019-04-031-0/+1
| |
* | attempts at generating builtins, startDavid Monniaux2019-04-031-1/+8
| |
* | la division flottante fonctionneDavid Monniaux2019-03-201-2/+16
| |
* | ça semble passerDavid Monniaux2019-03-201-2/+4
| |
* | added helper functions but strangeDavid Monniaux2019-03-191-1/+17
|/ | | | idiv.c: error: __compcert_i32_sdiv: missing or incorrect declaration
* 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.
generated by cgit (git 2.34.1) at 2024-05-20 08:23:14 +0000