Skip to content

Commit

Permalink
Merge branch 'kaist-plrg-fix-ctx'
Browse files Browse the repository at this point in the history
  • Loading branch information
@702fbtngus
702fbtngus committed Sep 19, 2024
2 parents 688ccee + cb5f4d7 commit 8bd084b
Show file tree
Hide file tree
Showing 25 changed files with 765 additions and 1,176 deletions.
5 changes: 5 additions & 0 deletions spectec/spec/wasm-3.0/4-runtime.watsup
View file
Original file line number Diff line number Diff line change
Expand Up @@ -155,3 +155,8 @@ syntax instr/admin hint(desc "administrative instruction") =
| FRAME_ n `{frame} instr* hint(show FRAME_%#% %%)
| HANDLER_ n `{catch*} instr* hint(show HANDLER_%#% %%)
| TRAP

syntax evalctx hint(desc "evaluation context") =
| LABEL_ n `{instr*} hint(show LABEL_%#%)
| FRAME_ n `{frame} hint(show FRAME_%#%)
| HANDLER_ n `{catch*} hint(show HANDLER_%#%)
35 changes: 19 additions & 16 deletions spectec/src/al/al_util.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,24 +61,15 @@ let invCallE ?(at = no) ~note (id, il, el) = InvCallE (id, il, el) |> mk_expr at
let iterE ?(at = no) ~note (e, ite) = IterE (e, ite) |> mk_expr at note
let optE ?(at = no) ~note e_opt = OptE e_opt |> mk_expr at note
let listE ?(at = no) ~note el = ListE el |> mk_expr at note
let arityE ?(at = no) ~note e = ArityE e |> mk_expr at note
let frameE ?(at = no) ~note (e_opt, e) = FrameE (e_opt, e) |> mk_expr at note
let labelE ?(at = no) ~note (e1, e2) = LabelE (e1, e2) |> mk_expr at note
let getCurStateE ?(at = no) ~note () = GetCurStateE |> mk_expr at note
let getCurFrameE ?(at = no) ~note () = GetCurFrameE |> mk_expr at note
let getCurLabelE ?(at = no) ~note () = GetCurLabelE |> mk_expr at note
let getCurContextE ?(at = no) ~note () = GetCurContextE |> mk_expr at note
let contE ?(at = no) ~note e = ContE e |> mk_expr at note
let getCurContextE ?(at = no) ~note e = GetCurContextE e |> mk_expr at note
let chooseE ?(at = no) ~note e = ChooseE e |> mk_expr at note
let isCaseOfE ?(at = no) ~note (e, a) = IsCaseOfE (e, a) |> mk_expr at note
let isValidE ?(at = no) ~note e = IsValidE e |> mk_expr at note
let contextKindE ?(at = no) ~note a = ContextKindE a |> mk_expr at note
let isDefinedE ?(at = no) ~note e = IsDefinedE e |> mk_expr at note
let matchE ?(at = no) ~note (e1, e2) = MatchE (e1, e2) |> mk_expr at note
let hasTypeE ?(at = no) ~note (e, ty) = HasTypeE (e, ty) |> mk_expr at note
let topLabelE ?(at = no) ~note () = TopLabelE |> mk_expr at note
let topFrameE ?(at = no) ~note () = TopFrameE |> mk_expr at note
let topHandlerE ?(at = no) ~note () = TopHandlerE |> mk_expr at note
let topValueE ?(at = no) ~note e_opt = TopValueE e_opt |> mk_expr at note
let topValuesE ?(at = no) ~note e = TopValuesE e |> mk_expr at note
let subE ?(at = no) ~note (id, ty) = SubE (id, ty) |> mk_expr at note
Expand Down Expand Up @@ -185,6 +176,12 @@ let rec typ_to_var_name ty =
| Il.Ast.TupT tys -> List.map typ_to_var_name (List.map snd tys) |> String.concat "_"
| Il.Ast.IterT (t, _) -> typ_to_var_name t

let context_names = [
"FRAME_";
"LABEL_";
"HANDLER_";
]

(* Destruct *)

let unwrap_optv: value -> value option = function
Expand Down Expand Up @@ -250,16 +247,25 @@ let args_of_casev = function
| v -> fail_value "args_of_casev" v

let arity_of_framev: value -> value = function
| FrameV (Some v, _) -> v
| CaseV ("FRAME_", [v; _]) -> v
| v -> fail_value "arity_of_framev" v

let unwrap_framev: value -> value = function
| FrameV (_, v) -> v
| CaseV ("FRAME_", [_; v]) -> v
| v -> fail_value "unwrap_framev" v


(* Mixop *)

let atom_of_name name typ = El.Atom.Atom name $$ no_region % (El.Atom.info typ)
let atom_of_atom' atom' typ = atom' $$ no_region % (El.Atom.info typ)

let frame_atom = atom_of_name "FRAME_" "evalctx"
let frameE ?(at = no) ~note (arity, e) =
let frame_mixop = [[frame_atom]; [atom_of_atom' El.Atom.LBrace "evalctx"]; [atom_of_atom' El.Atom.RBrace "evalctx"]] in
caseE (frame_mixop, [arity; e]) ~at:at ~note:note


let get_atom op =
match List.find_opt (fun al -> List.length al <> 0) op with
| Some al -> Some(List.hd al)
Expand All @@ -279,11 +285,8 @@ let boolT = Il.Ast.BoolT $ no_region
let natT = Il.Ast.NumT Il.Ast.NatT $ no_region
let topT = varT "TOP" []
let valT = varT "val" []
let callframeT = varT "callframe" []
let frameT = varT "frame" []
let labelT = varT "label" []
let handlerT = varT "handler" []
let stateT = varT "state" []
let instrT = varT "instr" []
let admininstrT = varT "admininstr" []
let funcT = varT "func" []
let evalctxT = varT "evalctx" []
15 changes: 2 additions & 13 deletions spectec/src/al/ast.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,8 +35,6 @@ and value =
| CaseV of id * value list (* constructor *)
| OptV of value option (* optional value *)
| TupV of value list (* tuple of values *)
| FrameV of value option * value (* TODO: desugar using CaseV? *)
| LabelV of value * value (* TODO: desugar using CaseV? *)
| FnameV of id (* name of the first order function *)

type extend_dir = (* direction of extension *)
Expand Down Expand Up @@ -101,25 +99,16 @@ and expr' =
| IterE of expr * iterexp (* expr (`{` id* `}`)* *)
| OptE of expr option (* expr? *)
| ListE of expr list (* `[` expr* `]` *)
| ArityE of expr (* "the arity of expr" *)
| FrameE of expr option * expr (* "the activation of expr (with arity expr)?" *)
| LabelE of expr * expr (* "the label whose arity is expr and whose continuation is expr" *)
| GetCurStateE (* "the current state" *)
| GetCurFrameE (* "the current frame" *)
| GetCurLabelE (* "the current lbael" *)
| GetCurContextE (* "the current context" *)
| ContE of expr (* "the continuation of" expr *)
| GetCurContextE of atom option (* "the current context of certain (Some) or any (None) type" *)
| ChooseE of expr (* "an element of" expr *)
(* Conditions *)
| IsCaseOfE of expr * atom (* expr is of the case atom *)
| IsValidE of expr (* expr is valid *)
| ContextKindE of atom (* "the top of the stack is a" atom *)
| ContextKindE of atom (* "the fisrt non-value entry of the stack is a" atom *)
| IsDefinedE of expr (* expr is defined *)
| MatchE of expr * expr (* expr matches expr *)
| HasTypeE of expr * typ (* the type of expr is ty *)
| TopFrameE (* "a frame is now on the top of the stack" *)
| TopLabelE (* "a label is now on the top of the stack" *)
| TopHandlerE (* "a handler is now on the top of the stack" *)
(* Conditions used in assertions *)
| TopValueE of expr option (* "a value (of type expr)? is now on the top of the stack" *)
| TopValuesE of expr (* "at least expr number of values on the top of the stack" *)
Expand Down
15 changes: 2 additions & 13 deletions spectec/src/al/eq.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,26 +36,15 @@ let rec eq_expr e1 e2 =
eq_expr e1 e2 && eq_iterexp ie1 ie2
| OptE eo1, OptE eo2 -> eq_expr_opt eo1 eo2
| ListE el1, ListE el2 -> eq_exprs el1 el2
| ArityE e1, ArityE e2 -> eq_expr e1 e2
| FrameE (eo1, e1), FrameE (eo2, e2) ->
eq_expr_opt eo1 eo2 && eq_expr e1 e2
| LabelE (e11, e12), LabelE (e21, e22) ->
eq_expr e11 e21 && eq_expr e12 e22
| GetCurStateE, GetCurStateE
| GetCurFrameE, GetCurFrameE
| GetCurLabelE, GetCurLabelE
| GetCurContextE, GetCurContextE -> true
| ContE e1, ContE e2 -> eq_expr e1 e2
| GetCurStateE, GetCurStateE -> true
| GetCurContextE i1, GetCurContextE i2 -> Option.equal (=) i1 i2
| ChooseE e1, ChooseE e2 -> eq_expr e1 e2
| IsCaseOfE (e1, a1), IsCaseOfE (e2, a2) -> eq_expr e1 e2 && El.Atom.eq a1 a2
| IsValidE e1, IsValidE e2 -> eq_expr e1 e2
| ContextKindE a1, ContextKindE a2 -> El.Atom.eq a1 a2
| IsDefinedE e1, IsDefinedE e2 -> eq_expr e1 e2
| MatchE (e11, e12), MatchE (e21, e22) -> eq_expr e11 e21 && eq_expr e12 e22
| HasTypeE (e1, t1), HasTypeE (e2, t2) -> eq_expr e1 e2 && Il.Eq.eq_typ t1 t2
| TopLabelE, TopLabelE
| TopFrameE, TopFrameE
| TopHandlerE, TopHandlerE -> true
| TopValueE eo1, TopValueE eo2 -> eq_expr_opt eo1 eo2
| TopValuesE e1, TopValuesE e2 -> eq_expr e1 e2
| SubE (i1, t1), SubE (i2, t2) -> i1 = i2 && Il.Eq.eq_typ t1 t2
Expand Down
5 changes: 2 additions & 3 deletions spectec/src/al/eval.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,12 +21,11 @@ let rec get_subst lhs rhs s =
match lhs.it, rhs.it with
| VarE id, _ -> Subst.add id rhs s
| UnE (op1, e1), UnE (op2, e2) when op1 = op2 -> get_subst e1 e2 s
| OptE (Some e1), OptE (Some e2) | FrameE (None, e1), FrameE (None, e2) ->
| OptE (Some e1), OptE (Some e2) ->
get_subst e1 e2 s
| BinE (op1, e11, e12), BinE (op2, e21, e22) when op1 = op2 ->
s |> get_subst e11 e21 |> get_subst e12 e22
| CompE (e11, e12), CompE (e21, e22) | CatE (e11, e12), CatE (e21, e22)
| LabelE (e11, e12), LabelE (e21, e22) | FrameE (Some e11, e12), FrameE (Some e21, e22) ->
| CompE (e11, e12), CompE (e21, e22) | CatE (e11, e12), CatE (e21, e22) ->
s |> get_subst e11 e21 |> get_subst e12 e22
| TupE el1, TupE el2 | ListE el1, ListE el2 ->
List.fold_right2 get_subst el1 el2 s
Expand Down
13 changes: 2 additions & 11 deletions spectec/src/al/free.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,24 +19,18 @@ let rec free_expr expr =
| NumE _
| BoolE _
| GetCurStateE
| GetCurLabelE
| GetCurContextE
| GetCurFrameE
| GetCurContextE _
| ContextKindE _
| YetE _ -> IdSet.empty
| VarE id
| SubE (id, _) -> free_id id
| UnE (_, e)
| LenE e
| ArityE e
| ContE e
| ChooseE e -> free_expr e
| BinE (_, e1, e2)
| CompE (e1, e2)
| CatE (e1, e2)
| MemE (e1, e2)
| LabelE (e1, e2) -> free_expr e1 @ free_expr e2
| FrameE (e_opt, e) -> free_opt free_expr e_opt @ free_expr e
| MemE (e1, e2) -> free_expr e1 @ free_expr e2
| CallE (_, al)
| InvCallE (_, _, al) -> free_list free_arg al
| TupE el
Expand All @@ -54,9 +48,6 @@ let rec free_expr expr =
let bound, free2 = free_iterexp ie in
(free1 - bound) @ free2
| MatchE (e1, e2) -> free_expr e1 @ free_expr e2
| TopLabelE
| TopFrameE
| TopHandlerE
| TopValueE None -> IdSet.empty
| IsDefinedE e
| IsCaseOfE (e, _)
Expand Down
53 changes: 8 additions & 45 deletions spectec/src/al/print.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,10 +58,6 @@ let rec string_of_record r =

and string_of_value =
function
| LabelV (v1, v2) ->
sprintf "Label_%s %s" (string_of_value v1) (string_of_value v2)
| FrameV (None, v2) -> sprintf "(Frame %s)" (string_of_value v2)
| FrameV (Some v1, v2) -> sprintf "(Frame %s %s)" (string_of_value v1) (string_of_value v2)
| ListV lv -> "[" ^ string_of_values ", " (Array.to_list !lv) ^ "]"
| NumV n -> "0x" ^ Z.format "%X" n
| BoolV b -> string_of_bool b
Expand Down Expand Up @@ -152,16 +148,9 @@ and string_of_expr expr =
| MemE (e1, e2) ->
sprintf "%s <- %s" (string_of_expr e1) (string_of_expr e2)
| LenE e -> sprintf "|%s|" (string_of_expr e)
| ArityE e -> sprintf "arity(%s)" (string_of_expr e)
| GetCurStateE -> "current_state()"
| GetCurLabelE -> "current_label()"
| GetCurFrameE -> "current_frame()"
| GetCurContextE -> "current_context()"
| FrameE (None, e2) ->
sprintf "callframe(%s)" (string_of_expr e2)
| FrameE (Some e1, e2) ->
sprintf "callframe(%s, %s)" (string_of_expr e1)
(string_of_expr e2)
| GetCurContextE None -> "current_context()"
| GetCurContextE (Some a) -> sprintf "current_context(%s)" (string_of_atom a)
| ListE el -> "[" ^ string_of_exprs ", " el ^ "]"
| AccE (e, p) -> sprintf "%s%s" (string_of_expr e) (string_of_path p)
| ExtE (e1, ps, e2, dir) -> (
Expand All @@ -171,10 +160,7 @@ and string_of_expr expr =
| UpdE (e1, ps, e2) ->
sprintf "update(%s%s, %s)" (string_of_expr e1) (string_of_paths ps) (string_of_expr e2)
| StrE r -> string_of_record_expr r
| ContE e -> sprintf "cont(%s)" (string_of_expr e)
| ChooseE e -> sprintf "choose(%s)" (string_of_expr e)
| LabelE (e1, e2) ->
sprintf "label(%s, %s)" (string_of_expr e1) (string_of_expr e2)
| VarE id -> id
| SubE (id, _) -> id
| IterE (e, ie) -> string_of_expr e ^ string_of_iterexp ie
Expand All @@ -185,6 +171,9 @@ and string_of_expr expr =
let op' = List.map (fun al -> String.concat "" (List.map string_of_atom al)) op in
(match op' with
| [] -> "()"
| _::tl when List.length tl != List.length el ->
let res = String.concat ", " (List.map string_of_expr el) in
"(Invalid CaseE: " ^ (string_of_mixop op) ^ " (" ^ res ^ "))"
| hd::tl ->
let res =
List.fold_left2 (
Expand All @@ -202,12 +191,6 @@ and string_of_expr expr =
| IsCaseOfE (e, a) -> sprintf "case(%s) == %s" (string_of_expr e) (string_of_atom a)
| HasTypeE (e, t) -> sprintf "type(%s) == %s" (string_of_expr e) (string_of_typ t)
| IsValidE e -> sprintf "valid(%s)" (string_of_expr e)
| TopLabelE -> "top_label()"
(* TODO: "type(top()) == label"*)
| TopFrameE -> "top_frame()"
(* TODO: "type(top()) == frame"*)
| TopHandlerE -> "top_handler()"
(* TODO: "type(top()) == handler"*)
| TopValueE (Some e) -> sprintf "top_value(%s)" (string_of_expr e)
| TopValueE None -> "top_value()"
| TopValuesE e -> sprintf "top_values(%s)" (string_of_expr e)
Expand Down Expand Up @@ -267,12 +250,7 @@ let enter_block f instrs =
(* Prefix for stack push/pop operations *)
let string_of_stack_prefix expr =
match expr.it with
| GetCurContextE
| GetCurFrameE
| GetCurLabelE
| ContE _
| LabelE _
| FrameE _
| GetCurContextE _
| VarE ("F" | "L") -> ""
| IterE _ -> ""
| _ -> ""
Expand Down Expand Up @@ -396,8 +374,6 @@ let string_of_algorithm algo =
(* Values *)

let rec structured_string_of_value = function
| LabelV (v1, v2) -> "LabelV (" ^ structured_string_of_value v1 ^ "," ^ structured_string_of_value v2 ^ ")"
| FrameV _ -> "FrameV (TODO)"
| ListV lv -> "ListV" ^ "[" ^ string_of_values ", " (Array.to_list !lv) ^ "]"
| BoolV b -> "BoolV (" ^ string_of_bool b ^ ")"
| NumV n -> "NumV (" ^ Z.to_string n ^ ")"
Expand Down Expand Up @@ -473,12 +449,9 @@ and structured_string_of_expr expr =
^ structured_string_of_expr e2
^ ")"
| LenE e -> "LenE (" ^ structured_string_of_expr e ^ ")"
| ArityE e -> "ArityE (" ^ structured_string_of_expr e ^ ")"
| GetCurStateE -> "GetCurStateE"
| GetCurLabelE -> "GetCurLabelE"
| GetCurFrameE -> "GetCurFrameE"
| GetCurContextE -> "GetCurContextE"
| FrameE _ -> "FrameE TODO"
| GetCurContextE None -> "GetCurContextE"
| GetCurContextE (Some a) -> sprintf "GetCurContextE (%s)" (string_of_atom a)
| ListE el -> "ListE ([" ^ structured_string_of_exprs el ^ "])"
| AccE (e, p) ->
"AccE ("
Expand All @@ -505,14 +478,7 @@ and structured_string_of_expr expr =
^ structured_string_of_expr e2
^ ")"
| StrE r -> "StrE (" ^ structured_string_of_record_expr r ^ ")"
| ContE e1 -> "ContE (" ^ structured_string_of_expr e1 ^ ")"
| ChooseE e1 -> "ChooseE (" ^ structured_string_of_expr e1 ^ ")"
| LabelE (e1, e2) ->
"LabelE ("
^ structured_string_of_expr e1
^ ", "
^ structured_string_of_expr e2
^ ")"
| VarE id -> "VarE (" ^ id ^ ")"
| SubE (id, t) -> sprintf "SubE (%s, %s)" id (string_of_typ t)
| IterE (e, (iter, xes)) ->
Expand All @@ -534,9 +500,6 @@ and structured_string_of_expr expr =
| HasTypeE (e, t) ->
sprintf "HasTypeE (%s, %s)" (structured_string_of_expr e) (string_of_typ t)
| IsValidE e -> "IsValidE (" ^ structured_string_of_expr e ^ ")"
| TopLabelE -> "TopLabelE"
| TopFrameE -> "TopFrameE"
| TopHandlerE -> "TopHandlerE"
| TopValueE None -> "TopValueE"
| TopValueE (Some e) -> "TopValueE (" ^ structured_string_of_expr e ^ ")"
| TopValuesE e -> "TopValuesE (" ^ structured_string_of_expr e ^ ")"
Expand Down
36 changes: 4 additions & 32 deletions spectec/src/al/valid.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -468,7 +468,8 @@ and valid_expr env (expr: expr) : unit =
| VarE id ->
if not (Env.mem id env) then error expr.at ("free identifier " ^ id)
| NumE _ -> check_num source expr.note;
| BoolE _ | TopFrameE | TopLabelE | TopHandlerE | ContextKindE _ -> check_bool source expr.note
| BoolE _ | IsCaseOfE _ | IsValidE _ | MatchE _ | HasTypeE _ | ContextKindE _ ->
check_bool source expr.note;
| UnE (NotOp, expr') ->
valid_expr env expr';
check_bool source expr.note;
Expand Down Expand Up @@ -578,39 +579,10 @@ and valid_expr env (expr: expr) : unit =
l
|> List.map note
|> List.iter (check_match source elem_typ)
| ArityE expr1 ->
valid_expr env expr1;
check_num source expr.note;
check_context source expr1.note;
| FrameE (expr_opt, expr1) ->
Option.iter (valid_expr env) expr_opt;
valid_expr env expr1;
check_context source expr.note;
Option.iter (fun expr2 -> check_num source expr2.note) expr_opt;
check_match source expr1.note (varT "frame")
| LabelE (expr1, expr2) ->
valid_expr env expr1;
valid_expr env expr2;
check_context source expr.note;
check_num source expr1.note;
check_match source expr2.note (iterT (varT "instr") List)
| GetCurStateE | GetCurFrameE | GetCurLabelE | GetCurContextE ->
| GetCurStateE | GetCurContextE _ ->
check_context source expr.note
| IsCaseOfE (expr', _) | IsValidE expr' | HasTypeE (expr', _) ->
valid_expr env expr';
check_bool source expr.note;
| MatchE (expr1, expr2) ->
valid_expr env expr1;
valid_expr env expr2;
check_bool source expr.note;
| ContE expr1 ->
valid_expr env expr1;
check_match source expr.note (iterT (varT "instr") List);
check_match source expr1.note (varT "label");
| ChooseE expr1 ->
valid_expr env expr1;
check_list source expr1.note;
check_match source expr1.note (iterT expr.note List);
check_list source expr1.note; check_match source expr1.note (iterT expr.note List)
| IsDefinedE expr1 ->
valid_expr env expr1;
check_opt source expr1.note;
Expand Down
Loading

0 comments on commit 8bd084b

Please sign in to comment.