[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

Author: takikawa

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)
 

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
 

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 =

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...");

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

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)])]

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 :

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) =