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, 138 insertions, 86 deletions

diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp
index 172f7a4..b27f405 100644
--- a/ia32/ConstpropOp.vp
+++ b/ia32/ConstpropOp.vp
@@ -44,6 +44,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.
+
 Nondetfunction addr_strength_reduction
                 (addr: addressing) (args: list reg) (vl: list aval) :=
   match addr, args, vl with
@@ -92,20 +109,20 @@ Definition make_addimm (n: int) (r: reg) :=
   then (Omove, r :: nil)
   else (Olea (Aindexed n), r :: nil).
 
-Definition make_shlimm (n: int) (r: reg) :=
-  if Int.eq n Int.zero
-  then (Omove, r :: nil)
-  else (Oshlimm n, r :: nil).
+Definition make_shlimm (n: int) (r1 r2: reg) :=
+  if Int.eq n Int.zero then (Omove, r1 :: nil)
+  else if Int.ltu n Int.iwordsize then (Oshlimm n, r1 :: nil)
+  else (Oshl, r1 :: r2 :: nil).
 
-Definition make_shrimm (n: int) (r: reg) :=
-  if Int.eq n Int.zero
-  then (Omove, r :: nil)
-  else (Oshrimm n, r :: nil).
+Definition make_shrimm (n: int) (r1 r2: reg) :=
+  if Int.eq n Int.zero then (Omove, r1 :: nil)
+  else if Int.ltu n Int.iwordsize then (Oshrimm n, r1 :: nil)
+  else (Oshr, r1 :: r2 :: nil).
 
-Definition make_shruimm (n: int) (r: reg) :=
-  if Int.eq n Int.zero
-  then (Omove, r :: nil)
-  else (Oshruimm n, r :: nil).
+Definition make_shruimm (n: int) (r1 r2: reg) :=
+  if Int.eq n Int.zero then (Omove, r1 :: nil)
+  else if Int.ltu n Int.iwordsize then (Oshruimm n, r1 :: nil)
+  else (Oshru, r1 :: r2 :: nil).
 
 Definition make_mulimm (n: int) (r: reg) :=
   if Int.eq n Int.zero then
@@ -114,7 +131,7 @@ Definition make_mulimm (n: int) (r: reg) :=
     (Omove, r :: nil)
   else
     match Int.is_power2 n with
-    | Some l => make_shlimm l r
+    | Some l => (Oshlimm l, r :: nil)
     | None => (Omulimm n, r :: nil)
     end.
 
@@ -146,7 +163,7 @@ Definition make_divimm n (r1 r2: reg) :=
 
 Definition make_divuimm n (r1 r2: reg) :=
   match Int.is_power2 n with
-  | Some l => make_shruimm l r1
+  | Some l => (Oshruimm l, r1 :: nil)
   | None   => (Odivu, r1 :: r2 :: nil)
   end.
 
@@ -194,16 +211,14 @@ Nondetfunction op_strength_reduction
   | Oor, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_orimm n2 r1
   | Oxor, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_xorimm n1 r2
   | Oxor, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_xorimm n2 r1
-  | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shlimm n2 r1
-  | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrimm n2 r1
-  | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1
+  | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shlimm n2 r1 r2
+  | 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
   | Olea addr, args, vl =>
       let (addr', args') := addr_strength_reduction addr args vl in
       (Olea addr', args')
   | 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/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v
index 6a83c1a..8a05534 100644
--- a/ia32/ConstpropOpproof.v
+++ b/ia32/ConstpropOpproof.v
@@ -160,6 +160,52 @@ Proof.
 - econstructor; eauto.
 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' e##args' m = Some v 
+         /\ Val.lessdef (Val.of_optbool (eval_condition c e##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' e##args' m = Some v 
+         /\ Val.lessdef (Val.of_optbool (eval_condition c e##args m)) v.
+Proof.
+  intros c args vl.
+  assert (Y: forall r, vincl (AE.get r ae) (Uns 1) = true ->
+             e#r = Vundef \/ e#r = Vint Int.zero \/ e#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 (e#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 e#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 (e#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 e#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
@@ -172,36 +218,45 @@ Proof.
 Qed.
   
 Lemma make_shlimm_correct:
-  forall n r1,
-  let (op, args) := make_shlimm n r1 in
+  forall n r1 r2,
+  e#r2 = Vint n ->
+  let (op, args) := make_shlimm n r1 r2 in
   exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.shl e#r1 (Vint n)) v.
 Proof.
   intros; unfold make_shlimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
   exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shl_zero. auto.
+  destruct (Int.ltu n Int.iwordsize). 
   econstructor; split. simpl. eauto. auto.
+  econstructor; split. simpl. eauto. rewrite H; auto.
 Qed.
 
 Lemma make_shrimm_correct:
-  forall n r1,
-  let (op, args) := make_shrimm n r1 in
+  forall n r1 r2,
+  e#r2 = Vint n ->
+  let (op, args) := make_shrimm n r1 r2 in
   exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.shr e#r1 (Vint n)) v.
 Proof.
   intros; unfold make_shrimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
   exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shr_zero. auto.
-  econstructor; split; eauto. simpl. auto.
+  destruct (Int.ltu n Int.iwordsize). 
+  econstructor; split. simpl. eauto. auto.
+  econstructor; split. simpl. eauto. rewrite H; auto.
 Qed.
 
 Lemma make_shruimm_correct:
-  forall n r1,
-  let (op, args) := make_shruimm n r1 in
+  forall n r1 r2,
+  e#r2 = Vint n ->
+  let (op, args) := make_shruimm n r1 r2 in
   exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.shru e#r1 (Vint n)) v.
 Proof.
   intros; unfold make_shruimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
   exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shru_zero. auto.
-  econstructor; split; eauto. simpl. congruence.
+  destruct (Int.ltu n Int.iwordsize). 
+  econstructor; split. simpl. eauto. auto.
+  econstructor; split. simpl. eauto. rewrite H; auto.
 Qed.
 
 Lemma make_mulimm_correct:
@@ -215,7 +270,7 @@ Proof.
   predSpec Int.eq Int.eq_spec n Int.one; intros. subst.
   exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.mul_one; auto.
   destruct (Int.is_power2 n) eqn:?; intros.
-  rewrite (Val.mul_pow2 e#r1 _ _ Heqo). apply make_shlimm_correct; auto. 
+  rewrite (Val.mul_pow2 e#r1 _ _ Heqo). econstructor; split. simpl; eauto. auto.
   econstructor; split; eauto. auto. 
 Qed.
 
@@ -243,9 +298,8 @@ Lemma make_divuimm_correct:
 Proof.
   intros; unfold make_divuimm.
   destruct (Int.is_power2 n) eqn:?.
-  replace v with (Val.shru e#r1 (Vint i)). 
-  eapply make_shruimm_correct; eauto.
-  eapply Val.divu_pow2; eauto. congruence.
+  econstructor; split. simpl; eauto. 
+  rewrite H0 in H. erewrite Val.divu_pow2 by eauto. auto.
   exists v; auto.
 Qed.
 
@@ -466,9 +520,7 @@ Proof.
 (* singleoffloat *)
   InvApproxRegs; SimplVM; inv H0. apply make_singleoffloat_correct; auto.
 (* cond *)
-  generalize (cond_strength_reduction_correct c args0 vl0 H). 
-  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) e#r2).
diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp
index 5f47df2..e82d0a3 100644
--- a/ia32/SelectOp.vp
+++ b/ia32/SelectOp.vp
@@ -144,39 +144,48 @@ Definition shift_is_scale (n: int) : bool :=
   Int.eq n (Int.repr 1) || Int.eq n (Int.repr 2) || Int.eq n (Int.repr 3).
 
 Nondetfunction shlimm (e1: expr) (n: int) :=
-  if Int.eq n Int.zero then e1 else
-  match e1 with
-  | Eop (Ointconst n1) Enil =>
-      Eop (Ointconst(Int.shl n1 n)) Enil
-  | Eop (Oshlimm n1) (t1:::Enil) =>
-      if Int.ltu (Int.add n n1) Int.iwordsize
-      then Eop (Oshlimm (Int.add n n1)) (t1:::Enil)
-      else Eop (Oshlimm n) (e1:::Enil)
-  | Eop (Olea (Aindexed n1)) (t1:::Enil) =>
-      if shift_is_scale n
-      then Eop (Olea (Ascaled (Int.shl Int.one n) (Int.shl n1 n))) (t1:::Enil)
-      else Eop (Oshlimm n) (e1:::Enil)
-  | _ =>
-      if shift_is_scale n
-      then Eop (Olea (Ascaled (Int.shl Int.one n) Int.zero)) (e1:::Enil)
-      else Eop (Oshlimm n) (e1:::Enil)
-  end.
+  if Int.eq n Int.zero then e1
+  if negb (Int.ltu n Int.iwordsize) then
+    Eop Oshl (e1:::Eop (Ointconst n):::Enil)
+  else
+    match e1 with
+    | Eop (Ointconst n1) Enil =>
+        Eop (Ointconst(Int.shl n1 n)) Enil
+    | Eop (Oshlimm n1) (t1:::Enil) =>
+        if Int.ltu (Int.add n n1) Int.iwordsize
+        then Eop (Oshlimm (Int.add n n1)) (t1:::Enil)
+        else Eop (Oshlimm n) (e1:::Enil)
+    | Eop (Olea (Aindexed n1)) (t1:::Enil) =>
+        if shift_is_scale n
+        then Eop (Olea (Ascaled (Int.shl Int.one n) (Int.shl n1 n))) (t1:::Enil)
+        else Eop (Oshlimm n) (e1:::Enil)
+    | _ =>
+        if shift_is_scale n
+        then Eop (Olea (Ascaled (Int.shl Int.one n) Int.zero)) (e1:::Enil)
+        else Eop (Oshlimm n) (e1:::Enil)
+    end.
 
 Nondetfunction shruimm (e1: expr) (n: int) :=
   if Int.eq n Int.zero then e1 else
-  match e1 with
-  | Eop (Ointconst n1) Enil =>
-      Eop (Ointconst(Int.shru n1 n)) Enil
-  | Eop (Oshruimm n1) (t1:::Enil) =>
-      if Int.ltu (Int.add n n1) Int.iwordsize
-      then Eop (Oshruimm (Int.add n n1)) (t1:::Enil)
-      else Eop (Oshruimm n) (e1:::Enil)
-  | _ =>
-      Eop (Oshruimm n) (e1:::Enil)
-  end.
+  if negb (Int.ltu n Int.iwordsize) then
+    Eop Oshru (e1:::Eop (Ointconst n):::Enil)
+  else
+    match e1 with
+    | Eop (Ointconst n1) Enil =>
+        Eop (Ointconst(Int.shru n1 n)) Enil
+    | Eop (Oshruimm n1) (t1:::Enil) =>
+        if Int.ltu (Int.add n n1) Int.iwordsize
+        then Eop (Oshruimm (Int.add n n1)) (t1:::Enil)
+        else Eop (Oshruimm n) (e1:::Enil)
+    | _ =>
+        Eop (Oshruimm n) (e1:::Enil)
+    end.
 
 Nondetfunction shrimm (e1: expr) (n: int) :=
   if Int.eq n Int.zero then e1 else
+  if negb (Int.ltu n Int.iwordsize) then
+    Eop Oshr (e1:::Eop (Ointconst n):::Enil)
+  else
   match e1 with
   | Eop (Ointconst n1) Enil =>
       Eop (Ointconst(Int.shr n1 n)) Enil
@@ -337,18 +346,6 @@ Definition addf (e1 e2: expr) :=  Eop Oaddf (e1 ::: e2 ::: Enil).
 Definition subf (e1 e2: expr) :=  Eop Osubf (e1 ::: e2 ::: Enil).
 Definition mulf (e1 e2: expr) :=  Eop Omulf (e1 ::: e2 ::: Enil).
 
-Definition divfimm (e: expr) (n: float) :=
-  match Float.exact_inverse n with
-  | Some n' => Eop Omulf (e ::: Eop (Ofloatconst n') Enil ::: Enil)
-  | None    => Eop Odivf (e ::: Eop (Ofloatconst n) Enil ::: Enil)
-  end.
-
-Nondetfunction divf (e1: expr) (e2: expr) :=
-  match e2 with
-  | Eop (Ofloatconst n2) Enil => divfimm e1 n2
-  | _ => Eop Odivf (e1 ::: e2 ::: Enil)
-  end.
-
 (** ** Comparisons *)
 
 Nondetfunction compimm (default: comparison -> int -> condition)
diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v
index 30e8c5b..16879c0 100644
--- a/ia32/SelectOpproof.v
+++ b/ia32/SelectOpproof.v
@@ -565,18 +565,6 @@ Proof.
   red; intros; TrivialExists.
 Qed.
 
-Theorem eval_divf: binary_constructor_sound divf Val.divf.
-Proof.
-  red. intros until y. unfold divf. destruct (divf_match b); intros.
-- unfold divfimm. destruct (Float.exact_inverse n2) as [n2' | ] eqn:EINV.
-  + inv H0. inv H4. simpl in H6. inv H6. econstructor; split.
-    EvalOp. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. 
-    simpl; eauto. 
-    destruct x; simpl; auto. erewrite Float.div_mul_inverse; eauto. 
-  + TrivialExists. 
-- TrivialExists.
-Qed.
-
 Section COMP_IMM.
 
 Variable default: comparison -> int -> condition.