refactor(al): add pop all instrs, remove remove_or

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

@@ -60,9 +60,11 @@ rule Step_pure/select-false:
 
 ;; Block instructions
 
-rule Step_read/block:
-  z; (BLOCK t? instr*)  ~>  (LABEL_ n `{eps} instr*)
-  -- if t? = eps /\ n = 0 \/ t? =/= eps /\ n = 1  ;; TODO: allow |t?|
+rule Step_read/block-0:
+  z; (BLOCK eps instr*)  ~>  (LABEL_ 0 `{eps} instr*)
+
+rule Step_read/block-1:
+  z; (BLOCK t instr*)  ~>  (LABEL_ 1 `{eps} instr*)
 
 rule Step_read/loop:
   z; (LOOP t? instr*)  ~>  (LABEL_ 0 `{LOOP t? instr*} instr*)

spectec/src/al/al_util.ml

@@ -24,6 +24,7 @@ let pushI ?(at = no) e = PushI e |> mk_instr at
 let popI ?(at = no) e = PopI e |> mk_instr at
 let popsI ?(at = no) e _ = PopI e |> mk_instr at (* TODO *)
 let popAllI ?(at = no) e = PopAllI e |> mk_instr at
+let popAllInstrI ?(at = no) e = PopAllInstrI e |> mk_instr at
 let letI ?(at = no) (e1, e2) = LetI (e1, e2) |> mk_instr at
 let trapI ?(at = no) () = TrapI |> mk_instr at
 let throwI ?(at = no) e = ThrowI e |> mk_instr at

spectec/src/al/ast.ml

@@ -148,6 +148,7 @@ and instr' =
   | PushI of expr                         (* `push` expr *)
   | PopI of expr                          (* `pop` expr *)
   | PopAllI of expr                       (* `popall` expr *)
+  | PopAllInstrI of expr                  (* `popall` expr on instruction stack *)
   | LetI of expr * expr                   (* `let` expr `=` expr *)
   | TrapI                                 (* `trap` *)
   | ThrowI of expr                        (* `throw` *)

spectec/src/al/eq.ml

@@ -105,6 +105,7 @@ let rec eq_instr i1 i2 =
   | PushI e1, PushI e2
   | PopI e1, PopI e2
   | PopAllI e1, PopAllI e2 -> eq_expr e1 e2
+  | PopAllInstrI e1, PopAllInstrI e2 -> eq_expr e1 e2
   | LetI (e11, e12), LetI (e21, e22) -> eq_expr e11 e21 && eq_expr e12 e22
   | TrapI, TrapI
   | NopI, NopI -> true

spectec/src/al/free.ml

@@ -91,7 +91,7 @@ let rec free_instr instr =
   | OtherwiseI il -> free_list free_instr il
   | EitherI (il1, il2) -> free_list free_instr il1 @ free_list free_instr il2
   | TrapI | NopI | ReturnI None | ExitI _ | YetI _ -> IdSet.empty
-  | ThrowI e | PushI e | PopI e | PopAllI e | ReturnI (Some e)
+  | ThrowI e | PushI e | PopI e | PopAllI e | PopAllInstrI e | ReturnI (Some e)
   | ExecuteI e | ExecuteSeqI e ->
     free_expr e
   | LetI (e1, e2) | AppendI (e1, e2) | FieldWiseAppendI (e1, e2) -> free_expr e1 @ free_expr e2

spectec/src/al/print.ml

@@ -320,6 +320,9 @@ let rec string_of_instr' depth instr =
   | PopAllI e ->
     sprintf " Pop_all %s"
       (string_of_expr e)
+  | PopAllInstrI e ->
+    sprintf " Pop_all_instr %s"
+      (string_of_expr e)
   | LetI (e1, e2) ->
     sprintf " Let %s = %s" (string_of_expr e1)
       (string_of_expr e2)
@@ -595,6 +598,7 @@ let rec structured_string_of_instr' depth instr =
   | PushI e -> "PushI (" ^ structured_string_of_expr e ^ ")"
   | PopI e -> "PopI (" ^ structured_string_of_expr e ^ ")"
   | PopAllI e -> "PopAllI (" ^ structured_string_of_expr e ^ ")"
+  | PopAllInstrI e -> "PopAllInstrI (" ^ structured_string_of_expr e ^ ")"
   | LetI (e1, e2) ->
     "LetI ("
     ^ structured_string_of_expr e1

spectec/src/al/walk.ml

@@ -71,7 +71,7 @@ let walk_instr (walker: unit_walker) (instr: instr) : unit =
     walker.walk_expr walker e1; walker.walk_expr walker e2;
     List.iter (walker.walk_instr walker) il
   | TrapI | NopI | ReturnI None | ExitI _ | YetI _ -> ()
-  | AssertI e | ThrowI e | PushI e | PopI e | PopAllI e
+  | AssertI e | ThrowI e | PushI e | PopI e | PopAllI e | PopAllInstrI e
   | ReturnI (Some e)| ExecuteI e | ExecuteSeqI e -> walker.walk_expr walker e
   | LetI (e1, e2) | AppendI (e1, e2) | FieldWiseAppendI (e1, e2) ->
     walker.walk_expr walker e1; walker.walk_expr walker e2
@@ -184,6 +184,7 @@ let walk_instr (walker: walker) (instr: instr) : instr =
     | PushI e -> PushI (walk_expr e)
     | PopI e -> PopI (walk_expr e)
     | PopAllI e -> PopAllI (walk_expr e)
+    | PopAllInstrI e -> PopAllInstrI (walk_expr e)
     | LetI (e1, e2) -> LetI (walk_expr e1, walk_expr e2)
     | TrapI -> TrapI
     | ThrowI e -> ThrowI (walk_expr e)
@@ -335,6 +336,7 @@ let rec walk_instr f (instr:instr) : instr list =
       | PushI e -> PushI (new_e e)
       | PopI e -> PopI (new_e e)
       | PopAllI e -> PopAllI (new_e e)
+      | PopAllInstrI e -> PopAllInstrI (new_e e)
       | LetI (e1, e2) -> LetI (new_e e1, new_e e2)
       | TrapI -> TrapI
       | ThrowI e -> ThrowI (new_e e)

spectec/src/backend-interpreter/ds.ml

@@ -327,6 +327,10 @@ module WasmContext = struct
 
   (* Instr stack *)
 
+  let pop_instr_stack () =
+    let v_ctx, vs, vs_instr = pop_context () in
+    push_context (v_ctx, vs, []); vs_instr
+
   let pop_instr () =
     let v_ctx, vs, vs_instr = pop_context () in
     match vs_instr with

spectec/src/backend-interpreter/ds.mli

@@ -79,6 +79,7 @@ module WasmContext : sig
   val push_value : value -> unit
   val pop_value : unit -> value
 
+  val pop_instr_stack : unit -> value list
   val pop_instr : unit -> value
 end
 

spectec/src/backend-interpreter/interpreter.ml

@@ -628,6 +628,10 @@ and step_instr (fname: string) (ctx: AlContext.t) (env: value Env.t) (instr: ins
     let v = WasmContext.pop_value_stack () |> List.rev |> listV_of_list in
     let new_env = assign e v env in
     AlContext.set_env new_env ctx
+  | PopAllInstrI e ->
+    let v = WasmContext.pop_instr_stack () |> listV_of_list in
+    let new_env = assign e v env in
+    AlContext.set_env new_env ctx
   | LetI (e1, e2) ->
     let new_env = ctx |> AlContext.get_env |> assign e1 (eval_expr env e2) in
     AlContext.set_env new_env ctx

spectec/src/backend-prose/print.ml

@@ -327,6 +327,9 @@ let rec string_of_instr' depth instr =
   | PopAllI e ->
     sprintf "%s Pop all values %s from the top of the stack." (make_index depth)
       (string_of_expr e)
+  | PopAllInstrI e ->
+    sprintf "%s Pop all instructions %s from the top of the stack." (make_index depth)
+      (string_of_expr e)
   | LetI (e1, e2) ->
     sprintf "%s Let %s be %s." (make_index depth) (string_of_expr e1)
       (string_of_expr e2)

spectec/src/backend-prose/render.ml

@@ -634,6 +634,9 @@ let rec render_al_instr env algoname index depth instr =
   | Al.Ast.PopAllI e ->
     sprintf "%s Pop all values %s from the top of the stack." (render_order index depth)
       (render_expr env e)
+  | Al.Ast.PopAllInstrI e ->
+    sprintf "%s Pop all instructions %s from the top of the stack." (render_order index depth)
+      (render_expr env e)
   | Al.Ast.LetI (e, { it = Al.Ast.IterE ({ it = Al.Ast.InvCallE (id, nl, al); _ }, ids, iter); _ }) ->
     let elhs, erhs = al_invcalle_to_al_bine e id nl al in
     let ebin = Al.Al_util.binE (Al.Ast.EqOp, elhs, erhs) ~note:Al.Al_util.no_note in

spectec/src/il2al/animate.ml

@@ -48,7 +48,7 @@ let is_assign env (tag, prem, _) =
 let is_pop env row =
   is_assign env row &&
   match (unwrap row).it with
-  | LetPr (_, rhs, _) -> Il.Print.string_of_typ rhs.note = "stackT"
+  | LetPr (_, rhs, _) -> List.mem (Il.Print.string_of_typ rhs.note) ["stackT"; "instrstackT"]
   | _ -> false
 
 (* iteratively select pop, condition and assignment premises,

spectec/src/il2al/encode.ml

@@ -89,6 +89,7 @@ let arg e =
 let input_vars = [
   "input";
   "stack0";
+  "instrstack0";
   "ctxt";
   "state";
   "unused";
@@ -99,10 +100,19 @@ let input_vars = [
 let encode_inner_stack context_opt stack =
   let dropped, es = stack_to_list stack |> List.rev |> drop_until is_case in
 
-  let unused_prems =
-    if List.length dropped = 0 then
-      []
-    else
+  (* HARDCODE: try to match instr* at the end *)
+  let rec real_typ typ = function
+    | SubE (e, typ, _) -> real_typ typ e.it
+    | _ -> typ
+  in
+  let instr_prems = match dropped with
+    | [] -> []
+    | [{ it = IterE (instr, (List, _)); _ } as instrs] when real_typ instr.note instr.it |> Print.string_of_typ = "instr" ->
+      let t = mk_varT "instrstackT" in
+      let rhs = CallE (mk_id "pop_instrs", [ arg (mk_varE "instrstack0" "instrstackT") ]) $$ no_region % t in
+      let lhs = { instrs with note = t } in
+      [IfPr (CmpE (EqOp, lhs, rhs) $$ instrs.at % (BoolT $ no_region)) $ instrs.at]
+    | _ ->
       let unused = TupE dropped $$ no_region % (mk_varT "unusedT") in
       [LetPr (unused, mk_varE "unused" "unusedT", free_ids unused) $ no_region]
   in
@@ -114,7 +124,7 @@ let encode_inner_stack context_opt stack =
       match context_opt with
       | None -> assert false
       | Some e ->
-        Some (LetPr (e, mk_varE "input" "inputT", free_ids e) $ e.at), unused_prems
+        Some (LetPr (e, mk_varE "input" "inputT", free_ids e) $ e.at), instr_prems
     )
   | _ ->
     (* ASSUMPTION: The top of the stack should be now the target instruction *)
@@ -136,7 +146,7 @@ let encode_inner_stack context_opt stack =
       IfPr (CmpE (EqOp, lhs, rhs) $$ e.at % (BoolT $ no_region)) $ e.at
     ) operands in
 
-    None, prem :: prems @ unused_prems
+    None, prem :: prems @ instr_prems
 
 let encode_stack stack =
   match stack.it with

spectec/src/il2al/il2al_util.ml

@@ -43,6 +43,7 @@ let is_let_prem_with_rhs_type t prem =
     )
   | _ -> false
 let is_pop : prem -> bool = is_let_prem_with_rhs_type "stackT"
+let is_pop_instr : prem -> bool = is_let_prem_with_rhs_type "instrstackT"
 let is_ctxt_prem : prem -> bool = is_let_prem_with_rhs_type "contextT"
 
 let extract_context r =
@@ -55,7 +56,7 @@ let extract_pops rgroup =
   (* Helpers *)
   let rec extract_pops' acc prems premss =
     match prems with
-    | hd :: tl when is_pop hd ->
+    | hd :: tl when is_pop hd || is_pop_instr hd ->
       let partitions = List.map (List.partition (Il.Eq.eq_prem hd)) premss in
       let fsts = List.map fst partitions in
       let snds = List.map snd partitions in

spectec/src/il2al/preprocess.ml

@@ -6,62 +6,6 @@ open Def
 open Il2al_util
 
 
-(* Remove or *)
-let remove_or_exp e =
-  match e.it with (* TODO: recursive *)
-  | BinE (OrOp, e1, e2) -> [ e1; e2 ]
-  | _ -> [ e ]
-
-let rec remove_or_prem prem =
-  match prem.it with
-  | IfPr e -> e |> remove_or_exp |> List.map (fun e' -> IfPr e' $ prem.at)
-  | IterPr (prem, iterexp) ->
-    prem
-    |> remove_or_prem
-    |> List.map (fun new_prem -> IterPr (new_prem, iterexp) $ prem.at)
-  | _ -> [ prem ]
-
-let remove_or_rule rule =
-  match rule.it with
-  | RuleD (id, binds, mixop, args, prems) ->
-    let premss = List.map remove_or_prem prems in
-    let premss' = List.fold_right (fun ps pss ->
-      (* Duplice pss *)
-      List.concat_map (fun cur ->
-        List.map (fun p -> p :: cur) ps
-      ) pss
-    ) premss [[]] in
-
-    if List.length premss' = 1 then [ rule ] else
-
-    List.mapi (fun i prems' ->
-      let id' = id.it ^ "-" ^ string_of_int i $ id.at in
-      RuleD (id', binds, mixop, args, prems') $ rule.at
-    ) premss'
-
-let remove_or_clause clause =
-  match clause.it with
-  | DefD (binds, args, exp, prems) ->
-    let premss = List.map remove_or_prem prems in
-    let premss' = List.fold_right (fun ps pss ->
-      (* Duplice pss *)
-      List.concat_map (fun cur ->
-        List.map (fun p -> p :: cur) ps
-      ) pss
-    ) premss [[]] in
-
-    if List.length premss' = 1 then [ clause ] else
-
-    List.map (fun prems' -> DefD (binds, args, exp, prems') $ clause.at) premss'
-
-let remove_or def =
-  match def.it with
-  | RelD (id, mixop, typ, rules) ->
-    RelD (id, mixop, typ, List.concat_map remove_or_rule rules) $ def.at
-  | DecD (id, params, typ, clauses) ->
-    DecD (id, params, typ, List.concat_map remove_or_clause clauses) $ def.at
-  | _ -> def
-
 (* HARDCODE: Remove a reduction rule for the block context, specifically, for THROW_REF *)
 let is_block_context_exp e =
   match e.it with
@@ -161,7 +105,6 @@ let preprocess_clause (clause: clause) : clause =
 let preprocess_def (def: def) : def =
   let def' =
     def
-    |> remove_or
     |> remove_block_context
   in
 

spectec/src/il2al/translate.ml

@@ -802,6 +802,8 @@ and handle_special_lhs lhs rhs free_ids =
     let args = args_of_call rhs in
     let pop_num = List.hd args |> arg2expr in
     insert_pop e pop_num
+  | _ when (Il.Print.string_of_typ rhs.note) = "instrstackT" ->
+    [popAllInstrI { lhs with note = listT instrT } ~at:lhs.at]
   (* Handle inverse function call *)
   | CallE _ -> handle_call_lhs lhs rhs free_ids
   (* Handle iterator *)

spectec/src/il2al/unify.ml

@@ -231,14 +231,14 @@ let is_encoded_ctxt pr =
   match pr.it with
   | LetPr (_, e, _) ->
     (match e.note.it with
-    | VarT (id, []) -> List.mem id.it ["inputT"; "stackT"; "contextT"]
+    | VarT (id, []) -> List.mem id.it ["inputT"; "stackT"; "instrstackT"; "contextT"]
     | _ -> false)
   | _ -> false
 let is_encoded_pop_or_winstr pr =
   match pr.it with
   | LetPr (_, e, _) ->
     (match e.note.it with
-    | VarT (id, []) -> List.mem id.it ["inputT"; "stackT"]
+    | VarT (id, []) -> List.mem id.it ["inputT"; "stackT"; "instrstackT"]
     | _ -> false)
   | _ -> false