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/Machregs.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/Machregs.v')
| -rw-r--r-- | aarch64/Machregs.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/aarch64/Machregs.v b/aarch64/Machregs.v index 704c392e..f9b9fd79 100644 --- a/aarch64/Machregs.v +++ b/aarch64/Machregs.v @@ -156,18 +156,18 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg := Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with - | EF_memcpy sz al => R15 :: R17 :: R29 :: nil + | EF_memcpy sz al => R14 :: R15 :: R17 :: nil | EF_inline_asm txt sg clob => destroyed_by_clobber clob | _ => nil end. Definition destroyed_by_setstack (ty: typ): list mreg := nil. -Definition destroyed_at_function_entry: list mreg := R29 :: nil. +Definition destroyed_at_function_entry: list mreg := R15 :: nil. Definition destroyed_at_indirect_call: list mreg := nil. -Definition temp_for_parent_frame: mreg := R29. +Definition temp_for_parent_frame: mreg := R15. Definition mregs_for_operation (op: operation): list (option mreg) * option mreg := (nil, None). |