diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-10-29 21:56:59 +0200 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-10-29 21:56:59 +0200 |
| commit | ae2d228c04f4fca1e281b146764646cbdd7d6b1d (patch) | |
| tree | 244f88aebc77a9ca2ef7e69731deb1dfee434ece /powerpc/Asmgen.v | |
| parent | e19d179d1f30d5893e5f30dbd33188350656831e (diff) | |
| parent | d194e47a7d494944385ff61c194693f8a67787cb (diff) | |
| download | compcert-kvx-ae2d228c04f4fca1e281b146764646cbdd7d6b1d.tar.gz compcert-kvx-ae2d228c04f4fca1e281b146764646cbdd7d6b1d.zip | |
Merge remote-tracking branch 'origin/master' into towards_3.10
Diffstat (limited to 'powerpc/Asmgen.v')
| -rw-r--r-- | powerpc/Asmgen.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 924773e7..eafb6d3c 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -183,7 +183,9 @@ Definition andimm64 (r1 r2: ireg) (n: int64) (k : code) := andimm64_base r1 r2 n k. Definition rolm64 (r1 r2: ireg) (amount: int) (mask: int64) (k: code) := - if is_rldl_mask mask || is_rldr_mask mask || is_rldl_mask (Int64.shru' mask amount) then + if is_rldl_mask mask || is_rldr_mask mask + || (let mask' := Int64.shru' mask amount in + Int64.eq mask (Int64.shl' mask' amount) && is_rldl_mask mask') then Prldinm r1 r2 amount mask :: k else Prldinm r1 r2 amount Int64.mone :: andimm64_base r1 r1 mask k. |