;; RUN: wast --assert default --snapshot tests/snapshots % -f stack-switching --ignore-error-messages
;; This file tests validation only, focusing on GC types and subtyping.
;;;;
;;;;; WasmFX types
;;;;
(module
(type $f (func))
(type $ft1 (sub (func (param (ref $f)) (result (ref func)))))
(type $ct1 (sub (cont $ft1)))
(type $ft2 (func (param (ref any)) (result (ref func))))
(type $ct2 (cont $ft2))
(type $ft3 (sub $ft1 (func (param (ref func)) (result (ref $f)))))
(type $ct3 (cont $ft3))
;; Okay: Continuation types are covariant, have declared $ft3 <: $ft1
(type $ct_sub (sub $ct1 (cont $ft3)))
(func $test
(param $p1 (ref $ct1))
(param $p2 (ref $ct_sub))
;; Okay: (ref $ct_sub) <: (ref $ct1)
(local.set $p1 (local.get $p2))
)
)
(assert_invalid
(module
(type $f (func))
(type $ft1 (sub (func (param (ref $f)) (result (ref func)))))
(type $ct1 (sub (cont $ft1)))
(type $ft2 (func (param (ref func)) (result (ref $f))))
;; Error: $ft2 and ft1 have compatible types, but have not declared $ft2 <: ft1
(type $error (sub $ct1 (cont $ft2)))
)
"sub type 4 does not match super type 2"
)
(assert_invalid
(module
(type $f (func))
(type $ft1 (sub (func (param (ref $f)) (result (ref func)))))
(type $ct1 (sub (cont $ft1)))
(type $ft2 (func (param (ref func)) (result (ref $f))))
(type $ct2 (cont $ft2))
(func $test
(param $p1 (ref $ct1))
(param $p2 (ref $ct2))
;; Error $ct2 and $ct1 have generally compatible types,
;; but have not declared $ft2 <: ft1 or $ct2 <: $ct1
;; Thus, $ct2 </: $ct1.
(local.set $p1 (local.get $p2))
)
)
"type mismatch"
)
(assert_invalid
(module
(type $f (func))
(type $ft1 (sub (func (param (ref $f)) (result (ref func)))))
(type $ct1 (sub (cont $ft1)))
(type $ft3 (sub $ft1 (func (param (ref func)) (result (ref $f)))))
(type $ct3 (cont $ft3))
(func $error
(param $p1 (ref $ct1))
;;(param $p2 (ref $ct2))
(param $p3 (ref $ct3))
;; Error $ct3 and $ct1 have generally compatible types,
;; (in particular: declared $ft3 <: ft1,
;; but have not declared $ct3 <: $ct1
;; $ct3 </: $ct1
(local.set $p1 (local.get $p3))
)
)
"type mismatch"
)
(assert_invalid
(module
(func $error
(param $p_any (ref any))
(param $p_cont (ref cont))
;; Error: cont </: any
(local.set $p_any (local.get $p_cont))
)
)
"type mismatch"
)
;;;;
;;;; cont_bind instructions
;;;;
(module $non_final
(type $ft1 (func (param i32) (result (ref func))))
(type $ct1 (sub (cont $ft1)))
(type $ft0 (func (result (ref func))))
(type $ct0 (sub (cont $ft0)))
(func $test1 (param $x (ref $ct1))
(i32.const 123)
(local.get $x)
;; Smoke test: using non-final types here
(cont.bind $ct1 $ct0)
(drop)
)
)
(module $subtyping0
(type $f (func))
(type $ft0_sup (func (result (ref func))))
(type $ct0_sup (cont $ft0_sup))
(type $ft1 (func (param i32) (result (ref $f))))
(type $ct1 (cont $ft1))
(type $ft0 (func (result (ref $f))))
(type $ct0 (cont $ft0))
(func $test2 (param $x (ref $ct1))
(i32.const 123)
(local.get $x)
;; Okay: The most natural second continuation type would be $ct0.
;; But we have (func (result (ref $f))) <: (func (result (ref $func)))
;; This holds without us needing to declare any subtyping relations at all.
(cont.bind $ct1 $ct0_sup)
(drop)
)
)
(module $recursive
(rec
(type $ft0 (func (result (ref $ct_rec))))
(type $ft1 (func (param i32) (result (ref $ct_rec))))
(type $ct_rec (cont $ft1))
)
(type $ct0 (cont $ft0))
(rec
(type $ft0' (func (result (ref $ct_rec'))))
(type $ft1' (func (param i32) (result (ref $ct_rec'))))
(type $ct_rec' (cont $ft1'))
)
(type $ct1 (cont $ft1'))
;; Okay: Some simple test where the types involved in cont.bind
;; are part of a recursion group
;; (more concretely: two equivalent recursion groups)
(func $test (param $x (ref $ct1))
(i32.const 123)
(local.get $x)
(cont.bind $ct1 $ct0)
(drop)
)
)
(module $recursive_subtyping
;; We define types such that $ft0 <: $ft0_sup and $ct_rec <: $ct_rec_sup
(rec
(type $ft0_sup (sub (func (result (ref $ct_rec_sup)))))
(type $ft0 (sub $ft0_sup (func (result (ref $ct_rec)))))
(type $ft1 (sub (func (param i32) (result (ref $ct_rec)))))
(type $ct_rec_sup (sub (cont $ft0_sup)))
(type $ct_rec (sub $ct_rec_sup (cont $ft0)))
)
(type $ct0_sup (cont $ft0_sup))
(type $ct0 (cont $ft0))
(type $ct1 (cont $ft1))
(func $test (param $x (ref $ct1))
(i32.const 123)
(local.get $x)
(cont.bind $ct1 $ct0)
(drop)
(i32.const 123)
(local.get $x)
;; Okay: We have (func (result (ref $ct_rec))) <: (func (result (ref
;; $ct_rec_sup)))
(cont.bind $ct1 $ct0_sup)
(drop)
)
)
;;;;
;;;; resume instructions
;;;;
(module $subtyping_resume0
(type $ft0 (func))
(type $ct0 (cont $ft0))
(type $ft_sup (func (param (ref $ft0))))
(type $ct_sup (cont $ft_sup))
(type $ft_sub (func (param (ref func))))
(type $ct_sub (cont $ft_sub)) ;; unused
(tag $t (result (ref func)))
(func $test0
(param $p (ref $ct0))
;; Here we test subtyping with respect to the continuations received by handlers.
;;
;; The most "straightforward" type of the continuation in $handler would be (ref
;; $ct_sub). Instead, we use $ct_sup. According to the spec, we neither need
;; to declare $ft_sub <: $ft_sup or $ct_sub <: $ct_sup for this to work. We
;; have (func (param (ref func))) <: (func (param (ref $ft0))), which is
;; sufficient
(block $handler (result (ref $ct_sup))
(local.get $p)
(resume $ct0 (on $t $handler))
(return)
)
(unreachable)
)
)
(module $subtyping_resume1
(type $ft0 (func))
(type $ct0 (cont $ft0))
(tag $t (param (ref $ft0)))
(func $test0
(param $p (ref $ct0))
;; Here we test subtyping with respect to the payloads received by handlers.
;; Instead of just (ref $ft0), then handler takes func.
(block $handler (result (ref func) (ref $ct0))
(local.get $p)
(resume $ct0 (on $t $handler))
(return)
)
(unreachable)
)
)
(assert_invalid
(module
(type $ft0 (func))
(type $ct0 (cont $ft0))
(type $ft_sup (sub (func (param (ref $ft0)))))
(type $ct_sup (sub (cont $ft_sup)))
(type $ft_sub (sub $ft_sup (func (param (ref func)))))
(type $ct_sub (cont $ft_sub))
(tag $t (param (ref $ct_sub)))
(func $test0
(param $p (ref $ct0))
;; This is similar to $subtyping1, but this time we use a continuation as payload.
;; But we did not actually declare $ct_sub <: $ct_sub.
;;
;; This is mostly just to check the following:
;; For the continuation received by every handler, we see through the
;; continuation type and do structural subtyping on the underlying
;; function type.
;; However, for continuations that are just payloads ($ct_sup here), we do
;; ordinary nominal subtyping.
(block $handler (result (ref $ct_sup) (ref $ct0))
(local.get $p)
(resume $ct0 (on $t $handler))
(return)
)
(unreachable)
)
)
"type mismatch"
)