From 76ea1108be6f8b4ba9dc0118a13f685bcb62bc2b Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 14 Sep 2013 16:24:30 +0000 Subject: 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 --- ia32/ConstpropOp.vp | 13 ++++++++++--- ia32/ConstpropOpproof.v | 36 ++++++++++++++++++++++++++++++++++++ ia32/Nan.v | 38 ++++++++++++++++++-------------------- ia32/SelectOp.vp | 13 ++++++++++++- ia32/SelectOpproof.v | 9 ++++++++- 5 files changed, 84 insertions(+), 25 deletions(-) (limited to 'ia32') diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp index a29b4508..8c3a7fa1 100644 --- a/ia32/ConstpropOp.vp +++ b/ia32/ConstpropOp.vp @@ -291,20 +291,25 @@ Definition make_moduimm n (r1 r2: reg) := | None => (Omodu, r1 :: r2 :: nil) end. -(** We must be careful to preserve 2-address constraints over the - RTL code, which means that commutative operations cannot - be specialized if their first argument is a constant. *) +Definition make_mulfimm (n: float) (r r1 r2: reg) := + if Float.eq_dec n (Float.floatofint (Int.repr 2)) + then (Oaddf, r :: r :: nil) + else (Omulf, r1 :: r2 :: nil). Nondetfunction op_strength_reduction (op: operation) (args: list reg) (vl: list approx) := match op, args, vl with | Osub, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_addimm (Int.neg n2) r1 + | Omul, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_mulimm n1 r2 | Omul, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_mulimm n2 r1 | Odiv, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_divimm n2 r1 r2 | Odivu, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_divuimm n2 r1 r2 | Omodu, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_moduimm n2 r1 r2 + | Oand, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_andimm n1 r2 | Oand, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm n2 r1 + | Oor, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_orimm n1 r2 | 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 @@ -315,6 +320,8 @@ Nondetfunction op_strength_reduction | Ocmp c, args, vl => let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args') + | 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) end. diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v index b6c3cdc3..a4cb4029 100644 --- a/ia32/ConstpropOpproof.v +++ b/ia32/ConstpropOpproof.v @@ -380,6 +380,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 -> @@ -392,6 +419,7 @@ Proof. (* sub *) InvApproxRegs. SimplVMA. inv H0; rewrite H. rewrite Val.sub_add_opp. apply make_addimm_correct; auto. (* mul *) + InvApproxRegs. SimplVMA. inv H0; rewrite H1. rewrite Val.mul_commut. apply make_mulimm_correct; auto. InvApproxRegs. SimplVMA. inv H0; rewrite H. apply make_mulimm_correct; auto. (* divs *) assert (rs#r2 = Vint n2). clear H0. InvApproxRegs; SimplVMA; auto. @@ -403,10 +431,13 @@ Proof. assert (rs#r2 = Vint n2). clear H0. InvApproxRegs; SimplVMA; auto. apply make_moduimm_correct; auto. (* and *) + InvApproxRegs. SimplVMA. inv H0; rewrite H1. rewrite Val.and_commut. apply make_andimm_correct; auto. InvApproxRegs. SimplVMA. inv H0; rewrite H. apply make_andimm_correct; auto. (* or *) + InvApproxRegs. SimplVMA. inv H0; rewrite H1. rewrite Val.or_commut. apply make_orimm_correct; auto. InvApproxRegs. SimplVMA. inv H0; rewrite H. apply make_orimm_correct; auto. (* xor *) + InvApproxRegs. SimplVMA. inv H0; rewrite H1. rewrite Val.xor_commut. apply make_xorimm_correct; auto. InvApproxRegs. SimplVMA. inv H0; rewrite H. apply make_xorimm_correct; auto. (* shl *) InvApproxRegs. SimplVMA. inv H0; rewrite H. apply make_shlimm_correct; auto. @@ -422,6 +453,11 @@ Proof. 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. +(* 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. diff --git a/ia32/Nan.v b/ia32/Nan.v index dadf0ca0..f3e777e1 100644 --- a/ia32/Nan.v +++ b/ia32/Nan.v @@ -1,28 +1,26 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + Require Import Fappli_IEEE. Require Import Fappli_IEEE_bits. Require Import Floats. Require Import ZArith. Require Import Integers. -(* Needed to break a circular reference after extraction *) -Definition transform_quiet_pl := - Eval unfold Float.transform_quiet_pl in Float.transform_quiet_pl. - Program Definition default_pl : bool * nan_pl 53 := (true, nat_iter 51 xO xH). -Definition binop_pl (pl1 pl2:binary64) : bool*nan_pl 53 := - match pl1, pl2 with - | B754_nan s1 pl1, _ => (s1, transform_quiet_pl pl1) - | _, B754_nan s2 pl2 => (s2, transform_quiet_pl pl2) - | _, _ => default_pl - end. - -Theorem binop_propagate1: Float.binop_propagate1_prop binop_pl. -Proof. - repeat intro. destruct f1, f2; try discriminate; simpl; reflexivity. -Qed. - -Theorem binop_propagate2: Float.binop_propagate2_prop binop_pl. -Proof. - repeat intro. destruct f1, f2, f3; try discriminate; simpl; reflexivity. -Qed. +Definition choose_binop_pl (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) := + false. (** always choose first NaN *) diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp index 209147e3..1471405e 100644 --- a/ia32/SelectOp.vp +++ b/ia32/SelectOp.vp @@ -334,7 +334,18 @@ 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). + +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 *) diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v index 85802b60..cec3b599 100644 --- a/ia32/SelectOpproof.v +++ b/ia32/SelectOpproof.v @@ -576,7 +576,14 @@ Qed. Theorem eval_divf: binary_constructor_sound divf Val.divf. Proof. - red; intros; TrivialExists. + 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. -- cgit