From 14a9bb4b267eeead8cd9503ee19e860a8bc0d763 Mon Sep 17 00:00:00 2001 From: xleroy 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 --- ia32/SelectOpproof.v | 26 +++++++++++++++++--------- 1 file changed, 17 insertions(+), 9 deletions(-) (limited to 'ia32/SelectOpproof.v') diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v index 59fed01..4279f29 100644 --- a/ia32/SelectOpproof.v +++ b/ia32/SelectOpproof.v @@ -835,10 +835,14 @@ 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_floatofint: forall le a x, @@ -875,9 +879,10 @@ Theorem eval_divf: Proof. intros; unfold divf; EvalOp. 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. @@ -889,10 +894,13 @@ Proof. 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. - fold im. 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_floatofintu: -- cgit v1.2.3