Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons over booleans.

Select*: more systematic constant propagation; don't CP shifts by amounts outside of [0..31].
Driver: timer for whole compilation.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2452 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

4 files changed, 153 insertions, 28 deletions

diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index 6aa0925..e1e1960 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -46,6 +46,23 @@ Nondetfunction cond_strength_reduction
       (cond, args)
   end.
 
+Definition make_cmp_base (c: condition) (args: list reg) (vl: list aval) :=
+  let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args').
+
+Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) :=
+  match c, args, vl with
+  | Ccompimm Ceq n, r1 :: nil, v1 :: nil =>
+      if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Omove, r1 :: nil)
+      else if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil)
+      else make_cmp_base c args vl
+  | Ccompimm Cne n, r1 :: nil, v1 :: nil =>
+      if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Omove, r1 :: nil)
+      else if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil)
+      else make_cmp_base c args vl
+  | _, _, _ =>
+      make_cmp_base c args vl
+  end.
+
 Definition make_addimm (n: int) (r: reg) :=
   if Int.eq n Int.zero
   then (Omove, r :: nil)
@@ -114,8 +131,8 @@ Definition make_orimm (n: int) (r: reg) :=
   else (Oorimm n, r :: nil).
 
 Definition make_xorimm (n: int) (r: reg) :=
-  if Int.eq n Int.zero
-  then (Omove, r :: nil)
+  if Int.eq n Int.zero then (Omove, r :: nil)
+  else if Int.eq n Int.mone then (Onot, r :: nil)
   else (Oxorimm n, r :: nil).
 
 Definition make_mulfimm (n: float) (r r1 r2: reg) :=
@@ -158,8 +175,7 @@ Nondetfunction op_strength_reduction
   | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrimm n2 r1 r2
   | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1 r2
   | Osingleoffloat, r1 :: nil, v1 :: nil => make_singleoffloat r1 v1
-  | Ocmp c, args, vl =>
-      let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args')
+  | Ocmp c, args, vl => make_cmp c args vl
   | Omulf, r1 :: r2 :: nil, v1 :: F n2 :: nil => make_mulfimm n2 r1 r1 r2
   | Omulf, r1 :: r2 :: nil, F n1 :: v2 :: nil => make_mulfimm n1 r2 r1 r2
   | _, _, _ => (op, args)
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index 0c88246..a28d908 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -106,6 +106,52 @@ Proof.
 - auto.
 Qed.
 
+Lemma make_cmp_base_correct:
+  forall c args vl,
+  vl = map (fun r => AE.get r ae) args ->
+  let (op', args') := make_cmp_base c args vl in
+  exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v 
+         /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v.
+Proof.
+  intros. unfold make_cmp_base. 
+  generalize (cond_strength_reduction_correct c args vl H). 
+  destruct (cond_strength_reduction c args vl) as [c' args']. intros EQ.
+  econstructor; split. simpl; eauto. rewrite EQ. auto. 
+Qed.
+
+Lemma make_cmp_correct:
+  forall c args vl,
+  vl = map (fun r => AE.get r ae) args ->
+  let (op', args') := make_cmp c args vl in
+  exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v 
+         /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v.
+Proof.
+  intros c args vl.
+  assert (Y: forall r, vincl (AE.get r ae) (Uns 1) = true ->
+             rs#r = Vundef \/ rs#r = Vint Int.zero \/ rs#r = Vint Int.one).
+  { intros. apply vmatch_Uns_1 with bc. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. }
+  unfold make_cmp. case (make_cmp_match c args vl); intros.
+- destruct (Int.eq_dec n Int.one && vincl v1 (Uns 1)) eqn:E1.
+  simpl in H; inv H. InvBooleans. subst n. 
+  exists (rs#r1); split; auto. simpl.
+  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+  destruct (Int.eq_dec n Int.zero && vincl v1 (Uns 1)) eqn:E0.
+  simpl in H; inv H. InvBooleans. subst n. 
+  exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl.
+  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+  apply make_cmp_base_correct; auto.
+- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns 1)) eqn:E0.
+  simpl in H; inv H. InvBooleans. subst n. 
+  exists (rs#r1); split; auto. simpl.
+  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+  destruct (Int.eq_dec n Int.one && vincl v1 (Uns 1)) eqn:E1.
+  simpl in H; inv H. InvBooleans. subst n. 
+  exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl.
+  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+  apply make_cmp_base_correct; auto.
+- apply make_cmp_base_correct; auto.
+Qed.
+
 Lemma make_addimm_correct:
   forall n r,
   let (op, args) := make_addimm n r in
@@ -256,7 +302,9 @@ Lemma make_xorimm_correct:
 Proof.
   intros; unfold make_xorimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
-  subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.xor_zero; auto.
+  subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.xor_zero; auto. 
+  predSpec Int.eq Int.eq_spec n Int.mone; intros.
+  subst n. exists (Val.notint rs#r); split; auto. 
   econstructor; split; eauto. auto. 
 Qed.
 
@@ -379,9 +427,7 @@ Proof.
 (* singleoffloat *)
   InvApproxRegs; SimplVM; inv H0. apply make_singleoffloat_correct; auto.
 (* cmp *)
-  generalize (cond_strength_reduction_correct c args0 vl0). 
-  destruct (cond_strength_reduction c args0 vl0) as [c' args']; intros.
-  rewrite <- H1 in H0; auto. econstructor; split; eauto.
+  inv H0. apply make_cmp_correct; auto.
 (* mulf *)
   InvApproxRegs; SimplVM; inv H0. rewrite <- H2. apply make_mulfimm_correct; auto.
   InvApproxRegs; SimplVM; inv H0. fold (Val.mulf (Vfloat n1) rs#r2).
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index ad4f3b9..371a08a 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -68,6 +68,7 @@ Nondetfunction notint (e: expr) :=
   | Eop Onxor (t1:::t2:::Enil) => Eop Oxor (t1:::t2:::Enil)
   | Eop Oandc (t1:::t2:::Enil) => Eop Oorc (t2:::t1:::Enil)
   | Eop Oorc (t1:::t2:::Enil) => Eop Oandc (t2:::t1:::Enil)
+  | Eop (Oxorimm n) (t1:::Enil) => Eop (Oxorimm (Int.not n)) (t1:::Enil)
   | _ => Eop Onot (e:::Enil)
   end.
 
@@ -121,10 +122,22 @@ Nondetfunction add (e1: expr) (e2: expr) :=
 
 (** ** Integer and pointer subtraction *)
 
+Nondetfunction subimm (n1: int) (e: expr) :=
+  match e with
+  | Eop (Ointconst n2) Enil =>
+      Eop (Ointconst (Int.sub n1 n2)) Enil
+  | Eop (Oaddimm n2) (t2:::Enil) =>
+      Eop (Osubimm (Int.sub n1 n2)) (t2 ::: Enil)
+  | _ =>
+      Eop (Osubimm n1) (e ::: Enil)
+  end.
+
 Nondetfunction sub (e1: expr) (e2: expr) :=
   match e1, e2 with
   | t1, Eop (Ointconst n2) Enil =>
       addimm (Int.neg n2) t1
+  | Eop (Ointconst n1) Enil, t2 =>
+      subimm n1 t2
   | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) =>
       addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil))
   | Eop (Oaddimm n1) (t1:::Enil), t2 =>
@@ -135,7 +148,7 @@ Nondetfunction sub (e1: expr) (e2: expr) :=
       Eop Osub (e1:::e2:::Enil)
   end.
 
-Definition negint (e: expr) := Eop (Osubimm Int.zero) (e ::: Enil).
+Definition negint (e: expr) := subimm Int.zero e.
 
 (** ** Rotates and immediate shifts *)
 
@@ -174,8 +187,12 @@ Definition shruimm (e1: expr) (n2: int) :=
 Nondetfunction shrimm (e1: expr) (n2: int) :=
   if Int.eq n2 Int.zero then
     e1
+  else if negb (Int.ltu n2 Int.iwordsize) then
+    Eop Oshr (e1:::Eop (Ointconst n2) Enil:::Enil)
   else
     match e1 with
+    | Eop (Ointconst n1) Enil =>
+        Eop (Ointconst (Int.shr n1 n2)) Enil
     | Eop (Oandimm mask1) (t1:::Enil) =>
         if Int.lt mask1 Int.zero
         then Eop (Oshrimm n2) (e1:::Enil)
@@ -293,9 +310,11 @@ Nondetfunction or (e1: expr) (e2: expr) :=
 
 Nondetfunction xorimm (n1: int) (e2: expr) :=
   if Int.eq n1 Int.zero then e2 else
+  if Int.eq n1 Int.mone then notint e2 else
   match e2 with
   | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.xor n1 n2)) Enil
   | Eop (Oxorimm n2) (t2:::Enil) => Eop (Oxorimm (Int.xor n1 n2)) (t2:::Enil)
+  | Eop Onot (t2:::Enil) => Eop (Oxorimm (Int.not n1)) (t2:::Enil)
   | _ => Eop (Oxorimm n1) (e2:::Enil)
   end.
 
@@ -418,11 +437,19 @@ Definition compf (c: comparison) (e1: expr) (e2: expr) :=
 
 Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e.
 
-Definition cast8signed (e: expr) := Eop Ocast8signed (e ::: Enil).
+Nondetfunction cast8signed (e: expr) :=
+  match e with
+  | Eop (Ointconst n) Enil => Eop (Ointconst (Int.sign_ext 8 n)) Enil
+  | _ => Eop Ocast8signed (e ::: Enil)
+  end.
 
 Definition cast16unsigned (e: expr) := andimm (Int.repr 65535) e.
 
-Definition cast16signed (e: expr) := Eop Ocast16signed (e ::: Enil).
+Nondetfunction cast16signed (e: expr) :=
+  match e with
+  | Eop (Ointconst n) Enil => Eop (Ointconst (Int.sign_ext 16 n)) Enil
+  | _ => Eop Ocast16signed (e ::: Enil)
+  end.
 
 (** ** Floating-point conversions *)
 
@@ -435,14 +462,24 @@ Definition intuoffloat (e: expr) :=
       (intoffloat (Eletvar 1))
       (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat.
 
-Definition floatofintu (e: expr) :=
-  subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil))
-       (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil).
+Nondetfunction floatofintu (e: expr) :=
+  match e with
+  | Eop (Ointconst n) Enil =>
+      Eop (Ofloatconst (Float.floatofintu n)) Enil
+  | _ =>
+      subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil))
+           (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil)
+  end.
 
-Definition floatofint (e: expr) :=
-  subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil
-                           ::: addimm Float.ox8000_0000 e ::: Enil))
-       (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil).
+Nondetfunction floatofint (e: expr) :=
+  match e with
+  | Eop (Ointconst n) Enil =>
+      Eop (Ofloatconst (Float.floatofint n)) Enil
+  | _ =>
+      subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil
+                               ::: addimm Float.ox8000_0000 e ::: Enil))
+           (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil)
+  end.
 
 Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil).
 
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 4d26cf6..b6412c0 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -150,6 +150,7 @@ Proof.
   subst. exists (Val.and v0 (Val.notint v1)); split. EvalOp. 
     destruct v0; destruct v1; simpl; auto. rewrite Int.not_or_and_not. rewrite Int.not_involutive.
     rewrite Int.and_commut. auto.
+  subst x. TrivialExists. simpl. rewrite Val.not_xor. rewrite Val.xor_assoc. auto.
   TrivialExists. 
 Qed.
 
@@ -218,11 +219,23 @@ Proof.
 - TrivialExists. 
 Qed.
 
+Theorem eval_subimm:
+  forall n, unary_constructor_sound (subimm n) (fun v => Val.sub (Vint n) v).
+Proof.
+  intros; red; intros until x. unfold subimm. destruct (subimm_match a); intros.
+  InvEval. TrivialExists. 
+  InvEval. subst x. TrivialExists. unfold eval_operation. destruct v1; simpl; auto.
+  rewrite ! Int.sub_add_opp. rewrite Int.add_assoc. f_equal. f_equal. f_equal.
+  rewrite Int.neg_add_distr.  apply Int.add_commut.
+  TrivialExists.
+Qed.
+
 Theorem eval_sub: binary_constructor_sound sub Val.sub.
 Proof.
   red; intros until y.
   unfold sub; case (sub_match a b); intros; InvEval.
   rewrite Val.sub_add_opp. apply eval_addimm; auto.
+  apply eval_subimm; auto.
   subst. rewrite Val.sub_add_l. rewrite Val.sub_add_r. 
     rewrite Val.add_assoc. simpl. rewrite Int.add_commut. rewrite <- Int.sub_add_opp.
     apply eval_addimm; EvalOp.
@@ -233,7 +246,7 @@ Qed.
 
 Theorem eval_negint: unary_constructor_sound negint (fun v => Val.sub Vzero v).
 Proof.
-  red; intros. unfold negint. TrivialExists.
+  red; intros. unfold negint. apply eval_subimm; auto. 
 Qed.
 
 Lemma eval_rolm:
@@ -280,15 +293,19 @@ 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.
+  destruct (Int.ltu n Int.iwordsize) eqn:WS.
   case (shrimm_match a); intros.
-  destruct (Int.lt mask1 Int.zero) eqn:?. 
+  InvEval. exists (Vint (Int.shr n1 n)); split. EvalOp. simpl; rewrite WS; auto.
+  simpl; destruct (Int.lt mask1 Int.zero) 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. 
+  destruct x; simpl; auto. rewrite WS.
   decEq. symmetry. InvEval. destruct v1; simpl in H0; inv H0. 
   apply Int.shr_and_is_shru_and; auto.
-  TrivialExists.
+  simpl. TrivialExists.
+  intros. simpl. TrivialExists.
+  constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. auto.
 Qed.
 
 Lemma eval_mulimm_base:
@@ -475,7 +492,9 @@ Proof.
   intros. subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.xor_zero; auto.
   clear H. destruct (xorimm_match a); intros; InvEval.
   TrivialExists. simpl. rewrite Int.xor_commut; auto.
-  subst. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. TrivialExists. 
+  subst. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. TrivialExists.
+  subst x. TrivialExists. simpl. rewrite Val.not_xor. rewrite Val.xor_assoc. 
+  simpl. rewrite Int.xor_commut; auto.
   TrivialExists.
 Qed.
 
@@ -735,7 +754,9 @@ Qed.
 
 Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8).
 Proof.
-  red; intros. unfold cast8signed. TrivialExists.
+  red; intros until x. unfold cast8signed. destruct (cast8signed_match a); intros.
+  InvEval; TrivialExists.
+  TrivialExists.
 Qed.
 
 Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8).
@@ -746,7 +767,9 @@ Qed.
 
 Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16).
 Proof.
-  red; intros. unfold cast16signed. TrivialExists.
+  red; intros until x. unfold cast16signed. destruct (cast16signed_match a); intros.
+  InvEval; TrivialExists.
+  TrivialExists.
 Qed.
 
 Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16).
@@ -813,9 +836,10 @@ Theorem eval_floatofint:
   Val.floatofint x = Some y ->
   exists v, eval_expr ge sp e m le (floatofint a) v /\ Val.lessdef y v.
 Proof.
-  intros. destruct x; simpl in H0; inv H0.
+  intros until y. unfold floatofint. destruct (floatofint_match a); intros.
+  InvEval. TrivialExists. 
+  rename e0 into a. destruct x; simpl in H0; inv H0.
   exists (Vfloat (Float.floatofint i)); split; auto.
-  unfold floatofint.
   set (t1 := addimm Float.ox8000_0000 a).
   set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: t1 ::: Enil)).
   set (t3 := Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil).
@@ -834,7 +858,9 @@ Theorem eval_floatofintu:
   Val.floatofintu x = Some y ->
   exists v, eval_expr ge sp e m le (floatofintu a) v /\ Val.lessdef y v.
 Proof.
-  intros. destruct x; simpl in H0; inv H0.
+  intros until y. unfold floatofintu. destruct (floatofintu_match a); intros.
+  InvEval. TrivialExists.
+  rename e0 into a. destruct x; simpl in H0; inv H0.
   exists (Vfloat (Float.floatofintu i)); split; auto.
   unfold floatofintu.
   set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: a ::: Enil)).