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/ConstpropOp.v      |  4 ++--
 arm/ConstpropOpproof.v |  2 ++
 arm/Op.v               |  5 ++++-
 arm/SelectOpproof.v    | 33 +++++++++++++++++++++------------
 4 files changed, 29 insertions(+), 15 deletions(-)

(limited to 'arm')

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:
-- 
cgit v1.2.3