Merge pull request #40 from WebAssembly/float-bits

wasm-compatible float32 and float64 arithmetic

ml-proto/src/Makefile

@@ -5,7 +5,7 @@
 NAME = wasm
 INCLUDES = -I host -I given -I spec
 MODULES = \
-  host/flags given/lib given/source spec/error \
+  host/flags given/lib given/source given/float32 given/float64 spec/error \
   spec/types spec/values spec/memory spec/ast \
   spec/check spec/arithmetic spec/eval \
   host/print host/builtins host/script \

ml-proto/src/given/float32.ml

@@ -0,0 +1,95 @@
+(* WebAssembly-compatible float32 implementation *)
+
+(*
+ * We represent float32 as its bits in an int32 so that we can be assured that
+ * all the bits of NaNs are preserved in all cases where we require them to be.
+ *)
+type t = int32
+type bits = int32
+
+(* TODO: Do something meaningful with nondeterminism *)
+let nondeterministic_nan = 0x7fc0f0f0l
+
+let of_float = Int32.bits_of_float
+let to_float = Int32.float_of_bits
+
+(* TODO: OCaml's string_of_float and float_of_string are insufficient *)
+let of_string x = of_float (float_of_string x)
+let to_string x = string_of_float (to_float x)
+
+let of_bits x = x
+let to_bits x = x
+
+(* Most arithmetic ops that return NaN return a nondeterministic NaN *)
+let arith_of_bits = to_float
+let bits_of_arith f = if f <> f then nondeterministic_nan else of_float f
+
+let zero = of_float 0.0
+
+let add x y = bits_of_arith ((arith_of_bits x) +. (arith_of_bits y))
+let sub x y = bits_of_arith ((arith_of_bits x) -. (arith_of_bits y))
+let mul x y = bits_of_arith ((arith_of_bits x) *. (arith_of_bits y))
+let div x y = bits_of_arith ((arith_of_bits x) /. (arith_of_bits y))
+
+let sqrt  x = bits_of_arith (Pervasives.sqrt (arith_of_bits x))
+
+let ceil  x = bits_of_arith (Pervasives.ceil  (arith_of_bits x))
+let floor x = bits_of_arith (Pervasives.floor (arith_of_bits x))
+
+let trunc x =
+  let xf = arith_of_bits x in
+  (* preserve the sign of zero *)
+  if xf = 0.0 then x else
+  (* trunc is either ceil or floor depending on which one is toward zero *)
+  let f = if xf < 0.0 then Pervasives.ceil xf else Pervasives.floor xf in
+  bits_of_arith f
+
+let nearest x =
+  let xf = arith_of_bits x in
+  (* preserve the sign of zero *)
+  if xf = 0.0 then x else
+  (* nearest is either ceil or floor depending on which is nearest or even *)
+  let u = Pervasives.ceil xf in
+  let d = Pervasives.floor xf in
+  let um = abs_float (xf -. u) in
+  let dm = abs_float (xf -. d) in
+  let u_or_d = um < dm || ((um = dm) && (mod_float u 2.0 = 0.0)) in
+  let f = if u_or_d then u else d in
+  bits_of_arith f
+
+let min x y =
+  let xf = arith_of_bits x in
+  let yf = arith_of_bits y in
+  (* min(-0, 0) is -0 *)
+  if xf = 0.0 && yf = 0.0 then (Int32.logor x y) else
+  if xf < yf then x else
+  if xf > yf then y else
+  nondeterministic_nan
+
+let max x y =
+  let xf = arith_of_bits x in
+  let yf = arith_of_bits y in
+  (* max(-0, 0) is 0 *)
+  if xf = 0.0 && yf = 0.0 then (Int32.logand x y) else
+  if xf > yf then x else
+  if xf < yf then y else
+  nondeterministic_nan
+
+(* abs, neg, and copysign are purely bitwise operations, even on NaN values *)
+let abs x =
+  Int32.logand x Int32.max_int
+
+let neg x =
+  Int32.logxor x Int32.min_int
+
+let copysign x y =
+  Int32.logor (abs x) (Int32.logand y Int32.min_int)
+
+let eq x y = (arith_of_bits x) =  (arith_of_bits y)
+let ne x y = (arith_of_bits x) <> (arith_of_bits y)
+let lt x y = (arith_of_bits x) <  (arith_of_bits y)
+let gt x y = (arith_of_bits x) >  (arith_of_bits y)
+let le x y = (arith_of_bits x) <= (arith_of_bits y)
+let ge x y = (arith_of_bits x) >= (arith_of_bits y)
+
+(* TODO: type conversion functions *)

ml-proto/src/given/float32.mli

@@ -0,0 +1,34 @@
+(* WebAssembly-compatible float32 implementation *)
+
+type t
+type bits = int32
+
+val of_float : float -> t
+val to_float : t -> float
+val of_bits : bits -> t
+val to_bits : t -> bits
+val of_string : string -> t
+val to_string : t -> string
+
+val zero : t
+
+val add : t -> t -> t
+val sub : t -> t -> t
+val mul : t -> t -> t
+val div : t -> t -> t
+val sqrt : t -> t
+val min : t -> t -> t
+val max : t -> t -> t
+val ceil : t -> t
+val floor : t -> t
+val trunc : t -> t
+val nearest : t -> t
+val abs : t -> t
+val neg : t -> t
+val copysign : t -> t -> t
+val eq : t -> t -> bool
+val ne : t -> t -> bool
+val lt : t -> t -> bool
+val le : t -> t -> bool
+val gt : t -> t -> bool
+val ge : t -> t -> bool

ml-proto/src/given/float64.ml

@@ -0,0 +1,95 @@
+(* WebAssembly-compatible float64 implementation *)
+
+(*
+ * We represent float64 as its bits in an int64 so that we can be assured that
+ * all the bits of NaNs are preserved in all cases where we require them to be.
+ *)
+type t = int64
+type bits = int64
+
+(* TODO: Do something meaningful with nondeterminism *)
+let nondeterministic_nan = 0x7fff0f0f0f0f0f0fL
+
+let of_float = Int64.bits_of_float
+let to_float = Int64.float_of_bits
+
+(* TODO: OCaml's string_of_float and float_of_string are insufficient *)
+let of_string x = of_float (float_of_string x)
+let to_string x = string_of_float (to_float x)
+
+let of_bits x = x
+let to_bits x = x
+
+(* Most arithmetic ops that return NaN return a nondeterministic NaN *)
+let arith_of_bits = to_float
+let bits_of_arith f = if f <> f then nondeterministic_nan else of_float f
+
+let zero = of_float 0.0
+
+let add x y = bits_of_arith ((arith_of_bits x) +. (arith_of_bits y))
+let sub x y = bits_of_arith ((arith_of_bits x) -. (arith_of_bits y))
+let mul x y = bits_of_arith ((arith_of_bits x) *. (arith_of_bits y))
+let div x y = bits_of_arith ((arith_of_bits x) /. (arith_of_bits y))
+
+let sqrt  x = bits_of_arith (Pervasives.sqrt (arith_of_bits x))
+
+let ceil  x = bits_of_arith (Pervasives.ceil  (arith_of_bits x))
+let floor x = bits_of_arith (Pervasives.floor (arith_of_bits x))
+
+let trunc x =
+  let xf = arith_of_bits x in
+  (* preserve the sign of zero *)
+  if xf = 0.0 then x else
+  (* trunc is either ceil or floor depending on which one is toward zero *)
+  let f = if xf < 0.0 then Pervasives.ceil xf else Pervasives.floor xf in
+  bits_of_arith f
+
+let nearest x =
+  let xf = arith_of_bits x in
+  (* preserve the sign of zero *)
+  if xf = 0.0 then x else
+  (* nearest is either ceil or floor depending on which is nearest or even *)
+  let u = Pervasives.ceil xf in
+  let d = Pervasives.floor xf in
+  let um = abs_float (xf -. u) in
+  let dm = abs_float (xf -. d) in
+  let u_or_d = um < dm || ((um = dm) && (mod_float u 2.0 = 0.0)) in
+  let f = if u_or_d then u else d in
+  bits_of_arith f
+
+let min x y =
+  let xf = arith_of_bits x in
+  let yf = arith_of_bits y in
+  (* min(-0, 0) is -0 *)
+  if xf = 0.0 && yf = 0.0 then (Int64.logor x y) else
+  if xf < yf then x else
+  if xf > yf then y else
+  nondeterministic_nan
+
+let max x y =
+  let xf = arith_of_bits x in
+  let yf = arith_of_bits y in
+  (* max(-0, 0) is 0 *)
+  if xf = 0.0 && yf = 0.0 then (Int64.logand x y) else
+  if xf > yf then x else
+  if xf < yf then y else
+  nondeterministic_nan
+
+(* abs, neg, and copysign are purely bitwise operations, even on NaN values *)
+let abs x =
+  Int64.logand x Int64.max_int
+
+let neg x =
+  Int64.logxor x Int64.min_int
+
+let copysign x y =
+  Int64.logor (abs x) (Int64.logand y Int64.min_int)
+
+let eq x y = (arith_of_bits x) =  (arith_of_bits y)
+let ne x y = (arith_of_bits x) <> (arith_of_bits y)
+let lt x y = (arith_of_bits x) <  (arith_of_bits y)
+let gt x y = (arith_of_bits x) >  (arith_of_bits y)
+let le x y = (arith_of_bits x) <= (arith_of_bits y)
+let ge x y = (arith_of_bits x) >= (arith_of_bits y)
+
+(* TODO: type conversion functions *)

ml-proto/src/given/float64.mli

@@ -0,0 +1,34 @@
+(* WebAssembly-compatible float64 implementation *)
+
+type t
+type bits = int64
+
+val of_float : float -> t
+val to_float : t -> float
+val of_bits : bits -> t
+val to_bits : t -> bits
+val of_string : string -> t
+val to_string : t -> string
+
+val zero : t
+
+val add : t -> t -> t
+val sub : t -> t -> t
+val mul : t -> t -> t
+val div : t -> t -> t
+val sqrt : t -> t
+val min : t -> t -> t
+val max : t -> t -> t
+val ceil : t -> t
+val floor : t -> t
+val trunc : t -> t
+val nearest : t -> t
+val abs : t -> t
+val neg : t -> t
+val copysign : t -> t -> t
+val eq : t -> t -> bool
+val ne : t -> t -> bool
+val lt : t -> t -> bool
+val le : t -> t -> bool
+val gt : t -> t -> bool
+val ge : t -> t -> bool

ml-proto/src/host/parser.mly

@@ -36,9 +36,8 @@ let literal at s t =
     match t with
     | Types.Int32Type -> Values.Int32 (Int32.of_string s) @@ at
     | Types.Int64Type -> Values.Int64 (Int64.of_string s) @@ at
-    | Types.Float32Type ->
-      Values.Float32 (Values.float32 (float_of_string s)) @@ at
-    | Types.Float64Type -> Values.Float64 (float_of_string s) @@ at
+    | Types.Float32Type -> Values.Float32 (Float32.of_string s) @@ at
+    | Types.Float64Type -> Values.Float64 (Float64.of_string s) @@ at
   with _ -> Error.error at "constant out of range"