diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2020-01-22 16:42:23 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2020-01-22 16:42:23 +0100 |
commit | 89e029310d175ee7ddbb157494bac46a08304b19 (patch) | |
tree | bd516047d1cea2be0141d00c1a18e440f4f368aa /riscV/Asmgen.v | |
parent | 60c15c9d1105dc2e53c17b3fb28ee9cc4716cbc6 (diff) | |
parent | fd2181ce5f6a3a5ba27349d1642ee4c59a6d9b34 (diff) | |
download | compcert-kvx-89e029310d175ee7ddbb157494bac46a08304b19.tar.gz compcert-kvx-89e029310d175ee7ddbb157494bac46a08304b19.zip |
Merge branch 'mppa-work' into mppa-duplicate-oracle
Diffstat (limited to 'riscV/Asmgen.v')
-rw-r--r-- | riscV/Asmgen.v | 30 |
1 files changed, 20 insertions, 10 deletions
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index 0fa47fca..b431d63d 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -505,11 +505,16 @@ Definition transl_op OK (Psrliw rd rs n :: k) | Oshrximm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; - OK (if Int.eq n Int.zero then Pmv rd rs :: k else - Psraiw X31 rs (Int.repr 31) :: - Psrliw X31 X31 (Int.sub Int.iwordsize n) :: - Paddw X31 rs X31 :: - Psraiw rd X31 n :: k) + OK (if Int.eq n Int.zero + then Pmv rd rs :: k + else if Int.eq n Int.one + then Psrliw X31 rs (Int.repr 31) :: + Paddw X31 rs X31 :: + Psraiw rd X31 Int.one :: k + else Psraiw X31 rs (Int.repr 31) :: + Psrliw X31 X31 (Int.sub Int.iwordsize n) :: + Paddw X31 rs X31 :: + Psraiw rd X31 n :: k) (* [Omakelong], [Ohighlong] should not occur *) | Olowlong, a1 :: nil => @@ -594,11 +599,16 @@ Definition transl_op OK (Psrlil rd rs n :: k) | Oshrxlimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; - OK (if Int.eq n Int.zero then Pmv rd rs :: k else - Psrail X31 rs (Int.repr 63) :: - Psrlil X31 X31 (Int.sub Int64.iwordsize' n) :: - Paddl X31 rs X31 :: - Psrail rd X31 n :: k) + OK (if Int.eq n Int.zero + then Pmv rd rs :: k + else if Int.eq n Int.one + then Psrlil X31 rs (Int.repr 63) :: + Paddl X31 rs X31 :: + Psrail rd X31 Int.one :: k + else Psrail X31 rs (Int.repr 63) :: + Psrlil X31 X31 (Int.sub Int64.iwordsize' n) :: + Paddl X31 rs X31 :: + Psrail rd X31 n :: k) | Onegf, a1 :: nil => do rd <- freg_of res; do rs <- freg_of a1; |