aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64
Commit message (Collapse)AuthorAgeFilesLines
* 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.