diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml index a82dae8fb..2ed751c1d 100644 --- a/interpreter/binary/decode.ml +++ b/interpreter/binary/decode.ml @@ -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; diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml index f9dec6ff0..f2df56e43 100644 --- a/interpreter/binary/encode.ml +++ b/interpreter/binary/encode.ml @@ -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 diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index 423db9951..cc4fbecd4 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -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 -> @@ -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 @@ -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 @@ -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 diff --git a/interpreter/syntax/ast.ml b/interpreter/syntax/ast.ml index 00ff25b51..cd7b805a9 100644 --- a/interpreter/syntax/ast.ml +++ b/interpreter/syntax/ast.ml @@ -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 *) diff --git a/interpreter/syntax/free.ml b/interpreter/syntax/free.ml index 9d9f82478..467902d57 100644 --- a/interpreter/syntax/free.ml +++ b/interpreter/syntax/free.ml @@ -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) diff --git a/interpreter/syntax/operators.ml b/interpreter/syntax/operators.ml index 0710bda96..d996c2b77 100644 --- a/interpreter/syntax/operators.ml +++ b/interpreter/syntax/operators.ml @@ -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 diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml index 57fb4aa42..dc9794bdb 100644 --- a/interpreter/syntax/types.ml +++ b/interpreter/syntax/types.ml @@ -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 diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml index fceb82f60..1268f0b1c 100644 --- a/interpreter/text/arrange.ml +++ b/interpreter/text/arrange.ml @@ -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", diff --git a/interpreter/text/lexer.mll b/interpreter/text/lexer.mll index 4949cdbf0..dd508a8f2 100644 --- a/interpreter/text/lexer.mll +++ b/interpreter/text/lexer.mll @@ -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 } diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index b6834d82b..938dbd0da 100644 --- a/interpreter/text/parser.mly +++ b/interpreter/text/parser.mly @@ -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 @@ -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) } diff --git a/interpreter/util/lib.ml b/interpreter/util/lib.ml index 23bace335..5446c3fd2 100644 --- a/interpreter/util/lib.ml +++ b/interpreter/util/lib.ml @@ -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 diff --git a/interpreter/util/lib.mli b/interpreter/util/lib.mli index bde64f1da..c6acfa94d 100644 --- a/interpreter/util/lib.mli +++ b/interpreter/util/lib.mli @@ -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 *) diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index 4234e653b..a934daf74 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -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"; @@ -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 -> diff --git a/test/core/cont.wast b/test/core/cont.wast index 6b3c1277e..0fb990108 100644 --- a/test/core/cont.wast +++ b/test/core/cont.wast @@ -71,13 +71,13 @@ (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) @@ -85,7 +85,7 @@ (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) @@ -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))) ) ) @@ -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