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

4 files changed, 25 insertions, 12 deletions

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: