aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Update the RISC-V calling conventions (#221)Xavier Leroy2020-02-262-137/+149
| | | | | | | | | | | | We were implementing the ABI described in the RISC-V Instruction Set Manual, version 2.1. However, this ABI was superseded by the RISC-V ELF psABI specification. This commit changes the calling conventions to better match the ELF psABI specification. This should greatly improve interoperability with code compiled by other RISC-V compilers. One incompatibility remains: when all 8 FP argument registers have been used, further FP arguments should be passed in integer argument registers if available, while this PR passes them on stack.
* The type of a wide char constant is wchar_t. (#223)Bernhard Schommer2020-02-241-1/+2
| | | | See ISO C2011 standard, section 6.4.4.4 para 11.
* Platform-independent implementation of Conventions.size_arguments (#222)Xavier Leroy2020-02-247-649/+68
| | | | | | | | | | | | | | The "size_arguments" function and its properties can be systematically derived from the "loc_arguments" function and its properties. Before, the RISC-V port used this derivation, and all other ports used hand-written "size_arguments" functions and proofs. This commit moves the definition of "size_arguments" to the platform-independent file backend/Conventions.v, using the systematic derivation, and removes the platform-specific definitions. This reduces code and proof size, and makes it easier to change the calling conventions.
* AArch64: normalize function return values of small integer typeXavier Leroy2020-02-211-3/+11
| | | | | | | According to AAPCS64 (the AArch64 ABI specification), the top bits of the register containing the function result have unspecified value, so we need to sign- or zero-extend the function result before using it, as in the x86 port.
* Cosmetic: in OCaml code, write "open! Module" instead of "open !Module"Xavier Leroy2020-02-215-6/+6
| | | | | | "open!" is the form used in the examples in the OCaml manual. Based on a quick poll it seems to be the preferred form of the OCaml core dev team.
* Add interoperability test for functions returning small integer typesXavier Leroy2020-02-212-0/+23
|
* Support re-normalization of values returned by function callsXavier Leroy2020-02-217-33/+174
| | | | | | | | | | | | | | | | | | | | | | | | | 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-2143-286/+445
| | | | | | | | | | 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.
* Support vertical tabs and treat them as whitespace (#218)Bernhard Schommer2020-02-181-1/+1
| | | | Some preprocessors don't remove the vertical tab from the input so we should be able to handle them in the lexer.
* 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.
* Added base address if needed.Bernhard Schommer2020-02-063-33/+53
| | | | | | | | Ranges of locations are relative to some base address. Most times this is just the same as the compilation unit. However if the compilation unit contains functions in multiple sections we need to add a base address of the section that the locations are contained.
* Compatibility with OCaml 4.10 (#214)Xavier Leroy2020-02-063-7/+7
| | | | | | | | debug/DwarfPrinter.mli: unused functor parameter trigger warning 69, replace by non-dependent functor type. Makefile.extr: turn warning 69 (unused functor parameter) off for extracted code configure: accept OCaml versions above 4.09 configure: update messages for unsupported versions of OCaml and Coq
* Revised menhirLib autoconfiguration (#331)Xavier Leroy2020-02-053-5/+9
| | | | | | | | | | | | | | | | | Since Menhir version 20200123, we need to link with menhirLib.cmxa instead of menhirLib.cmx. This commit chooses automatically the file to link with: menhirLib.cmxa if it exists in the menhirLib installation directory, menhirLib.cmx otherwise. To reliably find the installation directory, configure was changed to record the menhirLib directory in Makefile.config, variable MENHIR_DIR, instead of a pre-cooked command-line option MENHIR_INCLUDES. Makefile.extr was adapted accordingly. Fixes: #329 Closes: #330
* Support Coq 8.11.0 (#212)Xavier Leroy2020-02-054-2/+8
| | | | Update configure. Ignore and clean up .vok and .vos files, which Coq 8.11.0 generates.
* Incorrect computation of extra stack size for vararg calls in RISC-V (#213)Bernhard Schommer2020-02-051-2/+2
| | | | | Currently, the extra size for the variable arguments is too small for the 64 bit RISC-V and the extra arguments are stored in the wrong stack slots.
* Reduce the checking time for the "decidable_equality_from" tacticxavier.leroy2020-01-301-4/+5
| | | | Just moved a frequent failure case ahead of a costly "simpl".
* Remove __builtin_nop from list of x86 builtins.Bernhard Schommer2020-01-031-3/+0
|
* Revert "Remove `__builtin_nop` for some architectures. (#208)"Bernhard Schommer2020-01-0314-3/+33
| | | | This reverts commit 4dfcd7d4be18e8bc437ca170782212aa06635a95.
* Added error for unknown builtin functions. (#208)Bernhard Schommer2019-12-211-1/+6
| | | | | | | | | Previously, using an unknown builtin function was treated like any other call to an undeclared function: a warning was emitted, and an error occurred at link-time. With this commit, using an unknown builtin function is an error, like in Clang.
* Remove `__builtin_nop` for some architectures. (#208)Bernhard Schommer2019-12-2114-33/+3
| | | | | | | The `__builtin_nop` function is documented only for PowerPC. It was added to the other architectures by copy paste, but has no known uses. So, remove `__builtin_nop` from all architectures but PowerPC.
* The SP register has dwarf register number 31.Bernhard Schommer2019-12-111-1/+1
|
* Allow Coq 8.10.2.Bernhard Schommer2019-12-031-1/+1
|
* Fix for AArch64 alignment problem (#206)Bernhard Schommer2019-11-284-2/+13
| | | | | | | | | 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.
* Added dwarf register numbers for aarch64Bernhard Schommer2019-11-281-3/+18
|
* Added back unused_ais_parameter warning.Bernhard Schommer2019-11-261-0/+1
|
* Simplified diagnostics module.Bernhard Schommer2019-11-251-118/+41
| | | | | | | Instead of constructing four different lists for maintaining the state of the warnings only one list is now used. This list contains the name of the warning and a boolean indicating whether this option should be active by default. The rest is computed from this list.
* Remove no longer needed file PrintLTLinBernhard Schommer2019-11-121-115/+0
|
* Use `intuition idtac` instead of `intuition` (#321)Vincent Laporte2019-11-121-1/+1
| | | | A stronger `intuition` in the near future would break this use of `intuition`.
* Raise minimal required versions for OCaml and Coq (#203)Bernhard Schommer2019-10-311-9/+4
| | | At least OCaml 4.05 is now required as well as Coq 8.8.
* More robust proof of `size_and` (#320)Frédéric Besson2019-10-301-4/+5
| | | | The proposed proof only uses `zify` for closing the goal. This is needed for Coq PR #10982 which changes the inner working of `zify`.
* Add support for Coq 8.10.1Xavier Leroy2019-10-281-2/+2
|
* clightgen: sanitize names of functions and global variablesXavier Leroy2019-10-282-4/+16
| | | | | A "dollar" sign in a function name or a global variable name was producing incorrect Coq identifiers. (Issue #319.)
* Fix configure for coq 8.10.0Michael Schmidt2019-10-131-2/+2
|
* Make explicit the use of hints from OrderedType (#316)Vincent Laporte2019-10-024-15/+17
| | | | | | | Some hints will move from the core database to the `ordered_type` database (see https://github.com/coq/coq/pull/9772). This commit prepares for this move by adding `with ordered_type` to the invocations of `auto` and `eauto` that use the hints in question.
* Remove duplicated ticks.Bernhard Schommer2019-10-011-2/+2
|
* Use pointer type for evaluated constants.Bernhard Schommer2019-10-011-1/+1
|
* Various improvements for diagnostics.Bernhard Schommer2019-09-303-10/+34
| | | | | | | | | | | | | | | | | | | | | | | | * Extend check for incomplete type. Extended the check to also include a check for variables with incomplete object type that are not arrays, that have an initializer. Furthermore the warning includes the type and variable name. * Warning for incomplete type in compound literals. Incomplete types are not allowed for compound literals, except for array types. * Extend type printing function. The type of a typedeof of an anonymous type should not be printed. Furthermore added '<anonymous>' to the printing of anonymous types. * Unify incomplete type errors message. The incomplete type error messages should all look the same including name of the variable, parameter, etc. and then the incomplete type.
* Added .gitattributes file.Bernhard Schommer2019-09-301-0/+3
| | | | Treat doc as documentation and tests as vendored for github linguist
* Functions that are extern should stay extern (#201)Bernhard Schommer2019-09-251-1/+1
| | | | | | In ISO C, inline functions behaves differently whether they have been declared `extern` at least once or not (i.e. all the declarations have no `extern` and no `static` modifier). Hence, functions that have been declared / defined `extern` once should remain `extern` when redeclared without `extern`. This gives the ISO C behavior for inline functions and has no impact for non-inline functions.
* Model GPR0 in isel (#199)Xavier Leroy2019-09-172-2/+4
| | | | | | | | If the first argument to `isel` is GPR0, it reads as the constant 0. This cannot occur in code generated by CompCert, due to the fact that GPR0 is not available as register for register allocation. However the assembler semantics should be as close as possible to the actual hardware.
* Update for release 3.6v3.6Xavier Leroy2019-09-171-2/+3
|
* Revise the "bench" entries of the test suiteXavier Leroy2019-09-175-12/+110
| | | | | | | | Initially, the "bench" entries of the test suite used a "xtime" utility developed in-house and not publically available. This commit adds a version of "xtime" written in OCaml (tools/xtime.ml) and updates the "bench" entries of the test/*/Makefile to use it.
* Updates in preparation for release 3.6Xavier Leroy2019-09-162-1/+63
|
* -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-163-16/+35
| | | | | | | | | | | | | 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
* Reworked json export.Bernhard Schommer2019-09-125-78/+91
| | | | | | | | | | | | | | The json export prints formatted json, which takes a lot of additional time, however the result is only consumed by other tools and not meant for human reading. This commit implements several small changes in order to speedup the json export: * Removal of usage of the Format Module * Replacing `fprintf` calls by calls to function that print directly, such as `output_string`, etc. * Replacing list of all instruction names by a set of all instructions
* Asmgenproof1: useless unfolding in proof scripts causing "omega" to failXavier Leroy2019-09-111-3/+3
| | | | "omega" fails in Coq 8.7, but not in 8.8 and later.
* Merge pull request #313 from AbsInt/aarch64Xavier Leroy2019-09-1163-167/+15898
|\ | | | | | | Support target architecture AArch64 (ARMv8 in 64-bit mode)
| * AArch64: wrong expected type for arguments of Cmaskl{zero,notzero}aarch64xavier.leroy2019-08-312-4/+4
| | | | | | | | | | | | | | | | The argument is of type Tlong, not Tint. This caused spurious errors in RTLtyping. Also: in AArch64/PrintOp.ml, print Cmaskl{zero,notzero} with "&l" to distinguish them from Cmask{zero,notzero}.
generated by cgit (git 2.34.1) at 2024-07-02 22:59:04 +0000