From c48b7c63592e5930f022452ee6c3f1cf3d1ada97 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 2 Dec 2020 18:02:23 +0100 Subject: Adding semantics for Pldp This commit prepare the backend for a peephole optimization in Asmblock. --- aarch64/Asmblockgen.v | 36 ++++++++++++++++++------------------ 1 file changed, 18 insertions(+), 18 deletions(-) (limited to 'aarch64/Asmblockgen.v') diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v index b25a95da..abc9162b 100644 --- a/aarch64/Asmblockgen.v +++ b/aarch64/Asmblockgen.v @@ -280,13 +280,13 @@ Definition indexed_memory_access_bc (insn: addressing -> basic) Definition loadind (base: iregsp) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: bcode) := match ty, preg_of dst with - | Tint, IR rd => OK (indexed_memory_access_bc (PLoad Pldrw rd) 4 base ofs k) - | Tlong, IR rd => OK (indexed_memory_access_bc (PLoad Pldrx rd) 8 base ofs k) - | Tsingle, FR rd => OK (indexed_memory_access_bc (PLoad Pldrs rd) 4 base ofs k) - | Tfloat, FR rd => OK (indexed_memory_access_bc (PLoad Pldrd rd) 8 base ofs k) - | Tany32, IR rd => OK (indexed_memory_access_bc (PLoad Pldrw_a rd) 4 base ofs k) - | Tany64, IR rd => OK (indexed_memory_access_bc (PLoad Pldrx_a rd) 8 base ofs k) - | Tany64, FR rd => OK (indexed_memory_access_bc (PLoad Pldrd_a rd) 8 base ofs k) + | Tint, IR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrw rd) 4 base ofs k) + | Tlong, IR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrx rd) 8 base ofs k) + | Tsingle, FR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrs rd) 4 base ofs k) + | Tfloat, FR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrd rd) 8 base ofs k) + | Tany32, IR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrw_a rd) 4 base ofs k) + | Tany64, IR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrx_a rd) 8 base ofs k) + | Tany64, FR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrd_a rd) 8 base ofs k) | _, _ => Error (msg "Asmgen.loadind") end. @@ -303,7 +303,7 @@ Definition storeind (src: mreg) (base: iregsp) (ofs: ptrofs) (ty: typ) (k: bcode end. Definition loadptr_bc (base: iregsp) (ofs: ptrofs) (dst: ireg) (k: bcode): bcode := - indexed_memory_access_bc (PLoad Pldrx dst) 8 base ofs k. + indexed_memory_access_bc (PLd_rd_a Pldrx dst) 8 base ofs k. Definition storeptr_bc (src: ireg) (base: iregsp) (ofs: ptrofs) (k: bcode): bcode := indexed_memory_access_bc (PStore Pstrx src) 8 base ofs k. @@ -1096,25 +1096,25 @@ Definition transl_load (chunk: memory_chunk) (addr: Op.addressing) (args: list mreg) (dst: mreg) (k: bcode) : res bcode := match chunk with | Mint8unsigned => - do rd <- ireg_of dst; transl_addressing 1 addr args (PLoad (Pldrb W) rd) k + do rd <- ireg_of dst; transl_addressing 1 addr args (PLd_rd_a (Pldrb W) rd) k | Mint8signed => - do rd <- ireg_of dst; transl_addressing 1 addr args (PLoad (Pldrsb W) rd) k + do rd <- ireg_of dst; transl_addressing 1 addr args (PLd_rd_a (Pldrsb W) rd) k | Mint16unsigned => - do rd <- ireg_of dst; transl_addressing 2 addr args (PLoad (Pldrh W) rd) k + do rd <- ireg_of dst; transl_addressing 2 addr args (PLd_rd_a (Pldrh W) rd) k | Mint16signed => - do rd <- ireg_of dst; transl_addressing 2 addr args (PLoad (Pldrsh W) rd) k + do rd <- ireg_of dst; transl_addressing 2 addr args (PLd_rd_a (Pldrsh W) rd) k | Mint32 => - do rd <- ireg_of dst; transl_addressing 4 addr args (PLoad Pldrw rd) k + do rd <- ireg_of dst; transl_addressing 4 addr args (PLd_rd_a Pldrw rd) k | Mint64 => - do rd <- ireg_of dst; transl_addressing 8 addr args (PLoad Pldrx rd) k + do rd <- ireg_of dst; transl_addressing 8 addr args (PLd_rd_a Pldrx rd) k | Mfloat32 => - do rd <- freg_of dst; transl_addressing 4 addr args (PLoad Pldrs rd) k + do rd <- freg_of dst; transl_addressing 4 addr args (PLd_rd_a Pldrs rd) k | Mfloat64 => - do rd <- freg_of dst; transl_addressing 8 addr args (PLoad Pldrd rd) k + do rd <- freg_of dst; transl_addressing 8 addr args (PLd_rd_a Pldrd rd) k | Many32 => - do rd <- ireg_of dst; transl_addressing 4 addr args (PLoad Pldrw_a rd) k + do rd <- ireg_of dst; transl_addressing 4 addr args (PLd_rd_a Pldrw_a rd) k | Many64 => - do rd <- ireg_of dst; transl_addressing 8 addr args (PLoad Pldrx_a rd) k + do rd <- ireg_of dst; transl_addressing 8 addr args (PLd_rd_a Pldrx_a rd) k end. Definition transl_store (chunk: memory_chunk) (addr: Op.addressing) -- cgit