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/Asmgenproof.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'powerpc/Asmgenproof.v') diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 85541118..9f2ddc36 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -294,10 +294,10 @@ Opaque Int.eq. - unfold xorimm64, opimm64. destruct Int64.eq. TailNoLabel. destruct ireg_eq; [apply tail_nolabel_cons; unfold nolabel;auto|]; eapply tail_nolabel_trans; TailNoLabel. - unfold rolm64, andimm64_base, opimm64. - destruct (is_rldl_mask i0 || is_rldr_mask i0 || is_rldl_mask (Int64.shru' i0 i)). TailNoLabel. - apply tail_nolabel_cons; unfold nolabel; auto. + destruct orb. + TailNoLabel. destruct Int64.eq. TailNoLabel. - destruct ireg_eq; [apply tail_nolabel_cons; unfold nolabel;auto|]; eapply tail_nolabel_trans; TailNoLabel. + destruct ireg_eq; TailNoLabel; eapply tail_nolabel_trans; TailNoLabel. - eapply transl_cond_op_label; eauto. - destruct (preg_of r); monadInv H. eapply transl_select_op_label; eauto. eapply transl_fselect_op_label; eauto. Qed. -- cgit