From 14a9bb4b267eeead8cd9503ee19e860a8bc0d763 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 28 Oct 2010 14:56:39 +0000 Subject: 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 --- lib/Floataux.ml | 8 ++++++-- lib/Floats.v | 31 +++++++++++++++++++++++++------ 2 files changed, 31 insertions(+), 8 deletions(-) (limited to 'lib') diff --git a/lib/Floataux.ml b/lib/Floataux.ml index f0db1fa..dfdd6ce 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 6257bcc..50712af 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. -- cgit v1.2.3