From d194e47a7d494944385ff61c194693f8a67787cb Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 27 Oct 2021 17:03:26 +0200 Subject: PPC64: revised generation of rldic* instructions In Op.v, the definitions of is_rldl_mask and is_rldr_mask mask were swapped: - rldl is for [00001111] masks that clear on the left, hence start with 1s and finish with 0s; - rldr is for [11110000] masks that clear on the right, hence start with 0s and finish with 1s. In Asmgen.v, the case for masks of the form [00011111100] that can generate a rldic instruction was incorrectly detected. --- powerpc/Asmgen.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'powerpc/Asmgen.v') diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 7b6ac9af..6dfdf21a 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. -- cgit