Parsing, testing infrastructure, and tests for f32 and f64

ml-proto/README.md

@@ -197,7 +197,8 @@ script: <cmd>*
 cmd:
   <module>                                             ;; define, validate, and initialize module
   ( invoke <name> <expr>* )                            ;; invoke export and print result
-  ( assert_eq (invoke <name> <expr>* ) <expr> )        ;; assert expected results of invocation
+  ( assert_return (invoke <name> <expr>* ) <expr> )    ;; assert return with expected result of invocation
+  ( assert_return_nan (invoke <name> <expr>* ))        ;; assert return with floating point nan result of invocation
   ( assert_trap (invoke <name> <expr>* ) <failure> )   ;; assert invocation traps with given failure string
   ( assert_invalid <module> <failure> )                ;; assert invalid module with given failure string
 ```

ml-proto/TestingTodo.md

@@ -17,28 +17,28 @@ Operator semantics:
  - test that promote/demote, sext/trunc, zext/trunc is bit-preserving if not NaN
  - ~~test that clz/ctz handle zero~~
  - test that numbers slightly outside of the int32 range round into the int32 range in floating-to-int32 conversion
- - test that neg, abs, copysign, reinterpretcast, store+load, set+get, preserve the sign bit and significand bits of NaN and don't canonicalize
+ - ~~test that neg, abs, copysign, reinterpretcast, store+load, set+get, preserve the sign bit and significand bits of NaN and don't canonicalize~~
  - ~~test that shifts don't mask their shift count. 32 is particularly nice to test.~~
  - test that `page_size` returns something sane [(power of 2?)](https://github.com/WebAssembly/design/pull/296)
  - test that arithmetic operands are evaluated left-to-right
  - ~~test that add/sub/mul/wrap/wrapping-store silently wrap on overflow~~
  - ~~test that sdiv/udiv/srem/urem trap on divide-by-zero~~
  - ~~test that sdiv traps on overflow~~
  - ~~test that srem doesn't trap when the corresponding sdiv would overflow~~
- - test that float-to-integer conversion traps on overflow and invalid
+ - ~~test that float-to-integer conversion traps on overflow and invalid~~
  - ~~test that unsigned operations are properly unsigned~~
 
 Floating point semantics:
- - test for round-to-nearest rounding
- - test for ties-to-even rounding
- - test that all operations with floating point inputs correctly handle all their NaN, -0, 0, Infinity, and -Infinity special cases
- - test that all operations that can overflow produce Infinity and with the correct sign
- - test that all operations that can divide by zero produce Infinity with the correct sign
- - test that all operations that can have an invalid produce NaN
+ - ~~test for round-to-nearest rounding~~
+ - ~~test for ties-to-even rounding~~
+ - ~~test that all operations with floating point inputs correctly handle all their NaN, -0, 0, Infinity, and -Infinity special cases~~
+ - ~~test that all operations that can overflow produce Infinity and with the correct sign~~
+ - ~~test that all operations that can divide by zero produce Infinity with the correct sign~~
+ - ~~test that all operations that can have an invalid produce NaN~~
  - test that all operations that can have underflow behave [correctly](https://github.com/WebAssembly/design/issues/148)
- - test that nearestint doesn't do JS-style Math.round or C-style round(3) rounding
- - test that signalling NaN doesn't cause weirdness
- - test that signalling/quiet NaNs can have sign bits and payloads in literals
+ - ~~test that nearestint doesn't do JS-style Math.round or C-style round(3) rounding~~
+ - ~~test that signalling NaN doesn't cause weirdness~~
+ - ~~test that signalling/quiet NaNs can have sign bits and payloads in literals~~
  - test that conversion from int32/int64 to float32 rounds correctly
 
 Linear memory semantics:
@@ -86,8 +86,8 @@ Misc x86 optimizer bait:
  - test that oeq handles NaN right in if, if-else, and setcc cases
 
 Misc x87-isms:
- - test for invalid Precision-Control-style x87 math
- - test for invalid -ffloat-store-style x87 math
+ - ~~test for invalid Precision-Control-style x87 math~~
+ - ~~test for invalid -ffloat-store-style x87 math~~
  - test for evaluating intermediate results at greater precision
  - test for loading and storing NaNs
 

ml-proto/host/lexer.mll

@@ -90,10 +90,16 @@ let tick = '\''
 let escape = ['n''t''\\''\'''\"']
 let character = [^'"''\\''\n'] | '\\'escape | '\\'hexdigit hexdigit
 
-let num = ('+' | '-')? digit+
-let hexnum = ('+' | '-')? "0x" hexdigit+
+let sign = ('+' | '-')?
+let num = sign digit+
+let hexnum = sign "0x" hexdigit+
 let int = num | hexnum
-let float = (num '.' digit+) | num ('.' digit+)? ('e' | 'E') num
+let float = (num '.' digit+)
+          | num ('.' digit+)? ('e' | 'E') num
+          | sign "0x" hexdigit+ '.'? hexdigit* 'p' sign digit+
+          | sign "infinity"
+          | sign "nan"
+          | sign "nan(0x" hexdigit+ ")"
 let text = '"' character* '"'
 let name = '$' (letter | digit | '_' | tick | symbol)+
 
@@ -247,7 +253,8 @@ rule token = parse
   | "table" { TABLE }
 
   | "assert_invalid" { ASSERTINVALID }
-  | "assert_eq" { ASSERTEQ }
+  | "assert_return" { ASSERTRETURN }
+  | "assert_return_nan" { ASSERTRETURNNAN }
   | "assert_trap" { ASSERTTRAP }
   | "invoke" { INVOKE }
 

ml-proto/host/parser.mly

@@ -38,7 +38,9 @@ let literal at s t =
     | Types.Int64Type -> Values.Int64 (I64.of_string s) @@ at
     | Types.Float32Type -> Values.Float32 (F32.of_string s) @@ at
     | Types.Float64Type -> Values.Float64 (F64.of_string s) @@ at
-  with _ -> Error.error at "constant out of range"
+  with
+    | Failure reason -> Error.error at ("constant out of range: " ^ reason)
+    | _ -> Error.error at "constant out of range"
 
 
 (* Symbolic variables *)
@@ -99,7 +101,7 @@ let anon_label c = {c with labels = VarMap.map ((+) 1) c.labels}
 %token CONST UNARY BINARY COMPARE CONVERT
 %token FUNC PARAM RESULT LOCAL MODULE MEMORY SEGMENT IMPORT EXPORT TABLE
 %token PAGESIZE MEMORYSIZE RESIZEMEMORY
-%token ASSERTINVALID ASSERTEQ ASSERTTRAP INVOKE
+%token ASSERTINVALID ASSERTRETURN ASSERTRETURNNAN ASSERTTRAP INVOKE
 %token EOF
 
 %token<string> INT
@@ -341,8 +343,10 @@ cmd :
   | LPAR ASSERTINVALID module_ TEXT RPAR { AssertInvalid ($3, $4) @@ at() }
   | LPAR INVOKE TEXT expr_list RPAR
     { Invoke ($3, $4 (c0 ())) @@ at() }
-  | LPAR ASSERTEQ LPAR INVOKE TEXT expr_list RPAR expr RPAR
-    { AssertEq ($5, $6 (c0 ()), $8 (c0 ())) @@ at() }
+  | LPAR ASSERTRETURN LPAR INVOKE TEXT expr_list RPAR expr RPAR
+    { AssertReturn ($5, $6 (c0 ()), $8 (c0 ())) @@ at() }
+  | LPAR ASSERTRETURNNAN LPAR INVOKE TEXT expr_list RPAR RPAR
+    { AssertReturnNaN ($5, $6 (c0 ())) @@ at() }
   | LPAR ASSERTTRAP LPAR INVOKE TEXT expr_list RPAR TEXT RPAR
     { AssertTrap ($5, $6 (c0 ()), $8) @@ at() }
 ;

ml-proto/host/script.ml

@@ -11,7 +11,8 @@ and command' =
   | Define of Ast.module_
   | AssertInvalid of Ast.module_ * string
   | Invoke of string * Ast.expr list
-  | AssertEq of string * Ast.expr list * Ast.expr
+  | AssertReturn of string * Ast.expr list * Ast.expr
+  | AssertReturnNaN of string * Ast.expr list
   | AssertTrap of string * Ast.expr list * string
 
 type script = command list
@@ -30,6 +31,24 @@ let eval_args es at =
     | None -> Error.error at "unexpected () value" in
   List.map reject_none evs
 
+let get_module at = match !current_module with
+  | Some m -> m
+  | None -> Error.error at "no module defined to invoke"
+
+let show_value label v = begin
+  print_string (label ^ ": ");
+  Print.print_value v
+end
+
+let show_result got_v = begin
+  show_value "Result" got_v
+end
+
+let show_result_expect got_v expect_v = begin
+  show_result got_v;
+  show_value "Expect" expect_v
+end
+
 let assert_error f err re at =
   match f () with
   | exception Error.Error (_, s) ->
@@ -58,37 +77,71 @@ let run_command cmd =
 
   | Invoke (name, es) ->
     trace "Invoking...";
-    let m = match !current_module with
-      | Some m -> m
-      | None -> Error.error cmd.at "no module defined to invoke"
-    in
+    let m = get_module cmd.at in
     let vs = eval_args es cmd.at in
     let v = Eval.invoke m name vs in
     if v <> None then Print.print_value v
 
-  | AssertEq (name, arg_es, expect_e) ->
-    trace "Assert invoking...";
-    let m = match !current_module with
-      | Some m -> m
-      | None -> Error.error cmd.at "no module defined to invoke"
-    in
+  | AssertReturn (name, arg_es, expect_e) ->
+    let open Values in
+    trace "AssertReturn invoking...";
+    let m = get_module cmd.at in
     let arg_vs = eval_args arg_es cmd.at in
     let got_v = Eval.invoke m name arg_vs in
     let expect_v = Eval.eval expect_e in
-    if got_v <> expect_v then begin
-      print_string "Result: ";
-      Print.print_value got_v;
-      print_string "Expect: ";
-      Print.print_value expect_v;
-      Error.error cmd.at "assertion failed"
-    end
+    (match got_v, expect_v with
+     | Some Int32 got_i32, Some Int32 expect_i32 ->
+       if got_i32 <> expect_i32 then begin
+         show_result_expect got_v expect_v;
+         Error.error cmd.at "assert_return i32 operands are not equal"
+       end
+     | Some Int64 got_i64, Some Int64 expect_i64 ->
+       if got_i64 <> expect_i64 then begin
+         show_result_expect got_v expect_v;
+         Error.error cmd.at "assert_return i64 operands are not equal"
+       end
+     | Some Float32 got_f32, Some Float32 expect_f32 ->
+       if (F32.to_bits got_f32) <> (F32.to_bits expect_f32) then begin
+         show_result_expect got_v expect_v;
+         Error.error cmd.at
+                     "assert_return f32 operands have different bit patterns"
+       end
+     | Some Float64 got_f64, Some Float64 expect_f64 ->
+       if (F64.to_bits got_f64) <> (F64.to_bits expect_f64) then begin
+         show_result_expect got_v expect_v;
+         Error.error cmd.at
+                     "assert_return f64 operands have different bit patterns"
+       end
+     | _, _ -> begin
+         show_result_expect got_v expect_v;
+         Error.error cmd.at "assert_return operands must be the same type"
+       end)
+
+  | AssertReturnNaN (name, arg_es) ->
+    let open Values in
+    trace "AssertReturnNaN invoking...";
+    let m = get_module cmd.at in
+    let arg_vs = eval_args arg_es cmd.at in
+    let got_v = Eval.invoke m name arg_vs in
+    (match got_v with
+     | Some Float32 got_f32 ->
+       if (F32.eq got_f32 got_f32) then begin
+         show_result got_v;
+         Error.error cmd.at "assert_return_nan f32 operand is not a NaN"
+       end
+     | Some Float64 got_f64 ->
+       if (F64.eq got_f64 got_f64) then begin
+         show_result got_v;
+         Error.error cmd.at "assert_return_nan f64 operand is not a NaN"
+       end
+     | _ -> begin
+         show_result got_v;
+         Error.error cmd.at "assert_return_nan operand must be f32 or f64"
+       end)
 
   | AssertTrap (name, es, re) ->
-    trace "Assert trap invoking...";
-    let m = match !current_module with
-      | Some m -> m
-      | None -> Error.error cmd.at "no module defined to invoke"
-    in
+    trace "AssertTrap invoking...";
+    let m = get_module cmd.at in
     let vs = eval_args es cmd.at in
     assert_error (fun () -> Eval.invoke m name vs) "trap" re cmd.at
 
@@ -99,7 +152,8 @@ let dry_command cmd =
     if !Flags.print_sig then Print.print_module_sig m
   | AssertInvalid _ -> ()
   | Invoke _ -> ()
-  | AssertEq _ -> ()
+  | AssertReturn _ -> ()
+  | AssertReturnNaN _ -> ()
   | AssertTrap _ -> ()
 
 let run script =

ml-proto/host/script.mli

@@ -7,7 +7,8 @@ and command' =
   | Define of Ast.module_
   | AssertInvalid of Ast.module_ * string
   | Invoke of string * Ast.expr list
-  | AssertEq of string * Ast.expr list * Ast.expr
+  | AssertReturn of string * Ast.expr list * Ast.expr
+  | AssertReturnNaN of string * Ast.expr list
   | AssertTrap of string * Ast.expr list * string
 
 type script = command list

ml-proto/spec/f32.ml

@@ -8,6 +8,7 @@ type t = int32
 type bits = int32
 
 (* TODO: Do something meaningful with nondeterminism *)
+let bare_nan = 0x7f800000l
 let nondeterministic_nan = 0x7fc0f0f0l
 
 let of_float = Int32.bits_of_float
@@ -89,6 +90,37 @@ 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: 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_signless_string x len =
+  if x <> "nan" &&
+     (len > 7) &&
+     (String.sub x 0 6) = "nan(0x" && (String.get x (len - 1)) = ')' then
+    (let s = Int32.of_string (String.sub x 4 ((len - 5))) in
+     if s = Int32.zero then
+       raise (Failure "nan payload must not be zero")
+     else if Int32.logand s bare_nan <> Int32.zero then
+       raise (Failure "nan payload must not overlap with exponent bits")
+     else if s < Int32.zero then
+       raise (Failure "nan payload must not overlap with sign bit")
+     else
+       Int32.logor s bare_nan)
+  else
+    (* TODO: OCaml's float_of_string is insufficient *)
+    of_float (float_of_string x)
+
+let of_string x =
+  let len = String.length x in
+  if len > 0 && (String.get x 0) = '-' then
+    neg (of_signless_string (String.sub x 1 (len - 1)) (len - 1))
+  else if len > 0 && (String.get x 0) = '+' then
+    of_signless_string (String.sub x 1 (len - 1)) (len - 1)
+  else
+    of_signless_string x len
+
+let to_string x =
+  (if x < Int32.zero then "-" else "") ^ let a = abs x in
+  let af = arith_of_bits a in
+  if af <> af then
+   ("nan(0x" ^ (Printf.sprintf "%lx" (abs (Int32.logxor bare_nan a))) ^ ")")
+  else
+    (* TODO: OCaml's string_of_float is insufficient *)
+    string_of_float (to_float a)

ml-proto/spec/f64.ml

@@ -8,6 +8,7 @@ type t = int64
 type bits = int64
 
 (* TODO: Do something meaningful with nondeterminism *)
+let bare_nan = 0x7ff0000000000000L
 let nondeterministic_nan = 0x7fff0f0f0f0f0f0fL
 
 let of_float = Int64.bits_of_float
@@ -89,6 +90,37 @@ 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: 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_signless_string x len =
+  if x <> "nan" &&
+     (len > 7) &&
+     (String.sub x 0 6) = "nan(0x" && (String.get x (len - 1)) = ')' then
+    (let s = Int64.of_string (String.sub x 4 ((len - 5))) in
+     if s = Int64.zero then
+       raise (Failure "nan payload must not be zero")
+     else if Int64.logand s bare_nan <> Int64.zero then
+       raise (Failure "nan payload must not overlap with exponent bits")
+     else if s < Int64.zero then
+       raise (Failure "nan payload must not overlap with sign bit")
+     else
+       Int64.logor s bare_nan)
+  else
+    (* TODO: OCaml's float_of_string is insufficient *)
+    of_float (float_of_string x)
+
+let of_string x =
+  let len = String.length x in
+  if len > 0 && (String.get x 0) = '-' then
+    neg (of_signless_string (String.sub x 1 (len - 1)) (len - 1))
+  else if len > 0 && (String.get x 0) = '+' then
+    of_signless_string (String.sub x 1 (len - 1)) (len - 1)
+  else
+    of_signless_string x len
+
+let to_string x =
+  (if x < Int64.zero then "-" else "") ^ let a = abs x in
+  let af = arith_of_bits a in
+  if af <> af then
+   ("nan(0x" ^ (Printf.sprintf "%Lx" (abs (Int64.logxor bare_nan a))) ^ ")")
+  else
+    (* TODO: OCaml's string_of_float is insufficient *)
+    string_of_float (to_float a)