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

2 files changed, 22 insertions, 0 deletions

diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index 40c9011..3bb5544 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -210,6 +210,13 @@ Nondetfunction andimm (n1: int) (e2: expr) :=
   match e2 with
   | Eop (Ointconst n2) Enil =>
       Eop (Ointconst (Int.and n1 n2)) Enil
+  | Eop (Oandimm n2) (Eop (Oshrimm amount) (t2:::Enil) ::: Enil) =>
+      let n := Int.and n1 n2 in
+      if Int.eq (Int.shru (Int.shl n amount) amount) n
+      && Int.ltu amount Int.iwordsize
+      then rolm t2 (Int.sub Int.iwordsize amount) 
+                   (Int.and (Int.shru Int.mone amount) n)
+      else Eop (Oandimm n) (Eop (Oshrimm amount) (t2:::Enil) ::: Enil)
   | Eop (Oandimm n2) (t2:::Enil) =>
       Eop (Oandimm (Int.and n1 n2)) (t2:::Enil)
   | Eop (Orolm amount2 mask2) (t2:::Enil) =>
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 8ad9807..cc14d33 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.