diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-09-14 16:24:30 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-09-14 16:24:30 +0000 |
commit | 76ea1108be6f8b4ba9dc0118a13f685bcb62bc2b (patch) | |
tree | 8b2dad961e6b368426573e8a217594b9bcb42752 /powerpc/ConstpropOpproof.v | |
parent | 9a0ff6bb768cb0a6e45c1c75727d1cd8199cb89e (diff) | |
download | compcert-76ea1108be6f8b4ba9dc0118a13f685bcb62bc2b.tar.gz compcert-76ea1108be6f8b4ba9dc0118a13f685bcb62bc2b.zip |
Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms
are necessary, only two parameters (default_pl and choose_binop_pl).
SelectDiv: optimize FP division by a power of 2.
ConstpropOp: optimize 2.0 * x and x * 2.0 into x + x.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2326 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/ConstpropOpproof.v')
-rw-r--r-- | powerpc/ConstpropOpproof.v | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index 9d833bf1..b7fad699 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -364,6 +364,33 @@ Proof. econstructor; split; eauto. auto. Qed. +Lemma make_mulfimm_correct: + forall n r1 r2, + rs#r2 = Vfloat n -> + let (op, args) := make_mulfimm n r1 r1 r2 in + exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v. +Proof. + intros; unfold make_mulfimm. + destruct (Float.eq_dec n (Float.floatofint (Int.repr 2))); intros. + simpl. econstructor; split. eauto. rewrite H; subst n. + destruct (rs#r1); simpl; auto. rewrite Float.mul2_add; auto. + simpl. econstructor; split; eauto. +Qed. + +Lemma make_mulfimm_correct_2: + forall n r1 r2, + rs#r1 = Vfloat n -> + let (op, args) := make_mulfimm n r2 r1 r2 in + exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v. +Proof. + intros; unfold make_mulfimm. + destruct (Float.eq_dec n (Float.floatofint (Int.repr 2))); intros. + simpl. econstructor; split. eauto. rewrite H; subst n. + destruct (rs#r2); simpl; auto. rewrite Float.mul2_add; auto. + rewrite Float.mul_commut; auto. + simpl. econstructor; split; eauto. +Qed. + Lemma op_strength_reduction_correct: forall op args vl v, vl = approx_regs app args -> @@ -407,6 +434,11 @@ Proof. 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. +(* mulf *) + inv H0. assert (rs#r2 = Vfloat n2). InvApproxRegs; SimplVMA; auto. + apply make_mulfimm_correct; auto. + inv H0. assert (rs#r1 = Vfloat n1). InvApproxRegs; SimplVMA; auto. + apply make_mulfimm_correct_2; auto. (* default *) exists v; auto. Qed. |