Skip to content

Commit

Permalink
Fix remaining bugs after merge with the GC proposal.
Browse files Browse the repository at this point in the history
  • Loading branch information
dhil committed Oct 18, 2023
1 parent 5e0e3f8 commit 8ce5b1f
Show file tree
Hide file tree
Showing 8 changed files with 203 additions and 198 deletions.
2 changes: 2 additions & 0 deletions interpreter/binary/decode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -189,6 +189,7 @@ let heap_type s =
| -0x14 -> I31HT
| -0x15 -> StructHT
| -0x16 -> ArrayHT
| -0x17 -> ContHT
| _ -> error s pos "malformed heap type"
)
] s
Expand All @@ -206,6 +207,7 @@ let ref_type s =
| -0x14 -> (Null, I31HT)
| -0x15 -> (Null, StructHT)
| -0x16 -> (Null, ArrayHT)
| -0x17 -> (Null, ContHT)
| -0x1c -> (NoNull, heap_type s)
| -0x1d -> (Null, heap_type s)
| _ -> error s pos "malformed reference type"
Expand Down
2 changes: 2 additions & 0 deletions interpreter/binary/encode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -125,6 +125,7 @@ struct
| NoFuncHT -> s7 (-0x0d)
| ExternHT -> s7 (-0x11)
| NoExternHT -> s7 (-0x0e)
| ContHT -> s7 (-0x17)
| VarHT x -> var_type s33 x
| DefHT _ | BotHT -> assert false

Expand All @@ -143,6 +144,7 @@ struct
| (Null, NoFuncHT) -> s7 (-0x0d)
| (Null, ExternHT) -> s7 (-0x11)
| (Null, NoExternHT) -> s7 (-0x0e)
| (Null, ContHT) -> s7 (-0x17)
| (Null, t) -> s7 (-0x1d); heap_type t
| (NoNull, t) -> s7 (-0x1c); heap_type t

Expand Down
22 changes: 17 additions & 5 deletions interpreter/exec/eval.ml
Original file line number Diff line number Diff line change
Expand Up @@ -177,6 +177,18 @@ let drop n (vs : 'a stack) at =

let split n (vs : 'a stack) at = take n vs at, drop n vs at

let str_type_of_heap_type (inst : module_inst) ht : str_type =
match ht with
| VarHT (StatX x | RecX x) -> str_type inst (x @@ Source.no_region)
| DefHT dt -> expand_def_type dt
| _ -> Printf.printf "HERE\n%!"; assert false

let func_type_of_cont_type (inst : module_inst) (ContT ht) : func_type =
as_func_str_type (str_type_of_heap_type inst ht)

let func_type_of_tag_type (inst : module_inst) (TagT ht) : func_type =
as_func_str_type (str_type_of_heap_type inst ht)


(* Evaluation *)

Expand Down Expand Up @@ -243,7 +255,7 @@ let rec step (c : config) : config =

| Throw x, vs ->
let tagt = tag c.frame.inst x in
let FuncT (ts, _) = as_func_tag_type (Tag.type_of tagt) in
let FuncT (ts, _) = func_type_of_tag_type c.frame.inst (Tag.type_of tagt) in
let vs0, vs' = split (Lib.List32.length ts) vs e.at in
vs', [Throwing (tagt, vs0) @@ e.at]

Expand Down Expand Up @@ -354,7 +366,7 @@ let rec step (c : config) : config =
| ContBind (x, y), Ref (ContRef ({contents = Some (n, ctxt)} as cont)) :: vs ->
let ct = cont_type c.frame.inst y in
let ct = subst_cont_type (subst_of c.frame.inst) ct in
let FuncT (ts', _) = as_func_cont_type ct in
let FuncT (ts', _) = func_type_of_cont_type c.frame.inst ct in
let args, vs' =
try split (Int32.sub n (Lib.List32.length ts')) vs e.at
with Failure _ -> Crash.error e.at "type mismatch at continuation bind"
Expand All @@ -365,7 +377,7 @@ let rec step (c : config) : config =

| Suspend x, vs ->
let tagt = tag c.frame.inst x in
let FuncT (ts, _) = as_func_tag_type (Tag.type_of tagt) in
let FuncT (ts, _) = func_type_of_tag_type c.frame.inst (Tag.type_of tagt) in
let args, vs' = split (Lib.List32.length ts) vs e.at in
vs', [Suspending (tagt, args, fun code -> code) @@ e.at]

Expand All @@ -389,7 +401,7 @@ let rec step (c : config) : config =

| ResumeThrow (x, y, xls), Ref (ContRef ({contents = Some (n, ctxt)} as cont)) :: vs ->
let tagt = tag c.frame.inst y in
let FuncT (ts, _) = as_func_tag_type (Tag.type_of tagt) in
let FuncT (ts, _) = func_type_of_tag_type c.frame.inst (Tag.type_of tagt) in
let hs = List.map (fun (x, l) -> tag c.frame.inst x, l) xls in
let args, vs' = split (Lib.List32.length ts) vs e.at in
cont := None;
Expand Down Expand Up @@ -1231,7 +1243,7 @@ let rec step (c : config) : config =

| Handle (Some hs, (vs', {it = Suspending (tagt, vs1, ctxt); at} :: es')), vs
when List.mem_assq tagt hs ->
let FuncT (_, ts) = as_func_tag_type (Tag.type_of tagt) in
let FuncT (_, ts) = func_type_of_tag_type c.frame.inst (Tag.type_of tagt) in
let ctxt' code = compose (ctxt code) (vs', es') in
[Ref (ContRef (ref (Some (Lib.List32.length ts, ctxt'))))] @ vs1 @ vs,
[Plain (Br (List.assq tagt hs)) @@ e.at]
Expand Down
1 change: 1 addition & 0 deletions interpreter/syntax/free.ml
Original file line number Diff line number Diff line change
Expand Up @@ -81,6 +81,7 @@ let heap_type = function
| I31HT | StructHT | ArrayHT -> empty
| FuncHT | NoFuncHT -> empty
| ExternHT | NoExternHT -> empty
| ContHT -> empty
| VarHT x -> var_type x
| DefHT _ct -> empty (* assume closed *)
| BotHT -> empty
Expand Down
18 changes: 3 additions & 15 deletions interpreter/syntax/types.ml
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ type heap_type =
| AnyHT | NoneHT | EqHT | I31HT | StructHT | ArrayHT
| FuncHT | NoFuncHT
| ExternHT | NoExternHT
| ContHT
| VarHT of var
| DefHT of def_type
| BotHT
Expand Down Expand Up @@ -149,6 +150,7 @@ let subst_heap_type s = function
| NoFuncHT -> NoFuncHT
| ExternHT -> ExternHT
| NoExternHT -> NoExternHT
| ContHT -> ContHT
| VarHT x -> s x
| DefHT dt -> DefHT dt (* assume closed *)
| BotHT -> BotHT
Expand Down Expand Up @@ -277,7 +279,6 @@ let unpacked_storage_type = function

let unpacked_field_type (FieldT (_mut, t)) = unpacked_storage_type t


let as_func_str_type (st : str_type) : func_type =
match st with
| DefFuncT ft -> ft
Expand All @@ -288,17 +289,6 @@ let as_cont_str_type (dt : str_type) : cont_type =
| DefContT ct -> ct
| _ -> assert false

let as_func_heap_type (ht : heap_type) : func_type =
match ht with
| DefHT dt -> as_func_str_type (expand_def_type dt)
| _ -> assert false

let as_func_cont_type (ContT ct) : func_type =
as_func_heap_type ct

let as_func_tag_type (TagT et) : func_type =
as_func_heap_type et

let as_struct_str_type (st : str_type) : struct_type =
match st with
| DefStructT st -> st
Expand All @@ -309,9 +299,6 @@ let as_array_str_type (st : str_type) : array_type =
| DefArrayT at -> at
| _ -> assert false

let as_heap_str_type (st : str_type) : heap_type =
DefHT (DefT (RecT [SubT (Final, [], st)], Int32.of_int 0))

let extern_type_of_import_type (ImportT (et, _, _)) = et
let extern_type_of_export_type (ExportT (et, _)) = et

Expand Down Expand Up @@ -372,6 +359,7 @@ let rec string_of_heap_type = function
| NoFuncHT -> "nofunc"
| ExternHT -> "extern"
| NoExternHT -> "noextern"
| ContHT -> "cont"
| VarHT x -> string_of_var x
| DefHT dt -> "(" ^ string_of_def_type dt ^ ")"
| BotHT -> "something"
Expand Down
6 changes: 5 additions & 1 deletion interpreter/valid/match.ml
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ let lookup c x = Lib.List32.nth c x
let abs_of_str_type _c = function
| DefStructT _ | DefArrayT _ -> StructHT
| DefFuncT _ -> FuncHT
| DefContT _ -> assert false (* TODO(dhil): should we add an abstract ContHT? *)
| DefContT _ -> ContHT

let rec top_of_str_type c st =
top_of_heap_type c (abs_of_str_type c st)
Expand All @@ -22,6 +22,7 @@ and top_of_heap_type c = function
| AnyHT | NoneHT | EqHT | StructHT | ArrayHT | I31HT -> AnyHT
| FuncHT | NoFuncHT -> FuncHT
| ExternHT | NoExternHT -> ExternHT
| ContHT -> ContHT
| DefHT dt -> top_of_str_type c (expand_def_type dt)
| VarHT (StatX x) -> top_of_str_type c (expand_def_type (lookup c x))
| VarHT (RecX _) | BotHT -> assert false
Expand All @@ -33,6 +34,7 @@ and bot_of_heap_type c = function
| AnyHT | NoneHT | EqHT | StructHT | ArrayHT | I31HT -> NoneHT
| FuncHT | NoFuncHT -> NoFuncHT
| ExternHT | NoExternHT -> NoExternHT
| ContHT -> ContHT
| DefHT dt -> bot_of_str_type c (expand_def_type dt)
| VarHT (StatX x) -> bot_of_str_type c (expand_def_type (lookup c x))
| VarHT (RecX _) | BotHT -> assert false
Expand Down Expand Up @@ -73,6 +75,7 @@ let rec match_heap_type c t1 t2 =
| NoneHT, t -> match_heap_type c t AnyHT
| NoFuncHT, t -> match_heap_type c t FuncHT
| NoExternHT, t -> match_heap_type c t ExternHT
| ContHT, t -> match_heap_type c t ContHT
| VarHT (StatX x1), _ -> match_heap_type c (DefHT (lookup c x1)) t2
| _, VarHT (StatX x2) -> match_heap_type c t1 (DefHT (lookup c x2))
| DefHT dt1, DefHT dt2 -> match_def_type c dt1 dt2
Expand All @@ -85,6 +88,7 @@ let rec match_heap_type c t1 t2 =
| DefArrayT _, EqHT -> true
| DefArrayT _, ArrayHT -> true
| DefFuncT _, FuncHT -> true
| DefContT _, ContHT -> true
| _ -> false
)
| BotHT, _ -> true
Expand Down
98 changes: 47 additions & 51 deletions interpreter/valid/valid.ml
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,7 @@ let func_type (c : context) x =
let cont_type (c : context) x =
match expand_def_type (type_ c x) with
| DefContT ct -> ct
| _ -> error x.at ("non-continuation type " ^ Int32.to_string x.it)
| _ as t -> Printf.printf "%s\n%!" (string_of_str_type t); error x.at ("non-continuation type " ^ Int32.to_string x.it)

let struct_type (c : context) x =
match expand_def_type (type_ c x) with
Expand All @@ -86,20 +86,35 @@ let array_type (c : context) x =
| DefArrayT at -> at
| _ -> error x.at ("non-array type " ^ I32.to_string_u x.it)

let tag_type (c : context) x =
let TagT ht = tag c x in
match ht with
| DefHT dt -> TagT (DefHT dt)
| VarHT (StatX y) -> TagT (as_heap_str_type (DefFuncT (func_type c (y @@ x.at))))
| _ -> assert false

let refer category (s : Free.Set.t) x =
if not (Free.Set.mem x.it s) then
error x.at
("undeclared " ^ category ^ " reference " ^ I32.to_string_u x.it)

let refer_func (c : context) x = refer "function" c.refs.Free.funcs x

(* Conversions *)

let cont_type_of_heap_type (c : context) (ht : heap_type) at : cont_type =
match ht with
| DefHT dt -> as_cont_str_type (expand_def_type dt)
| VarHT (RecX x | StatX x) -> cont_type c (x @@ at)
| _ -> assert false

let func_type_of_heap_type (c : context) (ht : heap_type) at : func_type =
match ht with
| DefHT dt -> as_func_str_type (expand_def_type dt)
| VarHT (RecX x | StatX x) -> func_type c (x @@ at)
| _ -> assert false

let func_type_of_cont_type (c : context) (ContT ht) at : func_type =
func_type_of_heap_type c ht at

let func_type_of_tag_type (c : context) (TagT ht) at : func_type =
func_type_of_heap_type c ht at

let heap_type_of_str_type (_c : context) (st : str_type) : heap_type =
DefHT (DefT (RecT [SubT (Final, [], st)], Int32.of_int 0))

(* Types *)

Expand All @@ -122,10 +137,11 @@ let check_heap_type (c : context) (t : heap_type) at =
match t with
| AnyHT | NoneHT | EqHT | I31HT | StructHT | ArrayHT
| FuncHT | NoFuncHT
| ExternHT | NoExternHT -> ()
| ExternHT | NoExternHT
| ContHT -> ()
| VarHT (StatX x) -> let _dt = type_ c (x @@ at) in ()
| VarHT (RecX _) -> assert false
| DefHT _ -> ()
| DefHT _ -> assert false
| BotHT -> ()

let check_ref_type (c : context) (t : ref_type) at =
Expand Down Expand Up @@ -404,32 +420,13 @@ let check_memop (c : context) (memop : ('t, 's) memop) ty_size get_sz at =
*)

let check_resume_table (c : context) ts2 (xys : (idx * idx) list) at =
let is_heap_cont_type = function
| VarHT (StatX x) ->
(try ignore(cont_type c (x @@ at)); true with _ -> false)
| DefHT dt ->
(match expand_def_type dt with
| DefContT _ -> true
| _ -> false)
| _ -> false
in
let extract_cont_heap_type = function
| VarHT (StatX x) ->
let ContT ht = cont_type c (x @@ at) in
ht
| DefHT dt ->
(match expand_def_type dt with
| DefContT (ContT ht) -> ht
| _ -> assert false)
| _ -> assert false
in
List.iter (fun (x1, x2) ->
let FuncT (ts3, ts4) = as_func_tag_type (tag_type c x1) in
let FuncT (ts3, ts4) = func_type_of_tag_type c (tag c x1) x1.at in
let (_, ts') = label c x2 in
match Lib.List.last_opt ts' with
| Some (RefT (nul', ht)) when is_heap_cont_type ht ->
let ht' = extract_cont_heap_type ht in
let ft' = as_func_heap_type ht' in
| Some (RefT (nul', ht)) ->
let ct = cont_type_of_heap_type c ht x2.at in
let ft' = func_type_of_cont_type c ct x2.at in
require (match_func_type c.types (FuncT (ts4, ts2)) ft') x2.at
"type mismatch in continuation type";
check_stack c (ts3 @ [RefT (nul', ht)]) ts' x2.at
Expand Down Expand Up @@ -487,9 +484,8 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
(ts1 @ [NumT I32T]) --> ts2, List.map (fun x -> x @@ e.at) xs

| Throw x ->
let tag = tag_type c x in
check_tag_type c tag e.at;
let FuncT (ts1, _) = as_func_tag_type tag in
let tag = tag c x in
let FuncT (ts1, _) = func_type_of_tag_type c tag x.at in
ts1 -->... [], []

| Rethrow x ->
Expand Down Expand Up @@ -624,41 +620,41 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in

| ContNew x ->
let ct = cont_type c x in
let ft = as_func_cont_type ct in
[RefT (Null, as_heap_str_type (DefFuncT ft))] -->
let ft = func_type_of_cont_type c ct x.at in
[RefT (Null, heap_type_of_str_type c (DefFuncT ft))] -->
[RefT (NoNull, DefHT (type_ c x))], []

| ContBind (x, y) ->
let ct = cont_type c x in
let FuncT (ts1, ts2) = as_func_cont_type ct in
let FuncT (ts1, ts2) = func_type_of_cont_type c ct x.at in
let ct' = cont_type c y in
let FuncT (ts1', _) as ft' = as_func_cont_type ct' in
let FuncT (ts1', _) as ft' = func_type_of_cont_type c ct' y.at in
require (List.length ts1 >= List.length ts1') x.at
"type mismatch in continuation arguments";
let ts11, ts12 = Lib.List.split (List.length ts1 - List.length ts1') ts1 in
require (match_func_type c.types (FuncT (ts12, ts2)) ft') e.at
"type mismatch in continuation types";
(ts11 @ [RefT (Null, as_heap_str_type (DefContT ct))]) -->
[RefT (NoNull, as_heap_str_type (DefContT ct'))], []
(ts11 @ [RefT (Null, heap_type_of_str_type c (DefContT ct))]) -->
[RefT (NoNull, heap_type_of_str_type c (DefContT ct'))], []

| Suspend x ->
let tag = tag_type c x in
let FuncT (ts1, ts2) = as_func_tag_type tag in
let tag = tag c x in
let FuncT (ts1, ts2) = func_type_of_tag_type c tag x.at in
ts1 --> ts2, []

| Resume (x, xys) ->
let ct = cont_type c x in
let FuncT (ts1, ts2) = as_func_cont_type ct in
let FuncT (ts1, ts2) = func_type_of_cont_type c ct x.at in
check_resume_table c ts2 xys e.at;
(ts1 @ [RefT (Null, as_heap_str_type (DefContT ct))]) --> ts2, []
(ts1 @ [RefT (Null, heap_type_of_str_type c (DefContT ct))]) --> ts2, []

| ResumeThrow (x, y, xys) ->
let ct = cont_type c x in
let FuncT (ts1, ts2) = as_func_cont_type ct in
let tag = tag_type c y in
let FuncT (ts0, _) = as_func_tag_type tag in
let FuncT (ts1, ts2) = func_type_of_cont_type c ct x.at in
let tag = tag c y in
let FuncT (ts0, _) = func_type_of_tag_type c tag y.at in
check_resume_table c ts2 xys e.at;
(ts0 @ [RefT (Null, as_heap_str_type (DefContT ct))]) --> ts2, []
(ts0 @ [RefT (Null, heap_type_of_str_type c (DefContT ct))]) --> ts2, []

| Barrier (bt, es) ->
let InstrT (ts1, ts2, xs) as ft = check_block_type c bt e.at in
Expand Down Expand Up @@ -1038,7 +1034,7 @@ and check_block (c : context) (es : instr list) (it : instr_type) at =

and check_catch (ct : idx * instr list) (c : context) (ft : instr_type) at =
let (x, es) = ct in
let FuncT (ts1, _) = as_func_tag_type (tag_type c x) in
let FuncT (ts1, _) = func_type_of_tag_type c (tag c x) x.at in
let InstrT (_, ts2, xs) = ft in
check_block c es (InstrT (ts1, ts2, xs)) at

Expand Down
Loading

0 comments on commit 8ce5b1f

Please sign in to comment.