Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

simplify block_type type by constraining the type with as instead of having two type parameter #77

Merged
merged 1 commit into from
Nov 22, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/assigned.ml
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ type t =
; global : (Text.global, simplified global_type) Runtime.t Named.t
; table : (simplified table, simplified table_type) Runtime.t Named.t
; mem : (mem, limits) Runtime.t Named.t
; func : (text func, (text, text) block_type) Runtime.t Named.t
; func : (text func, text block_type) Runtime.t Named.t
; elem : Text.elem Named.t
; data : Text.data Named.t
; exports : Grouped.opt_exports
Expand Down
2 changes: 1 addition & 1 deletion src/assigned.mli
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ type t =
; global : (Text.global, simplified global_type) Runtime.t Named.t
; table : (simplified table, simplified table_type) Runtime.t Named.t
; mem : (Types.mem, Types.limits) Runtime.t Named.t
; func : (text func, (text, text) block_type) Runtime.t Named.t
; func : (text func, text block_type) Runtime.t Named.t
; elem : Text.elem Named.t
; data : Text.data Named.t
; exports : Grouped.opt_exports
Expand Down
4 changes: 2 additions & 2 deletions src/grouped.ml
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ type t =
; global : (Text.global, simplified global_type) Runtime.t Indexed.t list
; table : (simplified table, simplified table_type) Runtime.t Indexed.t list
; mem : (mem, limits) Runtime.t Indexed.t list
; func : (text func, (text, text) block_type) Runtime.t Indexed.t list
; func : (text func, text block_type) Runtime.t Indexed.t list
; elem : Text.elem Indexed.t list
; data : Text.data Indexed.t list
; exports : opt_exports
Expand Down Expand Up @@ -189,7 +189,7 @@ let of_symbolic (modul : Text.modul) : t Result.t =
( { fields with func; function_type; type_checks }
, { curr with func = succ curr.func } )
| MImport ({ desc = Import_func (a, b); _ } as import) ->
let imported : (text, text) block_type Imported.t = imp import (a, b) in
let imported : text block_type Imported.t = imp import (a, b) in
ok @@ add_func (Imported imported) fields curr
| MExport { name; desc = Export_func id } ->
let id = curr_id curr.func id in
Expand Down
2 changes: 1 addition & 1 deletion src/grouped.mli
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ type t =
; global : (Text.global, simplified global_type) Runtime.t Indexed.t list
; table : (simplified table, simplified table_type) Runtime.t Indexed.t list
; mem : (mem, Types.limits) Runtime.t Indexed.t list
; func : (text func, (text, text) block_type) Runtime.t Indexed.t list
; func : (text func, text block_type) Runtime.t Indexed.t list
; elem : Text.elem Indexed.t list
; data : Text.data Indexed.t list
; exports : opt_exports
Expand Down
6 changes: 2 additions & 4 deletions src/interpret.ml
Original file line number Diff line number Diff line change
Expand Up @@ -687,7 +687,7 @@ module Make (P : Interpret_functor_intf.P) :
end

let exec_block (state : State.exec_state) ~is_loop
(bt : (simplified, simplified) block_type option) expr =
(bt : simplified block_type option) expr =
let pt, rt =
match bt with
| None -> ([], [])
Expand Down Expand Up @@ -772,9 +772,7 @@ module Make (P : Interpret_functor_intf.P) :
(* exec_vfunc ~return state func *)

let call_indirect ~return (state : State.exec_state)
( tbl_i
, (Bt_raw ((None | Some _), typ_i) : (simplified, simplified) block_type) )
=
(tbl_i, (Bt_raw ((None | Some _), typ_i) : simplified block_type)) =
let fun_i, stack = Stack.pop_i32 state.stack in
let state = { state with stack } in
let/ t = Env.get_table state.env tbl_i in
Expand Down
4 changes: 2 additions & 2 deletions src/link.ml
Original file line number Diff line number Diff line change
Expand Up @@ -175,8 +175,8 @@ let func_types_are_compatible a b =
in
remove_param a = remove_param b

let load_func (ls : 'f state)
(import : (simplified, simplified) block_type Imported.t) : func Result.t =
let load_func (ls : 'f state) (import : simplified block_type Imported.t) :
func Result.t =
let (Bt_raw ((None | Some _), typ)) = import.desc in
let* func = load_from_module ls (fun (e : exports) -> e.functions) import in
let type' =
Expand Down
15 changes: 5 additions & 10 deletions src/rewrite.ml
Original file line number Diff line number Diff line change
Expand Up @@ -70,8 +70,7 @@ let rewrite_expr (modul : Assigned.t) (locals : simplified param list)
else Ok (Raw id)
in

let bt_some_to_raw :
(text, text) block_type -> (simplified, simplified) block_type Result.t =
let bt_some_to_raw : text block_type -> simplified block_type Result.t =
function
| Bt_ind ind -> begin
let* v = get "unknown type" modul.typ (Some ind) in
Expand All @@ -96,8 +95,7 @@ let rewrite_expr (modul : Assigned.t) (locals : simplified param list)
in

let bt_to_raw :
(text, text) block_type option
-> (simplified, simplified) block_type option Result.t = function
text block_type option -> simplified block_type option Result.t = function
| None -> Ok None
| Some bt ->
let+ raw = bt_some_to_raw bt in
Expand Down Expand Up @@ -398,9 +396,8 @@ let rewrite_const_expr (modul : Assigned.t) (expr : text expr) :
in
list_map const_instr expr

let rewrite_block_type (modul : Assigned.t)
(block_type : (text, text) block_type) :
(simplified, simplified) block_type Result.t =
let rewrite_block_type (modul : Assigned.t) (block_type : text block_type) :
simplified block_type Result.t =
match block_type with
| Bt_ind id -> begin
let* v = get "unknown type" modul.typ (Some id) in
Expand Down Expand Up @@ -519,9 +516,7 @@ let modul (modul : Assigned.t) : Simplified.modul Result.t =
let* elem = rewrite_named (rewrite_elem modul) modul.elem in
let* data = rewrite_named (rewrite_data modul) modul.data in
let* exports = rewrite_exports modul modul.exports in
let* (func :
(simplified func, (simplified, simplified) block_type) Runtime.t
Named.t ) =
let* (func : (simplified func, simplified block_type) Runtime.t Named.t) =
let import = rewrite_import (rewrite_block_type modul) in
let runtime = rewrite_runtime (rewrite_func modul) import in
rewrite_named runtime modul.func
Expand Down
3 changes: 1 addition & 2 deletions src/simplified.ml
Original file line number Diff line number Diff line change
Expand Up @@ -52,8 +52,7 @@ type modul =
; global : (global, simplified global_type) Runtime.t Named.t
; table : (simplified table, simplified table_type) Runtime.t Named.t
; mem : (mem, limits) Runtime.t Named.t
; func :
(simplified func, (simplified, simplified) block_type) Runtime.t Named.t
; func : (simplified func, simplified block_type) Runtime.t Named.t
(* TODO: switch to func_type *)
; elem : elem Named.t
; data : data Named.t
Expand Down
4 changes: 2 additions & 2 deletions src/symbolic_memory.ml
Original file line number Diff line number Diff line change
Expand Up @@ -94,10 +94,10 @@ module M = struct
| Extract (e1, h, m1), Extract (e2, m2, l) ->
merge_extracts (e1, h, m1) (e2, m2, l)
| Extract (e1, h, m1), Concat ({ e = Extract (e2, m2, l); _ }, e3) ->
let ty: Ty.t = if offset >= 4 then Ty_bitv S64 else Ty_bitv S32 in
let ty : Ty.t = if offset >= 4 then Ty_bitv S64 else Ty_bitv S32 in
Concat (merge_extracts (e1, h, m1) (e2, m2, l), e3) @: ty
| _ ->
let ty: Ty.t = if offset >= 4 then Ty_bitv S64 else Ty_bitv S32 in
let ty : Ty.t = if offset >= 4 then Ty_bitv S64 else Ty_bitv S32 in
Concat (msb, lsb) @: ty

let loadn m a n : int32 =
Expand Down
16 changes: 6 additions & 10 deletions src/typecheck.ml
Original file line number Diff line number Diff line change
Expand Up @@ -39,8 +39,7 @@ module Env = struct
{ locals : typ Index.Map.t
; globals : (global, simplified global_type) Runtime.t Named.t
; result_type : simplified result_type
; funcs :
(simplified func, (simplified, simplified) block_type) Runtime.t Named.t
; funcs : (simplified func, simplified block_type) Runtime.t Named.t
; blocks : typ list list
; tables : (simplified table, simplified table_type) Runtime.t Named.t
; elems : elem Named.t
Expand Down Expand Up @@ -129,7 +128,7 @@ module Stack : sig

val push : t -> t -> t Result.t

val pop_push : (simplified, simplified) block_type option -> t -> t Result.t
val pop_push : simplified block_type option -> t -> t Result.t

val pop_ref : t -> t Result.t

Expand Down Expand Up @@ -226,7 +225,7 @@ end = struct

let push t stack = ok @@ t @ stack

let pop_push (bt : (simplified, simplified) block_type option) stack =
let pop_push (bt : simplified block_type option) stack =
match bt with
| None -> Ok stack
| Some (Bt_raw ((None | Some _), (pt, rt))) ->
Expand Down Expand Up @@ -494,15 +493,12 @@ let rec typecheck_instr (env : env) (stack : stack) (instr : simplified instr) :
Log.debug "TODO (typecheck instr) %a" Types.Pp.instr i;
Ok stack

and typecheck_expr env expr ~is_loop
(block_type : (simplified, simplified) block_type option)
and typecheck_expr env expr ~is_loop (block_type : simplified block_type option)
~stack:previous_stack : stack Result.t =
let pt, rt =
Option.fold ~none:([], [])
~some:(fun
(Bt_raw ((None | Some _), (pt, rt)) :
(simplified, simplified) block_type )
-> (List.rev_map typ_of_pt pt, List.rev_map typ_of_val_type rt) )
~some:(fun (Bt_raw ((None | Some _), (pt, rt)) : simplified block_type) ->
(List.rev_map typ_of_pt pt, List.rev_map typ_of_val_type rt) )
block_type
in
let jump_type = if is_loop then pt else rt in
Expand Down
24 changes: 12 additions & 12 deletions src/types.ml
Original file line number Diff line number Diff line change
Expand Up @@ -227,13 +227,13 @@ let pp_result_ fmt vt = pp fmt "(result %a)" pp_val_type vt
let pp_result_type fmt results = pp_list ~pp_sep:pp_space pp_result_ fmt results

(* TODO: add a third case that only has (pt * rt) and is the only one used in simplified *)
type ('a, _) block_type =
| Bt_ind : 'a indice -> ('a, < with_ind_bt ; .. >) block_type
type 'a block_type =
| Bt_ind : 'a indice -> (< with_ind_bt ; .. > as 'a) block_type
| Bt_raw :
('a indice option * ('a param_type * 'a result_type))
-> ('a, < .. >) block_type
-> (< .. > as 'a) block_type

let pp_block_type (type kind) fmt : (kind, kind) block_type -> unit = function
let pp_block_type (type kind) fmt : kind block_type -> unit = function
| Bt_ind ind -> pp fmt "(type %a)" pp_indice ind
| Bt_raw (_ind, (pt, rt)) -> pp fmt "%a %a" pp_param_type pt pp_result_type rt

Expand Down Expand Up @@ -328,9 +328,9 @@ type 'a instr =
(* Control instructions *)
| Nop
| Unreachable
| Block of string option * ('a, 'a) block_type option * 'a expr
| Loop of string option * ('a, 'a) block_type option * 'a expr
| If_else of string option * ('a, 'a) block_type option * 'a expr * 'a expr
| Block of string option * 'a block_type option * 'a expr
| Loop of string option * 'a block_type option * 'a expr
| If_else of string option * 'a block_type option * 'a expr * 'a expr
| Br of 'a indice
| Br_if of 'a indice
| Br_table of 'a indice array * 'a indice
Expand All @@ -340,10 +340,10 @@ type 'a instr =
| Br_on_null of 'a indice
| Return
| Return_call of 'a indice
| Return_call_indirect of 'a indice * ('a, 'a) block_type
| Return_call_ref of ('a, 'a) block_type
| Return_call_indirect of 'a indice * 'a block_type
| Return_call_ref of 'a block_type
| Call of 'a indice
| Call_indirect of 'a indice * ('a, 'a) block_type
| Call_indirect of 'a indice * 'a block_type
| Call_ref of 'a indice
(* Array instructions *)
| Array_get of 'a indice
Expand Down Expand Up @@ -373,7 +373,7 @@ and 'a expr = 'a instr list
(* TODO: func and expr should also be parametrised on block type:
using (param_type, result_type) M.block_type before simplify and directly an indice after *)
type 'a func =
{ type_f : ('a, 'a) block_type
{ type_f : 'a block_type
; locals : 'a param list
; body : 'a expr
; id : string option
Expand All @@ -386,7 +386,7 @@ type 'a table = string option * 'a table_type
(* Modules *)

type 'a import_desc =
| Import_func of string option * ('a, 'a) block_type
| Import_func of string option * 'a block_type
| Import_table of string option * 'a table_type
| Import_mem of string option * limits
| Import_global of string option * 'a global_type
Expand Down
4 changes: 2 additions & 2 deletions test/fuzz/env.ml
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,8 @@ type t =
; mutable tables : (string * text table_type) list
; mutable globals : (string * text global_type) list
; mutable locals : (string * text val_type) list
; mutable blocks : (block_kind * string * (text, text) block_type) list
; mutable funcs : (string * (text, text) block_type) list
; mutable blocks : (block_kind * string * text block_type) list
; mutable funcs : (string * text block_type) list
; mutable fuel : int
}

Expand Down
Loading