aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64
Commit message (Collapse)AuthorAgeFilesLines
* 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-18/+4
| | | | | | 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-32/+25
| | | | | | | | | | | | 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 .
* AArch64: make register X29 callee-saveXavier Leroy2022-05-306-34/+34
| | | | | | | | | CompCert doesn't maintain a frame pointer in X29. However, it must treat X29 as callee-save, so that CompCert-generated code can be called from code that uses X29 as frame pointer. This commit makes X29 callee-save. In places where X29 was used as a temporary, X15 or X14 is used instead.
* 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
* For __builtin_memcpy_aligned, watch out for alignment of stack offsetsXavier Leroy2021-09-231-0/+1
| | | | | | | | | | Stack offsets must be multiple of 8 when using ldp/stp instructions and multiple of the transferred size when using other load/store instructions with offsets greater than 256. For simplicity, always require that the offset is multiple of 8. Fixes: #410
* 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.
* Section handling: finer control of variable initializationXavier Leroy2021-02-231-1/+1
| | | | | | | | | | | | | Distinguish between: - uninitialized variables, which can go in COMM if supported - variables initialized with fixed, numeric quantities, which can go in a readonly section if "const" - variables initialized with symbol addresses which may need relocation, which cannot go in a readonly section even if "const", but can go in a special "const_data" section. Also: on macOS, use ".const" instead of ".literal8" for literals, as not all literals have size 8.
* Introduce and use PrintAsmaux.variable_sectionXavier Leroy2021-02-231-4/+4
| | | | | | | 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-212-3/+3
| | | | | | | 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`.
* "macosx" is now called "macos"Xavier Leroy2021-01-183-3/+3
| | | | | The configure script still accepts "macosx" for backward compatibility, but every other part of CompCert now uses "macos".
* Support re-normalization of function parameters at function entryXavier Leroy2021-01-161-6/+10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-299-133/+133
| | | | | | | | | | | 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`.
* AArch64 / macOS: use __DATA,__CONST section instead of .const (temporary fix)Xavier Leroy2020-12-261-1/+1
| | | | | | | | The .const section cannot contain absolute references to symbols, as these may need relocation and therefore must be writable. This should be fixed more generally by distinguishing between initialization data that contains absolute references to symbols and initialization data that does not.
* AArch64: macOS portXavier Leroy2020-12-2612-215/+484
| | | | | This commit adds support for macOS (and probably iOS) running on AArch64 / ARM 64-bit / "Apple silicon" processors.
* AArch64: clarify the printing of extending-register arithmetic operationsXavier Leroy2020-12-261-13/+13
| | | | | The extended register is now printed as an X register if the extension mode is UXTX, and as a W register otherwise.
* AArch64: wrong function alignmentXavier Leroy2020-12-261-1/+1
| | | | | The alignment was 2 bytes (like for ARM) but should be 4 bytes. It was ignored by the GNU assembler, but the LLVM assembler warns.
* AArch64 modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-8/+11
| | | | | | Pfmovimms, Pfmovimmd destroy X16 Pbtbl preserves X17 Inlined built-in functions destroy X16 and X30
* Added implementation for fmin/fmax for aarch64.Bernhard Schommer2020-11-063-0/+12
| | | | | The two built-in function map to the fmax and fmin instruction. Bug 30035
* 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.
* Move declarations of __builtin_clz* and __builtin_ctz* to C2C.mlXavier Leroy2020-07-271-8/+0
| | | | These functions are now available on all targets.
* AArch64 implementation of __builtin_ctz*Xavier Leroy2020-07-273-1/+11
| | | | Using the "rbit" instruction (reverse bits).
* 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-281-17/+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-281-2/+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.
* Dual-license aarch64/{Archi.v,Cbuiltins.ml,extractionMachdep.v}Xavier Leroy2020-05-053-0/+9
| | | | | | The corresponding files in all other ports are dual-licensed (GPL + non-commercial), there is no reason it should be different for aarch64.
* Platform-independent implementation of Conventions.size_arguments (#222)Xavier Leroy2020-02-241-107/+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.
* 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.
* Support re-normalization of values returned by function callsXavier Leroy2020-02-211-0/+5
| | | | | | | | | | | | | | | | | | | | | | | | | 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-10/+9
| | | | | | | | | | 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.
* Revert "Remove `__builtin_nop` for some architectures. (#208)"Bernhard Schommer2020-01-033-1/+8
| | | | This reverts commit 4dfcd7d4be18e8bc437ca170782212aa06635a95.
* Remove `__builtin_nop` for some architectures. (#208)Bernhard Schommer2019-12-213-8/+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.
* The SP register has dwarf register number 31.Bernhard Schommer2019-12-111-1/+1
|
* Fix for AArch64 alignment problem (#206)Bernhard Schommer2019-11-283-2/+8
| | | | | | | | | 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
|
* 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.
* 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}.
* Offset out of range for ldp/stp instructionsxavier.leroy2019-08-231-1/+3
| | | | These instructions are generated by __builtin_memcpy.
* AArch64 portXavier Leroy2019-08-0827-0/+14370
This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
generated by cgit (git 2.34.1) at 2024-06-02 18:27:05 +0000