Float.intoffloat and Float.intuoffloat are now partial functions.

(May fail if float is too big to be converted.)


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1544 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

21 files changed, 139 insertions, 62 deletions

diff --git a/arm/ConstpropOp.v b/arm/ConstpropOp.v
index a56a5ef..fa97c6c 100644
--- a/arm/ConstpropOp.v
+++ b/arm/ConstpropOp.v
@@ -185,7 +185,7 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
   | Omulf, F n1 :: F n2 :: nil => F(Float.mul n1 n2)
   | Odivf, F n1 :: F n2 :: nil => F(Float.div n1 n2)
   | Osingleoffloat, F n1 :: nil => F(Float.singleoffloat n1)
-  | Ointoffloat, F n1 :: nil => I(Float.intoffloat n1)
+  | Ointoffloat, F n1 :: nil =>  match Float.intoffloat n1 with Some x => I x | None => Unknown end
   | Ofloatofint, I n1 :: nil => F(Float.floatofint n1)
   | Ofloatofintu, I n1 :: nil => F(Float.floatofintu n1)
   | Ocmp c, vl =>
@@ -560,7 +560,7 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
   | eval_static_operation_case47 n1 =>
       F(Float.singleoffloat n1)
   | eval_static_operation_case48 n1 =>
-      I(Float.intoffloat n1)
+      match Float.intoffloat n1 with Some x => I x | None => Unknown end
   | eval_static_operation_case49 n1 =>
       F(Float.floatofint n1)
   | eval_static_operation_case51 c vl =>
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index 9778ace..3f98b88 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -141,6 +141,8 @@ Proof.
 
   rewrite <- H3. replace v0 with (Vfloat n1). reflexivity. congruence.
 
+  inv H4. destruct (Float.intoffloat f); simpl in H0; inv H0. red; auto.
+
   caseEq (eval_static_condition c vl0).
   intros. generalize (eval_static_condition_correct _ _ _ _ H H1).
   intro. rewrite H2 in H0. 
diff --git a/arm/Op.v b/arm/Op.v
index 606281d..acd1bdb 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -281,7 +281,7 @@ Definition eval_operation
   | Omulf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.mul f1 f2))
   | Odivf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.div f1 f2))
   | Osingleoffloat, v1 :: nil => Some (Val.singleoffloat v1)
-  | Ointoffloat, Vfloat f1 :: nil => Some (Vint (Float.intoffloat f1))
+  | Ointoffloat, Vfloat f1 :: nil => option_map Vint (Float.intoffloat f1)
   | Ofloatofint, Vint n1 :: nil => Some (Vfloat (Float.floatofint n1))
   | Ocmp c, _ =>
       match eval_condition c vl with
@@ -547,6 +547,7 @@ Proof.
   destruct (Int.ltu i (Int.repr 31)).
   injection H0; intro; subst v; exact I. discriminate.
   destruct v0; exact I.
+  destruct (Float.intoffloat f); simpl in H0; inv H0. exact I.
   destruct (eval_condition c vl). 
   destruct b; injection H0; intro; subst v; exact I.
   discriminate.
@@ -718,6 +719,7 @@ Proof.
   unfold Int.ltu. rewrite zlt_true. congruence. 
   assert (Int.unsigned (Int.repr 31) < Int.unsigned Int.iwordsize). vm_compute; auto.
   omega. discriminate.
+  destruct (Float.intoffloat f); simpl in H; inv H. auto.
   caseEq (eval_condition c vl); intros; rewrite H0 in H.
   replace v with (Val.of_bool b).
   eapply eval_condition_weaken; eauto.
@@ -819,6 +821,7 @@ Proof.
   destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialExists.
   destruct (Int.ltu i (Int.repr 31)); inv H0; TrivialExists.
   exists (Val.singleoffloat v2); split. auto. apply Val.singleoffloat_lessdef; auto.
+  destruct (Float.intoffloat f); simpl in *; inv H0. TrivialExists.
   caseEq (eval_condition c vl1); intros. rewrite H1 in H0. 
   rewrite (eval_condition_lessdef c H H1).
   destruct b; inv H0; TrivialExists.
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index c8f177b..87dc63e 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -928,29 +928,38 @@ Theorem eval_divf:
 Proof. intros; unfold divf; EvalOp. Qed.
 
 Theorem eval_intoffloat:
-  forall le a x,
+  forall le a x n,
   eval_expr ge sp e m le a (Vfloat x) ->
-  eval_expr ge sp e m le (intoffloat a) (Vint (Float.intoffloat x)).
-Proof. TrivialOp intoffloat. Qed.
+  Float.intoffloat x = Some n ->
+  eval_expr ge sp e m le (intoffloat a) (Vint n).
+Proof.
+  intros; unfold intoffloat; EvalOp.
+  simpl. rewrite H0. auto.
+Qed.
 
 Theorem eval_intuoffloat:
-  forall le a x,
+  forall le a x n,
   eval_expr ge sp e m le a (Vfloat x) ->
-  eval_expr ge sp e m le (intuoffloat a) (Vint (Float.intuoffloat x)).
+  Float.intuoffloat x = Some n ->
+  eval_expr ge sp e m le (intuoffloat a) (Vint n).
 Proof.
   intros. unfold intuoffloat. 
   econstructor. eauto. 
-  set (f := Float.floatofintu Float.ox8000_0000).
+  set (im := Int.repr Int.half_modulus).
+  set (fm := Float.floatofintu im).
   assert (eval_expr ge sp e m (Vfloat x :: le) (Eletvar O) (Vfloat x)).
     constructor. auto. 
-  apply eval_Econdition with (v1 := Float.cmp Clt x f).
+  apply eval_Econdition with (v1 := Float.cmp Clt x fm).
   econstructor. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
   simpl. auto.
-  caseEq (Float.cmp Clt x f); intros.
-  rewrite Float.intuoffloat_intoffloat_1; auto.
-  EvalOp.
-  rewrite Float.intuoffloat_intoffloat_2; auto.
-  apply eval_addimm. apply eval_intoffloat. apply eval_subf; auto. EvalOp.
+  caseEq (Float.cmp Clt x fm); intros.
+  rewrite Float.intuoffloat_intoffloat_1 in H0; auto.
+  EvalOp. simpl. rewrite H0; auto.
+  exploit Float.intuoffloat_intoffloat_2; eauto. intro EQ.
+  replace n with (Int.add (Int.sub n Float.ox8000_0000) Float.ox8000_0000).
+  apply eval_addimm. eapply eval_intoffloat; eauto.
+  apply eval_subf; auto. EvalOp.
+  rewrite Int.sub_add_opp. rewrite Int.add_assoc. apply Int.add_zero. 
 Qed.
 
 Theorem eval_floatofint:
diff --git a/backend/Cminor.v b/backend/Cminor.v
index 4e57d3c..a3a166c 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -240,8 +240,8 @@ Definition eval_unop (op: unary_operation) (arg: val) : option val :=
   | Onegf, Vfloat f1 => Some (Vfloat (Float.neg f1))
   | Oabsf, Vfloat f1 => Some (Vfloat (Float.abs f1))
   | Osingleoffloat, _ => Some (Val.singleoffloat arg)
-  | Ointoffloat, Vfloat f1 => Some (Vint (Float.intoffloat f1))
-  | Ointuoffloat, Vfloat f1 => Some (Vint (Float.intuoffloat f1))
+  | Ointoffloat, Vfloat f1 => option_map Vint (Float.intoffloat f1)
+  | Ointuoffloat, Vfloat f1 => option_map Vint (Float.intuoffloat f1)
   | Ofloatofint, Vint n1 => Some (Vfloat (Float.floatofint n1))
   | Ofloatofintu, Vint n1 => Some (Vfloat (Float.floatofintu n1))
   | _, _ => None
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index cb9f4fc..d997015 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -220,8 +220,8 @@ Proof.
   apply eval_negf; auto.
   apply eval_absf; auto.
   apply eval_singleoffloat; auto.
-  apply eval_intoffloat; auto.
-  apply eval_intuoffloat; auto.
+  remember (Float.intoffloat f) as oi; destruct oi; inv H0. eapply eval_intoffloat; eauto.
+  remember (Float.intuoffloat f) as oi; destruct oi; inv H0. eapply eval_intuoffloat; eauto.
   apply eval_floatofint; auto.
   apply eval_floatofintu; auto.
 Qed.
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 5b2ad9b..480acbb 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -1250,8 +1250,8 @@ Proof.
   inv H0; inv H; TrivialOp.
   inv H0; inv H; TrivialOp.
   inv H0; inv H; TrivialOp.
-  inv H0; inv H; TrivialOp.
-  inv H0; inv H; TrivialOp.
+  inv H0; inv H. destruct (Float.intoffloat f0); simpl in H1; inv H1. TrivialOp.
+  inv H0; inv H. destruct (Float.intuoffloat f0); simpl in H1; inv H1. TrivialOp.
   inv H0; inv H; TrivialOp.
   inv H0; inv H; TrivialOp.
 Qed.
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 742a969..927cd69 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -49,7 +49,7 @@ Definition cast_int_float (si : signedness) (i: int) : float :=
   | Unsigned => Float.floatofintu i
   end.
 
-Definition cast_float_int (si : signedness) (f: float) : int :=
+Definition cast_float_int (si : signedness) (f: float) : option int :=
   match si with
   | Signed => Float.intoffloat f
   | Unsigned => Float.intuoffloat f
@@ -75,9 +75,10 @@ Inductive cast : val -> type -> type -> val -> Prop :=
   | cast_ii:   forall i sz2 sz1 si1 si2,            (**r int to int  *)
       cast (Vint i) (Tint sz1 si1) (Tint sz2 si2)
            (Vint (cast_int_int sz2 si2 i))
-  | cast_fi:   forall f sz1 sz2 si2,                (**r float to int *)
+  | cast_fi:   forall f sz1 sz2 si2 i,              (**r float to int *)
+      cast_float_int si2 f = Some i ->
       cast (Vfloat f) (Tfloat sz1) (Tint sz2 si2)
-           (Vint (cast_int_int sz2 si2 (cast_float_int si2 f)))
+           (Vint (cast_int_int sz2 si2 i))
   | cast_if:   forall i sz1 sz2 si1,                (**r int to float  *)
       cast (Vint i) (Tint sz1 si1) (Tfloat sz2)
           (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 4784e1e..88f042d 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -361,8 +361,18 @@ Proof.
   destruct sg; econstructor; eauto. 
 Qed.
 
+Lemma make_intoffloat_correct:
+  forall e le m a sg f i,
+  eval_expr ge e le m a (Vfloat f) ->
+  cast_float_int sg f = Some i ->
+  eval_expr ge e le m (make_intoffloat a sg) (Vint i).
+Proof.
+  unfold cast_float_int, make_intoffloat; intros.
+  destruct sg; econstructor; eauto; simpl; rewrite H0; auto.
+Qed.
+
 Hint Resolve make_intconst_correct make_floatconst_correct
-             make_floatofint_correct
+             make_floatofint_correct make_intoffloat_correct
              eval_Eunop eval_Ebinop: cshm.
 Hint Extern 2 (@eq trace _ _) => traceEq: cshm.
 
@@ -650,7 +660,8 @@ Proof.
   (* cast_int_int *)
     destruct sz2; destruct si2; repeat econstructor; eauto with cshm.
   (* cast_float_int *)
-    destruct sz2; destruct si2; unfold make_intoffloat; repeat econstructor; eauto with cshm; simpl; auto.
+    exploit make_intoffloat_correct; eauto. intros A.
+    destruct sz2; destruct si2; eauto with cshm.
   (* cast_int_float *)
     destruct sz2; destruct si1; unfold make_floatofint; repeat econstructor; eauto with cshm; simpl; auto.
   (* cast_float_float *)
diff --git a/common/Values.v b/common/Values.v
index af242c9..ceff333 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -117,13 +117,13 @@ Definition absf (v: val) : val :=
 
 Definition intoffloat (v: val) : val :=
   match v with
-  | Vfloat f => Vint (Float.intoffloat f)
+  | Vfloat f => match Float.intoffloat f with Some n => Vint n | None => Vundef end
   | _ => Vundef
   end.
 
 Definition intuoffloat (v: val) : val :=
   match v with
-  | Vfloat f => Vint (Float.intuoffloat f)
+  | Vfloat f => match Float.intuoffloat f with Some n => Vint n | None => Vundef end
   | _ => Vundef
   end.
 
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 8e3c1aa..984bee0 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -30,6 +30,7 @@ Extract Inlined Constant Floats.float => "float".
 Extract Constant Floats.Float.zero   => "0.".
 Extract Constant Floats.Float.neg => "( ~-. )".
 Extract Constant Floats.Float.abs => "abs_float".
+Extract Constant Floats.Float.of_Z => "fun x -> assert false".
 Extract Constant Floats.Float.singleoffloat => "Floataux.singleoffloat".
 Extract Constant Floats.Float.intoffloat => "Floataux.intoffloat".
 Extract Constant Floats.Float.intuoffloat => "Floataux.intuoffloat".
diff --git a/ia32/ConstpropOp.v b/ia32/ConstpropOp.v
index 7dfa046..815ba0e 100644
--- a/ia32/ConstpropOp.v
+++ b/ia32/ConstpropOp.v
@@ -288,7 +288,7 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
   | Omulf, F n1 :: F n2 :: nil => F(Float.mul n1 n2)
   | Odivf, F n1 :: F n2 :: nil => F(Float.div n1 n2)
   | Osingleoffloat, F n1 :: nil => F(Float.singleoffloat n1)
-  | Ointoffloat, F n1 :: nil => I(Float.intoffloat n1)
+  | Ointoffloat, F n1 :: nil => match Float.intoffloat n1 with Some x => I x | None => Unknown end
   | Ofloatofint, I n1 :: nil => F(Float.floatofint n1)
   | Ocmp c, vl => match eval_static_condition c vl with None => Unknown | Some b => I(if b then Int.one else Int.zero) end
   | _, _ => Unknown
@@ -590,7 +590,7 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
   | eval_static_operation_case38 n1 =>
       F(Float.singleoffloat n1)
   | eval_static_operation_case39 n1 =>
-      I(Float.intoffloat n1)
+      match Float.intoffloat n1 with Some x => I x | None => Unknown end
   | eval_static_operation_case41 n1 =>
       F(Float.floatofint n1)
   | eval_static_operation_case43 c vl =>
diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v
index ea90446..105a7bd 100644
--- a/ia32/ConstpropOpproof.v
+++ b/ia32/ConstpropOpproof.v
@@ -178,6 +178,8 @@ Proof.
 
   rewrite <- H3. replace v0 with (Vfloat n1). reflexivity. congruence.
 
+  inv H4. destruct (Float.intoffloat f); inv H0. red; auto.
+
   caseEq (eval_static_condition c vl0).
   intros. generalize (eval_static_condition_correct _ _ _ _ H H1).
   intro. rewrite H2 in H0. 
diff --git a/ia32/Op.v b/ia32/Op.v
index ea28845..c09dc5b 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -285,7 +285,7 @@ Definition eval_operation
   | Osingleoffloat, v1 :: nil =>
       Some (Val.singleoffloat v1)
   | Ointoffloat, Vfloat f1 :: nil => 
-      Some (Vint (Float.intoffloat f1))
+      option_map Vint (Float.intoffloat f1)
   | Ofloatofint, Vint n1 :: nil => 
       Some (Vfloat (Float.floatofint n1))
   | Ocmp c, _ =>
@@ -547,6 +547,7 @@ Proof.
   injection H0; intro; subst v; exact I. discriminate.
   simpl. eapply type_of_addressing_sound; eauto.
   destruct v0; exact I.
+  destruct (Float.intoffloat f); simpl in H0; inv H0. exact I.
   destruct (eval_condition c vl). 
   destruct b; injection H0; intro; subst v; exact I.
   discriminate.
@@ -727,6 +728,7 @@ Proof.
   destruct (Int.ltu i Int.iwordsize); congruence.
   destruct (Int.ltu i Int.iwordsize); congruence.
   apply eval_addressing_weaken; auto.
+  destruct (Float.intoffloat f); simpl in H; inv H. auto.
   caseEq (eval_condition c vl); intros; rewrite H0 in H.
   replace v with (Val.of_bool b).
   eapply eval_condition_weaken; eauto.
@@ -832,6 +834,7 @@ Proof.
   destruct (Int.ltu i Int.iwordsize); inv H0; TrivialExists.
   eapply eval_addressing_lessdef; eauto.
   exists (Val.singleoffloat v2); split. auto. apply Val.singleoffloat_lessdef; auto.
+  exists v1; split; auto. 
   caseEq (eval_condition c vl1); intros. rewrite H1 in H0. 
   rewrite (eval_condition_lessdef c H H1).
   destruct b; inv H0; TrivialExists.
diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v
index 59fed01..4279f29 100644
--- a/ia32/SelectOpproof.v
+++ b/ia32/SelectOpproof.v
@@ -835,10 +835,14 @@ Theorem eval_absf:
 Proof. intros; unfold absf; EvalOp. Qed.
 
 Theorem eval_intoffloat:
-  forall le a x,
+  forall le a x n,
   eval_expr ge sp e m le a (Vfloat x) ->
-  eval_expr ge sp e m le (intoffloat a) (Vint (Float.intoffloat x)).
-Proof. intros; unfold intoffloat; EvalOp. Qed.
+  Float.intoffloat x = Some n ->
+  eval_expr ge sp e m le (intoffloat a) (Vint n).
+Proof.
+  intros; unfold intoffloat; EvalOp.
+  simpl. rewrite H0. auto.
+Qed.
 
 Theorem eval_floatofint:
   forall le a x,
@@ -875,9 +879,10 @@ Theorem eval_divf:
 Proof. intros; unfold divf; EvalOp. Qed.
 
 Theorem eval_intuoffloat:
-  forall le a x,
+  forall le a x n,
   eval_expr ge sp e m le a (Vfloat x) ->
-  eval_expr ge sp e m le (intuoffloat a) (Vint (Float.intuoffloat x)).
+  Float.intuoffloat x = Some n ->
+  eval_expr ge sp e m le (intuoffloat a) (Vint n).
 Proof.
   intros. unfold intuoffloat. 
   econstructor. eauto. 
@@ -889,10 +894,13 @@ Proof.
   econstructor. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
   simpl. auto.
   caseEq (Float.cmp Clt x fm); intros.
-  rewrite Float.intuoffloat_intoffloat_1; auto.
-  EvalOp.
-  rewrite Float.intuoffloat_intoffloat_2; auto.
-  fold im. apply eval_addimm. apply eval_intoffloat. apply eval_subf; auto. EvalOp.
+  rewrite Float.intuoffloat_intoffloat_1 in H0; auto.
+  EvalOp. simpl. rewrite H0; auto.
+  exploit Float.intuoffloat_intoffloat_2; eauto. intro EQ.
+  replace n with (Int.add (Int.sub n Float.ox8000_0000) Float.ox8000_0000).
+  apply eval_addimm. eapply eval_intoffloat; eauto.
+  apply eval_subf; auto. EvalOp.
+  rewrite Int.sub_add_opp. rewrite Int.add_assoc. apply Int.add_zero. 
 Qed.
 
 Theorem eval_floatofintu:
diff --git a/lib/Floataux.ml b/lib/Floataux.ml
index f0db1fa..dfdd6ce 100644
--- a/lib/Floataux.ml
+++ b/lib/Floataux.ml
@@ -19,10 +19,14 @@ let singleoffloat f =
   Int32.float_of_bits (Int32.bits_of_float f)
 
 let intoffloat f =
-  coqint_of_camlint (Int32.of_float f)
+  if f < 2147483648.0 (*2^31 *) && f > -2147483649.0 (* -2^31-1 *)
+  then Some (coqint_of_camlint (Int32.of_float f))
+  else None
 
 let intuoffloat f =
-  coqint_of_camlint (Int64.to_int32 (Int64.of_float f))
+  if f < 4294967296.0 (* 2^32 *) && f >= 0.0
+  then Some (coqint_of_camlint (Int64.to_int32 (Int64.of_float f)))
+  else None
 
 let floatofint i =
   Int32.to_float (camlint_of_coqint i)
diff --git a/lib/Floats.v b/lib/Floats.v
index 6257bcc..50712af 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -31,13 +31,15 @@ Parameter zero: float.                  (**r the float [+0.0] *)
 
 Axiom eq_dec: forall (f1 f2: float), {f1 = f2} + {f1 <> f2}.
 
+Parameter of_Z: Z -> float.             (**r conversion from exact integers, for specification *)
+
 (** Arithmetic operations *)
 
 Parameter neg: float -> float.          (**r opposite (change sign) *)
 Parameter abs: float -> float.          (**r absolute value (set sign to [+]) *)
 Parameter singleoffloat: float -> float. (**r conversion to single precision *)
-Parameter intoffloat: float -> int.     (**r conversion to signed 32-bit int *)
-Parameter intuoffloat: float -> int.    (**r conversion to unsigned 32-bit int *)
+Parameter intoffloat: float -> option int. (**r conversion to signed 32-bit int *)
+Parameter intuoffloat: float -> option int. (**r conversion to unsigned 32-bit int *)
 Parameter floatofint: int -> float.     (**r conversion from signed 32-bit int *)
 Parameter floatofintu: int -> float.    (**r conversion from unsigned 32-bit int *)
 
@@ -116,6 +118,18 @@ Axiom bits_of_singleoffloat:
 Axiom singleoffloat_of_bits:
   forall b, singleoffloat (single_of_bits b) = single_of_bits b.
 
+(** Range of conversions from floats to ints. *)
+
+Axiom intuoffloat_defined:
+  forall f, 
+  cmp Clt f (of_Z Int.modulus) = true /\ cmp Cge f zero = true
+  <-> exists n, intuoffloat f = Some n.
+
+Axiom intoffloat_defined:
+  forall f, 
+  cmp Clt f (of_Z Int.half_modulus) = true /\ cmp Cgt f (of_Z (- Int.half_modulus - 1)) = true
+  <-> exists n, intoffloat f = Some n.
+
 (** Conversions between floats and unsigned ints can be defined
   in terms of conversions between floats and signed ints.
   (Most processors provide only the latter, forcing the compiler
@@ -140,11 +154,16 @@ Axiom intuoffloat_intoffloat_1:
   intuoffloat x = intoffloat x.
 
 Axiom intuoffloat_intoffloat_2:
-  forall x,
+  forall x n,
+  cmp Clt x (floatofintu ox8000_0000) = false ->
+  intuoffloat x = Some n ->
+  intoffloat (sub x (floatofintu ox8000_0000)) = Some (Int.sub n ox8000_0000).
+
+Axiom intuoffloat_intoffloat_3:
+  forall x n,
   cmp Clt x (floatofintu ox8000_0000) = false ->
-  intuoffloat x =
-  Int.add (intoffloat (sub x (floatofintu ox8000_0000)))
-          ox8000_0000.
+  intoffloat (sub x (floatofintu ox8000_0000)) = Some n ->
+  intuoffloat x = Some (Int.add n ox8000_0000).
 
 (** Conversions from ints to floats can be defined as bitwise manipulations
   over the in-memory representation.  This is what the PowerPC port does.
diff --git a/powerpc/ConstpropOp.v b/powerpc/ConstpropOp.v
index b6eecc7..07a1872 100644
--- a/powerpc/ConstpropOp.v
+++ b/powerpc/ConstpropOp.v
@@ -181,7 +181,7 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
   | Omuladdf, F n1 :: F n2 :: F n3 :: nil => F(Float.add (Float.mul n1 n2) n3)
   | Omulsubf, F n1 :: F n2 :: F n3 :: nil => F(Float.sub (Float.mul n1 n2) n3)
   | Osingleoffloat, F n1 :: nil => F(Float.singleoffloat n1)
-  | Ointoffloat, F n1 :: nil => I(Float.intoffloat n1)
+  | Ointoffloat, F n1 :: nil => match Float.intoffloat n1 with Some x => I x | None => Unknown end
   | Ofloatofwords, I n1 :: I n2 :: nil => F(Float.from_words n1 n2)
   | Ocmp c, vl =>
       match eval_static_condition c vl with
@@ -518,7 +518,7 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
   | eval_static_operation_case43 n1 =>
       F(Float.singleoffloat n1)
   | eval_static_operation_case44 n1 =>
-      I(Float.intoffloat n1)
+      match Float.intoffloat n1 with Some x => I x | None => Unknown end
   | eval_static_operation_case45 n1 n2 =>
       F(Float.from_words n1 n2)
   | eval_static_operation_case47 c vl =>
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index b5e2e8e..ac15c0d 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -147,6 +147,8 @@ Proof.
 
   rewrite <- H3. replace v0 with (Vfloat n1). reflexivity. congruence.
 
+  inv H4. destruct (Float.intoffloat f); simpl in H0; inv H0. red; auto.
+
   caseEq (eval_static_condition c vl0).
   intros. generalize (eval_static_condition_correct _ _ _ _ H H1).
   intro. rewrite H2 in H0. 
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 902fc02..6f05e55 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -247,7 +247,7 @@ Definition eval_operation
   | Osingleoffloat, v1 :: nil =>
       Some (Val.singleoffloat v1)
   | Ointoffloat, Vfloat f1 :: nil => 
-      Some (Vint (Float.intoffloat f1))
+      option_map Vint (Float.intoffloat f1)
   | Ofloatofwords, Vint i1 :: Vint i2 :: nil =>
       Some (Vfloat (Float.from_words i1 i2))
   | Ocmp c, _ =>
@@ -515,6 +515,7 @@ Proof.
   destruct (Int.ltu i0 Int.iwordsize).
   injection H0; intro; subst v; exact I. discriminate.
   destruct v0; exact I.
+  destruct (Float.intoffloat f); simpl in H0; inv H0. exact I.
   destruct (eval_condition c vl). 
   destruct b; injection H0; intro; subst v; exact I.
   discriminate.
@@ -678,6 +679,7 @@ Proof.
   destruct (Int.ltu i Int.iwordsize); congruence.
   destruct (Int.ltu i Int.iwordsize); congruence.
   destruct (Int.ltu i0 Int.iwordsize); congruence.
+  destruct (Float.intoffloat f); inv H. auto.
   caseEq (eval_condition c vl); intros; rewrite H0 in H.
   replace v with (Val.of_bool b).
   eapply eval_condition_weaken; eauto.
@@ -782,6 +784,7 @@ Proof.
   destruct (Int.ltu i Int.iwordsize); inv H0; TrivialExists.
   destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists.
   exists (Val.singleoffloat v2); split. auto. apply Val.singleoffloat_lessdef; auto.
+  destruct (Float.intoffloat f); simpl in *; inv H0. TrivialExists.
   caseEq (eval_condition c vl1); intros. rewrite H1 in H0. 
   rewrite (eval_condition_lessdef c H H1).
   destruct b; inv H0; TrivialExists.
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 8a06433..60c11dc 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -847,28 +847,37 @@ Theorem eval_absf:
 Proof. intros; unfold absf; EvalOp. Qed.
 
 Theorem eval_intoffloat:
-  forall le a x,
+  forall le a x n,
   eval_expr ge sp e m le a (Vfloat x) ->
-  eval_expr ge sp e m le (intoffloat a) (Vint (Float.intoffloat x)).
-Proof. intros; unfold intoffloat; EvalOp. Qed.
+  Float.intoffloat x = Some n ->
+  eval_expr ge sp e m le (intoffloat a) (Vint n).
+Proof.
+  intros; unfold intoffloat; EvalOp. simpl. rewrite H0; auto.
+Qed.
 
 Theorem eval_intuoffloat:
-  forall le a x,
+  forall le a x n,
   eval_expr ge sp e m le a (Vfloat x) ->
-  eval_expr ge sp e m le (intuoffloat a) (Vint (Float.intuoffloat x)).
+  Float.intuoffloat x = Some n ->
+  eval_expr ge sp e m le (intuoffloat a) (Vint n).
 Proof.
   intros. unfold intuoffloat. 
   econstructor. eauto. 
-  set (fm := Float.floatofintu Float.ox8000_0000).
-  assert (eval_expr ge sp e m (Vfloat x :: le) (Eletvar O) (Vfloat x)). constructor. auto. 
+  set (im := Int.repr Int.half_modulus).
+  set (fm := Float.floatofintu im).
+  assert (eval_expr ge sp e m (Vfloat x :: le) (Eletvar O) (Vfloat x)).
+    constructor. auto. 
   apply eval_Econdition with (v1 := Float.cmp Clt x fm).
   econstructor. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
   simpl. auto.
   caseEq (Float.cmp Clt x fm); intros.
-  rewrite Float.intuoffloat_intoffloat_1; auto.
-  EvalOp.
-  rewrite Float.intuoffloat_intoffloat_2; auto.
-  apply eval_addimm. apply eval_intoffloat. apply eval_subf; auto. EvalOp.
+  rewrite Float.intuoffloat_intoffloat_1 in H0; auto.
+  EvalOp. simpl. rewrite H0; auto.
+  exploit Float.intuoffloat_intoffloat_2; eauto. intro EQ.
+  replace n with (Int.add (Int.sub n Float.ox8000_0000) Float.ox8000_0000).
+  apply eval_addimm. eapply eval_intoffloat; eauto.
+  apply eval_subf; auto. EvalOp.
+  rewrite Int.sub_add_opp. rewrite Int.add_assoc. apply Int.add_zero. 
 Qed.
 
 Theorem eval_floatofint: