Skip to content

Commit 1afa12a

Browse files
authored
[interpreter] Add page type to IR of memory types (#50)
2 parents d755d6f + 0588ee4 commit 1afa12a

File tree

10 files changed

+49
-38
lines changed

10 files changed

+49
-38
lines changed

interpreter/binary/decode.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -296,7 +296,7 @@ let globaltype s =
296296

297297
let memorytype s =
298298
let at, lim = limits u64 s in
299-
MemoryT (at, lim)
299+
MemoryT (at, lim, PageT 0x10000) (* TODO(custom-page-sizes) *)
300300

301301
let tabletype s =
302302
let t = reftype s in

interpreter/binary/encode.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -194,7 +194,7 @@ struct
194194
| GlobalT (mut, t) -> valtype t; mutability mut
195195

196196
let memorytype = function
197-
| MemoryT (at, lim) -> limits at lim
197+
| MemoryT (at, lim, pt) -> limits at lim (* TODO(custom-page-sizes) *)
198198

199199
let tabletype = function
200200
| TableT (at, lim, t) -> reftype t; limits at lim

interpreter/host/spectest.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ let table64 =
2828
ExternTable (Table.alloc tt (NullRef FuncHT))
2929

3030
let memory =
31-
let mt = MemoryT (I32AT, {min = 1L; max = Some 2L}) in
31+
let mt = MemoryT (I32AT, {min = 1L; max = Some 2L}, PageT 0x10000) in
3232
ExternMemory (Memory.alloc mt)
3333

3434
let func f ts1 ts2 =

interpreter/runtime/memory.ml

Lines changed: 12 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -29,45 +29,48 @@ let valid_size at i =
2929
| I32AT -> I64.le_u i 0xffffL
3030
| I64AT -> true
3131

32-
let create n =
32+
let create n (PageT ps) =
3333
try
34-
let size = Int64.(mul n page_size) in
34+
let size = Int64.(mul n (Int64.of_int ps)) in
3535
let mem = Array1_64.create Int8_unsigned C_layout size in
3636
Array1.fill mem 0;
3737
mem
3838
with Out_of_memory -> raise OutOfMemory
3939

40-
let alloc (MemoryT (at, lim) as ty) =
40+
let alloc (MemoryT (at, lim, pt) as ty) =
4141
assert Free.((memorytype ty).types = Set.empty);
4242
if not (valid_size at lim.min) then raise SizeOverflow;
4343
if not (valid_limits lim) then raise Type;
44-
{ty; content = create lim.min}
44+
{ty; content = create lim.min pt}
4545

4646
let bound mem =
4747
Array1_64.dim mem.content
4848

49+
let pagesize mem =
50+
let MemoryT (_, _, PageT x) = mem.ty in Int64.of_int x
51+
4952
let size mem =
50-
Int64.(div (bound mem) page_size)
53+
Int64.(div (bound mem) (pagesize mem))
5154

5255
let type_of mem =
5356
mem.ty
5457

5558
let addrtype_of mem =
56-
let MemoryT (at, _) = type_of mem in at
59+
let MemoryT (at, _, _) = type_of mem in at
5760

5861
let grow mem delta =
59-
let MemoryT (at, lim) = mem.ty in
62+
let MemoryT (at, lim, pt) = mem.ty in
6063
assert (lim.min = size mem);
6164
let old_size = lim.min in
6265
let new_size = Int64.add old_size delta in
6366
if I64.gt_u old_size new_size then raise SizeOverflow else
6467
let lim' = {lim with min = new_size} in
6568
if not (valid_size at new_size) then raise SizeOverflow else
6669
if not (valid_limits lim') then raise SizeLimit else
67-
let after = create new_size in
70+
let after = create new_size pt in
6871
let dim = Array1_64.dim mem.content in
6972
Array1.blit (Array1_64.sub mem.content 0L dim) (Array1_64.sub after 0L dim);
70-
mem.ty <- MemoryT (at, lim');
73+
mem.ty <- MemoryT (at, lim', pt);
7174
mem.content <- after
7275

7376
let load_byte mem a =

interpreter/syntax/free.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -118,7 +118,7 @@ and deftype = function
118118

119119
let tagtype (TagT ut) = typeuse ut
120120
let globaltype (GlobalT (_mut, t)) = valtype t
121-
let memorytype (MemoryT (_at, _lim)) = empty
121+
let memorytype (MemoryT (_at, _pt, _lim)) = empty
122122
let tabletype (TableT (_at, _lim, t)) = reftype t
123123

124124
let externtype = function

interpreter/syntax/types.ml

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ type limits = {min : int64; max : int64 option}
1313
type typeuse = Idx of typeidx | Rec of int32 | Def of deftype
1414

1515
and addrtype = I32AT | I64AT
16+
and pagetype = PageT of int
1617
and numtype = I32T | I64T | F32T | F64T
1718
and vectype = V128T
1819
and heaptype =
@@ -39,7 +40,7 @@ and deftype = DefT of rectype * int32
3940

4041
type tagtype = TagT of typeuse
4142
type globaltype = GlobalT of mut * valtype
42-
type memorytype = MemoryT of addrtype * limits
43+
type memorytype = MemoryT of addrtype * limits * pagetype
4344
type tabletype = TableT of addrtype * limits * reftype
4445
type localtype = LocalT of init * valtype
4546
type externtype =
@@ -219,7 +220,7 @@ let subst_globaltype s = function
219220
| GlobalT (mut, t) -> GlobalT (mut, subst_valtype s t)
220221

221222
let subst_memorytype s = function
222-
| MemoryT (at, lim) -> MemoryT (subst_addrtype s at, lim)
223+
| MemoryT (at, pt, lim) -> MemoryT (subst_addrtype s at, pt, lim)
223224

224225
let subst_tabletype s = function
225226
| TableT (at, lim, t) -> TableT (subst_addrtype s at, lim, subst_reftype s t)
@@ -322,6 +323,9 @@ let string_of_numtype = function
322323
let string_of_addrtype at =
323324
string_of_numtype (numtype_of_addrtype at)
324325

326+
let string_of_pagetype = function
327+
| PageT x -> string_of_int x
328+
325329
let string_of_vectype = function
326330
| V128T -> "v128"
327331

@@ -408,7 +412,7 @@ let string_of_globaltype = function
408412
| GlobalT (mut, t) -> string_of_mut (string_of_valtype t) mut
409413

410414
let string_of_memorytype = function
411-
| MemoryT (at, lim) -> string_of_addrtype at ^ " " ^ string_of_limits lim
415+
| MemoryT (at, lim, pt) -> string_of_addrtype at ^ " " ^ string_of_limits lim ^ " " ^ string_of_pagetype pt
412416

413417
let string_of_tabletype = function
414418
| TableT (at, lim, t) ->

interpreter/text/arrange.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -118,8 +118,8 @@ let tagtype (TagT ut) =
118118
let globaltype (GlobalT (mut, t)) =
119119
[mutability (atom string_of_valtype t) mut]
120120

121-
let memorytype (MemoryT (at, lim)) =
122-
[Atom (addrtype at ^ " " ^ limits nat64 lim)]
121+
let memorytype (MemoryT (at, lim, pt)) =
122+
[Atom (addrtype at ^ " " ^ limits nat64 lim)] (* TODO(custom-page-sizes) *)
123123

124124
let tabletype (TableT (at, lim, t)) =
125125
[Atom (addrtype at ^ " " ^ limits nat64 lim); atom reftype t]

interpreter/text/parser.mly

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -466,7 +466,7 @@ tabletype :
466466
| addrtype limits reftype { fun c -> TableT ($1, $2, $3 c) }
467467

468468
memorytype :
469-
| addrtype limits { fun c -> MemoryT ($1, $2) }
469+
| addrtype limits { fun c -> MemoryT ($1, $2, PageT 0x10000) }
470470

471471
limits :
472472
| NAT { {min = nat64 $1 $loc($1); max = None} }
@@ -1130,7 +1130,7 @@ memory_fields :
11301130
{ fun c x loc ->
11311131
let size = Int64.(div (add (of_int (String.length $4)) 65535L) 65536L) in
11321132
let offset = [at_const $1 (0L @@ loc) @@ loc] @@ loc in
1133-
[Memory (MemoryT ($1, {min = size; max = Some size})) @@ loc],
1133+
[Memory (MemoryT ($1, {min = size; max = Some size}, PageT 0x10000)) @@ loc],
11341134
[Data ($4, Active (x, offset) @@ loc) @@ loc],
11351135
[], [] }
11361136

interpreter/valid/match.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -165,8 +165,8 @@ let match_globaltype c (GlobalT (mut1, t1)) (GlobalT (mut2, t2)) =
165165
| Cons -> true
166166
| Var -> match_valtype c t2 t1
167167

168-
let match_memorytype c (MemoryT (at1, lim1)) (MemoryT (at2, lim2)) =
169-
at1 = at2 && match_limits c lim1 lim2
168+
let match_memorytype c (MemoryT (at1, lim1, pt1)) (MemoryT (at2, lim2, pt2)) =
169+
at1 = at2 && pt1 = pt2 && match_limits c lim1 lim2
170170

171171
let match_tabletype c (TableT (at1, lim1, t1)) (TableT (at2, lim2, t2)) =
172172
at1 = at2 && match_limits c lim1 lim2 &&

interpreter/valid/valid.ml

Lines changed: 20 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -104,6 +104,9 @@ let check_limits {min; max} range at msg =
104104
require (I64.le_u min max) at
105105
"size minimum must not be greater than maximum"
106106

107+
let check_pagetype (PageT ps) at =
108+
require (ps = 0x10000 || ps = 1) at "page size must be 1 or 64KiB"
109+
107110
let check_numtype (c : context) (t : numtype) at =
108111
()
109112

@@ -196,13 +199,14 @@ let check_globaltype (c : context) (gt : globaltype) at =
196199
check_valtype c t at
197200

198201
let check_memorytype (c : context) (mt : memorytype) at =
199-
let MemoryT (at_, lim) = mt in
202+
let MemoryT (at_, lim, pt) = mt in
200203
let sz, s =
201204
match at_ with
202205
| I32AT -> 0x1_0000L, "2^16 pages (4 GiB) for i32"
203206
| I64AT -> 0x1_0000_0000_0000L, "2^48 pages (256 TiB) for i64"
204207
in
205-
check_limits lim sz at ("memory size must be at most " ^ s)
208+
check_limits lim sz at ("memory size must be at most " ^ s);
209+
check_pagetype pt at
206210

207211
let check_tabletype (c : context) (tt : tabletype) at =
208212
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 =
384388
in
385389
require (1 lsl memop.align >= 1 && 1 lsl memop.align <= size) at
386390
"alignment must not be larger than natural";
387-
let MemoryT (at_, _lim) = memory c (0l @@ at) in
391+
let MemoryT (at_, _lim, _pt) = memory c (0l @@ at) in
388392
if at_ = I32AT then
389393
require (I64.lt_u memop.offset 0x1_0000_0000L) at
390394
"offset out of range";
@@ -648,60 +652,60 @@ let rec check_instr (c : context) (e : instr) (s : infer_resulttype) : infer_ins
648652
[] --> [], []
649653

650654
| Load (x, memop) ->
651-
let MemoryT (at, _lim) = memory c x in
655+
let MemoryT (at, _lim, _pt) = memory c x in
652656
let t = check_memop c memop num_size (Lib.Option.map fst) e.at in
653657
[NumT (numtype_of_addrtype at)] --> [NumT t], []
654658

655659
| Store (x, memop) ->
656-
let MemoryT (at, _lim) = memory c x in
660+
let MemoryT (at, _lim, _pt) = memory c x in
657661
let t = check_memop c memop num_size (fun sz -> sz) e.at in
658662
[NumT (numtype_of_addrtype at); NumT t] --> [], []
659663

660664
| VecLoad (x, memop) ->
661-
let MemoryT (at, _lim) = memory c x in
665+
let MemoryT (at, _lim, _pt) = memory c x in
662666
let t = check_memop c memop vec_size (Lib.Option.map fst) e.at in
663667
[NumT (numtype_of_addrtype at)] --> [VecT t], []
664668

665669
| VecStore (x, memop) ->
666-
let MemoryT (at, _lim) = memory c x in
670+
let MemoryT (at, _lim, _pt) = memory c x in
667671
let t = check_memop c memop vec_size (fun _ -> None) e.at in
668672
[NumT (numtype_of_addrtype at); VecT t] --> [], []
669673

670674
| VecLoadLane (x, memop, i) ->
671-
let MemoryT (at, _lim) = memory c x in
675+
let MemoryT (at, _lim, _pt) = memory c x in
672676
let t = check_memop c memop vec_size (fun sz -> Some sz) e.at in
673677
require (I8.to_int_u i < vec_size t / Pack.packed_size memop.pack) e.at
674678
"invalid lane index";
675679
[NumT (numtype_of_addrtype at); VecT t] --> [VecT t], []
676680

677681
| VecStoreLane (x, memop, i) ->
678-
let MemoryT (at, _lim) = memory c x in
682+
let MemoryT (at, _lim, _pt) = memory c x in
679683
let t = check_memop c memop vec_size (fun sz -> Some sz) e.at in
680684
require (I8.to_int_u i < vec_size t / Pack.packed_size memop.pack) e.at
681685
"invalid lane index";
682686
[NumT (numtype_of_addrtype at); VecT t] --> [], []
683687

684688
| MemorySize x ->
685-
let MemoryT (at, _lim) = memory c x in
689+
let MemoryT (at, _lim, _pt) = memory c x in
686690
[] --> [NumT (numtype_of_addrtype at)], []
687691

688692
| MemoryGrow x ->
689-
let MemoryT (at, _lim) = memory c x in
693+
let MemoryT (at, _lim, _pt) = memory c x in
690694
[NumT (numtype_of_addrtype at)] --> [NumT (numtype_of_addrtype at)], []
691695

692696
| MemoryFill x ->
693-
let MemoryT (at, _lim) = memory c x in
697+
let MemoryT (at, _lim, _pt) = memory c x in
694698
[NumT (numtype_of_addrtype at); NumT I32T;
695699
NumT (numtype_of_addrtype at)] --> [], []
696700

697701
| MemoryCopy (x, y)->
698-
let MemoryT (at1, _lib1) = memory c x in
699-
let MemoryT (at2, _lib2) = memory c y in
702+
let MemoryT (at1, _pt, _lib1) = memory c x in
703+
let MemoryT (at2, _pt, _lib2) = memory c y in
700704
[NumT (numtype_of_addrtype at1); NumT (numtype_of_addrtype at2);
701705
NumT (numtype_of_addrtype (min at1 at2))] --> [], []
702706

703707
| MemoryInit (x, y) ->
704-
let MemoryT (at, _lib) = memory c x in
708+
let MemoryT (at, _pt, _lib) = memory c x in
705709
let () = data c y in
706710
[NumT (numtype_of_addrtype at); NumT I32T; NumT I32T] --> [], []
707711

@@ -1071,7 +1075,7 @@ let check_datamode (c : context) (mode : segmentmode) =
10711075
match mode.it with
10721076
| Passive -> ()
10731077
| Active (x, offset) ->
1074-
let MemoryT (at, _) = memory c x in
1078+
let MemoryT (at, _, _) = memory c x in
10751079
check_const c offset (NumT (numtype_of_addrtype at))
10761080
| Declarative -> assert false
10771081

0 commit comments

Comments
 (0)