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

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.