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 --- ia32/ConstpropOp.vp | 55 +++++++++++++++++++++------------ ia32/ConstpropOpproof.v | 82 ++++++++++++++++++++++++++++++++++++++++--------- ia32/SelectOp.vp | 75 ++++++++++++++++++++++---------------------- ia32/SelectOpproof.v | 12 -------- 4 files changed, 138 insertions(+), 86 deletions(-) (limited to 'ia32') 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. -- cgit v1.2.3