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

2 files changed, 31 insertions, 16 deletions

diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index a1457df..d913958 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 fa6b560..7d3ae83 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.