diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-10-29 09:01:15 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-10-29 09:01:15 +0100 |
| commit | 350c39da5179b5b3d79357240d2bf9debc458b49 (patch) | |
| tree | 83cab9e0c727fd9514607f6fdf27a7ee3e5044cf /aarch64/Asmgen.v | |
| parent | f57103ff244a72201e12864e998eae791681e68f (diff) | |
| download | compcert-kvx-350c39da5179b5b3d79357240d2bf9debc458b49.tar.gz compcert-kvx-350c39da5179b5b3d79357240d2bf9debc458b49.zip | |
Found a bug in Asmgen about iregsp constructor
Diffstat (limited to 'aarch64/Asmgen.v')
| -rw-r--r-- | aarch64/Asmgen.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index af069929..5038245a 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -111,11 +111,11 @@ Definition basic_to_instruction (b: basic) : res Asm.instruction := | PArith (PArithPP (Pfcvtzu isz fsz) rd rs) => do rd' <- ireg_of_preg rd; do rs' <- freg_of_preg rs; OK (Asm.Pfcvtzu isz fsz rd' rs') - | PArith (PArithPP (Paddimm sz n) rd rs) => do rd' <- ireg_of_preg rd; - do rs' <- ireg_of_preg rs; + | PArith (PArithPP (Paddimm sz n) rd rs) => do rd' <- iregsp_of_preg rd; + do rs' <- iregsp_of_preg rs; OK (Asm.Paddimm sz rd' rs' n) - | PArith (PArithPP (Psubimm sz n) rd rs) => do rd' <- ireg_of_preg rd; - do rs' <- ireg_of_preg rs; + | PArith (PArithPP (Psubimm sz n) rd rs) => do rd' <- iregsp_of_preg rd; + do rs' <- iregsp_of_preg rs; OK (Asm.Psubimm sz rd' rs' n) | PArith (PArithPPP (Pasrv sz) rd r1 r2) => do rd' <- ireg_of_preg rd; @@ -150,12 +150,12 @@ Definition basic_to_instruction (b: basic) : res Asm.instruction := do r1' <- ireg_of_preg r1; do r2' <- ireg_of_preg r2; OK (Asm.Pudiv sz rd' r1' r2') - | PArith (PArithPPP (Paddext x) rd r1 r2) => do rd' <- ireg_of_preg rd; - do r1' <- ireg_of_preg r1; + | PArith (PArithPPP (Paddext x) rd r1 r2) => do rd' <- iregsp_of_preg rd; + do r1' <- iregsp_of_preg r1; do r2' <- ireg_of_preg r2; OK (Asm.Paddext rd' r1' r2' x) - | PArith (PArithPPP (Psubext x) rd r1 r2) => do rd' <- ireg_of_preg rd; - do r1' <- ireg_of_preg r1; + | PArith (PArithPPP (Psubext x) rd r1 r2) => do rd' <- iregsp_of_preg rd; + do r1' <- iregsp_of_preg r1; do r2' <- ireg_of_preg r2; OK (Asm.Psubext rd' r1' r2' x) | PArith (PArithPPP (Pfadd sz) rd r1 r2) => do rd' <- freg_of_preg rd; @@ -359,4 +359,4 @@ Definition transf_program (p: Mach.program) : res Asm.program := let mbp := Machblockgen.transf_program p in do mbp' <- PseudoAsmblockproof.transf_program mbp; do abp <- Asmblockgen.transf_program mbp'; - Asmblock_TRANSF.transf_program abp.
\ No newline at end of file + Asmblock_TRANSF.transf_program abp. |