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

1 files changed, 18 insertions, 10 deletions

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.