summaryrefslogtreecommitdiff
path: root/flocq/Appli
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-07-23 08:54:56 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-07-23 08:54:56 +0000
commit2a0168fea37b68ad14e2cb60bf215111e49d4870 (patch)
tree2f59373790d8ce3a5df66ef7a692271cf0666c6c /flocq/Appli
parent00805153cf9b88aa07cc6694b17d93f5ba2e7de8 (diff)
Merge of "newspilling" branch:
- Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'flocq/Appli')
-rw-r--r--flocq/Appli/Fappli_IEEE_bits.v51
1 files changed, 51 insertions, 0 deletions
diff --git a/flocq/Appli/Fappli_IEEE_bits.v b/flocq/Appli/Fappli_IEEE_bits.v
index a41fba9..937e8d4 100644
--- a/flocq/Appli/Fappli_IEEE_bits.v
+++ b/flocq/Appli/Fappli_IEEE_bits.v
@@ -248,6 +248,57 @@ discriminate.
now apply Zlt_0_le_0_pred.
Qed.
+Theorem bits_of_binary_float_range:
+ forall x, (0 <= bits_of_binary_float x < 2^(mw+ew+1))%Z.
+Proof.
+ intros.
+Local Open Scope Z_scope.
+ assert (J: forall s m e,
+ 0 <= m < 2^mw -> 0 <= e < 2^ew ->
+ 0 <= join_bits s m e < 2^(mw+ew+1)).
+ {
+ intros. unfold join_bits.
+ set (se := (if s then 2 ^ ew else 0) + e).
+ assert (0 <= se < 2^(ew+1)).
+ { rewrite (Zpower_plus radix2) by omega. change (radix2^1) with 2. simpl.
+ unfold se. destruct s; omega. }
+ assert (0 <= se * 2^mw <= (2^(ew+1) - 1) * 2^mw).
+ { split. apply Zmult_gt_0_le_0_compat; omega.
+ apply Zmult_le_compat_r; omega. }
+ rewrite Z.mul_sub_distr_r in H2.
+ replace (mw + ew + 1) with ((ew + 1) + mw) by omega.
+ rewrite (Zpower_plus radix2) by omega. simpl. omega.
+ }
+ assert (D: forall p n, Z.of_nat (S (digits2_Pnat p)) <= n ->
+ 0 <= Z.pos p < 2^n).
+ {
+ intros.
+ generalize (digits2_Pnat_correct p). simpl. rewrite ! Zpower_nat_Z. intros [A B].
+ split. zify; omega. eapply Zlt_le_trans. eassumption.
+ apply (Zpower_le radix2); auto.
+ }
+ destruct x; unfold bits_of_binary_float.
+- apply J; omega.
+- apply J; omega.
+- destruct n as [pl pl_range]. apply Z.ltb_lt in pl_range.
+ apply J. apply D. unfold prec, Z_of_nat' in pl_range; omega. omega.
+- unfold bounded in e0. apply Bool.andb_true_iff in e0; destruct e0 as [A B].
+ apply Z.leb_le in B.
+ unfold canonic_mantissa, FLT_exp in A. apply Zeq_bool_eq in A.
+ assert (G: Z.of_nat (S (digits2_Pnat m)) <= prec) by (zify; omega).
+ assert (M: emin <= e) by (unfold emin; zify; omega).
+ generalize (Zle_bool_spec (2^mw) (Z.pos m)); intro SPEC; inversion SPEC.
+ + apply J.
+ * split. omega. generalize (D _ _ G). unfold prec.
+ rewrite (Zpower_plus radix2) by omega.
+ change (radix2^1) with 2. simpl radix_val. omega.
+ * split. omega. unfold emin. replace (2^ew) with (2 * emax). omega.
+ symmetry. replace ew with (1 + (ew - 1)) by omega.
+ apply (Zpower_plus radix2); omega.
+ + apply J. zify; omega. omega.
+Local Close Scope Z_scope.
+Qed.
+
Definition binary_float_of_bits_aux x :=
let '(sx, mx, ex) := split_bits x in
if Zeq_bool ex 0 then