diff --git a/ml-proto/host/lexer.mll b/ml-proto/host/lexer.mll index 228aef0f4d..57ae850f7c 100644 --- a/ml-proto/host/lexer.mll +++ b/ml-proto/host/lexer.mll @@ -101,7 +101,7 @@ let float = | sign "0x" hexdigit+ '.'? hexdigit* 'p' sign digit+ | sign "infinity" | sign "nan" - | sign "nan(0x" hexdigit+ ")" + | sign "nan:0x" hexdigit+ let text = '"' character* '"' let name = '$' (letter | digit | '_' | tick | symbol)+ @@ -242,6 +242,7 @@ rule token = parse | (ixx as t)".select" { SELECT ( intop t Int32Op.Select Int64Op.Select) } | (fxx as t)".select" { SELECT ( floatop t Float32Op.Select Float64Op.Select) } + | "unreachable" { UNREACHABLE } | "page_size" { PAGE_SIZE } | "memory_size" { MEMORY_SIZE } | "grow_memory" { GROW_MEMORY } diff --git a/ml-proto/host/parser.mly b/ml-proto/host/parser.mly index 36f8b673fc..8d8ec1c134 100644 --- a/ml-proto/host/parser.mly +++ b/ml-proto/host/parser.mly @@ -165,7 +165,7 @@ let implicit_decl c t at = %token CONST UNARY BINARY COMPARE CONVERT %token FUNC TYPE PARAM RESULT LOCAL %token MODULE MEMORY SEGMENT IMPORT EXPORT TABLE -%token PAGE_SIZE MEMORY_SIZE GROW_MEMORY HAS_FEATURE +%token UNREACHABLE PAGE_SIZE MEMORY_SIZE GROW_MEMORY HAS_FEATURE %token ASSERT_INVALID ASSERT_RETURN ASSERT_RETURN_NAN ASSERT_TRAP INVOKE %token EOF @@ -292,6 +292,7 @@ expr1 : | SELECT expr expr expr { fun c -> select ($1, $2 c, $3 c, $4 c) } | COMPARE expr expr { fun c -> compare ($1, $2 c, $3 c) } | CONVERT expr { fun c -> convert ($1, $2 c) } + | UNREACHABLE { fun c -> unreachable } | PAGE_SIZE { fun c -> host (PageSize, []) } | MEMORY_SIZE { fun c -> host (MemorySize, []) } | GROW_MEMORY expr { fun c -> host (GrowMemory, [$2 c]) } diff --git a/ml-proto/spec/ast.ml b/ml-proto/spec/ast.ml index 0b1bf7bddb..72f56ee085 100644 --- a/ml-proto/spec/ast.ml +++ b/ml-proto/spec/ast.ml @@ -104,6 +104,7 @@ and expr' = | Select of selop * expr * expr * expr (* branchless conditional *) | Compare of relop * expr * expr (* arithmetic comparison *) | Convert of cvt * expr (* conversion *) + | Unreachable (* trap *) | Host of hostop * expr list (* host interaction *) diff --git a/ml-proto/spec/check.ml b/ml-proto/spec/check.ml index f979020928..0dc2e29ddb 100644 --- a/ml-proto/spec/check.ml +++ b/ml-proto/spec/check.ml @@ -218,6 +218,9 @@ let rec check_expr c et e = check_expr c (Some t1) e1; check_type (Some t) et e.at + | Unreachable -> + () + | Host (hostop, es) -> let ({ins; out}, hasmem) = type_hostop hostop in if hasmem then diff --git a/ml-proto/spec/eval.ml b/ml-proto/spec/eval.ml index cb9cb25f33..ebf43e3e74 100644 --- a/ml-proto/spec/eval.ml +++ b/ml-proto/spec/eval.ml @@ -253,6 +253,9 @@ let rec eval_expr (c : config) (e : expr) = (try Some (Arithmetic.eval_cvt cvt v1) with exn -> arithmetic_error e.at e1.at e1.at exn) + | Unreachable -> + Trap.error e.at "unreachable executed" + | Host (hostop, es) -> let vs = List.map (eval_expr c) es in eval_hostop c hostop vs e.at diff --git a/ml-proto/spec/float.ml b/ml-proto/spec/float.ml index 1e326fdcb0..d57805600f 100644 --- a/ml-proto/spec/float.ml +++ b/ml-proto/spec/float.ml @@ -143,9 +143,9 @@ struct 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 = Rep.of_string (String.sub x 4 ((len - 5))) in + (len > 6) && + (String.sub x 0 6) = "nan:0x" then + (let s = Rep.of_string (String.sub x 4 (len - 4)) in if s = Rep.zero then raise (Failure "nan payload must not be zero") else if Rep.logand s bare_nan <> Rep.zero then @@ -172,7 +172,7 @@ struct let a = abs x in let af = arith_of_bits a in if af <> af then - ("nan(0x" ^ Rep.print_nan_significand_digits a ^ ")") + ("nan:0x" ^ Rep.print_nan_significand_digits a) else (* TODO: OCaml's string_of_float is insufficient *) string_of_float (to_float a) diff --git a/ml-proto/spec/sugar.ml b/ml-proto/spec/sugar.ml index db136a3bfc..da02fcbb84 100644 --- a/ml-proto/spec/sugar.ml +++ b/ml-proto/spec/sugar.ml @@ -107,6 +107,9 @@ let compare (relop, e1, e2) = let convert (cvt, e) = Convert (cvt, e) +let unreachable = + Unreachable + let host (hostop, es) = Host (hostop, es) diff --git a/ml-proto/spec/sugar.mli b/ml-proto/spec/sugar.mli index 91789a65d3..4666e831b3 100644 --- a/ml-proto/spec/sugar.mli +++ b/ml-proto/spec/sugar.mli @@ -31,6 +31,7 @@ val binary : binop * expr * expr -> expr' val select : selop * expr * expr * expr -> expr' val compare : relop * expr * expr -> expr' val convert : cvt * expr -> expr' +val unreachable : expr' val host : hostop * expr list -> expr' val func_body : expr list -> expr' diff --git a/ml-proto/test/float_literals.wast b/ml-proto/test/float_literals.wast index 27ed205ee7..ca71a77eb0 100644 --- a/ml-proto/test/float_literals.wast +++ b/ml-proto/test/float_literals.wast @@ -2,12 +2,12 @@ (func $f32.nan (result i32) (i32.reinterpret/f32 (f32.const nan))) (func $f32.positive_nan (result i32) (i32.reinterpret/f32 (f32.const +nan))) (func $f32.negative_nan (result i32) (i32.reinterpret/f32 (f32.const -nan))) - (func $f32.plain_nan (result i32) (i32.reinterpret/f32 (f32.const nan(0x400000)))) - (func $f32.informally_known_as_plain_snan (result i32) (i32.reinterpret/f32 (f32.const nan(0x200000)))) - (func $f32.allones_nan (result i32) (i32.reinterpret/f32 (f32.const -nan(0x7fffff)))) - (func $f32.misc_nan (result i32) (i32.reinterpret/f32 (f32.const nan(0x012345)))) - (func $f32.misc_positive_nan (result i32) (i32.reinterpret/f32 (f32.const +nan(0x304050)))) - (func $f32.misc_negative_nan (result i32) (i32.reinterpret/f32 (f32.const -nan(0x2abcde)))) + (func $f32.plain_nan (result i32) (i32.reinterpret/f32 (f32.const nan:0x400000))) + (func $f32.informally_known_as_plain_snan (result i32) (i32.reinterpret/f32 (f32.const nan:0x200000))) + (func $f32.allones_nan (result i32) (i32.reinterpret/f32 (f32.const -nan:0x7fffff))) + (func $f32.misc_nan (result i32) (i32.reinterpret/f32 (f32.const nan:0x012345))) + (func $f32.misc_positive_nan (result i32) (i32.reinterpret/f32 (f32.const +nan:0x304050))) + (func $f32.misc_negative_nan (result i32) (i32.reinterpret/f32 (f32.const -nan:0x2abcde))) (func $f32.infinity (result i32) (i32.reinterpret/f32 (f32.const infinity))) (func $f32.positive_infinity (result i32) (i32.reinterpret/f32 (f32.const +infinity))) (func $f32.negative_infinity (result i32) (i32.reinterpret/f32 (f32.const -infinity))) @@ -24,12 +24,12 @@ (func $f64.nan (result i64) (i64.reinterpret/f64 (f64.const nan))) (func $f64.positive_nan (result i64) (i64.reinterpret/f64 (f64.const +nan))) (func $f64.negative_nan (result i64) (i64.reinterpret/f64 (f64.const -nan))) - (func $f64.plain_nan (result i64) (i64.reinterpret/f64 (f64.const nan(0x8000000000000)))) - (func $f64.informally_known_as_plain_snan (result i64) (i64.reinterpret/f64 (f64.const nan(0x4000000000000)))) - (func $f64.allones_nan (result i64) (i64.reinterpret/f64 (f64.const -nan(0xfffffffffffff)))) - (func $f64.misc_nan (result i64) (i64.reinterpret/f64 (f64.const nan(0x0123456789abc)))) - (func $f64.misc_positive_nan (result i64) (i64.reinterpret/f64 (f64.const +nan(0x3040506070809)))) - (func $f64.misc_negative_nan (result i64) (i64.reinterpret/f64 (f64.const -nan(0x2abcdef012345)))) + (func $f64.plain_nan (result i64) (i64.reinterpret/f64 (f64.const nan:0x8000000000000))) + (func $f64.informally_known_as_plain_snan (result i64) (i64.reinterpret/f64 (f64.const nan:0x4000000000000))) + (func $f64.allones_nan (result i64) (i64.reinterpret/f64 (f64.const -nan:0xfffffffffffff))) + (func $f64.misc_nan (result i64) (i64.reinterpret/f64 (f64.const nan:0x0123456789abc))) + (func $f64.misc_positive_nan (result i64) (i64.reinterpret/f64 (f64.const +nan:0x3040506070809))) + (func $f64.misc_negative_nan (result i64) (i64.reinterpret/f64 (f64.const -nan:0x2abcdef012345))) (func $f64.infinity (result i64) (i64.reinterpret/f64 (f64.const infinity))) (func $f64.positive_infinity (result i64) (i64.reinterpret/f64 (f64.const +infinity))) (func $f64.negative_infinity (result i64) (i64.reinterpret/f64 (f64.const -infinity))) diff --git a/ml-proto/test/float_memory.wast b/ml-proto/test/float_memory.wast index 03490f7a16..b9418a5159 100644 --- a/ml-proto/test/float_memory.wast +++ b/ml-proto/test/float_memory.wast @@ -23,11 +23,11 @@ ) (assert_return (invoke "store_i32" (i32.const 0x7f800001)) (i32.const 0x7f800001)) -(assert_return (invoke "load_f32") (f32.const nan(0x000001))) +(assert_return (invoke "load_f32") (f32.const nan:0x000001)) (assert_return (invoke "store_i32" (i32.const 0x80000000)) (i32.const 0x80000000)) (assert_return (invoke "load_f32") (f32.const -0.0)) -(assert_return (invoke "store_f32" (f32.const nan(0x000001))) (f32.const nan(0x000001))) +(assert_return (invoke "store_f32" (f32.const nan:0x000001)) (f32.const nan:0x000001)) (assert_return (invoke "load_i32") (i32.const 0x7f800001)) (assert_return (invoke "store_f32" (f32.const -0.0)) (f32.const -0.0)) (assert_return (invoke "load_i32") (i32.const 0x80000000)) @@ -54,11 +54,11 @@ ) (assert_return (invoke "store_i64" (i64.const 0x7ff0000000000001)) (i64.const 0x7ff0000000000001)) -(assert_return (invoke "load_f64") (f64.const nan(0x0000000000001))) +(assert_return (invoke "load_f64") (f64.const nan:0x0000000000001)) (assert_return (invoke "store_i64" (i64.const 0x8000000000000000)) (i64.const 0x8000000000000000)) (assert_return (invoke "load_f64") (f64.const -0.0)) -(assert_return (invoke "store_f64" (f64.const nan(0x0000000000001))) (f64.const nan(0x0000000000001))) +(assert_return (invoke "store_f64" (f64.const nan:0x0000000000001)) (f64.const nan:0x0000000000001)) (assert_return (invoke "load_i64") (i64.const 0x7ff0000000000001)) (assert_return (invoke "store_f64" (f64.const -0.0)) (f64.const -0.0)) (assert_return (invoke "load_i64") (i64.const 0x8000000000000000)) diff --git a/ml-proto/test/float_misc.wast b/ml-proto/test/float_misc.wast index 12a8f2da20..c447d621df 100644 --- a/ml-proto/test/float_misc.wast +++ b/ml-proto/test/float_misc.wast @@ -64,7 +64,7 @@ (assert_return (invoke "f32.add" (f32.const 0x1.000002p+23) (f32.const 0x1p-1)) (f32.const 0x1.000004p+23)) ;; Test that what some systems call signalling NaN behaves as a quiet NaN. -(assert_return_nan (invoke "f32.add" (f32.const nan(0x200000)) (f32.const 1.0))) +(assert_return_nan (invoke "f32.add" (f32.const nan:0x200000) (f32.const 1.0))) (assert_return (invoke "f64.add" (f64.const 1.1234567890) (f64.const 1.2345e-10)) (f64.const 0x1.1f9add37c11f7p+0)) @@ -136,7 +136,7 @@ (assert_return (invoke "f64.add" (f64.const -0x0.3f3d1a052fa2bp-1022) (f64.const -0x1.4b78292c7d2adp-1021)) (f64.const -0x1.6b16b62f14fc2p-1021)) ;; Test that what some systems call signalling NaN behaves as a quiet NaN. -(assert_return_nan (invoke "f64.add" (f64.const nan(0x4000000000000)) (f64.const 1.0))) +(assert_return_nan (invoke "f64.add" (f64.const nan:0x4000000000000) (f64.const 1.0))) ;; Test for a historic spreadsheet bug. ;; https://blogs.office.com/2007/09/25/calculation-issue-update/ @@ -260,41 +260,41 @@ (assert_return (invoke "f32.abs" (f32.const nan)) (f32.const nan)) (assert_return (invoke "f32.abs" (f32.const -nan)) (f32.const nan)) -(assert_return (invoke "f32.abs" (f32.const nan(0x0f1e2))) (f32.const nan(0x0f1e2))) -(assert_return (invoke "f32.abs" (f32.const -nan(0x0f1e2))) (f32.const nan(0x0f1e2))) +(assert_return (invoke "f32.abs" (f32.const nan:0x0f1e2)) (f32.const nan:0x0f1e2)) +(assert_return (invoke "f32.abs" (f32.const -nan:0x0f1e2)) (f32.const nan:0x0f1e2)) (assert_return (invoke "f64.abs" (f64.const nan)) (f64.const nan)) (assert_return (invoke "f64.abs" (f64.const -nan)) (f64.const nan)) -(assert_return (invoke "f64.abs" (f64.const nan(0x0f1e27a6b))) (f64.const nan(0x0f1e27a6b))) -(assert_return (invoke "f64.abs" (f64.const -nan(0x0f1e27a6b))) (f64.const nan(0x0f1e27a6b))) +(assert_return (invoke "f64.abs" (f64.const nan:0x0f1e27a6b)) (f64.const nan:0x0f1e27a6b)) +(assert_return (invoke "f64.abs" (f64.const -nan:0x0f1e27a6b)) (f64.const nan:0x0f1e27a6b)) (assert_return (invoke "f32.neg" (f32.const nan)) (f32.const -nan)) (assert_return (invoke "f32.neg" (f32.const -nan)) (f32.const nan)) -(assert_return (invoke "f32.neg" (f32.const nan(0x0f1e2))) (f32.const -nan(0x0f1e2))) -(assert_return (invoke "f32.neg" (f32.const -nan(0x0f1e2))) (f32.const nan(0x0f1e2))) +(assert_return (invoke "f32.neg" (f32.const nan:0x0f1e2)) (f32.const -nan:0x0f1e2)) +(assert_return (invoke "f32.neg" (f32.const -nan:0x0f1e2)) (f32.const nan:0x0f1e2)) (assert_return (invoke "f64.neg" (f64.const nan)) (f64.const -nan)) (assert_return (invoke "f64.neg" (f64.const -nan)) (f64.const nan)) -(assert_return (invoke "f64.neg" (f64.const nan(0x0f1e27a6b))) (f64.const -nan(0x0f1e27a6b))) -(assert_return (invoke "f64.neg" (f64.const -nan(0x0f1e27a6b))) (f64.const nan(0x0f1e27a6b))) +(assert_return (invoke "f64.neg" (f64.const nan:0x0f1e27a6b)) (f64.const -nan:0x0f1e27a6b)) +(assert_return (invoke "f64.neg" (f64.const -nan:0x0f1e27a6b)) (f64.const nan:0x0f1e27a6b)) (assert_return (invoke "f32.copysign" (f32.const nan) (f32.const nan)) (f32.const nan)) (assert_return (invoke "f32.copysign" (f32.const nan) (f32.const -nan)) (f32.const -nan)) (assert_return (invoke "f32.copysign" (f32.const -nan) (f32.const nan)) (f32.const nan)) (assert_return (invoke "f32.copysign" (f32.const -nan) (f32.const -nan)) (f32.const -nan)) -(assert_return (invoke "f32.copysign" (f32.const nan(0x0f1e2)) (f32.const nan)) (f32.const nan(0x0f1e2))) -(assert_return (invoke "f32.copysign" (f32.const nan(0x0f1e2)) (f32.const -nan)) (f32.const -nan(0x0f1e2))) -(assert_return (invoke "f32.copysign" (f32.const -nan(0x0f1e2)) (f32.const nan)) (f32.const nan(0x0f1e2))) -(assert_return (invoke "f32.copysign" (f32.const -nan(0x0f1e2)) (f32.const -nan)) (f32.const -nan(0x0f1e2))) +(assert_return (invoke "f32.copysign" (f32.const nan:0x0f1e2) (f32.const nan)) (f32.const nan:0x0f1e2)) +(assert_return (invoke "f32.copysign" (f32.const nan:0x0f1e2) (f32.const -nan)) (f32.const -nan:0x0f1e2)) +(assert_return (invoke "f32.copysign" (f32.const -nan:0x0f1e2) (f32.const nan)) (f32.const nan:0x0f1e2)) +(assert_return (invoke "f32.copysign" (f32.const -nan:0x0f1e2) (f32.const -nan)) (f32.const -nan:0x0f1e2)) (assert_return (invoke "f64.copysign" (f64.const nan) (f64.const nan)) (f64.const nan)) (assert_return (invoke "f64.copysign" (f64.const nan) (f64.const -nan)) (f64.const -nan)) (assert_return (invoke "f64.copysign" (f64.const -nan) (f64.const nan)) (f64.const nan)) (assert_return (invoke "f64.copysign" (f64.const -nan) (f64.const -nan)) (f64.const -nan)) -(assert_return (invoke "f64.copysign" (f64.const nan(0x0f1e27a6b)) (f64.const nan)) (f64.const nan(0x0f1e27a6b))) -(assert_return (invoke "f64.copysign" (f64.const nan(0x0f1e27a6b)) (f64.const -nan)) (f64.const -nan(0x0f1e27a6b))) -(assert_return (invoke "f64.copysign" (f64.const -nan(0x0f1e27a6b)) (f64.const nan)) (f64.const nan(0x0f1e27a6b))) -(assert_return (invoke "f64.copysign" (f64.const -nan(0x0f1e27a6b)) (f64.const -nan)) (f64.const -nan(0x0f1e27a6b))) +(assert_return (invoke "f64.copysign" (f64.const nan:0x0f1e27a6b) (f64.const nan)) (f64.const nan:0x0f1e27a6b)) +(assert_return (invoke "f64.copysign" (f64.const nan:0x0f1e27a6b) (f64.const -nan)) (f64.const -nan:0x0f1e27a6b)) +(assert_return (invoke "f64.copysign" (f64.const -nan:0x0f1e27a6b) (f64.const nan)) (f64.const nan:0x0f1e27a6b)) +(assert_return (invoke "f64.copysign" (f64.const -nan:0x0f1e27a6b) (f64.const -nan)) (f64.const -nan:0x0f1e27a6b)) ;; Test that ceil isn't implemented as adding 0.5 and rounding to nearest. (assert_return (invoke "f32.ceil" (f32.const 0x1.fffffep-1)) (f32.const 1.0)) diff --git a/ml-proto/test/select.wast b/ml-proto/test/select.wast index d242cbd870..d5b0994864 100644 --- a/ml-proto/test/select.wast +++ b/ml-proto/test/select.wast @@ -13,9 +13,9 @@ ;; Check that both sides of the select are evaluated (func $select_trap_l (param $cond i32) (result i32) - (i32.select (get_local $cond) (i32.div_s (i32.const 1)(i32.const 0)) (i32.const 0))) + (i32.select (get_local $cond) (unreachable) (i32.const 0))) (func $select_trap_r (param $cond i32) (result i32) - (i32.select (get_local $cond) (i32.const 0) (i32.div_s (i32.const 1)(i32.const 0)))) + (i32.select (get_local $cond) (i32.const 0) (unreachable))) (export "select_i32" $select_i32) (export "select_i64" $select_i64) @@ -41,7 +41,7 @@ (assert_return_nan (invoke "select_f64" (i32.const 1) (f64.const nan) (f64.const 1))) (assert_return_nan (invoke "select_f64" (i32.const 0) (f64.const 2) (f64.const nan))) -(assert_trap (invoke "select_trap_l" (i32.const 1)) "integer divide by zero") -(assert_trap (invoke "select_trap_l" (i32.const 0)) "integer divide by zero") -(assert_trap (invoke "select_trap_r" (i32.const 1)) "integer divide by zero") -(assert_trap (invoke "select_trap_r" (i32.const 0)) "integer divide by zero") \ No newline at end of file +(assert_trap (invoke "select_trap_l" (i32.const 1)) "unreachable executed") +(assert_trap (invoke "select_trap_l" (i32.const 0)) "unreachable executed") +(assert_trap (invoke "select_trap_r" (i32.const 1)) "unreachable executed") +(assert_trap (invoke "select_trap_r" (i32.const 0)) "unreachable executed") diff --git a/ml-proto/test/unreachable.wast b/ml-proto/test/unreachable.wast new file mode 100644 index 0000000000..89dcfb160f --- /dev/null +++ b/ml-proto/test/unreachable.wast @@ -0,0 +1,35 @@ +(module + (func $return_i32 (result i32) + (unreachable)) + (func $return_f64 (result f64) + (unreachable)) + + (func $if (param i32) (result f32) + (if_else (get_local 0) (unreachable) (f32.const 0))) + + (func $block + (block (i32.const 1) (unreachable) (i32.const 2))) + + (func $return_i64 (result i64) + (return (i64.const 1)) + (unreachable)) + + (func $call (result f64) + (call $return_i32) + (unreachable)) + + (export "return_i32" $return_i32) + (export "return_f64" $return_f64) + (export "if" $if) + (export "block" $block) + (export "return_i64" $return_i64) + (export "call" $call) +) + +(assert_trap (invoke "return_i32") "unreachable executed") +(assert_trap (invoke "return_f64") "unreachable executed") +(assert_trap (invoke "if" (i32.const 1)) "unreachable executed") +(assert_return (invoke "if" (i32.const 0)) (f32.const 0)) +(assert_trap (invoke "block") "unreachable executed") +(assert_return (invoke "return_i64") (i64.const 1)) +(assert_trap (invoke "call") "unreachable executed")