From 2a0168fea37b68ad14e2cb60bf215111e49d4870 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 23 Jul 2014 08:54:56 +0000 Subject: 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 --- flocq/Appli/Fappli_IEEE_bits.v | 51 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) (limited to 'flocq') 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 -- cgit v1.2.3