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

1 files changed, 20 insertions, 11 deletions

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: