Micro-optimization of (x & mask) >>s amount into a rolm when mask >= 0.

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

3 files changed, 77 insertions, 16 deletions

diff --git a/lib/Integers.v b/lib/Integers.v
index 8dc5b6f5..6630de33 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -653,6 +653,14 @@ Proof.
   auto. unfold max_signed in H. omegaContradiction.
 Qed.
 
+Theorem signed_positive:
+  forall x, signed x >= 0 <-> unsigned x <= max_signed.
+Proof.
+  intros. unfold signed, max_signed.
+  generalize (unsigned_range x) half_modulus_modulus half_modulus_pos; intros.
+  destruct (zlt (unsigned x) half_modulus); omega.
+Qed.
+
 (** ** Properties of zero, one, minus one *)
 
 Theorem unsigned_zero: unsigned zero = 0.
@@ -2660,6 +2668,44 @@ Proof.
   generalize min_signed_neg. unfold max_signed. omega. 
 Qed.
 
+(** Connections between [shr] and [shru]. *)
+
+Lemma shr_shru_positive:
+  forall x y,
+  signed x >= 0 -> 
+  shr x y = shru x y.
+Proof.
+  intros.
+  rewrite shr_div_two_p. rewrite shru_div_two_p.
+  rewrite signed_eq_unsigned. auto. apply signed_positive. auto.
+Qed.
+
+Lemma and_positive:
+  forall x y, signed y >= 0 -> signed (and x y) >= 0.
+Proof.
+  intros.
+  assert (unsigned y < half_modulus). rewrite signed_positive in H. unfold max_signed in H; omega. 
+  generalize (sign_bit_of_Z y). rewrite zlt_true; auto. intros A.
+  generalize (sign_bit_of_Z (and x y)).
+  unfold and at 1. unfold bitwise_binop at 1.
+  set (fx := bits_of_Z wordsize (unsigned x)).
+  set (fy := bits_of_Z wordsize (unsigned y)).
+  rewrite unsigned_repr; auto with ints. 
+  rewrite bits_of_Z_of_bits. unfold fy. rewrite A. rewrite andb_false_r. 
+  destruct (zlt (unsigned (and x y)) half_modulus); intros.
+  rewrite signed_positive. unfold max_signed; omega.
+  congruence.
+  generalize wordsize_pos; omega.
+Qed.
+
+Theorem shr_and_is_shru_and:
+  forall x y z,
+  lt y zero = false -> shr (and x y) z = shru (and x y) z.
+Proof.
+  intros. apply shr_shru_positive. apply and_positive. 
+  unfold lt in H. rewrite signed_zero in H. destruct (zlt (signed y) 0). congruence. auto.
+Qed.
+
 (** ** Properties of integer zero extension and sign extension. *)
 
 Section EXTENSIONS.
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index a1457dfa..d9139585 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -179,12 +179,6 @@ Definition shlimm (e1: expr) (n2: int) :=
   else
     Eop Oshl (e1:::Eop (Ointconst n2) Enil:::Enil).
 
-Definition shrimm (e1: expr) (n2: int) :=
-  if Int.eq n2 Int.zero then
-    e1
-  else
-    Eop (Oshrimm n2) (e1:::Enil).
-
 Definition shruimm (e1: expr) (n2: int) :=
   if Int.eq n2 Int.zero then
     e1
@@ -193,6 +187,19 @@ Definition shruimm (e1: expr) (n2: int) :=
   else
     Eop Oshru (e1:::Eop (Ointconst n2) Enil:::Enil).
 
+Nondetfunction shrimm (e1: expr) (n2: int) :=
+  if Int.eq n2 Int.zero then
+    e1
+  else
+    match e1 with
+    | Eop (Oandimm mask1) (t1:::Enil) =>
+        if Int.lt mask1 Int.zero
+        then Eop (Oshrimm n2) (e1:::Enil)
+        else shruimm e1 n2
+    | _ =>
+        Eop (Oshrimm n2) (e1:::Enil)
+    end.
+
 (** ** Integer multiply *)
 
 Definition mulimm_base (n1: int) (e2: expr) :=
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index fa6b5608..7d3ae831 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -286,16 +286,6 @@ Proof.
   TrivialExists. econstructor. eauto. econstructor. EvalOp. simpl; eauto. constructor. auto.
 Qed.
 
-Theorem eval_shrimm:
-  forall n, unary_constructor_sound (fun a => shrimm a n)
-                                    (fun x => Val.shr x (Vint n)).
-Proof.
-  red; intros.  unfold shrimm.
-  predSpec Int.eq Int.eq_spec n Int.zero.
-  subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shr_zero; auto.
-  TrivialExists.
-Qed.
-
 Theorem eval_shruimm:
   forall n, unary_constructor_sound (fun a => shruimm a n)
                                     (fun x => Val.shru x (Vint n)).
@@ -308,6 +298,24 @@ Proof.
   TrivialExists. econstructor. eauto. econstructor. EvalOp. simpl; eauto. constructor. auto.
 Qed.
 
+Theorem eval_shrimm:
+  forall n, unary_constructor_sound (fun a => shrimm a n)
+                                    (fun x => Val.shr x (Vint n)).
+Proof.
+  red; intros until x. unfold shrimm. 
+  predSpec Int.eq Int.eq_spec n Int.zero.
+  intros. subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shr_zero; auto.
+  case (shrimm_match a); intros.
+  destruct (Int.lt mask1 Int.zero) as []_eqn. 
+  TrivialExists.
+  replace (Val.shr x (Vint n)) with (Val.shru x (Vint n)). 
+  apply eval_shruimm; auto.
+  destruct x; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto. 
+  decEq. symmetry. InvEval. destruct v1; simpl in H0; inv H0. 
+  apply Int.shr_and_is_shru_and; auto.
+  TrivialExists.
+Qed.
+
 Lemma eval_mulimm_base:
   forall n, unary_constructor_sound (mulimm_base n) (fun x => Val.mul x (Vint n)).
 Proof.