Skip to content

Named handlers #129

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: named-handlers
Choose a base branch
from
Open

Named handlers #129

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 16 additions & 0 deletions interpreter/binary/decode.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -193,6 +193,8 @@ let heap_type s =
| -0x16 -> ArrayHT
| -0x17 -> ExnHT
| -0x18 -> ContHT
| -0x1e -> HandlerHT
| -0x1a -> NoHandlerHT
| _ -> error s pos "malformed heap type"
)
] s
Expand All @@ -214,6 +216,8 @@ let ref_type s =
| -0x16 -> (Null, ArrayHT)
| -0x17 -> (Null, ExnHT)
| -0x18 -> (Null, ContHT)
| -0x19 -> (Null, HandlerHT)
| -0x1a -> (Null, NoHandlerHT)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's getting crowded here...

| -0x1c -> (NoNull, heap_type s)
| -0x1d -> (Null, heap_type s)
| _ -> error s pos "malformed reference type"
Expand Down Expand Up @@ -259,12 +263,16 @@ let func_type s =
let cont_type s =
ContT (heap_type s)

let handler_type s =
HandlerT (result_type s)

let str_type s =
match s7 s with
| -0x20 -> DefFuncT (func_type s)
| -0x21 -> DefStructT (struct_type s)
| -0x22 -> DefArrayT (array_type s)
| -0x23 -> DefContT (cont_type s) (* TODO(dhil): See comment in encode.ml *)
| -0x24 -> DefHandlerT (handler_type s)
| _ -> error s (pos s - 1) "malformed definition type"

let sub_type s =
Expand Down Expand Up @@ -650,6 +658,14 @@ let rec instr s =
let x = at var s in
let y = at var s in
switch x y
| 0xe7 ->
let x = at var s in
let y = at var s in
suspend_to x y
| 0xe8 ->
let x = at var s in
let xls = vec on_clause s in
resume_with x xls

| 0xfb as b ->
(match u32 s with
Expand Down
8 changes: 8 additions & 0 deletions interpreter/binary/encode.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -132,6 +132,8 @@ struct
| NoExternHT -> s7 (-0x0e)
| ContHT -> s7 (-0x18)
| NoContHT -> s7 (-0x0b)
| HandlerHT -> s7 (-0x1e)
| NoHandlerHT -> s7 (-0x1a)
| VarHT x -> var_type s33 x
| DefHT _ | BotHT -> assert false

Expand Down Expand Up @@ -187,6 +189,9 @@ struct
let cont_type = function
| ContT ht -> heap_type ht

let handler_type = function
| HandlerT ts -> vec val_type ts

let str_type = function
| DefStructT st -> s7 (-0x21); struct_type st
| DefArrayT at -> s7 (-0x22); array_type at
Expand All @@ -195,6 +200,7 @@ struct
(* TODO(dhil): This might need to change again in the future as a
different proposal might claim this opcode! GC proposal claimed
the previous opcode we were using. *)
| DefHandlerT ht -> s7 (-0x24); handler_type ht

let sub_type = function
| SubT (Final, [], st) -> str_type st
Expand Down Expand Up @@ -301,8 +307,10 @@ struct
| ContNew x -> op 0xe0; var x
| ContBind (x, y) -> op 0xe1; var x; var y
| Suspend x -> op 0xe2; var x
| SuspendTo (x, y) -> op 0xe7; var x; var y
| Resume (x, xls) -> op 0xe3; var x; resumetable xls
| ResumeThrow (x, y, xls) -> op 0xe4; var x; var y; resumetable xls
| ResumeWith (x, xls) -> op 0xe8; var x; resumetable xls
| Switch (x, y) -> op 0xe5; var x; var y

| Throw x -> op 0x08; var x
Expand Down
95 changes: 67 additions & 28 deletions interpreter/exec/eval.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,7 @@ type frame =
}

type code = value stack * admin_instr list
and handler_name = exn

and admin_instr = admin_instr' phrase
and admin_instr' =
Expand All @@ -72,25 +73,28 @@ and admin_instr' =
| Label of int * instr list * code
| Frame of int * frame * code
| Handler of int * catch list * code
| Prompt of handle_table * code
| Suspending of tag_inst * value stack * (int32 * ref_) option * ctxt
| Prompt of handler_name option * handle_table * code
| Suspending of tag_inst * value stack * (int32 * ref_) option * ref_ option * ctxt

and ctxt = code -> code
and handle_table = (tag_inst * idx) list * tag_inst list

type cont = int32 * ctxt (* TODO: represent type properly *)
type ref_ += ContRef of cont option ref
| HandlerRef of handler_name option ref
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
| HandlerRef of handler_name option ref
type ref_ += HandlerRef of handler_name option ref


let () =
let type_of_ref' = !Value.type_of_ref' in
Value.type_of_ref' := function
| ContRef _ -> ContHT
| HandlerRef _ -> HandlerHT
| r -> type_of_ref' r

let () =
let string_of_ref' = !Value.string_of_ref' in
Value.string_of_ref' := function
| ContRef _ -> "cont"
| HandlerRef _ -> "handler"
| r -> string_of_ref' r

let plain e = Plain e.it @@ e.at
Expand Down Expand Up @@ -379,7 +383,18 @@ let rec step (c : config) : config =
let tagt = tag c.frame.inst x in
let FuncT (ts, _) = func_type_of_tag_type c.frame.inst (Tag.type_of tagt) in
let args, vs' = i32_split (Lib.List32.length ts) vs e.at in
vs', [Suspending (tagt, args, None, fun code -> code) @@ e.at]
vs', [Suspending (tagt, args, None, None, fun code -> code) @@ e.at]

| SuspendTo (x, y), vs ->
let tagt = tag c.frame.inst y in
let FuncT (ts, _) = func_type_of_tag_type c.frame.inst (Tag.type_of tagt) in
let args, vs' = i32_split (Int32.add (Lib.List32.length ts) 1l) vs e.at in
let args, href =
match args with
| Ref r :: rest -> rest, r
| _ -> Crash.error e.at "type mismatch at suspend to"
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
| _ -> Crash.error e.at "type mismatch at suspend to"
| _ -> Crash.error e.at "type mismatch at suspend_to"

in
vs', [Suspending (tagt, args, None, Some href, fun code -> code) @@ e.at]

| Resume (x, xls), Ref (NullRef _) :: vs ->
vs, [Trapping "null continuation reference" @@ e.at]
Expand All @@ -391,7 +406,7 @@ let rec step (c : config) : config =
let hs = handle_table c xls in
let args, vs' = i32_split n vs e.at in
cont := None;
vs', [Prompt (hs, ctxt (args, [])) @@ e.at]
vs', [Prompt (None, hs, ctxt (args, [])) @@ e.at]

| ResumeThrow (x, y, xls), Ref (NullRef _) :: vs ->
vs, [Trapping "null continuation reference" @@ e.at]
Expand All @@ -405,7 +420,23 @@ let rec step (c : config) : config =
let hs = handle_table c xls in
let args, vs' = i32_split (Lib.List32.length ts) vs e.at in
cont := None;
vs', [Prompt (hs, ctxt ([], [Throwing (tagt, args) @@ e.at])) @@ e.at]
vs', [Prompt (None, hs, ctxt ([], [Throwing (tagt, args) @@ e.at])) @@ e.at]

| ResumeWith (x, xls), Ref (NullRef _) :: vs ->
vs, [Trapping "null continuation reference" @@ e.at]

| ResumeWith (x, xls), Ref (ContRef {contents = None}) :: vs ->
vs, [Trapping "continuation already consumed" @@ e.at]

| ResumeWith (x, xls), Ref (ContRef ({contents = Some (n, ctxt)} as cont)) :: vs ->
let hs = handle_table c xls in
let args, vs' = i32_split (Int32.sub n 1l) vs e.at in
let exception Name in
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Instead of abusing exceptions, can we define our own extensible datatype prompt_name above and extend that here? Unfortunately, this:

Suggested change
let exception Name in
let type prompt_name += Name in

doesn't work, you'll have to do

Suggested change
let exception Name in
let module N = struct type prompt_name += Name end in

and use N.name.

let name =
Ref (HandlerRef (ref (Some Name)))
in
Comment on lines +435 to +437
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
let name =
Ref (HandlerRef (ref (Some Name)))
in
let name = Ref (HandlerRef (ref (Some Name))) in

cont := None;
vs', [Prompt (Some Name, hs, ctxt (name :: args, [])) @@ e.at]

| Switch (x, y), Ref (NullRef _) :: vs ->
vs, [Trapping "null continuation reference" @@ e.at]
Expand All @@ -419,7 +450,7 @@ let rec step (c : config) : config =
let arity = Lib.List32.length ts' in
let tagt = tag c.frame.inst y in
let args, vs' = i32_split (Int32.sub n 1l) vs e.at in
vs', [Suspending (tagt, args, Some (arity, ContRef cont), fun code -> code) @@ e.at]
vs', [Suspending (tagt, args, Some (arity, ContRef cont), None, fun code -> code) @@ e.at]

| ReturnCall x, vs ->
(match (step {c with code = (vs, [Plain (Call x) @@ e.at])}).code with
Expand Down Expand Up @@ -1180,9 +1211,9 @@ let rec step (c : config) : config =
| Label (n, es0, (vs', [])), vs ->
vs' @ vs, []

| Label (n, es0, (vs', {it = Suspending (tagt, vs1, contref, ctxt); at} :: es')), vs ->
| Label (n, es0, (vs', {it = Suspending (tagt, vs1, contref, href, ctxt); at} :: es')), vs ->
let ctxt' code = [], [Label (n, es0, compose (ctxt code) (vs', es')) @@ e.at] in
vs, [Suspending (tagt, vs1, contref, ctxt') @@ at]
vs, [Suspending (tagt, vs1, contref, href, ctxt') @@ at]

| Label (n, es0, (vs', {it = ReturningInvoke (vs0, f); at} :: es')), vs ->
vs, [ReturningInvoke (vs0, f) @@ at]
Expand All @@ -1209,9 +1240,9 @@ let rec step (c : config) : config =
| Frame (n, frame', (vs', {it = Throwing (a, vs0); at} :: es')), vs ->
vs, [Throwing (a, vs0) @@ at]

| Frame (n, frame', (vs', {it = Suspending (tagt, vs1, contref, ctxt); at} :: es')), vs ->
| Frame (n, frame', (vs', {it = Suspending (tagt, vs1, contref, href, ctxt); at} :: es')), vs ->
let ctxt' code = [], [Frame (n, frame', compose (ctxt code) (vs', es')) @@ e.at] in
vs, [Suspending (tagt, vs1, contref, ctxt') @@ at]
vs, [Suspending (tagt, vs1, contref, href, ctxt') @@ at]

| Frame (n, frame', (vs', {it = Returning vs0; at} :: es')), vs ->
take n vs0 e.at @ vs, []
Expand Down Expand Up @@ -1251,9 +1282,9 @@ let rec step (c : config) : config =
| Handler (n, [], (vs', {it = Throwing (a, vs0); at} :: es')), vs ->
vs, [Throwing (a, vs0) @@ at]

| Handler (n, cs, (vs', {it = Suspending (tagt, vs1, contref, ctxt); at} :: es')), vs ->
| Handler (n, cs, (vs', {it = Suspending (tagt, vs1, contref, href, ctxt); at} :: es')), vs ->
let ctxt' code = [], [Handler (n, cs, compose (ctxt code) (vs', es')) @@ e.at] in
vs, [Suspending (tagt, vs1, contref, ctxt') @@ at]
vs, [Suspending (tagt, vs1, contref, href, ctxt') @@ at]

| Handler (n, cs, (vs', e' :: es')), vs when is_jumping e' ->
vs, [e']
Expand Down Expand Up @@ -1285,36 +1316,44 @@ let rec step (c : config) : config =
with Crash (_, msg) -> Crash.error e.at msg)
)

| Prompt (hso, (vs', [])), vs ->
| Prompt (name, hso, (vs', [])), vs ->
vs' @ vs, []

| Prompt ((hs, _), (vs', {it = Suspending (tagt, vs1, None, ctxt); at} :: es')), vs
| Prompt (name, (hs, _), (vs', {it = Suspending (tagt, vs1, None, None, ctxt); at} :: es')), vs
when List.mem_assq tagt hs ->
let FuncT (_, ts) = func_type_of_tag_type c.frame.inst (Tag.type_of tagt) in
let ctxt' code = compose (ctxt code) (vs', es') in
[Ref (ContRef (ref (Some (Lib.List32.length ts, ctxt'))))] @ vs1 @ vs,
[Plain (Br (List.assq tagt hs)) @@ e.at]

| Prompt ((_, hs) as hso, (vs', {it = Suspending (tagt, vs1, Some (ar, ContRef ({contents = Some (_, ctxt)} as cont)), ctxt'); at} :: es')), vs
when List.memq tagt hs ->
let ctxt'' code = compose (ctxt' code) (vs', es') in
let cont' = Ref (ContRef (ref (Some (ar, ctxt'')))) in
let args = cont' :: vs1 in
cont := None;
vs' @ vs, [Prompt (hso, ctxt (args, [])) @@ e.at]
| Prompt (Some h, (hs, _), (vs', {it = Suspending (tagt, vs1, None, Some (HandlerRef ({contents = Some h'} as href)), ctxt); at} :: es')), vs
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wonder if we can avoid doubling the rules by factoring out an auxiliary

let matches_name name1 name2 =
  match name1, name2 with
  | None, _-> true
  | _, None -> false
  | Some n1, Some n2 -> n1 == n2

when h == h' && List.mem_assq tagt hs ->
let FuncT (_, ts) = func_type_of_tag_type c.frame.inst (Tag.type_of tagt) in
let ctxt' code = compose (ctxt code) (vs', es') in
href := None;
[Ref (ContRef (ref (Some (Int32.add (Lib.List32.length ts) 1l, ctxt'))))] @ vs1 @ vs,
[Plain (Br (List.assq tagt hs)) @@ e.at]

| Prompt (None, ((_, hs) as hso), (vs', {it = Suspending (tagt, vs1, Some (ar, ContRef ({contents = Some (_, ctxt)} as cont)), None, ctxt'); at} :: es')), vs
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Isn't this missing an equivalent rule for bubbling a named Suspending? (But see previous comment about avoiding duplication.)

when List.memq tagt hs ->
let ctxt'' code = compose (ctxt' code) (vs', es') in
let cont' = Ref (ContRef (ref (Some (ar, ctxt'')))) in
let args = cont' :: vs1 in
cont := None;
vs' @ vs, [Prompt (None, hso, ctxt (args, [])) @@ e.at]

| Prompt (hso, (vs', {it = Suspending (tagt, vs1, contref, ctxt); at} :: es')), vs ->
let ctxt' code = [], [Prompt (hso, compose (ctxt code) (vs', es')) @@ e.at] in
vs, [Suspending (tagt, vs1, contref, ctxt') @@ at]
| Prompt (name, hso, (vs', {it = Suspending (tagt, vs1, contref, href, ctxt); at} :: es')), vs ->
let ctxt' code = [], [Prompt (name, hso, compose (ctxt code) (vs', es')) @@ e.at] in
vs, [Suspending (tagt, vs1, contref, href, ctxt') @@ at]

| Prompt (hso, (vs', e' :: es')), vs when is_jumping e' ->
| Prompt (name, hso, (vs', e' :: es')), vs when is_jumping e' ->
vs, [e']

| Prompt (hso, code'), vs ->
| Prompt (name, hso, code'), vs ->
let c' = step {c with code = code'} in
vs, [Prompt (hso, c'.code) @@ e.at]
vs, [Prompt (name, hso, c'.code) @@ e.at]

| Suspending (_, _, _, _), _ -> assert false
| Suspending (_, _, _, _, _), _ -> assert false

in {c with code = vs', es' @ List.tl es}

Expand Down
2 changes: 2 additions & 0 deletions interpreter/syntax/ast.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -175,8 +175,10 @@ and instr' =
| ContNew of idx (* create continuation *)
| ContBind of idx * idx (* bind continuation arguments *)
| Suspend of idx (* suspend continuation *)
| SuspendTo of idx * idx (* named suspend continuation *)
| Resume of idx * (idx * hdl) list (* resume continuation *)
| ResumeThrow of idx * idx * (idx * hdl) list (* abort continuation *)
| ResumeWith of idx * (idx * hdl) list (* named resume continuation *)
| Switch of idx * idx (* direct switch continuation *)
| Throw of idx (* throw exception *)
| ThrowRef (* rethrow exception *)
Expand Down
5 changes: 5 additions & 0 deletions interpreter/syntax/free.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -82,6 +82,7 @@ let heap_type = function
| ExnHT | NoExnHT -> empty
| ExternHT | NoExternHT -> empty
| ContHT | NoContHT -> empty
| HandlerHT | NoHandlerHT -> empty
| VarHT x -> var_type x
| DefHT _ct -> empty (* assume closed *)
| BotHT -> empty
Expand Down Expand Up @@ -109,12 +110,14 @@ let field_type (FieldT (_mut, st)) = storage_type st
let struct_type (StructT fts) = list field_type fts
let array_type (ArrayT ft) = field_type ft
let func_type (FuncT (ts1, ts2)) = list val_type ts1 ++ list val_type ts2
let handler_type (HandlerT ts) = list val_type ts

let str_type = function
| DefStructT st -> struct_type st
| DefArrayT at -> array_type at
| DefFuncT ft -> func_type ft
| DefContT ct -> cont_type ct
| DefHandlerT ht -> handler_type ht

let sub_type = function
| SubT (_fin, hts, st) -> list heap_type hts ++ str_type st
Expand Down Expand Up @@ -182,7 +185,9 @@ let rec instr (e : instr) =
| 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
| Resume (x, xys) -> types (idx x) ++ list (fun (x, y) -> tags (idx x) ++ hdl y) xys
| ResumeWith (x, xys) -> types (idx x) ++ list (fun (x, y) -> tags (idx x) ++ hdl y) xys
| Suspend x -> tags (idx x)
| SuspendTo (x, y) -> types (idx x) ++ tags (idx y)
| Switch (x, z) -> types (idx x) ++ tags (idx z)
| Throw x -> tags (idx x)
| ThrowRef -> empty
Expand Down
2 changes: 2 additions & 0 deletions interpreter/syntax/operators.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,8 +52,10 @@ let return_call_indirect x y = ReturnCallIndirect (x, y)
let cont_new x = ContNew x
let cont_bind x y = ContBind (x, y)
let suspend x = Suspend x
let suspend_to x y = SuspendTo (x, y)
let resume x xys = Resume (x, xys)
let resume_throw x y xys = ResumeThrow (x, y, xys)
let resume_with x xys = ResumeWith (x, xys)
let switch x y = Switch (x, y)
let throw x = Throw x
let throw_ref = ThrowRef
Expand Down
Loading