From 14a9bb4b267eeead8cd9503ee19e860a8bc0d763 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 28 Oct 2010 14:56:39 +0000
Subject: 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
---
 arm/SelectOpproof.v | 33 +++++++++++++++++++++------------
 1 file changed, 21 insertions(+), 12 deletions(-)

(limited to 'arm/SelectOpproof.v')

diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index c8f177b3..87dc63ee 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:
-- 
cgit