Skip to content

Commit

Permalink
Add cont.bind; check handler types
Browse files Browse the repository at this point in the history
  • Loading branch information
rossberg committed Apr 8, 2021
1 parent 261d1a8 commit ee429ef
Show file tree
Hide file tree
Showing 14 changed files with 103 additions and 25 deletions.
9 changes: 5 additions & 4 deletions interpreter/binary/decode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -553,10 +553,11 @@ let rec instr s =
| 0xd4 -> br_on_null (at var s)

| 0xe0 -> cont_new (at var s)
| 0xe1 -> suspend (at var s)
| 0xe2 -> resume (vec var_pair s)
| 0xe3 -> resume_throw (at var s)
| 0xe4 ->
| 0xe1 -> cont_bind (at var s)
| 0xe2 -> suspend (at var s)
| 0xe3 -> resume (vec var_pair s)
| 0xe4 -> resume_throw (at var s)
| 0xe5 ->
let bt = block_type s in
let es' = instr_block s in
end_ s;
Expand Down
9 changes: 5 additions & 4 deletions interpreter/binary/encode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -215,10 +215,11 @@ struct
| FuncBind x -> op 0x16; var x

| ContNew x -> op 0xe0; var x
| Suspend x -> op 0xe1; var x
| Resume xls -> op 0xe2; vec var_pair xls
| ResumeThrow x -> op 0xe3; var x
| Barrier (bt, es) -> op 0xe4; block_type bt; list instr es; end_ ()
| ContBind x -> op 0xe1; var x
| Suspend x -> op 0xe2; var x
| Resume xls -> op 0xe3; vec var_pair xls
| ResumeThrow x -> op 0xe4; var x
| Barrier (bt, es) -> op 0xe5; block_type bt; list instr es; end_ ()

| Drop -> op 0x1a
| Select None -> op 0x1b
Expand Down
22 changes: 20 additions & 2 deletions interpreter/exec/eval.ml
Original file line number Diff line number Diff line change
Expand Up @@ -131,6 +131,7 @@ let data (inst : module_inst) x = lookup "data segment" inst.datas x
let local (frame : frame) x = lookup "local" frame.locals x

let func_type (inst : module_inst) x = as_func_def_type (def_of (type_ inst x))
let cont_type (inst : module_inst) x = as_cont_def_type (def_of (type_ inst x))

let any_ref inst x i at =
try Table.load (table inst x) i with Table.Bounds ->
Expand Down Expand Up @@ -316,6 +317,23 @@ let rec step (c : config) : config =
let ctxt code = compose code ([], [Invoke f @@ e.at]) in
Ref (ContRef (ref (Some (List.length ts, ctxt)))) :: vs, []

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

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

| ContBind x, Ref (ContRef ({contents = Some (n, ctxt)} as cont)) :: vs ->
let ContType z = cont_type c.frame.inst x in
let FuncType (ts', _) = as_func_def_type (def_of (as_sem_var z)) in
let args, vs' =
try split (n - List.length ts') vs e.at
with Failure _ -> Crash.error e.at "type mismatch at continuation bind"
in
cont := None;
let ctxt' code = ctxt (compose (args, []) code) in
Ref (ContRef (ref (Some (n - List.length args, ctxt')))) :: vs, []

| Suspend x, vs ->
let evt = event c.frame.inst x in
let EventType (FuncType (ts, _), _) = Event.type_of evt in
Expand All @@ -326,7 +344,7 @@ let rec step (c : config) : config =
vs, [Trapping "null continuation reference" @@ e.at]

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

| Resume xls, Ref (ContRef ({contents = Some (n, ctxt)} as cont)) :: vs ->
let hs = List.map (fun (x, l) -> event c.frame.inst x, l) xls in
Expand All @@ -338,7 +356,7 @@ let rec step (c : config) : config =
vs, [Trapping "null continuation reference" @@ e.at]

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

| ResumeThrow x, Ref (ContRef ({contents = Some (n, ctxt)} as cont)) :: vs ->
let evt = event c.frame.inst x in
Expand Down
1 change: 1 addition & 0 deletions interpreter/syntax/ast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -99,6 +99,7 @@ and instr' =
| ReturnCallIndirect of idx * idx (* tail-call function through table *)
| FuncBind of idx (* create closure *)
| ContNew of idx (* create continuation *)
| ContBind of idx (* bind continuation arguments *)
| Suspend of idx (* suspend continuation *)
| Resume of (idx * idx) list (* resume continuation *)
| ResumeThrow of idx (* abort continuation *)
Expand Down
2 changes: 1 addition & 1 deletion interpreter/syntax/free.ml
Original file line number Diff line number Diff line change
Expand Up @@ -123,7 +123,7 @@ let rec instr (e : instr) =
| Call x | ReturnCall x -> funcs (idx x)
| CallIndirect (x, y) | ReturnCallIndirect (x, y) ->
tables (idx x) ++ types (idx y)
| FuncBind x | ContNew x -> types (idx x)
| FuncBind x | ContNew x | ContBind x -> types (idx x)
| Resume xys -> list (fun (x, y) -> events (idx x) ++ labels (idx y)) xys
| LocalGet x | LocalSet x | LocalTee x -> locals (idx x)
| GlobalGet x | GlobalSet x -> globals (idx x)
Expand Down
1 change: 1 addition & 0 deletions interpreter/syntax/operators.ml
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@ let return_call_indirect x y = ReturnCallIndirect (x, y)
let func_bind x = FuncBind x

let cont_new x = ContNew x
let cont_bind x = ContBind x
let suspend x = Suspend x
let resume xys = Resume xys
let resume_throw x = ResumeThrow x
Expand Down
9 changes: 9 additions & 0 deletions interpreter/syntax/types.ml
Original file line number Diff line number Diff line change
Expand Up @@ -81,11 +81,20 @@ let as_syn_var = function
| SynVar x -> x
| SemVar _ -> assert false

let as_sem_var = function
| SynVar _ -> assert false
| SemVar x -> x

let as_func_def_type (dt : def_type) : func_type =
match dt with
| FuncDefType ft -> ft
| _ -> assert false

let as_cont_def_type (dt : def_type) : cont_type =
match dt with
| ContDefType x -> x
| _ -> assert false

let extern_type_of_import_type (ImportType (et, _, _)) = et
let extern_type_of_export_type (ExportType (et, _)) = et

Expand Down
1 change: 1 addition & 0 deletions interpreter/text/arrange.ml
Original file line number Diff line number Diff line change
Expand Up @@ -279,6 +279,7 @@ let rec instr e =
"return_call_indirect " ^ var x, [Node ("type " ^ var y, [])]
| FuncBind x -> "func.bind", [Node ("type " ^ var x, [])]
| ContNew x -> "cont.new", [Node ("type " ^ var x, [])]
| ContBind x -> "cont.bind", [Node ("type " ^ var x, [])]
| Suspend x -> "suspend " ^ var x, []
| Resume xys ->
"resume",
Expand Down
1 change: 1 addition & 0 deletions interpreter/text/lexer.mll
Original file line number Diff line number Diff line change
Expand Up @@ -218,6 +218,7 @@ rule token = parse
| "catch_all" { CATCH_ALL }

| "cont.new" { CONT_NEW }
| "cont.bind" { CONT_BIND }
| "suspend" { SUSPEND }
| "resume" { RESUME }
| "resume_throw" { RESUME_THROW }
Expand Down
3 changes: 2 additions & 1 deletion interpreter/text/parser.mly
Original file line number Diff line number Diff line change
Expand Up @@ -217,7 +217,7 @@ let inline_func_type_explicit (c : context) x ft at =
%token UNREACHABLE NOP DROP SELECT
%token BLOCK END IF THEN ELSE LOOP LET
%token THROW TRY DO CATCH CATCH_ALL
%token CONT_NEW SUSPEND RESUME RESUME_THROW BARRIER
%token CONT_NEW CONT_BIND SUSPEND RESUME RESUME_THROW BARRIER
%token BR BR_IF BR_TABLE BR_ON_NULL
%token CALL CALL_REF CALL_INDIRECT
%token RETURN RETURN_CALL RETURN_CALL_REF RETURN_CALL_INDIRECT
Expand Down Expand Up @@ -450,6 +450,7 @@ plain_instr :
| RETURN_CALL var { fun c -> return_call ($2 c func) }
| RETURN_CALL_REF { fun c -> return_call_ref }
| CONT_NEW LPAR TYPE var RPAR { fun c -> cont_new ($4 c type_) }
| CONT_BIND LPAR TYPE var RPAR { fun c -> cont_bind ($4 c type_) }
| SUSPEND var { fun c -> suspend ($2 c event) }
| RESUME_THROW var { fun c -> resume_throw ($2 c event) }
| LOCAL_GET var { fun c -> local_get ($2 c local) }
Expand Down
5 changes: 5 additions & 0 deletions interpreter/util/lib.ml
Original file line number Diff line number Diff line change
Expand Up @@ -87,6 +87,11 @@ struct
| n, y::ys' when n > 0 -> split' (n - 1) (y::xs) ys'
| _ -> failwith "split"

let rec last_opt = function
| x::[] -> Some x
| _::xs -> last_opt xs
| [] -> None

let rec last = function
| x::[] -> x
| _::xs -> last xs
Expand Down
1 change: 1 addition & 0 deletions interpreter/util/lib.mli
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ sig
val drop : int -> 'a list -> 'a list (* raises Failure *)
val split : int -> 'a list -> 'a list * 'a list (* raises Failure *)

val last_opt : 'a list -> 'a option
val last : 'a list -> 'a (* raises Failure *)
val split_last : 'a list -> 'a list * 'a (* raises Failure *)

Expand Down
36 changes: 33 additions & 3 deletions interpreter/valid/valid.ml
Original file line number Diff line number Diff line change
Expand Up @@ -480,6 +480,28 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
[RefType (NonNullable, DefHeapType y)] -->
[RefType (NonNullable, DefHeapType (SynVar x.it))]

| ContBind x ->
(match peek_ref 0 s e.at with
| nul, DefHeapType (SynVar y) ->
let ContType z = cont_type c (y @@ e.at) in
let FuncType (ts1, ts2) = func_type c (as_syn_var z @@ e.at) in
let ContType z' = cont_type c x in
let FuncType (ts1', _) as ft' = func_type c (as_syn_var z' @@ x.at) in
require (List.length ts1 >= List.length ts1') x.at
"type mismatch in continuation arguments";
let ts11, ts12 = Lib.List.split (List.length ts1 - List.length ts1') ts1 in
require (match_func_type c.types [] (FuncType (ts12, ts2)) ft') e.at
"type mismatch in continuation type";
(ts11 @ [RefType (nul, DefHeapType (SynVar y))]) -->
[RefType (NonNullable, DefHeapType (SynVar x.it))]
| (_, BotHeapType) as rt ->
[RefType rt] -->.. [RefType (NonNullable, DefHeapType (SynVar x.it))]
| rt ->
error e.at
("type mismatch: instruction requires continuation reference type" ^
" but stack has " ^ string_of_value_type (RefType rt))
)

| Suspend x ->
let EventType (FuncType (ts1, ts2), res) = event c x in
require (res = Resumable) e.at "suspending with a non-resumable event";
Expand All @@ -493,9 +515,17 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
List.iter (fun (x1, x2) ->
let EventType (FuncType (ts3, ts4), res) = event c x1 in
require (res = Resumable) x1.at "handling a non-resumable event";
(* TODO: check label; problem: we don't have a type idx to produce here
check_stack c (ts3 @ [RefType (NonNullable, DefHeapType (SynVar ?))]) (label c x2) x2.at
*)
match Lib.List.last_opt (label c x2) with
| Some (RefType (NonNullable, DefHeapType (SynVar y'))) ->
let ContType z' = cont_type c (y' @@ x2.at) in
let FuncType (ts1', ts2') = func_type c (as_syn_var z' @@ x2.at) in
check_stack c ts4 ts1' x2.at;
check_stack c ts2 ts2' x2.at;
check_stack c (ts3 @ [RefType (NonNullable, DefHeapType (SynVar y'))]) (label c x2) x2.at
| _ ->
error e.at
("type mismatch: instruction requires continuation reference type" ^
" but label has " ^ string_of_result_type (label c x2))
) xys;
(ts1 @ [RefType (nul, DefHeapType (SynVar y))]) --> ts2
| _, BotHeapType ->
Expand Down
28 changes: 18 additions & 10 deletions test/core/cont.wast
Original file line number Diff line number Diff line change
Expand Up @@ -71,21 +71,21 @@

(elem declare func $r0 $r1)
(func $r0)
(func $r1 (suspend $e1))
(func $r1 (suspend $e1) (suspend $e1))

(func $nl0 (param $k (ref $k1))
(func $nl1 (param $k (ref $k1))
(resume (local.get $k))
(resume (local.get $k))
)
(func $nl1 (param $k (ref $k1))
(func $nl2 (param $k (ref $k1))
(block $h (result (ref $k1))
(resume (event $e1 $h) (local.get $k))
(unreachable)
)
(resume (local.get $k))
(unreachable)
)
(func $nl2 (param $k (ref $k1))
(func $nl3 (param $k (ref $k1))
(block $h1 (result (ref $k1))
(resume (event $e1 $h1) (local.get $k))
(unreachable)
Expand All @@ -99,15 +99,22 @@
(unreachable)
)
)
(func $nl4 (param $k (ref $k1))
(drop (cont.bind (type $k1) (local.get $k)))
(resume (local.get $k))
)

(func (export "non-linear-1")
(call $nl0 (cont.new (type $k1) (ref.func $r0)))
(call $nl1 (cont.new (type $k1) (ref.func $r0)))
)
(func (export "non-linear-2")
(call $nl1 (cont.new (type $k1) (ref.func $r1)))
(call $nl2 (cont.new (type $k1) (ref.func $r1)))
)
(func (export "non-linear-3")
(call $nl1 (cont.new (type $k1) (ref.func $r1)))
(call $nl3 (cont.new (type $k1) (ref.func $r1)))
)
(func (export "non-linear-4")
(call $nl4 (cont.new (type $k1) (ref.func $r1)))
)
)

Expand All @@ -121,9 +128,10 @@

(assert_trap (invoke "barrier") "barrier")

(assert_trap (invoke "non-linear-1") "continuation resumed twice")
(assert_trap (invoke "non-linear-2") "continuation resumed twice")
(assert_trap (invoke "non-linear-3") "continuation resumed twice")
(assert_trap (invoke "non-linear-1") "continuation already consumed")
(assert_trap (invoke "non-linear-2") "continuation already consumed")
(assert_trap (invoke "non-linear-3") "continuation already consumed")
(assert_trap (invoke "non-linear-4") "continuation already consumed")


;; Simple state example
Expand Down

0 comments on commit ee429ef

Please sign in to comment.