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 --- arm/ConstpropOp.vp | 20 ++++++++++++++++++-- arm/ConstpropOpproof.v | 50 +++++++++++++++++++++++++++++++++++++++++++++++--- arm/SelectOp.vp | 43 ++++++++++++++++++++++++++++++++++++------- arm/SelectOpproof.v | 49 ++++++++++++++++++++++++++++++++++++------------- 4 files changed, 137 insertions(+), 25 deletions(-) (limited to 'arm') diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp index bf08610..2b658a4 100644 --- a/arm/ConstpropOp.vp +++ b/arm/ConstpropOp.vp @@ -74,6 +74,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) @@ -191,8 +208,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/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index 90e18f2..7cf5879 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -126,6 +126,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 @@ -416,9 +462,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/arm/SelectOp.vp b/arm/SelectOp.vp index 43745ca..efd9e48 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -58,9 +58,11 @@ Definition addrstack (ofs: int) := Nondetfunction notint (e: expr) := match e with + | Eop (Ointconst n) Enil => Eop (Ointconst (Int.not n)) Enil | Eop (Oshift s) (t1:::Enil) => Eop (Onotshift s) (t1:::Enil) | Eop Onot (t1:::Enil) => t1 | Eop (Onotshift s) (t1:::Enil) => Eop (Oshift s) (t1:::Enil) + | Eop (Oxorimm n) (t1:::Enil) => Eop (Oxorimm (Int.not n)) (t1:::Enil) | _ => Eop Onot (e:::Enil) end. @@ -93,6 +95,14 @@ Nondetfunction add (e1: expr) (e2: expr) := (** ** Integer and pointer subtraction *) +Nondetfunction rsubimm (n: int) (e: expr) := + match e with + | Eop (Ointconst m) Enil => Eop (Ointconst (Int.sub n m)) Enil + | Eop (Oaddimm m) (t:::Enil) => Eop (Orsubimm (Int.sub n m)) (t:::Enil) + | Eop (Orsubimm m) (t:::Enil) => Eop (Oaddimm (Int.sub n m)) (t:::Enil) + | _ => Eop (Orsubimm n) (e:::Enil) + end. + Nondetfunction sub (e1: expr) (e2: expr) := match e1, e2 with | t1, Eop (Ointconst n2) Enil => addimm (Int.neg n2) t1 @@ -102,13 +112,13 @@ Nondetfunction sub (e1: expr) (e2: expr) := addimm n1 (Eop Osub (t1:::t2:::Enil)) | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil)) - | Eop (Ointconst n1) Enil, t2 => Eop (Orsubimm n1) (t2:::Enil) + | Eop (Ointconst n1) Enil, t2 => rsubimm n1 t2 | Eop (Oshift s) (t1:::Enil), t2 => Eop (Orsubshift s) (t2:::t1:::Enil) | t1, Eop (Oshift s) (t2:::Enil) => Eop (Osubshift s) (t1:::t2:::Enil) | _, _ => Eop Osub (e1:::e2:::Enil) end. -Definition negint (e: expr) := Eop (Orsubimm Int.zero) (e ::: Enil). +Definition negint (e: expr) := rsubimm Int.zero e. (** ** Immediate shifts *) @@ -247,9 +257,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. @@ -315,7 +327,6 @@ Definition absf (e: expr) := Eop Oabsf (e ::: Enil). 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 divf (e1 e2: expr) := Eop Odivf (e1 ::: e2 ::: Enil). (** ** Comparisons *) @@ -370,19 +381,37 @@ 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 *) Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil). Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). Definition intuoffloat (e: expr) := Eop Ointuoffloat (e ::: Enil). -Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil). -Definition floatofintu (e: expr) := Eop Ofloatofintu (e ::: Enil). + +Nondetfunction floatofint (e: expr) := + match e with + | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.floatofint n)) Enil + | _ => Eop Ofloatofint (e ::: Enil) + end. + +Nondetfunction floatofintu (e: expr) := + match e with + | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.floatofintu n)) Enil + | _ => Eop Ofloatofintu (e ::: Enil) + end. (** ** Recognition of addressing modes for load and store operations *) diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index 9fbab44..d10e7fc 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -133,9 +133,11 @@ Qed. Theorem eval_notint: unary_constructor_sound notint Val.notint. Proof. unfold notint; red; intros until x; case (notint_match a); intros; InvEval. + TrivialExists. subst x. TrivialExists. exists v1; split; auto. subst. destruct v1; simpl; auto. rewrite Int.not_involutive; auto. exists (eval_shift s v1); split. EvalOp. subst x. destruct (eval_shift s v1); simpl; auto. rewrite Int.not_involutive; auto. + subst x. rewrite Val.not_xor. rewrite Val.xor_assoc. TrivialExists. TrivialExists. Qed. @@ -177,6 +179,20 @@ Proof. TrivialExists. Qed. +Theorem eval_rsubimm: forall n, unary_constructor_sound (rsubimm n) (fun v => Val.sub (Vint n) v). +Proof. + red; intros until x. unfold rsubimm; case (rsubimm_match a); intros. + InvEval. TrivialExists. + InvEval. subst x. econstructor; split. EvalOp. unfold eval_operation; eauto. + destruct v1; simpl; auto. rewrite Int.sub_add_r. rewrite <- Int.sub_add_opp. + auto. + InvEval. subst x. econstructor; split. EvalOp. simpl; eauto. + fold (Val.sub (Vint m0) v1). destruct v1; simpl; auto. + rewrite ! Int.sub_add_opp. rewrite Int.neg_add_distr. rewrite Int.neg_involutive. + rewrite (Int.add_permut i). rewrite (Int.add_commut i). auto. + TrivialExists. +Qed. + Theorem eval_sub: binary_constructor_sound sub Val.sub. Proof. red; intros until y. @@ -187,7 +203,7 @@ Proof. apply eval_addimm; EvalOp. subst. rewrite Val.sub_add_l. apply eval_addimm; EvalOp. subst. rewrite Val.sub_add_r. apply eval_addimm; EvalOp. - TrivialExists. + apply eval_rsubimm; auto. subst. TrivialExists. subst. TrivialExists. TrivialExists. @@ -195,7 +211,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_rsubimm; auto. Qed. Theorem eval_shlimm: @@ -426,9 +442,13 @@ Proof. predSpec Int.eq Int.eq_spec n Int.zero. intros. exists x; split. auto. destruct x; simpl; auto. subst n. rewrite Int.xor_zero. auto. - destruct (xorimm_match a); intros; InvEval. + predSpec Int.eq Int.eq_spec n Int.mone. + intros. subst n. rewrite <- Val.not_xor. apply eval_notint; auto. + intros. 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. rewrite Val.not_xor. rewrite Val.xor_assoc. + rewrite (Val.xor_commut (Vint Int.mone)). TrivialExists. TrivialExists. Qed. @@ -614,11 +634,6 @@ Proof. red; intros; TrivialExists. Qed. -Theorem eval_divf: binary_constructor_sound divf Val.divf. -Proof. - red; intros; TrivialExists. -Qed. - Section COMP_IMM. Variable default: comparison -> int -> condition. @@ -716,7 +731,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; case (cast8signed_match a); intros. + InvEval. TrivialExists. + TrivialExists. Qed. Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8). @@ -727,7 +744,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; case (cast16signed_match a); intros. + InvEval. TrivialExists. + TrivialExists. Qed. Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16). @@ -756,7 +775,9 @@ 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; unfold floatofint. TrivialExists. + intros until y; unfold floatofint. case (floatofint_match a); intros. + InvEval. simpl in H0. TrivialExists. + TrivialExists. Qed. Theorem eval_intuoffloat: @@ -774,7 +795,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; unfold floatofintu. TrivialExists. + intros until y; unfold floatofintu. case (floatofintu_match a); intros. + InvEval. simpl in H0. TrivialExists. + TrivialExists. Qed. Theorem eval_addressing: -- cgit v1.2.3