Support assert_throw

spectec/spec/wasm-3.0/8-reduction.watsup

@@ -184,6 +184,9 @@ rule Step_read/return_call:
 rule Step_read/return_call_ref-label:
   z; (LABEL_ k `{instr'*} val* (RETURN_CALL_REF yy) instr*)  ~>  val* (RETURN_CALL_REF yy)
 
+rule Step_read/return_call_ref-handler:
+  z; (HANDLER_ k `{catch*} val* (RETURN_CALL_REF yy) instr*)  ~>  val* (RETURN_CALL_REF yy)
+
 rule Step_read/return_call_ref-frame-null:
   z; (FRAME_ k `{f} val* (REF.NULL ht) (RETURN_CALL_REF yy) instr*)  ~>  TRAP
 

spectec/src/al/al_util.ml

@@ -191,6 +191,10 @@ let unwrap_listv: value -> value growable_array = function
 let unwrap_listv_to_array (v: value): value array = !(unwrap_listv v)
 let unwrap_listv_to_list (v: value): value list = unwrap_listv_to_array v |> Array.to_list
 
+let unwrap_seq_to_array: value -> value array = function
+  | OptV opt -> opt |> Option.to_list |> Array.of_list
+  | v -> unwrap_listv_to_array v
+
 let unwrap_textv: value -> string = function
   | TextV str -> str
   | v -> fail_value "unwrap_textv" v

spectec/src/backend-interpreter/exception.ml

@@ -1,4 +1,5 @@
 exception Trap
+exception Throw
 exception OutOfMemory
 exception Timeout
 exception MissingReturnValue of string

spectec/src/backend-interpreter/interpreter.ml

@@ -248,8 +248,8 @@ and eval_expr env expr =
     (* TODO: interpret CompE *)
     raise (Exception.MissingReturnValue "CompE") *)
   | CatE (e1, e2) ->
-    let a1 = eval_expr env e1 |> unwrap_listv_to_array in
-    let a2 = eval_expr env e2 |> unwrap_listv_to_array in
+    let a1 = eval_expr env e1 |> unwrap_seq_to_array in
+    let a2 = eval_expr env e2 |> unwrap_seq_to_array in
     Array.append a1 a2 |> listV
   | LenE e ->
     eval_expr env e |> unwrap_listv_to_array |> Array.length |> Z.of_int |> numV
@@ -609,6 +609,7 @@ and step_instr (fname: string) (ctx: AlContext.t) (env: value Env.t) (instr: ins
     call_func f args |> ignore;
     ctx
   | TrapI -> raise Exception.Trap
+  | ThrowI _ -> raise Exception.Throw
   | NopI -> ctx
   | ReturnI None -> AlContext.tl ctx
   | ReturnI (Some e) ->

spectec/src/backend-interpreter/runner.ml

@@ -9,6 +9,7 @@ open Ds
 
 (* Errors *)
 
+module Assert = Reference_interpreter.Error.Make ()
 let error_interpret at msg = Error.error at "interpreter" msg
 
 (* Logging *)
@@ -170,6 +171,11 @@ let test_assertion assertion =
       fail
     with Exception.Trap -> success
   )
+  | AssertException action -> (
+    match run_action action with
+    | exception Exception.Throw -> success
+    | _ -> Assert.error assertion.at "expected exception"
+  )
   (* ignore other kinds of assertions *)
   | _ -> pass
 

spectec/src/il2al/manual.ml

@@ -36,14 +36,15 @@ let manual_algos = [eval_expr]
 
 let return_instrs_of_instantiate config =
   let store, frame, rhs = config in
+  let vals, instrs = rhs in
   let ty = listT admininstrT in
   let ty' = varT "moduleinst" [] in
   let ty'' = Il.Ast.TupT (List.map (fun t -> no_name, t) [store.note; ty']) $ no_region in
   [
     enterI (
       frameE (Some (numE Z.zero ~note:natT), frame) ~note:callframeT,
-      listE ([ caseE ([[atom_of_name "FRAME_" "admininstr"]], []) ~note:admininstrT]) ~note:ty,
-      rhs
+      catE (instrs, (listE [caseE ([[atom_of_name "FRAME_" "admininstr"]], []) ~note:admininstrT] ~note:ty)) ~note:ty,
+      vals
     );
     returnI (Some (tupE [
       store;
@@ -52,6 +53,7 @@ let return_instrs_of_instantiate config =
   ]
 let return_instrs_of_invoke config =
   let _, frame, rhs = config in
+  let vals, instrs = rhs in
   let arity = varE "k" ~note:natT in
   let value = varE "val" ~note:valT in
   let ty = listT admininstrT in
@@ -64,8 +66,8 @@ let return_instrs_of_invoke config =
     letI (arity,  len_expr);
     enterI (
       frameE (Some (arity), frame) ~note:callframeT,
-      listE ([caseE ([[atom_of_name "FRAME_" "admininstr"]], []) ~note:admininstrT]) ~note:ty,
-      rhs
+      catE (instrs, listE [caseE ([[atom_of_name "FRAME_" "admininstr"]], []) ~note:admininstrT] ~note:ty) ~note:ty,
+      vals
     );
     popI (iterE (value, ["val"], ListN (arity, None)) ~note:ty');
     returnI (Some (iterE (value, ["val"], ListN (arity, None)) ~note:ty'))

spectec/src/il2al/translate.ml

@@ -150,6 +150,54 @@ let lhs_of_prem pr =
   | Il.LetPr (lhs, _, _) -> lhs
   | _ -> Error.error pr.at "prose translation" "expected a LetPr"
 
+let rec is_wasm_value e =
+  (* TODO: use hint? *)
+  match e.it with
+  | Il.SubE (e, _, _) -> is_wasm_value e
+  | Il.CaseE ([{it = Atom id; _}]::_, _) when
+    List.mem id [
+      "CONST";
+      "VCONST";
+      "REF.I31_NUM";
+      "REF.STRUCT_ADDR";
+      "REF.ARRAY_ADDR";
+      "REF.EXN_ADDR";
+      "REF.FUNC_ADDR";
+      "REF.HOST_ADDR";
+      "REF.EXTERN";
+      "REF.NULL"
+    ] -> true
+  | Il.CallE (id, _) when id.it = "const" -> true
+  | _ -> Valid.sub_typ e.note valT
+let is_wasm_instr e =
+  (* TODO: use hint? *)
+  Valid.sub_typ e.note instrT || Valid.sub_typ e.note admininstrT
+
+let split_vals (exp: Il.exp): Il.exp list * Il.exp list =
+  (* ASSUMPTION: exp is of the form v* i* *)
+  let rec spread_cat e =
+    match e.it with
+    | Il.CatE (e1, e2) -> spread_cat e1 @ spread_cat e2
+    | Il.ListE es -> List.map (fun e' -> {e' with it = Il.ListE [e']; note = e.note}) es
+    | _ -> [e]
+  in
+  let is_wasm_values e =
+    match e.it with
+    | Il.IterE (e, _) -> is_wasm_value e
+    | Il.ListE es -> List.for_all is_wasm_value es
+    | _ -> false
+  in
+
+  spread_cat exp
+  |> List.partition is_wasm_values
+
+let concat_exprs es =
+  match es with
+  | [] -> assert false
+  | hd :: tl -> List.fold_left (fun e1 e2 ->
+    catE (e1, e2) ~at:(over_region [e1.at; e2.at]) ~note:hd.note
+  ) hd tl
+
 (** Translation *)
 
 (* `Il.iter` -> `iter` *)
@@ -431,27 +479,9 @@ let rec translate_rhs exp =
     let instrs = translate_rhs inner_exp in
     List.map (walker.walk_instr walker) instrs
   (* Value *)
-  | _ when Valid.sub_typ exp.note valT -> [ pushI (translate_exp exp) ]
-  | Il.CaseE ([{it = Atom id; _}]::_, _) when List.mem id [
-      (* TODO: Consider automating this *)
-      "CONST";
-      "VCONST";
-      "REF.I31_NUM";
-      "REF.STRUCT_ADDR";
-      "REF.ARRAY_ADDR";
-      "REF.EXN_ADDR";
-      "REF.FUNC_ADDR";
-      "REF.HOST_ADDR";
-      "REF.EXTERN";
-      "REF.NULL"
-  ] -> [ pushI { (translate_exp exp) with note=valT } ~at:at ]
-  (* TODO: use hint *)
-  | Il.CallE (id, _) when id.it = "const" ->
-    [ pushI { (translate_exp exp) with note=valT } ~at:at ]
+  | _ when is_wasm_value exp -> [ pushI {(translate_exp exp) with note = valT} ]
   (* Instr *)
-  (* TODO: use hint *)
-  | _ when Valid.sub_typ exp.note instrT || Valid.sub_typ exp.note admininstrT ->
-    [ executeI (translate_exp exp) ]
+  | _ when is_wasm_instr exp -> [ executeI (translate_exp exp) ]
   | _ -> error_exp exp "expression on rhs of reduction"
 
 and translate_context_rhs exp =
@@ -989,13 +1019,21 @@ and translate_prem prem =
 let translate_prems =
   List.fold_right (fun prem il -> translate_prem prem |> insert_instrs il)
 
-(* s; f; e -> `expr * expr * instr list` *)
+(* s; f; e -> `expr * expr * instr list * expr list` *)
 let get_config_return_instrs name exp at =
   assert(is_config exp);
   let state, rhs = split_config exp in
   let store, f = split_state state in
-
-  let config = translate_exp store, translate_exp f, translate_rhs rhs in
+  let vals, instrs = split_vals rhs in
+
+  let config =
+    translate_exp store,
+    translate_exp f,
+    (
+      List.concat_map translate_rhs vals,
+      List.map translate_exp instrs |> concat_exprs
+    )
+  in
   (* HARDCODE: hardcoding required for config returning helper functions *)
   match name with
   | "instantiate" -> Manual.return_instrs_of_instantiate config
@@ -1215,6 +1253,7 @@ let rec translate_rgroup' instr_name rgroup =
         | _ -> assert false
       ) pops in
       let u_group = Il2il.unify_ctxt popped_vars subgroup in
+      let pops, u_group = extract_pops u_group in
       let ctxt = extract_context (List.hd u_group) |> Option.get in
       let atom = case_of_case ctxt |> List.hd |> List.hd in
       let cond = ContextKindE atom $$ atom.at % boolT in
@@ -1224,7 +1263,8 @@ let rec translate_rgroup' instr_name rgroup =
         List.map (translate_reduction ~context_opt:(Some middle_instr)) u_group
         (* TODO: Consider inserting otherwise to normal case also *)
         |> List.mapi (fun i instrs -> if i = 0 || is_otherwise instrs then instrs else [otherwiseI instrs])
-        |> Transpile.merge_blocks in
+        |> Transpile.merge_blocks
+        |> translate_prems pops in
       k, [
         ifI (
           cond,