diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst
index db73b5be..d2b33904 100644
--- a/document/core/exec/instructions.rst
+++ b/document/core/exec/instructions.rst
@@ -695,6 +695,9 @@ Memory Instructions
(\iff n > 1) \\
\end{array}
+.. note::
+ The use of the :math:`\vconst_t` meta function in the rules for this and the following instructions ensures that an overflowing index turns into a :ref:`trap <syntax-trap>`.
+
.. _exec-memory.init:
@@ -936,12 +939,12 @@ Memory Instructions
\end{array} \\
\end{array}
\\ \qquad
- (\iff dst <= src \wedge cnt > 1)
+ (\iff dst \leq src \wedge cnt > 1)
\\[1ex]
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~cnt)~\MEMORYCOPY &\stepto& S; F;
\begin{array}[t]{@{}l@{}}
- (\I32.\CONST~(dst+cnt-1))~(\I32.\CONST~(src+cnt-1))~(\I32.\CONST~1)~\MEMORYCOPY \\
+ (\vconst_{\I32}(dst+cnt-1))~(\vconst_{\I32}(src+cnt-1))~(\I32.\CONST~1)~\MEMORYCOPY \\
(\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~(cnt-1))~\MEMORYCOPY \\
\end{array} \\
\end{array}
diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml
index 5aaf42ad..48e923cd 100644
--- a/interpreter/exec/eval.ml
+++ b/interpreter/exec/eval.ml
@@ -117,6 +117,10 @@ let drop n (vs : 'a stack) at =
* c : config
*)
+let const_i32_add i j at msg =
+ let k = I32.add i j in
+ if I32.lt_u k i then Trapping msg else Plain (Const (I32 k @@ at))
+
let rec step (c : config) : config =
let {frame; code = vs, es; _} = c in
let e = List.hd es in
@@ -198,11 +202,13 @@ 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")
+ (* TODO: turn into small-step, but needs reference values *)
| TableCopy, I32 n :: I32 s :: I32 d :: vs' ->
let tab = table frame.inst (0l @@ e.at) in
(try Table.copy tab d s n; vs', []
with exn -> vs', [Trapping (table_error e.at exn) @@ e.at])
+ (* TODO: turn into small-step, but needs reference values *)
| TableInit x, I32 n :: I32 s :: I32 d :: vs' ->
let tab = table frame.inst (0l @@ e.at) in
(match !(elem frame.inst x) with
@@ -253,30 +259,97 @@ let rec step (c : config) : config =
with Memory.SizeOverflow | Memory.SizeLimit | Memory.OutOfMemory -> -1l
in I32 result :: vs', []
- | MemoryFill, I32 n :: I32 b :: I32 i :: vs' ->
- let mem = memory frame.inst (0l @@ e.at) in
- let addr = I64_convert.extend_i32_u i in
- (try Memory.fill mem addr (Int32.to_int b) n; vs', []
- with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at])
+ | MemoryFill, I32 0l :: v :: I32 i :: vs' ->
+ vs', []
- | MemoryCopy, I32 n :: I32 s :: I32 d :: vs' ->
- let mem = memory frame.inst (0l @@ e.at) in
- let dst = I64_convert.extend_i32_u d in
- let src = I64_convert.extend_i32_u s in
- (try Memory.copy mem dst src n; vs', []
- with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at])
+ | MemoryFill, I32 1l :: v :: I32 i :: vs' ->
+ vs', List.map (at e.at) [
+ Plain (Const (I32 i @@ e.at));
+ Plain (Const (v @@ e.at));
+ Plain (Store
+ {ty = I32Type; align = 0; offset = 0l; sz = Some Memory.Pack8});
+ ]
+
+ | MemoryFill, I32 n :: v :: I32 i :: vs' ->
+ vs', List.map (at e.at) [
+ Plain (Const (I32 i @@ e.at));
+ Plain (Const (v @@ e.at));
+ Plain (Const (I32 1l @@ e.at));
+ Plain (MemoryFill);
+ const_i32_add i 1l e.at (memory_error e.at Memory.Bounds);
+ Plain (Const (v @@ e.at));
+ Plain (Const (I32 (I32.sub n 1l) @@ e.at));
+ Plain (MemoryFill);
+ ]
+
+ | MemoryCopy, I32 0l :: I32 s :: I32 d :: vs' ->
+ vs', []
- | MemoryInit x, I32 n :: I32 s :: I32 d :: vs' ->
- let mem = memory frame.inst (0l @@ e.at) in
+ | MemoryCopy, I32 1l :: I32 s :: I32 d :: vs' ->
+ vs', List.map (at e.at) [
+ Plain (Const (I32 d @@ e.at));
+ Plain (Const (I32 s @@ e.at));
+ Plain (Load
+ {ty = I32Type; align = 0; offset = 0l; sz = Some Memory.(Pack8, ZX)});
+ Plain (Store
+ {ty = I32Type; align = 0; offset = 0l; sz = Some Memory.Pack8});
+ ]
+
+ | MemoryCopy, I32 n :: I32 s :: I32 d :: vs' when d <= s ->
+ vs', List.map (at e.at) [
+ Plain (Const (I32 d @@ e.at));
+ Plain (Const (I32 s @@ e.at));
+ Plain (Const (I32 1l @@ e.at));
+ Plain (MemoryCopy);
+ const_i32_add d 1l e.at (memory_error e.at Memory.Bounds);
+ const_i32_add s 1l e.at (memory_error e.at Memory.Bounds);
+ Plain (Const (I32 (I32.sub n 1l) @@ e.at));
+ Plain (MemoryCopy);
+ ]
+
+ | MemoryCopy, I32 n :: I32 s :: I32 d :: vs' when s < d ->
+ vs', List.map (at e.at) [
+ const_i32_add d (I32.sub n 1l) e.at (memory_error e.at Memory.Bounds);
+ const_i32_add s (I32.sub n 1l) e.at (memory_error e.at Memory.Bounds);
+ Plain (Const (I32 1l @@ e.at));
+ Plain (MemoryCopy);
+ Plain (Const (I32 d @@ e.at));
+ Plain (Const (I32 s @@ e.at));
+ Plain (Const (I32 (I32.sub n 1l) @@ e.at));
+ Plain (MemoryCopy);
+ ]
+
+ | MemoryInit x, I32 0l :: I32 s :: I32 d :: vs' ->
+ vs', []
+
+ | MemoryInit x, I32 1l :: I32 s :: I32 d :: vs' ->
(match !(data frame.inst x) with
+ | None ->
+ vs', [Trapping "data segment dropped" @@ e.at]
+ | Some bs when Int32.to_int s >= String.length bs ->
+ vs', [Trapping "out of bounds data segment access" @@ e.at]
| Some bs ->
- let dst = I64_convert.extend_i32_u d in
- let src = I64_convert.extend_i32_u s in
- (try Memory.init mem bs dst src n; vs', []
- with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at])
- | None -> vs', [Trapping "data segment dropped" @@ e.at]
+ let b = Int32.of_int (Char.code bs.[Int32.to_int s]) in
+ vs', List.map (at e.at) [
+ Plain (Const (I32 d @@ e.at));
+ Plain (Const (I32 b @@ e.at));
+ Plain (
+ Store {ty = I32Type; align = 0; offset = 0l; sz = Some Memory.Pack8});
+ ]
)
+ | MemoryInit x, I32 n :: I32 s :: I32 d :: vs' ->
+ vs', List.map (at e.at) [
+ Plain (Const (I32 d @@ e.at));
+ Plain (Const (I32 s @@ e.at));
+ Plain (Const (I32 1l @@ e.at));
+ Plain (MemoryInit x);
+ const_i32_add d 1l e.at (memory_error e.at Memory.Bounds);
+ const_i32_add s 1l e.at (memory_error e.at Memory.Bounds);
+ Plain (Const (I32 (I32.sub n 1l) @@ e.at));
+ Plain (MemoryInit x);
+ ]
+
| DataDrop x, vs ->
let seg = data frame.inst x in
(match !seg with
diff --git a/interpreter/runtime/memory.ml b/interpreter/runtime/memory.ml
index 27a8e6a5..889aa707 100644
--- a/interpreter/runtime/memory.ml
+++ b/interpreter/runtime/memory.ml
@@ -144,34 +144,3 @@ let store_packed sz mem a o v =
| I64 x -> x
| _ -> raise Type
in storen mem a o n x
-
-let init mem bs d s n =
- let load_str_byte a =
- try Char.code bs.[Int64.to_int a]
- with _ -> raise Bounds
- in let rec loop d s n =
- if I32.gt_u n 0l then begin
- store_byte mem d (load_str_byte s);
- loop (Int64.add d 1L) (Int64.add s 1L) (Int32.sub n 1l)
- end
- in loop d s n
-
-let copy mem d s n =
- let n' = I64_convert.extend_i32_u n in
- let rec loop d s n dx =
- if I32.gt_u n 0l then begin
- store_byte mem d (load_byte mem s);
- loop (Int64.add d dx) (Int64.add s dx) (Int32.sub n 1l) dx
- end
- in (if s < d then
- loop Int64.(add d (sub n' 1L)) Int64.(add s (sub n' 1L)) n (-1L)
- else
- loop d s n 1L)
-
-let fill mem a v n =
- let rec loop a n =
- if I32.gt_u n 0l then begin
- store_byte mem a v;
- loop (Int64.add a 1L) (Int32.sub n 1l)
- end
- in loop a n
diff --git a/interpreter/runtime/memory.mli b/interpreter/runtime/memory.mli
index a2071441..0c42124a 100644
--- a/interpreter/runtime/memory.mli
+++ b/interpreter/runtime/memory.mli
@@ -43,8 +43,3 @@ val load_packed :
val store_packed :
pack_size -> memory -> address -> offset -> value -> unit
(* raises Type, Bounds *)
-
-val init :
- memory -> string -> address -> address -> count -> unit (* raises Bounds *)
-val copy : memory -> address -> address -> count -> unit (* raises Bounds *)
-val fill : memory -> address -> int -> count -> unit (* raises Bounds *)
diff --git a/interpreter/util/source.ml b/interpreter/util/source.ml
index 0115825c..f659f6f2 100644
--- a/interpreter/util/source.ml
+++ b/interpreter/util/source.ml
@@ -3,6 +3,7 @@ type region = {left : pos; right : pos}
type 'a phrase = {at : region; it : 'a}
let (@@) x region = {it = x; at = region}
+let at region x = x @@ region
(* Positions and regions *)
diff --git a/interpreter/util/source.mli b/interpreter/util/source.mli
index 8cab3db8..240fe641 100644
--- a/interpreter/util/source.mli
+++ b/interpreter/util/source.mli
@@ -9,3 +9,4 @@ val string_of_pos : pos -> string
val string_of_region : region -> string
val (@@) : 'a -> region -> 'a phrase
+val at : region -> 'a -> 'a phrase
diff --git a/test/core/bulk.wast b/test/core/bulk.wast
index 98c4a49a..b2359d8f 100644
--- a/test/core/bulk.wast
+++ b/test/core/bulk.wast
@@ -148,24 +148,26 @@
;; data.drop
(module
(memory 1)
- (data $p "")
- (data $a 0 (i32.const 0) "")
+ (data $p "x")
+ (data $a 0 (i32.const 0) "x")
(func (export "drop_passive") (data.drop $p))
- (func (export "init_passive")
- (memory.init $p (i32.const 0) (i32.const 0) (i32.const 0)))
+ (func (export "init_passive") (param $len i32)
+ (memory.init $p (i32.const 0) (i32.const 0) (local.get $len)))
(func (export "drop_active") (data.drop $a))
- (func (export "init_active")
- (memory.init $a (i32.const 0) (i32.const 0) (i32.const 0)))
+ (func (export "init_active") (param $len i32)
+ (memory.init $a (i32.const 0) (i32.const 0) (local.get $len)))
)
-(invoke "init_passive")
+(invoke "init_passive" (i32.const 1))
(invoke "drop_passive")
(assert_trap (invoke "drop_passive") "data segment dropped")
-(assert_trap (invoke "init_passive") "data segment dropped")
+(assert_return (invoke "init_passive" (i32.const 0)))
+(assert_trap (invoke "init_passive" (i32.const 1)) "data segment dropped")
(assert_trap (invoke "drop_active") "data segment dropped")
-(assert_trap (invoke "init_active") "data segment dropped")
+(assert_return (invoke "init_active" (i32.const 0)))
+(assert_trap (invoke "init_active" (i32.const 1)) "data segment dropped")
;; table.init