Add an ARMv8-A (AArch64) backend

compiler/Makefile

@@ -10,11 +10,14 @@ CHECKCATS ?= \
 	x86-64-Intel \
 	x86-64-nolea \
 	arm-m4 \
+	armv8a \
 	risc-v \
 	x86-64-stack-zero-loop \
 	x86-64-stack-zero-unrolled \
 	arm-m4-stack-zero-loop \
 	arm-m4-stack-zero-unrolled \
+	armv8a-stack-zero-loop \
+	armv8a-stack-zero-unrolled \
 	risc-v-stack-zero-loop \
 	risc-v-stack-zero-unrolled \
 	CCT CCT-DOIT SCT
@@ -33,7 +36,7 @@ DISTDIR ?= jasmin-compiler
 OBELISK ?= obelisk
 
 # --------------------------------------------------------------------
-.PHONY: all CIL check check-ci
+.PHONY: all CIL check check-ci check-armv8a-semantics
 .PHONY: clean install uninstall dist
 
 all:
@@ -56,6 +59,12 @@ check-ec:
 	$(MAKE) -C examples/gimli/proofs
 	$(MAKE) -C examples/extraction-unit-tests
 
+# Differential test of the ARMv8-A instruction semantics (the Coq model of
+# armv8a_instr_decl.v, evaluated through its OCaml extraction) against real
+# hardware execution. Requires an AArch64 (ARMv8-A) host.
+check-armv8a-semantics:
+	$(MAKE) -C tests/armv8a-hw-semantics check
+
 check-all: check
 	dune runtest -f
 

compiler/config/tests.config

@@ -54,6 +54,11 @@ bin = ./scripts/check
 args = -arch riscv
 okdirs = examples/**/risc-v tests/success/**/risc-v tests/success/**/common
 
+[test-armv8a]
+bin = ./scripts/check
+args = -arch armv8a
+okdirs = tests/success/**/armv8a
+
 [test-risc-v-extraction]
 bin = ./scripts/extract-and-check
 args = riscv
@@ -80,6 +85,16 @@ bin     = ./scripts/check
 args    = -arch arm-m4 -stack-zero=unrolled
 okdirs  = tests/success/stack_zeroization/**/arm-m4
 
+[test-armv8a-stack-zero-loop]
+bin     = ./scripts/check
+args    = -arch armv8a -stack-zero=loop
+okdirs  = tests/success/stack_zeroization/**/armv8a
+
+[test-armv8a-stack-zero-unrolled]
+bin     = ./scripts/check
+args    = -arch armv8a -stack-zero=unrolled
+okdirs  = tests/success/stack_zeroization/**/armv8a
+
 [test-risc-v-stack-zero-loop]
 bin     = ./scripts/check
 args    = -arch riscv -stack-zero=loop

compiler/doc/armv8a_register_model.md

@@ -0,0 +1,144 @@
+# ARMv8-A (AArch64) register model and stack-pointer handling — rationale and sources
+
+This note documents the modeling decisions in the Jasmin AArch64 backend that
+concern the **architecture declaration** (`proofs/compiler/armv8a_decl.v`) and
+the **stack-pointer handling** in the linearization parameters
+(`proofs/compiler/armv8a_params.v`). Each decision departs from a naive "one
+Coq constructor per hardware register" model for a documented architectural or
+ABI reason; the citations below let a reviewer check every claim.
+
+Primary sources:
+
+- **Arm ARM** — *Arm Architecture Reference Manual, A-profile*, Arm DDI 0487M.a
+  (`DDI0487_M.a.a_a-profile_architecture_reference_manual.pdf`,
+  sha256 `c07b1302a3db0c6bc0490808c771d66684ddd5adfb2ef64fd23e6beeb7b22e48`; the
+  same edition and hash recorded in `armv8a_isa_docs.json`). Page ids below are
+  the manual's own `Sn-NNNN` labels.
+- **AAPCS64** — *Procedure Call Standard for the Arm 64-bit Architecture
+  (AArch64)*, Arm IHI 0055F.
+- **Apple** — *Writing ARM64 Code for Apple Platforms*, Apple Developer
+  documentation.
+
+---
+
+## 1. The general-purpose register set
+
+AArch64 has 31 general-purpose registers `R0..R30`, each addressable as a 64-bit
+`X` register or a 32-bit `W` register, plus a dedicated stack pointer `SP`.
+`R30` is the procedure-call link register.
+
+> Arm ARM, **B1.2 "Registers in AArch64 Execution state"**, p. B1-203:
+> "31 general-purpose registers, R0 to R30 ... The X30 general-purpose register
+> is used as the procedure call link register. SP — A 64-bit dedicated Stack
+> Pointer register."
+
+The model keeps `R0..R30` and `RSP`. Two registers that a hardware-faithful
+model might include are deliberately omitted (§2, §3).
+
+## 2. The zero register (XZR/WZR) is not modeled
+
+In an instruction encoding the 5-bit register field value `31` (`0b11111`) does
+**not** name a physical register; its meaning depends on which register accessor
+the instruction uses:
+
+> Arm ARM, **B1.2**, p. B1-206:
+> "For the general-purpose register X[] accessor, register number 31 accesses
+> the zero register, ZR, which reads as zero and ignores writes."
+
+The stack pointer is reached through a **separate `SP[]` accessor**, so the same
+field value `31` means `SP` only for the instructions that select it (ADD/SUB in
+their SP forms, MOV-to/from-SP, and loads/stores that allow `SP` as base).
+
+Consequences for the model:
+
+- Modeling `ZR` as an allocatable register would be **unsound**: a value written
+  to it is discarded and any read returns 0. The register allocator, treating it
+  as ordinary storage, produced code such as `mov sp, xzr` (setting SP to 0).
+- We therefore omit it entirely, exactly as the Jasmin RISC-V backend omits the
+  hardwired `x0`/`zero`. The handful of operations that genuinely need `ZR` as an
+  operand — `CMP` (`SUBS` to `ZR`), `NEG`, `TST`, etc. — are emitted as dedicated
+  assembler mnemonics by the printer, never as writes to a `ZR` register.
+- `RSP` is the single encoding-31 register we keep, and it always denotes `SP`.
+
+## 3. The platform register (x18) is not modeled
+
+`x18` is not an architectural special register; it is reserved by the software
+ABI:
+
+> AAPCS64 (IHI 0055F), *General-purpose registers*: r18 is
+> "The Platform Register, if needed; otherwise a temporary register", and a
+> platform ABI may reserve it.
+>
+> Apple, *Writing ARM64 Code for Apple Platforms*:
+> "The platforms reserve register x18. Don't use this register."
+
+On Apple platforms, under Windows, and under shadow-call-stack Linux, the OS or
+runtime may overwrite `x18` **asynchronously** (i.e. between two instructions of
+otherwise straight-line user code). Jasmin's register allocator chooses the
+register that holds a function's saved stack pointer by proving the program does
+not clobber it (`get_reg_oracle` in `compiler/src/regalloc.ml`); that analysis
+cannot see writes performed outside the program, so it happily picked `x18` and
+the saved SP was corrupted to 0 at run time.
+
+Keeping `x18` out of the allocation pool is the only safe choice across these
+platforms. On a platform where `x18` is a plain temporary this merely forgoes
+one scratch register; correctness is unaffected.
+
+## 4. The stack pointer must stay 16-byte aligned
+
+Whenever `SP` is used as the base of a memory access it must be 16-byte aligned.
+This is an **architectural** check (an exception), not just an ABI convention:
+
+> Arm ARM, **D1.4.10.2 "SP alignment checking"**, p. D1-7135:
+> - rule **RRDMXG**: "When the SP is used as the base address of a calculation,
+>   regardless of any offset applied by the instruction, if bits [3:0] of the SP
+>   are not 0b0000, there is a misaligned SP."
+> - rule **RTFVSM**: "If SP alignment checking is enabled, then the execution of
+>   a load or store using the SP with a misaligned SP generates a synchronous SP
+>   Alignment exception on that load or store."
+> - rule **RSTDYJ**: the check is enabled by `SCTLR_EL1.SA` (EL1),
+>   `SCTLR_EL1.SA0`/`SCTLR_EL2.SA0` (EL0), etc.
+
+The check is enabled for EL0 on the platforms we target. The 16-byte alignment
+of `SP` at public interfaces is also mandated by the AAPCS64 (IHI 0055F, *The
+stack*: "SP mod 16 = 0"), which B1.2 (p. B1-203) cross-references.
+
+Jasmin sizes each stack frame to the alignment of the objects it holds
+(`sao_align`), which for pure 64-bit code is only 8 bytes, so a raw frame size
+need not be a multiple of 16. The backend therefore:
+
+- rounds every frame allocation/deallocation up to a multiple of 16
+  (`round_up_16`, used by `armv8a_allocate_stack_frame` /
+  `armv8a_free_stack_frame`), so nested calls preserve the invariant; and
+- never aligns a re-aligned frame to less than 16 bytes
+  (`armv8a_set_up_sp_register`).
+
+The extra padding lands at the top of the frame and is never accessed.
+
+## 5. The stack pointer cannot be an LDR destination
+
+Because a load writes its result through the general-purpose `X[]` accessor, and
+register number 31 in that accessor is `ZR` (§2), an A64 `LDR` can never write
+`SP`: its destination operand is `<Xt>`, not `<Xt|SP>`. (This differs from
+ARMv7, where R13/SP is an ordinary register that `LDR` can target — which is why
+the shared linearization default, `lloads_imm_dfl`, is fine for the 32-bit Arm
+backend but not here.)
+
+When the saved stack pointer has been spilled to the stack (the usual case for a
+function that saves callee-saved registers), it must therefore be reloaded into
+a scratch register and then copied to `SP` with a `MOV` (which reaches `SP` via
+the `SP[]` accessor). This is what the backend's custom `armv8a_lloads` does: it
+restores the ordinary saved registers first (relative to the still-live `SP`),
+then loads the saved `SP` into `X17` and issues `MOV SP, X17`.
+
+---
+
+### Cross-reference to the code
+
+| Decision | File / definition | Source |
+|---|---|---|
+| Omit `XZR` | `armv8a_decl.v` — `register`, `registers`, `register_to_string` | Arm ARM B1.2, p. B1-206 |
+| Omit `x18` | `armv8a_decl.v` — `register`, `registers`, `armv8a_internal_call_conv` | AAPCS64 IHI 0055F; Apple ABI |
+| Round frames to 16 | `armv8a_params.v` — `round_up_16`, `armv8a_allocate_stack_frame`, `armv8a_free_stack_frame` | Arm ARM D1.4.10.2 (RRDMXG, RTFVSM) |
+| Re-align frames ≥ 16 | `armv8a_params.v` — `armv8a_set_up_sp_register` | Arm ARM D1.4.10.2; AAPCS64 |
+| Restore `SP` via scratch + `MOV` | `armv8a_params.v` — `armv8a_lloads` | Arm ARM B1.2, p. B1-206 |

compiler/entry/commonCLI.ml

@@ -5,7 +5,8 @@ open Utils
 let arch =
   let alts =
     [
-      ("x86-64", Utils.X86_64); ("arm-m4", Utils.ARM_M4); ("riscv", Utils.RISCV);
+      ("x86-64", Utils.X86_64); ("arm-m4", Utils.ARM_M4);
+      ("armv8a", Utils.ARMv8A); ("riscv", Utils.RISCV);
     ]
   in
   let doc =

compiler/safetylib/arm_safety.ml

@@ -7,16 +7,16 @@ module Arm_safety
       with type reg = Arm_decl.register
        and type regx = Arch_utils.empty
        and type xreg = Arch_utils.empty
-       and type rflag = Arm_decl.rflag
-       and type cond = Arm_decl.condt
+       and type rflag = Arm_common.rflag
+       and type cond = Arm_common.condt
        and type asm_op = Arm_instr_decl.arm_op
        and type extra_op = Arm_extra.arm_extra_op)
   : SafetyArch
     with type reg = Arm_decl.register
      and type regx = Arch_utils.empty
      and type xreg = Arch_utils.empty
-     and type rflag = Arm_decl.rflag
-     and type cond = Arm_decl.condt
+     and type rflag = Arm_common.rflag
+     and type cond = Arm_common.condt
      and type asm_op = Arm_instr_decl.arm_op
      and type extra_op = Arm_extra.arm_extra_op
   = struct

compiler/safetylib/safetyMain.ml

@@ -60,3 +60,12 @@ let get_arch_with_analyze arch call_conv : (module ArchWithAnalyze) =
 
         let analyze = Safety.analyze
       end)
+  | ARMv8A ->
+      (module struct
+        module C = CoreArchFactory.Core_arch_ARMV8A
+        module A = Arch_full.Arch_from_Core_arch (C)
+
+        let analyze ?fmt:_ ~safety_param:_ _ _ =
+          hierror ~loc:Lnone ~kind:"safety analysis"
+            "the safety checker is not implemented for ARMv8-A"
+      end)

compiler/scripts/check

@@ -32,6 +32,9 @@ elif [ $ARCH = "riscv" ]
 then
      # +m enables integer multiplication
      ASARGS="--triple=riscv32 --mcpu=generic-rv32 -mattr=+m"
+elif [ $ARCH = "armv8a" ]
+then
+    ASARGS="--triple=aarch64"
 else
     ASARGS="--triple=x86_64"
 fi

compiler/src/arch_full.ml

@@ -35,6 +35,19 @@ module type Core_arch = sig
 
   val callstyle : reg callstyle
 
+  (* Minimal alignment of every stack frame. Frame sizes are rounded up to
+     the frame's alignment (see [stack_frame_allocation_size]), so this
+     bounds the alignment the stack pointer keeps across calls. AArch64
+     requires 16 bytes (SP alignment checking, Arm ARM DDI0487M.a,
+     D1.4.10.2); other architectures have no requirement beyond the one of
+     the stack slots themselves. *)
+  val sp_min_align : Wsize.wsize
+
+  (* Widest store the architecture can perform in one instruction. Used to
+     cap the default stack-zeroization clear step when [sp_min_align]
+     raises the frame alignment beyond it. *)
+  val max_store_size : Wsize.wsize
+
   val known_implicits : (Name.t * string) list
 
   val is_ct_asm_op : asm_op -> bool

compiler/src/arch_full.mli

@@ -37,6 +37,13 @@ module type Core_arch = sig
 
   val callstyle : reg callstyle
 
+  (* Minimal alignment of every stack frame; see arch_full.ml. *)
+  val sp_min_align : Wsize.wsize
+
+  (* Widest store the architecture can perform in one instruction; see
+     arch_full.ml. *)
+  val max_store_size : Wsize.wsize
+
   val known_implicits : (Name.t * string) list
 
   val is_ct_asm_op : asm_op -> bool

compiler/src/arm_arch_full.ml

@@ -1,4 +1,5 @@
 open Arch_decl
+open Arm_common
 open Arm_decl
 
 
@@ -56,5 +57,9 @@ module Arm (Lowering_params : Arm_input) : Arch_full.Core_arch
 
   let callstyle = Arch_full.ByReg { call = Some LR; return = false }
 
+  let sp_min_align = Wsize.U8
+
+  let max_store_size = Wsize.U32
+
   let internal_call_conv = Arm_decl.arm_internal_call_conv
 end

compiler/src/armv8a_arch_full.ml

@@ -0,0 +1,63 @@
+(* ARMv8A architecture full integration *)
+open Arch_decl
+
+module type Armv8a_input = sig
+  val call_conv : (Armv8a_decl.register, Arch_utils.empty, Arch_utils.empty, Arm_common.rflag, Arm_common.condt) calling_convention
+end
+
+(* Create arch_toIdent for ARMv8A *)
+let atoI armv8a_decl =
+  let open Prog in
+  let mk_var k t s =
+    V.mk s (Reg(k,Direct)) (Conv.ty_of_cty (Type.atype_of_ltype t)) L._dummy [] in
+  match Arch_extra.MkAToIdent.mk armv8a_decl mk_var with
+  | Utils0.Error e ->
+      let e = Conv.error_of_cerror (Printer.pp_err ~debug:true) e in
+      raise (Utils.HiError e)
+  | Utils0.Ok atoI -> atoI
+
+module Armv8a (Lowering_params : Armv8a_input) = struct
+  module AD = Armv8a_decl
+
+  type reg = AD.register
+  type regx = Arch_utils.empty
+  type xreg = Arch_utils.empty
+  type nonrec rflag = Arm_common.rflag
+  type cond = Arm_common.condt
+  type asm_op = Armv8a_instr_decl.armv8a_asm_op
+  type extra_op = Armv8a_extra.armv8a_extra_op
+
+  let atoI = atoI AD.armv8a_decl
+
+  let asm_e = Armv8a_extra.armv8a_extra atoI
+
+  let aparams = Armv8a_params.armv8a_params atoI
+
+  let known_implicits = ["NF", "_nf_"; "ZF", "_zf_"; "CF", "_cf_"; "VF", "_vf_"]
+
+  let alloc_stack_need_extra _ = false
+
+  let is_ct_asm_op (o : asm_op) =
+    match o with
+    | Armv8a_instr_decl.ARMv8A_op ((Armv8a_instr_decl.SDIV | Armv8a_instr_decl.UDIV), _) -> false
+    | _ -> true
+
+  let is_ct_asm_extra (_o : extra_op) = true
+
+  let not_saved_stack = []
+
+  let pp_asm = Pp_arm_v8a.print_prog
+
+  let callstyle = Arch_full.ByReg { call = Some Armv8a_decl.R30; return = true }
+
+  (* SP must stay 16-byte aligned: SP alignment checking, Arm ARM
+     DDI0487M.a, D1.4.10.2 (see also the AAPCS64 stack constraints). *)
+  let sp_min_align = Wsize.U128
+
+  (* One X-register store; SIMD (NEON) stores would raise this to u128. *)
+  let max_store_size = Wsize.U64
+
+  let internal_call_conv = Armv8a_decl.armv8a_internal_call_conv
+
+  include Lowering_params
+end

compiler/src/compile.ml

@@ -360,7 +360,14 @@ let compile (type reg regx xreg rflag cond asm_op extra_op)
   in
 
   let szs_of_fn fn =
-    (get_annot fn).stack_zero_strategy
+    match (get_annot fn).stack_zero_strategy with
+    | Some (szs, None) when wsize_lt Arch.max_store_size Arch.sp_min_align ->
+        (* The default clear step is the frame alignment, which
+           [sp_min_align] may raise beyond the widest store the
+           architecture can perform in one instruction (u128 vs u64 on
+           armv8a): cap the default at that width. *)
+        Some (szs, Some Arch.max_store_size)
+    | szs -> szs
   in
 
   (* This implements an analysis returning the set of variables becoming dead