Skip to content

Commit

Permalink
Update "index type" to "address type" in the spec interpreter
Browse files Browse the repository at this point in the history
  • Loading branch information
bvisness committed Oct 17, 2024
1 parent 5a12b70 commit 538c851
Show file tree
Hide file tree
Showing 15 changed files with 150 additions and 150 deletions.
6 changes: 3 additions & 3 deletions interpreter/binary/decode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
10 changes: 5 additions & 5 deletions interpreter/binary/encode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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

Expand Down
8 changes: 4 additions & 4 deletions interpreter/exec/eval.ml
Original file line number Diff line number Diff line change
Expand Up @@ -385,15 +385,15 @@ 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
let old_size = Table.size tab in
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
Expand Down Expand Up @@ -552,15 +552,15 @@ 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
let old_size = Memory.size mem in
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
Expand Down
6 changes: 3 additions & 3 deletions interpreter/host/spectest.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down
18 changes: 9 additions & 9 deletions interpreter/runtime/memory.ml
Original file line number Diff line number Diff line change
Expand Up @@ -25,19 +25,19 @@ 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
Array1.fill mem 0;
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
Expand All @@ -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
Expand All @@ -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 =
Expand Down
2 changes: 1 addition & 1 deletion interpreter/runtime/memory.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
22 changes: 11 additions & 11 deletions interpreter/runtime/table.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand All @@ -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
Expand All @@ -49,25 +49,25 @@ 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 =
if i < 0L || i >= Lib.Array64.length tab.content then raise Bounds;
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
Expand Down
2 changes: 1 addition & 1 deletion interpreter/runtime/table.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 4 additions & 4 deletions interpreter/runtime/value.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions interpreter/syntax/free.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
26 changes: 13 additions & 13 deletions interpreter/syntax/types.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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
Expand Down Expand Up @@ -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 *)

Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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) ^ "]"
Expand Down Expand Up @@ -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
Expand Down
10 changes: 5 additions & 5 deletions interpreter/text/arrange.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
Loading

0 comments on commit 538c851

Please sign in to comment.