From ea7f2c06a6be9ae60e51677429ce4a009e7a99c0 Mon Sep 17 00:00:00 2001 From: Asumu Takikawa Date: Wed, 15 Sep 2021 13:12:02 -0700 Subject: [PATCH] [interpreter] Add support for validation and evaluation for exceptions (#175) * Add support for exception validation * Add evaluation support for exceptions * Handle exceptions in the script runner * Improve core tests * Rename AssertUncaughtException -> AssertException --- interpreter/exec/eval.ml | 119 +++++++++++++++++++++++++++++++++++ interpreter/exec/eval.mli | 1 + interpreter/script/js.ml | 2 +- interpreter/script/run.ml | 8 ++- interpreter/script/script.ml | 2 +- interpreter/text/arrange.ml | 2 +- interpreter/text/parser.mly | 2 +- interpreter/valid/valid.ml | 68 ++++++++++++++------ test/core/rethrow.wast | 13 ++++ test/core/throw.wast | 6 ++ test/core/try_catch.wast | 40 +++++++++++- test/core/try_delegate.wast | 25 ++++++++ 12 files changed, 263 insertions(+), 25 deletions(-) diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index f12d933bb0..60268afbe9 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -9,11 +9,13 @@ open Source module Link = Error.Make () module Trap = Error.Make () +module Exception = Error.Make () module Crash = Error.Make () module Exhaustion = Error.Make () exception Link = Link.Error exception Trap = Trap.Error +exception Exception = Exception.Error exception Crash = Crash.Error (* failure that cannot happen in valid code *) exception Exhaustion = Exhaustion.Error @@ -62,8 +64,14 @@ and admin_instr' = | Trapping of string | Returning of value stack | Breaking of int32 * value stack + | Throwing of Tag.t * value stack + | Rethrowing of int32 * (admin_instr -> admin_instr) | Label of int32 * instr list * code | Frame of int32 * frame * code + | Catch of int32 * (Tag.t * instr list) list * instr list option * code + | Caught of int32 * Tag.t * value stack * code + | Delegate of int32 * code + | Delegating of int32 * Tag.t * value stack type config = { @@ -205,6 +213,32 @@ let rec step (c : config) : config = else vs, [Invoke func @@ e.at] + | Throw x, vs -> + let t = tag frame.inst x in + let FuncType (ts, _) = Tag.type_of t in + let n = Lib.List32.length ts in + let args, vs' = take n vs e.at, drop n vs e.at in + vs', [Throwing (t, args) @@ e.at] + + | Rethrow x, vs -> + vs, [Rethrowing (x.it, fun e -> e) @@ e.at] + + | TryCatch (bt, es', cts, ca), vs -> + let FuncType (ts1, ts2) = block_type frame.inst bt in + let n1 = Lib.List32.length ts1 in + let n2 = Lib.List32.length ts2 in + let args, vs' = take n1 vs e.at, drop n1 vs e.at in + let cts' = List.map (fun (x, es'') -> ((tag frame.inst x), es'')) cts in + vs', [Label (n2, [], ([], [Catch (n2, cts', ca, (args, List.map plain es')) @@ e.at])) @@ e.at] + + | TryDelegate (bt, es', x), vs -> + let FuncType (ts1, ts2) = block_type frame.inst bt in + let n1 = Lib.List32.length ts1 in + let n2 = Lib.List32.length ts2 in + let args, vs' = take n1 vs e.at, drop n1 vs e.at in + let k = Int32.succ x.it in + vs', [Label (n2, [], ([], [Delegate (k, (args, List.map plain es')) @@ e.at])) @@ e.at] + | Drop, v :: vs' -> vs', [] @@ -482,6 +516,15 @@ let rec step (c : config) : config = | Breaking (k, vs'), vs -> Crash.error e.at "undefined label" + | Throwing _, _ -> + assert false + + | Rethrowing _, _ -> + Crash.error e.at "undefined catch label" + + | Delegating _, _ -> + Crash.error e.at "undefined delegate label" + | Label (n, es0, (vs', [])), vs -> vs' @ vs, [] @@ -497,6 +540,18 @@ let rec step (c : config) : config = | Label (n, es0, (vs', {it = Breaking (k, vs0); at} :: es')), vs -> vs, [Breaking (Int32.sub k 1l, vs0) @@ at] + | Label (n, es0, (vs', {it = Throwing (a, vs0); at} :: es')), vs -> + vs, [Throwing (a, vs0) @@ at] + + | Label (n, es0, (vs', {it = Delegating (0l, a, vs0); at} :: es')), vs -> + vs, [Throwing (a, vs0) @@ at] + + | Label (n, es0, (vs', {it = Delegating (k, a, vs0); at} :: es')), vs -> + vs, [Delegating (Int32.sub k 1l, a, vs0) @@ at] + + | Label (n, es0, (vs', {it = Rethrowing (k, cont); at} :: es')), vs -> + vs, [Rethrowing (Int32.sub k 1l, (fun e -> Label (n, es0, (vs', cont e :: es')) @@ e.at)) @@ at] + | Label (n, es0, code'), vs -> let c' = step {c with code = code'} in vs, [Label (n, es0, c'.code) @@ e.at] @@ -510,10 +565,70 @@ let rec step (c : config) : config = | Frame (n, frame', (vs', {it = Returning vs0; at} :: es')), vs -> take n vs0 e.at @ vs, [] + | Frame (n, frame', (vs', {it = Throwing (a, vs0); at} :: es')), vs -> + vs, [Throwing (a, vs0) @@ at] + | Frame (n, frame', code'), vs -> let c' = step {frame = frame'; code = code'; budget = c.budget - 1} in vs, [Frame (n, c'.frame, c'.code) @@ e.at] + | Catch (n, cts, ca, (vs', [])), vs -> + vs' @ vs, [] + + | Catch (n, cts, ca, (vs', {it = Delegating (0l, a, vs0); at} :: es')), vs -> + vs, [Catch (n, cts, ca, (vs', (Throwing (a, vs0) @@ at) :: es')) @@ e.at] + + | Catch (n, cts, ca, (vs', ({it = Trapping _ | Breaking _ | Returning _ | Delegating _; at} as e) :: es')), vs -> + vs, [e] + + | Catch (n, cts, ca, (vs', {it = Rethrowing (k, cont); at} :: es')), vs -> + vs, [Rethrowing (k, (fun e -> Catch (n, cts, ca, (vs', (cont e) :: es')) @@ e.at)) @@ at] + + | Catch (n, (a', es'') :: cts, ca, (vs', {it = Throwing (a, vs0); at} :: es')), vs -> + if a == a' then + vs, [Caught (n, a, vs0, (vs0, List.map plain es'')) @@ at] + else + vs, [Catch (n, cts, ca, (vs', {it = Throwing (a, vs0); at} :: es')) @@ e.at] + + | Catch (n, [], Some es'', (vs', {it = Throwing (a, vs0); at} :: es')), vs -> + vs, [Caught (n, a, vs0, (vs0, List.map plain es'')) @@ at] + + | Catch (n, [], None, (vs', {it = Throwing (a, vs0); at} :: es')), vs -> + vs, [Throwing (a, vs0) @@ at] + + | Catch (n, cts, ca, code'), vs -> + let c' = step {c with code = code'} in + vs, [Catch (n, cts, ca, c'.code) @@ e.at] + + | Caught (n, a, vs0, (vs', [])), vs -> + vs' @ vs, [] + + | Caught (n, a, vs0, (vs', ({it = Trapping _ | Breaking _ | Returning _ | Throwing _ | Delegating _; at} as e) :: es')), vs -> + vs, [e] + + | Caught (n, a, vs0, (vs', {it = Rethrowing (0l, cont); at} :: es')), vs -> + vs, [Caught (n, a, vs0, (vs', (cont (Throwing (a, vs0) @@ at)) :: es')) @@ e.at] + + | Caught (n, a, vs0, (vs', {it = Rethrowing (k, cont); at} :: es')), vs -> + vs, [Rethrowing (k, (fun e -> Caught (n, a, vs0, (vs', (cont e) :: es')) @@ e.at)) @@ at] + + | Caught (n, a, vs0, code'), vs -> + let c' = step {c with code = code'} in + vs, [Caught (n, a, vs0, c'.code) @@ e.at] + + | Delegate (l, (vs', [])), vs -> + vs' @ vs, [] + + | Delegate (l, (vs', ({it = Trapping _ | Breaking _ | Returning _ | Rethrowing _ | Delegating _; at} as e) :: es')), vs -> + vs, [e] + + | Delegate (l, (vs', {it = Throwing (a, vs0); at} :: es')), vs -> + vs, [Delegating (l, a, vs0) @@ e.at] + + | Delegate (l, code'), vs -> + let c' = step {c with code = code'} in + vs, [Delegate (l, c'.code) @@ e.at] + | Invoke func, vs when c.budget = 0 -> Exhaustion.error e.at "call stack exhausted" @@ -543,6 +658,10 @@ let rec eval (c : config) : value stack = | vs, {it = Trapping msg; at} :: _ -> Trap.error at msg + | vs, {it = Throwing (a, args); at} :: _ -> + let msg = "uncaught exception with args (" ^ string_of_values args ^ ")" in + Exception.error at msg + | vs, es -> eval (step c) diff --git a/interpreter/exec/eval.mli b/interpreter/exec/eval.mli index 825cc74f09..be074a232c 100644 --- a/interpreter/exec/eval.mli +++ b/interpreter/exec/eval.mli @@ -3,6 +3,7 @@ open Instance exception Link of Source.region * string exception Trap of Source.region * string +exception Exception of Source.region * string exception Crash of Source.region * string exception Exhaustion of Source.region * string diff --git a/interpreter/script/js.ml b/interpreter/script/js.ml index 434cfbfb80..b955fb9a8b 100644 --- a/interpreter/script/js.ml +++ b/interpreter/script/js.ml @@ -513,7 +513,7 @@ let of_assertion mods ass = of_assertion' mods act "assert_trap" [] None | AssertExhaustion (act, _) -> of_assertion' mods act "assert_exhaustion" [] None - | AssertUncaughtException act -> + | AssertException act -> of_assertion' mods act "assert_exception" [] None let of_command mods cmd = diff --git a/interpreter/script/run.ml b/interpreter/script/run.ml index 54c8a7b5ef..2337bb837e 100644 --- a/interpreter/script/run.ml +++ b/interpreter/script/run.ml @@ -112,6 +112,7 @@ let input_from get_script run = | Eval.Trap (at, msg) -> error at "runtime trap" msg | Eval.Exhaustion (at, msg) -> error at "resource exhaustion" msg | Eval.Crash (at, msg) -> error at "runtime crash" msg + | Eval.Exception (at, msg) -> error at "uncaught exception" msg | Encode.Code (at, msg) -> error at "encoding error" msg | Script.Error (at, msg) -> error at "script error" msg | IO (at, msg) -> error at "i/o error" msg @@ -458,7 +459,12 @@ let run_assertion ass = | _ -> Assert.error ass.at "expected runtime error" ) - | AssertUncaughtException act -> () (* TODO *) + | AssertException act -> + trace ("Asserting exception..."); + (match run_action act with + | exception Eval.Exception (_, msg) -> () + | _ -> Assert.error ass.at "expected exception" + ) | AssertExhaustion (act, re) -> trace ("Asserting exhaustion..."); diff --git a/interpreter/script/script.ml b/interpreter/script/script.ml index 282cfc612b..8ee3aeb178 100644 --- a/interpreter/script/script.ml +++ b/interpreter/script/script.ml @@ -32,7 +32,7 @@ and assertion' = | AssertUninstantiable of definition * string | AssertReturn of action * result list | AssertTrap of action * string - | AssertUncaughtException of action + | AssertException of action | AssertExhaustion of action * string type command = command' Source.phrase diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml index 94cbe27096..0ceb981a37 100644 --- a/interpreter/text/arrange.ml +++ b/interpreter/text/arrange.ml @@ -550,7 +550,7 @@ let assertion mode ass = [Node ("assert_return", action mode act :: List.map (result mode) results)] | AssertTrap (act, re) -> [Node ("assert_trap", [action mode act; Atom (string re)])] - | AssertUncaughtException act -> + | AssertException act -> [Node ("assert_exception", [action mode act])] | AssertExhaustion (act, re) -> [Node ("assert_exhaustion", [action mode act; Atom (string re)])] diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index b4af96da76..39c599cfa6 100644 --- a/interpreter/text/parser.mly +++ b/interpreter/text/parser.mly @@ -1169,7 +1169,7 @@ assertion : | LPAR ASSERT_RETURN action result_list RPAR { AssertReturn ($3, $4) @@ at () } | LPAR ASSERT_TRAP action STRING RPAR { AssertTrap ($3, $4) @@ at () } | LPAR ASSERT_EXCEPTION action RPAR - { AssertUncaughtException $3 @@ at () } + { AssertException $3 @@ at () } | LPAR ASSERT_EXHAUSTION action STRING RPAR { AssertExhaustion ($3, $4) @@ at () } cmd : diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index 776511f478..6ab7f0f0e5 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -14,6 +14,8 @@ let require b at s = if not b then error at s (* Context *) +type label_kind = BlockLabel | CatchLabel + type context = { types : func_type list; @@ -26,7 +28,7 @@ type context = datas : unit list; locals : value_type list; results : value_type list; - labels : stack_type list; + labels : (label_kind * stack_type) list; refs : Free.t; } @@ -229,32 +231,35 @@ let rec check_instr (c : context) (e : instr) (s : infer_stack_type) : op_type = | Block (bt, es) -> let FuncType (ts1, ts2) as ft = check_block_type c bt in - check_block {c with labels = ts2 :: c.labels} es ft e.at; + check_block {c with labels = (BlockLabel, ts2) :: c.labels} es ft e.at; ts1 --> ts2 | Loop (bt, es) -> let FuncType (ts1, ts2) as ft = check_block_type c bt in - check_block {c with labels = ts1 :: c.labels} es ft e.at; + check_block {c with labels = (BlockLabel, ts1) :: c.labels} es ft e.at; ts1 --> ts2 | If (bt, es1, es2) -> let FuncType (ts1, ts2) as ft = check_block_type c bt in - check_block {c with labels = ts2 :: c.labels} es1 ft e.at; - check_block {c with labels = ts2 :: c.labels} es2 ft e.at; + check_block {c with labels = (BlockLabel, ts2) :: c.labels} es1 ft e.at; + check_block {c with labels = (BlockLabel, ts2) :: c.labels} es2 ft e.at; (ts1 @ [NumType I32Type]) --> ts2 | Br x -> - label c x -->... [] + let (_, ts) = label c x in + ts -->... [] | BrIf x -> - (label c x @ [NumType I32Type]) --> label c x + let (_, ts) = label c x in + (ts @ [NumType I32Type]) --> ts | BrTable (xs, x) -> - let n = List.length (label c x) in - let ts = Lib.List.table n (fun i -> peek (n - i) s) in - check_stack ts (known (label c x)) x.at; - List.iter (fun x' -> check_stack ts (known (label c x')) x'.at) xs; - (ts @ [Some (NumType I32Type)]) -~>... [] + let (_, ts) = label c x in + let n = List.length ts in + let ts' = Lib.List.table n (fun i -> peek (n - i) s) in + check_stack ts' (known ts) x.at; + List.iter (fun x' -> check_stack ts' (known (snd (label c x'))) x'.at) xs; + (ts' @ [Some (NumType I32Type)]) -~>... [] | Return -> c.results -->... [] @@ -271,6 +276,31 @@ let rec check_instr (c : context) (e : instr) (s : infer_stack_type) : op_type = " but table has " ^ string_of_ref_type t); (ts1 @ [NumType I32Type]) --> ts2 + | Throw x -> + let TagType y = tag c x in + let FuncType (ts1, _) = type_ c (y @@ e.at) in + ts1 -->... [] + + | Rethrow x -> + let (kind, _) = label c x in + require (kind = CatchLabel) e.at "invalid rethrow label"; + [] -->... [] + + | TryCatch (bt, es, cts, ca) -> + let FuncType (ts1, ts2) as ft = check_block_type c bt in + let c_try = {c with labels = (BlockLabel, ts2) :: c.labels} in + let c_catch = {c with labels = (CatchLabel, ts2) :: c.labels} in + check_block c_try es ft e.at; + List.iter (fun ct -> check_catch ct c_catch ft e.at) cts; + Lib.Option.app (fun es -> check_block c_catch es ft e.at) ca; + ts1 --> ts2 + + | TryDelegate (bt, es, x) -> + let FuncType (ts1, ts2) as ft = check_block_type c bt in + ignore (label c x); + check_block {c with labels = (BlockLabel, ts2) :: c.labels} es ft e.at; + ts1 --> ts2 + | LocalGet x -> [] --> [local c x] @@ -402,11 +432,6 @@ let rec check_instr (c : context) (e : instr) (s : infer_stack_type) : op_type = let t1, t2 = type_cvtop e.at cvtop in [NumType t1] --> [NumType t2] - | TryCatch _ -> [] --> [] (* TODO *) - | TryDelegate _ -> [] --> [] (* TODO *) - | Throw _ -> [] --> [] (* TODO *) - | Rethrow _ -> [] --> [] (* TODO *) - and check_seq (c : context) (s : infer_stack_type) (es : instr list) : infer_stack_type = match es with @@ -427,6 +452,13 @@ and check_block (c : context) (es : instr list) (ft : func_type) at = ("type mismatch: block requires " ^ string_of_stack_type ts2 ^ " but stack has " ^ string_of_infer_types (snd s)) +and check_catch (ct : var * instr list) (c : context) (ft : func_type) at = + let (x, es) = ct in + let TagType y = tag c x in + let FuncType (ts1, _) = type_ c (y @@ at) in + let FuncType (_, ts2) = ft in + check_block c es (FuncType (ts1, ts2)) at + (* Types *) @@ -491,7 +523,7 @@ let check_type (t : type_) = let check_func (c : context) (f : func) = let {ftype; locals; body} = f.it in let FuncType (ts1, ts2) = type_ c ftype in - let c' = {c with locals = ts1 @ locals; results = ts2; labels = [ts2]} in + let c' = {c with locals = ts1 @ locals; results = ts2; labels = [(BlockLabel, ts2)]} in check_block c' body (FuncType ([], ts2)) f.at let check_tag (c : context) (t : tag) = diff --git a/test/core/rethrow.wast b/test/core/rethrow.wast index 7f836987bb..e41d94b2bb 100644 --- a/test/core/rethrow.wast +++ b/test/core/rethrow.wast @@ -63,6 +63,13 @@ ) ) ) + + (func (export "rethrow-stack-polymorphism") + (try + (do (throw $e0)) + (catch $e0 (i32.const 1) (rethrow 0)) + ) + ) ) (assert_exception (invoke "catch-rethrow-0")) @@ -81,3 +88,9 @@ (assert_return (invoke "rethrow-recatch" (i32.const 0)) (i32.const 23)) (assert_return (invoke "rethrow-recatch" (i32.const 1)) (i32.const 42)) +(assert_exception (invoke "rethrow-stack-polymorphism")) + +(assert_invalid (module (func (rethrow 0))) "invalid rethrow label") +(assert_invalid (module (func (block (rethrow 0)))) "invalid rethrow label") +(assert_invalid (module (func (try (do (rethrow 0)) (delegate 0)))) + "invalid rethrow label") diff --git a/test/core/throw.wast b/test/core/throw.wast index 7d635753da..d53b5b5500 100644 --- a/test/core/throw.wast +++ b/test/core/throw.wast @@ -43,3 +43,9 @@ (assert_exception (invoke "throw-param-f64" (f64.const 5.0))) (assert_return (invoke "test-throw-1-2")) + +(assert_invalid (module (func (throw 0))) "unknown tag 0") +(assert_invalid (module (tag (param i32)) (func (throw 0))) + "type mismatch: instruction requires [i32] but stack has []") +(assert_invalid (module (tag (param i32)) (func (i64.const 5) (throw 0))) + "type mismatch: instruction requires [i32] but stack has [i64]") diff --git a/test/core/try_catch.wast b/test/core/try_catch.wast index 4609c374ad..6564e201b9 100644 --- a/test/core/try_catch.wast +++ b/test/core/try_catch.wast @@ -154,10 +154,10 @@ (assert_return (invoke "simple-throw-catch" (i32.const 0)) (i32.const 23)) (assert_return (invoke "simple-throw-catch" (i32.const 1)) (i32.const 42)) -(assert_exception (invoke "unreachable-not-caught")) +(assert_trap (invoke "unreachable-not-caught") "unreachable") (assert_return (invoke "trap-in-callee" (i32.const 7) (i32.const 2)) (i32.const 3)) -(assert_exception (invoke "trap-in-callee" (i32.const 1) (i32.const 0))) +(assert_trap (invoke "trap-in-callee" (i32.const 1) (i32.const 0)) "integer divide by zero") (assert_return (invoke "catch-complex-1" (i32.const 0)) (i32.const 3)) (assert_return (invoke "catch-complex-1" (i32.const 1)) (i32.const 4)) @@ -188,6 +188,28 @@ (assert_return (invoke "catchless-try" (i32.const 0)) (i32.const 0)) (assert_return (invoke "catchless-try" (i32.const 1)) (i32.const 1)) +(module + (func $imported-throw (import "test" "throw")) + (tag $e0) + + (func (export "imported-mismatch") (result i32) + (try (result i32) + (do + (try (result i32) + (do + (i32.const 1) + (call $imported-throw) + ) + (catch $e0 (i32.const 2)) + ) + ) + (catch_all (i32.const 3)) + ) + ) +) + +(assert_return (invoke "imported-mismatch") (i32.const 3)) + (assert_malformed (module quote "(module (func (catch_all)))") "unexpected token" @@ -204,3 +226,17 @@ ) "unexpected token" ) + +(assert_invalid (module (func (result i32) (try (result i32) (do)))) + "type mismatch: instruction requires [i32] but stack has []") +(assert_invalid (module (func (result i32) (try (result i32) (do (i64.const 42))))) + "type mismatch: instruction requires [i32] but stack has [i64]") +(assert_invalid (module (tag) (func (try (do) (catch 0 (i32.const 42))))) + "type mismatch: block requires [] but stack has [i32]") +(assert_invalid (module + (tag (param i64)) + (func (result i32) + (try (result i32) (do (i32.const 42)) (catch 0)))) + "type mismatch: instruction requires [i32] but stack has [i64]") +(assert_invalid (module (func (try (do) (catch_all (i32.const 42))))) + "type mismatch: block requires [] but stack has [i32]") diff --git a/test/core/try_delegate.wast b/test/core/try_delegate.wast index d51eefbaa7..bbc5c0a0bb 100644 --- a/test/core/try_delegate.wast +++ b/test/core/try_delegate.wast @@ -45,6 +45,23 @@ ) ) + (func (export "delegate-to-block") (result i32) + (try (result i32) + (do (block (try (do (throw $e0)) (delegate 0))) + (i32.const 0)) + (catch_all (i32.const 1))) + ) + + (func (export "delegate-to-catch") (result i32) + (try (result i32) + (do (try + (do (throw $e0)) + (catch $e0 + (try (do (rethrow 1)) (delegate 0)))) + (i32.const 0)) + (catch_all (i32.const 1))) + ) + (func (export "delegate-to-caller") (try (do (try (do (throw $e0)) (delegate 1))) (catch_all)) ) @@ -92,6 +109,9 @@ (assert_return (invoke "delegate-skip") (i32.const 3)) +(assert_return (invoke "delegate-to-block") (i32.const 1)) +(assert_return (invoke "delegate-to-catch") (i32.const 1)) + (assert_exception (invoke "delegate-to-caller")) (assert_malformed @@ -113,3 +133,8 @@ (module quote "(module (func (try (do) (delegate) (delegate 0))))") "unexpected token" ) + +(assert_invalid + (module (func (try (do) (delegate 1)))) + "unknown label" +)