Skip to content

Commit

Permalink
Support for the Memory64 proposal in the spec interpreter (#14)
Browse files Browse the repository at this point in the history
* Support for the Memory64 proposal in the spec interpreter

* Apply suggestions from code review

Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>

* Memory64 code review fixes

* Update interpreter/syntax/types.ml

Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>

Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>
  • Loading branch information
aardappel and rossberg authored Feb 2, 2021
1 parent a481942 commit 2bbd2a1
Show file tree
Hide file tree
Showing 16 changed files with 177 additions and 127 deletions.
19 changes: 11 additions & 8 deletions interpreter/binary/decode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -94,8 +94,8 @@ let rec vsN n s =
then (if b land 0x40 = 0 then x else Int64.(logor x (logxor (-1L) 0x7fL)))
else Int64.(logor x (shift_left (vsN (n - 7) s) 7))

let vu1 s = Int64.to_int (vuN 1 s)
let vu32 s = Int64.to_int32 (vuN 32 s)
let vu64 s = vuN 64 s
let vs7 s = Int64.to_int (vsN 7 s)
let vs32 s = Int64.to_int32 (vsN 32 s)
let vs33 s = I32_convert.wrap_i64 (vsN 33 s)
Expand All @@ -109,7 +109,6 @@ let len32 s =
if I32.le_u n (Int32.of_int (len s)) then Int32.to_int n else
error s pos "length out of bounds"

let bool s = (vu1 s = 1)
let string s = let n = len32 s in get_string n s
let rec list f n s = if n = 0 then [] else let x = f s in x :: list f (n - 1) s
let opt f b s = if b then Some (f s) else None
Expand Down Expand Up @@ -155,19 +154,23 @@ let func_type s =
| _ -> error s (pos s - 1) "malformed function type"

let limits vu s =
let has_max = bool s in
let flags = u8 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 min = vu s in
let max = opt vu has_max s in
{min; max}
{min; max}, is64

let table_type s =
let t = elem_type s in
let lim = limits vu32 s in
let lim, is64 = limits vu32 s in
require (not is64) s (pos s - 1) "tables cannot have 64-bit indices";
TableType (lim, t)

let memory_type s =
let lim = limits vu32 s in
MemoryType lim
let lim, is64 = limits vu64 s in
MemoryType (lim, if is64 then I64IndexType else I32IndexType)

let mutability s =
match u8 s with
Expand All @@ -194,7 +197,7 @@ let end_ s = expect 0x0b s "END opcode expected"
let memop s =
let align = vu32 s in
require (I32.le_u align 32l) s (pos s - 1) "malformed memop flags";
let offset = vu32 s in
let offset = vu64 s in
Int32.to_int align, offset

let block_type s =
Expand Down
15 changes: 8 additions & 7 deletions interpreter/binary/encode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -56,21 +56,21 @@ let encode m =
if -64L <= i && i < 64L then u8 b
else (u8 (b lor 0x80); vs64 (Int64.shift_right i 7))

let vu1 i = vu64 Int64.(logand (of_int i) 1L)
let vu32 i = vu64 Int64.(logand (of_int32 i) 0xffffffffL)
let vs7 i = vs64 (Int64.of_int i)
let vs32 i = vs64 (Int64.of_int32 i)
let vs33 i = vs64 (I64_convert.extend_i32_s i)
let f32 x = u32 (F32.to_bits x)
let f64 x = u64 (F64.to_bits x)

let flag b i = if b then 1 lsl i else 0

let len i =
if Int32.to_int (Int32.of_int i) <> i then
Code.error Source.no_region
"cannot encode length with more than 32 bit";
vu32 (Int32.of_int i)

let bool b = vu1 (if b then 1 else 0)
let string bs = len (String.length bs); put_string s bs
let name n = string (Utf8.encode n)
let list f xs = List.iter f xs
Expand Down Expand Up @@ -104,14 +104,15 @@ let encode m =
let func_type = function
| FuncType (ins, out) -> vs7 (-0x20); stack_type ins; stack_type out

let limits vu {min; max} =
bool (max <> None); vu min; opt vu max
let limits vu {min; max} it =
let flags = flag (max <> None) 0 + flag (it = I64IndexType) 2 in
u8 flags; vu min; opt vu max

let table_type = function
| TableType (lim, t) -> elem_type t; limits vu32 lim
| TableType (lim, t) -> elem_type t; limits vu32 lim I32IndexType

let memory_type = function
| MemoryType lim -> limits vu32 lim
| MemoryType (lim, it) -> limits vu64 lim it

let mutability = function
| Immutable -> u8 0
Expand All @@ -129,7 +130,7 @@ let encode m =
let op n = u8 n
let end_ () = op 0x0b

let memop {align; offset; _} = vu32 (Int32.of_int align); vu32 offset
let memop {align; offset; _} = vu32 (Int32.of_int align); vu64 offset

let var x = vu32 x.it

Expand Down
18 changes: 9 additions & 9 deletions interpreter/exec/eval.ml
Original file line number Diff line number Diff line change
Expand Up @@ -209,9 +209,9 @@ 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")

| Load {offset; ty; sz; _}, I32 i :: vs' ->
| Load {offset; ty; sz; _}, a :: vs' ->
let mem = memory frame.inst (0l @@ e.at) in
let addr = I64_convert.extend_i32_u i in
let addr = Memory.address_of_value a in
(try
let v =
match sz with
Expand All @@ -220,9 +220,9 @@ let rec step (c : config) : config =
in v :: vs', []
with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at])

| Store {offset; sz; _}, v :: I32 i :: vs' ->
| Store {offset; sz; _}, v :: a :: vs' ->
let mem = memory frame.inst (0l @@ e.at) in
let addr = I64_convert.extend_i32_u i in
let addr = Memory.address_of_value a in
(try
(match sz with
| None -> Memory.store_value mem addr offset v
Expand All @@ -233,15 +233,15 @@ let rec step (c : config) : config =

| MemorySize, vs ->
let mem = memory frame.inst (0l @@ e.at) in
I32 (Memory.size mem) :: vs, []
Memory.value_of_address (Memory.index_of mem) (Memory.size mem) :: vs, []

| MemoryGrow, I32 delta :: vs' ->
| MemoryGrow, delta :: vs' ->
let mem = memory frame.inst (0l @@ e.at) in
let old_size = Memory.size mem in
let result =
try Memory.grow mem delta; old_size
with Memory.SizeOverflow | Memory.SizeLimit | Memory.OutOfMemory -> -1l
in I32 result :: vs', []
try Memory.grow mem (Memory.address_of_value delta); old_size
with Memory.SizeOverflow | Memory.SizeLimit | Memory.OutOfMemory -> -1L
in (Memory.value_of_address (Memory.index_of mem) result) :: vs', []

| Const v, vs ->
v.it :: vs, []
Expand Down
2 changes: 1 addition & 1 deletion interpreter/host/spectest.ml
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ let global (GlobalType (t, _) as gt) =
in Global.alloc gt v

let table = Table.alloc (TableType ({min = 10l; max = Some 20l}, FuncRefType))
let memory = Memory.alloc (MemoryType {min = 1l; max = Some 2l})
let memory = Memory.alloc (MemoryType ({min = 1L; max = Some 2L}, I32IndexType))
let func f t = Func.alloc_host t (f t)

let print_value v =
Expand Down
43 changes: 27 additions & 16 deletions interpreter/runtime/memory.ml
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,12 @@ open Lib.Bigarray
open Types
open Values

type size = int32 (* number of pages *)
type size = int64 (* number of pages *)
type address = int64
type offset = int32
type offset = int64

type memory' = (int, int8_unsigned_elt, c_layout) Array1.t
type memory = {mutable content : memory'; max : size option}
type memory = {mutable content : memory'; max : size option; it : index_type}
type t = memory

exception Type
Expand All @@ -21,36 +21,47 @@ let page_size = 0x10000L (* 64 KiB *)

let within_limits n = function
| None -> true
| Some max -> I32.le_u n max
| Some max -> I64.le_u n max

let create n =
if I32.gt_u n 0x10000l then raise SizeOverflow else
let create n it =
if I64.gt_u n 0x10000L && it = I32IndexType then raise SizeOverflow else
try
let size = Int64.(mul (of_int32 n) page_size) in
let size = Int64.(mul n page_size) in
let mem = Array1_64.create Int8_unsigned C_layout size in
Array1.fill mem 0;
mem
with Out_of_memory -> raise OutOfMemory

let alloc (MemoryType {min; max}) =
let alloc (MemoryType ({min; max}, it)) =
assert (within_limits min max);
{content = create min; max}
{content = create min it; max; it}

let bound mem =
Array1_64.dim mem.content

let size mem =
Int64.(to_int32 (div (bound mem) page_size))
Int64.(div (bound mem) page_size)

let type_of mem =
MemoryType {min = size mem; max = mem.max}
MemoryType ({min = size mem; max = mem.max}, mem.it)

let index_of mem = mem.it

let value_of_address it x =
if it = I64IndexType then I64 (x) else I32 (Int64.to_int32 x)

let address_of_value x =
match x with
| I64 i -> i
| I32 i -> I64_convert.extend_i32_u i
| _ -> raise Type

let grow mem delta =
let old_size = size mem in
let new_size = Int32.add old_size delta in
if I32.gt_u old_size new_size then raise SizeOverflow else
let new_size = Int64.add old_size delta in
if I64.gt_u old_size new_size then raise SizeOverflow else
if not (within_limits new_size mem.max) then raise SizeLimit else
let after = create new_size in
let after = create new_size mem.it 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.content <- after
Expand All @@ -74,7 +85,7 @@ let store_bytes mem a bs =
done

let effective_address a o =
let ea = Int64.(add a (of_int32 o)) in
let ea = Int64.(add a o) in
if I64.lt_u ea a then raise Bounds;
ea

Expand All @@ -91,7 +102,7 @@ let storen mem a o n x =
assert (n > 0 && n <= 8);
let rec loop a n x =
if n > 0 then begin
Int64.(loop (add a 1L) (n - 1) (shift_right x 8));
Int64.(loop (effective_address a 1L) (n - 1) (shift_right x 8));
store_byte mem a (Int64.to_int x land 0xff)
end
in loop (effective_address a o) n x
Expand Down
7 changes: 5 additions & 2 deletions interpreter/runtime/memory.mli
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,9 @@ open Values
type memory
type t = memory

type size = int32 (* number of pages *)
type size = int64 (* number of pages *)
type address = int64
type offset = int32
type offset = int64

exception Type
exception Bounds
Expand All @@ -18,8 +18,11 @@ val page_size : int64

val alloc : memory_type -> memory (* raises SizeOverflow, OutOfMemory *)
val type_of : memory -> memory_type
val index_of : memory -> index_type
val size : memory -> size
val bound : memory -> address
val value_of_address : index_type -> address -> value
val address_of_value : value -> address
val grow : memory -> size -> unit
(* raises SizeLimit, SizeOverflow, OutOfMemory *)

Expand Down
33 changes: 21 additions & 12 deletions interpreter/syntax/types.ml
Original file line number Diff line number Diff line change
@@ -1,14 +1,15 @@
(* Types *)

type value_type = I32Type | I64Type | F32Type | F64Type
type index_type = I32IndexType | I64IndexType
type elem_type = FuncRefType
type stack_type = value_type list
type func_type = FuncType of stack_type * stack_type

type 'a limits = {min : 'a; max : 'a option}
type mutability = Immutable | Mutable
type table_type = TableType of Int32.t limits * elem_type
type memory_type = MemoryType of Int32.t limits
type memory_type = MemoryType of Int64.t limits * index_type
type global_type = GlobalType of value_type * mutability
type extern_type =
| ExternFuncType of func_type
Expand All @@ -31,24 +32,28 @@ let packed_size = function
| Pack16 -> 2
| Pack32 -> 4

let value_type_of_index_type = function
| I32IndexType -> I32Type
| I64IndexType -> I64Type


(* Subtyping *)

let match_limits lim1 lim2 =
I32.ge_u lim1.min lim2.min &&
let match_limits ge lim1 lim2 =
ge lim1.min lim2.min &&
match lim1.max, lim2.max with
| _, None -> true
| None, Some _ -> false
| Some i, Some j -> I32.le_u i j
| Some i, Some j -> ge j i

let match_func_type ft1 ft2 =
ft1 = ft2

let match_table_type (TableType (lim1, et1)) (TableType (lim2, et2)) =
et1 = et2 && match_limits lim1 lim2
et1 = et2 && match_limits I32.ge_u lim1 lim2

let match_memory_type (MemoryType lim1) (MemoryType lim2) =
match_limits lim1 lim2
let match_memory_type (MemoryType (lim1, it1)) (MemoryType (lim2, it2)) =
it1 = it2 && match_limits I64.ge_u lim1 lim2

let match_global_type gt1 gt2 =
gt1 = gt2
Expand Down Expand Up @@ -89,15 +94,19 @@ let string_of_value_types = function
let string_of_elem_type = function
| FuncRefType -> "funcref"

let string_of_limits {min; max} =
I32.to_string_u min ^
(match max with None -> "" | Some n -> " " ^ I32.to_string_u n)
let string_of_limits to_string {min; max} =
to_string min ^
(match max with None -> "" | Some n -> " " ^ to_string n)

let string_of_memory_type = function
| MemoryType lim -> string_of_limits lim
| MemoryType (lim, it) ->
string_of_value_type (value_type_of_index_type it) ^
" " ^ string_of_limits I64.to_string_u lim


let string_of_table_type = function
| TableType (lim, t) -> string_of_limits lim ^ " " ^ string_of_elem_type t
| TableType (lim, t) -> string_of_limits I32.to_string_u lim ^ " " ^
string_of_elem_type t

let string_of_global_type = function
| GlobalType (t, Immutable) -> string_of_value_type t
Expand Down
10 changes: 7 additions & 3 deletions interpreter/text/arrange.ml
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ open Sexpr

let nat n = I32.to_string_u (I32.of_int_u n)
let nat32 = I32.to_string_u
let nat64 = I64.to_string_u

let add_hex_char buf c = Printf.bprintf buf "\\%02x" (Char.code c)
let add_char buf = function
Expand Down Expand Up @@ -57,6 +58,8 @@ let break_string s =

let value_type t = string_of_value_type t

let index_type t = string_of_value_type (value_type_of_index_type t)

let elem_type t = string_of_elem_type t

let decls kind ts = tab kind (atom value_type) ts
Expand Down Expand Up @@ -201,7 +204,7 @@ let cvtop = oper (IntOp.cvtop, FloatOp.cvtop)

let memop name {ty; align; offset; _} sz =
value_type ty ^ "." ^ name ^
(if offset = 0l then "" else " offset=" ^ nat32 offset) ^
(if offset = 0L then "" else " offset=" ^ nat64 offset) ^
(if 1 lsl align = sz then "" else " align=" ^ nat (1 lsl align))

let loadop op =
Expand Down Expand Up @@ -294,8 +297,9 @@ let table off i tab =
)

let memory off i mem =
let {mtype = MemoryType lim} = mem.it in
Node ("memory $" ^ nat (off + i) ^ " " ^ limits nat32 lim, [])
let {mtype = MemoryType (lim, it)} = mem.it in
Node ("memory $" ^ nat (off + i) ^ " " ^ index_type it ^ " " ^
limits nat64 lim, [])

let segment head dat seg =
let {index; offset; init} = seg.it in
Expand Down
Loading

0 comments on commit 2bbd2a1

Please sign in to comment.