diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-05-25 15:32:17 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-05-30 17:38:07 +0200 |
| commit | d357b5c52fb9ac70679fa8abd47094e89a6c3fa1 (patch) | |
| tree | afc9759833de393a36b6156a1ff0a7cc1db65bec /aarch64/Asm.v | |
| parent | 318fc06823eb577e9b386aeea57133e8c3938ecf (diff) | |
| download | compcert-d357b5c52fb9ac70679fa8abd47094e89a6c3fa1.tar.gz compcert-d357b5c52fb9ac70679fa8abd47094e89a6c3fa1.zip | |
AArch64: make register X29 callee-save
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.
Diffstat (limited to 'aarch64/Asm.v')
| -rw-r--r-- | aarch64/Asm.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/aarch64/Asm.v b/aarch64/Asm.v index b5f4c838..c5f4032e 100644 --- a/aarch64/Asm.v +++ b/aarch64/Asm.v @@ -1067,7 +1067,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out let sp := (Vptr stk Ptrofs.zero) in match Mem.storev Mint64 m1 (Val.offset_ptr sp pos) rs#SP with | None => Stuck - | Some m2 => Next (nextinstr (rs #X29 <- (rs#SP) #SP <- sp #X16 <- Vundef)) m2 + | Some m2 => Next (nextinstr (rs #X15 <- (rs#SP) #SP <- sp #X16 <- Vundef)) m2 end | Pfreeframe sz pos => match Mem.loadv Mint64 m (Val.offset_ptr rs#SP pos) with |