diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-14 11:05:36 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-14 11:05:36 +0100 |
| commit | 9c6fac6cd52b824aaefac66089bf5c71e27845be (patch) | |
| tree | a3724f9a2109d6de563606a231ad7c59a5b693de /riscV/Asmgen.v | |
| parent | 804e8174a944e3d8983c077502e57113ecdda6dd (diff) | |
| download | compcert-kvx-9c6fac6cd52b824aaefac66089bf5c71e27845be.tar.gz compcert-kvx-9c6fac6cd52b824aaefac66089bf5c71e27845be.zip | |
rv32: 3-instruction signed divide-by-two sequence (as opposed to 4)
Diffstat (limited to 'riscV/Asmgen.v')
| -rw-r--r-- | riscV/Asmgen.v | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index a704ed74..5952aa82 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -503,11 +503,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 => |