summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-07-08 08:38:02 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-07-08 08:38:02 +0000
commitbdac1f6aba5370b21b34c9ee12429c3920b3dffb (patch)
treebc81db2ee38bc44158a9032905830a76c888d04b
parent56257af93c1b0785d44e3feba9574e77250d420c (diff)
Revised handling of int->float conversions:
- introduce Float.floatofint{,u} and use it in the semantics of C - prove that it is equivalent to int->double conversion followed by double->float rounding, and use this fact to justify code generation in Cshmgen. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2294 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r--cfrontend/Cop.v12
-rw-r--r--cfrontend/Cshmgen.v12
-rw-r--r--cfrontend/Cshmgenproof.v10
-rw-r--r--cfrontend/SimplLocalsproof.v5
-rw-r--r--lib/Floats.v84
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.