diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-08 13:55:00 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-08 13:55:00 +0100 |
| commit | dc1e8157540655cd303df5c36e41c50a3dcc678e (patch) | |
| tree | aa66e7c08777be9edad92fbd23c0e83ccb52a97b /aarch64/Asmgen.v | |
| parent | 8350d5ab1823db94d04dd4e1aaa4b4b64c27371d (diff) | |
| download | compcert-kvx-dc1e8157540655cd303df5c36e41c50a3dcc678e.tar.gz compcert-kvx-dc1e8157540655cd303df5c36e41c50a3dcc678e.zip | |
fix new register erasing scheme for AArch64
Diffstat (limited to 'aarch64/Asmgen.v')
| -rw-r--r-- | aarch64/Asmgen.v | 13 |
1 files changed, 4 insertions, 9 deletions
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index 024c9a17..683530d4 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -969,8 +969,8 @@ Definition transl_addressing (sz: Z) (addr: Op.addressing) (args: list mreg) (** Translation of loads and stores *) Definition transl_load (trap: trapping_mode) - (chunk: memory_chunk) (addr: Op.addressing) - (args: list mreg) (dst: mreg) (k: code) : res code := + (chunk: memory_chunk) (addr: Op.addressing) + (args: list mreg) (dst: mreg) (k: code) : res code := match trap with | NOTRAP => Error (msg "Asmgen.transl_load non-trapping loads unsupported on aarch64") | TRAP => @@ -1061,13 +1061,8 @@ Definition storeptr (src: ireg) (base: iregsp) (ofs: ptrofs) (k: code) := (** Function epilogue *) Definition make_epilogue (f: Mach.function) (k: code) := - (* FIXME - Cannot be used because memcpy destroys X30; - issue being discussed with X. Leroy *) - (* if is_leaf_function f - then Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k - else*) loadptr XSP f.(fn_retaddr_ofs) RA - (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k). + loadptr XSP f.(fn_retaddr_ofs) RA + (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k). (** Translation of a Mach instruction. *) |