Skip to content

Commit

Permalink
simplify block_type type by constraining the type with as instead of
Browse files Browse the repository at this point in the history
having two type parameter
  • Loading branch information
zapashcanon committed Nov 22, 2023
1 parent f7e6a6c commit ee0a6a9
Show file tree
Hide file tree
Showing 12 changed files with 37 additions and 49 deletions.
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

0 comments on commit ee0a6a9

Please sign in to comment.