diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-29 11:39:44 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-29 11:39:44 +0200 |
| commit | ec99800447f584e31523345469cee96977266327 (patch) | |
| tree | 0d66a7d21b81b48cc9c50533a22c05e7fbf58401 /mppa_k1c/Asmblockgen.v | |
| parent | cd3642815d4260a9e7868fce3fb6a4a8a8ea8746 (diff) | |
| download | compcert-kvx-ec99800447f584e31523345469cee96977266327.tar.gz compcert-kvx-ec99800447f584e31523345469cee96977266327.zip | |
begin using shrx
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 80210f7f..835b8a8c 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -519,11 +519,7 @@ Definition transl_op OK (Psrliw rd rs n ::i 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 ::i k else - Psraiw RTMP rs (Int.repr 31) ::i - Psrliw RTMP RTMP (Int.sub Int.iwordsize n) ::i - Paddw RTMP rs RTMP ::i - Psraiw rd RTMP n ::i k) + OK (Psrxiw rd rs n ::i k) | Ororimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Proriw rd rs n ::i k) |