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 | |
parent | b54721f58c2ecb65ce554d8b34f214d5121a2b0c (diff) | |
download | compcert-kvx-14a9bb4b267eeead8cd9503ee19e860a8bc0d763.tar.gz compcert-kvx-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
-rw-r--r-- | arm/ConstpropOp.v | 4 | ||||
-rw-r--r-- | arm/ConstpropOpproof.v | 2 | ||||
-rw-r--r-- | arm/Op.v | 5 | ||||
-rw-r--r-- | arm/SelectOpproof.v | 33 | ||||
-rw-r--r-- | backend/Cminor.v | 4 | ||||
-rw-r--r-- | backend/Selectionproof.v | 4 | ||||
-rw-r--r-- | cfrontend/Cminorgenproof.v | 4 | ||||
-rw-r--r-- | cfrontend/Csem.v | 7 | ||||
-rw-r--r-- | cfrontend/Cshmgenproof.v | 15 | ||||
-rw-r--r-- | common/Values.v | 4 | ||||
-rw-r--r-- | extraction/extraction.v | 1 | ||||
-rw-r--r-- | ia32/ConstpropOp.v | 4 | ||||
-rw-r--r-- | ia32/ConstpropOpproof.v | 2 | ||||
-rw-r--r-- | ia32/Op.v | 5 | ||||
-rw-r--r-- | ia32/SelectOpproof.v | 26 | ||||
-rw-r--r-- | lib/Floataux.ml | 8 | ||||
-rw-r--r-- | lib/Floats.v | 31 | ||||
-rw-r--r-- | powerpc/ConstpropOp.v | 4 | ||||
-rw-r--r-- | powerpc/ConstpropOpproof.v | 2 | ||||
-rw-r--r-- | powerpc/Op.v | 5 | ||||
-rw-r--r-- | powerpc/SelectOpproof.v | 31 |
21 files changed, 139 insertions, 62 deletions
diff --git a/arm/ConstpropOp.v b/arm/ConstpropOp.v index a56a5ef8..fa97c6c4 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 9778acef..3f98b881 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. @@ -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 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: diff --git a/backend/Cminor.v b/backend/Cminor.v index 4e57d3ce..a3a166c0 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -240,8 +240,8 @@ Definition eval_unop (op: unary_operation) (arg: val) : option val := | Onegf, Vfloat f1 => Some (Vfloat (Float.neg f1)) | Oabsf, Vfloat f1 => Some (Vfloat (Float.abs f1)) | Osingleoffloat, _ => Some (Val.singleoffloat arg) - | Ointoffloat, Vfloat f1 => Some (Vint (Float.intoffloat f1)) - | Ointuoffloat, Vfloat f1 => Some (Vint (Float.intuoffloat f1)) + | Ointoffloat, Vfloat f1 => option_map Vint (Float.intoffloat f1) + | Ointuoffloat, Vfloat f1 => option_map Vint (Float.intuoffloat f1) | Ofloatofint, Vint n1 => Some (Vfloat (Float.floatofint n1)) | Ofloatofintu, Vint n1 => Some (Vfloat (Float.floatofintu n1)) | _, _ => None diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index cb9f4fc5..d997015f 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -220,8 +220,8 @@ Proof. apply eval_negf; auto. apply eval_absf; auto. apply eval_singleoffloat; auto. - apply eval_intoffloat; auto. - apply eval_intuoffloat; auto. + remember (Float.intoffloat f) as oi; destruct oi; inv H0. eapply eval_intoffloat; eauto. + remember (Float.intuoffloat f) as oi; destruct oi; inv H0. eapply eval_intuoffloat; eauto. apply eval_floatofint; auto. apply eval_floatofintu; auto. Qed. diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 5b2ad9b5..480acbb9 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -1250,8 +1250,8 @@ Proof. inv H0; inv H; TrivialOp. inv H0; inv H; TrivialOp. inv H0; inv H; TrivialOp. - inv H0; inv H; TrivialOp. - inv H0; inv H; TrivialOp. + inv H0; inv H. destruct (Float.intoffloat f0); simpl in H1; inv H1. TrivialOp. + inv H0; inv H. destruct (Float.intuoffloat f0); simpl in H1; inv H1. TrivialOp. inv H0; inv H; TrivialOp. inv H0; inv H; TrivialOp. Qed. diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 742a969a..927cd69d 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -49,7 +49,7 @@ Definition cast_int_float (si : signedness) (i: int) : float := | Unsigned => Float.floatofintu i end. -Definition cast_float_int (si : signedness) (f: float) : int := +Definition cast_float_int (si : signedness) (f: float) : option int := match si with | Signed => Float.intoffloat f | Unsigned => Float.intuoffloat f @@ -75,9 +75,10 @@ Inductive cast : val -> type -> type -> val -> Prop := | cast_ii: forall i sz2 sz1 si1 si2, (**r int to int *) cast (Vint i) (Tint sz1 si1) (Tint sz2 si2) (Vint (cast_int_int sz2 si2 i)) - | cast_fi: forall f sz1 sz2 si2, (**r float to int *) + | cast_fi: forall f sz1 sz2 si2 i, (**r float to int *) + cast_float_int si2 f = Some i -> cast (Vfloat f) (Tfloat sz1) (Tint sz2 si2) - (Vint (cast_int_int sz2 si2 (cast_float_int si2 f))) + (Vint (cast_int_int sz2 si2 i)) | cast_if: forall i sz1 sz2 si1, (**r int to float *) cast (Vint i) (Tint sz1 si1) (Tfloat sz2) (Vfloat (cast_float_float sz2 (cast_int_float si1 i))) diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 4784e1ed..88f042de 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -361,8 +361,18 @@ Proof. destruct sg; econstructor; eauto. Qed. +Lemma make_intoffloat_correct: + forall e le m a sg f i, + eval_expr ge e le m a (Vfloat f) -> + cast_float_int sg f = Some i -> + eval_expr ge e le m (make_intoffloat a sg) (Vint i). +Proof. + unfold cast_float_int, make_intoffloat; intros. + destruct sg; econstructor; eauto; simpl; rewrite H0; auto. +Qed. + Hint Resolve make_intconst_correct make_floatconst_correct - make_floatofint_correct + make_floatofint_correct make_intoffloat_correct eval_Eunop eval_Ebinop: cshm. Hint Extern 2 (@eq trace _ _) => traceEq: cshm. @@ -650,7 +660,8 @@ Proof. (* cast_int_int *) destruct sz2; destruct si2; repeat econstructor; eauto with cshm. (* cast_float_int *) - destruct sz2; destruct si2; unfold make_intoffloat; repeat econstructor; eauto with cshm; simpl; auto. + exploit make_intoffloat_correct; eauto. intros A. + destruct sz2; destruct si2; eauto with cshm. (* cast_int_float *) destruct sz2; destruct si1; unfold make_floatofint; repeat econstructor; eauto with cshm; simpl; auto. (* cast_float_float *) diff --git a/common/Values.v b/common/Values.v index af242c93..ceff3339 100644 --- a/common/Values.v +++ b/common/Values.v @@ -117,13 +117,13 @@ Definition absf (v: val) : val := Definition intoffloat (v: val) : val := match v with - | Vfloat f => Vint (Float.intoffloat f) + | Vfloat f => match Float.intoffloat f with Some n => Vint n | None => Vundef end | _ => Vundef end. Definition intuoffloat (v: val) : val := match v with - | Vfloat f => Vint (Float.intuoffloat f) + | Vfloat f => match Float.intuoffloat f with Some n => Vint n | None => Vundef end | _ => Vundef end. diff --git a/extraction/extraction.v b/extraction/extraction.v index 8e3c1aa8..984bee05 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -30,6 +30,7 @@ Extract Inlined Constant Floats.float => "float". Extract Constant Floats.Float.zero => "0.". Extract Constant Floats.Float.neg => "( ~-. )". Extract Constant Floats.Float.abs => "abs_float". +Extract Constant Floats.Float.of_Z => "fun x -> assert false". Extract Constant Floats.Float.singleoffloat => "Floataux.singleoffloat". Extract Constant Floats.Float.intoffloat => "Floataux.intoffloat". Extract Constant Floats.Float.intuoffloat => "Floataux.intuoffloat". diff --git a/ia32/ConstpropOp.v b/ia32/ConstpropOp.v index 7dfa0465..815ba0e0 100644 --- a/ia32/ConstpropOp.v +++ b/ia32/ConstpropOp.v @@ -288,7 +288,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) | Ocmp c, vl => match eval_static_condition c vl with None => Unknown | Some b => I(if b then Int.one else Int.zero) end | _, _ => Unknown @@ -590,7 +590,7 @@ Definition eval_static_operation (op: operation) (vl: list approx) := | eval_static_operation_case38 n1 => F(Float.singleoffloat n1) | eval_static_operation_case39 n1 => - I(Float.intoffloat n1) + match Float.intoffloat n1 with Some x => I x | None => Unknown end | eval_static_operation_case41 n1 => F(Float.floatofint n1) | eval_static_operation_case43 c vl => diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v index ea904469..105a7bdf 100644 --- a/ia32/ConstpropOpproof.v +++ b/ia32/ConstpropOpproof.v @@ -178,6 +178,8 @@ Proof. rewrite <- H3. replace v0 with (Vfloat n1). reflexivity. congruence. + inv H4. destruct (Float.intoffloat f); inv H0. red; auto. + caseEq (eval_static_condition c vl0). intros. generalize (eval_static_condition_correct _ _ _ _ H H1). intro. rewrite H2 in H0. @@ -285,7 +285,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) | Ofloatofint, Vint n1 :: nil => Some (Vfloat (Float.floatofint n1)) | Ocmp c, _ => @@ -547,6 +547,7 @@ Proof. injection H0; intro; subst v; exact I. discriminate. simpl. eapply type_of_addressing_sound; eauto. 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. @@ -727,6 +728,7 @@ Proof. destruct (Int.ltu i Int.iwordsize); congruence. destruct (Int.ltu i Int.iwordsize); congruence. apply eval_addressing_weaken; auto. + 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. @@ -832,6 +834,7 @@ Proof. destruct (Int.ltu i Int.iwordsize); inv H0; TrivialExists. eapply eval_addressing_lessdef; eauto. exists (Val.singleoffloat v2); split. auto. apply Val.singleoffloat_lessdef; auto. + exists v1; split; auto. 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/ia32/SelectOpproof.v b/ia32/SelectOpproof.v index 59fed01d..4279f29d 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: diff --git a/lib/Floataux.ml b/lib/Floataux.ml index f0db1fa0..dfdd6ce9 100644 --- a/lib/Floataux.ml +++ b/lib/Floataux.ml @@ -19,10 +19,14 @@ let singleoffloat f = Int32.float_of_bits (Int32.bits_of_float f) let intoffloat f = - coqint_of_camlint (Int32.of_float f) + if f < 2147483648.0 (*2^31 *) && f > -2147483649.0 (* -2^31-1 *) + then Some (coqint_of_camlint (Int32.of_float f)) + else None let intuoffloat f = - coqint_of_camlint (Int64.to_int32 (Int64.of_float f)) + if f < 4294967296.0 (* 2^32 *) && f >= 0.0 + then Some (coqint_of_camlint (Int64.to_int32 (Int64.of_float f))) + else None let floatofint i = Int32.to_float (camlint_of_coqint i) diff --git a/lib/Floats.v b/lib/Floats.v index 6257bcc0..50712af2 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -31,13 +31,15 @@ Parameter zero: float. (**r the float [+0.0] *) Axiom eq_dec: forall (f1 f2: float), {f1 = f2} + {f1 <> f2}. +Parameter of_Z: Z -> float. (**r conversion from exact integers, for specification *) + (** Arithmetic operations *) Parameter neg: float -> float. (**r opposite (change sign) *) Parameter abs: float -> float. (**r absolute value (set sign to [+]) *) Parameter singleoffloat: float -> float. (**r conversion to single precision *) -Parameter intoffloat: float -> int. (**r conversion to signed 32-bit int *) -Parameter intuoffloat: float -> int. (**r conversion to unsigned 32-bit int *) +Parameter intoffloat: float -> option int. (**r conversion to signed 32-bit int *) +Parameter intuoffloat: float -> option int. (**r conversion to unsigned 32-bit int *) Parameter floatofint: int -> float. (**r conversion from signed 32-bit int *) Parameter floatofintu: int -> float. (**r conversion from unsigned 32-bit int *) @@ -116,6 +118,18 @@ Axiom bits_of_singleoffloat: Axiom singleoffloat_of_bits: forall b, singleoffloat (single_of_bits b) = single_of_bits b. +(** Range of conversions from floats to ints. *) + +Axiom intuoffloat_defined: + forall f, + cmp Clt f (of_Z Int.modulus) = true /\ cmp Cge f zero = true + <-> exists n, intuoffloat f = Some n. + +Axiom intoffloat_defined: + forall f, + cmp Clt f (of_Z Int.half_modulus) = true /\ cmp Cgt f (of_Z (- Int.half_modulus - 1)) = true + <-> exists n, intoffloat f = Some n. + (** Conversions between floats and unsigned ints can be defined in terms of conversions between floats and signed ints. (Most processors provide only the latter, forcing the compiler @@ -140,11 +154,16 @@ Axiom intuoffloat_intoffloat_1: intuoffloat x = intoffloat x. Axiom intuoffloat_intoffloat_2: - forall x, + forall x n, + cmp Clt x (floatofintu ox8000_0000) = false -> + intuoffloat x = Some n -> + intoffloat (sub x (floatofintu ox8000_0000)) = Some (Int.sub n ox8000_0000). + +Axiom intuoffloat_intoffloat_3: + forall x n, cmp Clt x (floatofintu ox8000_0000) = false -> - intuoffloat x = - Int.add (intoffloat (sub x (floatofintu ox8000_0000))) - ox8000_0000. + intoffloat (sub x (floatofintu ox8000_0000)) = Some n -> + intuoffloat x = Some (Int.add n ox8000_0000). (** Conversions from ints to floats can be defined as bitwise manipulations over the in-memory representation. This is what the PowerPC port does. 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: |