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

3 files changed, 19 insertions, 7 deletions

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 *)