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.

4 files changed, 31 insertions, 20 deletions

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.