diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index 9c07c003..9173e3c6 100644 --- a/interpreter/valid/valid.ml +++ b/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 -> diff --git a/proposals/stack-switching/Explainer.md b/proposals/stack-switching/Explainer.md index ab996223..3e64fc77 100644 --- a/proposals/stack-switching/Explainer.md +++ b/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`, diff --git a/test/core/stack-switching/validation.wast b/test/core/stack-switching/validation.wast index 5a1ed682..116b3d17 100644 --- a/test/core/stack-switching/validation.wast +++ b/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" +)