Statically disallow casts over continuations

Author: rossberg

interpreter/valid/valid.ml

@@ -114,6 +114,7 @@ let func_type_of_tag_type (c : context) (TagT dt) at : func_type =
   | DefFuncT ft -> ft
   | _ -> error at "non-function type"
 
+
 (* Types *)
 
 let check_limits {min; max} range at msg =
@@ -413,6 +414,10 @@ let check_memop (c : context) (memop : ('t, 's) memop) ty_size get_sz at =
       "offset out of range";
   memop.ty
 
+let check_cast (c : context) rt at =
+  require (not (match_ref_type c.types rt (Null, ContHT))) at
+    "invalid cast to continuation types"
+
 
 (*
  * Conventions:
@@ -540,6 +545,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
   | BrOnCast (x, rt1, rt2) ->
     check_ref_type c rt1 e.at;
     check_ref_type c rt2 e.at;
+    check_cast c rt2 e.at;
     require
       (match_ref_type c.types rt2 rt1) e.at
       ("type mismatch on cast: type " ^ string_of_ref_type rt2 ^
@@ -556,6 +562,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
   | BrOnCastFail (x, rt1, rt2) ->
     check_ref_type c rt1 e.at;
     check_ref_type c rt2 e.at;
+    check_cast c rt2 e.at;
     let rt1' = diff_ref_type rt1 rt2 in
     require
       (match_ref_type c.types rt2 rt1) e.at
@@ -835,11 +842,13 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
   | RefTest rt ->
     let (_nul, ht) = rt in
     check_ref_type c rt e.at;
+    check_cast c rt e.at;
     [RefT (Null, top_of_heap_type c.types ht)] --> [NumT I32T], []
 
   | RefCast rt ->
     let (nul, ht) = rt in
     check_ref_type c rt e.at;
+    check_cast c rt e.at;
     [RefT (Null, top_of_heap_type c.types ht)] --> [RefT (nul, ht)], []
 
   | RefEq ->

proposals/stack-switching/Explainer.md

@@ -900,8 +900,8 @@ critical use-cases requires multi-shot continuations.
 
 ## Specification changes
 
-This proposal is based on the [function references proposal](https://github.com/WebAssembly/function-references)
-and [exception handling proposal](https://github.com/WebAssembly/exception-handling).
+This proposal is based on Wasm 3.0, specifically [function references](https://github.com/WebAssembly/function-references)
+and [exception handling](https://github.com/WebAssembly/exception-handling).
 
 ### Types
 
@@ -998,6 +998,15 @@ This abbreviation will be formalised with an auxiliary function or other means i
     - and `C.types[$ct2] ~~ cont [t2*] -> [te2*]`
     - and `t* <: te2*`
 
+In addition to these new rules, the existing rules for cast instructions `ref.test`, `ref.cast`, `br_on_cast`, and `br_on_cast_fail` are amended with an additional side condition to rule out casting of continuation types:
+
+  - iff `rt castable`
+
+where `rt` is the respective target type of the cast instruction, and the `castable` predicate is defined as follows:
+
+- `rt castable`
+  - iff not (rt <: (ref null cont))
+
 ### Execution
 
 The same control tag may be used simultaneously by `throw`, `suspend`,

test/core/stack-switching/validation.wast

@@ -796,3 +796,108 @@
   )
   "unknown tag"
 )
+
+
+;; Illegal casts
+
+(assert_invalid
+  (module
+    (func (drop (ref.test contref (unreachable))))
+  )
+  "invalid cast"
+)
+(assert_invalid
+  (module
+    (func (drop (ref.test nullcontref (unreachable))))
+  )
+  "invalid cast"
+)
+(assert_invalid
+  (module
+    (type $f (func))
+    (type $c (cont $f))
+    (func (drop (ref.test (ref $c) (unreachable))))
+  )
+  "invalid cast"
+)
+
+(assert_invalid
+  (module
+    (func (drop (ref.cast contref (unreachable))))
+  )
+  "invalid cast"
+)
+(assert_invalid
+  (module
+    (func (drop (ref.cast nullcontref (unreachable))))
+  )
+  "invalid cast"
+)
+(assert_invalid
+  (module
+    (type $f (func))
+    (type $c (cont $f))
+    (func (drop (ref.cast (ref $c) (unreachable))))
+  )
+  "invalid cast"
+)
+
+(assert_invalid
+  (module
+    (func
+      (block (result contref) (br_on_cast 0 contref contref (unreachable)))
+      (drop)
+    )
+  )
+  "invalid cast"
+)
+(assert_invalid
+  (module
+    (func
+      (block (result contref) (br_on_cast 0 nullcontref nullcontref (unreachable)))
+      (drop)
+    )
+  )
+  "invalid cast"
+)
+(assert_invalid
+  (module
+    (type $f (func))
+    (type $c (cont $f))
+    (func
+      (block (result contref) (br_on_cast 0 (ref $c) (ref $c) (unreachable)))
+      (drop)
+    )
+  )
+  "invalid cast"
+)
+
+(assert_invalid
+  (module
+    (func
+      (block (result contref) (br_on_cast_fail 0 contref contref (unreachable)))
+      (drop)
+    )
+  )
+  "invalid cast"
+)
+(assert_invalid
+  (module
+    (func
+      (block (result contref) (br_on_cast_fail 0 nullcontref nullcontref (unreachable)))
+      (drop)
+    )
+  )
+  "invalid cast"
+)
+(assert_invalid
+  (module
+    (type $f (func))
+    (type $c (cont $f))
+    (func
+      (block (result contref) (br_on_cast_fail 0 (ref $c) (ref $c) (unreachable)))
+      (drop)
+    )
+  )
+  "invalid cast"
+)