diff options
| -rw-r--r-- | Changelog | 5 | ||||
| -rw-r--r-- | cfrontend/C2C.ml | 50 | ||||
| -rw-r--r-- | cparser/.depend | 4 | ||||
| -rw-r--r-- | cparser/C.mli | 9 | ||||
| -rw-r--r-- | cparser/Cabs.ml | 10 | ||||
| -rw-r--r-- | cparser/Ceval.ml | 30 | ||||
| -rw-r--r-- | cparser/Cprint.ml | 20 | ||||
| -rw-r--r-- | cparser/Cutil.ml | 9 | ||||
| -rw-r--r-- | cparser/Cutil.mli | 4 | ||||
| -rw-r--r-- | cparser/Elab.ml | 35 | ||||
| -rw-r--r-- | cparser/Lexer.mll | 46 | ||||
| -rw-r--r-- | cparser/Parser.mly | 3 | ||||
| -rw-r--r-- | flocq/Appli/Fappli_IEEE.v | 8 | ||||
| -rw-r--r-- | lib/Floats.v | 42 |
14 files changed, 180 insertions, 95 deletions
@@ -1,6 +1,11 @@ Release 1.12 ======================== +Improvements in confidence: +- Floating-point literals are now parsed and converted to IEEE-754 binary + FP numbers using a provably-correct conversion function implemented on + top of the Flocq library. + Language semantics: - The "&&" and "||" operators are now primitive in CompCert C and are given explicit semantic rules, instead of being expressed in terms diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 9a93017..c659b86 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -26,6 +26,7 @@ open Ctypes open Cop open Csyntax open Initializers +open Floats (** Record useful information about global variables and functions, and associate it with the corresponding atoms. *) @@ -331,6 +332,51 @@ let first_class_value env ty = | C.TInt((C.ILongLong|C.IULongLong), _) -> false | _ -> true +(** Floating point constants *) + +let z_of_str hex str fst = + let res = ref BinInt.Z0 in + let base = if hex then 16l else 10l in + for i = fst to String.length str - 1 do + let d = int_of_char str.[i] in + let d = + if hex && d >= int_of_char 'a' && d <= int_of_char 'f' then + d - int_of_char 'a' + 10 + else if hex && d >= int_of_char 'A' && d <= int_of_char 'F' then + d - int_of_char 'A' + 10 + else + d - int_of_char '0' + in + let d = Int32.of_int d in + assert (d >= 0l && d < base); + res := BinInt.coq_Zplus + (BinInt.coq_Zmult (z_of_camlint base) !res) (z_of_camlint d) + done; + !res + +let convertFloat f kind = + let mant = z_of_str f.C.hex (f.C.intPart ^ f.C.fracPart) 0 in + match mant with + | BinInt.Z0 -> Float.zero + | BinInt.Zpos mant -> + + let sgExp = match f.C.exp.[0] with '+' | '-' -> true | _ -> false in + let exp = z_of_str false f.C.exp (if sgExp then 1 else 0) in + let exp = if f.C.exp.[0] = '-' then BinInt.coq_Zopp exp else exp in + let shift_exp = + Int32.of_int ((if f.C.hex then 4 else 1) * String.length f.C.fracPart) in + let exp = BinInt.coq_Zminus exp (z_of_camlint shift_exp) in + + let base = positive_of_camlint (if f.C.hex then 16l else 10l) in + + begin match kind with + | FFloat -> + Float.build_from_parsed32 base mant exp + | FDouble | FLongDouble -> + Float.build_from_parsed64 base mant exp + end + | BinInt.Zneg _ -> assert false + (** Expressions *) let ezero = Eval(Vint(coqint_of_camlint 0l), type_int32s) @@ -354,10 +400,10 @@ let rec convertExpr env e = if k = C.ILongLong || k = C.IULongLong then unsupported "'long long' integer literal"; Eval(Vint(convertInt i), ty) - | C.EConst(C.CFloat(f, k, _)) -> + | C.EConst(C.CFloat(f, k)) -> if k = C.FLongDouble && not !Clflags.option_flongdouble then unsupported "'long double' floating-point literal"; - Eval(Vfloat(coqfloat_of_camlfloat f), ty) + Eval(Vfloat(convertFloat f k), ty) | C.EConst(C.CStr s) -> let ty = typeStringLiteral s in Evalof(Evar(name_for_string_literal env s, ty), ty) diff --git a/cparser/.depend b/cparser/.depend index 63cd2cb..0b38315 100644 --- a/cparser/.depend +++ b/cparser/.depend @@ -46,8 +46,8 @@ Env.cmo: C.cmi Env.cmi Env.cmx: C.cmi Env.cmi GCC.cmo: Cutil.cmi C.cmi Builtins.cmi GCC.cmi GCC.cmx: Cutil.cmx C.cmi Builtins.cmx GCC.cmi -Lexer.cmo: Parser.cmi Parse_aux.cmi Cabshelper.cmo Lexer.cmi -Lexer.cmx: Parser.cmx Parse_aux.cmx Cabshelper.cmx Lexer.cmi +Lexer.cmo: Parser.cmi Parse_aux.cmi Cabshelper.cmo Cabs.cmo Lexer.cmi +Lexer.cmx: Parser.cmx Parse_aux.cmx Cabshelper.cmx Cabs.cmx Lexer.cmi Machine.cmo: Machine.cmi Machine.cmx: Machine.cmi Main.cmo: Parse.cmi GCC.cmi Cprint.cmi Builtins.cmi diff --git a/cparser/C.mli b/cparser/C.mli index 52f02c4..8e73bc5 100644 --- a/cparser/C.mli +++ b/cparser/C.mli @@ -52,9 +52,16 @@ type fkind = (** Constants *) +type float_cst = { + hex : bool; + intPart : string; + fracPart : string; + exp : string; +} + type constant = | CInt of int64 * ikind * string (* as it appeared in the source *) - | CFloat of float * fkind * string (* as it appeared in the source *) + | CFloat of float_cst * fkind | CStr of string | CWStr of int64 list | CEnum of ident * int64 (* enum tag, integer value *) diff --git a/cparser/Cabs.ml b/cparser/Cabs.ml index a2bb512..23d3643 100644 --- a/cparser/Cabs.ml +++ b/cparser/Cabs.ml @@ -267,9 +267,17 @@ and expression = | MEMBEROFPTR of expression * string | GNU_BODY of block +and floatInfo = { + isHex_FI:bool; + integer_FI:string option; + fraction_FI:string option; + exponent_FI:string option; + suffix_FI:char option; +} + and constant = | CONST_INT of string (* the textual representation *) - | CONST_FLOAT of string (* the textual representaton *) + | CONST_FLOAT of floatInfo | CONST_CHAR of int64 list | CONST_WCHAR of int64 list | CONST_STRING of string diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml index 4fc01e5..621fbbf 100644 --- a/cparser/Ceval.ml +++ b/cparser/Ceval.ml @@ -51,27 +51,19 @@ let normalize_int n ik = (* Reduce n to the range of representable floats of the given kind *) -let normalize_float f fk = - match fk with - | FFloat -> Int32.float_of_bits (Int32.bits_of_float f) - | FDouble -> f - | FLongDouble -> raise Notconst (* cannot accurately compute on this type *) - type value = | I of int64 - | F of float | S of string | WS of int64 list let boolean_value v = match v with | I n -> n <> 0L - | F n -> n <> 0.0 | S _ | WS _ -> true let constant = function | CInt(v, ik, _) -> I (normalize_int v ik) - | CFloat(v, fk, _) -> F (normalize_float v fk) + | CFloat(v, fk) -> raise Notconst | CStr s -> S s | CWStr s -> WS s | CEnum(id, v) -> I v @@ -87,22 +79,12 @@ let cast env ty_to ty_from v = if boolean_value v then I 1L else I 0L | TInt(ik, _), I n -> I(normalize_int n ik) - | TInt(ik, _), F n -> - I(normalize_int (Int64.of_float n) ik) | TInt(ik, _), (S _ | WS _) -> if sizeof_ikind ik >= !config.sizeof_ptr then v else raise Notconst - | TFloat(fk, _), F n -> - F(normalize_float n fk) - | TFloat(fk, _), I n -> - if is_signed env ty_from - then F(normalize_float (Int64.to_float n) fk) - else F(normalize_float (int64_unsigned_to_float n) fk) | TPtr(ty, _), I n -> I (normalize_int n ptr_t_ikind) - | TPtr(ty, _), F n -> - if n = 0.0 then I 0L else raise Notconst | TPtr(ty, _), (S _ | WS _) -> v | _, _ -> @@ -112,9 +94,7 @@ let unop env op tyres ty v = let res = match op, tyres, v with | Ominus, TInt _, I n -> I (Int64.neg n) - | Ominus, TFloat _, F n -> F (-. n) | Oplus, TInt _, I n -> I n - | Oplus, TFloat _, F n -> F n | Olognot, _, _ -> if boolean_value v then I 0L else I 1L | Onot, _, I n -> I (Int64.lognot n) | _ -> raise Notconst @@ -128,8 +108,6 @@ let comparison env direction ptraction tyop ty1 v1 ty2 v2 = if is_signed env tyop then direction (compare n1 n2) 0 else direction (int64_unsigned_compare n1 n2) 0 (* including pointers *) - | F n1, F n2 -> - direction (compare n1 n2) 0 | (S _ | WS _), I 0L -> begin match ptraction with None -> raise Notconst | Some b -> b end | I 0L, (S _ | WS _) -> @@ -147,7 +125,6 @@ let binop env op tyop tyres ty1 v1 ty2 v2 = if is_arith_type env ty1 && is_arith_type env ty2 then begin match cast env tyop ty1 v1, cast env tyop ty2 v2 with | I n1, I n2 -> I (Int64.add n1 n2) - | F n1, F n2 -> F (n1 +. n2) | _, _ -> raise Notconst end else raise Notconst @@ -155,14 +132,12 @@ let binop env op tyop tyres ty1 v1 ty2 v2 = if is_arith_type env ty1 && is_arith_type env ty2 then begin match cast env tyop ty1 v1, cast env tyop ty2 v2 with | I n1, I n2 -> I (Int64.sub n1 n2) - | F n1, F n2 -> F (n1 -. n2) | _, _ -> raise Notconst end else raise Notconst | Omul -> begin match cast env tyop ty1 v1, cast env tyop ty2 v2 with | I n1, I n2 -> I (Int64.mul n1 n2) - | F n1, F n2 -> F (n1 *. n2) | _, _ -> raise Notconst end | Odiv -> @@ -171,7 +146,6 @@ let binop env op tyop tyres ty1 v1 ty2 v2 = if n2 = 0L then raise Notconst else if is_signed env tyop then I (Int64.div n1 n2) else I (int64_unsigned_div n1 n2) - | F n1, F n2 -> F (n1 /. n2) | _, _ -> raise Notconst end | Omod -> @@ -261,6 +235,7 @@ let rec expr env e = if boolean_value (expr env e1) then cast env e.etyp e2.etyp (expr env e2) else cast env e.etyp e3.etyp (expr env e3) + (* | ECast(TInt (_, _), EConst (CFloat (_, _))) -> TODO *) | ECast(ty, e1) -> cast env ty e1.etyp (expr env e1) | ECall _ -> @@ -277,7 +252,6 @@ let constant_expr env ty e = try match unroll env ty, cast env ty e.etyp (expr env e) with | TInt(ik, _), I n -> Some(CInt(n, ik, "")) - | TFloat(fk, _), F n -> Some(CFloat(n, fk, "")) | TPtr(_, _), I 0L -> Some(CInt(0L, IInt, "")) | TPtr(_, _), S s -> Some(CStr s) | TPtr(_, _), WS s -> Some(CWStr s) diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml index 2924c3d..2548f3b 100644 --- a/cparser/Cprint.ml +++ b/cparser/Cprint.ml @@ -45,16 +45,16 @@ let const pp = function | IUInt -> fprintf pp "U" | _ -> () end - | CFloat(v, fk, s) -> - if s <> "" then - fprintf pp "%s" s - else begin - fprintf pp "%.18g" v; - match fk with - | FFloat -> fprintf pp "F" - | FLongDouble -> fprintf pp "L" - | _ -> () - end + | CFloat(v, fk) -> + if v.hex then + fprintf pp "0x%s.%sP%s" v.intPart v.fracPart v.exp + else + fprintf pp "%s.%sE%s" v.intPart v.fracPart v.exp; + begin match fk with + | FFloat -> fprintf pp "F" + | FLongDouble -> fprintf pp "L" + | FDouble -> () + end | CStr s -> fprintf pp "\""; for i = 0 to String.length s - 1 do diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 4856c01..d84b9c9 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -625,7 +625,7 @@ let enum_ikind = IInt let type_of_constant = function | CInt(_, ik, _) -> TInt(ik, []) - | CFloat(_, fk, _) -> TFloat(fk, []) + | CFloat(_, fk) -> TFloat(fk, []) | CStr _ -> TPtr(TInt(IChar, []), []) (* XXX or array? const? *) | CWStr _ -> TPtr(TInt(wchar_ikind, []), []) (* XXX or array? const? *) | CEnum(_, _) -> TInt(IInt, []) @@ -708,10 +708,11 @@ let valid_cast env tfrom tto = let intconst v ik = { edesc = EConst(CInt(v, ik, "")); etyp = TInt(ik, []) } -(* Construct a float constant *) +(* Construct the 0 float constant of double type *) -let floatconst v fk = - { edesc = EConst(CFloat(v, fk, "")); etyp = TFloat(fk, []) } +let floatconst0 = + { edesc = EConst(CFloat({hex=false; intPart="0"; fracPart="0"; exp="0"}, FDouble)); + etyp = TFloat(FDouble, []) } (* Construct the literal "0" with void * type *) diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 3c39b99..6488117 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -165,8 +165,8 @@ val fundef_typ: fundef -> typ val intconst : int64 -> ikind -> exp (* Build expression for given integer constant. *) -val floatconst : float -> fkind -> exp - (* Build expression for given float constant. *) +val floatconst0 : exp + (* Build expression for (double)0. *) val nullconst : exp (* Expression for [(void * ) 0] *) val eaddrof : exp -> exp diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 2473cf2..0e7b549 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -200,20 +200,19 @@ let elab_int_constant loc s0 = in (v, ty) -let elab_float_constant loc s0 = - let s = String.uppercase s0 in - (* Determine type and chop suffix *) - let (s, ty) = - if has_suffix s "L" then - (chop_last s 1, FLongDouble) - else if has_suffix s "F" then - (chop_last s 1, FFloat) - else - (s, FDouble) in - (* Convert to Caml float - XXX loss of precision for long double *) - let v = - try float_of_string s - with Failure _ -> error loc "bad float literal '%s'" s0; 0.0 in +let elab_float_constant loc f = + let ty = match f.suffix_FI with + | Some 'l' | Some 'L' -> FLongDouble + | Some 'f' | Some 'F' -> FFloat + | None -> FDouble + | _ -> assert false (* The lexer should not accept anything else. *) + in + let v = { + hex=f.isHex_FI; + intPart=begin match f.integer_FI with Some s -> s | None -> "0" end; + fracPart=begin match f.fraction_FI with Some s -> s | None -> "0" end; + exp=begin match f.exponent_FI with Some s -> s | None -> "0" end } + in (v, ty) let elab_char_constant loc sz cl = @@ -238,9 +237,9 @@ let elab_constant loc = function | CONST_INT s -> let (v, ik) = elab_int_constant loc s in CInt(v, ik, s) - | CONST_FLOAT s -> - let (v, fk) = elab_float_constant loc s in - CFloat(v, fk, s) + | CONST_FLOAT f -> + let (v, fk) = elab_float_constant loc f in + CFloat(v, fk) | CONST_CHAR cl -> let (v, ik) = elab_char_constant loc 1 cl in CInt(v, ik, "") @@ -1386,7 +1385,7 @@ let rec elab_init loc env ty ile = | (NO_INIT :: ile1) | ([] as ile1) -> begin match unroll env ty with | TInt _ -> (Init_single (intconst 0L IInt), ile1) - | TFloat _ -> (Init_single (floatconst 0.0 FDouble), ile1) + | TFloat _ -> (Init_single floatconst0, ile1) | TPtr _ -> (Init_single nullconst, ile1) | _ -> assert false end diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index 424252e..0820e4e 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -365,9 +365,8 @@ let letter = ['a'- 'z' 'A'-'Z'] let usuffix = ['u' 'U'] let lsuffix = "l"|"L"|"ll"|"LL" -let intsuffix = lsuffix | usuffix | usuffix lsuffix | lsuffix usuffix +let intsuffix = lsuffix | usuffix | usuffix lsuffix | lsuffix usuffix | usuffix ? "i64" - let hexprefix = '0' ['x' 'X'] @@ -375,21 +374,19 @@ let intnum = decdigit+ intsuffix? let octnum = '0' octdigit+ intsuffix? let hexnum = hexprefix hexdigit+ intsuffix? -let exponent = ['e' 'E']['+' '-']? decdigit+ -let fraction = '.' decdigit+ -let decfloat = (intnum? fraction) - |(intnum exponent) - |(intnum? fraction exponent) - | (intnum '.') - | (intnum '.' exponent) - -let hexfraction = hexdigit* '.' hexdigit+ | hexdigit+ -let binexponent = ['p' 'P'] ['+' '-']? decdigit+ -let hexfloat = hexprefix hexfraction binexponent - | hexprefix hexdigit+ binexponent - -let floatsuffix = ['f' 'F' 'l' 'L'] -let floatnum = (decfloat | hexfloat) floatsuffix? +let floating_suffix = ['f' 'F' 'l' 'L'] as suffix +let exponent_part = ['e' 'E']((['+' '-']? decdigit+) as expo) +let fractional_constant = ((decdigit+ as intpart)? '.' (decdigit+ as frac)) + |((decdigit+ as intpart) '.') +let decimal_floating_constant = + (fractional_constant exponent_part? floating_suffix?) + |((decdigit+ as intpart) exponent_part floating_suffix?) +let binary_exponent_part = ['p' 'P']((['+' '-']? decdigit+) as expo) +let hexadecimal_fractional_constant = ((hexdigit+ as intpart)? '.' (hexdigit+ as frac)) + |((hexdigit+ as intpart) '.') +let hexadecimal_floating_constant = + (hexprefix hexadecimal_fractional_constant binary_exponent_part floating_suffix?) + |(hexprefix (hexdigit+ as intpart) binary_exponent_part floating_suffix?) let ident = (letter|'_'|'$')(letter|decdigit|'_'|'$')* let blank = [' ' '\t' '\012' '\r']+ @@ -425,7 +422,20 @@ rule initial = CST_STRING (str lexbuf, currentLoc lexbuf) } | "L\"" { (* weimer: wchar_t string literal *) CST_WSTRING(str lexbuf, currentLoc lexbuf) } -| floatnum {CST_FLOAT (Lexing.lexeme lexbuf, currentLoc lexbuf)} +| decimal_floating_constant + {CST_FLOAT ({Cabs.isHex_FI = false; + Cabs.integer_FI = intpart; + Cabs.fraction_FI = frac; + Cabs.exponent_FI = expo; + Cabs.suffix_FI = suffix}, + currentLoc lexbuf)} +| hexadecimal_floating_constant + {CST_FLOAT ({Cabs.isHex_FI = true; + Cabs.integer_FI = intpart; + Cabs.fraction_FI = frac; + Cabs.exponent_FI = Some expo; + Cabs.suffix_FI = suffix}, + currentLoc lexbuf)} | hexnum {CST_INT (Lexing.lexeme lexbuf, currentLoc lexbuf)} | octnum {CST_INT (Lexing.lexeme lexbuf, currentLoc lexbuf)} | intnum {CST_INT (Lexing.lexeme lexbuf, currentLoc lexbuf)} diff --git a/cparser/Parser.mly b/cparser/Parser.mly index 0eebb84..83b1984 100644 --- a/cparser/Parser.mly +++ b/cparser/Parser.mly @@ -199,14 +199,13 @@ let transformOffsetOf (speclist, dtype) member = let sizeofType = [SpecType Tunsigned], JUSTBASE in let resultExpr = CAST (sizeofType, SINGLE_INIT addrExpr) in resultExpr - %} %token <string * Cabs.cabsloc> IDENT %token <int64 list * Cabs.cabsloc> CST_CHAR %token <int64 list * Cabs.cabsloc> CST_WCHAR %token <string * Cabs.cabsloc> CST_INT -%token <string * Cabs.cabsloc> CST_FLOAT +%token <Cabs.floatInfo * Cabs.cabsloc> CST_FLOAT %token <string * Cabs.cabsloc> NAMED_TYPE /* Each character is its own list element, and the terminating nul is not diff --git a/flocq/Appli/Fappli_IEEE.v b/flocq/Appli/Fappli_IEEE.v index 79f6a4c..63b150f 100644 --- a/flocq/Appli/Fappli_IEEE.v +++ b/flocq/Appli/Fappli_IEEE.v @@ -1309,7 +1309,7 @@ Definition Fdiv_core_binary m1 e1 m2 e2 := (q, e', new_location m2 r loc_Exact). Lemma Bdiv_correct_aux : - forall m sx mx ex (Hx : bounded mx ex = true) sy my ey (Hy : bounded my ey = true), + forall m sx mx ex sy my ey, let x := F2R (Float radix2 (cond_Zopp sx (Zpos mx)) ex) in let y := F2R (Float radix2 (cond_Zopp sy (Zpos my)) ey) in let z := @@ -1325,7 +1325,7 @@ Lemma Bdiv_correct_aux : else z = binary_overflow m (xorb sx sy). Proof. -intros m sx mx ex Hx sy my ey Hy. +intros m sx mx ex sy my ey. replace (Fdiv_core_binary (Zpos mx) ex (Zpos my) ey) with (Fdiv_core radix2 prec (Zpos mx) ex (Zpos my) ey). 2: now unfold Fdiv_core_binary ; rewrite 2!Zdigits2_Zdigits. refine (_ (Fdiv_core_correct radix2 prec (Zpos mx) ex (Zpos my) ey _ _ _)) ; try easy. @@ -1418,8 +1418,8 @@ Definition Bdiv m x y := | B754_finite sx _ _ _, B754_zero sy => B754_infinity (xorb sx sy) | B754_zero sx, B754_finite sy _ _ _ => B754_zero (xorb sx sy) | B754_zero sx, B754_zero sy => B754_nan - | B754_finite sx mx ex Hx, B754_finite sy my ey Hy => - FF2B _ (proj1 (Bdiv_correct_aux m sx mx ex Hx sy my ey Hy)) + | B754_finite sx mx ex _, B754_finite sy my ey _ => + FF2B _ (proj1 (Bdiv_correct_aux m sx mx ex sy my ey)) end. Theorem Bdiv_correct : diff --git a/lib/Floats.v b/lib/Floats.v index edb6d6b..556cc41 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -66,6 +66,13 @@ Definition binary_normalize64_correct (m e:Z) (s:bool) := binary_normalize_correct 53 1024 eq_refl eq_refl mode_NE m e s. Global Opaque binary_normalize64_correct. +Definition binary_normalize32 (m e:Z) (s:bool) : binary32 := + binary_normalize 24 128 eq_refl eq_refl mode_NE m e s. + +Definition binary_normalize32_correct (m e:Z) (s:bool) := + binary_normalize_correct 24 128 eq_refl eq_refl mode_NE m e s. +Global Opaque binary_normalize32_correct. + Definition floatofbinary32 (f: binary32) : float := (**r single precision embedding in double precision *) match f with | B754_nan => B754_nan _ _ @@ -81,13 +88,12 @@ Definition binary32offloat (f: float) : binary32 := (**r conversion to single pr | B754_infinity s => B754_infinity _ _ s | B754_zero s => B754_zero _ _ s | B754_finite s m e _ => - binary_normalize 24 128 eq_refl eq_refl mode_NE (cond_Zopp s (Zpos m)) e s + binary_normalize32 (cond_Zopp s (Zpos m)) e s end. Definition singleoffloat (f: float): float := (**r conversion to single precision, embedded in double *) floatofbinary32 (binary32offloat f). - Definition Zoffloat (f:float): option Z := (**r conversion to Z *) match f with | B754_finite s m (Zpos e) _ => Some (cond_Zopp s (Zpos m) * Zpower_pos radix2 e) @@ -117,6 +123,35 @@ Definition intuoffloat (f:float): option int := (**r conversion to unsigned 32-b | None => None end. +(* Functions used to parse floats *) +Program Definition build_from_parsed + (prec:Z) (emax:Z) (prec_gt_0 :Prec_gt_0 prec) (Hmax:prec < emax) + (base:positive) (intPart:positive) (expPart:Z) := + match expPart return _ with + | Z0 => + binary_normalize prec emax prec_gt_0 Hmax mode_NE (Zpos intPart) Z0 false + | Zpos p => + binary_normalize prec emax prec_gt_0 Hmax mode_NE ((Zpos intPart) * Zpower_pos (Zpos base) p) Z0 false + | Zneg p => + let exp := Zpower_pos (Zpos base) p in + match exp return 0 < exp -> _ with + | Zneg _ | Z0 => _ + | Zpos p => + fun _ => + FF2B prec emax _ (proj1 (Bdiv_correct_aux prec emax prec_gt_0 Hmax mode_NE false intPart Z0 false p Z0)) + end _ + end. +Next Obligation. +apply Zpower_pos_gt_0. +reflexivity. +Qed. + +Definition build_from_parsed64 (base:positive) (intPart:positive) (expPart:Z) : float := + build_from_parsed 53 1024 eq_refl eq_refl base intPart expPart. + +Definition build_from_parsed32 (base:positive) (intPart:positive) (expPart:Z) : float := + floatofbinary32 (build_from_parsed 24 128 eq_refl eq_refl base intPart expPart). + Definition floatofint (n:int): float := (**r conversion from signed 32-bit int *) binary_normalize64 (Int.signed n) 0 false. Definition floatofintu (n:int): float:= (**r conversion from unsigned 32-bit int *) @@ -260,9 +295,10 @@ Proof. specialize (H eq_refl); destruct H. destruct (floatofbinary32 (B754_finite 24 128 s m e e0)) as [ | | |s1 m1 e1]; try discriminate. unfold binary32offloat. - pose proof (binary_normalize_correct 24 128 eq_refl eq_refl mode_NE (cond_Zopp s1 (Zpos m1)) e1 s1). + pose proof (binary_normalize32_correct (cond_Zopp s1 (Zpos m1)) e1 s1). unfold B2R at 2 in H0; cbv iota zeta beta in H0; rewrite <- H0, round_generic in H1. rewrite Rlt_bool_true in H1. + unfold binary_normalize32. apply B2R_inj; intuition; match goal with [|- _ _ _ ?f = true] => destruct f end; try discriminate. symmetry in H2; apply F2R_eq_0_reg in H2; destruct s; discriminate. reflexivity. |