From 5c3940bffbf61adb55421e901a322683ed29b28d Mon Sep 17 00:00:00 2001 From: Sam Clegg Date: Wed, 6 Nov 2024 14:02:29 -0800 Subject: [PATCH] Intepreter and test updates from @rossberg Interpreter: - Fixed evaluation of v128 load/store instructions to work with i64 - Reworked bulk operation execution to still reduce to well-typed instructions for i32 - Added missing size check to table allocation - Various minor refactorings and clean-ups Tests: - Added tests for size check in i64 table and memory type limits Split out from https://github.com/WebAssembly/spec/pull/1839 --- interpreter/binary/decode.ml | 12 +- interpreter/binary/encode.ml | 10 +- interpreter/exec/eval.ml | 244 +++++++++++++++----------------- interpreter/host/spectest.ml | 6 +- interpreter/runtime/data.ml | 1 - interpreter/runtime/data.mli | 3 +- interpreter/runtime/elem.mli | 2 +- interpreter/runtime/memory.ml | 36 ++--- interpreter/runtime/memory.mli | 5 +- interpreter/runtime/table.ml | 26 ++-- interpreter/runtime/table.mli | 13 +- interpreter/runtime/value.ml | 20 ++- interpreter/syntax/free.ml | 4 +- interpreter/syntax/operators.ml | 4 + interpreter/syntax/types.ml | 40 +++--- interpreter/text/arrange.ml | 6 +- interpreter/text/parser.mly | 86 ++++------- interpreter/valid/match.ml | 9 +- interpreter/valid/valid.ml | 144 +++++++++---------- test/core/memory.wast | 37 +++-- test/core/memory64.wast | 18 +++ test/core/table.wast | 6 +- 22 files changed, 370 insertions(+), 362 deletions(-) diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml index 1db0dce4f..53c7294c8 100644 --- a/interpreter/binary/decode.ml +++ b/interpreter/binary/decode.ml @@ -281,19 +281,19 @@ let limits uN s = let flags = byte s in require (flags land 0xfa = 0) s (pos s - 1) "malformed limits flags"; let has_max = (flags land 1 = 1) in - let is64 = (flags land 4 = 4) in + let at = if flags land 4 = 4 then I64AT else I32AT in let min = uN s in let max = opt uN has_max s in - {min; max}, is64 + at, {min; max} let table_type s = let t = ref_type s in - let lim, is64 = limits u64 s in - TableT (lim, (if is64 then I64AddrType else I32AddrType), t) + let at, lim = limits u64 s in + TableT (at, lim, t) let memory_type s = - let lim, is64 = limits u64 s in - MemoryT (lim, if is64 then I64AddrType else I32AddrType) + let at, lim = limits u64 s in + MemoryT (at, lim) let global_type s = let t = val_type s in diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml index 3e7003a89..eb1e729b0 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} at = - let flags = flag (max <> None) 0 + flag (at = I64AddrType) 2 in - byte flags; vu min; opt vu max + let limits at {min; max} = + let flags = flag (max <> None) 0 + flag (at = I64AT) 2 in + byte flags; u64 min; opt u64 max let table_type = function - | TableT (lim, at, t) -> ref_type t; limits u64 lim at + | TableT (at, lim, t) -> ref_type t; limits at lim let memory_type = function - | MemoryT (lim, at) -> limits u64 lim at + | MemoryT (at, lim) -> limits at lim let global_type = function | GlobalT (mut, t) -> val_type t; mutability mut diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index c5631d1ba..8af47528d 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -157,48 +157,27 @@ let split n (vs : 'a stack) at = take n vs at, drop n vs at * c : config *) -let inc_address i loc = - match i with - | I32 x -> (I32 (I32.add x 1l) @@ loc) - | I64 x -> (I64 (I64.add x 1L) @@ loc) - | _ -> Crash.error loc ("bad address type") - -let index_of_num x = - match x with - | I64 i -> i - | I32 i -> I64_convert.extend_i32_u i - | _ -> raise Type - let mem_oob frame x i n = let mem = (memory frame.inst x) in - let start = Memory.address_of_num i in - I64.gt_u (I64.add start (Memory.address_of_num n)) + I64.gt_u (I64.add (addr_of_num i) (addr_of_num n)) (Memory.bound mem) let data_oob frame x i n = - I64.gt_u (I64.add (Memory.address_of_num i) (Memory.address_of_num n)) + I64.gt_u (I64.add (addr_of_num i) (addr_of_num n)) (Data.size (data frame.inst x)) let table_oob frame x i n = - I64.gt_u (I64.add (Table.index_of_num i) (Table.index_of_num n)) + I64.gt_u (I64.add (addr_of_num i) (addr_of_num n)) (Table.size (table frame.inst x)) let elem_oob frame x i n = - I64.gt_u (I64.add (Table.index_of_num i) (Table.index_of_num n)) - (Elem.size (elem frame.inst x)) - -let elem_oob2 frame x i n = - I64.gt_u (I64.add (Table.index_of_num i) (I64_convert.extend_i32_u n)) + I64.gt_u (I64.add (addr_of_num i) (addr_of_num n)) (Elem.size (elem frame.inst x)) let array_oob a i n = I64.gt_u (I64.add (I64_convert.extend_i32_u i) (I64_convert.extend_i32_u n)) (I64_convert.extend_i32_u (Aggr.array_length a)) -let array_oob2 a i n = - I64.gt_u (I64.add (I64_convert.extend_i32_u i) (index_of_num n)) - (I64_convert.extend_i32_u (Aggr.array_length a)) - let rec step (c : config) : config = let vs, es = c.code in let e = List.hd es in @@ -284,9 +263,9 @@ let rec step (c : config) : config = | CallRef _x, Ref (FuncRef f) :: vs -> vs, [Invoke f @@ e.at] - | CallIndirect (x, y), Num n :: vs -> - let i = Table.index_of_num n in - let f = func_ref c.frame.inst x i e.at in + | CallIndirect (x, y), Num i :: vs -> + let i_64 = addr_of_num i in + let f = func_ref c.frame.inst x i_64 e.at in if Match.match_def_type [] (Func.type_of f) (type_ c.frame.inst y) then vs, [Invoke f @@ e.at] else @@ -373,96 +352,96 @@ let rec step (c : config) : config = with Global.NotMutable -> Crash.error e.at "write to immutable global" | Global.Type -> Crash.error e.at "type mismatch at global write") - | TableGet x, Num n :: vs' -> - let i = Table.index_of_num n in - (try Ref (Table.load (table c.frame.inst x) i) :: vs', [] + | TableGet x, Num i :: vs' -> + let i_64 = addr_of_num i in + (try Ref (Table.load (table c.frame.inst x) i_64) :: vs', [] with exn -> vs', [Trapping (table_error e.at exn) @@ e.at]) - | TableSet x, Ref r :: Num n :: vs' -> - let i = Table.index_of_num n in - (try Table.store (table c.frame.inst x) i r; vs', [] + | TableSet x, Ref r :: Num i :: vs' -> + let i_64 = addr_of_num i in + (try Table.store (table c.frame.inst x) i_64 r; vs', [] with exn -> vs', [Trapping (table_error e.at exn) @@ e.at]) | TableSize x, vs -> let tab = table c.frame.inst x in - value_of_addr (Table.addr_type_of tab) (Table.size (table c.frame.inst x)) :: vs, [] + Num (num_of_addr (Table.addr_type_of tab) (Table.size tab)) :: vs, [] - | TableGrow x, Num delta :: Ref r :: vs' -> + | TableGrow x, Num n :: Ref r :: vs' -> + let n_64 = addr_of_num n in 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 + try Table.grow tab n_64 r; old_size with Table.SizeOverflow | Table.SizeLimit | Table.OutOfMemory -> -1L - in (value_of_addr (Table.addr_type_of tab) result) :: vs', [] + in Num (num_of_addr (Table.addr_type_of tab) result) :: vs', [] | TableFill x, Num n :: Ref r :: Num i :: vs' -> - let n_64 = Table.index_of_num n in + let n_64 = addr_of_num n in + let i_64 = addr_of_num i in if table_oob c.frame x i n then vs', [Trapping (table_error e.at Table.Bounds) @@ e.at] else if n_64 = 0L then vs', [] else - let i_64 = Table.index_of_num i in let _ = assert (I64.lt_u i_64 0xffff_ffff_ffff_ffffL) in vs', List.map (Lib.Fun.flip (@@) e.at) [ - Plain (Const (I64 i_64 @@ e.at)); + Plain (Const (i @@ e.at)); Refer r; Plain (TableSet x); - Plain (Const (I64 (I64.add i_64 1L) @@ e.at)); + Plain (Const (addr_add i 1L @@ e.at)); Refer r; - Plain (Const (I64 (I64.sub n_64 1L) @@ e.at)); + Plain (Const (addr_sub n 1L @@ e.at)); Plain (TableFill x); ] | TableCopy (x, y), Num n :: Num s :: Num d :: vs' -> - let n_64 = Table.index_of_num n in - let s_64 = Table.index_of_num s in - let d_64 = Table.index_of_num d in + let n_64 = addr_of_num n in + let s_64 = addr_of_num s in + let d_64 = addr_of_num d in if table_oob c.frame x d n || table_oob c.frame y s n then vs', [Trapping (table_error e.at Table.Bounds) @@ e.at] else if n_64 = 0L then vs', [] else if I64.le_u d_64 s_64 then vs', List.map (Lib.Fun.flip (@@) e.at) [ - Plain (Const (I64 d_64 @@ e.at)); - Plain (Const (I64 s_64 @@ e.at)); + Plain (Const (d @@ e.at)); + Plain (Const (s @@ e.at)); Plain (TableGet y); Plain (TableSet x); - Plain (Const (I64 (I64.add d_64 1L) @@ e.at)); - Plain (Const (I64 (I64.add s_64 1L) @@ e.at)); - Plain (Const (I64 (I64.sub n_64 1L) @@ e.at)); + Plain (Const (addr_add d 1L @@ e.at)); + Plain (Const (addr_add s 1L @@ e.at)); + Plain (Const (addr_sub n 1L @@ e.at)); Plain (TableCopy (x, y)); ] else (* d > s *) let n' = I64.sub n_64 1L in vs', List.map (Lib.Fun.flip (@@) e.at) [ - Plain (Const (I64 (I64.add d_64 n') @@ e.at)); - Plain (Const (I64 (I64.add s_64 n') @@ e.at)); + Plain (Const (addr_add d n' @@ e.at)); + Plain (Const (addr_add s n' @@ e.at)); Plain (TableGet y); Plain (TableSet x); - Plain (Const (I64 d_64 @@ e.at)); - Plain (Const (I64 s_64 @@ e.at)); - Plain (Const (I64 n' @@ e.at)); + Plain (Const (d @@ e.at)); + Plain (Const (s @@ e.at)); + Plain (Const (addr_sub n 1L @@ e.at)); Plain (TableCopy (x, y)); ] | TableInit (x, y), Num n :: Num s :: Num d :: vs' -> - let n_64 = Table.index_of_num n in + let n_64 = addr_of_num n in + let s_64 = addr_of_num s in if table_oob c.frame x d n || elem_oob c.frame y s n then vs', [Trapping (table_error e.at Table.Bounds) @@ e.at] else if n_64 = 0L then vs', [] else - let d_64 = Table.index_of_num d in - let s_64 = Table.index_of_num s in let seg = elem c.frame.inst y in vs', List.map (Lib.Fun.flip (@@) e.at) [ - Plain (Const (I64 d_64 @@ e.at)); + Plain (Const (d @@ e.at)); Refer (Elem.load seg s_64); Plain (TableSet x); - Plain (Const (I64 (I64.add d_64 1L) @@ e.at)); - Plain (Const (I64 (I64.add s_64 1L) @@ e.at)); - Plain (Const (I64 (I64.sub n_64 1L) @@ e.at)); + Plain (Const (addr_add d 1L @@ e.at)); + Plain (Const (addr_add s 1L @@ e.at)); + Plain (Const (addr_sub n 1L @@ e.at)); Plain (TableInit (x, y)); ] @@ -472,98 +451,99 @@ let rec step (c : config) : config = vs, [] | Load (x, {offset; ty; pack; _}), Num i :: vs' -> + let i_64 = addr_of_num i in let mem = memory c.frame.inst x in - let a = Memory.address_of_num i in (try let n = match pack with - | None -> Memory.load_num mem a offset ty - | Some (sz, ext) -> Memory.load_num_packed sz ext mem a offset ty + | None -> Memory.load_num mem i_64 offset ty + | Some (sz, ext) -> Memory.load_num_packed sz ext mem i_64 offset ty in Num n :: vs', [] with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]) | Store (x, {offset; pack; _}), Num n :: Num i :: vs' -> + let i_64 = addr_of_num i in let mem = memory c.frame.inst x in - let a = Memory.address_of_num i in (try (match pack with - | None -> Memory.store_num mem a offset n - | Some sz -> Memory.store_num_packed sz mem a offset n + | None -> Memory.store_num mem i_64 offset n + | Some sz -> Memory.store_num_packed sz mem i_64 offset n ); vs', [] with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]); - | VecLoad (x, {offset; ty; pack; _}), Num (I32 i) :: vs' -> + | VecLoad (x, {offset; ty; pack; _}), Num i :: vs' -> + let i_64 = addr_of_num i in let mem = memory c.frame.inst x in - let a = I64_convert.extend_i32_u i in (try let v = match pack with - | None -> Memory.load_vec mem a offset ty - | Some (sz, ext) -> Memory.load_vec_packed sz ext mem a offset ty + | None -> Memory.load_vec mem i_64 offset ty + | Some (sz, ext) -> Memory.load_vec_packed sz ext mem i_64 offset ty in Vec v :: vs', [] with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]) - | VecStore (x, {offset; _}), Vec v :: Num (I32 i) :: vs' -> + | VecStore (x, {offset; _}), Vec v :: Num i :: vs' -> + let i_64 = addr_of_num i in let mem = memory c.frame.inst x in - let addr = I64_convert.extend_i32_u i in (try - Memory.store_vec mem addr offset v; + Memory.store_vec mem i_64 offset v; vs', [] with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]); - | VecLoadLane (x, {offset; ty; pack; _}, j), Vec (V128 v) :: Num (I32 i) :: vs' -> + | VecLoadLane (x, {offset; ty; pack; _}, j), Vec (V128 v) :: Num i :: vs' -> + let i_64 = addr_of_num i in let mem = memory c.frame.inst x in - let addr = I64_convert.extend_i32_u i in (try let v = match pack with | Pack8 -> V128.I8x16.replace_lane j v - (I32Num.of_num 0 (Memory.load_num_packed Pack8 SX mem addr offset I32T)) + (I32Num.of_num 0 (Memory.load_num_packed Pack8 SX mem i_64 offset I32T)) | Pack16 -> V128.I16x8.replace_lane j v - (I32Num.of_num 0 (Memory.load_num_packed Pack16 SX mem addr offset I32T)) + (I32Num.of_num 0 (Memory.load_num_packed Pack16 SX mem i_64 offset I32T)) | Pack32 -> V128.I32x4.replace_lane j v - (I32Num.of_num 0 (Memory.load_num mem addr offset I32T)) + (I32Num.of_num 0 (Memory.load_num mem i_64 offset I32T)) | Pack64 -> V128.I64x2.replace_lane j v - (I64Num.of_num 0 (Memory.load_num mem addr offset I64T)) + (I64Num.of_num 0 (Memory.load_num mem i_64 offset I64T)) in Vec (V128 v) :: vs', [] with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]) - | VecStoreLane (x, {offset; ty; pack; _}, j), Vec (V128 v) :: Num (I32 i) :: vs' -> + | VecStoreLane (x, {offset; ty; pack; _}, j), Vec (V128 v) :: Num i :: vs' -> + let i_64 = addr_of_num i in let mem = memory c.frame.inst x in - let addr = I64_convert.extend_i32_u i in (try (match pack with | Pack8 -> - Memory.store_num_packed Pack8 mem addr offset (I32 (V128.I8x16.extract_lane_s j v)) + Memory.store_num_packed Pack8 mem i_64 offset (I32 (V128.I8x16.extract_lane_s j v)) | Pack16 -> - Memory.store_num_packed Pack16 mem addr offset (I32 (V128.I16x8.extract_lane_s j v)) + Memory.store_num_packed Pack16 mem i_64 offset (I32 (V128.I16x8.extract_lane_s j v)) | Pack32 -> - Memory.store_num mem addr offset (I32 (V128.I32x4.extract_lane_s j v)) + Memory.store_num mem i_64 offset (I32 (V128.I32x4.extract_lane_s j v)) | Pack64 -> - Memory.store_num mem addr offset (I64 (V128.I64x2.extract_lane_s j v)) + Memory.store_num mem i_64 offset (I64 (V128.I64x2.extract_lane_s j v)) ); vs', [] with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]) | MemorySize x, vs -> let mem = memory c.frame.inst x in - value_of_addr (Memory.addr_type_of mem) (Memory.size mem) :: vs, [] + Num (num_of_addr (Memory.addr_type_of mem) (Memory.size mem)) :: vs, [] - | MemoryGrow x, Num delta :: vs' -> + | MemoryGrow x, Num n :: vs' -> + let n_64 = addr_of_num n in 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 + try Memory.grow mem n_64; old_size with Memory.SizeOverflow | Memory.SizeLimit | Memory.OutOfMemory -> -1L - in (value_of_addr (Memory.addr_type_of mem) result) :: vs', [] + in Num (num_of_addr (Memory.addr_type_of mem) result) :: vs', [] | MemoryFill x, Num n :: Num k :: Num i :: vs' -> - let n_64 = Memory.address_of_num n in + let n_64 = addr_of_num n in if mem_oob c.frame x i n then vs', [Trapping (memory_error e.at Memory.Bounds) @@ e.at] else if n_64 = 0L then @@ -574,67 +554,66 @@ let rec step (c : config) : config = Plain (Const (k @@ e.at)); Plain (Store (x, {ty = I32T; align = 0; offset = 0L; pack = Some Pack8})); - Plain (Const (inc_address i e.at)); + Plain (Const (addr_add i 1L @@ e.at)); Plain (Const (k @@ e.at)); - Plain (Const (I64 (I64.sub n_64 1L) @@ e.at)); + Plain (Const (addr_sub n 1L @@ e.at)); Plain (MemoryFill x); ] | MemoryCopy (x, y), Num n :: Num s :: Num d :: vs' -> - let n_64 = Memory.address_of_num n in - let s_64 = Memory.address_of_num s in - let d_64 = Memory.address_of_num d in + let n_64 = addr_of_num n in + let s_64 = addr_of_num s in + let d_64 = addr_of_num d in if mem_oob c.frame x d n || mem_oob c.frame y s n then vs', [Trapping (memory_error e.at Memory.Bounds) @@ e.at] else if n_64 = 0L then vs', [] else if I64.le_u d_64 s_64 then vs', List.map (Lib.Fun.flip (@@) e.at) [ - Plain (Const (I64 d_64 @@ e.at)); - Plain (Const (I64 s_64 @@ e.at)); + Plain (Const (d @@ e.at)); + Plain (Const (s @@ e.at)); Plain (Load (y, {ty = I32T; align = 0; offset = 0L; pack = Some (Pack8, ZX)})); Plain (Store (x, {ty = I32T; align = 0; offset = 0L; pack = Some Pack8})); - Plain (Const (I64 (I64.add d_64 1L) @@ e.at)); - Plain (Const (I64 (I64.add s_64 1L) @@ e.at)); - Plain (Const (I64 (I64.sub n_64 1L) @@ e.at)); + Plain (Const (addr_add d 1L @@ e.at)); + Plain (Const (addr_add s 1L @@ e.at)); + Plain (Const (addr_sub n 1L @@ e.at)); Plain (MemoryCopy (x, y)); ] else (* d > s *) let n' = I64.sub n_64 1L in vs', List.map (Lib.Fun.flip (@@) e.at) [ - Plain (Const (I64 (I64.add d_64 n') @@ e.at)); - Plain (Const (I64 (I64.add s_64 n') @@ e.at)); + Plain (Const (addr_add d n' @@ e.at)); + Plain (Const (addr_add s n' @@ e.at)); Plain (Load (y, {ty = I32T; align = 0; offset = 0L; pack = Some (Pack8, ZX)})); Plain (Store (x, {ty = I32T; align = 0; offset = 0L; pack = Some Pack8})); - Plain (Const (I64 d_64 @@ e.at)); - Plain (Const (I64 s_64 @@ e.at)); - Plain (Const (I64 n' @@ e.at)); + Plain (Const (d @@ e.at)); + Plain (Const (s @@ e.at)); + Plain (Const (addr_sub n 1L @@ e.at)); Plain (MemoryCopy (x, y)); ] | MemoryInit (x, y), Num n :: Num s :: Num d :: vs' -> - let n_64 = Memory.address_of_num n in + let n_64 = addr_of_num n in + let s_64 = addr_of_num s in if mem_oob c.frame x d n || data_oob c.frame y s n then vs', [Trapping (memory_error e.at Memory.Bounds) @@ e.at] else if n_64 = 0L then vs', [] else let seg = data c.frame.inst y in - let s_64 = Memory.address_of_num s in - let d_64 = Memory.address_of_num d in let b = Data.load_byte seg s_64 in vs', List.map (Lib.Fun.flip (@@) e.at) [ - Plain (Const (I64 d_64 @@ e.at)); - Plain (Const (I64 (I64.of_int_u (Char.code b)) @@ e.at)); + Plain (Const (d @@ e.at)); + Plain (Const (I32 (I32.of_int_u (Char.code b)) @@ e.at)); Plain (Store (x, {ty = I64T; align = 0; offset = 0L; pack = Some Pack8})); - Plain (Const (I64 (I64.add d_64 1L) @@ e.at)); - Plain (Const (I64 (I64.add s_64 1L) @@ e.at)); - Plain (Const (I64 (I64.sub n_64 1L) @@ e.at)); + Plain (Const (addr_add d 1L @@ e.at)); + Plain (Const (addr_add s 1L @@ e.at)); + Plain (Const (addr_sub n 1L @@ e.at)); Plain (MemoryInit (x, y)); ] @@ -748,12 +727,14 @@ let rec step (c : config) : config = in Ref (Aggr.ArrayRef array) :: vs'', [] | ArrayNewElem (x, y), Num n :: Num s :: vs' -> + let n_64 = addr_of_num n in + let s_64 = addr_of_num s in if elem_oob c.frame y s n then vs', [Trapping (table_error e.at Table.Bounds) @@ e.at] else let seg = elem c.frame.inst y in - let s_64 = Table.index_of_num s in - let rs = Lib.List64.init (Table.index_of_num n) (fun i -> Elem.load seg (Int64.add s_64 i)) in + let rs = Lib.List64.init n_64 + (fun i -> Elem.load seg (Int64.add s_64 i)) in let args = List.map (fun r -> Ref r) rs in let array = try Aggr.alloc_array (type_ c.frame.inst x) args @@ -761,14 +742,16 @@ let rec step (c : config) : config = in Ref (Aggr.ArrayRef array) :: vs', [] | ArrayNewData (x, y), Num n :: Num s :: vs' -> + let n_64 = addr_of_num n in + let s_64 = addr_of_num s in if data_oob c.frame y s n then vs', [Trapping (memory_error e.at Memory.Bounds) @@ e.at] else let ArrayT (FieldT (_mut, st)) = array_type c.frame.inst x in let seg = data c.frame.inst y in - let args = Lib.List64.init (Memory.address_of_num n) + let args = Lib.List64.init n_64 (fun i -> - let a = I64.(add (Memory.address_of_num s) (mul i (I64.of_int_u (storage_size st)))) in + let a = I64.(add s_64 (mul i (I64.of_int_u (storage_size st)))) in Data.load_val_storage seg a st ) in @@ -884,18 +867,17 @@ let rec step (c : config) : config = vs', [Trapping "null array reference" @@ e.at] | ArrayInitData (x, y), - Num n :: Num s :: Num (I32 d) :: Ref (Aggr.ArrayRef a) :: vs' -> - let n_64 = Memory.address_of_num n in - if array_oob2 a d n then + Num (I32 n) :: Num s :: Num (I32 d) :: Ref (Aggr.ArrayRef a) :: vs' -> + let s_64 = addr_of_num s in + if array_oob a d n then vs', [Trapping "out of bounds array access" @@ e.at] - else if data_oob c.frame y s n then + else if data_oob c.frame y s (I64 (I64_convert.extend_i32_u n)) then vs', [Trapping (memory_error e.at Memory.Bounds) @@ e.at] - else if n_64 = 0L then + else if n = 0l then vs', [] else let ArrayT (FieldT (_mut, st)) = array_type c.frame.inst x in let seg = data c.frame.inst y in - let s_64 = Memory.address_of_num s in let v = Data.load_val_storage seg s_64 st in vs', List.map (Lib.Fun.flip (@@) e.at) [ Refer (Aggr.ArrayRef a); @@ -904,8 +886,8 @@ let rec step (c : config) : config = Plain (ArraySet x); Refer (Aggr.ArrayRef a); Plain (Const (I32 (I32.add d 1l) @@ e.at)); - Plain (Const (I64 (I64.add s_64 (I64.of_int_u (storage_size st))) @@ e.at)); - Plain (Const (I64 (I64.sub n_64 1L) @@ e.at)); + Plain (Const (addr_add s (I64.of_int_u (storage_size st)) @@ e.at)); + Plain (Const (I32 (I32.sub n 1l) @@ e.at)); Plain (ArrayInitData (x, y)); ] @@ -915,15 +897,15 @@ let rec step (c : config) : config = | ArrayInitElem (x, y), Num (I32 n) :: Num s :: Num (I32 d) :: Ref (Aggr.ArrayRef a) :: vs' -> + let s_64 = addr_of_num s in if array_oob a d n then vs', [Trapping "out of bounds array access" @@ e.at] - else if elem_oob2 c.frame y s n then + else if elem_oob c.frame y s (I64 (I64_convert.extend_i32_u n)) then vs', [Trapping (table_error e.at Table.Bounds) @@ e.at] else if n = 0l then vs', [] else let seg = elem c.frame.inst y in - let s_64 = Table.index_of_num s in let v = Ref (Elem.load seg s_64) in vs', List.map (Lib.Fun.flip (@@) e.at) [ Refer (Aggr.ArrayRef a); @@ -932,7 +914,7 @@ let rec step (c : config) : config = Plain (ArraySet x); Refer (Aggr.ArrayRef a); Plain (Const (I32 (I32.add d 1l) @@ e.at)); - Plain (Const (I64 (I64.add s_64 1L) @@ e.at)); + Plain (Const (addr_add s 1L @@ e.at)); Plain (Const (I32 (I32.sub n 1l) @@ e.at)); Plain (ArrayInitElem (x, y)); ] diff --git a/interpreter/host/spectest.ml b/interpreter/host/spectest.ml index aaf8f0665..8d6c039bf 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}, I32AddrType, (Null, FuncHT)) in + let tt = TableT (I32AT, {min = 10L; max = Some 20L}, (Null, FuncHT)) in ExternTable (Table.alloc tt (NullRef FuncHT)) let table64 = - let tt = TableT ({min = 10L; max = Some 20L}, I64AddrType, (Null, FuncHT)) in + let tt = TableT (I64AT, {min = 10L; max = Some 20L}, (Null, FuncHT)) in ExternTable (Table.alloc tt (NullRef FuncHT)) let memory = - let mt = MemoryT ({min = 1L; max = Some 2L}, I32AddrType) in + let mt = MemoryT (I32AT, {min = 1L; max = Some 2L}) in ExternMemory (Memory.alloc mt) let func f ft = diff --git a/interpreter/runtime/data.ml b/interpreter/runtime/data.ml index 785dcc608..66c2ad58d 100644 --- a/interpreter/runtime/data.ml +++ b/interpreter/runtime/data.ml @@ -1,6 +1,5 @@ type data = string ref type t = data -type address = Memory.address exception Bounds diff --git a/interpreter/runtime/data.mli b/interpreter/runtime/data.mli index f0074e366..86741d5c0 100644 --- a/interpreter/runtime/data.mli +++ b/interpreter/runtime/data.mli @@ -1,6 +1,7 @@ +open Value + type data type t = data -type address = Memory.address exception Bounds diff --git a/interpreter/runtime/elem.mli b/interpreter/runtime/elem.mli index b9b35a11d..d61442907 100644 --- a/interpreter/runtime/elem.mli +++ b/interpreter/runtime/elem.mli @@ -7,5 +7,5 @@ exception Bounds val alloc : ref_ list -> elem val size : elem -> Table.size -val load : elem -> Table.index -> ref_ (* raises Bounds *) +val load : elem -> address -> ref_ (* raises Bounds *) val drop : elem -> unit diff --git a/interpreter/runtime/memory.ml b/interpreter/runtime/memory.ml index 113a9cd25..3c3742d94 100644 --- a/interpreter/runtime/memory.ml +++ b/interpreter/runtime/memory.ml @@ -4,8 +4,7 @@ open Bigarray open Lib.Bigarray type size = int64 (* number of pages *) -type address = int64 -type offset = int64 +type offset = address type count = int32 type memory' = (int, int8_unsigned_elt, c_layout) Array1.t @@ -25,8 +24,12 @@ let valid_limits {min; max} = | None -> true | Some m -> I64.le_u min m -let create n at = - if I64.gt_u n 0x10000L && at = I32AddrType then raise SizeOverflow else +let valid_size at i = + match at with + | I32AT -> I64.le_u i 0xffffL + | I64AT -> true + +let create n = try let size = Int64.(mul n page_size) in let mem = Array1_64.create Int8_unsigned C_layout size in @@ -34,10 +37,11 @@ let create n at = mem with Out_of_memory -> raise OutOfMemory -let alloc (MemoryT (lim, at) as ty) = +let alloc (MemoryT (at, lim) as ty) = assert Free.((memory_type ty).types = Set.empty); + if not (valid_size at lim.min) then raise SizeOverflow; if not (valid_limits lim) then raise Type; - {ty; content = create lim.min at} + {ty; content = create lim.min} let bound mem = Array1_64.dim mem.content @@ -49,31 +53,21 @@ let type_of mem = mem.ty let addr_type_of mem = - let (MemoryT (_, at)) = type_of mem in at - -let address_of_num x = - match x with - | I32 i -> I64_convert.extend_i32_u i - | I64 i -> i - | _ -> raise Type - -let address_of_value x = - match x with - | Num n -> address_of_num n - | _ -> raise Type + let MemoryT (at, _) = type_of mem in at let grow mem delta = - let MemoryT (lim, at) = mem.ty in + let MemoryT (at, lim) = 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_size at new_size) then raise SizeOverflow else if not (valid_limits lim') then raise SizeLimit else - let after = create new_size (addr_type_of mem) in + let after = create new_size 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', at); + mem.ty <- MemoryT (at, lim'); mem.content <- after let load_byte mem a = diff --git a/interpreter/runtime/memory.mli b/interpreter/runtime/memory.mli index da9f468f8..9f0edc7cd 100644 --- a/interpreter/runtime/memory.mli +++ b/interpreter/runtime/memory.mli @@ -5,8 +5,7 @@ type memory type t = memory type size = int64 (* number of pages *) -type address = int64 -type offset = int64 +type offset = address type count = int32 exception Type @@ -22,8 +21,6 @@ val type_of : memory -> memory_type val addr_type_of : memory -> addr_type val size : memory -> size val bound : memory -> address -val address_of_value : value -> address -val address_of_num : num -> address val grow : memory -> size -> unit (* raises SizeLimit, SizeOverflow, OutOfMemory *) diff --git a/interpreter/runtime/table.ml b/interpreter/runtime/table.ml index b18dbd5df..d87807f4c 100644 --- a/interpreter/runtime/table.ml +++ b/interpreter/runtime/table.ml @@ -1,9 +1,8 @@ open Types open Value -type size = int64 -type index = int64 -type count = int32 +type size = address +type offset = address type table = {mutable ty : table_type; mutable content : ref_ array} type t = table @@ -19,17 +18,18 @@ let valid_limits {min; max} = | None -> true | Some m -> I64.le_u min m -let valid_addr at i = +let valid_size at i = match at with - | I32AddrType -> I64.le_u i 0xffff_ffffL - | I64AddrType -> true + | I32AT -> I64.le_u i 0xffff_ffffL + | I64AT -> true let create size r = try Lib.Array64.make size r with Out_of_memory | Invalid_argument _ -> raise OutOfMemory -let alloc (TableT (lim, at, t) as ty) r = +let alloc (TableT (at, lim, t) as ty) r = assert Free.((ref_type t).types = Set.empty); + if not (valid_size at lim.min) then raise SizeOverflow; if not (valid_limits lim) then raise Type; {ty; content = create lim.min r} @@ -40,26 +40,26 @@ let type_of tab = tab.ty let addr_type_of tab = - let (TableT (_, at, _)) = type_of tab in at + let TableT (at, _, _) = type_of tab in at -let index_of_num x = +let addr_of_num x = match x with | I64 i -> i | I32 i -> I64_convert.extend_i32_u i | _ -> raise Type let grow tab delta r = - let TableT (lim, at, t) = tab.ty in + let TableT (at, lim, 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_addr at new_size) then raise SizeOverflow else + if not (valid_size 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', at, t); + tab.ty <- TableT (at, lim', 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, _at, t) = tab.ty in + let TableT (_at, _lim, 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 6ebba6068..53caf5965 100644 --- a/interpreter/runtime/table.mli +++ b/interpreter/runtime/table.mli @@ -4,9 +4,8 @@ open Value type table type t = table -type size = int64 -type index = int64 -type count = int32 +type size = address +type offset = address exception Type exception Bounds @@ -18,10 +17,10 @@ val alloc : table_type -> ref_ -> table (* raises Type, OutOfMemory *) val type_of : table -> table_type val addr_type_of : table -> addr_type val size : table -> size -val index_of_num : num -> index +val addr_of_num : num -> address val grow : table -> size -> ref_ -> unit (* raises SizeOverflow, SizeLimit, OutOfMemory *) -val load : table -> index -> ref_ (* raises Bounds *) -val store : table -> index -> ref_ -> unit (* raises Type, Bounds *) -val blit : table -> index -> ref_ list -> unit (* raises Bounds *) +val load : table -> address -> ref_ (* raises Bounds *) +val store : table -> address -> ref_ -> unit (* raises Type, Bounds *) +val blit : table -> address -> ref_ list -> unit (* raises Bounds *) diff --git a/interpreter/runtime/value.ml b/interpreter/runtime/value.ml index 5381b67f1..75c5cd2c9 100644 --- a/interpreter/runtime/value.ml +++ b/interpreter/runtime/value.ml @@ -19,6 +19,8 @@ type t = value type ref_ += NullRef of heap_type +type address = I64.t + (* Injection & projection *) @@ -281,10 +283,22 @@ let storage_bits_of_val st v = let value_of_bool b = Num (I32 (if b then 1l else 0l)) -let value_of_addr at x = +let num_of_addr at i = match at with - | I64AddrType -> Num (I64 x) - | I32AddrType -> Num (I32 (Int64.to_int32 x)) + | I64AT -> I64 i + | I32AT -> I32 (I32_convert.wrap_i64 i) + +let addr_of_num x = + match x with + | I32 i -> I64_convert.extend_i32_u i + | I64 i -> i + | _ -> raise Type + +let addr_add n i = + num_of_addr (addr_type_of_num_type (type_of_num n)) (I64.add (addr_of_num n) i) +let addr_sub n i = + num_of_addr (addr_type_of_num_type (type_of_num n)) (I64.sub (addr_of_num n) i) + 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 efbbd58da..37ab763fe 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, _at, t)) = ref_type t -let memory_type (MemoryT (_lim, _at)) = empty +let table_type (TableT (_at, _lim, t)) = ref_type t +let memory_type (MemoryT (_at, _lim)) = empty let tag_type (TagT dt) = def_type dt let extern_type = function diff --git a/interpreter/syntax/operators.ml b/interpreter/syntax/operators.ml index 2f9879ef8..b6e65a360 100644 --- a/interpreter/syntax/operators.ml +++ b/interpreter/syntax/operators.ml @@ -15,6 +15,10 @@ let v128_const n = VecConst (V128 n.it @@ n.at) let ref_null t = RefNull t let ref_func x = RefFunc x +let at_const = function + | I32AT -> fun n -> i32_const (I32_convert.wrap_i64 n.it @@ n.at) + | I64AT -> i64_const + let unreachable = Unreachable let nop = Nop let drop = Drop diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml index fb5246445..f6a7fe245 100644 --- a/interpreter/syntax/types.ml +++ b/interpreter/syntax/types.ml @@ -12,6 +12,7 @@ type 'a limits = {min : 'a; max : 'a option} type var = StatX of type_idx | RecX of int32 +type addr_type = I32AT | I64AT type num_type = I32T | I64T | F32T | F64T type vec_type = V128T type heap_type = @@ -25,7 +26,6 @@ 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 addr_type = I32AddrType | I64AddrType 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 * addr_type * ref_type -type memory_type = MemoryT of Int64.t limits * addr_type +type table_type = TableT of addr_type * Int64.t limits * ref_type +type memory_type = MemoryT of addr_type * Int64.t limits type global_type = GlobalT of mut * val_type type tag_type = TagT of def_type type local_type = LocalT of init * val_type @@ -111,7 +111,17 @@ let defaultable = function | BotT -> assert false -(* Projections *) +(* Conversions & Projections *) + +let num_type_of_addr_type = function + | I32AT -> I32T + | I64AT -> I64T + +let addr_type_of_num_type = function + | I32T -> I32AT + | I64T -> I64AT + | _ -> assert false + let unpacked_storage_type = function | ValStorageT t -> t @@ -147,11 +157,6 @@ 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_addr_type = function - | I32AddrType -> I32T - | I64AddrType -> I64T - -let value_type_of_addr_type t = NumT (num_type_of_addr_type t) (* Substitution *) @@ -161,6 +166,8 @@ let subst_of dts = function | StatX x -> DefHT (Lib.List32.nth dts x) | RecX i -> VarHT (RecX i) +let subst_addr_type s t = t + let subst_num_type s t = t let subst_vec_type s t = t @@ -228,10 +235,10 @@ let subst_def_type s = function let subst_memory_type s = function - | MemoryT (lim, at) -> MemoryT (lim, at) + | MemoryT (at, lim) -> MemoryT (subst_addr_type s at, lim) let subst_table_type s = function - | TableT (lim, at, t) -> TableT (lim, at, subst_ref_type s t) + | TableT (at, lim, t) -> TableT (subst_addr_type s at, lim, subst_ref_type s t) let subst_global_type s = function | GlobalT (mut, t) -> GlobalT (mut, subst_val_type s t) @@ -294,6 +301,7 @@ let expand_def_type (dt : def_type) : str_type = let SubT (_, _, st) = unroll_def_type dt in st + (* String conversion *) let string_of_idx x = @@ -336,6 +344,9 @@ let string_of_num_type = function | F32T -> "f32" | F64T -> "f64" +let string_of_addr_type at = + string_of_num_type (num_type_of_addr_type at) + let string_of_vec_type = function | V128T -> "v128" @@ -365,9 +376,6 @@ and string_of_val_type = function | RefT t -> string_of_ref_type t | BotT -> "bot" -and string_of_addr_type t = - string_of_val_type (value_type_of_addr_type t) - and string_of_result_type = function | ts -> "[" ^ String.concat " " (List.map string_of_val_type ts) ^ "]" @@ -418,10 +426,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, at) -> string_of_num_type (num_type_of_addr_type at) ^ " " ^ string_of_limits lim + | MemoryT (at, lim) -> string_of_addr_type at ^ " " ^ string_of_limits lim let string_of_table_type = function - | TableT (lim, at, t) -> string_of_num_type (num_type_of_addr_type at) ^ " " ^ string_of_limits lim ^ " " ^ string_of_ref_type t + | TableT (at, lim, t) -> string_of_addr_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 6f7eccdaa..76c987f94 100644 --- a/interpreter/text/arrange.ml +++ b/interpreter/text/arrange.ml @@ -64,6 +64,7 @@ let mutability node = function | Cons -> node | Var -> Node ("mut", [node]) +let addr_type t = string_of_addr_type t let num_type t = string_of_num_type t let vec_type t = string_of_vec_type t let ref_type t = @@ -77,7 +78,6 @@ let ref_type t = | (Null, ExnHT) -> "exnref" | t -> string_of_ref_type t -let addr_type t = string_of_val_type (value_type_of_addr_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,13 +657,13 @@ let tag off i tag = ) let table off i tab = - let {ttype = TableT (lim, at, t); tinit} = tab.it in + let {ttype = TableT (at, lim, t); tinit} = tab.it in Node ("table $" ^ nat (off + i) ^ " " ^ addr_type at ^ " " ^ limits nat64 lim, atom ref_type t :: list instr tinit.it ) let memory off i mem = - let {mtype = MemoryT (lim, at)} = mem.it in + let {mtype = MemoryT (at, lim)} = mem.it in Node ("memory $" ^ nat (off + i) ^ " " ^ addr_type at ^ " " ^ limits nat64 lim, []) let is_elem_kind = function diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index df2ec4057..1fbeeeccc 100644 --- a/interpreter/text/parser.mly +++ b/interpreter/text/parser.mly @@ -264,39 +264,6 @@ let inline_func_type_explicit (c : context) x ft loc = error (at loc) "inline function type does not match explicit type"; x -let addr_type_of_num_type t loc = - match t with - | I32T -> I32AddrType - | I64T -> I64AddrType - | _ -> error (at loc) "illegal address type" - -let addr_type_of_value_type t loc = - match t with - | NumT t -> addr_type_of_num_type t loc - | _ -> error (at loc) "illegal address type" - -let memory_data init at c x loc = - let size = Int64.(div (add (of_int (String.length init)) 65535L) 65536L) in - let instr = match at with - | I32AddrType -> i32_const (0l @@ loc) - | I64AddrType -> i64_const (0L @@ loc) in - let offset = [instr @@ loc] @@ loc in - [{mtype = MemoryT ({min = size; max = Some size}, at)} @@ loc], - [{dinit = init; dmode = Active {index = x; offset} @@ loc} @@ loc], - [], [] - -let table_data tinit init at etype c x loc = - let instr = match at with - | I32AddrType -> i32_const (0l @@ loc) - | I64AddrType -> 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}, at, etype); tinit} @@ loc], - [{etype; einit; emode} @@ loc], - [], [] (* Custom annotations *) @@ -397,6 +364,14 @@ string_list : /* Types */ +%inline addr_type : + | NUM_TYPE + { match $1 with + | I32T -> I32AT + | I64T -> I64AT + | _ -> error (at $sloc) "malformed address type" } + | /* empty */ { I32AT } /* Sugar */ + null_opt : | /* empty */ { NoNull } | NULL { Null } @@ -501,12 +476,10 @@ 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, addr_type_of_value_type ($1 c) $sloc, $3 c) } - | limits ref_type { fun c -> TableT ($1, I32AddrType, $2 c) } + | addr_type limits ref_type { fun c -> TableT ($1, $2, $3 c) } memory_type : - | val_type limits { fun c -> MemoryT ($2, addr_type_of_value_type ($1 c) $sloc) } - | limits { fun c -> MemoryT ($1, I32AddrType) } + | addr_type limits { fun c -> MemoryT ($1, $2) } limits : | NAT { {min = nat64 $1 $loc($1); max = None} } @@ -1156,28 +1129,28 @@ table_fields : | inline_export table_fields /* Sugar */ { fun c x loc -> let tabs, elems, ims, exs = $2 c x loc in tabs, elems, ims, $1 (TableExport x) c :: exs } - | ref_type LPAR ELEM elem_expr elem_expr_list RPAR /* Sugar */ + | addr_type ref_type LPAR ELEM elem_expr elem_expr_list RPAR /* Sugar */ { fun c x loc -> - let offset = [i32_const (0l @@ loc) @@ loc] @@ loc in - let einit = $4 c :: $5 c in - let size = Lib.List32.length einit in - let size64 = Int64.of_int32 size in + let offset = [at_const $1 (0L @@ loc) @@ loc] @@ loc in + let einit = $5 c :: $6 c in + let size = Lib.List64.length einit in let emode = Active {index = x; offset} @@ loc in - let (_, ht) as etype = $1 c in + let (_, ht) as etype = $2 c in let tinit = [RefNull ht @@ loc] @@ loc in - [{ttype = TableT ({min = size64; max = Some size64}, I32AddrType, etype); tinit} @@ loc], + [{ttype = TableT ($1, {min = size; max = Some size}, 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 I32AddrType etype c x loc } - | val_type ref_type LPAR ELEM elem_var_list RPAR /* Sugar */ + | addr_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 (addr_type_of_value_type ($1 c) loc) etype c x loc } + let offset = [at_const $1 (0L @@ loc) @@ loc] @@ loc in + let einit = $5 c in + let size = Lib.List64.length einit in + let emode = Active {index = x; offset} @@ loc in + [{ttype = TableT ($1, {min = size; max = Some size}, etype); tinit} @@ loc], + [{etype; einit; emode} @@ loc], + [], [] } data : | LPAR DATA bind_var_opt string_list RPAR @@ -1208,10 +1181,13 @@ memory_fields : | inline_export memory_fields /* Sugar */ { 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 I32AddrType } - | val_type LPAR DATA string_list RPAR /* Sugar */ - { fun c x loc -> memory_data $4 (addr_type_of_value_type ($1 c) $sloc) c x loc } + | addr_type LPAR DATA string_list RPAR /* Sugar */ + { fun c x loc -> + let size = Int64.(div (add (of_int (String.length $4)) 65535L) 65536L) in + let offset = [at_const $1 (0L @@ loc) @@ loc] @@ loc in + [{mtype = MemoryT ($1, {min = size; max = Some size})} @@ loc], + [{dinit = $4; dmode = Active {index = x; offset} @@ loc} @@ loc], + [], [] } tag : | LPAR TAG bind_var_opt tag_fields RPAR diff --git a/interpreter/valid/match.ml b/interpreter/valid/match.ml index b2cc26630..7d889b899 100644 --- a/interpreter/valid/match.ml +++ b/interpreter/valid/match.ml @@ -161,11 +161,12 @@ 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, 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_table_type c (TableT (at1, lim1, t1)) (TableT (at2, lim2, t2)) = + at1 = at2 && match_limits c lim1 lim2 && + match_ref_type c t1 t2 && match_ref_type c t2 t1 -let match_memory_type c (MemoryT (lim1, at1)) (MemoryT (lim2, at2)) = - match_limits c lim1 lim2 && at1 = at2 +let match_memory_type c (MemoryT (at1, lim1)) (MemoryT (at2, lim2)) = + at1 = at2 && match_limits c lim1 lim2 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 6fc75ace7..ba4e8bb55 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -89,13 +89,13 @@ let refer_func (c : context) x = refer "function" c.refs.Free.funcs x (* Types *) -let check_limits le_u {min; max} range at msg = - require (le_u min range) at msg; +let check_limits {min; max} range at msg = + require (I64.le_u min range) at msg; match max with | None -> () | Some max -> - require (le_u max range) at msg; - require (le_u min max) at + require (I64.le_u max range) at msg; + require (I64.le_u min max) at "size minimum must not be greater than maximum" let check_num_type (c : context) (t : num_type) at = @@ -151,30 +151,29 @@ 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, _at, t) = tt in + let TableT (at_, lim, t) = tt in check_ref_type c t at; - match _at with - | I64AddrType -> - check_limits I64.le_u lim 0xffff_ffff_ffff_ffffL at - "table size must be at most 2^64-1" - | I32AddrType -> - check_limits I64.le_u lim 0xffff_ffffL at - "table size must be at most 2^32-1" + let sz, s = + match at_ with + | I32AT -> 0xffff_ffffL, "2^32-1 for i32" + | I64AT -> 0xffff_ffff_ffff_ffffL, "2^64-1 for i64" + in + check_limits lim sz at ("table size must be at most " ^ s) let check_memory_type (c : context) (mt : memory_type) at = - let MemoryT (lim, _at) = mt in - match _at with - | I32AddrType -> - check_limits I64.le_u lim 0x1_0000L at - "memory size must be at most 65536 pages (4GiB)" - | I64AddrType -> - check_limits I64.le_u lim 0x1_0000_0000_0000L at - "memory size must be at most 48 bits of pages" + let MemoryT (at_, lim) = mt in + let sz, s = + match at_ with + | I32AT -> 0x1_0000L, "2^16 pages (4 GiB) for i32" + | I64AT -> 0x1_0000_0000_0000L, "2^48 pages (256 TiB) for i64" + in + check_limits lim sz at ("memory size must be at most " ^ s) let check_global_type (c : context) (gt : global_type) at = let GlobalT (_mut, t) = gt in check_val_type c t at + let check_str_type (c : context) (st : str_type) at = match st with | DefStructT st -> check_struct_type c st at @@ -370,8 +369,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, _at) = memory c (0l @@ at) in - if _at = I32AddrType then + let MemoryT (at_, _lim) = memory c (0l @@ at) in + if at_ = I32AT then require (I64.lt_u memop.offset 0x1_0000_0000L) at "offset out of range"; memop.ty @@ -518,12 +517,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, at, t) = table c x in + let TableT (at, _lim, 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_addr_type at]) --> ts2, [] + (ts1 @ [NumT (num_type_of_addr_type at)]) --> ts2, [] | ReturnCall x -> let FuncT (ts1, ts2) = as_func_str_type (expand_def_type (func c x)) in @@ -542,13 +541,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, at, t) = table c x in + let TableT (at, _lim, 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_addr_type at]) -->... [], [] + (ts1 @ [NumT (num_type_of_addr_type at)]) -->... [], [] | Throw x -> let TagT dt = tag c x in @@ -588,102 +587,105 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in [t] --> [], [] | TableGet x -> - let TableT (_lim, at, rt) = table c x in - [value_type_of_addr_type at] --> [RefT rt], [] + let TableT (at, _lim, rt) = table c x in + [NumT (num_type_of_addr_type at)] --> [RefT rt], [] | TableSet x -> - let TableT (_lim, at, rt) = table c x in - [value_type_of_addr_type at; RefT rt] --> [], [] + let TableT (at, _lim, rt) = table c x in + [NumT (num_type_of_addr_type at); RefT rt] --> [], [] | TableSize x -> - let TableT (_lim, at, _rt) = table c x in - [] --> [value_type_of_addr_type at], [] + let TableT (at, _lim, _rt) = table c x in + [] --> [NumT (num_type_of_addr_type at)], [] | TableGrow x -> - let TableT (_lim, at, rt) = table c x in - [RefT rt; value_type_of_addr_type at] --> [value_type_of_addr_type at], [] + let TableT (at, _lim, rt) = table c x in + [RefT rt; NumT (num_type_of_addr_type at)] --> + [NumT (num_type_of_addr_type at)], [] | TableFill x -> - let TableT (_lim, at, rt) = table c x in - [value_type_of_addr_type at; RefT rt; value_type_of_addr_type at] --> [], [] + let TableT (at, _lim, rt) = table c x in + [NumT (num_type_of_addr_type at); RefT rt; + NumT (num_type_of_addr_type at)] --> [], [] | TableCopy (x, y) -> - 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 + let TableT (at1, _lim1, t1) = table c x in + let TableT (at2, _lim2, t2) = table c y 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_addr_type at1; value_type_of_addr_type at2; value_type_of_addr_type at_min] --> [], [] + [NumT (num_type_of_addr_type at1); NumT (num_type_of_addr_type at2); + NumT (num_type_of_addr_type (min at1 at2))] --> [], [] | TableInit (x, y) -> - let TableT (_lim1, at, t1) = table c x in + let TableT (at, _lim1, 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_addr_type at; NumT I32T; NumT I32T] --> [], [] + [NumT (num_type_of_addr_type at); NumT I32T; NumT I32T] --> [], [] | ElemDrop x -> ignore (elem c x); [] --> [], [] | Load (x, memop) -> - let MemoryT (_lim, at) = memory c x in + let MemoryT (at, _lim) = memory c x in let t = check_memop c memop num_size (Lib.Option.map fst) e.at in - [value_type_of_addr_type at] --> [NumT t], [] + [NumT (num_type_of_addr_type at)] --> [NumT t], [] | Store (x, memop) -> - let MemoryT (_lim, at) = memory c x in + let MemoryT (at, _lim) = memory c x in let t = check_memop c memop num_size (fun sz -> sz) e.at in - [value_type_of_addr_type at; NumT t] --> [], [] + [NumT (num_type_of_addr_type at); NumT t] --> [], [] | VecLoad (x, memop) -> - let MemoryT (_lim, at) = memory c x in + let MemoryT (at, _lim) = memory c x in let t = check_memop c memop vec_size (Lib.Option.map fst) e.at in - [value_type_of_addr_type at] --> [VecT t], [] + [NumT (num_type_of_addr_type at)] --> [VecT t], [] | VecStore (x, memop) -> - let MemoryT (_lim, at) = memory c x in + let MemoryT (at, _lim) = memory c x in let t = check_memop c memop vec_size (fun _ -> None) e.at in - [value_type_of_addr_type at; VecT t] --> [], [] + [NumT (num_type_of_addr_type at); VecT t] --> [], [] | VecLoadLane (x, memop, i) -> - let MemoryT (_lim, at) = memory c x in + let MemoryT (at, _lim) = 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_addr_type at; VecT t] --> [VecT t], [] + [NumT (num_type_of_addr_type at); VecT t] --> [VecT t], [] | VecStoreLane (x, memop, i) -> - let MemoryT (_lim, at) = memory c x in + let MemoryT (at, _lim) = 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_addr_type at; VecT t] --> [], [] + [NumT (num_type_of_addr_type at); VecT t] --> [], [] | MemorySize x -> - let MemoryT (_lim, at) = memory c x in - [] --> [value_type_of_addr_type at], [] + let MemoryT (at, _lim) = memory c x in + [] --> [NumT (num_type_of_addr_type at)], [] | MemoryGrow x -> - let MemoryT (_lim, at) = memory c x in - [value_type_of_addr_type at] --> [value_type_of_addr_type at], [] + let MemoryT (at, _lim) = memory c x in + [NumT (num_type_of_addr_type at)] --> [NumT (num_type_of_addr_type at)], [] | MemoryFill x -> - let MemoryT (_lim, at) = memory c x in - [value_type_of_addr_type at; NumT I32T; value_type_of_addr_type at] --> [], [] + let MemoryT (at, _lim) = memory c x in + [NumT (num_type_of_addr_type at); NumT I32T; + NumT (num_type_of_addr_type at)] --> [], [] | MemoryCopy (x, y)-> - 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_addr_type at1; value_type_of_addr_type at2; value_type_of_addr_type at_min] --> [], [] + let MemoryT (at1, _lib1) = memory c x in + let MemoryT (at2, _lib2) = memory c y in + [NumT (num_type_of_addr_type at1); NumT (num_type_of_addr_type at2); + NumT (num_type_of_addr_type (min at1 at2))] --> [], [] | MemoryInit (x, y) -> - let MemoryT (_lib, at) = memory c x in + let MemoryT (at, _lib) = memory c x in let () = data c y in - [value_type_of_addr_type at; NumT I32T; NumT I32T] --> [], [] + [NumT (num_type_of_addr_type at); NumT I32T; NumT I32T] --> [], [] | DataDrop x -> let () = data c x in @@ -1029,7 +1031,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, _at, rt) = ttype in + let TableT (_at, _lim, rt) = ttype in check_table_type c ttype tab.at; check_const c tinit (RefT rt); {c with tables = c.tables @ [ttype]} @@ -1048,11 +1050,11 @@ let check_elem_mode (c : context) (t : ref_type) (mode : segment_mode) = match mode.it with | Passive -> () | Active {index; offset} -> - let TableT (_lim, at, et) = table c index in + let TableT (at, _lim, 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_addr_type at) + check_const c offset (NumT (num_type_of_addr_type at)) | Declarative -> () let check_elem (c : context) (seg : elem_segment) : context = @@ -1066,8 +1068,8 @@ let check_data_mode (c : context) (mode : segment_mode) = match mode.it with | Passive -> () | Active {index; offset} -> - let MemoryT (_, at) = memory c index in - check_const c offset (value_type_of_addr_type at) + let MemoryT (at, _) = memory c index in + check_const c offset (NumT (num_type_of_addr_type at)) | Declarative -> assert false let check_data (c : context) (seg : data_segment) : context = diff --git a/test/core/memory.wast b/test/core/memory.wast index 1c57a8f35..e01170a8f 100644 --- a/test/core/memory.wast +++ b/test/core/memory.wast @@ -50,40 +50,53 @@ ) (assert_invalid (module (memory 65537)) - "memory size must be at most 65536 pages (4GiB)" + "memory size" ) (assert_invalid (module (memory 2147483648)) - "memory size must be at most 65536 pages (4GiB)" + "memory size" ) (assert_invalid (module (memory 4294967295)) - "memory size must be at most 65536 pages (4GiB)" + "memory size" ) (assert_invalid (module (memory 0 65537)) - "memory size must be at most 65536 pages (4GiB)" + "memory size" ) (assert_invalid (module (memory 0 2147483648)) - "memory size must be at most 65536 pages (4GiB)" + "memory size" ) (assert_invalid (module (memory 0 4294967295)) - "memory size must be at most 65536 pages (4GiB)" + "memory size" ) (assert_invalid - (module quote "(memory 0x1_0000_0000)") - "memory size must be at most 65536 pages (4GiB)" + (module (memory 0x1_0000_0000)) + "memory size" ) (assert_invalid - (module quote "(memory 0x1_0000_0000 0x1_0000_0000)") - "memory size must be at most 65536 pages (4GiB)" + (module (memory 0x1_0000_0000 0x1_0000_0000)) + "memory size" ) (assert_invalid - (module quote "(memory 0 0x1_0000_0000)") - "memory size must be at most 65536 pages (4GiB)" + (module (memory 0 0x1_0000_0000)) + "memory size" +) + +(assert_invalid + (module (memory (import "M" "m") 0x1_0000_0000)) + "memory size" +) +(assert_invalid + (module (memory (import "M" "m") 0x1_0000_0000 0x1_0000_0000)) + "memory size" +) +(assert_invalid + (module (memory (import "M" "m") 0 0x1_0000_0000)) + "memory size" ) (module diff --git a/test/core/memory64.wast b/test/core/memory64.wast index 41e1bf034..ba3b24233 100644 --- a/test/core/memory64.wast +++ b/test/core/memory64.wast @@ -48,6 +48,24 @@ "size minimum must not be greater than maximum" ) +(assert_invalid + (module (memory i64 0x1_0000_0000_0001)) + "memory size" +) +(assert_invalid + (module (memory i64 0 0x1_0000_0000_0001)) + "memory size" +) + +(assert_invalid + (module (memory (import "M" "m") i64 0x1_0000_0000_0001)) + "memory size" +) +(assert_invalid + (module (memory (import "M" "m") i64 0 0x1_0000_0000_0001)) + "memory size" +) + (module (memory i64 1) (data (i64.const 0) "ABC\a7D") (data (i64.const 20) "WASM") diff --git a/test/core/table.wast b/test/core/table.wast index 8648df070..a0feefff9 100644 --- a/test/core/table.wast +++ b/test/core/table.wast @@ -33,15 +33,15 @@ (assert_invalid (module quote "(table 0x1_0000_0000 funcref)") - "table size must be at most 2^32-1" + "table size" ) (assert_invalid (module quote "(table 0x1_0000_0000 0x1_0000_0000 funcref)") - "table size must be at most 2^32-1" + "table size" ) (assert_invalid (module quote "(table 0 0x1_0000_0000 funcref)") - "table size must be at most 2^32-1" + "table size" ) ;; Same as above but with i64 address types