From 2c46ae4bd8f9f49554daa31988fd98793cc5601e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 26 Sep 2021 17:37:52 +0200 Subject: Qualify `Instance` and `Program Instance` as `Global` This avoids a new warning of Coq 8.14. --- powerpc/Machregs.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 9967bbae..eeca880a 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -75,9 +75,9 @@ Proof. intros. specialize (H r). InvBooleans. auto. Qed. -Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. +Global Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. -Instance Finite_mreg : Finite mreg := { +Global Instance Finite_mreg : Finite mreg := { Finite_elements := all_mregs; Finite_elements_spec := all_mregs_complete }. -- cgit 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 +++- powerpc/Asmgenproof.v | 6 +++--- powerpc/Asmgenproof1.v | 2 +- powerpc/Op.v | 39 ++++++++++++++++++++++++--------------- 4 files changed, 31 insertions(+), 20 deletions(-) (limited to 'powerpc') 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. 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. 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. diff --git a/powerpc/Op.v b/powerpc/Op.v index a96a0439..b849efa0 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -1272,53 +1272,62 @@ Definition is_rlw_mask (x: int) : bool := is_mask_rec rlw_transition rlw_accepting Int.wordsize RLW_S0 (Int.unsigned x). (** For the 64-bit [rldicl] and [rldicr] instructions, the acceptable - masks are [1111100000] and [0000011111], that is, some ones in the - high bits and some zeroes in the low bits, or conversely. All ones - is OK, but not all zeroes. The corresponding automata are: -<< - 0 1 - / \ / \ - \ / \ / (accepting: [1]) - [0] --1--> [1] + masks are (in big endian): +- for [rldicl]: masks that clear the leftmost bits (most significant bits), + that is, [00000011111], that is, ones in the low bits followed by zeros + in the high bits; +- for [rldicr]: masks that clear the rightmost bits (least significant bits), + that is, [11110000000], that is, zeros in the low bits followed by ones + in the high bits. + All ones is OK, but not all zeroes. + The corresponding automata for [rldicl] is +<< 1 0 / \ / \ \ / \ / (accepting: [1], [2]) [0] --1--> [1] --0--> [2] +>> + The automata for [rldicr] is +<< + 0 1 + / \ / \ + \ / \ / (accepting: [1]) + [0] --1--> [1] >> *) -Inductive rll_state: Type := RLL_S0 | RLL_S1 | RLL_Sbad. +Inductive rll_state: Type := RLL_S0 | RLL_S1 | RLL_S2 | RLL_Sbad. Definition rll_transition (s: rll_state) (b: bool) : rll_state := match s, b with - | RLL_S0, false => RLL_S0 | RLL_S0, true => RLL_S1 + | RLL_S1, false => RLL_S2 | RLL_S1, true => RLL_S1 + | RLL_S2, false => RLL_S2 | _, _ => RLL_Sbad end. Definition rll_accepting (s: rll_state) : bool := match s with - | RLL_S1 => true + | RLL_S1 | RLL_S2 => true | _ => false end. -Inductive rlr_state: Type := RLR_S0 | RLR_S1 | RLR_S2 | RLR_Sbad. +Inductive rlr_state: Type := RLR_S0 | RLR_S1 | RLR_Sbad. Definition rlr_transition (s: rlr_state) (b: bool) : rlr_state := match s, b with + | RLR_S0, false => RLR_S0 | RLR_S0, true => RLR_S1 - | RLR_S1, false => RLR_S2 | RLR_S1, true => RLR_S1 - | RLR_S2, false => RLR_S2 | _, _ => RLR_Sbad end. Definition rlr_accepting (s: rlr_state) : bool := match s with - | RLR_S1 | RLR_S2 => true + | RLR_S1 => true | _ => false end. -- cgit