Skip to content
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

Jump to bottom

[interpreter] Add support for validation and evaluation for exceptions #175

Merged
merged 8 commits into from
Sep 15, 2021
Merged

[interpreter] Add support for validation and evaluation for exceptions #175

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
3d534e9
[interpreter] Add support for exception validation
takikawa Jul 5, 2021
acaa7d7
[interpreter] Add evaluation support for exceptions
takikawa Jul 6, 2021
b8d929a
[interpreter] Handle exceptions in the script runner
takikawa Jul 7, 2021
21246b8
[interpreter] Improve core tests
takikawa Jul 7, 2021
33ad602
[interpreter] rename AssertUncaughtException -> AssertException
takikawa Jul 15, 2021
ac67cdd
Commit suggested edit on Rethrowing rule
takikawa Sep 3, 2021
adaf36b
Address review comments
takikawa Sep 3, 2021
7d22147
Add invocation of recent rethrow test
takikawa Sep 15, 2021
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
119 changes: 119 additions & 0 deletions interpreter/exec/eval.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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 =
{
Expand Down Expand Up @@ -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', []

Expand Down Expand Up @@ -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, []

Expand All @@ -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]
takikawa marked this conversation as resolved.
Show resolved Hide resolved

| 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]
Expand All @@ -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]
Comment on lines +578 to +579
Copy link
Member

Choose a reason for hiding this comment

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

Since delegation always targets a label, this rule should be unnecessary.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

This rule seems needed as tests fail without it. I believe the issue is that since the label is outside the catch (when TryCatch is reduced to [Label (... [Catch ...])]), if we drop the Catch and let Delegating go up to the label, the handler that we were supposed to delegate to is gone.

Copy link
Member

Choose a reason for hiding this comment

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

I see. Hm, this is a bit unfortunate. Operationally, we could just switch around the nesting of Label and Catch to handle this naturally, but that would break the hack we use to type catch labels... Fine for now I guess, maybe I can come up with an idea later.

@ioannad, FYI, since @takikawa's observation likely applies to the formal reduction rules as well.


| 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"

Expand Down Expand Up @@ -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)

Expand Down
1 change: 1 addition & 0 deletions interpreter/exec/eval.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion interpreter/script/js.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down
8 changes: 7 additions & 1 deletion interpreter/script/run.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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...");
Expand Down
2 changes: 1 addition & 1 deletion interpreter/script/script.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion interpreter/text/arrange.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)])]
Expand Down
2 changes: 1 addition & 1 deletion interpreter/text/parser.mly
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 :
Expand Down
68 changes: 50 additions & 18 deletions interpreter/valid/valid.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
}

Expand Down Expand Up @@ -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 -->... []
Expand All @@ -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]

Expand Down Expand Up @@ -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
Expand All @@ -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 *)

Expand Down Expand Up @@ -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) =
Expand Down
Loading