diff options
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. |