Type-check dead code and introduce assert_soft_invalid

ml-proto/README.md

@@ -96,6 +96,7 @@ wasm -d script.wast -o script.js
 The first creates a new test scripts where all embedded modules are converted to binary, the second one where all are converted to textual.
 
 The last invocation produces an equivalent, self-contained JavaScript test file.
+By default, the generated script will require `assert_soft_invalid` (see below) to detect validation failures. Use the `-us` flag ("unchecked soft") to deactivate these assertions to run on implementations that do not validate dead code.
 
 #### Command Line Expressions
 
@@ -274,6 +275,7 @@ assertion:
   ( assert_trap <action> <failure> )         ;; assert action traps with given failure string
   ( assert_malformed <module> <failure> )    ;; assert module cannot be decoded with given failure string
   ( assert_invalid <module> <failure> )      ;; assert module is invalid with given failure string
+  ( assert_soft_invalid <module> <failure> ) ;; assert module is for cases that are not required to be checked
   ( assert_unlinkable <module> <failure> )   ;; assert module fails to link
   ( assert_trap <module> <failure> )         ;; assert module traps on instantiation
 
@@ -294,6 +296,8 @@ The `input` and `output` meta commands determine the requested file format from
 The interpreter supports a "dry" mode (flag `-d`), in which modules are only validated. In this mode, all actions and assertions are ignored.
 It also supports an "unchecked" mode (flag `-u`), in which module definitions are not validated before use.
 
+Finally, "unchecked soft" mode (flag `-us`), will not require `assert_soft_valid` assertions to succeed. When outputing JavaScript scripts, this flag also controls how the created script implements this assertions.
+
 ## Abstract Syntax
 
 The abstract WebAssembly syntax, as described above and in the [design doc](https://github.com/WebAssembly/design/blob/master/AstSemantics.md), is defined in [ast.ml](spec/ast.ml).

ml-proto/host/arrange.ml

@@ -411,6 +411,8 @@ let assertion mode ass =
     Node ("assert_malformed", [definition `Original None def; Atom (string re)])
   | AssertInvalid (def, re) ->
     Node ("assert_invalid", [definition mode None def; Atom (string re)])
+  | AssertSoftInvalid (def, re) ->
+    Node ("assert_soft_invalid", [definition mode None def; Atom (string re)])
   | AssertUnlinkable (def, re) ->
     Node ("assert_unlinkable", [definition mode None def; Atom (string re)])
   | AssertUninstantiable (def, re) ->

ml-proto/host/flags.ml

@@ -1,6 +1,7 @@
 let interactive = ref false
 let trace = ref false
 let unchecked = ref false
+let unchecked_soft = ref false
 let print_sig = ref false
 let dry = ref false
 let width = ref 80

ml-proto/host/js.ml

@@ -9,6 +9,8 @@ open Source
 let prefix =
   "'use strict';\n" ^
   "\n" ^
+  "let soft_validate = " ^ string_of_bool (not !Flags.unchecked_soft) ^ ";\n" ^
+  "\n" ^
   "let spectest = {\n" ^
   "  print: print || ((...xs) => console.log(...xs)),\n" ^
   "  global: 666,\n" ^
@@ -51,6 +53,15 @@ let prefix =
   "  throw new Error(\"Wasm validation failure expected\");\n" ^
   "}\n" ^
   "\n" ^
+  "function assert_soft_invalid(bytes) {\n" ^
+  "  try { module(bytes) } catch (e) {\n" ^
+  "    if (e instanceof WebAssembly.CompileError) return;\n" ^
+  "    throw new Error(\"Wasm validation failure expected\");\n" ^
+  "  }\n" ^
+  "  if (soft_validate)\n" ^
+  "    throw new Error(\"Wasm validation failure expected\");\n" ^
+  "}\n" ^
+  "\n" ^
   "function assert_unlinkable(bytes) {\n" ^
   "  let mod = module(bytes);\n" ^
   "  try { new WebAssembly.Instance(mod, registry) } catch (e) {\n" ^
@@ -273,6 +284,8 @@ let of_assertion mods ass =
     "assert_malformed(" ^ of_definition def ^ ");"
   | AssertInvalid (def, _) ->
     "assert_invalid(" ^ of_definition def ^ ");"
+  | AssertSoftInvalid (def, _) ->
+    "assert_soft_invalid(" ^ of_definition def ^ ");"
   | AssertUnlinkable (def, _) ->
     "assert_unlinkable(" ^ of_definition def ^ ");"
   | AssertUninstantiable (def, _) ->

ml-proto/host/lexer.mll

@@ -306,6 +306,7 @@ rule token = parse
   | "get" { GET }
   | "assert_malformed" { ASSERT_MALFORMED }
   | "assert_invalid" { ASSERT_INVALID }
+  | "assert_soft_invalid" { ASSERT_SOFT_INVALID }
   | "assert_unlinkable" { ASSERT_UNLINKABLE }
   | "assert_return" { ASSERT_RETURN }
   | "assert_return_nan" { ASSERT_RETURN_NAN }

ml-proto/host/main.ml

@@ -28,6 +28,7 @@ let argspec = Arg.align
     " configure output width (default is 80)";
   "-s", Arg.Set Flags.print_sig, " show module signatures";
   "-u", Arg.Set Flags.unchecked, " unchecked, do not perform validation";
+  "-us", Arg.Set Flags.unchecked_soft, " do not perform soft validation checks";
   "-d", Arg.Set Flags.dry, " dry, do not run program";
   "-t", Arg.Set Flags.trace, " trace execution";
   "-v", Arg.Unit banner, " show version"

ml-proto/host/parser.mly

@@ -167,7 +167,7 @@ let inline_type c t at =
 %token FUNC START TYPE PARAM RESULT LOCAL GLOBAL
 %token MODULE TABLE ELEM MEMORY DATA OFFSET IMPORT EXPORT TABLE
 %token SCRIPT REGISTER INVOKE GET
-%token ASSERT_MALFORMED ASSERT_INVALID ASSERT_UNLINKABLE
+%token ASSERT_MALFORMED ASSERT_INVALID ASSERT_SOFT_INVALID ASSERT_UNLINKABLE
 %token ASSERT_RETURN ASSERT_RETURN_NAN ASSERT_TRAP
 %token INPUT OUTPUT
 %token EOF
@@ -691,6 +691,8 @@ assertion :
     { AssertMalformed (snd $3, $4) @@ at () }
   | LPAR ASSERT_INVALID module_ TEXT RPAR
     { AssertInvalid (snd $3, $4) @@ at () }
+  | LPAR ASSERT_SOFT_INVALID module_ TEXT RPAR
+    { AssertSoftInvalid (snd $3, $4) @@ at () }
   | LPAR ASSERT_UNLINKABLE module_ TEXT RPAR
     { AssertUnlinkable (snd $3, $4) @@ at () }
   | LPAR ASSERT_TRAP module_ TEXT RPAR

ml-proto/host/run.ml

@@ -271,8 +271,14 @@ let run_assertion ass =
       Assert.error ass.at "expected decoding error"
     )
 
-  | AssertInvalid (def, re) ->
-    trace "Asserting invalid...";
+  | AssertInvalid (def, re)
+  | AssertSoftInvalid (def, re) ->
+    let active =
+      match ass.it with
+      | AssertSoftInvalid _ -> not !Flags.unchecked_soft
+      | _ -> true
+    in
+    trace ("Asserting " ^ (if active then "" else "soft ") ^ "invalid...");
     (match
       let m = run_definition def in
       Check.check_module m
@@ -284,7 +290,7 @@ let run_assertion ass =
         Assert.error ass.at "wrong validation error"
       end
     | _ ->
-      Assert.error ass.at "expected validation error"
+      if active then Assert.error ass.at "expected validation error"
     )
 
   | AssertUnlinkable (def, re) ->

ml-proto/host/script.ml

@@ -14,6 +14,7 @@ type assertion = assertion' Source.phrase
 and assertion' =
   | AssertMalformed of definition * string
   | AssertInvalid of definition * string
+  | AssertSoftInvalid of definition * string
   | AssertUnlinkable of definition * string
   | AssertUninstantiable of definition * string
   | AssertReturn of action * Ast.literal list