diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-10-28 14:56:39 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-10-28 14:56:39 +0000 |
commit | 14a9bb4b267eeead8cd9503ee19e860a8bc0d763 (patch) | |
tree | c70dda532a974a7b62969c6b199b80d65784dc91 /arm/SelectOpproof.v | |
parent | b54721f58c2ecb65ce554d8b34f214d5121a2b0c (diff) | |
download | compcert-14a9bb4b267eeead8cd9503ee19e860a8bc0d763.tar.gz compcert-14a9bb4b267eeead8cd9503ee19e860a8bc0d763.zip |
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
Diffstat (limited to 'arm/SelectOpproof.v')
-rw-r--r-- | arm/SelectOpproof.v | 33 |
1 files changed, 21 insertions, 12 deletions
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: |