From 1fccc8d831d609f07466252b5f5f4261b3c85547 Mon Sep 17 00:00:00 2001 From: DJ Date: Tue, 30 Apr 2024 16:16:07 +0900 Subject: [PATCH] Handle missing operand in the stack --- spectec/src/il2al/il2il.ml | 5 ++ spectec/src/il2al/manual.ml | 92 +------------------------------- spectec/src/il2al/translate.ml | 12 +++-- spectec/test-prose/TEST.md | 97 ++++++++-------------------------- spectec/test-splice/TEST.md | 1 - 5 files changed, 38 insertions(+), 169 deletions(-) diff --git a/spectec/src/il2al/il2il.ml b/spectec/src/il2al/il2il.ml index ddf8f29996..5c202da14b 100644 --- a/spectec/src/il2al/il2il.ml +++ b/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 diff --git a/spectec/src/il2al/manual.ml b/spectec/src/il2al/manual.ml index 12e8f97ccc..6687718cf7 100644 --- a/spectec/src/il2al/manual.ml +++ b/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 diff --git a/spectec/src/il2al/translate.ml b/spectec/src/il2al/translate.ml index e042d21e9c..75227d5fb3 100644 --- a/spectec/src/il2al/translate.ml +++ b/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 diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index 46fa0f5d56..231bf16345 100644 --- a/spectec/test-prose/TEST.md +++ b/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: diff --git a/spectec/test-splice/TEST.md b/spectec/test-splice/TEST.md index 83d3aad71c..6a804d2874 100644 --- a/spectec/test-splice/TEST.md +++ b/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