[interpreter] Use small-step semantics

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}

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

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

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 *)

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 *)

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

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