From d80122bd767a48277c42e12cb542cf452838074b Mon Sep 17 00:00:00 2001 From: rossberg-chromium Date: Tue, 12 Jul 2016 12:52:47 +0200 Subject: [PATCH] Implement non-trapping grow_memory semantics --- ml-proto/host/encode.ml | 2 +- ml-proto/host/format.ml | 2 +- ml-proto/host/parser.mly | 20 ++++++++++++++++---- ml-proto/spec/check.ml | 6 +++--- ml-proto/spec/decode.ml | 4 ++-- ml-proto/spec/eval.ml | 18 ++++++------------ ml-proto/spec/memory.ml | 22 +++++++++++++--------- ml-proto/spec/memory.mli | 9 +++++---- ml-proto/test/memory.wast | 2 +- ml-proto/test/memory_trap.wast | 2 +- 10 files changed, 49 insertions(+), 38 deletions(-) diff --git a/ml-proto/host/encode.ml b/ml-proto/host/encode.ml index 43126be3e2..b82e98984f 100644 --- a/ml-proto/host/encode.ml +++ b/ml-proto/host/encode.ml @@ -329,7 +329,7 @@ let encode m = (* Memory section *) let memory mem = let {min; max; _} = mem.it in - vu64 min; vu64 max; bool true (*TODO: pending change*) + vu32 min; vu32 max; bool true (*TODO: pending change*) let memory_section memo = section "memory" (opt memory) memo (memo <> None) diff --git a/ml-proto/host/format.ml b/ml-proto/host/format.ml index 80001e421a..e516020b5d 100644 --- a/ml-proto/host/format.ml +++ b/ml-proto/host/format.ml @@ -261,7 +261,7 @@ let segment seg = let memory mem = let {min; max; segments} = mem.it in - Node ("memory " ^ int64 min ^ " " ^ int64 max, list segment segments) + Node ("memory " ^ int32 min ^ " " ^ int32 max, list segment segments) (* Modules *) diff --git a/ml-proto/host/parser.mly b/ml-proto/host/parser.mly index c503474bc6..68b94497d6 100644 --- a/ml-proto/host/parser.mly +++ b/ml-proto/host/parser.mly @@ -39,6 +39,18 @@ let literal f s = | Failure msg -> error s.at ("constant out of range: " ^ msg) | _ -> error s.at "constant out of range" +let int s at = + try int_of_string s with Failure _ -> + error at "int constant out of range" + +let int32 s at = + try I32.of_string s with Failure _ -> + error at "i32 constant out of range" + +let int64 s at = + try I64.of_string s with Failure _ -> + error at "i64 constant out of range" + (* Symbolic variables *) @@ -197,7 +209,7 @@ literal : ; var : - | NAT { let at = at () in fun c lookup -> int_of_string $1 @@ at } + | NAT { let at = at () in fun c lookup -> int $1 at @@ at } | VAR { let at = at () in fun c lookup -> lookup c ($1 @@ at) @@ at } ; var_list : @@ -353,7 +365,7 @@ start : segment : | LPAR SEGMENT NAT text_list RPAR - { {Memory.addr = Int64.of_string $3; Memory.data = $4} @@ at () } + { {Memory.addr = int64 $3 (ati 3); Memory.data = $4} @@ at () } ; segment_list : | /* empty */ { [] } @@ -362,10 +374,10 @@ segment_list : memory : | LPAR MEMORY NAT NAT segment_list RPAR - { {min = Int64.of_string $3; max = Int64.of_string $4; segments = $5} + { {min = int32 $3 (ati 3); max = int32 $4 (ati 4); segments = $5} @@ at () } | LPAR MEMORY NAT segment_list RPAR - { {min = Int64.of_string $3; max = Int64.of_string $3; segments = $4} + { {min = int32 $3 (ati 3); max = int32 $3 (ati 3); segments = $4} @@ at () } ; diff --git a/ml-proto/spec/check.ml b/ml-proto/spec/check.ml index 508317ea42..d3830b2dd8 100644 --- a/ml-proto/spec/check.ml +++ b/ml-proto/spec/check.ml @@ -332,15 +332,15 @@ let check_segment pages prev_end seg = 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 (Int64.mul pages Memory.page_size >= seg_end) seg.at + require (Int64.mul (Int64.of_int32 pages) Memory.page_size >= seg_end) seg.at "data segment does not fit memory"; seg_end let check_memory memory = let mem = memory.it in - require (mem.min <= mem.max) memory.at + require (I32.le_u mem.min mem.max) memory.at "minimum memory pages must be less than or equal to the maximum"; - require (mem.max <= 65535L) memory.at + require (I32.le_u mem.max 65535l) memory.at "linear memory pages must be less or equal to 65535 (4GiB)"; ignore (List.fold_left (check_segment mem.min) 0L mem.segments) diff --git a/ml-proto/spec/decode.ml b/ml-proto/spec/decode.ml index 5b10d925c5..62a396c79b 100644 --- a/ml-proto/spec/decode.ml +++ b/ml-proto/spec/decode.ml @@ -494,8 +494,8 @@ let table_section s = (* Memory section *) let memory s = - let min = vu64 s in - let max = vu64 s in + let min = vu32 s in + let max = vu32 s in let _ = bool s in (*TODO: pending change*) {min; max; segments = []} diff --git a/ml-proto/spec/eval.ml b/ml-proto/spec/eval.ml index a7260a01f5..9944236546 100644 --- a/ml-proto/spec/eval.ml +++ b/ml-proto/spec/eval.ml @@ -288,22 +288,16 @@ and eval_hostop c hostop vs at = | CurrentMemory, [] -> let mem = memory c at in let size = Memory.size mem in - assert (I64.lt_u size (Int64.of_int32 Int32.max_int)); - Some (Int32 (Int64.to_int32 size)) + Some (Int32 size) | GrowMemory, [v] -> let mem = memory c at in - let delta = address32 v at in + let delta = int32 v at in let old_size = Memory.size mem in - let new_size = Int64.add old_size delta in - if I64.lt_u new_size old_size then - Trap.error at "memory size overflow"; - (* Test whether the new size overflows the memory type. - * Since we currently only support i32, just test that. *) - if I64.gt_u new_size (Int64.of_int32 Int32.max_int) then - Trap.error at "memory size exceeds implementation limit"; - Memory.grow mem delta; - Some (Int32 (Int64.to_int32 old_size)) + let result = + try Memory.grow mem delta; old_size + with Memory.SizeOverflow | Memory.OutOfMemory -> -1l + in Some (Int32 result) | _, _ -> Crash.error at "invalid invocation of host operator" diff --git a/ml-proto/spec/memory.ml b/ml-proto/spec/memory.ml index 4f6e75f8d5..62f26f7fae 100644 --- a/ml-proto/spec/memory.ml +++ b/ml-proto/spec/memory.ml @@ -2,9 +2,9 @@ open Bigarray open Types open Values +type size = int32 (* number of pages *) type address = int64 -type size = address -type offset = address +type offset = int64 type mem_size = Mem8 | Mem16 | Mem32 type extension = SX | ZX type segment = {addr : address; data : string} @@ -18,6 +18,7 @@ type t = memory exception Type exception Bounds exception SizeOverflow +exception OutOfMemory let page_size = 0x10000L (* 64 KiB *) @@ -46,10 +47,13 @@ let host_index_of_int64 a n = let create' n = - let sz = host_size_of_int64 (Int64.mul n page_size) in - let mem = Array1.create Int8_unsigned C_layout sz in - Array1.fill mem 0; - mem + if I32.gt_u n 0x10000l then raise SizeOverflow else + try + let sz = host_size_of_int64 (Int64.mul (Int64.of_int32 n) page_size) in + let mem = Array1.create Int8_unsigned C_layout sz in + Array1.fill mem 0; + mem + with Out_of_memory -> raise OutOfMemory let create n = ref (create' n) @@ -66,13 +70,13 @@ let init mem segs = try List.iter (init_seg mem) segs with Invalid_argument _ -> raise Bounds let size mem = - Int64.div (int64_of_host_size (Array1.dim !mem)) page_size + Int64.to_int32 (Int64.div (int64_of_host_size (Array1.dim !mem)) page_size) let grow mem pages = let host_old_size = Array1.dim !mem in let old_size = size mem in - let new_size = Int64.add old_size pages in - if I64.gt_u old_size new_size then raise SizeOverflow else + let new_size = Int32.add old_size pages in + if I32.gt_u old_size new_size then raise SizeOverflow else let after = create' new_size in Array1.blit (Array1.sub !mem 0 host_old_size) (Array1.sub after 0 host_old_size); mem := after diff --git a/ml-proto/spec/memory.mli b/ml-proto/spec/memory.mli index 2e60e8eb66..6cefe86ecb 100644 --- a/ml-proto/spec/memory.mli +++ b/ml-proto/spec/memory.mli @@ -1,7 +1,7 @@ type memory type t = memory +type size = int32 (* number of pages *) type address = int64 -type size = int64 type offset = int64 type mem_size = Mem8 | Mem16 | Mem32 type extension = SX | ZX @@ -12,13 +12,14 @@ type value = Values.value exception Type exception Bounds exception SizeOverflow +exception OutOfMemory -val page_size : size +val page_size : offset -val create : size -> memory +val create : size -> memory (* raise SizeOverflow, OutOfMemory *) val init : memory -> segment list -> unit val size : memory -> size -val grow : memory -> size -> unit +val grow : memory -> size -> unit (* raise SizeOverflow, OutOfMemory *) val load : memory -> address -> offset -> value_type -> value val store : memory -> address -> offset -> value -> unit diff --git a/ml-proto/test/memory.wast b/ml-proto/test/memory.wast index f98118839d..db4409a667 100644 --- a/ml-proto/test/memory.wast +++ b/ml-proto/test/memory.wast @@ -41,7 +41,7 @@ "linear memory pages must be less or equal to 65535 (4GiB)" ) (assert_invalid - (module (memory 0 4294967296)) + (module (memory 0 4294967295)) "linear memory pages must be less or equal to 65535 (4GiB)" ) diff --git a/ml-proto/test/memory_trap.wast b/ml-proto/test/memory_trap.wast index a3f45abd6b..3749143890 100644 --- a/ml-proto/test/memory_trap.wast +++ b/ml-proto/test/memory_trap.wast @@ -33,4 +33,4 @@ (assert_trap (invoke "load" (i32.const 0)) "out of bounds memory access") (assert_trap (invoke "store" (i32.const 0x80000000) (i32.const 13)) "out of bounds memory access") (assert_trap (invoke "load" (i32.const 0x80000000)) "out of bounds memory access") -(assert_trap (invoke "grow_memory" (i32.const 0x80000000)) "memory size exceeds implementation limit") +(assert_return (invoke "grow_memory" (i32.const 0x10001)) (i32.const -1))