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/Asmgenproof1.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'powerpc/Asmgenproof1.v') diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 6ae520ef..761833cc 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -788,7 +788,7 @@ Lemma rolm64_correct: /\ forall r': preg, r' <> r1 -> r' <> GPR12 -> important_preg r' = true -> rs'#r' = rs#r'. Proof. intros. unfold rolm64. - destruct (is_rldl_mask mask || is_rldr_mask mask || is_rldl_mask (Int64.shru' mask amount)). + destruct orb. - econstructor; split. eapply exec_straight_one. simpl; reflexivity. reflexivity. intuition Simpl. - edestruct (andimm64_base_correct r1 r1 mask k) as (rs2 & A & B & C); auto. -- cgit