aboutsummaryrefslogtreecommitdiffstats
path: root/riscV
Commit message (Collapse)AuthorAgeFilesLines
* Change preference for new register in allocatorBernhard Schommer2023-03-061-0/+17
| | | | | | | | | | | | Currently, the register allocator picks caller-save registers in preference to callee-save registers. But for ARM in Thumb mode, more compact code is obtained if we prefer integer registers R0...R3 rather than all integer caller-save registers. This commit introduces an `allocatable_registers` function in $ARCH/Conventions1.v that determines the preferred and remaining registers to be used for register allocation.
* RISC-V: print flt.s, feq.s, fle.s with a tab after the mnemonic (#481)David Monniaux2023-02-071-3/+3
|
* Use .data.rel.ro section for const data with relocatable inits on ELF ↵Xavier Leroy2022-10-241-1/+4
| | | | | | | | | | | | | targets (#457) Follow-up to ed89275cb. AArch64, ARM, RISC-V and x86 ELF targets are changed. PowerPC / ELF is unchanged because we use the EABI variant, which has no `.data.rel.ro` section as far as I can see in GCC's output. (The SVR4 variant has `.data.rel.ro` but does not have `.sdata2`, which CompCert uses.) Fixes: #454
* Add `Declare Scope` where appropriate (#440)Xavier Leroy2022-09-191-0/+1
| | | | | | And re-enable the `undeclared-scope` warning. `Declare Scope` has been available since Coq 8.12, which is now the minimal Coq version supported.
* More simplifications for literal printingBernhard Schommer2022-09-031-5/+0
| | | | | | | Use the same code to split 64 bit literals into two 32 bit halfs as is used for 64 bit initialization data and print them in PrintAsm. This removes the need for a target specific printing function for 64 bit literals.
* Refactor emitting of constants.Bernhard Schommer2022-09-031-16/+2
| | | | | | The function was the same for nearly all backends and also the way 32 bit literals are printed so we moved it to PrintAsm. The 64 bit literals however are still target specific.
* Support mergeable sections for fixed-size literalsXavier Leroy2022-08-291-30/+21
| | | | | | | | | | | | On platforms that support them (ELF, macOS), use mergeable sections (like `.rodata.cst8`) for 4-, 8- and 16-byte wide literals. Works only if the LITERAL section is the default one. If the user provided their own LITERAL section, all literals are put in it regardless of their sizes. Support for mergeable string sections is introduced in this commit too but needs further changes in C2C.ml .
* Expand "j_s symb" to "jump symb, x31" assembly pseudo-instructionXavier Leroy2022-06-243-4/+3
| | | | | | | | | | As suggested by Léo Gourdin in #437. The previous expansion as a plain "j" instruction fails when the jump offset is too large to be represented (issue #436). Fixes: #436 Closes: #437
* Introduce float_conversion_default_nan parameter for float-float conversionsBernhard Schommer2022-04-251-1/+4
| | | | | | | | | | | | | For RISC-V we need to return the canonical NaN value if the argument of a float32->float64 or float64->float32 conversion is any NaN. This is in line with 11.3 from the RISC-V manual, the description of the conversion operations as well as what the spike ISA simulator and qemu do. Other platforms convert the NaN payload (by truncation or expansion) in float32->float64 and float64->float32 conversions. Fixes: #428
* Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-031-2/+2
| | | | This avoids a new warning of Coq 8.14.
* Fix wrong expansion of __builtin_memcpy_alignedXavier Leroy2021-09-231-2/+2
| | | | | | | | | In the "small" case, there was an error in the choice of temporary registers to use when one argument is a stack location and the other is a register. The chosen temporary could conflict with the argument that resides in a register. Fixes: #412
* Int.sign_ext_shr_shl: weaker hypothesisXavier Leroy2021-08-221-2/+2
| | | | | | Works also for sign_ext 32. ARM, RISC-V: adapt Asmgenproof1 accordingly
* Register X1 is destroyed by some built-in functionsXavier Leroy2021-05-132-3/+5
| | | | E.g. __builtin_bswap. Update Asm modeling of builtins accordingly.
* Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-084-16/+20
| | | | | | The GPL makes sense for whole applications, but the dual-licensed Coq and OCaml files are more like libraries to be combined with other code, so the LGPL is more appropriate.
* Support __builtin_unreachableXavier Leroy2021-05-021-0/+4
| | | | Not yet used for optimizations.
* Introduce and use PrintAsmaux.variable_sectionXavier Leroy2021-02-231-2/+2
| | | | | | | This is a generalization of the previous PrintAsmaux.common_section function that - handles initialized variables in addition to uninitialized variables; - can be used for Section_const, not just for Section_data.
* Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-211-1/+1
| | | | | | | This avoids a new warning of Coq 8.13. Eventually these `Global Hint` should become `#[export] Hint`, with a cleaner but different meaning than `Global Hint`.
* Support re-normalization of function parameters at function entryXavier Leroy2021-01-161-1/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | This is complementary to 28f235806 Some ABIs leave more flexibility concerning function parameters than CompCert expects. For instance, the AArch64/ELF ABI allow the caller of a function to leave unspecified the "padding bits" of function parameters. As an example, a parameter of type "unsigned char" may not have zeros in bits 8 to 63, but may have any bits there. When the caller is compiled by CompCert, it normalizes argument values to the parameter types before the call, so padding bits are always correct w.r.t. the type of the argument. This is no longer guaranteed in interoperability scenarios, when the caller is not compiled by CompCert. This commit adds a general mechanism to insert "re-normalization" conversions on the parameters of a function, at function entry. This is controlled by the platform-dependent function Convention1.return_value_needs_normalization. The semantic preservation proof is still conducted against the CompCert model, where the argument 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 pass arguments that are not normalized.
* RISC-V: fix FP calling conventionsXavier Leroy2021-01-144-117/+171
| | | | | | | | | | | | | | | | | | | | | | | This is a follow-up to e81d015e3. In the RISC-V ABI, FP arguments to functions are passed in integer registers (or pairs of integer registers) in two cases: 1- the FP argument is a variadic argument 2- the FP argument is a fixed argument but all 8 FP registers reserved for parameter passing have been used already. The previous implementation handled only case 1, with some problems. This commit implements both 1 and 2. To this end, 8 extra FP caller-save registers are used to hold the values of the FP arguments that must be passed in integer registers. Fixup code moves these FP registers to integer registers / register pairs. Symmetrically, at function entry, the integer registers / register pairs are moved back to the FP registers. 8 extra FP registers is enough because there are only 8 integer registers used for parameter passing, so at most 8 FP arguments may need to be moved to integer registers.
* RISC-V: wrong fixup code generated for vararg calls with fixed FP argsXavier Leroy2021-01-101-12/+18
| | | | | | | | | This is a follow-up to 2076a3bb3. Integer registers were wrongly reserved for fixed FP arguments, causing variadic FP arguments to end up in the wrong integer registers. Added regression test in test/regression/varargs2.c
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-299-76/+76
| | | | | | | | | | | Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
* RISC-V: revised calling conventions for variadic functionsXavier Leroy2020-12-252-63/+105
| | | | | Fixed (non-variadic) arguments follow the standard calling conventions. It's only the variadic arguments that need special treatment.
* Changed cc_varargs to an option typeBernhard Schommer2020-12-252-4/+5
| | | | | | Instead of being a simple boolean we now use an option type to record the number of fixed (non-vararg) arguments. Hence, `None` means not vararg, and `Some n` means `n` fixed arguments followed with varargs.
* Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-211-2/+1
| | | | configure flags -use-external-Flocq and -use external-MenhirLib.
* Add __builtin_sqrt as synonymous for __builtin_fsqrtXavier Leroy2020-07-271-1/+1
| | | | __builtin_sqrt (no "f") is the name used by GCC and Clang.
* RISC-V implementation of __builtin_clz* and __builtin_ctz*Xavier Leroy2020-07-272-0/+134
| | | | Using binary search loops expanded at point of use.
* No need to process __builtin_fabs in $ARCH/Asmexpand.mlXavier Leroy2020-07-271-2/+0
| | | | __builtin_fabs has already been expanded in backend/Selection.v .
* Move shared code in new file.Bernhard Schommer2020-06-282-18/+0
| | | | | The name_of_register and register_of_name function are shared between all architectures and can be moved in a common file.
* Remove the `can_reserve_register` function.Bernhard Schommer2020-06-282-3/+0
| | | | | The function is in fact just a call to the function`is_callee_save_register` from `Conventions1.v`.
* Use Hashtbl.find_opt.Bernhard Schommer2020-06-281-1/+1
| | | | | Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None` by a call to the function Hashtbl.find_opt.
* Update the RISC-V calling conventions, continued (#227)Xavier Leroy2020-03-021-7/+10
| | | | | | | | Double FP arguments passed on stack were incorrectly aligned: they must be 8-aligned but were 4-aligned only. This was due to the use of `Location.typealign`, which is the minimal hardware-supported alignment for a given type, namely 1 word for type Tfloat. To get the correct alignments, `Location.typesize` must be used instead.
* 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.
* Platform-independent implementation of Conventions.size_arguments (#222)Xavier Leroy2020-02-241-64/+0
| | | | | | | | | | | | | | 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.
* Cosmetic: in OCaml code, write "open! Module" instead of "open !Module"Xavier Leroy2020-02-211-1/+1
| | | | | | "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.
* Support re-normalization of values returned by function callsXavier Leroy2020-02-211-0/+6
| | | | | | | | | | | | | | | | | | | | | | | | | 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-212-12/+11
| | | | | | | | | | 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.
* 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.
* Revert "Remove `__builtin_nop` for some architectures. (#208)"Bernhard Schommer2020-01-033-1/+7
| | | | This reverts commit 4dfcd7d4be18e8bc437ca170782212aa06635a95.
* Remove `__builtin_nop` for some architectures. (#208)Bernhard Schommer2019-12-213-7/+1
| | | | | | | 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.
* Merge pull request #313 from AbsInt/aarch64Xavier Leroy2019-09-112-22/+6
|\ | | | | | | Support target architecture AArch64 (ARMv8 in 64-bit mode)
| * Fix compile for architectures other than AArch64 (#192)Bernhard Schommer2019-08-172-6/+6
| | | | | | Some changes were not correctly propagated to all architectures.
| * AArch64 portXavier Leroy2019-08-081-16/+0
| | | | | | | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
* | bswap builtins: give semantics to them, support bswap64 on all targetsBernhard Schommer2019-08-121-3/+0
|/ | | | | | | | | | | | * 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.
* Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-173-17/+56
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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-2/+2
| | | | | | | | | 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()`.
* Add floating-point square root and fused multiply-addXavier Leroy2019-07-171-0/+5
| | | | | | | | We just lift the corresponding functions from Flocq and add the computation of NaN payloads. NaN payloads for FMA are described in the ARM and RISC-V specifications, and were determined experimentally for x86 and for Power.
* Revised specification of NaN payload behaviorXavier Leroy2019-07-121-13/+15
| | | | | | | | | | | | | | When an FP arithmetic instruction produces a NaN result, the payload of this NaN depends on the architecture. Before, the payload behavior was specified by 3 architecture-dependent parameters: `Archi.choose_binop_pl_64` and `Archi.choose_binop_pl_32` and `Archi.fpu_results_default_qNaN`. This was adequate for two-argument operations, but doesn't extend to FMA. In preparation for FMA support, this commit generalizes the `Archi.choose` functions from two arguments to any number of arguments. In passing, `Archi.fpu_results_default_qNaN` is no longer needed.
* Extended asm: print register names according to their typesXavier Leroy2019-06-171-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When printing an extended asm code fragment, placeholders %n are replaced by register names. Currently we ignore the fact that some assemblers use different register names depending on the width of the data that resides in the register. For example, x86_64 uses %rax for a 64-bit quantity and %eax for a 32-bit quantity, but CompCert always prints %rax in extended asm statements. This is problematic if we want to use 32-bit integer instructions in extended asm, e.g. int x, y; asm("addl %1, %0", "=r"(x), "r"(y)); produces addl %rax, %rdx which is syntactically incorrect. Another example is ARM FP registers: D0 is a double-precision float, but S0 is a single-precision float. This commit partially solves this issue by taking into account the Cminor type of the asm parameter when printing the corresponding register. Continuing the previous example, int x, y; asm("addl %1, %0", "=r"(x), "r"(y)); now produces addl %eax, %edx This is not perfect yet: we use Cminor types, because this is all we have at hand, and not source C types, hence "char" and "short" parameters are still printed like "int" parameters, which is not good for x86. (I.e. we produce %eax where GCC might have produced %al or %ax.) We'll leave this issue open.
* Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-311-1/+1
| | | | | | 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.
* Provide a default "select" operation for the RiscV portXavier Leroy2019-05-202-0/+20
| | | | | No `Osel` operation for this port, so `SelectOp.select` always returns None.
generated by cgit (git 2.34.1) at 2024-05-18 07:35:38 +0000