From 336a1f906a9c617e68e9d43e244bf42e9bdbae64 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 9 Apr 2014 13:26:16 +0000 Subject: 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 --- backend/SelectLong.vp | 38 ++++++++++++++++++++++---------------- backend/SelectLongproof.v | 20 ++++---------------- backend/ValueDomain.v | 14 ++++++++++++++ 3 files changed, 40 insertions(+), 32 deletions(-) (limited to 'backend') 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 := -- cgit v1.2.3