From 538c851277df25a5801113591f44dce29cc2d29c Mon Sep 17 00:00:00 2001 From: Ben Visness Date: Thu, 17 Oct 2024 12:09:40 +0200 Subject: [PATCH] Update "index type" to "address type" in the spec interpreter --- interpreter/binary/decode.ml | 6 +- interpreter/binary/encode.ml | 10 +-- interpreter/exec/eval.ml | 8 +-- interpreter/host/spectest.ml | 6 +- interpreter/runtime/memory.ml | 18 ++--- interpreter/runtime/memory.mli | 2 +- interpreter/runtime/table.ml | 22 +++--- interpreter/runtime/table.mli | 2 +- interpreter/runtime/value.ml | 8 +-- interpreter/syntax/free.ml | 4 +- interpreter/syntax/types.ml | 26 ++++---- interpreter/text/arrange.ml | 10 +-- interpreter/text/parser.mly | 52 +++++++-------- interpreter/valid/match.ml | 8 +-- interpreter/valid/valid.ml | 118 ++++++++++++++++----------------- 15 files changed, 150 insertions(+), 150 deletions(-) diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml index 4ca94d68b..920d9841d 100644 --- a/interpreter/binary/decode.ml +++ b/interpreter/binary/decode.ml @@ -289,11 +289,11 @@ let limits uN s = let table_type s = let t = ref_type s in let lim, is64 = limits u64 s in - TableT (lim, (if is64 then I64IndexType else I32IndexType), t) + TableT (lim, (if is64 then I64AddressType else I32AddressType), t) let memory_type s = let lim, is64 = limits u64 s in - MemoryT (lim, if is64 then I64IndexType else I32IndexType) + MemoryT (lim, if is64 then I64AddressType else I32AddressType) let global_type s = let t = val_type s in @@ -1099,7 +1099,7 @@ let table s = ); (fun s -> let at = region s (pos s) (pos s) in - let TableT (_, _it, (_, ht)) as ttype = table_type s in + let TableT (_, _at, (_, ht)) as ttype = table_type s in {ttype; tinit = [RefNull ht @@ at] @@ at} ); ] s diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml index aca2a5454..d6cb3db6c 100644 --- a/interpreter/binary/encode.ml +++ b/interpreter/binary/encode.ml @@ -194,15 +194,15 @@ struct | RecT [st] -> sub_type st | RecT sts -> s7 (-0x32); vec sub_type sts - let limits vu {min; max} it = - let flags = flag (max <> None) 0 + flag (it = I64IndexType) 2 in + let limits vu {min; max} at = + let flags = flag (max <> None) 0 + flag (at = I64AddressType) 2 in byte flags; vu min; opt vu max let table_type = function - | TableT (lim, it, t) -> ref_type t; limits u64 lim it + | TableT (lim, at, t) -> ref_type t; limits u64 lim at let memory_type = function - | MemoryT (lim, it) -> limits u64 lim it + | MemoryT (lim, at) -> limits u64 lim at let global_type = function | GlobalT (mut, t) -> val_type t; mutability mut @@ -972,7 +972,7 @@ struct let table tab = let {ttype; tinit} = tab.it in match ttype, tinit.it with - | TableT (_, _it, (_, ht1)), [{it = RefNull ht2; _}] when ht1 = ht2 -> + | TableT (_, _at, (_, ht1)), [{it = RefNull ht2; _}] when ht1 = ht2 -> table_type ttype | _ -> op 0x40; op 0x00; table_type ttype; const tinit diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index 2d632dc9f..a68114c7c 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -385,7 +385,7 @@ let rec step (c : config) : config = | TableSize x, vs -> let tab = table c.frame.inst x in - value_of_index (Table.index_type_of tab) (Table.size (table c.frame.inst x)) :: vs, [] + value_of_address (Table.address_type_of tab) (Table.size (table c.frame.inst x)) :: vs, [] | TableGrow x, Num delta :: Ref r :: vs' -> let tab = table c.frame.inst x in @@ -393,7 +393,7 @@ let rec step (c : config) : config = let result = try Table.grow tab (Table.index_of_num delta) r; old_size with Table.SizeOverflow | Table.SizeLimit | Table.OutOfMemory -> -1L - in (value_of_index (Table.index_type_of tab) result) :: vs', [] + in (value_of_address (Table.address_type_of tab) result) :: vs', [] | TableFill x, Num n :: Ref r :: Num i :: vs' -> let n_64 = Table.index_of_num n in @@ -552,7 +552,7 @@ let rec step (c : config) : config = | MemorySize x, vs -> let mem = memory c.frame.inst x in - value_of_index (Memory.index_type_of mem) (Memory.size mem) :: vs, [] + value_of_address (Memory.address_type_of mem) (Memory.size mem) :: vs, [] | MemoryGrow x, Num delta :: vs' -> let mem = memory c.frame.inst x in @@ -560,7 +560,7 @@ let rec step (c : config) : config = let result = try Memory.grow mem (Memory.address_of_num delta); old_size with Memory.SizeOverflow | Memory.SizeLimit | Memory.OutOfMemory -> -1L - in (value_of_index (Memory.index_type_of mem) result) :: vs', [] + in (value_of_address (Memory.address_type_of mem) result) :: vs', [] | MemoryFill x, Num n :: Num k :: Num i :: vs' -> let n_64 = Memory.address_of_num n in diff --git a/interpreter/host/spectest.ml b/interpreter/host/spectest.ml index 0ab23ec4c..5eb0ca3db 100644 --- a/interpreter/host/spectest.ml +++ b/interpreter/host/spectest.ml @@ -20,15 +20,15 @@ let global (GlobalT (_, t) as gt) = in ExternGlobal (Global.alloc gt v) let table = - let tt = TableT ({min = 10L; max = Some 20L}, I32IndexType, (Null, FuncHT)) in + let tt = TableT ({min = 10L; max = Some 20L}, I32AddressType, (Null, FuncHT)) in ExternTable (Table.alloc tt (NullRef FuncHT)) let table64 = - let tt = TableT ({min = 10L; max = Some 20L}, I64IndexType, (Null, FuncHT)) in + let tt = TableT ({min = 10L; max = Some 20L}, I64AddressType, (Null, FuncHT)) in ExternTable (Table.alloc tt (NullRef FuncHT)) let memory = - let mt = MemoryT ({min = 1L; max = Some 2L}, I32IndexType) in + let mt = MemoryT ({min = 1L; max = Some 2L}, I32AddressType) in ExternMemory (Memory.alloc mt) let func f ft = diff --git a/interpreter/runtime/memory.ml b/interpreter/runtime/memory.ml index 03571a730..afd750057 100644 --- a/interpreter/runtime/memory.ml +++ b/interpreter/runtime/memory.ml @@ -25,8 +25,8 @@ let valid_limits {min; max} = | None -> true | Some m -> I64.le_u min m -let create n it = - if I64.gt_u n 0x10000L && it = I32IndexType then raise SizeOverflow else +let create n at = + if I64.gt_u n 0x10000L && at = I32AddressType then raise SizeOverflow else try let size = Int64.(mul n page_size) in let mem = Array1_64.create Int8_unsigned C_layout size in @@ -34,10 +34,10 @@ let create n it = mem with Out_of_memory -> raise OutOfMemory -let alloc (MemoryT (lim, it) as ty) = +let alloc (MemoryT (lim, at) as ty) = assert Free.((memory_type ty).types = Set.empty); if not (valid_limits lim) then raise Type; - {ty; content = create lim.min it} + {ty; content = create lim.min at} let bound mem = Array1_64.dim mem.content @@ -48,8 +48,8 @@ let size mem = let type_of mem = mem.ty -let index_type_of mem = - let (MemoryT (_, it)) = type_of mem in it +let address_type_of mem = + let (MemoryT (_, at)) = type_of mem in at let address_of_num x = match x with @@ -63,17 +63,17 @@ let address_of_value x = | _ -> raise Type let grow mem delta = - let MemoryT (lim, it) = mem.ty in + let MemoryT (lim, at) = mem.ty in assert (lim.min = size mem); let old_size = lim.min in let new_size = Int64.add old_size delta in if I64.gt_u old_size new_size then raise SizeOverflow else let lim' = {lim with min = new_size} in if not (valid_limits lim') then raise SizeLimit else - let after = create new_size (index_type_of mem) in + let after = create new_size (address_type_of mem) in let dim = Array1_64.dim mem.content in Array1.blit (Array1_64.sub mem.content 0L dim) (Array1_64.sub after 0L dim); - mem.ty <- MemoryT (lim', it); + mem.ty <- MemoryT (lim', at); mem.content <- after let load_byte mem a = diff --git a/interpreter/runtime/memory.mli b/interpreter/runtime/memory.mli index ab06999d3..eb7278fcf 100644 --- a/interpreter/runtime/memory.mli +++ b/interpreter/runtime/memory.mli @@ -19,7 +19,7 @@ val page_size : int64 val alloc : memory_type -> memory (* raises Type, SizeOverflow, OutOfMemory *) val type_of : memory -> memory_type -val index_type_of : memory -> index_type +val address_type_of : memory -> address_type val size : memory -> size val bound : memory -> address val address_of_value : value -> address diff --git a/interpreter/runtime/table.ml b/interpreter/runtime/table.ml index 0db065c90..a7eb48531 100644 --- a/interpreter/runtime/table.ml +++ b/interpreter/runtime/table.ml @@ -19,16 +19,16 @@ let valid_limits {min; max} = | None -> true | Some m -> I64.le_u min m -let valid_index it i = - match it with - | I32IndexType -> I64.le_u i 0xffff_ffffL - | I64IndexType -> true +let valid_index at i = + match at with + | I32AddressType -> I64.le_u i 0xffff_ffffL + | I64AddressType -> true let create size r = try Lib.Array64.make size r with Out_of_memory | Invalid_argument _ -> raise OutOfMemory -let alloc (TableT (lim, it, t) as ty) r = +let alloc (TableT (lim, at, t) as ty) r = assert Free.((ref_type t).types = Set.empty); if not (valid_limits lim) then raise Type; {ty; content = create lim.min r} @@ -39,8 +39,8 @@ let size tab = let type_of tab = tab.ty -let index_type_of tab = - let (TableT (_, it, _)) = type_of tab in it +let address_type_of tab = + let (TableT (_, at, _)) = type_of tab in at let index_of_num x = match x with @@ -49,17 +49,17 @@ let index_of_num x = | _ -> raise Type let grow tab delta r = - let TableT (lim, it, t) = tab.ty in + let TableT (lim, at, t) = tab.ty in assert (lim.min = size tab); let old_size = lim.min in let new_size = Int64.add old_size delta in if I64.gt_u old_size new_size then raise SizeOverflow else let lim' = {lim with min = new_size} in - if not (valid_index it new_size) then raise SizeOverflow else + if not (valid_index at new_size) then raise SizeOverflow else if not (valid_limits lim') then raise SizeLimit else let after = create new_size r in Array.blit tab.content 0 after 0 (Array.length tab.content); - tab.ty <- TableT (lim', it, t); + tab.ty <- TableT (lim', at, t); tab.content <- after let load tab i = @@ -67,7 +67,7 @@ let load tab i = Lib.Array64.get tab.content i let store tab i r = - let TableT (_lim, _it, t) = tab.ty in + let TableT (_lim, _at, t) = tab.ty in if not (Match.match_ref_type [] (type_of_ref r) t) then raise Type; if i < 0L || i >= Lib.Array64.length tab.content then raise Bounds; Lib.Array64.set tab.content i r diff --git a/interpreter/runtime/table.mli b/interpreter/runtime/table.mli index 07e84d5b6..e3791daa6 100644 --- a/interpreter/runtime/table.mli +++ b/interpreter/runtime/table.mli @@ -16,7 +16,7 @@ exception OutOfMemory val alloc : table_type -> ref_ -> table (* raises Type, OutOfMemory *) val type_of : table -> table_type -val index_type_of : table -> index_type +val address_type_of : table -> address_type val size : table -> size val index_of_num : num -> index val grow : table -> size -> ref_ -> unit diff --git a/interpreter/runtime/value.ml b/interpreter/runtime/value.ml index 5988336ad..3c19a3c7d 100644 --- a/interpreter/runtime/value.ml +++ b/interpreter/runtime/value.ml @@ -281,10 +281,10 @@ let storage_bits_of_val st v = let value_of_bool b = Num (I32 (if b then 1l else 0l)) -let value_of_index it x = - match it with - | I64IndexType -> Num (I64 x) - | I32IndexType -> Num (I32 (Int64.to_int32 x)) +let value_of_address at x = + match at with + | I64AddressType -> Num (I64 x) + | I32AddressType -> Num (I32 (Int64.to_int32 x)) let string_of_num = function | I32 i -> I32.to_string_s i diff --git a/interpreter/syntax/free.ml b/interpreter/syntax/free.ml index 72314487f..efbbd58da 100644 --- a/interpreter/syntax/free.ml +++ b/interpreter/syntax/free.ml @@ -121,8 +121,8 @@ let def_type = function | DefT (rt, _i) -> rec_type rt let global_type (GlobalT (_mut, t)) = val_type t -let table_type (TableT (_lim, _it, t)) = ref_type t -let memory_type (MemoryT (_lim, _it)) = empty +let table_type (TableT (_lim, _at, t)) = ref_type t +let memory_type (MemoryT (_lim, _at)) = empty let tag_type (TagT dt) = def_type dt let extern_type = function diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml index 729a564ad..2e5ce2514 100644 --- a/interpreter/syntax/types.ml +++ b/interpreter/syntax/types.ml @@ -25,7 +25,7 @@ type heap_type = and ref_type = null * heap_type and val_type = NumT of num_type | VecT of vec_type | RefT of ref_type | BotT -and index_type = I32IndexType | I64IndexType +and address_type = I32AddressType | I64AddressType and result_type = val_type list and instr_type = InstrT of result_type * result_type * local_idx list @@ -45,8 +45,8 @@ and sub_type = SubT of final * heap_type list * str_type and rec_type = RecT of sub_type list and def_type = DefT of rec_type * int32 -type table_type = TableT of Int64.t limits * index_type * ref_type -type memory_type = MemoryT of Int64.t limits * index_type +type table_type = TableT of Int64.t limits * address_type * ref_type +type memory_type = MemoryT of Int64.t limits * address_type type global_type = GlobalT of mut * val_type type tag_type = TagT of def_type type local_type = LocalT of init * val_type @@ -147,11 +147,11 @@ let memories = List.filter_map (function ExternMemoryT mt -> Some mt | _ -> None let globals = List.filter_map (function ExternGlobalT gt -> Some gt | _ -> None) let tags = List.filter_map (function ExternTagT tt -> Some tt | _ -> None) -let num_type_of_index_type = function - | I32IndexType -> I32T - | I64IndexType -> I64T +let num_type_of_address_type = function + | I32AddressType -> I32T + | I64AddressType -> I64T -let value_type_of_index_type t = NumT (num_type_of_index_type t) +let value_type_of_address_type t = NumT (num_type_of_address_type t) (* Substitution *) @@ -228,10 +228,10 @@ let subst_def_type s = function let subst_memory_type s = function - | MemoryT (lim, it) -> MemoryT (lim, it) + | MemoryT (lim, at) -> MemoryT (lim, at) let subst_table_type s = function - | TableT (lim, it, t) -> TableT (lim, it, subst_ref_type s t) + | TableT (lim, at, t) -> TableT (lim, at, subst_ref_type s t) let subst_global_type s = function | GlobalT (mut, t) -> GlobalT (mut, subst_val_type s t) @@ -365,8 +365,8 @@ and string_of_val_type = function | RefT t -> string_of_ref_type t | BotT -> "bot" -and string_of_index_type t = - string_of_val_type (value_type_of_index_type t) +and string_of_address_type t = + string_of_val_type (value_type_of_address_type t) and string_of_result_type = function | ts -> "[" ^ String.concat " " (List.map string_of_val_type ts) ^ "]" @@ -418,10 +418,10 @@ let string_of_limits = function (match max with None -> "" | Some n -> " " ^ I64.to_string_u n) let string_of_memory_type = function - | MemoryT (lim, it) -> string_of_num_type (num_type_of_index_type it) ^ " " ^ string_of_limits lim + | MemoryT (lim, at) -> string_of_num_type (num_type_of_address_type at) ^ " " ^ string_of_limits lim let string_of_table_type = function - | TableT (lim, it, t) -> string_of_num_type (num_type_of_index_type it) ^ " " ^ string_of_limits lim ^ " " ^ string_of_ref_type t + | TableT (lim, at, t) -> string_of_num_type (num_type_of_address_type at) ^ " " ^ string_of_limits lim ^ " " ^ string_of_ref_type t let string_of_global_type = function | GlobalT (mut, t) -> string_of_mut (string_of_val_type t) mut diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml index fe9fbf2a4..4b7a19b43 100644 --- a/interpreter/text/arrange.ml +++ b/interpreter/text/arrange.ml @@ -77,7 +77,7 @@ let ref_type t = | (Null, ExnHT) -> "exnref" | t -> string_of_ref_type t -let index_type t = string_of_val_type (value_type_of_index_type t) +let address_type t = string_of_val_type (value_type_of_address_type t) let heap_type t = string_of_heap_type t let val_type t = string_of_val_type t let storage_type t = string_of_storage_type t @@ -657,14 +657,14 @@ let tag off i tag = ) let table off i tab = - let {ttype = TableT (lim, it, t); tinit} = tab.it in - Node ("table $" ^ nat (off + i) ^ " " ^ index_type it ^ " " ^ limits nat64 lim, + let {ttype = TableT (lim, at, t); tinit} = tab.it in + Node ("table $" ^ nat (off + i) ^ " " ^ address_type at ^ " " ^ limits nat64 lim, atom ref_type t :: list instr tinit.it ) let memory off i mem = - let {mtype = MemoryT (lim, it)} = mem.it in - Node ("memory $" ^ nat (off + i) ^ " " ^ index_type it ^ " " ^ limits nat64 lim, []) + let {mtype = MemoryT (lim, at)} = mem.it in + Node ("memory $" ^ nat (off + i) ^ " " ^ address_type at ^ " " ^ limits nat64 lim, []) let is_elem_kind = function | (NoNull, FuncHT) -> true diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index bd5d205ac..d505297ea 100644 --- a/interpreter/text/parser.mly +++ b/interpreter/text/parser.mly @@ -264,37 +264,37 @@ let inline_func_type_explicit (c : context) x ft loc = error (at loc) "inline function type does not match explicit type"; x -let index_type_of_num_type t loc = +let address_type_of_num_type t loc = match t with - | I32T -> I32IndexType - | I64T -> I64IndexType - | _ -> error (at loc) "illegal index type" + | I32T -> I32AddressType + | I64T -> I64AddressType + | _ -> error (at loc) "illegal address type" -let index_type_of_value_type t loc = +let address_type_of_value_type t loc = match t with - | NumT t -> index_type_of_num_type t loc - | _ -> error (at loc) "illegal index type" + | NumT t -> address_type_of_num_type t loc + | _ -> error (at loc) "illegal address type" -let memory_data init it c x loc = +let memory_data init at c x loc = let size = Int64.(div (add (of_int (String.length init)) 65535L) 65536L) in - let instr = match it with - | I32IndexType -> i32_const (0l @@ loc) - | I64IndexType -> i64_const (0L @@ loc) in + let instr = match at with + | I32AddressType -> i32_const (0l @@ loc) + | I64AddressType -> i64_const (0L @@ loc) in let offset = [instr @@ loc] @@ loc in - [{mtype = MemoryT ({min = size; max = Some size}, it)} @@ loc], + [{mtype = MemoryT ({min = size; max = Some size}, at)} @@ loc], [{dinit = init; dmode = Active {index = x; offset} @@ loc} @@ loc], [], [] -let table_data tinit init it etype c x loc = - let instr = match it with - | I32IndexType -> i32_const (0l @@ loc) - | I64IndexType -> i64_const (0L @@ loc) in +let table_data tinit init at etype c x loc = + let instr = match at with + | I32AddressType -> i32_const (0l @@ loc) + | I64AddressType -> i64_const (0L @@ loc) in let offset = [instr @@ loc] @@ loc in let einit = init c in let size = Lib.List32.length einit in let size64 = Int64.of_int32 size in let emode = Active {index = x; offset} @@ loc in - [{ttype = TableT ({min = size64; max = Some size64}, it, etype); tinit} @@ loc], + [{ttype = TableT ({min = size64; max = Some size64}, at, etype); tinit} @@ loc], [{etype; einit; emode} @@ loc], [], [] @@ -501,12 +501,12 @@ sub_type : List.map (fun y -> VarHT (StatX y.it)) ($4 c type_), $5 c x) } table_type : - | val_type limits ref_type { fun c -> TableT ($2, index_type_of_value_type ($1 c) $sloc, $3 c) } - | limits ref_type { fun c -> TableT ($1, I32IndexType, $2 c) } + | val_type limits ref_type { fun c -> TableT ($2, address_type_of_value_type ($1 c) $sloc, $3 c) } + | limits ref_type { fun c -> TableT ($1, I32AddressType, $2 c) } memory_type : - | val_type limits { fun c -> MemoryT ($2, index_type_of_value_type ($1 c) $sloc) } - | limits { fun c -> MemoryT ($1, I32IndexType) } + | val_type limits { fun c -> MemoryT ($2, address_type_of_value_type ($1 c) $sloc) } + | limits { fun c -> MemoryT ($1, I32AddressType) } limits : | NAT { {min = nat64 $1 $loc($1); max = None} } @@ -1165,19 +1165,19 @@ table_fields : let emode = Active {index = x; offset} @@ loc in let (_, ht) as etype = $1 c in let tinit = [RefNull ht @@ loc] @@ loc in - [{ttype = TableT ({min = size64; max = Some size64}, I32IndexType, etype); tinit} @@ loc], + [{ttype = TableT ({min = size64; max = Some size64}, I32AddressType, etype); tinit} @@ loc], [{etype; einit; emode} @@ loc], [], [] } | ref_type LPAR ELEM elem_var_list RPAR /* Sugar */ { fun c x loc -> let (_, ht) as etype = $1 c in let tinit = [RefNull ht @@ loc] @@ loc in - table_data tinit $4 I32IndexType etype c x loc } + table_data tinit $4 I32AddressType etype c x loc } | val_type ref_type LPAR ELEM elem_var_list RPAR /* Sugar */ { fun c x loc -> let (_, ht) as etype = $2 c in let tinit = [RefNull ht @@ loc] @@ loc in - table_data tinit $5 (index_type_of_value_type ($1 c) loc) etype c x loc } + table_data tinit $5 (address_type_of_value_type ($1 c) loc) etype c x loc } data : | LPAR DATA bind_var_opt string_list RPAR @@ -1209,9 +1209,9 @@ memory_fields : { fun c x loc -> let mems, data, ims, exs = $2 c x loc in mems, data, ims, $1 (MemoryExport x) c :: exs } | LPAR DATA string_list RPAR /* Sugar */ - { memory_data $3 I32IndexType } + { memory_data $3 I32AddressType } | val_type LPAR DATA string_list RPAR /* Sugar */ - { fun c x loc -> memory_data $4 (index_type_of_value_type ($1 c) $sloc) c x loc } + { fun c x loc -> memory_data $4 (address_type_of_value_type ($1 c) $sloc) c x loc } tag : | LPAR TAG bind_var_opt tag_fields RPAR diff --git a/interpreter/valid/match.ml b/interpreter/valid/match.ml index 77c9c4f57..b2cc26630 100644 --- a/interpreter/valid/match.ml +++ b/interpreter/valid/match.ml @@ -161,11 +161,11 @@ let match_global_type c (GlobalT (mut1, t1)) (GlobalT (mut2, t2)) = | Cons -> true | Var -> match_val_type c t2 t1 -let match_table_type c (TableT (lim1, it1, t1)) (TableT (lim2, it2, t2)) = - match_limits c lim1 lim2 && it1 = it2 && match_ref_type c t1 t2 && match_ref_type c t2 t1 +let match_table_type c (TableT (lim1, at1, t1)) (TableT (lim2, at2, t2)) = + match_limits c lim1 lim2 && at1 = at2 && match_ref_type c t1 t2 && match_ref_type c t2 t1 -let match_memory_type c (MemoryT (lim1, it1)) (MemoryT (lim2, it2)) = - match_limits c lim1 lim2 && it1 = it2 +let match_memory_type c (MemoryT (lim1, at1)) (MemoryT (lim2, at2)) = + match_limits c lim1 lim2 && at1 = at2 let match_tag_type c (TagT dt1) (TagT dt2) = match_def_type c dt1 dt2 && match_def_type c dt2 dt1 diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index 511c34b09..2b94dfa5c 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -151,23 +151,23 @@ let check_func_type (c : context) (ft : func_type) at = check_result_type c ts2 at let check_table_type (c : context) (tt : table_type) at = - let TableT (lim, it, t) = tt in + let TableT (lim, _at, t) = tt in check_ref_type c t at; - match it with - | I64IndexType -> + match _at with + | I64AddressType -> check_limits I64.le_u lim 0xffff_ffff_ffff_ffffL at "table size must be at most 2^64-1" - | I32IndexType -> + | I32AddressType -> check_limits I64.le_u lim 0xffff_ffffL at "table size must be at most 2^32-1" let check_memory_type (c : context) (mt : memory_type) at = - let MemoryT (lim, it) = mt in - match it with - | I32IndexType -> + let MemoryT (lim, _at) = mt in + match _at with + | I32AddressType -> check_limits I64.le_u lim 0x1_0000L at "memory size must be at most 65536 pages (4GiB)" - | I64IndexType -> + | I64AddressType -> check_limits I64.le_u lim 0x1_0000_0000_0000L at "memory size must be at most 48 bits of pages" @@ -370,8 +370,8 @@ let check_memop (c : context) (memop : ('t, 's) memop) ty_size get_sz at = in require (1 lsl memop.align >= 1 && 1 lsl memop.align <= size) at "alignment must not be larger than natural"; - let MemoryT (_lim, it) = memory c (0l @@ at) in - if it = I32IndexType then + let MemoryT (_lim, _at) = memory c (0l @@ at) in + if _at = I32AddressType then require (I64.lt_u memop.offset 0x1_0000_0000L) at "offset out of range"; memop.ty @@ -518,12 +518,12 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in (ts1 @ [RefT (Null, DefHT (type_ c x))]) --> ts2, [] | CallIndirect (x, y) -> - let TableT (lim, it, t) = table c x in + let TableT (lim, at, t) = table c x in let FuncT (ts1, ts2) = func_type c y in require (match_ref_type c.types t (Null, FuncHT)) x.at ("type mismatch: instruction requires table of function type" ^ " but table has element type " ^ string_of_ref_type t); - (ts1 @ [value_type_of_index_type it]) --> ts2, [] + (ts1 @ [value_type_of_address_type at]) --> ts2, [] | ReturnCall x -> let FuncT (ts1, ts2) = as_func_str_type (expand_def_type (func c x)) in @@ -542,13 +542,13 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in (ts1 @ [RefT (Null, DefHT (type_ c x))]) -->... [], [] | ReturnCallIndirect (x, y) -> - let TableT (_lim, it, t) = table c x in + let TableT (_lim, at, t) = table c x in let FuncT (ts1, ts2) = func_type c y in require (match_result_type c.types ts2 c.results) e.at ("type mismatch: current function requires result type " ^ string_of_result_type c.results ^ " but callee returns " ^ string_of_result_type ts2); - (ts1 @ [value_type_of_index_type it]) -->... [], [] + (ts1 @ [value_type_of_address_type at]) -->... [], [] | Throw x -> let TagT dt = tag c x in @@ -588,102 +588,102 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in [t] --> [], [] | TableGet x -> - let TableT (_lim, it, rt) = table c x in - [value_type_of_index_type it] --> [RefT rt], [] + let TableT (_lim, at, rt) = table c x in + [value_type_of_address_type at] --> [RefT rt], [] | TableSet x -> - let TableT (_lim, it, rt) = table c x in - [value_type_of_index_type it; RefT rt] --> [], [] + let TableT (_lim, at, rt) = table c x in + [value_type_of_address_type at; RefT rt] --> [], [] | TableSize x -> - let TableT (_lim, it, _rt) = table c x in - [] --> [value_type_of_index_type it], [] + let TableT (_lim, at, _rt) = table c x in + [] --> [value_type_of_address_type at], [] | TableGrow x -> - let TableT (_lim, it, rt) = table c x in - [RefT rt; value_type_of_index_type it] --> [value_type_of_index_type it], [] + let TableT (_lim, at, rt) = table c x in + [RefT rt; value_type_of_address_type at] --> [value_type_of_address_type at], [] | TableFill x -> - let TableT (_lim, it, rt) = table c x in - [value_type_of_index_type it; RefT rt; value_type_of_index_type it] --> [], [] + let TableT (_lim, at, rt) = table c x in + [value_type_of_address_type at; RefT rt; value_type_of_address_type at] --> [], [] | TableCopy (x, y) -> - let TableT (_lim1, it1, t1) = table c x in - let TableT (_lim2, it2, t2) = table c y in - let it_min = min it1 it2 in + let TableT (_lim1, at1, t1) = table c x in + let TableT (_lim2, at2, t2) = table c y in + let at_min = min at1 at2 in require (match_ref_type c.types t2 t1) x.at ("type mismatch: source element type " ^ string_of_ref_type t1 ^ " does not match destination element type " ^ string_of_ref_type t2); - [value_type_of_index_type it1; value_type_of_index_type it2; value_type_of_index_type it_min] --> [], [] + [value_type_of_address_type at1; value_type_of_address_type at2; value_type_of_address_type at_min] --> [], [] | TableInit (x, y) -> - let TableT (_lim1, it, t1) = table c x in + let TableT (_lim1, at, t1) = table c x in let t2 = elem c y in require (match_ref_type c.types t2 t1) x.at ("type mismatch: element segment's type " ^ string_of_ref_type t1 ^ " does not match table's element type " ^ string_of_ref_type t2); - [value_type_of_index_type it; NumT I32T; NumT I32T] --> [], [] + [value_type_of_address_type at; NumT I32T; NumT I32T] --> [], [] | ElemDrop x -> ignore (elem c x); [] --> [], [] | Load (x, memop) -> - let MemoryT (_lim, it) = memory c x in + let MemoryT (_lim, at) = memory c x in let t = check_memop c memop num_size (Lib.Option.map fst) e.at in - [value_type_of_index_type it] --> [NumT t], [] + [value_type_of_address_type at] --> [NumT t], [] | Store (x, memop) -> - let MemoryT (_lim, it) = memory c x in + let MemoryT (_lim, at) = memory c x in let t = check_memop c memop num_size (fun sz -> sz) e.at in - [value_type_of_index_type it; NumT t] --> [], [] + [value_type_of_address_type at; NumT t] --> [], [] | VecLoad (x, memop) -> - let MemoryT (_lim, it) = memory c x in + let MemoryT (_lim, at) = memory c x in let t = check_memop c memop vec_size (Lib.Option.map fst) e.at in - [value_type_of_index_type it] --> [VecT t], [] + [value_type_of_address_type at] --> [VecT t], [] | VecStore (x, memop) -> - let MemoryT (_lim, it) = memory c x in + let MemoryT (_lim, at) = memory c x in let t = check_memop c memop vec_size (fun _ -> None) e.at in - [value_type_of_index_type it; VecT t] --> [], [] + [value_type_of_address_type at; VecT t] --> [], [] | VecLoadLane (x, memop, i) -> - let MemoryT (_lim, it) = memory c x in + let MemoryT (_lim, at) = memory c x in let t = check_memop c memop vec_size (fun sz -> Some sz) e.at in require (i < vec_size t / Pack.packed_size memop.pack) e.at "invalid lane index"; - [value_type_of_index_type it; VecT t] --> [VecT t], [] + [value_type_of_address_type at; VecT t] --> [VecT t], [] | VecStoreLane (x, memop, i) -> - let MemoryT (_lim, it) = memory c x in + let MemoryT (_lim, at) = memory c x in let t = check_memop c memop vec_size (fun sz -> Some sz) e.at in require (i < vec_size t / Pack.packed_size memop.pack) e.at "invalid lane index"; - [value_type_of_index_type it; VecT t] --> [], [] + [value_type_of_address_type at; VecT t] --> [], [] | MemorySize x -> - let MemoryT (_lim, it) = memory c x in - [] --> [value_type_of_index_type it], [] + let MemoryT (_lim, at) = memory c x in + [] --> [value_type_of_address_type at], [] | MemoryGrow x -> - let MemoryT (_lim, it) = memory c x in - [value_type_of_index_type it] --> [value_type_of_index_type it], [] + let MemoryT (_lim, at) = memory c x in + [value_type_of_address_type at] --> [value_type_of_address_type at], [] | MemoryFill x -> - let MemoryT (_lim, it) = memory c x in - [value_type_of_index_type it; NumT I32T; value_type_of_index_type it] --> [], [] + let MemoryT (_lim, at) = memory c x in + [value_type_of_address_type at; NumT I32T; value_type_of_address_type at] --> [], [] | MemoryCopy (x, y)-> - let MemoryT (_lib1, it1) = memory c x in - let MemoryT (_lib2, it2) = memory c y in - let it_min = min it1 it2 in - [value_type_of_index_type it1; value_type_of_index_type it2; value_type_of_index_type it_min] --> [], [] + let MemoryT (_lib1, at1) = memory c x in + let MemoryT (_lib2, at2) = memory c y in + let at_min = min at1 at2 in + [value_type_of_address_type at1; value_type_of_address_type at2; value_type_of_address_type at_min] --> [], [] | MemoryInit (x, y) -> - let MemoryT (_lib, it) = memory c x in + let MemoryT (_lib, at) = memory c x in let () = data c y in - [value_type_of_index_type it; NumT I32T; NumT I32T] --> [], [] + [value_type_of_address_type at; NumT I32T; NumT I32T] --> [], [] | DataDrop x -> let () = data c x in @@ -1029,7 +1029,7 @@ let check_global (c : context) (glob : global) : context = let check_table (c : context) (tab : table) : context = let {ttype; tinit} = tab.it in - let TableT (_lim, _it, rt) = ttype in + let TableT (_lim, _at, rt) = ttype in check_table_type c ttype tab.at; check_const c tinit (RefT rt); {c with tables = c.tables @ [ttype]} @@ -1048,11 +1048,11 @@ let check_elem_mode (c : context) (t : ref_type) (mode : segment_mode) = match mode.it with | Passive -> () | Active {index; offset} -> - let TableT (_lim, it, et) = table c index in + let TableT (_lim, at, et) = table c index in require (match_ref_type c.types t et) mode.at ("type mismatch: element segment's type " ^ string_of_ref_type t ^ " does not match table's element type " ^ string_of_ref_type et); - check_const c offset (value_type_of_index_type it) + check_const c offset (value_type_of_address_type at) | Declarative -> () let check_elem (c : context) (seg : elem_segment) : context = @@ -1066,8 +1066,8 @@ let check_data_mode (c : context) (mode : segment_mode) = match mode.it with | Passive -> () | Active {index; offset} -> - let MemoryT (_, it) = memory c index in - check_const c offset (value_type_of_index_type it) + let MemoryT (_, at) = memory c index in + check_const c offset (value_type_of_address_type at) | Declarative -> assert false let check_data (c : context) (seg : data_segment) : context =