From 972f6b9890ea3644626fc097e460035028b940eb Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 4 Dec 2020 23:26:01 +0100 Subject: a first working draft on ldp/stp peephole --- aarch64/Asmgen.v | 28 ++++++++++++++++++---------- 1 file changed, 18 insertions(+), 10 deletions(-) (limited to 'aarch64/Asmgen.v') diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index d9d59929..f7ec07ae 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -331,16 +331,23 @@ Definition basic_to_instruction (b: basic) : res Asm.instruction := 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) - | PStore Pstrx r a => do r' <- ireg_of_preg r; OK (Asm.Pstrx r' a) - | PStore Pstrx_a r a => do r' <- ireg_of_preg r; OK (Asm.Pstrx_a r' a) - | PStore Pstrb r a => do r' <- ireg_of_preg r; OK (Asm.Pstrb r' a) - | PStore Pstrh r a => do r' <- ireg_of_preg r; OK (Asm.Pstrh r' a) - - | PStore Pstrs r a => do r' <- freg_of_preg r; OK (Asm.Pstrs r' a) - | PStore Pstrd r a => do r' <- freg_of_preg r; OK (Asm.Pstrd r' a) - | PStore Pstrd_a r a => do r' <- freg_of_preg r; OK (Asm.Pstrd_a r' a) + | PStore (PSt_rs_a Pstrw r a) => do r' <- ireg_of_preg r; OK (Asm.Pstrw r' a) + | PStore (PSt_rs_a Pstrw_a r a) => do r' <- ireg_of_preg r; OK (Asm.Pstrw_a r' a) + | PStore (PSt_rs_a Pstrx r a) => do r' <- ireg_of_preg r; OK (Asm.Pstrx r' a) + | PStore (PSt_rs_a Pstrx_a r a) => do r' <- ireg_of_preg r; OK (Asm.Pstrx_a r' a) + | PStore (PSt_rs_a Pstrb r a) => do r' <- ireg_of_preg r; OK (Asm.Pstrb r' a) + | PStore (PSt_rs_a Pstrh r a) => do r' <- ireg_of_preg r; OK (Asm.Pstrh r' a) + + | PStore (PSt_rs_a Pstrs r a) => do r' <- freg_of_preg r; OK (Asm.Pstrs r' a) + | PStore (PSt_rs_a Pstrd r a) => do r' <- freg_of_preg r; OK (Asm.Pstrd r' a) + | PStore (PSt_rs_a Pstrd_a r a) => do r' <- freg_of_preg r; OK (Asm.Pstrd_a r' a) + + | PStore (Pstp Pstpw rs1 rs2 a) => do rs1' <- ireg_of_preg rs1; + do rs2' <- ireg_of_preg rs2; + OK (Asm.Pstpw rs1 rs2 a) + | PStore (Pstp Pstpx rs1 rs2 a) => do rs1' <- ireg_of_preg rs1; + do rs2' <- ireg_of_preg rs2; + OK (Asm.Pstpx rs1 rs2 a) | Pallocframe sz linkofs => OK (Asm.Pallocframe sz linkofs) | Pfreeframe sz linkofs => OK (Asm.Pfreeframe sz linkofs) @@ -352,6 +359,7 @@ Definition basic_to_instruction (b: basic) : res Asm.instruction := | Pcvtuw2x rd r1 => OK (Asm.Pcvtuw2x rd r1) | Pcvtx2w rd => OK (Asm.Pcvtx2w rd) + | Pnop => OK (Asm.Pnop) end. Definition cf_instruction_to_instruction (cfi: cf_instruction) : Asm.instruction := -- cgit