Skip to content
This repository was archived by the owner on Nov 3, 2021. It is now read-only.

Commit 8db23a9

Browse files
rossbergrossberg
authored
[interpreter] Use small-step semantics (#115)
Implement bulk memory operations in small-step semantics, as in spec. Minor fixes: - In spec, memory.copy was missing use of \vconst in the backwards case - In interpreter & test, memory.init still trapped if segment has been dropped but length parameter was 0.
1 parent df2a55f commit 8db23a9

File tree

7 files changed

+109
-65
lines changed

7 files changed

+109
-65
lines changed

‎document/core/exec/instructions.rst

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -695,6 +695,9 @@ Memory Instructions
695695
(\iff n > 1) \\
696696
\end{array}
697697
698+
.. note::
699+
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>`.
700+
698701

699702
.. _exec-memory.init:
700703

@@ -936,12 +939,12 @@ Memory Instructions
936939
\end{array} \\
937940
\end{array}
938941
\\ \qquad
939-
(\iff dst <= src \wedge cnt > 1)
942+
(\iff dst \leq src \wedge cnt > 1)
940943
\\[1ex]
941944
\begin{array}{lcl@{\qquad}l}
942945
S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~cnt)~\MEMORYCOPY &\stepto& S; F;
943946
\begin{array}[t]{@{}l@{}}
944-
(\I32.\CONST~(dst+cnt-1))~(\I32.\CONST~(src+cnt-1))~(\I32.\CONST~1)~\MEMORYCOPY \\
947+
(\vconst_{\I32}(dst+cnt-1))~(\vconst_{\I32}(src+cnt-1))~(\I32.\CONST~1)~\MEMORYCOPY \\
945948
(\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~(cnt-1))~\MEMORYCOPY \\
946949
\end{array} \\
947950
\end{array}

‎interpreter/exec/eval.ml

Lines changed: 91 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -117,6 +117,10 @@ let drop n (vs : 'a stack) at =
117117
* c : config
118118
*)
119119

120+
let const_i32_add i j at msg =
121+
let k = I32.add i j in
122+
if I32.lt_u k i then Trapping msg else Plain (Const (I32 k @@ at))
123+
120124
let rec step (c : config) : config =
121125
let {frame; code = vs, es; _} = c in
122126
let e = List.hd es in
@@ -198,11 +202,13 @@ let rec step (c : config) : config =
198202
with Global.NotMutable -> Crash.error e.at "write to immutable global"
199203
| Global.Type -> Crash.error e.at "type mismatch at global write")
200204

205+
(* TODO: turn into small-step, but needs reference values *)
201206
| TableCopy, I32 n :: I32 s :: I32 d :: vs' ->
202207
let tab = table frame.inst (0l @@ e.at) in
203208
(try Table.copy tab d s n; vs', []
204209
with exn -> vs', [Trapping (table_error e.at exn) @@ e.at])
205210

211+
(* TODO: turn into small-step, but needs reference values *)
206212
| TableInit x, I32 n :: I32 s :: I32 d :: vs' ->
207213
let tab = table frame.inst (0l @@ e.at) in
208214
(match !(elem frame.inst x) with
@@ -253,30 +259,97 @@ let rec step (c : config) : config =
253259
with Memory.SizeOverflow | Memory.SizeLimit | Memory.OutOfMemory -> -1l
254260
in I32 result :: vs', []
255261

256-
| MemoryFill, I32 n :: I32 b :: I32 i :: vs' ->
257-
let mem = memory frame.inst (0l @@ e.at) in
258-
let addr = I64_convert.extend_i32_u i in
259-
(try Memory.fill mem addr (Int32.to_int b) n; vs', []
260-
with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at])
262+
| MemoryFill, I32 0l :: v :: I32 i :: vs' ->
263+
vs', []
261264

262-
| MemoryCopy, I32 n :: I32 s :: I32 d :: vs' ->
263-
let mem = memory frame.inst (0l @@ e.at) in
264-
let dst = I64_convert.extend_i32_u d in
265-
let src = I64_convert.extend_i32_u s in
266-
(try Memory.copy mem dst src n; vs', []
267-
with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at])
265+
| MemoryFill, I32 1l :: v :: I32 i :: vs' ->
266+
vs', List.map (at e.at) [
267+
Plain (Const (I32 i @@ e.at));
268+
Plain (Const (v @@ e.at));
269+
Plain (Store
270+
{ty = I32Type; align = 0; offset = 0l; sz = Some Memory.Pack8});
271+
]
272+
273+
| MemoryFill, I32 n :: v :: I32 i :: vs' ->
274+
vs', List.map (at e.at) [
275+
Plain (Const (I32 i @@ e.at));
276+
Plain (Const (v @@ e.at));
277+
Plain (Const (I32 1l @@ e.at));
278+
Plain (MemoryFill);
279+
const_i32_add i 1l e.at (memory_error e.at Memory.Bounds);
280+
Plain (Const (v @@ e.at));
281+
Plain (Const (I32 (I32.sub n 1l) @@ e.at));
282+
Plain (MemoryFill);
283+
]
284+
285+
| MemoryCopy, I32 0l :: I32 s :: I32 d :: vs' ->
286+
vs', []
268287

269-
| MemoryInit x, I32 n :: I32 s :: I32 d :: vs' ->
270-
let mem = memory frame.inst (0l @@ e.at) in
288+
| MemoryCopy, I32 1l :: I32 s :: I32 d :: vs' ->
289+
vs', List.map (at e.at) [
290+
Plain (Const (I32 d @@ e.at));
291+
Plain (Const (I32 s @@ e.at));
292+
Plain (Load
293+
{ty = I32Type; align = 0; offset = 0l; sz = Some Memory.(Pack8, ZX)});
294+
Plain (Store
295+
{ty = I32Type; align = 0; offset = 0l; sz = Some Memory.Pack8});
296+
]
297+
298+
| MemoryCopy, I32 n :: I32 s :: I32 d :: vs' when d <= s ->
299+
vs', List.map (at e.at) [
300+
Plain (Const (I32 d @@ e.at));
301+
Plain (Const (I32 s @@ e.at));
302+
Plain (Const (I32 1l @@ e.at));
303+
Plain (MemoryCopy);
304+
const_i32_add d 1l e.at (memory_error e.at Memory.Bounds);
305+
const_i32_add s 1l e.at (memory_error e.at Memory.Bounds);
306+
Plain (Const (I32 (I32.sub n 1l) @@ e.at));
307+
Plain (MemoryCopy);
308+
]
309+
310+
| MemoryCopy, I32 n :: I32 s :: I32 d :: vs' when s < d ->
311+
vs', List.map (at e.at) [
312+
const_i32_add d (I32.sub n 1l) e.at (memory_error e.at Memory.Bounds);
313+
const_i32_add s (I32.sub n 1l) e.at (memory_error e.at Memory.Bounds);
314+
Plain (Const (I32 1l @@ e.at));
315+
Plain (MemoryCopy);
316+
Plain (Const (I32 d @@ e.at));
317+
Plain (Const (I32 s @@ e.at));
318+
Plain (Const (I32 (I32.sub n 1l) @@ e.at));
319+
Plain (MemoryCopy);
320+
]
321+
322+
| MemoryInit x, I32 0l :: I32 s :: I32 d :: vs' ->
323+
vs', []
324+
325+
| MemoryInit x, I32 1l :: I32 s :: I32 d :: vs' ->
271326
(match !(data frame.inst x) with
327+
| None ->
328+
vs', [Trapping "data segment dropped" @@ e.at]
329+
| Some bs when Int32.to_int s >= String.length bs ->
330+
vs', [Trapping "out of bounds data segment access" @@ e.at]
272331
| Some bs ->
273-
let dst = I64_convert.extend_i32_u d in
274-
let src = I64_convert.extend_i32_u s in
275-
(try Memory.init mem bs dst src n; vs', []
276-
with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at])
277-
| None -> vs', [Trapping "data segment dropped" @@ e.at]
332+
let b = Int32.of_int (Char.code bs.[Int32.to_int s]) in
333+
vs', List.map (at e.at) [
334+
Plain (Const (I32 d @@ e.at));
335+
Plain (Const (I32 b @@ e.at));
336+
Plain (
337+
Store {ty = I32Type; align = 0; offset = 0l; sz = Some Memory.Pack8});
338+
]
278339
)
279340

341+
| MemoryInit x, I32 n :: I32 s :: I32 d :: vs' ->
342+
vs', List.map (at e.at) [
343+
Plain (Const (I32 d @@ e.at));
344+
Plain (Const (I32 s @@ e.at));
345+
Plain (Const (I32 1l @@ e.at));
346+
Plain (MemoryInit x);
347+
const_i32_add d 1l e.at (memory_error e.at Memory.Bounds);
348+
const_i32_add s 1l e.at (memory_error e.at Memory.Bounds);
349+
Plain (Const (I32 (I32.sub n 1l) @@ e.at));
350+
Plain (MemoryInit x);
351+
]
352+
280353
| DataDrop x, vs ->
281354
let seg = data frame.inst x in
282355
(match !seg with

‎interpreter/runtime/memory.ml

Lines changed: 0 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -144,34 +144,3 @@ let store_packed sz mem a o v =
144144
| I64 x -> x
145145
| _ -> raise Type
146146
in storen mem a o n x
147-
148-
let init mem bs d s n =
149-
let load_str_byte a =
150-
try Char.code bs.[Int64.to_int a]
151-
with _ -> raise Bounds
152-
in let rec loop d s n =
153-
if I32.gt_u n 0l then begin
154-
store_byte mem d (load_str_byte s);
155-
loop (Int64.add d 1L) (Int64.add s 1L) (Int32.sub n 1l)
156-
end
157-
in loop d s n
158-
159-
let copy mem d s n =
160-
let n' = I64_convert.extend_i32_u n in
161-
let rec loop d s n dx =
162-
if I32.gt_u n 0l then begin
163-
store_byte mem d (load_byte mem s);
164-
loop (Int64.add d dx) (Int64.add s dx) (Int32.sub n 1l) dx
165-
end
166-
in (if s < d then
167-
loop Int64.(add d (sub n' 1L)) Int64.(add s (sub n' 1L)) n (-1L)
168-
else
169-
loop d s n 1L)
170-
171-
let fill mem a v n =
172-
let rec loop a n =
173-
if I32.gt_u n 0l then begin
174-
store_byte mem a v;
175-
loop (Int64.add a 1L) (Int32.sub n 1l)
176-
end
177-
in loop a n

‎interpreter/runtime/memory.mli

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -43,8 +43,3 @@ val load_packed :
4343
val store_packed :
4444
pack_size -> memory -> address -> offset -> value -> unit
4545
(* raises Type, Bounds *)
46-
47-
val init :
48-
memory -> string -> address -> address -> count -> unit (* raises Bounds *)
49-
val copy : memory -> address -> address -> count -> unit (* raises Bounds *)
50-
val fill : memory -> address -> int -> count -> unit (* raises Bounds *)

‎interpreter/util/source.ml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ type region = {left : pos; right : pos}
33
type 'a phrase = {at : region; it : 'a}
44

55
let (@@) x region = {it = x; at = region}
6+
let at region x = x @@ region
67

78

89
(* Positions and regions *)

‎interpreter/util/source.mli

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,3 +9,4 @@ val string_of_pos : pos -> string
99
val string_of_region : region -> string
1010

1111
val (@@) : 'a -> region -> 'a phrase
12+
val at : region -> 'a -> 'a phrase

‎test/core/bulk.wast

Lines changed: 11 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -148,24 +148,26 @@
148148
;; data.drop
149149
(module
150150
(memory 1)
151-
(data $p "")
152-
(data $a 0 (i32.const 0) "")
151+
(data $p "x")
152+
(data $a 0 (i32.const 0) "x")
153153

154154
(func (export "drop_passive") (data.drop $p))
155-
(func (export "init_passive")
156-
(memory.init $p (i32.const 0) (i32.const 0) (i32.const 0)))
155+
(func (export "init_passive") (param $len i32)
156+
(memory.init $p (i32.const 0) (i32.const 0) (local.get $len)))
157157

158158
(func (export "drop_active") (data.drop $a))
159-
(func (export "init_active")
160-
(memory.init $a (i32.const 0) (i32.const 0) (i32.const 0)))
159+
(func (export "init_active") (param $len i32)
160+
(memory.init $a (i32.const 0) (i32.const 0) (local.get $len)))
161161
)
162162

163-
(invoke "init_passive")
163+
(invoke "init_passive" (i32.const 1))
164164
(invoke "drop_passive")
165165
(assert_trap (invoke "drop_passive") "data segment dropped")
166-
(assert_trap (invoke "init_passive") "data segment dropped")
166+
(assert_return (invoke "init_passive" (i32.const 0)))
167+
(assert_trap (invoke "init_passive" (i32.const 1)) "data segment dropped")
167168
(assert_trap (invoke "drop_active") "data segment dropped")
168-
(assert_trap (invoke "init_active") "data segment dropped")
169+
(assert_return (invoke "init_active" (i32.const 0)))
170+
(assert_trap (invoke "init_active" (i32.const 1)) "data segment dropped")
169171

170172

171173
;; table.init

0 commit comments

Comments
 (0)