diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-12-04 23:26:01 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-12-04 23:26:01 +0100 |
| commit | 972f6b9890ea3644626fc097e460035028b940eb (patch) | |
| tree | a29e64ad4e978f55f06e19345ee753858f1334e0 /aarch64/Asmgen.v | |
| parent | c48b7c63592e5930f022452ee6c3f1cf3d1ada97 (diff) | |
| download | compcert-kvx-972f6b9890ea3644626fc097e460035028b940eb.tar.gz compcert-kvx-972f6b9890ea3644626fc097e460035028b940eb.zip | |
a first working draft on ldp/stp peephole
Diffstat (limited to 'aarch64/Asmgen.v')
| -rw-r--r-- | aarch64/Asmgen.v | 28 |
1 files changed, 18 insertions, 10 deletions
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 := |