diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-12-02 18:02:23 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-12-02 18:02:23 +0100 |
| commit | c48b7c63592e5930f022452ee6c3f1cf3d1ada97 (patch) | |
| tree | 8b77e87f9dbc17e67da3c36b7402fae21f033e33 /aarch64/Asmgen.v | |
| parent | dd299de4b51c561b3a2d8e9f388396381b0e2b85 (diff) | |
| download | compcert-kvx-c48b7c63592e5930f022452ee6c3f1cf3d1ada97.tar.gz compcert-kvx-c48b7c63592e5930f022452ee6c3f1cf3d1ada97.zip | |
Adding semantics for Pldp
This commit prepare the backend for a peephole optimization in Asmblock.
Diffstat (limited to 'aarch64/Asmgen.v')
| -rw-r--r-- | aarch64/Asmgen.v | 35 |
1 files changed, 21 insertions, 14 deletions
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) |