diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml index 433b092ed..c4b0947bd 100644 --- a/interpreter/binary/decode.ml +++ b/interpreter/binary/decode.ml @@ -296,7 +296,7 @@ let globaltype s = let memorytype s = let at, lim = limits u64 s in - MemoryT (at, lim) + MemoryT (at, lim, PageT 0x10000) (* TODO(custom-page-sizes) *) let tabletype s = let t = reftype s in diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml index 884592772..651bee528 100644 --- a/interpreter/binary/encode.ml +++ b/interpreter/binary/encode.ml @@ -194,7 +194,7 @@ struct | GlobalT (mut, t) -> valtype t; mutability mut let memorytype = function - | MemoryT (at, lim) -> limits at lim + | MemoryT (at, lim, pt) -> limits at lim (* TODO(custom-page-sizes) *) let tabletype = function | TableT (at, lim, t) -> reftype t; limits at lim diff --git a/interpreter/host/spectest.ml b/interpreter/host/spectest.ml index 03ad95424..82ee4be45 100644 --- a/interpreter/host/spectest.ml +++ b/interpreter/host/spectest.ml @@ -28,7 +28,7 @@ let table64 = ExternTable (Table.alloc tt (NullRef FuncHT)) let memory = - let mt = MemoryT (I32AT, {min = 1L; max = Some 2L}) in + let mt = MemoryT (I32AT, {min = 1L; max = Some 2L}, PageT 0x10000) in ExternMemory (Memory.alloc mt) let func f ts1 ts2 = diff --git a/interpreter/runtime/memory.ml b/interpreter/runtime/memory.ml index 7914ebecc..9e73d6d2a 100644 --- a/interpreter/runtime/memory.ml +++ b/interpreter/runtime/memory.ml @@ -29,34 +29,37 @@ let valid_size at i = | I32AT -> I64.le_u i 0xffffL | I64AT -> true -let create n = +let create n (PageT ps) = try - let size = Int64.(mul n page_size) in + let size = Int64.(mul n (Int64.of_int ps)) 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 (at, lim) as ty) = +let alloc (MemoryT (at, lim, pt) as ty) = assert Free.((memorytype 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} + {ty; content = create lim.min pt} let bound mem = Array1_64.dim mem.content +let pagesize mem = + let MemoryT (_, _, PageT x) = mem.ty in Int64.of_int x + let size mem = - Int64.(div (bound mem) page_size) + Int64.(div (bound mem) (pagesize mem)) let type_of mem = mem.ty let addrtype_of mem = - let MemoryT (at, _) = type_of mem in at + let MemoryT (at, _, _) = type_of mem in at let grow mem delta = - let MemoryT (at, lim) = mem.ty in + let MemoryT (at, lim, pt) = mem.ty in assert (lim.min = size mem); let old_size = lim.min in let new_size = Int64.add old_size delta in @@ -64,10 +67,10 @@ let grow mem delta = 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 in + let after = create new_size pt 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 (at, lim'); + mem.ty <- MemoryT (at, lim', pt); mem.content <- after let load_byte mem a = diff --git a/interpreter/syntax/free.ml b/interpreter/syntax/free.ml index a5c9f9b3c..d2eb30789 100644 --- a/interpreter/syntax/free.ml +++ b/interpreter/syntax/free.ml @@ -118,7 +118,7 @@ and deftype = function let tagtype (TagT ut) = typeuse ut let globaltype (GlobalT (_mut, t)) = valtype t -let memorytype (MemoryT (_at, _lim)) = empty +let memorytype (MemoryT (_at, _pt, _lim)) = empty let tabletype (TableT (_at, _lim, t)) = reftype t let externtype = function diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml index fda781359..bd8066a87 100644 --- a/interpreter/syntax/types.ml +++ b/interpreter/syntax/types.ml @@ -13,6 +13,7 @@ type limits = {min : int64; max : int64 option} type typeuse = Idx of typeidx | Rec of int32 | Def of deftype and addrtype = I32AT | I64AT +and pagetype = PageT of int and numtype = I32T | I64T | F32T | F64T and vectype = V128T and heaptype = @@ -39,7 +40,7 @@ and deftype = DefT of rectype * int32 type tagtype = TagT of typeuse type globaltype = GlobalT of mut * valtype -type memorytype = MemoryT of addrtype * limits +type memorytype = MemoryT of addrtype * limits * pagetype type tabletype = TableT of addrtype * limits * reftype type localtype = LocalT of init * valtype type externtype = @@ -219,7 +220,7 @@ let subst_globaltype s = function | GlobalT (mut, t) -> GlobalT (mut, subst_valtype s t) let subst_memorytype s = function - | MemoryT (at, lim) -> MemoryT (subst_addrtype s at, lim) + | MemoryT (at, pt, lim) -> MemoryT (subst_addrtype s at, pt, lim) let subst_tabletype s = function | TableT (at, lim, t) -> TableT (subst_addrtype s at, lim, subst_reftype s t) @@ -322,6 +323,9 @@ let string_of_numtype = function let string_of_addrtype at = string_of_numtype (numtype_of_addrtype at) +let string_of_pagetype = function + | PageT x -> string_of_int x + let string_of_vectype = function | V128T -> "v128" @@ -408,7 +412,7 @@ let string_of_globaltype = function | GlobalT (mut, t) -> string_of_mut (string_of_valtype t) mut let string_of_memorytype = function - | MemoryT (at, lim) -> string_of_addrtype at ^ " " ^ string_of_limits lim + | MemoryT (at, lim, pt) -> string_of_addrtype at ^ " " ^ string_of_limits lim ^ " " ^ string_of_pagetype pt let string_of_tabletype = function | TableT (at, lim, t) -> diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml index 1ab2c222d..d9c987015 100644 --- a/interpreter/text/arrange.ml +++ b/interpreter/text/arrange.ml @@ -118,8 +118,8 @@ let tagtype (TagT ut) = let globaltype (GlobalT (mut, t)) = [mutability (atom string_of_valtype t) mut] -let memorytype (MemoryT (at, lim)) = - [Atom (addrtype at ^ " " ^ limits nat64 lim)] +let memorytype (MemoryT (at, lim, pt)) = + [Atom (addrtype at ^ " " ^ limits nat64 lim)] (* TODO(custom-page-sizes) *) let tabletype (TableT (at, lim, t)) = [Atom (addrtype at ^ " " ^ limits nat64 lim); atom reftype t] diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index 194590270..0ee8020c3 100644 --- a/interpreter/text/parser.mly +++ b/interpreter/text/parser.mly @@ -466,7 +466,7 @@ tabletype : | addrtype limits reftype { fun c -> TableT ($1, $2, $3 c) } memorytype : - | addrtype limits { fun c -> MemoryT ($1, $2) } + | addrtype limits { fun c -> MemoryT ($1, $2, PageT 0x10000) } limits : | NAT { {min = nat64 $1 $loc($1); max = None} } @@ -1130,7 +1130,7 @@ memory_fields : { 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 - [Memory (MemoryT ($1, {min = size; max = Some size})) @@ loc], + [Memory (MemoryT ($1, {min = size; max = Some size}, PageT 0x10000)) @@ loc], [Data ($4, Active (x, offset) @@ loc) @@ loc], [], [] } diff --git a/interpreter/valid/match.ml b/interpreter/valid/match.ml index e82706478..cd4083fad 100644 --- a/interpreter/valid/match.ml +++ b/interpreter/valid/match.ml @@ -165,8 +165,8 @@ let match_globaltype c (GlobalT (mut1, t1)) (GlobalT (mut2, t2)) = | Cons -> true | Var -> match_valtype c t2 t1 -let match_memorytype c (MemoryT (at1, lim1)) (MemoryT (at2, lim2)) = - at1 = at2 && match_limits c lim1 lim2 +let match_memorytype c (MemoryT (at1, lim1, pt1)) (MemoryT (at2, lim2, pt2)) = + at1 = at2 && pt1 = pt2 && match_limits c lim1 lim2 let match_tabletype c (TableT (at1, lim1, t1)) (TableT (at2, lim2, t2)) = at1 = at2 && match_limits c lim1 lim2 && diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index cb41335b8..c22a1d0cf 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -104,6 +104,9 @@ let check_limits {min; max} range at msg = require (I64.le_u min max) at "size minimum must not be greater than maximum" +let check_pagetype (PageT ps) at = + require (ps = 0x10000 || ps = 1) at "page size must be 1 or 64KiB" + let check_numtype (c : context) (t : numtype) at = () @@ -196,13 +199,14 @@ let check_globaltype (c : context) (gt : globaltype) at = check_valtype c t at let check_memorytype (c : context) (mt : memorytype) at = - let MemoryT (at_, lim) = mt in + let MemoryT (at_, lim, pt) = 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) + check_limits lim sz at ("memory size must be at most " ^ s); + check_pagetype pt at let check_tabletype (c : context) (tt : tabletype) at = let TableT (at_, lim, t) = tt in @@ -384,7 +388,7 @@ 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 (at_, _lim) = memory c (0l @@ at) in + let MemoryT (at_, _lim, _pt) = memory c (0l @@ at) in if at_ = I32AT then require (I64.lt_u memop.offset 0x1_0000_0000L) at "offset out of range"; @@ -648,60 +652,60 @@ let rec check_instr (c : context) (e : instr) (s : infer_resulttype) : infer_ins [] --> [], [] | Load (x, memop) -> - let MemoryT (at, _lim) = memory c x in + let MemoryT (at, _lim, _pt) = memory c x in let t = check_memop c memop num_size (Lib.Option.map fst) e.at in [NumT (numtype_of_addrtype at)] --> [NumT t], [] | Store (x, memop) -> - let MemoryT (at, _lim) = memory c x in + let MemoryT (at, _lim, _pt) = memory c x in let t = check_memop c memop num_size (fun sz -> sz) e.at in [NumT (numtype_of_addrtype at); NumT t] --> [], [] | VecLoad (x, memop) -> - let MemoryT (at, _lim) = memory c x in + let MemoryT (at, _lim, _pt) = memory c x in let t = check_memop c memop vec_size (Lib.Option.map fst) e.at in [NumT (numtype_of_addrtype at)] --> [VecT t], [] | VecStore (x, memop) -> - let MemoryT (at, _lim) = memory c x in + let MemoryT (at, _lim, _pt) = memory c x in let t = check_memop c memop vec_size (fun _ -> None) e.at in [NumT (numtype_of_addrtype at); VecT t] --> [], [] | VecLoadLane (x, memop, i) -> - let MemoryT (at, _lim) = memory c x in + let MemoryT (at, _lim, _pt) = memory c x in let t = check_memop c memop vec_size (fun sz -> Some sz) e.at in require (I8.to_int_u i < vec_size t / Pack.packed_size memop.pack) e.at "invalid lane index"; [NumT (numtype_of_addrtype at); VecT t] --> [VecT t], [] | VecStoreLane (x, memop, i) -> - let MemoryT (at, _lim) = memory c x in + let MemoryT (at, _lim, _pt) = memory c x in let t = check_memop c memop vec_size (fun sz -> Some sz) e.at in require (I8.to_int_u i < vec_size t / Pack.packed_size memop.pack) e.at "invalid lane index"; [NumT (numtype_of_addrtype at); VecT t] --> [], [] | MemorySize x -> - let MemoryT (at, _lim) = memory c x in + let MemoryT (at, _lim, _pt) = memory c x in [] --> [NumT (numtype_of_addrtype at)], [] | MemoryGrow x -> - let MemoryT (at, _lim) = memory c x in + let MemoryT (at, _lim, _pt) = memory c x in [NumT (numtype_of_addrtype at)] --> [NumT (numtype_of_addrtype at)], [] | MemoryFill x -> - let MemoryT (at, _lim) = memory c x in + let MemoryT (at, _lim, _pt) = memory c x in [NumT (numtype_of_addrtype at); NumT I32T; NumT (numtype_of_addrtype at)] --> [], [] | MemoryCopy (x, y)-> - let MemoryT (at1, _lib1) = memory c x in - let MemoryT (at2, _lib2) = memory c y in + let MemoryT (at1, _pt, _lib1) = memory c x in + let MemoryT (at2, _pt, _lib2) = memory c y in [NumT (numtype_of_addrtype at1); NumT (numtype_of_addrtype at2); NumT (numtype_of_addrtype (min at1 at2))] --> [], [] | MemoryInit (x, y) -> - let MemoryT (at, _lib) = memory c x in + let MemoryT (at, _pt, _lib) = memory c x in let () = data c y in [NumT (numtype_of_addrtype at); NumT I32T; NumT I32T] --> [], [] @@ -1071,7 +1075,7 @@ let check_datamode (c : context) (mode : segmentmode) = match mode.it with | Passive -> () | Active (x, offset) -> - let MemoryT (at, _) = memory c x in + let MemoryT (at, _, _) = memory c x in check_const c offset (NumT (numtype_of_addrtype at)) | Declarative -> assert false