Integers: cleaned up bitwise operations, redefined shr, zero_ext and sign_ext

  as bitwise operations rather than arithmetic ones.
CastOptimproof: fixed for ARM port.
Other files: adapted to changes in Integers.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1472 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

4 files changed, 102 insertions, 44 deletions

diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index ee2867e6..fc14830c 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -1217,10 +1217,10 @@ Proof.
     rewrite <- Int.shl_rolm. rewrite Int.shl_mul.
     rewrite Int.mul_signed.
     apply Int.signed_repr.
-    split. apply Zle_trans with 0. vm_compute; congruence. omega. 
+    split. apply Zle_trans with 0. compute; congruence. omega. 
     omega.
-    vm_compute. reflexivity.
-    vm_compute. apply Int.mkint_eq. auto.
+    compute. reflexivity.
+    apply Int.mkint_eq. compute. reflexivity.
   inv AT. simpl in H7. 
   set (k1 := Pbtbl GPR12 tbl :: transl_code f c).
   set (rs1 := nextinstr (rs0 # GPR12 <- (Vint (Int.rolm n (Int.repr 2) (Int.repr (-4)))))).
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 5ebde633..0b146daa 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -79,41 +79,25 @@ Proof.
   unfold high_s. 
   rewrite <- (Int.divu_pow2 (Int.sub n (low_s n)) (Int.repr 65536) (Int.repr 16)).
   change (two_p (Int.unsigned (Int.repr 16))) with 65536.
-
-  assert (forall x y, y > 0 -> (x - x mod y) mod y = 0).
-  intros. apply Zmod_unique with (x / y). 
-  generalize (Z_div_mod_eq x y H). intro. rewrite Zmult_comm. omega.
-  omega.
-
-  assert (Int.modu (Int.sub n (low_s n)) (Int.repr 65536) = Int.zero).
-  unfold Int.modu, Int.zero. decEq. 
-  change (Int.unsigned (Int.repr 65536)) with 65536.
-  unfold Int.sub. 
-  assert (forall a b, Int.eqm a b -> b mod 65536 = 0 -> a mod 65536 = 0).
-  intros a b [k EQ] H1. rewrite EQ. 
-  change Int.modulus with (65536 * 65536). 
-  rewrite Zmult_assoc. rewrite Zplus_comm. rewrite Z_mod_plus. auto.
-  omega.
-  eapply H0. apply Int.eqm_sym. apply Int.eqm_unsigned_repr. 
-  unfold low_s. unfold Int.sign_ext. 
-  change (two_p 16) with 65536. change (two_p (16-1)) with 32768. 
-  set (N := Int.unsigned n).
-  case (zlt (N mod 65536) 32768); intro.
-  apply H0 with (N - N mod 65536). auto with ints.
-  apply H. omega.
-  apply H0 with (N - (N mod 65536 - 65536)). auto with ints.
-  replace (N - (N mod 65536 - 65536))
-     with ((N - N mod 65536) + 1 * 65536).
-  rewrite Z_mod_plus. apply H. omega. omega. ring. 
-
-  assert (Int.repr 65536 <> Int.zero). compute. congruence. 
-  generalize (Int.modu_divu_Euclid (Int.sub n (low_s n)) (Int.repr 65536) H1).
-  rewrite H0. rewrite Int.add_zero. intro. rewrite <- H2. 
-  rewrite Int.sub_add_opp. rewrite Int.add_assoc. 
-  replace (Int.add (Int.neg (low_s n)) (low_s n)) with Int.zero.
-  apply Int.add_zero. symmetry. rewrite Int.add_commut. 
-  rewrite <- Int.sub_add_opp. apply Int.sub_idem.
-
+  set (x := Int.sub n (low_s n)).
+  assert (x = Int.add (Int.mul (Int.divu x (Int.repr 65536)) (Int.repr 65536))
+                      (Int.modu x (Int.repr 65536))).
+    apply Int.modu_divu_Euclid. compute; congruence.
+  assert (Int.modu x (Int.repr 65536) = Int.zero).
+    unfold Int.modu, Int.zero. decEq.
+    change 0 with (0 mod 65536).
+    change (Int.unsigned (Int.repr 65536)) with 65536.
+    apply Int.eqmod_mod_eq. omega. 
+    unfold x, low_s. eapply Int.eqmod_trans. 
+    eapply Int.eqm_eqmod_two_p with (n := 16). compute; auto.
+    unfold Int.sub. apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl. 
+    replace 0 with (Int.unsigned n - Int.unsigned n) by omega.
+    apply Int.eqmod_sub. apply Int.eqmod_refl. apply Int.eqmod_sign_ext'. 
+    compute; auto.
+  rewrite H0 in H. rewrite Int.add_zero in H.
+  rewrite <- H. unfold x. rewrite Int.sub_add_opp. rewrite Int.add_assoc.
+  rewrite (Int.add_commut (Int.neg (low_s n))). rewrite <- Int.sub_add_opp. 
+  rewrite Int.sub_idem. apply Int.add_zero.
   reflexivity.
 Qed.
 
diff --git a/powerpc/SelectOp.v b/powerpc/SelectOp.v
index fe30b96a..e6a281b2 100644
--- a/powerpc/SelectOp.v
+++ b/powerpc/SelectOp.v
@@ -371,6 +371,80 @@ Definition sub (e1: expr) (e2: expr) :=
 
 (** ** Rotates and immediate shifts *)
 
+(** Recognition of integers that are acceptable as immediate operands
+  to the [rlwim] PowerPC instruction.  These integers are of the form
+  [000011110000] or [111100001111], that is, a run of one bits
+  surrounded by zero bits, or conversely.  We recognize these integers by
+  running the following automaton on the bits.  The accepting states are
+  2, 3, 4, 5, and 6.
+<<
+               0          1          0
+              / \        / \        / \
+              \ /        \ /        \ /
+        -0--> [1] --1--> [2] --0--> [3]
+       /     
+     [0]
+       \
+        -1--> [4] --0--> [5] --1--> [6]
+              / \        / \        / \
+              \ /        \ /        \ /
+               1          0          1
+>>
+*)
+
+Inductive rlw_state: Type :=
+  | RLW_S0 : rlw_state
+  | RLW_S1 : rlw_state
+  | RLW_S2 : rlw_state
+  | RLW_S3 : rlw_state
+  | RLW_S4 : rlw_state
+  | RLW_S5 : rlw_state
+  | RLW_S6 : rlw_state
+  | RLW_Sbad : rlw_state.
+
+Definition rlw_transition (s: rlw_state) (b: bool) : rlw_state :=
+  match s, b with
+  | RLW_S0, false => RLW_S1
+  | RLW_S0, true  => RLW_S4
+  | RLW_S1, false => RLW_S1
+  | RLW_S1, true  => RLW_S2
+  | RLW_S2, false => RLW_S3
+  | RLW_S2, true  => RLW_S2
+  | RLW_S3, false => RLW_S3
+  | RLW_S3, true  => RLW_Sbad
+  | RLW_S4, false => RLW_S5
+  | RLW_S4, true  => RLW_S4
+  | RLW_S5, false => RLW_S5
+  | RLW_S5, true  => RLW_S6
+  | RLW_S6, false => RLW_Sbad
+  | RLW_S6, true  => RLW_S6
+  | RLW_Sbad, _ => RLW_Sbad
+  end.
+
+Definition rlw_accepting (s: rlw_state) : bool :=
+  match s with
+  | RLW_S0 => false
+  | RLW_S1 => false
+  | RLW_S2 => true
+  | RLW_S3 => true
+  | RLW_S4 => true
+  | RLW_S5 => true
+  | RLW_S6 => true
+  | RLW_Sbad => false
+  end.
+
+Fixpoint is_rlw_mask_rec (n: nat) (s: rlw_state) (x: Z) {struct n} : bool :=
+  match n with
+  | O =>
+      rlw_accepting s
+  | S m =>
+      let (b, y) := Int.Z_bin_decomp x in
+      is_rlw_mask_rec m (rlw_transition s b) y
+  end.
+
+Definition is_rlw_mask (x: int) : bool :=
+  is_rlw_mask_rec Int.wordsize RLW_S0 (Int.unsigned x).
+
 (*
 Definition rolm (e1: expr) :=
   match e1 with
@@ -414,7 +488,7 @@ Definition rolm (e1: expr) (amount2 mask2: int) :=
   | rolm_case2 amount1 mask1 t1 =>
       let amount := Int.modu (Int.add amount1 amount2) Int.iwordsize in
       let mask := Int.and (Int.rol mask1 amount2) mask2 in
-      if Int.is_rlw_mask mask
+      if is_rlw_mask mask
       then Eop (Orolm amount mask) (t1:::Enil)
       else Eop (Orolm amount2 mask2) (e1:::Enil)
   | rolm_default e1 =>
@@ -548,7 +622,7 @@ Definition mul (e1: expr) (e2: expr) :=
 (** ** Bitwise and, or, xor *)
 
 Definition andimm (n1: int) (e2: expr) :=
-  if Int.is_rlw_mask n1
+  if is_rlw_mask n1
   then rolm e2 Int.zero n1
   else Eop (Oandimm n1) (e2:::Enil).
 
@@ -591,7 +665,7 @@ Definition or (e1: expr) (e2: expr) :=
   match or_match e1 e2 with
   | or_case1 amount1 mask1 t1 amount2 mask2 t2 =>
       if Int.eq amount1 amount2
-      && Int.is_rlw_mask (Int.or mask1 mask2)
+      && is_rlw_mask (Int.or mask1 mask2)
       && same_expr_pure t1 t2
       then Eop (Orolm amount1 (Int.or mask1 mask2)) (t1:::Enil)
       else Eop Oor (e1:::e2:::Enil)
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 21614e82..2fc13273 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -355,7 +355,7 @@ Lemma eval_rolm:
 Proof.
   intros until x. unfold rolm; case (rolm_match a); intros; InvEval.
   eauto with evalexpr. 
-  case (Int.is_rlw_mask (Int.and (Int.rol mask1 amount) mask)).
+  case (is_rlw_mask (Int.and (Int.rol mask1 amount) mask)).
   EvalOp. simpl. subst x. 
   decEq. decEq. 
   symmetry. apply Int.rolm_rolm. apply int_wordsize_divides_modulus.
@@ -460,7 +460,7 @@ Theorem eval_andimm:
   eval_expr ge sp e m le a (Vint x) ->
   eval_expr ge sp e m le (andimm n a) (Vint (Int.and x n)).
 Proof.
-  intros.  unfold andimm. case (Int.is_rlw_mask n).
+  intros.  unfold andimm. case (is_rlw_mask n).
   rewrite <- Int.rolm_zero. apply eval_rolm; auto.
   EvalOp. 
 Qed.
@@ -500,7 +500,7 @@ Lemma eval_or:
 Proof.
   intros until y; unfold or; case (or_match a b); intros; InvEval.
   caseEq (Int.eq amount1 amount2 
-          && Int.is_rlw_mask (Int.or mask1 mask2) 
+          && is_rlw_mask (Int.or mask1 mask2) 
           && same_expr_pure t1 t2); intro.
   destruct (andb_prop _ _ H1). destruct (andb_prop _ _ H4).
   generalize (Int.eq_spec amount1 amount2). rewrite H6. intro. subst amount2.