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 --- powerpc/ConstpropOp.vp | 24 +++++++++++++++---- powerpc/ConstpropOpproof.v | 54 +++++++++++++++++++++++++++++++++++++++---- powerpc/SelectOp.vp | 57 ++++++++++++++++++++++++++++++++++++++-------- powerpc/SelectOpproof.v | 46 +++++++++++++++++++++++++++++-------- 4 files changed, 153 insertions(+), 28 deletions(-) (limited to 'powerpc') 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)). -- cgit v1.2.3