summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Changelog5
-rw-r--r--arm/ConstpropOp.vp7
-rw-r--r--arm/ConstpropOpproof.v32
-rw-r--r--arm/Nan.v47
-rw-r--r--backend/Constprop.v4
-rw-r--r--backend/Constpropproof.v12
-rw-r--r--backend/SelectDiv.vp18
-rw-r--r--backend/SelectDivproof.v18
-rw-r--r--extraction/extraction.v6
-rw-r--r--ia32/ConstpropOp.vp13
-rw-r--r--ia32/ConstpropOpproof.v36
-rw-r--r--ia32/Nan.v38
-rw-r--r--ia32/SelectOp.vp13
-rw-r--r--ia32/SelectOpproof.v9
-rw-r--r--lib/Floats.v140
-rw-r--r--powerpc/ConstpropOp.vp7
-rw-r--r--powerpc/ConstpropOpproof.v32
-rw-r--r--powerpc/Nan.v38
-rw-r--r--powerpc/SelectOp.vp1
-rw-r--r--powerpc/SelectOpproof.v5
20 files changed, 374 insertions, 107 deletions
diff --git a/Changelog b/Changelog
index 5f0c7c7..b603c32 100644
--- a/Changelog
+++ b/Changelog
@@ -5,8 +5,13 @@ Development trunk:
arithmetic.
- Optimize integer divisions by positive constants, turning them into
multiply-high and shifts.
+- Optimize floating-point divisions by powers of 2, turning them
+ into multiplications.
+- Optimize "x * 2.0" and "2.0 * x" into "x + x".
- Avoid double rounding issues in conversion from 64-bit integers
to single-precision floats.
+- Fixed typing rules for __builtin_annot() to avoid casting arguments
+ of small integer or FP types.
- PowerPC: more efficient implementation of division on 64-bit integers.
- Minor simplifications in the generic solvers for dataflow analysis.
diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp
index caf0da6..47d2086 100644
--- a/arm/ConstpropOp.vp
+++ b/arm/ConstpropOp.vp
@@ -287,6 +287,11 @@ Definition make_xorimm (n: int) (r: reg) :=
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) :=
+ 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
@@ -317,6 +322,8 @@ Nondetfunction op_strength_reduction
| Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1 r2
| 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/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index 687e08f..f0d6b7f 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -372,6 +372,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 ->
@@ -431,6 +458,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.
diff --git a/arm/Nan.v b/arm/Nan.v
index d66d6ec..e2bddf6 100644
--- a/arm/Nan.v
+++ b/arm/Nan.v
@@ -1,34 +1,29 @@
+(* *********************************************************************)
+(* *)
+(* 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 := (false, nat_iter 51 xO xH).
-Definition binop_pl (pl1 pl2:binary64) : bool*nan_pl 53 :=
- match pl1, pl2 with
- | B754_nan s1 pl1, B754_nan s2 pl2 =>
- if (Pos.testbit (proj1_sig pl1) 51 && (* pl2 is sNan but pl1 is qNan *)
- negb (Pos.testbit (proj1_sig pl2) 51))%bool
- then (s2, transform_quiet_pl pl2)
- else (s1, transform_quiet_pl pl1)
- | 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;
- destruct Pos.testbit; 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) :=
+ (** Choose second NaN if pl2 is sNaN but pl1 is qNan.
+ In all other cases, choose first NaN *)
+ (Pos.testbit (proj1_sig pl1) 51 &&
+ negb (Pos.testbit (proj1_sig pl2) 51))%bool.
diff --git a/backend/Constprop.v b/backend/Constprop.v
index 24573a5..e5ea64d 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -322,7 +322,9 @@ Function annot_strength_reduction
let (targs'', args'') := annot_strength_reduction app targs' args' in
match ty, approx_reg app arg with
| Tint, I n => (AA_int n :: targs'', args'')
- | Tfloat, F n => (AA_float n :: targs'', args'')
+ | Tfloat, F n => if generate_float_constants tt
+ then (AA_float n :: targs'', args'')
+ else (AA_arg ty :: targs'', arg :: args'')
| _, _ => (AA_arg ty :: targs'', arg :: args'')
end
| targ :: targs', _ =>
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index 328f724..898c4df 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -517,10 +517,14 @@ Proof.
exists (ev1 :: eargs''); split.
simpl; constructor; auto. simpl. congruence.
}
- destruct ty; destruct (approx_reg app arg) as [] eqn:E2; inv H; auto;
- exists eargs''; split; auto; simpl; f_equal; auto;
- generalize (MATCH arg); rewrite E2; simpl; intros E3;
- rewrite E3 in H5; inv H5; auto.
+ destruct ty; destruct (approx_reg app arg) as [] eqn:E2; inv H; auto.
+ * exists eargs''; split; auto; simpl; f_equal; auto.
+ generalize (MATCH arg); rewrite E2; simpl; intros E3;
+ rewrite E3 in H5; inv H5; auto.
+ * destruct (generate_float_constants tt); inv H1; auto.
+ exists eargs''; split; auto; simpl; f_equal; auto.
+ generalize (MATCH arg); rewrite E2; simpl; intros E3;
+ rewrite E3 in H5; inv H5; auto.
+ destruct (annot_strength_reduction app targs args) as [targs'' args''] eqn:E.
inv H.
exploit IHtargs; eauto. intros [eargs'' [A B]].
diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp
index e60a97d..1d9168c 100644
--- a/backend/SelectDiv.vp
+++ b/backend/SelectDiv.vp
@@ -10,7 +10,7 @@
(* *)
(* *********************************************************************)
-(** Instruction selection for integer division and modulus *)
+(** Instruction selection for division and modulus *)
Require Import Coqlib.
Require Import AST.
@@ -154,3 +154,19 @@ Nondetfunction mods (e1: expr) (e2: expr) :=
| _ => mods_base e1 e2
end.
+(** Floating-point division by a constant can also be turned into a FP
+ multiplication by the inverse constant, but only for powers of 2. *)
+
+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.
+
+
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v
index 4d8f96a..0719a5e 100644
--- a/backend/SelectDivproof.v
+++ b/backend/SelectDivproof.v
@@ -544,4 +544,22 @@ Proof.
- eapply eval_mods_base; eauto.
Qed.
+(** * Floating-point division *)
+
+Theorem eval_divf:
+ forall le a b x y,
+ eval_expr ge sp e m le a x ->
+ eval_expr ge sp e m le b y ->
+ exists v, eval_expr ge sp e m le (divf a b) v /\ Val.lessdef (Val.divf x y) v.
+Proof.
+ 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.
+
End CMCONSTRS.
diff --git a/extraction/extraction.v b/extraction/extraction.v
index ba1ca58..047a9b4 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -32,8 +32,8 @@ Require Import ExtrOcamlString.
Extraction Inline Wfsimpl.Fix Wfsimpl.Fixm.
(* Floats *)
-Extract Constant Floats.Float.binop_pl =>
- "Nan.binop_pl".
+Extract Constant Floats.Float.default_pl => "Nan.default_pl".
+Extract Constant Floats.Float.choose_binop_pl => "Nan.choose_binop_pl".
(* AST *)
Extract Constant AST.ident_of_string =>
@@ -135,4 +135,4 @@ Separate Extraction
RTL.instr_defs RTL.instr_uses
Machregs.mregs_for_operation Machregs.mregs_for_builtin
Machregs.two_address_op
- Nan.binop_pl.
+ Nan.default_pl Nan.choose_binop_pl.
diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp
index a29b450..8c3a7fa 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 b6c3cdc..a4cb402 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 dadf0ca..f3e777e 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 209147e..1471405 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 85802b6..cec3b59 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.
diff --git a/lib/Floats.v b/lib/Floats.v
index 0151cf0..0a30836 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -260,23 +260,27 @@ Definition singleoflong (n:int64): float := (**r conversion from signed 64-bit i
Definition singleoflongu (n:int64): float:= (**r conversion from unsigned 64-bit int to single-precision float *)
floatofbinary32 (binary_normalize32 (Int64.unsigned n) 0 false).
-Parameter binop_pl: binary64 -> binary64 -> bool*nan_pl 53.
-
-Definition binop_propagate1_prop binop_pl :=
- forall f1 f2:float, is_nan _ _ f1 = true -> is_nan _ _ f2 = false ->
- binop_pl f1 f1 = (binop_pl f1 f2 : bool*nan_pl 53).
-
-
-(* Proved in Nan.v for different architectures *)
-Hypothesis binop_propagate1: binop_propagate1_prop binop_pl.
-
-Definition binop_propagate2_prop binop_pl :=
- forall f1 f2 f3:float, is_nan _ _ f1 = true ->
- is_nan _ _ f2 = false -> is_nan _ _ f3 = false ->
- binop_pl f1 f2 = (binop_pl f1 f3 : bool*nan_pl 53).
-
-(* Proved in Nan.v for different architectures *)
-Hypothesis binop_propagate2: binop_propagate2_prop binop_pl.
+(* The Nan payload operations for two-argument arithmetic operations are not part of
+ the IEEE754 standard, but all architectures of Compcert share a similar
+ NaN behavior, parameterized by:
+- a "default" payload which occurs when an operation generates a NaN from
+ non-NaN arguments;
+- a choice function determining which of the payload arguments to choose,
+ when an operation is given two NaN arguments. *)
+
+Parameter default_pl : bool*nan_pl 53.
+Parameter choose_binop_pl : bool -> nan_pl 53 -> bool -> nan_pl 53 -> bool.
+
+Definition binop_pl (x y: binary64) : bool*nan_pl 53 :=
+ match x, y with
+ | B754_nan s1 pl1, B754_nan s2 pl2 =>
+ if choose_binop_pl s1 pl1 s2 pl2
+ then (s2, transform_quiet_pl pl2)
+ else (s1, transform_quiet_pl pl1)
+ | B754_nan s1 pl1, _ => (s1, transform_quiet_pl pl1)
+ | _, B754_nan s2 pl2 => (s2, transform_quiet_pl pl2)
+ | _, _ => default_pl
+ end.
Definition add: float -> float -> float := b64_plus binop_pl mode_NE. (**r addition *)
Definition sub: float -> float -> float := b64_minus binop_pl mode_NE. (**r subtraction *)
@@ -496,6 +500,57 @@ Proof.
right; red; intros; elim n. apply singleoffloat_of_single; auto.
Defined.
+(** Commutativity properties of addition and multiplication. *)
+
+Theorem add_commut:
+ forall x y, is_nan _ _ x = false \/ is_nan _ _ y = false -> add x y = add y x.
+Proof.
+ intros x y NAN. unfold add, b64_plus.
+ pose proof (Bplus_correct 53 1024 eq_refl eq_refl binop_pl mode_NE x y).
+ pose proof (Bplus_correct 53 1024 eq_refl eq_refl binop_pl mode_NE y x).
+ unfold Bplus in *; destruct x; destruct y; auto.
+- rewrite (eqb_sym b0 b). destruct (eqb b b0) eqn:EQB; auto. f_equal; apply eqb_prop; auto.
+- rewrite (eqb_sym b0 b). destruct (eqb b b0) eqn:EQB.
+ f_equal; apply eqb_prop; auto.
+ auto.
+- simpl in NAN; intuition congruence.
+- exploit H; auto. clear H. exploit H0; auto. clear H0.
+ set (x := B754_finite 53 1024 b0 m0 e1 e2).
+ set (rx := B2R 53 1024 x).
+ set (y := B754_finite 53 1024 b m e e0).
+ set (ry := B2R 53 1024 y).
+ rewrite (Rplus_comm ry rx). destruct Rlt_bool.
+ intros (A1 & A2 & A3) (B1 & B2 & B3).
+ apply B2R_Bsign_inj; auto. rewrite <- B1 in A1. auto.
+ rewrite Z.add_comm. rewrite Z.min_comm. auto.
+ intros (A1 & A2) (B1 & B2). apply B2FF_inj. rewrite B2 in B1. rewrite <- B1 in A1. auto.
+Qed.
+
+Theorem mul_commut:
+ forall x y, is_nan _ _ x = false \/ is_nan _ _ y = false -> mul x y = mul y x.
+Proof.
+ intros x y NAN. unfold mul, b64_mult.
+ pose proof (Bmult_correct 53 1024 eq_refl eq_refl binop_pl mode_NE x y).
+ pose proof (Bmult_correct 53 1024 eq_refl eq_refl binop_pl mode_NE y x).
+ unfold Bmult in *; destruct x; destruct y; auto.
+- f_equal. apply xorb_comm.
+- f_equal. apply xorb_comm.
+- f_equal. apply xorb_comm.
+- f_equal. apply xorb_comm.
+- simpl in NAN. intuition congruence.
+- f_equal. apply xorb_comm.
+- f_equal. apply xorb_comm.
+- set (x := B754_finite 53 1024 b0 m0 e1 e2) in *.
+ set (rx := B2R 53 1024 x) in *.
+ set (y := B754_finite 53 1024 b m e e0) in *.
+ set (ry := B2R 53 1024 y) in *.
+ rewrite (Rmult_comm ry rx) in *. destruct Rlt_bool.
+ destruct H as (A1 & A2 & A3); destruct H0 as (B1 & B2 & B3).
+ apply B2R_Bsign_inj; auto. rewrite <- B1 in A1. auto.
+ rewrite ! Bsign_FF2B. f_equal. f_equal. apply xorb_comm. apply Pos.mul_comm. apply Z.add_comm.
+ apply B2FF_inj. etransitivity. eapply H. rewrite xorb_comm. auto.
+Qed.
+
(** Properties of comparisons. *)
Theorem order_float_finite_correct:
@@ -1181,7 +1236,7 @@ Proof.
symmetry. etransitivity. apply H0.
f_equal. destruct Bsign; reflexivity.
- destruct f as [[]|[]| |]; try discriminate; try reflexivity.
- simpl. erewrite binop_propagate1; reflexivity.
+ simpl. destruct (choose_binop_pl b n b n); auto.
Qed.
Program Definition pow2_float (b:bool) (e:Z) (H:-1023 < e < 1023) : float :=
@@ -1216,9 +1271,7 @@ Proof.
+ apply B2FF_inj.
etransitivity. apply H0. symmetry. etransitivity. apply H1.
reflexivity.
- - destruct f; try discriminate EQFIN. reflexivity.
- simpl. erewrite binop_propagate2. reflexivity.
- reflexivity. reflexivity. reflexivity.
+ - destruct f; try discriminate EQFIN; auto.
- simpl.
assert ((4503599627370496 * bpow radix2 (e - 52))%R =
(/ (4503599627370496 * bpow radix2 (- e - 52)))%R).
@@ -1233,6 +1286,51 @@ Proof.
destruct b; simpl in H2; omega.
Qed.
+Definition exact_inverse_mantissa := nat_iter 52 xO xH.
+
+Program Definition exact_inverse (f: float) : option float :=
+ match f with
+ | B754_finite s m e B =>
+ if peq m exact_inverse_mantissa then
+ if zlt (-1023) (e + 52) then
+ if zlt (e + 52) 1023 then
+ Some(B754_finite _ _ s m (-e - 104) _)
+ else None else None else None
+ | _ => None
+ end.
+Next Obligation.
+ unfold Fappli_IEEE.bounded, canonic_mantissa. apply andb_true_iff; split.
+ simpl Z.of_nat. apply Zeq_bool_true. unfold FLT_exp. apply Z.max_case_strong; omega.
+ apply Zle_bool_true. omega.
+Qed.
+
+Remark B754_finite_eq:
+ forall s1 m1 e1 B1 s2 m2 e2 B2,
+ s1 = s2 -> m1 = m2 -> e1 = e2 ->
+ B754_finite _ _ s1 m1 e1 B1 = (B754_finite _ _ s2 m2 e2 B2 : float).
+Proof.
+ intros. subst. f_equal. apply proof_irrelevance.
+Qed.
+
+Theorem div_mul_inverse:
+ forall x y z, exact_inverse y = Some z -> div x y = mul x z.
+Proof with (try discriminate).
+ unfold exact_inverse; intros. destruct y...
+ destruct (peq m exact_inverse_mantissa)...
+ destruct (zlt (-1023) (e + 52))...
+ destruct (zlt (e + 52) 1023)...
+ inv H.
+ set (n := - e - 52).
+ assert (RNG1: -1023 < n < 1023) by (unfold n; omega).
+ assert (RNG2: -1023 < -n < 1023) by (unfold n; omega).
+ symmetry.
+ transitivity (mul x (pow2_float b n RNG1)).
+ f_equal. apply B754_finite_eq; auto. unfold n; omega.
+ transitivity (div x (pow2_float b (-n) RNG2)).
+ apply mul_div_pow2.
+ f_equal. apply B754_finite_eq; auto. unfold n; omega.
+Qed.
+
Global Opaque
zero eq_dec neg abs singleoffloat intoffloat intuoffloat floatofint floatofintu
add sub mul div cmp bits_of_double double_of_bits bits_of_single single_of_bits from_words.
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index d0322c1..b755b5e 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -245,6 +245,11 @@ Definition make_xorimm (n: int) (r: reg) :=
then (Omove, r :: nil)
else (Oxorimm n, r :: nil).
+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
@@ -267,6 +272,8 @@ Nondetfunction op_strength_reduction
| Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1 r2
| 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/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index 9d833bf..b7fad69 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.
diff --git a/powerpc/Nan.v b/powerpc/Nan.v
index 77a752e..c230789 100644
--- a/powerpc/Nan.v
+++ b/powerpc/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 := (false, 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; 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.
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index bc9b677..b0e7c4d 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -334,7 +334,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 *)
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 177d64a..c0601eb 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -600,11 +600,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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 19:04:24 +0000