[test] More tests for stack typing re WebAssembly#516

Author: rossberg

interpreter/valid/valid.ml

@@ -233,6 +233,8 @@ let check_stack (c : context) ts1 ts2 at =
      " but stack has " ^ string_of_result_type ts1)
 
 let pop c (ell1, ts1) (ell2, ts2) at =
+Printf.eprintf "[pop] %s\n%!"
+(String.concat " " (List.map string_of_val_type ts1));
   let n1 = List.length ts1 in
   let n2 = List.length ts2 in
   let n = min n1 n2 in
@@ -241,6 +243,8 @@ let pop c (ell1, ts1) (ell2, ts2) at =
   (ell2, if ell1 = Ellipses then [] else Lib.List.take (n2 - n) ts2)
 
 let push c (ell1, ts1) (ell2, ts2) =
+Printf.eprintf "[push] %s\n%!"
+(String.concat " " (List.map string_of_val_type ts1));
   assert (ell1 = NoEllipses || ts2 = []);
   (if ell1 = Ellipses || ell2 = Ellipses then Ellipses else NoEllipses),
   ts2 @ ts1
@@ -891,12 +895,14 @@ and check_seq (c : context) (s : infer_result_type) (es : instr list)
     s, []
 
   | e::es' ->
+Printf.eprintf "---- %s%!" (Sexpr.to_string 80 (Arrange.instr e));
     let {ins; outs}, xs = check_instr c e s in
     check_seq (init_locals c xs) (push c outs (pop c ins s e.at)) es'
 
 and check_block (c : context) (es : instr list) (it : instr_type) at =
   let InstrT (ts1, ts2, _xs) = it in
   let s, xs' = check_seq c (stack ts1) es in
+Printf.eprintf "---- end\n%!";
   let s' = pop c (stack ts2) s at in
   require (snd s' = []) at
     ("type mismatch: block requires " ^ string_of_result_type ts2 ^

test/core/br_if.wast

@@ -663,3 +663,17 @@
   "unknown label"
 )
 
+;; https://github.com/WebAssembly/gc/issues/516
+(assert_invalid
+  (module
+    (type $t (func))
+    (func $f (param (ref null $t)) (result funcref) (local.get 0))
+    (func (result funcref)
+      (ref.null $t)
+      (i32.const 0)
+      (br_if 0)  ;; only leaves funcref on the stack
+      (call $f)
+    )
+  )
+  "type mismatch"
+)

test/core/br_on_non_null.wast

@@ -71,3 +71,20 @@
 
 (assert_return (invoke "args-null" (i32.const 3)) (i32.const 3))
 (assert_return (invoke "args-f" (i32.const 3)) (i32.const 9))
+
+
+;; https://github.com/WebAssembly/gc/issues/516
+(assert_invalid
+  (module
+    (type $t (func))
+    (func $f (param (ref null $t)) (result funcref) (local.get 0))
+    (func (param funcref) (result funcref funcref)
+      (ref.null $t)
+      (local.get 0)
+      (br_on_non_null 0)  ;; only leaves a funcref on the stack
+      (call $f)
+      (local.get 0)
+    )
+  )
+  "type mismatch"
+)

test/core/gc/br_on_cast.wast

@@ -265,3 +265,21 @@
   )
   "type mismatch"
 )
+
+
+;; https://github.com/WebAssembly/gc/issues/516
+(assert_invalid
+  (module
+    (type $t (func))
+    (func $f (param (ref null $t)) (result funcref) (local.get 0))
+    (func (param funcref) (result funcref funcref)
+      (ref.null $t)
+      (local.get 0)
+      (br_on_cast 0 funcref (ref $t))  ;; only leaves two funcref's on the stack
+      (drop)
+      (call $f)
+      (local.get 0)
+    )
+  )
+  "type mismatch"
+)

test/core/gc/br_on_cast_fail.wast

@@ -280,3 +280,21 @@
   )
   "type mismatch"
 )
+
+
+;; https://github.com/WebAssembly/gc/issues/516
+(assert_invalid
+  (module
+    (type $t (func))
+    (func $f (param (ref null $t)) (result funcref) (local.get 0))
+    (func (param funcref) (result funcref funcref)
+      (ref.null $t)
+      (local.get 0)
+      (br_on_cast_fail 0 funcref (ref $t))  ;; only leaves two funcref's on the stack
+      (drop)
+      (call $f)
+      (local.get 0)
+    )
+  )
+  "type mismatch"
+)