Skip to content

[interpreter] Add page type to IR of memory types #50

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
titzer merged 5 commits into from
Dec 3, 2025
Merged

[interpreter] Add page type to IR of memory types #50

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
fa78b0f
Add page type to IR of memory types
titzer Dec 2, 2025
32012ae
Add pagesize calculations
titzer Dec 2, 2025
68879dd
Move pagesize after limits
titzer Dec 2, 2025
1d7740e
Check pagesize against 1 or 64KiB
titzer Dec 3, 2025
0588ee4
Rename to check_pagetype
titzer Dec 3, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion interpreter/binary/decode.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion interpreter/binary/encode.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion interpreter/host/spectest.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down
21 changes: 12 additions & 9 deletions interpreter/runtime/memory.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,45 +29,48 @@ 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
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 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 =
Expand Down
2 changes: 1 addition & 1 deletion interpreter/syntax/free.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
10 changes: 7 additions & 3 deletions interpreter/syntax/types.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand All @@ -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 =
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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"

Expand Down Expand Up @@ -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) ->
Expand Down
4 changes: 2 additions & 2 deletions interpreter/text/arrange.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
4 changes: 2 additions & 2 deletions interpreter/text/parser.mly
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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} }
Expand Down Expand Up @@ -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],
[], [] }

Expand Down
4 changes: 2 additions & 2 deletions interpreter/valid/match.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 &&
Expand Down
36 changes: 20 additions & 16 deletions interpreter/valid/valid.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
()

Expand Down Expand Up @@ -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 =
Copy link
Member

@rossberg rossberg Dec 3, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Don't you need to check here that pt is either 1 or 0x10000?

Copy link
Contributor Author

@titzer titzer Dec 3, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done.

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
Expand Down Expand Up @@ -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";
Expand Down Expand Up @@ -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] --> [], []

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

Expand Down