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

5 files changed, 84 insertions, 25 deletions

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.