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
---
 powerpc/ConstpropOp.v      |  4 ++--
 powerpc/ConstpropOpproof.v |  2 ++
 powerpc/Op.v               |  5 ++++-
 powerpc/SelectOpproof.v    | 31 ++++++++++++++++++++-----------
 4 files changed, 28 insertions(+), 14 deletions(-)

(limited to 'powerpc')

diff --git a/powerpc/ConstpropOp.v b/powerpc/ConstpropOp.v
index b6eecc74..07a1872e 100644
--- a/powerpc/ConstpropOp.v
+++ b/powerpc/ConstpropOp.v
@@ -181,7 +181,7 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
   | Omuladdf, F n1 :: F n2 :: F n3 :: nil => F(Float.add (Float.mul n1 n2) n3)
   | Omulsubf, F n1 :: F n2 :: F n3 :: nil => F(Float.sub (Float.mul n1 n2) n3)
   | 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
   | Ofloatofwords, I n1 :: I n2 :: nil => F(Float.from_words n1 n2)
   | Ocmp c, vl =>
       match eval_static_condition c vl with
@@ -518,7 +518,7 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
   | eval_static_operation_case43 n1 =>
       F(Float.singleoffloat n1)
   | eval_static_operation_case44 n1 =>
-      I(Float.intoffloat n1)
+      match Float.intoffloat n1 with Some x => I x | None => Unknown end
   | eval_static_operation_case45 n1 n2 =>
       F(Float.from_words n1 n2)
   | eval_static_operation_case47 c vl =>
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index b5e2e8ee..ac15c0d3 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -147,6 +147,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/powerpc/Op.v b/powerpc/Op.v
index 902fc025..6f05e550 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -247,7 +247,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)
   | Ofloatofwords, Vint i1 :: Vint i2 :: nil =>
       Some (Vfloat (Float.from_words i1 i2))
   | Ocmp c, _ =>
@@ -515,6 +515,7 @@ Proof.
   destruct (Int.ltu i0 Int.iwordsize).
   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.
@@ -678,6 +679,7 @@ Proof.
   destruct (Int.ltu i Int.iwordsize); congruence.
   destruct (Int.ltu i Int.iwordsize); congruence.
   destruct (Int.ltu i0 Int.iwordsize); congruence.
+  destruct (Float.intoffloat f); 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.
@@ -782,6 +784,7 @@ Proof.
   destruct (Int.ltu i Int.iwordsize); inv H0; TrivialExists.
   destruct (Int.ltu i0 Int.iwordsize); 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/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 8a06433f..60c11dcb 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:
-- 
cgit