diff --git a/ml-proto/host/parser.mly b/ml-proto/host/parser.mly index fe19130460..954cb46dd7 100644 --- a/ml-proto/host/parser.mly +++ b/ml-proto/host/parser.mly @@ -269,7 +269,7 @@ func : segment : | LPAR SEGMENT INT TEXT RPAR - { {Memory.addr = int_of_string $3; Memory.data = $4} @@ at() } + { {Memory.addr = Int64.of_string $3; Memory.data = $4} @@ at() } ; segment_list : | /* empty */ { [] } @@ -278,10 +278,10 @@ segment_list : memory : | LPAR MEMORY INT INT segment_list RPAR - { {initial = int_of_string $3; max = int_of_string $4; segments = $5 } + { {initial = Int64.of_string $3; max = Int64.of_string $4; segments = $5} @@ at() } | LPAR MEMORY INT segment_list RPAR - { {initial = int_of_string $3; max = int_of_string $3; segments = $4 } + { {initial = Int64.of_string $3; max = Int64.of_string $3; segments = $4} @@ at() } ; diff --git a/ml-proto/spec/ast.ml b/ml-proto/spec/ast.ml index 4dc34b28bf..27f1697945 100644 --- a/ml-proto/spec/ast.ml +++ b/ml-proto/spec/ast.ml @@ -114,8 +114,8 @@ and arm' = type memory = memory' Source.phrase and memory' = { - initial : Memory.size; - max : Memory.size; + initial : int64; + max : int64; segments : segment list; } and segment = Memory.segment Source.phrase diff --git a/ml-proto/spec/check.ml b/ml-proto/spec/check.ml index 921dcb8766..28afc891f0 100644 --- a/ml-proto/spec/check.ml +++ b/ml-proto/spec/check.ml @@ -306,7 +306,8 @@ let check_export c set ex = NameSet.add name set let check_segment size prev_end seg = - let seg_end = seg.it.Memory.addr + String.length seg.it.Memory.data in + let seg_len = Int64.of_int (String.length seg.it.Memory.data) in + let seg_end = Int64.add seg.it.Memory.addr seg_len in require (seg.it.Memory.addr >= prev_end) seg.at "data segment not disjoint and ordered"; require (size >= seg_end) seg.at @@ -314,9 +315,12 @@ let check_segment size prev_end seg = seg_end let check_memory memory = - require (memory.it.initial <= memory.it.max) memory.at + let mem = memory.it in + require (mem.initial <= mem.max) memory.at "initial memory size must be less than maximum"; - ignore (List.fold_left (check_segment memory.it.initial) 0 memory.it.segments) + require (mem.max <= 4294967296L) memory.at + "linear memory size must be less or equal to 4GiB"; + ignore (List.fold_left (check_segment mem.initial) Int64.zero mem.segments) let check_module m = let {imports; exports; tables; funcs; memory} = m.it in diff --git a/ml-proto/spec/eval.ml b/ml-proto/spec/eval.ml index 61e011a112..bc84b8094c 100644 --- a/ml-proto/spec/eval.ml +++ b/ml-proto/spec/eval.ml @@ -14,7 +14,7 @@ let error = Error.error type value = Values.value type func = Ast.func type import = value list -> value option -type host_params = {page_size : Memory.size} +type host_params = {page_size : int} module ExportMap = Map.Make(String) type export_map = func ExportMap.t @@ -42,9 +42,6 @@ type config = return : label } -let page_size c = - I32.of_int32 (Int32.of_int c.module_.host.page_size) - let lookup category list x = try List.nth list x.it with Failure _ -> error x.at ("runtime: undefined " ^ category ^ " " ^ string_of_int x.it) @@ -103,6 +100,11 @@ let int32 v at = | Int32 i -> i | v -> type_error at v Types.Int32Type +let mem_size v at = + let i32 = int32 v at in + let i64 = Int64.of_int32 i32 in + Int64.shift_right_logical (Int64.shift_left i64 32) 32 + (* Evaluation *) @@ -175,30 +177,26 @@ let rec eval_expr (c : config) (e : expr) = | Load ({ty; align = _}, e1) -> let mem = some_memory c e.at in - let v1 = some (eval_expr c e1) e1.at in - let a = Memory.address_of_value v1 in - (try Some (Memory.load mem a ty) with exn -> memory_error e.at exn) + let v1 = mem_size (eval_expr c e1) e1.at in + (try Some (Memory.load mem v1 ty) with exn -> memory_error e.at exn) | Store ({ty = _; align = _}, e1, e2) -> let mem = some_memory c e.at in - let v1 = some (eval_expr c e1) e1.at in + let v1 = mem_size (eval_expr c e1) e1.at in let v2 = some (eval_expr c e2) e2.at in - let a = Memory.address_of_value v1 in - (try Memory.store mem a v2 with exn -> memory_error e.at exn); + (try Memory.store mem v1 v2 with exn -> memory_error e.at exn); Some v2 | LoadExtend ({memop = {ty; align = _}; sz; ext}, e1) -> let mem = some_memory c e.at in - let v1 = some (eval_expr c e1) e1.at in - let a = Memory.address_of_value v1 in - (try Some (Memory.load_extend mem a sz ext ty) with exn -> memory_error e.at exn) + let v1 = mem_size (eval_expr c e1) e1.at in + (try Some (Memory.load_extend mem v1 sz ext ty) with exn -> memory_error e.at exn) | StoreWrap ({memop = {ty; align = _}; sz}, e1, e2) -> let mem = some_memory c e.at in - let v1 = some (eval_expr c e1) e1.at in + let v1 = mem_size (eval_expr c e1) e1.at in let v2 = some (eval_expr c e2) e2.at in - let a = Memory.address_of_value v1 in - (try Memory.store_wrap mem a sz v2 with exn -> memory_error e.at exn); + (try Memory.store_wrap mem v1 sz v2 with exn -> memory_error e.at exn); Some v2 | Const v -> @@ -237,19 +235,20 @@ let rec eval_expr (c : config) (e : expr) = | exn -> numerics_error e.at exn) | PageSize -> - Some (Int32 (page_size c)) + Some (Int32 (Int32.of_int c.module_.host.page_size)) | MemorySize -> let mem = some_memory c e.at in - Some (Int32 (I32.of_int32 (Int32.of_int (Memory.size mem)))) + let i64 = Memory.size mem in + assert (i64 < Int64.of_int32 (Int32.max_int)); + Some (Int32 (Int64.to_int32 i64)) | ResizeMemory e -> let mem = some_memory c e.at in - let i = int32 (eval_expr c e) e.at in - if (I32.rem_u i (page_size c)) <> I32.zero then + let sz = mem_size (eval_expr c e) e.at in + if (Int64.rem sz (Int64.of_int c.module_.host.page_size)) <> 0L then error e.at "runtime: resize_memory operand not multiple of page_size"; - (* TODO: The conversion to int could overflow. *) - Memory.resize mem (Int32.to_int i); + Memory.resize mem sz; None and eval_expr_option c eo = diff --git a/ml-proto/spec/eval.mli b/ml-proto/spec/eval.mli index 2442bfe13f..1a9ab090e8 100644 --- a/ml-proto/spec/eval.mli +++ b/ml-proto/spec/eval.mli @@ -5,7 +5,7 @@ type instance type value = Values.value type import = value list -> value option -type host_params = {page_size : Memory.size} +type host_params = {page_size : int} val init : Ast.module_ -> import list -> host_params -> instance val invoke : instance -> string -> value list -> value option diff --git a/ml-proto/spec/memory.ml b/ml-proto/spec/memory.ml index 4263b9fa69..336a36ffd5 100644 --- a/ml-proto/spec/memory.ml +++ b/ml-proto/spec/memory.ml @@ -6,10 +6,7 @@ open Bigarray open Types open Values - -(* Types and view types *) - -type address = int +type address = int64 type size = address type mem_size = Mem8 | Mem16 | Mem32 type extension = SX | ZX @@ -21,15 +18,37 @@ type memory' = (int, int8_unsigned_elt, c_layout) Array1.t type memory = memory' ref type t = memory - -(* Creation and initialization *) - exception Type exception Bounds exception Address +(* + * These limitations should be considered part of the host environment and not + * part of the spec defined by this file. + * ========================================================================== + *) + +let host_size_of_int64 n = + if n < Int64.zero || n > (Int64.of_int max_int) then raise Out_of_memory; + Int64.to_int n + +let int64_of_host_size n = + Int64.of_int n + +let host_index_of_int64 a n = + assert (n >= 0); + let n' = Int64.of_int n in + if (a < Int64.zero) || + (Int64.sub Int64.max_int a < n') || + (Int64.add a n' > Int64.of_int max_int) then raise Bounds; + Int64.to_int a + +(* ========================================================================== *) + + let create' n = - let mem = Array1.create Int8_unsigned C_layout n in + let sz = host_size_of_int64 n in + let mem = Array1.create Int8_unsigned C_layout sz in Array1.fill mem 0; mem @@ -38,48 +57,45 @@ let create n = let init_seg mem seg = (* There currently is no way to blit from a string. *) - for i = 0 to String.length seg.data - 1 do - !mem.{seg.addr + i} <- Char.code seg.data.[i] + let n = String.length seg.data in + let base = host_index_of_int64 seg.addr n in + for i = 0 to n - 1 do + !mem.{base + i} <- Char.code seg.data.[i] done let init mem segs = try List.iter (init_seg mem) segs with Invalid_argument _ -> raise Bounds - let size mem = - Array1.dim !mem + int64_of_host_size (Array1.dim !mem) let resize mem n = - let before = !mem in let after = create' n in - let min = min (Array1.dim before) n in - Array1.blit (Array1.sub before 0 min) (Array1.sub after 0 min); + let min = host_index_of_int64 (min (size mem) n) 0 in + Array1.blit (Array1.sub !mem 0 min) (Array1.sub after 0 min); mem := after -open Values - -(* TODO: The conversion to int could overflow *) -let address_of_value = function - | Int32 i -> Int32.to_int (I32.to_int32 i) - | _ -> raise Address - - -(* Load and store *) - let rec loadn mem n a = assert (n > 0 && n <= 8); - let byte = try Int64.of_int !mem.{a} with Invalid_argument _ -> raise Bounds in + let i = host_index_of_int64 a n in + try loadn' mem n i with Invalid_argument _ -> raise Bounds + +and loadn' mem n i = + let byte = Int64.of_int !mem.{i} in if n = 1 then byte else - Int64.logor byte (Int64.shift_left (loadn mem (n-1) (a+1)) 8) + Int64.logor byte (Int64.shift_left (loadn' mem (n-1) (i+1)) 8) let rec storen mem n a v = assert (n > 0 && n <= 8); - let byte = (Int64.to_int v) land 255 in - (try !mem.{a} <- byte with Invalid_argument _ -> raise Bounds); + let i = host_index_of_int64 a n in + try storen' mem n i v with Invalid_argument _ -> raise Bounds + +and storen' mem n i v = + !mem.{i} <- (Int64.to_int v) land 255; if (n > 1) then - storen mem (n-1) (a+1) (Int64.shift_right v 8) + storen' mem (n-1) (i+1) (Int64.shift_right v 8) let load mem a t = match t with diff --git a/ml-proto/spec/memory.mli b/ml-proto/spec/memory.mli index 6f7112a29f..2b3320a00d 100644 --- a/ml-proto/spec/memory.mli +++ b/ml-proto/spec/memory.mli @@ -4,7 +4,7 @@ type memory type t = memory -type address = int +type address = int64 type size = address type mem_size = Mem8 | Mem16 | Mem32 type extension = SX | ZX @@ -24,5 +24,3 @@ val load : memory -> address -> value_type -> value val store : memory -> address -> value -> unit val load_extend : memory -> address -> mem_size -> extension -> value_type -> value val store_wrap : memory -> address -> mem_size -> value -> unit - -val address_of_value : Values.value -> address