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

3 files changed, 40 insertions, 32 deletions

diff --git a/backend/SelectLong.vp b/backend/SelectLong.vp
index 09f29af..0c1cbb3 100644
--- a/backend/SelectLong.vp
+++ b/backend/SelectLong.vp
@@ -27,10 +27,10 @@ Open Local Scope cminorsel_scope.
   the names of these functions. *)
 
 Record helper_functions : Type := mk_helper_functions {
-  i64_dtos: ident;                      (**r float -> signed long *)
-  i64_dtou: ident;                      (**r float -> unsigned long *)
-  i64_stod: ident;                      (**r signed long -> float *)
-  i64_utod: ident;                      (**r unsigned long -> float *)
+  i64_dtos: ident;                      (**r float64 -> signed long *)
+  i64_dtou: ident;                      (**r float64 -> unsigned long *)
+  i64_stod: ident;                      (**r signed long -> float64 *)
+  i64_utod: ident;                      (**r unsigned long -> float64 *)
   i64_stof: ident;                      (**r signed long -> float32 *)
   i64_utof: ident;                      (**r unsigned long -> float32 *)
   i64_neg: ident;                       (**r opposite *)
@@ -304,13 +304,16 @@ Definition cmplu_gen (ch cl: comparison) (e1 e2: expr) :=
 Definition cmplu (c: comparison) (e1 e2: expr) :=
   match c with
   | Ceq =>
-      if is_longconst_zero e2
-      then cmpl_eq_zero e1
-      else cmpl_eq_zero (xorl e1 e2)
+      cmpl_eq_zero (xorl e1 e2)
+(*
+        (if is_longconst_zero e2 then e1
+         else if is_longconst_zero e1 then e2
+         else xorl e1 e2) *)
   | Cne =>
-      if is_longconst_zero e2
-      then cmpl_ne_zero e1
-      else cmpl_ne_zero (xorl e1 e2)
+      cmpl_ne_zero (xorl e1 e2)
+(*        (if is_longconst_zero e2 then e1
+         else if is_longconst_zero e1 then e2
+         else xorl e1 e2) *)
   | Clt =>
       cmplu_gen Clt Clt e1 e2
   | Cle =>
@@ -330,13 +333,16 @@ Definition cmpl_gen (ch cl: comparison) (e1 e2: expr) :=
 Definition cmpl (c: comparison) (e1 e2: expr) :=
   match c with
   | Ceq =>
-      if is_longconst_zero e2
-      then cmpl_eq_zero e1
-      else cmpl_eq_zero (xorl e1 e2)
+      cmpl_eq_zero (xorl e1 e2)
+(*
+        (if is_longconst_zero e2 then e1
+         else if is_longconst_zero e1 then e2
+         else xorl e1 e2) *)
   | Cne =>
-      if is_longconst_zero e2
-      then cmpl_ne_zero e1
-      else cmpl_ne_zero (xorl e1 e2)
+      cmpl_ne_zero (xorl e1 e2)
+(*        (if is_longconst_zero e2 then e1
+         else if is_longconst_zero e1 then e2
+         else xorl e1 e2) *)
   | Clt =>
       if is_longconst_zero e2
       then comp Clt (highlong e1) (Eop (Ointconst Int.zero) Enil)
diff --git a/backend/SelectLongproof.v b/backend/SelectLongproof.v
index 26f33da..ec0dd2c 100644
--- a/backend/SelectLongproof.v
+++ b/backend/SelectLongproof.v
@@ -1024,16 +1024,10 @@ Proof.
   rename i into x. rename i0 into y.
   destruct c; simpl.
 - (* Ceq *)
-  destruct (is_longconst_zero b) eqn:LC.
-+ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0.
-  apply eval_cmpl_eq_zero; auto.
-+ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B. inv B.
+  exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B. inv B.
   rewrite int64_eq_xor. apply eval_cmpl_eq_zero; auto.  
 - (* Cne *)
-  destruct (is_longconst_zero b) eqn:LC.
-+ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0.
-  apply eval_cmpl_ne_zero; auto.
-+ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B. inv B.
+  exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B. inv B.
   rewrite int64_eq_xor. apply eval_cmpl_ne_zero; auto.  
 - (* Clt *)
   exploit (eval_cmplu_gen Clt Clt). eexact H. eexact H0. simpl.
@@ -1095,16 +1089,10 @@ Proof.
   rename i into x. rename i0 into y.
   destruct c; simpl.
 - (* Ceq *)
-  destruct (is_longconst_zero b) eqn:LC.
-+ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0.
-  apply eval_cmpl_eq_zero; auto.
-+ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B; inv B.
+  exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B; inv B.
   rewrite int64_eq_xor. apply eval_cmpl_eq_zero; auto.
 - (* Cne *)
-  destruct (is_longconst_zero b) eqn:LC.
-+ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0.
-  apply eval_cmpl_ne_zero; auto.
-+ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B; inv B.
+  exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B; inv B.
   rewrite int64_eq_xor. apply eval_cmpl_ne_zero; auto.
 - (* Clt *)
   destruct (is_longconst_zero b) eqn:LC.
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 239dd47..2ece8cd 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -681,6 +681,14 @@ Qed.
 
 Hint Resolve is_uns_mon is_sgn_mon is_uns_sgn is_uns_usize is_sgn_ssize : va.
 
+Lemma is_uns_1:
+  forall n, is_uns 1 n -> n = Int.zero \/ n = Int.one.
+Proof.
+  intros. destruct (Int.testbit n 0) eqn:B0; [right|left]; apply Int.same_bits_eq; intros.
+  rewrite Int.bits_one. destruct (zeq i 0). subst i; auto. apply H; omega. 
+  rewrite Int.bits_zero. destruct (zeq i 0). subst i; auto. apply H; omega.
+Qed.
+
 (** Smart constructors for [Uns] and [Sgn]. *)
 
 Definition uns (n: Z) : aval :=
@@ -749,6 +757,12 @@ Qed.
 
 Hint Resolve vmatch_uns vmatch_uns_undef vmatch_sgn vmatch_sgn_undef : va.
 
+Lemma vmatch_Uns_1:
+  forall v, vmatch v (Uns 1) -> v = Vundef \/ v = Vint Int.zero \/ v = Vint Int.one.
+Proof.
+  intros. inv H; auto. right. exploit is_uns_1; eauto. intuition congruence.
+Qed.
+
 (** Ordering *)
 
 Inductive vge: aval -> aval -> Prop :=