From 576d79403ecb81d2be41e802790a5236f6fcf521 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 9 Jul 2012 13:43:41 +0000 Subject: 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 --- powerpc/SelectOpproof.v | 28 ++++++++++++++++++---------- 1 file changed, 18 insertions(+), 10 deletions(-) (limited to 'powerpc/SelectOpproof.v') 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. -- cgit v1.2.3