diff options
| -rw-r--r-- | cfrontend/Cop.v | 12 | ||||
| -rw-r--r-- | cfrontend/Cshmgen.v | 12 | ||||
| -rw-r--r-- | cfrontend/Cshmgenproof.v | 10 | ||||
| -rw-r--r-- | cfrontend/SimplLocalsproof.v | 5 | ||||
| -rw-r--r-- | lib/Floats.v | 84 |
5 files changed, 106 insertions, 17 deletions
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index 1148d09..a1860ec 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -127,10 +127,12 @@ Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int := | IBool, _ => if Int.eq i Int.zero then Int.zero else Int.one end. -Definition cast_int_float (si : signedness) (i: int) : float := - match si with - | Signed => Float.floatofint i - | Unsigned => Float.floatofintu i +Definition cast_int_float (si: signedness) (sz: floatsize) (i: int) : float := + match si, sz with + | Signed, F64 => Float.floatofint i + | Unsigned, F64 => Float.floatofintu i + | Signed, F32 => Float.singleofint i + | Unsigned, F32 => Float.singleofintu i end. Definition cast_float_int (si : signedness) (f: float) : option int := @@ -184,7 +186,7 @@ Definition sem_cast (v: val) (t1 t2: type) : option val := end | cast_case_i2f si1 sz2 => match v with - | Vint i => Some (Vfloat (cast_float_float sz2 (cast_int_float si1 i))) + | Vint i => Some (Vfloat (cast_int_float si1 sz2 i)) | _ => None end | cast_case_f2i sz2 si2 => diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index c8a030c..a303a7f 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -54,10 +54,12 @@ Definition make_floatconst (f: float) := Econst (Ofloatconst f). Definition make_longconst (f: int64) := Econst (Olongconst f). -Definition make_floatofint (e: expr) (sg: signedness) := - match sg with - | Signed => Eunop Ofloatofint e - | Unsigned => Eunop Ofloatofintu e +Definition make_floatofint (e: expr) (sg: signedness) (sz: floatsize) := + match sg, sz with + | Signed, F64 => Eunop Ofloatofint e + | Unsigned, F64 => Eunop Ofloatofintu e + | Signed, F32 => Eunop Osingleoffloat (Eunop Ofloatofint e) + | Unsigned, F32 => Eunop Osingleoffloat (Eunop Ofloatofintu e) end. Definition make_intoffloat (e: expr) (sg: signedness) := @@ -120,7 +122,7 @@ Definition make_cast (from to: type) (e: expr) := | cast_case_neutral => OK e | cast_case_i2i sz2 si2 => OK (make_cast_int e sz2 si2) | cast_case_f2f sz2 => OK (make_cast_float e sz2) - | cast_case_i2f si1 sz2 => OK (make_cast_float (make_floatofint e si1) sz2) + | cast_case_i2f si1 sz2 => OK (make_floatofint e si1 sz2) | cast_case_f2i sz2 si2 => OK (make_cast_int (make_intoffloat e si2) sz2 si2) | cast_case_l2l => OK e | cast_case_i2l si1 => OK (make_longofint e si1) diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 3d5bbba..24576fc 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -144,11 +144,15 @@ Proof. Qed. Lemma make_floatofint_correct: - forall a n sg e le m, + forall a n sg sz e le m, eval_expr ge e le m a (Vint n) -> - eval_expr ge e le m (make_floatofint a sg) (Vfloat(cast_int_float sg n)). + eval_expr ge e le m (make_floatofint a sg sz) (Vfloat(cast_int_float sg sz n)). Proof. - intros. unfold make_floatofint, cast_int_float. + intros. unfold make_floatofint, cast_int_float. + destruct sz. + destruct sg. + rewrite Float.singleofint_floatofint. econstructor. econstructor; eauto. simpl; reflexivity. auto. + rewrite Float.singleofintu_floatofintu. econstructor. econstructor; eauto. simpl; reflexivity. auto. destruct sg; econstructor; eauto. Qed. diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index ad8a06a..83e7375 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -286,7 +286,10 @@ Proof. destruct v; inv H. constructor. (* float *) destruct ty; simpl in H; try discriminate; destruct v; inv H. - constructor. apply cast_float_float_idem. + constructor. unfold cast_float_float, cast_int_float. + destruct f; destruct s; auto. + rewrite Float.singleofint_floatofint. apply Float.singleoffloat_idem. + rewrite Float.singleofintu_floatofintu. apply Float.singleoffloat_idem. constructor. unfold cast_float_float, cast_long_float. destruct f; destruct s; auto. apply Float.singleoflong_idem. apply Float.singleoflongu_idem. constructor. apply cast_float_float_idem. diff --git a/lib/Floats.v b/lib/Floats.v index 9df4106..7ae1705 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -180,6 +180,11 @@ Definition floatoflong (n:int64): float := (**r conversion from signed 64-bit in Definition floatoflongu (n:int64): float:= (**r conversion from unsigned 64-bit int *) binary_normalize64 (Int64.unsigned n) 0 false. +Definition singleofint (n:int): float := (**r conversion from signed 32-bit int to single-precision float *) + floatofbinary32 (binary_normalize32 (Int.signed n) 0 false). +Definition singleofintu (n:int): float:= (**r conversion from unsigned 32-bit int to single-precision float *) + floatofbinary32 (binary_normalize32 (Int.unsigned n) 0 false). + Definition singleoflong (n:int64): float := (**r conversion from signed 64-bit int to single-precision float *) floatofbinary32 (binary_normalize32 (Int64.signed n) 0 false). Definition singleoflongu (n:int64): float:= (**r conversion from unsigned 64-bit int to single-precision float *) @@ -524,7 +529,7 @@ Qed. Definition ox8000_0000 := Int.repr Int.half_modulus. (**r [0x8000_0000] *) Lemma round_exact: - forall n, -2^52 < n < 2^52 -> + forall n, -2^53 < n < 2^53 -> round radix2 (FLT_exp (3 - 1024 - 53) 53) (round_mode mode_NE) (Z2R n) = Z2R n. Proof. @@ -535,7 +540,7 @@ Proof. Qed. Lemma binary_normalize64_exact: - forall n, -2^52 < n < 2^52 -> + forall n, -2^53 < n < 2^53 -> B2R _ _ (binary_normalize64 n 0 false) = Z2R n /\ is_finite _ _ (binary_normalize64 n 0 false) = true. Proof. @@ -588,7 +593,7 @@ Proof. exfalso; now smart_omega. Qed. -Theorem Zoffloat_correct: +Lemma Zoffloat_correct: forall f, match Zoffloat f with | Some n => @@ -915,6 +920,79 @@ Local Transparent Int.repr Int64.repr. apply le_Z2R in H6; pose proof (Zabs_spec (Int.signed x)); exfalso; now smart_omega. Qed. +(** Conversions from 32-bit integers to single-precision floats can + be decomposed into a conversion to a double-precision float, + followed by a [singleoffloat] normalization. No double rounding occurs. *) + +Lemma is_finite_strict_ge_1: + forall (f: binary32), + is_finite _ _ f = true -> + (1 <= Rabs (B2R _ _ f))%R -> + is_finite_strict _ _ f = true. +Proof. + intros. destruct f; auto. simpl in H0. + change 0%R with (Z2R 0) in H0. + change 1%R with (Z2R 1) in H0. + rewrite <- Z2R_abs in H0. + exploit le_Z2R; eauto. +Qed. + +Lemma single_float_of_int: + forall n, + -2^53 < n < 2^53 -> + singleoffloat (binary_normalize64 n 0 false) = floatofbinary32 (binary_normalize32 n 0 false). +Proof. + intros. unfold singleoffloat. f_equal. + assert (EITHER: n = 0 \/ Z.abs n > 0) by (destruct n; compute; auto). + destruct EITHER as [EQ|GT]. + subst n; reflexivity. + exploit binary_normalize64_exact; eauto. intros [A B]. + destruct (binary_normalize64 n 0 false) as [ | | | s m e] eqn:B64; simpl in *. +- assert (0 = n) by (apply eq_Z2R; auto). subst n. simpl in GT. omegaContradiction. +- discriminate. +- discriminate. +- set (n1 := cond_Zopp s (Z.pos m)) in *. + generalize (binary_normalize32_correct n1 e s). + fold (binary_normalize32 n1 e s). intros C. + generalize (binary_normalize32_correct n 0 false). + fold (binary_normalize32 n 0 false). intros D. + assert (A': @F2R radix2 {| Fnum := n; Fexp := 0 |} = Z2R n). + { + unfold F2R. apply Rmult_1_r. + } + rewrite A in C. rewrite A' in D. + destruct (Rlt_bool + (Rabs + (round radix2 (FLT_exp (3 - 128 - 24) 24) (round_mode mode_NE) + (Z2R n))) (bpow radix2 128)). ++ destruct C as [C1 C2]; destruct D as [D1 D2]. + assert (1 <= Rabs (round radix2 (FLT_exp (3 - 128 - 24) 24) (round_mode mode_NE) (Z2R n)))%R. + { apply abs_round_ge_generic. + apply fexp_correct. red. omega. + apply valid_rnd_round_mode. + apply generic_format_bpow with (e := 0). compute. congruence. + rewrite <- Z2R_abs. change 1%R with (Z2R 1). apply Z2R_le. omega. } + apply B2R_inj. + apply is_finite_strict_ge_1; auto. rewrite C1; auto. + apply is_finite_strict_ge_1; auto. rewrite D1; auto. + congruence. ++ apply B2FF_inj. congruence. +Qed. + +Theorem singleofint_floatofint: + forall n, singleofint n = singleoffloat (floatofint n). +Proof. + intros. symmetry. apply single_float_of_int. + generalize (Int.signed_range n). smart_omega. +Qed. + +Theorem singleofintu_floatofintu: + forall n, singleofintu n = singleoffloat (floatofintu n). +Proof. + intros. symmetry. apply single_float_of_int. + generalize (Int.unsigned_range n). smart_omega. +Qed. + Global Opaque zero eq_dec neg abs singleoffloat intoffloat intuoffloat floatofint floatofintu add sub mul div cmp bits_of_double double_of_bits bits_of_single single_of_bits from_words. |