Handle missing operand in the stack

spectec/src/il2al/il2il.ml

@@ -164,6 +164,9 @@ let rec overlap e1 e2 = if eq_exp e1 e2 then e1 else
       CaseE (mixop1, overlap e1 e2) |> replace_it
     | SubE (e1, typ1, typ1'), SubE (e2, typ2, typ2') when eq_typ typ1 typ2 && eq_typ typ1' typ2' ->
       SubE (overlap e1 e2, typ1, typ1') |> replace_it
+    (* HARDCODE: Unifying CatE with non-CatE *)
+    | CatE ({ it = IterE (_, (ListN _, _)); _ } as e1', _), _ -> overlap e1 { e2 with it = CatE (e1', e2) }
+    | _, CatE ({ it = IterE (_, (ListN _, _)); _ } as e2', _) -> overlap { e1 with it = CatE (e2', e1) } e2
     | _ ->
       let ty = overlap_typ e1.note e2.note in
       let id = gen_new_unified ty in
@@ -226,6 +229,8 @@ let rec collect_unified template e = if eq_exp template e then [], [] else
     | ListE es1, ListE es2 ->
       List.fold_left2 (fun acc e1 e2 -> pairwise_concat acc (collect_unified e1 e2)) ([], []) es1 es2
     | CallE (_, as1), CallE (_, as2) -> collect_unified_args as1 as2
+    (* HARDCODE: Unifying CatE with non-CatE *)
+    | CatE (_, e1), _ -> collect_unified e1 e
     | _ -> Util.Error.error e.at "prose transformation" "cannot unify the expression with previous rule for the same instruction"
 
 and collect_unified_arg template a = if eq_arg template a then [], [] else match template.it, a.it with

spectec/src/il2al/manual.ml

@@ -1,7 +1,6 @@
 open Al
 open Ast
 open Al_util
-open Util
 
 type config = expr * expr * instr list
 
@@ -21,95 +20,6 @@ let eval_expr =
     ]
   )
 
-(*
-execution_of_CALL_REF ?(x)
-1. Assert: Due to validation, a value is on the top of the stack.
-2. Pop u_0 from the stack.
-3. If u_0 is of the case REF.NULL, then:
-  a. Trap.
-4. Assert: u_0 is of the case REF.FUNC_ADDR;
-4. Let (REF.FUNC_ADDR a) be u_0.
-5. If a < |$funcinst(z)|, then:
-  a. Let fi be $funcinst(z)[a].
-  b. Assert: fi.CODE is of the case FUNC;
-  1) Let (FUNC x' y_1 instr* ) be fi.CODE.
-  2) Let (LOCAL t)* be y_1.
-  3) Assert: $expanddt(fi.TYPE) is of the case FUNC;
-  a) Let (FUNC y_0) be $expanddt(fi.TYPE).
-  b) Let [t_1^n]->[t_2^m] be y_0.
-  c) Assert: Due to validation, there are at least n values on the top of the stack.
-  d) Pop val^n from the stack.
-  e) Let f be { LOCAL: ?(val)^n ++ $default_(t)*; MODULE: fi.MODULE; }.
-  f) Let F be the activation of f with arity m.
-  g) Enter F with label [FRAME_]:
-    1. Let L be the label_m{[]}.
-    2. Enter L with label instr* ++ [LABEL_]:
-
-*)
-
-let call_ref =
-  (* names *)
-  let x = varE "x" in
-  let ref = varE "ref" in
-  let a = varE "a" in
-  let z = varE "z" in
-  let fi = varE "fi" in
-  let y0 = varE "y_0" in
-  let y1 = varE "y_1" in
-  let t = varE "t" in
-  let t1 = varE "t_1" in
-  let t2 = varE "t_2" in
-  let n = varE "n" in
-  let m = varE "m" in
-  let v = varE "val" in
-  let f = varE "f" in
-  let ff = varE "F" in
-  let ll = varE "L" in
-  let instr = varE "instr" in
-
-  RuleA (
-    atom_of_name "CALL_REF" "admininstr",
-    [ x ],
-    [
-      assertI (topValueE None);
-      popI ref;
-      ifI (
-        isCaseOfE (ref, atom_of_name "REF.NULL" "admininstr"),
-        [ trapI () ],
-        []
-      );
-      assertI (isCaseOfE (ref, atom_of_name "REF.FUNC_ADDR" "admininstr"));
-      letI (caseE (atom_of_name "REF.FUNC_ADDR" "admininstr", [a]), ref);
-      ifI (
-        binE (LtOp, a, lenE (callE ("funcinst", [ z ]))),
-        [ letI (fi, accE (callE ("funcinst", [ z ]), idxP a));
-          assertI (isCaseOfE (accE (fi, dotP (atom_of_name "CODE" "code")), atom_of_name "FUNC" "func"));
-          letI (caseE (atom_of_name "FUNC" "func", [y0 ; y1 ; iterE (instr, ["instr"], List)]), accE (fi, dotP (atom_of_name "CODE" "code")));
-          letI (iterE (caseE (atom_of_name "LOCAL" "local", [t]), ["t"], List), y1);
-          assertI (isCaseOfE (callE ("expanddt", [ accE (fi, dotP (atom_of_name "TYPE" "type")) ]), atom_of_name "FUNC" "comptype"));
-          letI (caseE (atom_of_name "FUNC" "comptype", [y0]), callE ("expanddt", [ accE (fi, dotP (atom_of_name "TYPE" "type")) ]));
-          letI (infixE (iterE (t1, ["t_1"], ListN (n, None)), (Il.Atom.Arrow, ""), iterE (t2, ["t_2"], ListN (m, None))), y0);
-          assertI (topValuesE n);
-          popI (iterE (v, ["val"], ListN(n, None)));
-          letI (f, strE (Record.empty
-            |> Record.add
-              (atom_of_name "LOCALS" "frame")
-              (catE (iterE (optE (Some v), ["val"], ListN (n, None)), iterE (callE("default_", [t]), ["t"], List)))
-            |> Record.add
-              (atom_of_name "MODULE" "frame")
-              (accE (fi, dotP (atom_of_name "MODULE" "module")))
-          ));
-          letI (ff, frameE (Some m, f));
-          enterI (ff, listE ([caseE (atom_of_name "FRAME_" "admininstr", [])]),
-            [
-            letI (ll, labelE (m, listE []));
-            enterI (ll, catE (iterE (instr, ["instr"], List), listE ([caseE (atom_of_name "LABEL_" "admininstr", [])])), []);
-            ]
-          );
-        ], []);
-      ]
-    )
-
 (* Helper for the manual array_new.data algorithm *)
 
 let group_bytes_by =
@@ -209,7 +119,7 @@ let array_new_data =
     ]
   )
 
-let manual_algos = [eval_expr; call_ref; group_bytes_by; array_new_data;]
+let manual_algos = [eval_expr; group_bytes_by; array_new_data;]
 
 let return_instrs_of_instantiate config =
   let store, frame, rhs = config in

spectec/src/il2al/translate.ml

@@ -781,9 +781,15 @@ let translate_reduction deferred reduction =
   |> insert_deferred deferred
 
 
-let insert_pop_winstr vars = function
-  | h :: t when is_unbound vars h -> List.concat_map insert_pop t, Some h
-  | vs -> List.concat_map insert_pop vs, None
+let insert_pop_winstr vars es = match es with
+  | [] -> [], None
+  | _ ->
+    (* ASSUMPTION: The deferred pop is only possible at the bottom of the stack *)
+    let (hs, t) = Util.Lib.List.split_last es in
+    if is_unbound vars t then
+      List.concat_map insert_pop hs, Some t
+    else
+      List.concat_map insert_pop es, None
 
 let translate_context_winstr winstr =
   let at = winstr.at in

spectec/test-prose/TEST.md

@@ -1173,30 +1173,6 @@ eval_expr instr*
 2. Pop the value val from the stack.
 3. Return [val].
 
-execution_of_CALL_REF x
-1. Let z be the current state.
-2. Assert: Due to validation, a value is on the top of the stack.
-3. Pop the value ref from the stack.
-4. If ref is of the case REF.NULL, then:
-  a. Trap.
-5. Assert: Due to validation, ref is of the case REF.FUNC_ADDR.
-6. Let (REF.FUNC_ADDR a) be ref.
-7. If (a < |$funcinst(z)|), then:
-  a. Let fi be $funcinst(z)[a].
-  b. Assert: Due to validation, fi.CODE is of the case FUNC.
-  c. Let (FUNC y_0 y_1 instr*) be fi.CODE.
-  d. Let (LOCAL t)* be y_1.
-  e. Assert: Due to validation, $expanddt(fi.TYPE) is of the case FUNC.
-  f. Let (FUNC y_0) be $expanddt(fi.TYPE).
-  g. Let (t_1^n -> t_2^m) be y_0.
-  h. Assert: Due to validation, there are at least n values on the top of the stack.
-  i. Pop the values val^n from the stack.
-  j. Let f be { LOCALS: ?(val)^n ++ $default_(t)*; MODULE: fi.MODULE; }.
-  k. Let F be the activation of f with arity m.
-  l. Push F to the stack.
-  m. Let L be the label_m{[]}.
-  n. Enter instr* with label L.
-
 group_bytes_by n byte*
 1. Let n' be |byte*|.
 2. If (n' ≥ n), then:
@@ -3586,30 +3562,6 @@ eval_expr instr*
 2. Pop the value val from the stack.
 3. Return [val].
 
-execution_of_CALL_REF x
-1. Let z be the current state.
-2. Assert: Due to validation, a value is on the top of the stack.
-3. Pop the value ref from the stack.
-4. If ref is of the case REF.NULL, then:
-  a. Trap.
-5. Assert: Due to validation, ref is of the case REF.FUNC_ADDR.
-6. Let (REF.FUNC_ADDR a) be ref.
-7. If (a < |$funcinst(z)|), then:
-  a. Let fi be $funcinst(z)[a].
-  b. Assert: Due to validation, fi.CODE is of the case FUNC.
-  c. Let (FUNC y_0 y_1 instr*) be fi.CODE.
-  d. Let (LOCAL t)* be y_1.
-  e. Assert: Due to validation, $expanddt(fi.TYPE) is of the case FUNC.
-  f. Let (FUNC y_0) be $expanddt(fi.TYPE).
-  g. Let (t_1^n -> t_2^m) be y_0.
-  h. Assert: Due to validation, there are at least n values on the top of the stack.
-  i. Pop the values val^n from the stack.
-  j. Let f be { LOCALS: ?(val)^n ++ $default_(t)*; MODULE: fi.MODULE; }.
-  k. Let F be the activation of f with arity m.
-  l. Push F to the stack.
-  m. Let L be the label_m{[]}.
-  n. Enter instr* with label L.
-
 group_bytes_by n byte*
 1. Let n' be |byte*|.
 2. If (n' ≥ n), then:
@@ -6269,8 +6221,29 @@ execution_of_CALL x
 5. Push the value (REF.FUNC_ADDR a) to the stack.
 6. Execute the instruction (CALL_REF $funcinst(z)[a].TYPE).
 
-execution_of_CALL_REF
-1. YetI: TODO: It is likely that the value stack of two rules are different.
+execution_of_CALL_REF yy
+1. Let z be the current state.
+2. Assert: Due to validation, a value is on the top of the stack.
+3. Pop the value admin_u0 from the stack.
+4. If admin_u0 is of the case REF.NULL, then:
+  a. Trap.
+5. If admin_u0 is of the case REF.FUNC_ADDR, then:
+  a. Let (REF.FUNC_ADDR a) be admin_u0.
+  b. If (a < |$funcinst(z)|), then:
+    1) Let fi be $funcinst(z)[a].
+    2) Assert: Due to validation, fi.CODE is of the case FUNC.
+    3) Let (FUNC x y_0 instr*) be fi.CODE.
+    4) Let (LOCAL t)* be y_0.
+    5) Assert: Due to validation, $expanddt(fi.TYPE) is of the case FUNC.
+    6) Let (FUNC y_0) be $expanddt(fi.TYPE).
+    7) Let (t_1^n -> t_2^m) be y_0.
+    8) Assert: Due to validation, there are at least n values on the top of the stack.
+    9) Pop the values val^n from the stack.
+    10) Let f be { LOCALS: ?(val)^n ++ $default_(t)*; MODULE: fi.MODULE; }.
+    11) Let F be the activation of f with arity m.
+    12) Push F to the stack.
+    13) Let L be the label_m{[]}.
+    14) Enter instr* with label L.
 
 execution_of_RETURN_CALL x
 1. Let z be the current state.
@@ -7044,30 +7017,6 @@ eval_expr instr*
 2. Pop the value val from the stack.
 3. Return [val].
 
-execution_of_CALL_REF x
-1. Let z be the current state.
-2. Assert: Due to validation, a value is on the top of the stack.
-3. Pop the value ref from the stack.
-4. If ref is of the case REF.NULL, then:
-  a. Trap.
-5. Assert: Due to validation, ref is of the case REF.FUNC_ADDR.
-6. Let (REF.FUNC_ADDR a) be ref.
-7. If (a < |$funcinst(z)|), then:
-  a. Let fi be $funcinst(z)[a].
-  b. Assert: Due to validation, fi.CODE is of the case FUNC.
-  c. Let (FUNC y_0 y_1 instr*) be fi.CODE.
-  d. Let (LOCAL t)* be y_1.
-  e. Assert: Due to validation, $expanddt(fi.TYPE) is of the case FUNC.
-  f. Let (FUNC y_0) be $expanddt(fi.TYPE).
-  g. Let (t_1^n -> t_2^m) be y_0.
-  h. Assert: Due to validation, there are at least n values on the top of the stack.
-  i. Pop the values val^n from the stack.
-  j. Let f be { LOCALS: ?(val)^n ++ $default_(t)*; MODULE: fi.MODULE; }.
-  k. Let F be the activation of f with arity m.
-  l. Push F to the stack.
-  m. Let L be the label_m{[]}.
-  n. Enter instr* with label L.
-
 group_bytes_by n byte*
 1. Let n' be |byte*|.
 2. If (n' ≥ n), then:

spectec/test-splice/TEST.md

@@ -1294,7 +1294,6 @@ warning: definition `zbytes` was never spliced
 warning: definition `zero` was never spliced
 warning: definition `zsize` was never spliced
 warning: rule prose `exec/array.new_data` was never spliced
-warning: rule prose `exec/call_ref` was never spliced
 warning: rule prose `exec/data.drop` was never spliced
 warning: rule prose `exec/memory.grow` was never spliced
 warning: rule prose `exec/vstore_lane` was never spliced