From 8300978a64757b447558728ab182c823621054f3 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 23 Sep 2025 15:32:21 +0200 Subject: [PATCH 01/20] Statically disallow casts over continuations --- interpreter/valid/valid.ml | 9 ++ proposals/stack-switching/Explainer.md | 13 ++- test/core/stack-switching/validation.wast | 105 ++++++++++++++++++++++ 3 files changed, 125 insertions(+), 2 deletions(-) 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" +) From 389f6cce261ccd39b28d7aa48adcaec9159712cb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Fri, 3 Oct 2025 13:13:54 -0400 Subject: [PATCH 02/20] Reduction semantics (#109) * Reduction semantics This patch populates the "Execution" section of the Explainer document with the reduction rules for stack switching. * Some type expansions * Fix minor typo, hdl => hdl1 * Fix typo: stray ' * Address Andreas' feedback * Remove stray ^ * Incorporated comments Incorporated comments from before The biggest thing I am unsure of is lines 814 and 826. This pertains to what point the tag argument of suspend and switch is translated into a tag address. Doing it in the reduction rule for resume (as was the case in the previous version of Explainer.md) is wrong, for reasons explained in the comment I wrote at the time. I believe I was told in the actual implementation, the change happens during the validation phase, which is why I propose these lines 814 and 826; however my phrasing can perhaps be improved. * rectified the suspend address translation to its correct place Incorporating Thomas Lively's comment, I have rectified the spot where suspend and switch translate the tag index into a tag address, by creating new instructions suspend.addr and switch.addr that take addresses (rather than indices) as arguments. This allows for a rule focused on translating suspend to suspend.addr (and likewise for switch), enforcing that the correct wasm frame F is used. * Update proposals/stack-switching/Explainer.md Co-authored-by: Thomas Lively * Fix resume_throw semantics * Update proposals/stack-switching/Explainer.md Committing tlively's suggested change Co-authored-by: Thomas Lively * Update proposals/stack-switching/Explainer.md Committing tlively's suggested change Co-authored-by: Thomas Lively * Applied all suggested changes except taguse Applied all suggested changes except taguse which is the last remaining issue * Added tag uses * using taguse in hdl too * factored typing rules and added keyword 'on' where now necessary * Typo in typing rule for tag addresses * corrected $a to $e and added switch failure rules --------- Co-authored-by: mlegoupil <90708290+mlegoupil@users.noreply.github.com> Co-authored-by: Sam Lindley Co-authored-by: Thomas Lively --- proposals/stack-switching/Explainer.md | 149 ++++++++++++++++++++++--- 1 file changed, 133 insertions(+), 16 deletions(-) diff --git a/proposals/stack-switching/Explainer.md b/proposals/stack-switching/Explainer.md index 3e64fc77..8c832629 100644 --- a/proposals/stack-switching/Explainer.md +++ b/proposals/stack-switching/Explainer.md @@ -923,6 +923,15 @@ We change the wellformedness condition for tag types to be more liberal, i.e. In other words, the return type of tag types is allowed to be non-empty. +We also introduce tag uses, which can be either tag indices or tag addresses: + +- `taguse ::= tagidx | tagaddr` + - `$e : [t1*] -> [t2*]` + - iff `C.tags[$e] = tag $ft` + - and `C.types[$ft] ~~ func [t1*] -> [t2*]` + - `ea : [t1*] -> [t2*]` + - iff `S.tags[ea].type ~~ func [t1*] -> [t2*]` + ### Instructions The new instructions and their validation rules are as follows. To simplify the presentation, we write this: @@ -968,31 +977,27 @@ This abbreviation will be formalised with an auxiliary function or other means i - and `C.types[$ft] ~~ func [te*] -> []` - and `(hdl : t2*)*` -- `hdl = (on ) | (on switch)` +- `hdl = (on ) | (on switch)` - Handlers attached to `resume` and `resume_throw`, handling control tags for `suspend` and `switch`, respectively. - - `(on $e $l) : t*` - - iff `C.tags[$e] = tag $ft` - - and `C.types[$ft] ~~ func [t1*] -> [t2*]` + - `(on tu $l) : t*` + - iff `tu : [t1*] -> [t2*]` - and `C.labels[$l] = [t1'* (ref null? $ct)]` - and `t1* <: t1'*` - and `C.types[$ct] ~~ cont [t2'*] -> [t'*]` - and `[t2*] -> [t*] <: [t2'*] -> [t'*]` - - `(on $e switch) : t*` - - iff `C.tags[$e] = tag $ft` - - and `C.types[$ft] ~~ func [] -> [t*]` + - `(on tu switch) : t*` + - iff `tu : [] -> [t*]` -- `suspend ` +- `suspend ` - Use a control tag to suspend the current computation. - - `suspend $t : [t1*] -> [t2*]` - - iff `C.tags[$t] = tag $ft` - - and `C.types[$ft] ~~ func [t1*] -> [t2*]` + - `suspend tu : [t1*] -> [t2*]` + - iff `tu : func [t1*] -> [t2*]` -- `switch ` +- `switch ` - Switch to executing a given continuation directly, suspending the current execution. - The suspension and switch are performed from the perspective of a parent `(on $e switch)` handler, determined by the annotated control tag. - - `switch $ct1 $e : [t1* (ref null $ct1)] -> [t2*]` - - iff `C.tags[$e] = tag $ft` - - and `C.types[$ft] ~~ func [] -> [t*]` + - `switch $ct1 tu : [t1* (ref null $ct1)] -> [t2*]` + - iff `tu : [] -> [t*]` - and `C.types[$ct1] ~~ cont [t1* (ref null? $ct2)] -> [te1*]` - and `te1* <: t*` - and `C.types[$ct2] ~~ cont [t2*] -> [te2*]` @@ -1017,6 +1022,118 @@ events and only `(on $e switch)` handlers can handle `switch` events. The handler search continues past handlers for the wrong kind of event, even if they use the correct tag. +#### Store extensions + +* New store component `conts` for allocated continuations + - `S ::= {..., conts ?*}` + +* A continuation is a context annotated with its hole's arity + - `continst ::= (E : n)` + + +#### Administrative instructions + +* `(ref.cont a)` represents a continuation value, where `a` is a *continuation address* indexing into the store's `conts` component + - `ref.cont a : [] -> [(ref $ct)]` + - iff `S.conts[a] = epsilon \/ S.conts[a] = (E : n)` + + iff `E[val^n] : t2*` + + and `(val : t1)^n` + - and `$ct ~~ cont $ft` + - and `$ft ~~ [t1^n] -> [t2*]` + +* `(prompt{*} * end)` represents an active handler + - `(prompt{hdl*}? instr* end) : [] -> [t*]` + - iff `instr* : [] -> [t*]` in the empty context + - and `(hdl : [t*])*` + +#### Handler contexts + +``` +H^ea ::= + _ + val* H^ea instr* + label_n{instr*} H^ea end + frame_n{F} H^ea end + catch{...} H^ea end + prompt{hdl*} H^ea end (iff ea notin hdl*) +``` + + +#### Reduction + +* `S; F; (ref.null t) (cont.new $ct) --> S; F; trap` + +* `S; F; (ref.func fa) (cont.new $ct) --> S'; F; (ref.cont |S.conts|)` + - iff `S' = S with conts += (E : n)` + - and `E = _ (invoke fa)` + - and `$ct ~~ cont $ft` + - and `$ft ~~ [t1^n] -> [t2*]` + +* `S; F; (ref.null t) (cont.bind $ct $ct') --> S; F; trap` + +* `S; F; (ref.cont ca) (cont.bind $ct $ct') --> S; F; trap` + - iff `S.conts[ca] = epsilon` + +* `S; F; v^n (ref.cont ca) (cont.bind $ct $ct') --> S'; F; (ref.cont |S.conts|)` + - iff `S.conts[ca] = (E' : n')` + - and `$ct' ~~ cont $ft'` + - and `$ft' ~~ [t1'*] -> [t2'*]` + - and `n = n' - |t1'*|` + - and `S' = S with conts[ca] = epsilon with conts += (E : |t1'*|)` + - and `E = E'[v^n _]` + +* `S; F; (ref.null t) (resume $ct hdl*) --> S; F; trap` + +* `S; F; (ref.cont ca) (resume $ct hdl*) --> S; F; trap` + - iff `S.conts[ca] = epsilon` + +* `S; F; v^n (ref.cont ca) (resume $ct hdl*) --> S'; F; prompt{hdl'*} E[v^n] end` + - iff `S.conts[ca] = (E : n)` + - and `S' = S with conts[ca] = epsilon` + - and `hdl'* = hdl*[F.module.tags / 0..|F.module.tags|-1]` + +* `S; F; (ref.null t) (resume_throw $ct $e hdl*) --> S; F; trap` + +* `S; F; (ref.cont ca) (resume_throw $ct $e hdl*) --> S; F; trap` + - iff `S.conts[ca] = epsilon` + +* `S; F; v^m (ref.cont ca) (resume_throw $ct $e hdl*) --> S''; F; prompt{hdl'*} E[(ref.exn |S'.exns|) throw_ref] end` + - iff `S.conts[ca] = (E : n)` + - and `ta = S.tags[F.module.tags[$e]]` + - and `ta.type ~~ [t1^m] -> [t2*]` + - and `S' = S with exns += {ta, v^m}` + - and `S'' = S' with conts[ca] = epsilon` + - and `hdl'* = hdl*[F.module.tags / 0..|F.module.tags|-1]` + +* `S; F; (prompt{hdl*} v* end) --> S; F; v*` + +* `S; F; (suspend $e) --> S; F; (suspend ea)` + - iff `ea = F.module.tags[$e]` + +* `S; F; (prompt{hdl1* (on ea $l) hdl2*} H^ea[v^n (suspend ea)] end) --> S'; F; v^n (ref.cont |S.conts|) (br $l)` + - iff `forall $l', (on ea $l') notin hdl1*` + - and `S.tags[ea].type ~~ [t1^n] -> [t2^m]` + - and `S' = S with conts += (H^ea : m)` + +* `S; F; (switch $ct $e) --> S; F; (switch $ct ea)` + - iff `ea = F.module.tags[$e]` + +* `S; F; (ref.null t) (switch $ct ea) --> S; F; trap` + +* `S; F; (ref.cont ca) (switch $ct ea) --> S; F; trap` + - iff `S.conts[ca] = epsilon` + +* `S; F; (prompt{hdl1* (on ea switch) hdl2*} H^ea[v^n (ref.cont ca) (switch $ct ea)] end) --> S''; F; prompt{hdl1* (on ea switch) hdl2*} E[v^n (ref.cont |S.conts|)] end` + - iff `S.conts[ca] = (E : n')` + - and `n' = 1 + n` + - and `(on switch ea) notin hdl1*` + - and `$ct ~~ cont $ft` + - and `$ft ~~ [t1* (ref $ct2)] -> [t2*]` + - and `$ct2 ~~ cont $ft2` + - and `$ft2 ~~ [t1'^m] -> [t2'*]` + - and `S' = S with conts[ca] = epsilon` + - and `S'' = S' with conts += (H^ea : m)` + ### Binary format We extend the binary format of composite types, heap types, and instructions. @@ -1040,7 +1157,7 @@ The opcode for heap types is encoded as an `s33`. #### Instructions -We use the use the opcode space `0xe0-0xe5` for the seven new instructions. +We use the use the opcode space `0xe0-0xe5` for the six new instructions. | Opcode | Instruction | Immediates | | ------ | ------------------------ | ---------- | From 9579cb92f0981582d0e39e0f80baa77589ffa531 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Thu, 9 Oct 2025 10:36:27 -0700 Subject: [PATCH 03/20] Add resume_throw_ref to the explainer (#132) Give it opcode 0xe5 to be adjacent to `resume_throw` at 0xe4, and as a result bump `switch` to 0xe6. Update `switch` in the interpreter as well. Redefine the execution semantics of `resume_throw` in terms of `resume_throw_ref`. As a drive-by, fix the nullability of reference operands in the initial introduction of each other instruction. --- interpreter/binary/decode.ml | 3 +- interpreter/binary/encode.ml | 3 +- proposals/stack-switching/Explainer.md | 87 +++++++++++++++++--------- 3 files changed, 63 insertions(+), 30 deletions(-) diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml index 6ef9501d..68bddd9b 100644 --- a/interpreter/binary/decode.ml +++ b/interpreter/binary/decode.ml @@ -646,7 +646,8 @@ let rec instr s = let tag = at var s in let xls = vec on_clause s in resume_throw x tag xls - | 0xe5 -> + (* TODO: resume_throw_ref *) + | 0xe6 -> let x = at var s in let y = at var s in switch x y diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml index 8924dd57..f4942331 100644 --- a/interpreter/binary/encode.ml +++ b/interpreter/binary/encode.ml @@ -303,7 +303,8 @@ struct | Suspend x -> op 0xe2; var x | Resume (x, xls) -> op 0xe3; var x; resumetable xls | ResumeThrow (x, y, xls) -> op 0xe4; var x; var y; resumetable xls - | Switch (x, y) -> op 0xe5; var x; var y + (* TOOD: resume_throw_ref *) + | Switch (x, y) -> op 0xe6; var x; var y | Throw x -> op 0x08; var x | ThrowRef -> op 0x0a diff --git a/proposals/stack-switching/Explainer.md b/proposals/stack-switching/Explainer.md index 8c832629..d0fb016b 100644 --- a/proposals/stack-switching/Explainer.md +++ b/proposals/stack-switching/Explainer.md @@ -483,8 +483,8 @@ a task function would ordinarily return, it should instead switch to the next task. When doing so, it should pass a new flag to the target continuation to indicate that the source continuation should not be enqueued in the task list, but should instead be cancelled. Cancellation -can be implemented using another instruction, `resume_throw`, which is -described later in the document. +can be implemented using two more instructions, `resume_throw` and +`resume_throw_ref`, which are described later in the document. Full versions of `$scheduler1` and `$scheduler2` can be found [here](examples/scheduler1.wast) and [here](examples/scheduler2.wast). @@ -543,7 +543,7 @@ The following instruction creates a *suspended continuation* from a function. ```wast - cont.new $ct : [(ref $ft)] -> [(ref $ct)] + cont.new $ct : [(ref null $ft)] -> [(ref $ct)] where: - $ft = func [t1*] -> [t2*] - $ct = cont $ft @@ -561,7 +561,7 @@ continuation under a *handler*. The handler specifies what to do when control is subsequently suspended again. ```wast - resume $ct hdl* : [t1* (ref $ct)] -> [t2*] + resume $ct hdl* : [t1* (ref null $ct)] -> [t2*] where: - $ct = cont [t1*] -> [t2*] ``` @@ -581,7 +581,7 @@ The second way to invoke a continuation is to raise an exception at the control tag invocation site which causes the stack to be unwound. ```wast - resume_throw $ct $exn hdl* : [te* (ref $ct)])] -> [t2*] + resume_throw $ct $exn hdl* : [te* (ref null $ct)] -> [t2*] where: - $ct = cont [t1*] -> [t2*] - $exn : [te*] -> [] @@ -597,11 +597,24 @@ exception is being raised (the continuation is not actually being supplied a value) the parameter types for the continuation `t1*` are unconstrained. +Exceptions can also be raised at a suspension site using +`resume_throw_ref`. + +```wast + resume_throw_ref $ct hdl* : [exnref (ref null $ct)] -> [t2*] + where: + - $ct = cont [t1*] -> [t2*] +``` + +The `resume_throw_ref` instruction is identical to the `resume_throw` +instruction except that the exception it raises is given by an exnref +operand rather than by an exception tag immediate. + The third way to invoke a continuation is to perform a symmetric switch. ```wast - switch $ct1 $e : [t1* (ref $ct1)] -> [t2*] + switch $ct1 $e : [t1* (ref null $ct1)] -> [t2*] where: - $e : [] -> [t*] - $ct1 = cont [t1* (ref $ct2)] -> [t*] @@ -614,8 +627,9 @@ continuation argument (`$ct1`) and a control tag performs a direct switch to the suspended peer continuation (of type `$ct1`), passing in the required parameters (including the just suspended current continuation, in order to allow the peer to switch -back again). As with `resume` and `resume_throw`, the `switch` -instruction fully consumes its suspended continuation argument. +back again). As with `resume`, `resume_throw`, and `resume_throw_ref`, +the `switch` instruction fully consumes its suspended continuation +argument. ### Suspending continuations @@ -641,7 +655,7 @@ A suspended continuation can be partially applied to a prefix of its arguments yielding another suspended continuation. ```wast - cont.bind $ct1 $ct2 : [t1* (ref $ct1)] -> [(ref $ct2)] + cont.bind $ct1 $ct2 : [t1* (ref null $ct1)] -> [(ref $ct2)] where: - $ct1 = cont [t1* t3*] -> [t2*] - $ct2 = cont [t3*] -> [t2*] @@ -672,21 +686,23 @@ preallocating one slot for each continuation argument. #### Consuming continuations -There are four different ways in which suspended continuations are -consumed (`resume,resume_throw,switch,cont.bind`). A suspended -continuation may be resumed with a particular handler with `resume`; -aborted with `resume_throw`; directly switched to via `switch`; or -partially applied with `cont.bind`. +There are five different ways in which suspended continuations are +consumed (`resume`, `resume_throw`, `resume_throw_ref`, `switch`, +`cont.bind`). A suspended continuation may be resumed with a particular +handler with `resume`; aborted with `resume_throw` or +`resume_throw_ref`; directly switched to via `switch`; or partially +applied with `cont.bind`. In order to ensure that continuations are one-shot, `resume`, -`resume_throw`, `switch`, and `cont.bind` destructively modify the -suspended continuation such that any subsequent use of the same -suspended continuation will result in a trap. +`resume_throw`, `resume_throw_ref`, `switch`, and `cont.bind` +destructively modify the suspended continuation such that any +subsequent use of the same suspended continuation will result in a +trap. ## Further examples We now illustrate the use of tags with result values and the -instructions `cont.bind` and `resume.throw`, by adapting and extending +instructions `cont.bind` and `resume_throw`, by adapting and extending the examples of [Section 3](#introduction-to-continuation-based-stack-switching). @@ -977,6 +993,13 @@ This abbreviation will be formalised with an auxiliary function or other means i - and `C.types[$ft] ~~ func [te*] -> []` - and `(hdl : t2*)*` +- `resume_throw_ref hdl*` + - Execute a given continuation, but force it to immediately throw the given exception. + - Used to abort a continuation. + - `resume_throw_ref $ct hdl* : [exnref (ref null $ct)] -> [t2*]` + - iff `C.types[$ct] ~~ cont [t1*] -> [t2*]` + - and `(hdl : t2*)*` + - `hdl = (on ) | (on switch)` - Handlers attached to `resume` and `resume_throw`, handling control tags for `suspend` and `switch`, respectively. - `(on tu $l) : t*` @@ -1094,15 +1117,22 @@ H^ea ::= * `S; F; (ref.null t) (resume_throw $ct $e hdl*) --> S; F; trap` -* `S; F; (ref.cont ca) (resume_throw $ct $e hdl*) --> S; F; trap` +* `S; F; v^m (ref.cont ca) (resume_throw $ct $e hdl*) --> S'; F; (ref.exn |S.exns|) (ref.const ca) (resume_throw_ref $ct hdl*)` + - iff `ta = F.module.tags[$e]` + - and `S.tags[ta].type ~~ [t1^m] -> [t2*]` + - and `S' = S with exns += {S.tags[ta], v^m}` + +* `S; F; (ref.null t) (resume_throw_ref $ct hdl*) --> S; F; trap` + +* `S; F; (ref.cont ca) (resume_throw_ref $ct hdl*) --> S; F; trap` - iff `S.conts[ca] = epsilon` -* `S; F; v^m (ref.cont ca) (resume_throw $ct $e hdl*) --> S''; F; prompt{hdl'*} E[(ref.exn |S'.exns|) throw_ref] end` +* `S; F; (ref.null t) (ref.cont ca) (resume_throw_ref $ct hdl*) --> S; F; trap` + - iff `S.conts[ca] = (E : n)` + +* `S; F; (ref.exn ea) (ref.cont ca) (resume_throw_ref $ct hdl*) --> S'; F; prompt{hdl'*} E[(ref.exn ea) throw_ref] end` - iff `S.conts[ca] = (E : n)` - - and `ta = S.tags[F.module.tags[$e]]` - - and `ta.type ~~ [t1^m] -> [t2*]` - - and `S' = S with exns += {ta, v^m}` - - and `S'' = S' with conts[ca] = epsilon` + - and `S' = S with conts[ca] = epsilon` - and `hdl'* = hdl*[F.module.tags / 0..|F.module.tags|-1]` * `S; F; (prompt{hdl*} v* end) --> S; F; v*` @@ -1157,7 +1187,7 @@ The opcode for heap types is encoded as an `s33`. #### Instructions -We use the use the opcode space `0xe0-0xe5` for the six new instructions. +We use the use the opcode space `0xe0-0xe6` for the seven new instructions. | Opcode | Instruction | Immediates | | ------ | ------------------------ | ---------- | @@ -1166,10 +1196,11 @@ We use the use the opcode space `0xe0-0xe5` for the six new instructions. | 0xe2 | `suspend $t` | `$t : u32` | | 0xe3 | `resume $ct hdl*` | `$ct : u32` (for hdl see below) | | 0xe4 | `resume_throw $ct $e hdl*` | `$ct : u32`, `$e : u32` (for hdl see below) | -| 0xe5 | `switch $ct1 $e` | `$ct1 : u32`, `$e : u32` | +| 0xe5 | `resume_throw_ref $ct hdl*` | `$ct : u32` (for hdl see below) | +| 0xe6 | `switch $ct1 $t` | `$ct1 : u32`, `$t : u32` | -In the case of `resume` and `resume_throw` we use a leading byte to -indicate the shape of `hdl` as follows. +In the cases of `resume`, `resume_throw`, and `resume_throw_ref` we use a +leading byte to indicate the shape of `hdl` as follows. | Opcode | On clause shape | Immediates | | ------ | --------------- | ---------- | From 026f7238525ad98aa5c430df7ad8184bd77666f1 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Sun, 12 Oct 2025 18:01:59 -0700 Subject: [PATCH 04/20] Do not store continuation arities (#135) Real implementations will determine continuation arities by inspecting the type immediates on the instructions that manipulate those continuations, not by reading the arities off the continuations at runtime. Update the semantics given in the explainer to compute arities from type immediates as well. --- proposals/stack-switching/Explainer.md | 37 +++++++++++--------------- 1 file changed, 16 insertions(+), 21 deletions(-) diff --git a/proposals/stack-switching/Explainer.md b/proposals/stack-switching/Explainer.md index d0fb016b..4c70383d 100644 --- a/proposals/stack-switching/Explainer.md +++ b/proposals/stack-switching/Explainer.md @@ -1050,15 +1050,15 @@ of event, even if they use the correct tag. * New store component `conts` for allocated continuations - `S ::= {..., conts ?*}` -* A continuation is a context annotated with its hole's arity - - `continst ::= (E : n)` +* A continuation is a context + - `continst ::= E` #### Administrative instructions * `(ref.cont a)` represents a continuation value, where `a` is a *continuation address* indexing into the store's `conts` component - `ref.cont a : [] -> [(ref $ct)]` - - iff `S.conts[a] = epsilon \/ S.conts[a] = (E : n)` + - iff `S.conts[a] = epsilon \/ S.conts[a] = E` + iff `E[val^n] : t2*` + and `(val : t1)^n` - and `$ct ~~ cont $ft` @@ -1087,10 +1087,8 @@ H^ea ::= * `S; F; (ref.null t) (cont.new $ct) --> S; F; trap` * `S; F; (ref.func fa) (cont.new $ct) --> S'; F; (ref.cont |S.conts|)` - - iff `S' = S with conts += (E : n)` + - iff `S' = S with conts += E` - and `E = _ (invoke fa)` - - and `$ct ~~ cont $ft` - - and `$ft ~~ [t1^n] -> [t2*]` * `S; F; (ref.null t) (cont.bind $ct $ct') --> S; F; trap` @@ -1098,11 +1096,11 @@ H^ea ::= - iff `S.conts[ca] = epsilon` * `S; F; v^n (ref.cont ca) (cont.bind $ct $ct') --> S'; F; (ref.cont |S.conts|)` - - iff `S.conts[ca] = (E' : n')` - - and `$ct' ~~ cont $ft'` - - and `$ft' ~~ [t1'*] -> [t2'*]` - - and `n = n' - |t1'*|` - - and `S' = S with conts[ca] = epsilon with conts += (E : |t1'*|)` + - iff `S.conts[ca] = E'` + - and `$ct ~~ cont [t1*] -> [t2*]` + - and `$ct' ~~ cont [t1'*] -> [t2'*]` + - and `n = |t1*| - |t1'*|` + - and `S' = S with conts[ca] = epsilon with conts += E` - and `E = E'[v^n _]` * `S; F; (ref.null t) (resume $ct hdl*) --> S; F; trap` @@ -1111,8 +1109,9 @@ H^ea ::= - iff `S.conts[ca] = epsilon` * `S; F; v^n (ref.cont ca) (resume $ct hdl*) --> S'; F; prompt{hdl'*} E[v^n] end` - - iff `S.conts[ca] = (E : n)` + - iff `S.conts[ca] = E` - and `S' = S with conts[ca] = epsilon` + - and `$ct ~~ cont [t1^n] -> [t2*]` - and `hdl'* = hdl*[F.module.tags / 0..|F.module.tags|-1]` * `S; F; (ref.null t) (resume_throw $ct $e hdl*) --> S; F; trap` @@ -1128,10 +1127,10 @@ H^ea ::= - iff `S.conts[ca] = epsilon` * `S; F; (ref.null t) (ref.cont ca) (resume_throw_ref $ct hdl*) --> S; F; trap` - - iff `S.conts[ca] = (E : n)` + - iff `S.conts[ca] = E` * `S; F; (ref.exn ea) (ref.cont ca) (resume_throw_ref $ct hdl*) --> S'; F; prompt{hdl'*} E[(ref.exn ea) throw_ref] end` - - iff `S.conts[ca] = (E : n)` + - iff `S.conts[ca] = E` - and `S' = S with conts[ca] = epsilon` - and `hdl'* = hdl*[F.module.tags / 0..|F.module.tags|-1]` @@ -1154,15 +1153,11 @@ H^ea ::= - iff `S.conts[ca] = epsilon` * `S; F; (prompt{hdl1* (on ea switch) hdl2*} H^ea[v^n (ref.cont ca) (switch $ct ea)] end) --> S''; F; prompt{hdl1* (on ea switch) hdl2*} E[v^n (ref.cont |S.conts|)] end` - - iff `S.conts[ca] = (E : n')` - - and `n' = 1 + n` + - iff `S.conts[ca] = E` - and `(on switch ea) notin hdl1*` - - and `$ct ~~ cont $ft` - - and `$ft ~~ [t1* (ref $ct2)] -> [t2*]` - - and `$ct2 ~~ cont $ft2` - - and `$ft2 ~~ [t1'^m] -> [t2'*]` + - and `$ct ~~ cont [t1^n (ref $ct2)] -> [t2*]` - and `S' = S with conts[ca] = epsilon` - - and `S'' = S' with conts += (H^ea : m)` + - and `S'' = S' with conts += H^ea` ### Binary format From f369a8c37642fc1d85f285ebd103e9638a63f9c2 Mon Sep 17 00:00:00 2001 From: Thibaud Michaud Date: Mon, 13 Oct 2025 17:42:46 +0200 Subject: [PATCH 05/20] Tests: use JS-compatible module names When the core tests are converted to JS, module names are used as JS identifiers, so "-" is not a valid symbol in that context. Use "_" instead. --- test/core/stack-switching/cont.wast | 2 +- test/core/stack-switching/validation_gc.wast | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/test/core/stack-switching/cont.wast b/test/core/stack-switching/cont.wast index 3695edf3..0faa245e 100644 --- a/test/core/stack-switching/cont.wast +++ b/test/core/stack-switching/cont.wast @@ -574,7 +574,7 @@ ;; Nested example: generator in a thread -(module $concurrent-generator +(module $concurrent_generator (func $log (import "spectest" "print_i64") (param i64)) (tag $syield (import "scheduler" "yield")) diff --git a/test/core/stack-switching/validation_gc.wast b/test/core/stack-switching/validation_gc.wast index f6691e0c..f9c098d0 100644 --- a/test/core/stack-switching/validation_gc.wast +++ b/test/core/stack-switching/validation_gc.wast @@ -228,7 +228,7 @@ ;;;; -(module $subtyping-resume0 +(module $subtyping_resume0 (type $ft0 (func)) (type $ct0 (cont $ft0)) @@ -260,7 +260,7 @@ ) ) -(module $subtyping-resume1 +(module $subtyping_resume1 (type $ft0 (func)) (type $ct0 (cont $ft0)) From 92410d12712aafc65303bf541cc9d9a9179ef84d Mon Sep 17 00:00:00 2001 From: Francis McCabe Date: Thu, 16 Oct 2025 22:13:24 +0000 Subject: [PATCH 06/20] Initial implementation of resume_throw_ref Not tested. --- interpreter/binary/encode.ml | 2 +- interpreter/exec/eval.ml | 15 + interpreter/syntax/ast.ml | 1 + interpreter/syntax/free.ml | 1 + interpreter/syntax/operators.ml | 1 + interpreter/text/arrange.ml | 2 + interpreter/valid/valid.ml | 6 + test/core/stack-switching/resume_throw.wast | 286 ++++++++++++++++++++ test/core/throw_ref.wast | 3 +- 9 files changed, 315 insertions(+), 2 deletions(-) create mode 100644 test/core/stack-switching/resume_throw.wast diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml index f4942331..ca32b89b 100644 --- a/interpreter/binary/encode.ml +++ b/interpreter/binary/encode.ml @@ -303,7 +303,7 @@ struct | Suspend x -> op 0xe2; var x | Resume (x, xls) -> op 0xe3; var x; resumetable xls | ResumeThrow (x, y, xls) -> op 0xe4; var x; var y; resumetable xls - (* TOOD: resume_throw_ref *) + | ResumeThrowRef (x, xls) -> op 0xe5; var x; resumetable xls | Switch (x, y) -> op 0xe6; var x; var y | Throw x -> op 0x08; var x diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index 3fb2176b..0cf73eb5 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -407,6 +407,21 @@ let rec step (c : config) : config = cont := None; vs', [Prompt (hs, ctxt ([], [Throwing (tagt, args) @@ e.at])) @@ e.at] + | ResumeThrowRef (x, xls), Ref (NullRef _) :: vs -> + vs, [Trapping "null exception reference" @@ e.at] + + | ResumeThrowRef (x, xls), Ref _ :: Ref (NullRef _) :: vs -> + vs, [Trapping "null continuation reference" @@ e.at] + + | ResumeThrowRef (x, xls), Ref _ :: Ref (ContRef {contents = None}) :: vs -> + vs, [Trapping "continuation already consumed" @@ e.at] + + | ResumeThrowRef (x, xls), Ref (Exn.(ExnRef (Exn (tagt, args)))) :: + Ref (ContRef ({contents = Some (n, ctxt)} as cont)) :: vs -> + let hs = handle_table c xls in + cont := None; + vs, [Prompt (hs, ctxt ([], [Throwing (tagt, args) @@ e.at])) @@ e.at] + | Switch (x, y), Ref (NullRef _) :: vs -> vs, [Trapping "null continuation reference" @@ e.at] diff --git a/interpreter/syntax/ast.ml b/interpreter/syntax/ast.ml index 5ee382fd..30ea07dc 100644 --- a/interpreter/syntax/ast.ml +++ b/interpreter/syntax/ast.ml @@ -177,6 +177,7 @@ and instr' = | Suspend of idx (* suspend continuation *) | Resume of idx * (idx * hdl) list (* resume continuation *) | ResumeThrow of idx * idx * (idx * hdl) list (* abort continuation *) + | ResumeThrowRef of idx * (idx * hdl) list (* abort continuation *) | Switch of idx * idx (* direct switch continuation *) | Throw of idx (* throw exception *) | ThrowRef (* rethrow exception *) diff --git a/interpreter/syntax/free.ml b/interpreter/syntax/free.ml index 8bfb0d40..ef6a181f 100644 --- a/interpreter/syntax/free.ml +++ b/interpreter/syntax/free.ml @@ -181,6 +181,7 @@ let rec instr (e : instr) = | ContNew x -> types (idx x) | ContBind (x, y) -> types (idx x) ++ types (idx y) | ResumeThrow (x, y, xys) -> types (idx x) ++ tags (idx y) ++ list (fun (x, y) -> tags (idx x) ++ hdl y) xys + | ResumeThrowRef (x, xys) -> types (idx x) ++ list (fun (x, y) -> tags (idx x) ++ hdl y) xys | Resume (x, xys) -> types (idx x) ++ list (fun (x, y) -> tags (idx x) ++ hdl y) xys | Suspend x -> tags (idx x) | Switch (x, z) -> types (idx x) ++ tags (idx z) diff --git a/interpreter/syntax/operators.ml b/interpreter/syntax/operators.ml index e6b39aa3..42fa82cc 100644 --- a/interpreter/syntax/operators.ml +++ b/interpreter/syntax/operators.ml @@ -54,6 +54,7 @@ let cont_bind x y = ContBind (x, y) let suspend x = Suspend x let resume x xys = Resume (x, xys) let resume_throw x y xys = ResumeThrow (x, y, xys) +let resume_throw_ref x xys = ResumeThrowRef (x, xys) let switch x y = Switch (x, y) let throw x = Throw x let throw_ref = ThrowRef diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml index 9599265d..d369554c 100644 --- a/interpreter/text/arrange.ml +++ b/interpreter/text/arrange.ml @@ -561,6 +561,8 @@ let rec instr e = "resume " ^ var x, resumetable xys | ResumeThrow (x, y, xys) -> "resume_throw " ^ var x ^ " " ^ var y, resumetable xys + | ResumeThrowRef (x, xys) -> + "resume_throw_ref " ^ var x, resumetable xys | Switch (x, z) -> "switch " ^ var x ^ " " ^ var z, [] | Throw x -> "throw " ^ var x, [] diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index 9173e3c6..085865dd 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -658,6 +658,12 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in check_resume_table c ts2 xys e.at; (ts0 @ [RefT (Null, VarHT (StatX x.it))]) --> ts2, [] + | ResumeThrowRef (x, xys) -> + let ct = cont_type c x in + let FuncT (ts1, ts2) = func_type_of_cont_type c ct x.at in + check_resume_table c ts2 xys e.at; + ([RefT (Null, ExnHT); RefT (Null, VarHT (StatX x.it))]) --> ts2, [] + | Switch (x, y) -> let ct1 = cont_type c x in let FuncT (ts11, ts12) = func_type_of_cont_type c ct1 x.at in diff --git a/test/core/stack-switching/resume_throw.wast b/test/core/stack-switching/resume_throw.wast new file mode 100644 index 00000000..46114623 --- /dev/null +++ b/test/core/stack-switching/resume_throw.wast @@ -0,0 +1,286 @@ +;; Tests for resume_throw + +;; Test resume_throw on a continuation that is never resumed. +(module + (tag $exn) + + (type $f (func)) + (type $k (cont $f)) + + (func $never (unreachable)) + (elem declare func $never) + + (func (export "throw_never") + (block $h + (try_table (catch $exn $h) + (cont.new $k (ref.func $never)) + (resume_throw $k $exn) + (unreachable) + ) + ) + ) +) +(assert_return (invoke "throw_never")) + +;; Test resume_throw with a value type argument. +(module + (tag $exn_i32 (param i32)) + + (type $f (func)) + (type $k (cont $f)) + + (func $never (unreachable)) + (elem declare func $never) + + (func (export "throw_never_i32") (result i32) + (block $h (result i32) + (try_table (result i32) (catch $exn_i32 $h) + (i32.const 42) + (cont.new $k (ref.func $never)) + (resume_throw $k $exn_i32) + (unreachable) + ) + ) + ) +) + +(assert_return (invoke "throw_never_i32") (i32.const 42)) + +;; Test resume_throw with a reference type argument. +(module + (tag $exn_ref (param externref)) + + (type $f (func)) + (type $k (cont $f)) + + (func $never (unreachable)) + (elem declare func $never) + + (func (export "throw_never_ref") (param $val externref) (result externref) + (block $h (result externref) + (try_table (result externref) (catch $exn_ref $h) + (local.get $val) + (cont.new $k (ref.func $never)) + (resume_throw $k $exn_ref) + (unreachable) + ) + ) + ) +) +(assert_return (invoke "throw_never_ref" (ref.extern 1)) (ref.extern 1)) + +;; Test resume_throw where the continuation handles the exception. +(module + (tag $exn) + (tag $e1) + + (type $f (func)) + (type $k (cont $f)) + + (func $handler + (block $h + (try_table (catch $exn $h) + (suspend $e1) + ) + ) + ) + (elem declare func $handler) + + (func (export "throw_handled") + (block $h (result (ref $k)) + (resume $k (on $e1 $h) (cont.new $k (ref.func $handler))) + (unreachable) + ) + (resume_throw $k $exn) + ) +) +(assert_return (invoke "throw_handled")) + +;; Test resume_throw where the continuation does not handle the exception. +(module + (tag $exn) + (tag $e1) + + (type $f (func)) + (type $k (cont $f)) + + (func $no_handler + (suspend $e1) + ) + (elem declare func $no_handler) + + (func (export "throw_unhandled") + (block $h (result (ref $k)) + (resume $k (on $e1 $h) (cont.new $k (ref.func $no_handler))) + (unreachable) + ) + (resume_throw $k $exn) + ) +) +(assert_exception (invoke "throw_unhandled")) + +;; Test resume_throw on a consumed continuation. +(module + (tag $exn) + + (type $f (func)) + (type $k (cont $f)) + + (func $f1) + (elem declare func $f1) + + (func (export "throw_consumed") + (local $k_ref (ref $k)) + (local.set $k_ref (cont.new $k (ref.func $f1))) + (resume $k (local.get $k_ref)) ;; consume it + (resume_throw $k $exn (local.get $k_ref)) ;; should trap + ) +) +(assert_trap (invoke "throw_consumed") "continuation already consumed") + +;; Test resume_throw on a null continuation reference. +(module + (tag $exn) + (type $f (func)) + (type $k (cont $f)) + (func (export "throw_null") + (resume_throw $k $exn (ref.null $k)) + ) +) +(assert_trap (invoke "throw_null") "null continuation reference") + +;; Test resume_throw_ref where the continuation handles the exception. +(module + (tag $e0 (param i32)) + + (type $f (func (result i32))) + (type $k (cont $f)) + + (func (export "throw_handled_ref") (result i32) + (block $h (result exnref) + (try_table (catch_ref $e0 $h) (throw $e0 (i32.const 42))) + (unreachable) + ) + (resume_throw_ref $k (cont.new $k (ref.func $handler))) + ) + + (func $handler (result i32) + (block $h (result i32) + (try_table (catch_ref $e0 $h) + (unreachable) + ) + ) + ) + (elem declare func $handler) +) +(assert_return (invoke "throw_handled_ref") (i32.const 42)) + + +;; Test resume_throw_ref where the continuation does not handle the exception. +(module + (tag $e0) + + (type $f (func)) + (type $k (cont $f)) + + (func $no_handler + (unreachable) ;; We only throw into this function + ) + (elem declare func $no_handler) + + (func (export "throw_unhandled_ref") + (block $h (result exnref) + (try_table (catch_ref $e0 $h) (throw $e0)) + (unreachable) + ) + (resume_throw_ref $k (cont.new $k (ref.func $no_handler))) + ) +) +(assert_exception (invoke "throw_unhandled_ref")) + +;; Test resume_throw_ref on a consumed continuation. +(module + (tag $e0) + + (type $f (func)) + (type $k (cont $f)) + + (func $f1) + (elem declare func $f1) + + (func (export "throw_consumed_ref") + (local $k_ref (ref $k)) + (local.set $k_ref (cont.new $k (ref.func $f1))) + (resume $k (local.get $k_ref)) ;; consume it + (resume_throw_ref $k (local.get $k_ref)) ;; should trap + ) +) +(assert_trap (invoke "throw_consumed_ref") "continuation already consumed") + +;; Test resume_throw_ref on a null continuation reference. +(module + (tag $e0) + (type $f (func)) + (type $k (cont $f)) + (func (export "throw_null_ref") + (resume_throw_ref $k (ref.null $k)) + ) +) +(assert_trap (invoke "throw_null_ref") "null continuation reference") + +;; ---- Validation ---- + +(assert_invalid + (module + (type $ft (func)) + (type $ct (cont $ft)) + (tag $exn (param i32)) + (func + (i64.const 0) + (resume_throw $ct $exn (ref.null $ct)) + (unreachable))) + "type mismatch") + +(assert_invalid + (module + (type $ft (func)) + (type $ct (cont $ft)) + (tag $exn) + (func + (ref.null $ct) + (i32.const 0) + (resume_throw $ct $exn) + (unreachable))) + "type mismatch") + +(assert_invalid + (module + (type $ft (func)) + (type $ct (cont $ft)) + (tag $exn (param i32)) + (func + (resume_throw $ct $exn (ref.null $ct)) + (unreachable))) + "type mismatch") + + +(assert_invalid + (module + (type $ft (func)) + (type $ct (cont $ft)) + (tag $exn (param externref)) + (func + (i64.const 0) + (resume_throw_ref $ct $exn (ref.null $ct)) + (unreachable))) + "type mismatch") + +(assert_invalid + (module + (type $ft (func)) + (type $ct (cont $ft)) + (tag $exn (param externref)) + (func + (resume_throw_ref $ct $exn (ref.null $ct)) + (unreachable))) + "type mismatch") \ No newline at end of file diff --git a/test/core/throw_ref.wast b/test/core/throw_ref.wast index f59710a1..47216e2e 100644 --- a/test/core/throw_ref.wast +++ b/test/core/throw_ref.wast @@ -17,7 +17,8 @@ (try_table (result i32) (catch_ref $e0 $h) (throw $e0)) (return) ) - (if (param exnref) (i32.eqz (local.get 0)) + (if (param exnref + ) (i32.eqz (local.get 0)) (then (throw_ref)) (else (drop)) ) From 5ef83f2835bb51916a85bcab910c278c7908ad30 Mon Sep 17 00:00:00 2001 From: Francis McCabe Date: Thu, 16 Oct 2025 22:24:35 +0000 Subject: [PATCH 07/20] Add parsing of resume_throw_ref --- interpreter/text/lexer.mll | 1 + interpreter/text/parser.mly | 12 +++++++++++- test/core/stack-switching/resume_throw.wast | 5 ++--- 3 files changed, 14 insertions(+), 4 deletions(-) diff --git a/interpreter/text/lexer.mll b/interpreter/text/lexer.mll index cb124af8..001b4294 100644 --- a/interpreter/text/lexer.mll +++ b/interpreter/text/lexer.mll @@ -230,6 +230,7 @@ rule token = parse | "suspend" -> SUSPEND | "resume" -> RESUME | "resume_throw" -> RESUME_THROW + | "resume_throw_ref" -> RESUME_THROW_REF | "switch" -> SWITCH diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index c7f400e2..617b299b 100644 --- a/interpreter/text/parser.mly +++ b/interpreter/text/parser.mly @@ -304,7 +304,7 @@ let parse_annots (m : module_) : Custom.section list = %token MUT FIELD STRUCT ARRAY SUB FINAL REC %token UNREACHABLE NOP DROP SELECT %token BLOCK END IF THEN ELSE LOOP -%token CONT_NEW CONT_BIND SUSPEND RESUME RESUME_THROW SWITCH +%token CONT_NEW CONT_BIND SUSPEND RESUME RESUME_THROW RESUME_THROW_REF SWITCH %token BR BR_IF BR_TABLE BR_ON_NON_NULL %token Ast.instr'> BR_ON_NULL %token Types.ref_type -> Types.ref_type -> Ast.instr'> BR_ON_CAST @@ -789,6 +789,11 @@ resume_instr_instr_list : let x = $2 c type_ in let tag = $3 c tag in let hs, es = $4 c in (resume_throw x tag hs @@ loc1) :: es } + | RESUME_THROW_REF var resume_instr_handler_instr + { let loc1 = $loc($1) in + fun c -> + let x = $2 c type_ in + let hs, es = $3 c in (resume_throw_ref x hs @@ loc1) :: es } resume_instr_handler_instr : | LPAR ON var var RPAR resume_instr_handler_instr @@ -907,6 +912,11 @@ expr1 : /* Sugar */ let tag = $3 c tag in let hs, es = $4 c in es, resume_throw x tag hs } + | RESUME_THROW_REF var resume_expr_handler + { fun c -> + let x = $2 c type_ in + let hs, es = $3 c in + es, resume_throw_ref x hs } | BLOCK labeling_opt block { fun c -> let c' = $2 c [] in let bt, es = $3 c' in [], block bt es } | LOOP labeling_opt block diff --git a/test/core/stack-switching/resume_throw.wast b/test/core/stack-switching/resume_throw.wast index 46114623..046d115c 100644 --- a/test/core/stack-switching/resume_throw.wast +++ b/test/core/stack-switching/resume_throw.wast @@ -271,7 +271,7 @@ (tag $exn (param externref)) (func (i64.const 0) - (resume_throw_ref $ct $exn (ref.null $ct)) + (resume_throw_ref $ct (ref.null $ct)) (unreachable))) "type mismatch") @@ -279,8 +279,7 @@ (module (type $ft (func)) (type $ct (cont $ft)) - (tag $exn (param externref)) (func - (resume_throw_ref $ct $exn (ref.null $ct)) + (resume_throw_ref $ct (ref.null $ct)) (unreachable))) "type mismatch") \ No newline at end of file From a95b9a93d42a88c22bf63c75f566b958c12648d5 Mon Sep 17 00:00:00 2001 From: Francis McCabe Date: Thu, 16 Oct 2025 22:36:12 +0000 Subject: [PATCH 08/20] Fix funny in resume_throw_test (Still not right though) --- test/core/stack-switching/resume_throw.wast | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/core/stack-switching/resume_throw.wast b/test/core/stack-switching/resume_throw.wast index 046d115c..58b231a0 100644 --- a/test/core/stack-switching/resume_throw.wast +++ b/test/core/stack-switching/resume_throw.wast @@ -158,7 +158,7 @@ (func (export "throw_handled_ref") (result i32) (block $h (result exnref) - (try_table (catch_ref $e0 $h) (throw $e0 (i32.const 42))) + (try_table (catch_ref $e0 $h) (i32.const 42) (throw $e0)) (unreachable) ) (resume_throw_ref $k (cont.new $k (ref.func $handler))) From 3bc454809179e8103a94bfc8bc973d8e490fc581 Mon Sep 17 00:00:00 2001 From: Francis McCabe Date: Fri, 17 Oct 2025 18:40:19 +0000 Subject: [PATCH 09/20] Fixed issues. --- interpreter/exec/eval.ml | 11 +++--- test/core/stack-switching/resume_throw.wast | 44 +++++++++++++++++---- 2 files changed, 42 insertions(+), 13 deletions(-) diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index 0cf73eb5..c49f9fdf 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -407,17 +407,18 @@ let rec step (c : config) : config = cont := None; vs', [Prompt (hs, ctxt ([], [Throwing (tagt, args) @@ e.at])) @@ e.at] - | ResumeThrowRef (x, xls), Ref (NullRef _) :: vs -> + | ResumeThrowRef (x, xls), Ref _ :: Ref (NullRef _) :: vs -> vs, [Trapping "null exception reference" @@ e.at] - | ResumeThrowRef (x, xls), Ref _ :: Ref (NullRef _) :: vs -> + | ResumeThrowRef (x, xls), Ref (NullRef _) :: vs -> vs, [Trapping "null continuation reference" @@ e.at] - | ResumeThrowRef (x, xls), Ref _ :: Ref (ContRef {contents = None}) :: vs -> + | ResumeThrowRef (x, xls), Ref (ContRef {contents = None}) :: Ref _ :: vs -> vs, [Trapping "continuation already consumed" @@ e.at] - | ResumeThrowRef (x, xls), Ref (Exn.(ExnRef (Exn (tagt, args)))) :: - Ref (ContRef ({contents = Some (n, ctxt)} as cont)) :: vs -> + | ResumeThrowRef (x, xls), + Ref (ContRef ({contents = Some (n, ctxt)} as cont)) :: + Ref (Exn.(ExnRef (Exn (tagt, args)))) :: vs -> let hs = handle_table c xls in cont := None; vs, [Prompt (hs, ctxt ([], [Throwing (tagt, args) @@ e.at])) @@ e.at] diff --git a/test/core/stack-switching/resume_throw.wast b/test/core/stack-switching/resume_throw.wast index 58b231a0..64b676cf 100644 --- a/test/core/stack-switching/resume_throw.wast +++ b/test/core/stack-switching/resume_throw.wast @@ -152,26 +152,41 @@ ;; Test resume_throw_ref where the continuation handles the exception. (module (tag $e0 (param i32)) + (tag $yield) (type $f (func (result i32))) (type $k (cont $f)) (func (export "throw_handled_ref") (result i32) - (block $h (result exnref) - (try_table (catch_ref $e0 $h) (i32.const 42) (throw $e0)) + (local $k_ref (ref $k)) + (local.set $k_ref (cont.new $k (ref.func $yield42))) + + (block $y (result (ref $k)) + (resume $k (on $yield $y) + (local.get $k_ref)) + (return)) + (local.set $k_ref) + + (block $h (result i32 exnref) + (try_table (catch_ref $e0 $h) + (i32.const 42) + (throw $e0)) (unreachable) ) - (resume_throw_ref $k (cont.new $k (ref.func $handler))) + + (resume_throw_ref $k (local.get $k_ref)) + (return) ) - (func $handler (result i32) + (func $yield42 (result i32) (block $h (result i32) - (try_table (catch_ref $e0 $h) - (unreachable) + (try_table (result i32) (catch $e0 $h) + (suspend $yield) + (unreachable) ) ) ) - (elem declare func $handler) + (elem declare func $yield42) ) (assert_return (invoke "throw_handled_ref") (i32.const 42)) @@ -212,7 +227,15 @@ (local $k_ref (ref $k)) (local.set $k_ref (cont.new $k (ref.func $f1))) (resume $k (local.get $k_ref)) ;; consume it - (resume_throw_ref $k (local.get $k_ref)) ;; should trap + + (block $h (result exnref) + (try_table (catch_ref $e0 $h) + (throw $e0)) + (unreachable) + ) + (local.get $k_ref) + + (resume_throw_ref $k) ;; should trap ) ) (assert_trap (invoke "throw_consumed_ref") "continuation already consumed") @@ -223,6 +246,11 @@ (type $f (func)) (type $k (cont $f)) (func (export "throw_null_ref") + (block $h (result exnref) + (try_table (catch_ref $e0 $h) + (throw $e0)) + (unreachable) + ) (resume_throw_ref $k (ref.null $k)) ) ) From 62a58cc3b6a7702f1102872af69122f2131c388d Mon Sep 17 00:00:00 2001 From: Francis McCabe Date: Fri, 17 Oct 2025 19:56:14 +0000 Subject: [PATCH 10/20] Implement resume_throw_ref in decoder --- interpreter/binary/decode.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml index 68bddd9b..2ee875fe 100644 --- a/interpreter/binary/decode.ml +++ b/interpreter/binary/decode.ml @@ -646,7 +646,10 @@ let rec instr s = let tag = at var s in let xls = vec on_clause s in resume_throw x tag xls - (* TODO: resume_throw_ref *) + | 0xe5 -> + let x = at var s in + let xls = vec on_clause s in + resume_throw_ref x xls | 0xe6 -> let x = at var s in let y = at var s in From 7882f678e65052737b3c6899ccef3946b7dc87d2 Mon Sep 17 00:00:00 2001 From: Francis McCabe Date: Mon, 20 Oct 2025 09:09:16 -0700 Subject: [PATCH 11/20] Update interpreter/binary/decode.ml remove extra space Co-authored-by: Andreas Rossberg --- interpreter/binary/decode.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml index 2ee875fe..749007f3 100644 --- a/interpreter/binary/decode.ml +++ b/interpreter/binary/decode.ml @@ -647,7 +647,7 @@ let rec instr s = let xls = vec on_clause s in resume_throw x tag xls | 0xe5 -> - let x = at var s in + let x = at var s in let xls = vec on_clause s in resume_throw_ref x xls | 0xe6 -> From a1dee474716d5d108681d7cdf4fd4325fe5aa239 Mon Sep 17 00:00:00 2001 From: Francis McCabe Date: Mon, 20 Oct 2025 09:10:21 -0700 Subject: [PATCH 12/20] Update interpreter/valid/valid.ml mark pattern variable as not used Co-authored-by: Thomas Lively --- interpreter/valid/valid.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index 085865dd..7754c7bb 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -660,7 +660,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in | ResumeThrowRef (x, xys) -> let ct = cont_type c x in - let FuncT (ts1, ts2) = func_type_of_cont_type c ct x.at in + let FuncT (_ts1, ts2) = func_type_of_cont_type c ct x.at in check_resume_table c ts2 xys e.at; ([RefT (Null, ExnHT); RefT (Null, VarHT (StatX x.it))]) --> ts2, [] From 433effcf00f5493ed79aa30b748856b243674ccc Mon Sep 17 00:00:00 2001 From: Francis McCabe Date: Mon, 20 Oct 2025 09:13:44 -0700 Subject: [PATCH 13/20] Update test/core/stack-switching/resume_throw.wast Co-authored-by: Thomas Lively --- test/core/stack-switching/resume_throw.wast | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/core/stack-switching/resume_throw.wast b/test/core/stack-switching/resume_throw.wast index 64b676cf..42cd8f58 100644 --- a/test/core/stack-switching/resume_throw.wast +++ b/test/core/stack-switching/resume_throw.wast @@ -182,7 +182,7 @@ (block $h (result i32) (try_table (result i32) (catch $e0 $h) (suspend $yield) - (unreachable) + (unreachable) ) ) ) From 39ce64382301f9656bf5489df2c0cc328a5d6268 Mon Sep 17 00:00:00 2001 From: Francis McCabe Date: Mon, 20 Oct 2025 09:14:08 -0700 Subject: [PATCH 14/20] Update test/core/stack-switching/resume_throw.wast Co-authored-by: Thomas Lively --- test/core/stack-switching/resume_throw.wast | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/core/stack-switching/resume_throw.wast b/test/core/stack-switching/resume_throw.wast index 42cd8f58..47c7c74d 100644 --- a/test/core/stack-switching/resume_throw.wast +++ b/test/core/stack-switching/resume_throw.wast @@ -310,4 +310,4 @@ (func (resume_throw_ref $ct (ref.null $ct)) (unreachable))) - "type mismatch") \ No newline at end of file + "type mismatch") From b6612c1c4555c12ffffdfa78240a68e85ef8efe2 Mon Sep 17 00:00:00 2001 From: Francis McCabe Date: Mon, 20 Oct 2025 09:16:02 -0700 Subject: [PATCH 15/20] Update test/core/stack-switching/resume_throw.wast Co-authored-by: Thomas Lively --- test/core/stack-switching/resume_throw.wast | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/test/core/stack-switching/resume_throw.wast b/test/core/stack-switching/resume_throw.wast index 47c7c74d..c34c0711 100644 --- a/test/core/stack-switching/resume_throw.wast +++ b/test/core/stack-switching/resume_throw.wast @@ -229,9 +229,9 @@ (resume $k (local.get $k_ref)) ;; consume it (block $h (result exnref) - (try_table (catch_ref $e0 $h) - (throw $e0)) - (unreachable) + (try_table (result exnref) (catch_ref $e0 $h) + (throw $e0) + ) ) (local.get $k_ref) From a95dcb4d08ec77c7b312a90d4fde79ec05b8faf7 Mon Sep 17 00:00:00 2001 From: Francis McCabe Date: Mon, 20 Oct 2025 09:16:28 -0700 Subject: [PATCH 16/20] Update test/core/throw_ref.wast Co-authored-by: Thomas Lively --- test/core/throw_ref.wast | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/core/throw_ref.wast b/test/core/throw_ref.wast index 47216e2e..a920ff1d 100644 --- a/test/core/throw_ref.wast +++ b/test/core/throw_ref.wast @@ -17,8 +17,8 @@ (try_table (result i32) (catch_ref $e0 $h) (throw $e0)) (return) ) - (if (param exnref - ) (i32.eqz (local.get 0)) + (if (param exnref) + (i32.eqz (local.get 0)) (then (throw_ref)) (else (drop)) ) From 1e71133bf8d952672f659914d4fc4750642b827d Mon Sep 17 00:00:00 2001 From: Francis McCabe Date: Mon, 20 Oct 2025 09:16:54 -0700 Subject: [PATCH 17/20] Update test/core/stack-switching/resume_throw.wast Co-authored-by: Thomas Lively --- test/core/stack-switching/resume_throw.wast | 1 - 1 file changed, 1 deletion(-) diff --git a/test/core/stack-switching/resume_throw.wast b/test/core/stack-switching/resume_throw.wast index c34c0711..29e3b561 100644 --- a/test/core/stack-switching/resume_throw.wast +++ b/test/core/stack-switching/resume_throw.wast @@ -43,7 +43,6 @@ ) ) ) - (assert_return (invoke "throw_never_i32") (i32.const 42)) ;; Test resume_throw with a reference type argument. From 8aded36cfb9cff0a2303f9838b63af056f9fa20b Mon Sep 17 00:00:00 2001 From: Francis McCabe Date: Mon, 20 Oct 2025 11:22:07 -0700 Subject: [PATCH 18/20] Update test/core/stack-switching/resume_throw.wast Co-authored-by: Thomas Lively --- test/core/stack-switching/resume_throw.wast | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/core/stack-switching/resume_throw.wast b/test/core/stack-switching/resume_throw.wast index 29e3b561..e674add8 100644 --- a/test/core/stack-switching/resume_throw.wast +++ b/test/core/stack-switching/resume_throw.wast @@ -163,7 +163,7 @@ (block $y (result (ref $k)) (resume $k (on $yield $y) (local.get $k_ref)) - (return)) + (unreachable)) (local.set $k_ref) (block $h (result i32 exnref) From 4d84e15eb38a780115f39d8828726a87d9b23ada Mon Sep 17 00:00:00 2001 From: Francis McCabe Date: Mon, 20 Oct 2025 11:22:51 -0700 Subject: [PATCH 19/20] Update interpreter/exec/eval.ml Co-authored-by: Andreas Rossberg --- interpreter/exec/eval.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index c49f9fdf..3993697d 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -418,10 +418,10 @@ let rec step (c : config) : config = | ResumeThrowRef (x, xls), Ref (ContRef ({contents = Some (n, ctxt)} as cont)) :: - Ref (Exn.(ExnRef (Exn (tagt, args)))) :: vs -> + v :: vs -> let hs = handle_table c xls in cont := None; - vs, [Prompt (hs, ctxt ([], [Throwing (tagt, args) @@ e.at])) @@ e.at] + vs, [Prompt (hs, ctxt ([v], [ThrowRef @@ e.at])) @@ e.at] | Switch (x, y), Ref (NullRef _) :: vs -> vs, [Trapping "null continuation reference" @@ e.at] From 586ae27b2f42282f1fb4514002bcb4fdbe7b123f Mon Sep 17 00:00:00 2001 From: Francis McCabe Date: Mon, 20 Oct 2025 18:42:43 +0000 Subject: [PATCH 20/20] Refactor implementation of ResumeThrowRef and add some comments to tests. --- interpreter/exec/eval.ml | 2 +- test/core/stack-switching/resume_throw.wast | 10 +++++----- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index 3993697d..32b80606 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -421,7 +421,7 @@ let rec step (c : config) : config = v :: vs -> let hs = handle_table c xls in cont := None; - vs, [Prompt (hs, ctxt ([v], [ThrowRef @@ e.at])) @@ e.at] + vs, [Prompt (hs, ctxt ([v], [Plain ThrowRef @@ e.at])) @@ e.at] | Switch (x, y), Ref (NullRef _) :: vs -> vs, [Trapping "null continuation reference" @@ e.at] diff --git a/test/core/stack-switching/resume_throw.wast b/test/core/stack-switching/resume_throw.wast index e674add8..2b19f367 100644 --- a/test/core/stack-switching/resume_throw.wast +++ b/test/core/stack-switching/resume_throw.wast @@ -264,7 +264,7 @@ (tag $exn (param i32)) (func (i64.const 0) - (resume_throw $ct $exn (ref.null $ct)) + (resume_throw $ct $exn (ref.null $ct)) ;; null continuation (unreachable))) "type mismatch") @@ -276,7 +276,7 @@ (func (ref.null $ct) (i32.const 0) - (resume_throw $ct $exn) + (resume_throw $ct $exn) ;; exception tag does not take paramter (unreachable))) "type mismatch") @@ -286,7 +286,7 @@ (type $ct (cont $ft)) (tag $exn (param i32)) (func - (resume_throw $ct $exn (ref.null $ct)) + (resume_throw $ct $exn (ref.null $ct)) ;; missing exception payload (unreachable))) "type mismatch") @@ -298,7 +298,7 @@ (tag $exn (param externref)) (func (i64.const 0) - (resume_throw_ref $ct (ref.null $ct)) + (resume_throw_ref $ct (ref.null $ct)) ;; expecting an exception ref (unreachable))) "type mismatch") @@ -307,6 +307,6 @@ (type $ft (func)) (type $ct (cont $ft)) (func - (resume_throw_ref $ct (ref.null $ct)) + (resume_throw_ref $ct (ref.null $ct)) ;; expecting an exception ref (unreachable))) "type mismatch")