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/ConstpropOpproof.v | 82 ++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 67 insertions(+), 15 deletions(-) (limited to 'ia32/ConstpropOpproof.v') diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v index 6a83c1a1..8a055342 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). -- cgit