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/Asmgen.v | 35 +++++++++++++++++++++-------------- 1 file changed, 21 insertions(+), 14 deletions(-) (limited to 'aarch64/Asmgen.v') diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index 78c3f156..d9d59929 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -309,20 +309,27 @@ Definition basic_to_instruction (b: basic) : res Asm.instruction := end | PArith (Pfnmul fsz rd r1 r2) => OK (Asm.Pfnmul fsz rd r1 r2) - | PLoad Pldrw rd a => do rd' <- ireg_of_preg rd; OK (Asm.Pldrw rd' a) - | PLoad Pldrw_a rd a => do rd' <- ireg_of_preg rd; OK (Asm.Pldrw_a rd' a) - | PLoad Pldrx rd a => do rd' <- ireg_of_preg rd; OK (Asm.Pldrx rd' a) - | PLoad Pldrx_a rd a => do rd' <- ireg_of_preg rd; OK (Asm.Pldrx_a rd' a) - | PLoad (Pldrb sz) rd a => do rd' <- ireg_of_preg rd; OK (Asm.Pldrb sz rd' a) - | PLoad (Pldrsb sz) rd a => do rd' <- ireg_of_preg rd; OK (Asm.Pldrsb sz rd' a) - | PLoad (Pldrh sz) rd a => do rd' <- ireg_of_preg rd; OK (Asm.Pldrh sz rd' a) - | PLoad (Pldrsh sz) rd a => do rd' <- ireg_of_preg rd; OK (Asm.Pldrsh sz rd' a) - | PLoad Pldrzw rd a => do rd' <- ireg_of_preg rd; OK (Asm.Pldrzw rd' a) - | PLoad Pldrsw rd a => do rd' <- ireg_of_preg rd; OK (Asm.Pldrsw rd' a) - - | PLoad Pldrs rd a => do rd' <- freg_of_preg rd; OK (Asm.Pldrs rd' a) - | PLoad Pldrd rd a => do rd' <- freg_of_preg rd; OK (Asm.Pldrd rd' a) - | PLoad Pldrd_a rd a => do rd' <- freg_of_preg rd; OK (Asm.Pldrd_a rd' a) + | PLoad (PLd_rd_a Pldrw rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrw rd' a) + | PLoad (PLd_rd_a Pldrw_a rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrw_a rd' a) + | PLoad (PLd_rd_a Pldrx rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrx rd' a) + | PLoad (PLd_rd_a Pldrx_a rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrx_a rd' a) + | PLoad (PLd_rd_a (Pldrb sz) rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrb sz rd' a) + | PLoad (PLd_rd_a (Pldrsb sz) rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrsb sz rd' a) + | PLoad (PLd_rd_a (Pldrh sz) rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrh sz rd' a) + | PLoad (PLd_rd_a (Pldrsh sz) rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrsh sz rd' a) + | PLoad (PLd_rd_a Pldrzw rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrzw rd' a) + | PLoad (PLd_rd_a Pldrsw rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrsw rd' a) + + | PLoad (PLd_rd_a Pldrs rd a) => do rd' <- freg_of_preg rd; OK (Asm.Pldrs rd' a) + | PLoad (PLd_rd_a Pldrd rd a) => do rd' <- freg_of_preg rd; OK (Asm.Pldrd rd' a) + | PLoad (PLd_rd_a Pldrd_a rd a) => do rd' <- freg_of_preg rd; OK (Asm.Pldrd_a rd' a) + + | PLoad (Pldp Pldpw rd1 rd2 a) => do rd1' <- ireg_of_preg rd1; + do rd2' <- ireg_of_preg rd2; + OK (Asm.Pldpw rd1 rd2 a) + | PLoad (Pldp Pldpx rd1 rd2 a) => do rd1' <- ireg_of_preg rd1; + do rd2' <- ireg_of_preg rd2; + OK (Asm.Pldpx rd1 rd2 a) | PStore Pstrw r a => do r' <- ireg_of_preg r; OK (Asm.Pstrw r' a) | PStore Pstrw_a r a => do r' <- ireg_of_preg r; OK (Asm.Pstrw_a r' a) -- cgit