From d2b9858f3f5e013bbd9d2221c8d1a3d2960665be Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 21 Jan 2012 16:11:50 +0000 Subject: powerpc/SelectOp: optimize the pattern ((x >>s N) & N1) & N2 common in a certain customer's code backend/Coloringaux: avoid spilling the dummy result registers for built-ins that have no result. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1799 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/SelectOpproof.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'powerpc/SelectOpproof.v') diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 8ad9807e..cc14d339 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -343,6 +343,21 @@ Theorem eval_andimm: Proof. intros; red; intros until x. unfold andimm. case (andimm_match a); intros. InvEval. TrivialExists. simpl. rewrite Int.and_commut; auto. + set (n' := Int.and n n2). + destruct (Int.eq (Int.shru (Int.shl n' amount) amount) n' && + Int.ltu amount Int.iwordsize) as []_eqn. + InvEval. destruct (andb_prop _ _ Heqb). + generalize (Int.eq_spec (Int.shru (Int.shl n' amount) amount) n'). rewrite H1; intros. + replace (Val.and x (Vint n)) + with (Val.rolm v0 (Int.sub Int.iwordsize amount) (Int.and (Int.shru Int.mone amount) n')). + apply eval_rolm; auto. + subst. destruct v0; simpl; auto. rewrite H3. simpl. decEq. rewrite Int.and_assoc. + rewrite (Int.and_commut n2 n). + transitivity (Int.and (Int.shru i amount) (Int.and n n2)). + rewrite (Int.shru_rolm i); auto. unfold Int.rolm. rewrite Int.and_assoc; auto. + symmetry. apply Int.shr_and_shru_and. auto. + set (e2 := Eop (Oshrimm amount) (t2 ::: Enil)) in *. + InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists. InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists. InvEval. subst. TrivialExists. simpl. destruct v1; auto. simpl. unfold Int.rolm. rewrite Int.and_assoc. -- cgit