Skip to content
This repository was archived by the owner on Apr 25, 2025. It is now read-only.

Commit b2a5c4f

Browse files
rossbergrossberg
authored
[interpreter] Simplify zero-len and drop semantics (#126)
* [interpreter] Simplify zero-len and drop semantics * Update overview * [spec] Change drop semantics * [spec] Forgot to adjust prose for *.init ops * [test] Update generated tests for OOBs and dropping changes (#131)
1 parent 24b0882 commit b2a5c4f

18 files changed

+260
-213
lines changed

‎document/core/exec/instructions.rst

Lines changed: 24 additions & 62 deletions
Original file line numberDiff line numberDiff line change
@@ -728,7 +728,7 @@ Memory Instructions
728728

729729
8. Assert: due to :ref:`validation <valid-memory.init>`, :math:`S.\SDATA[\X{da}]` exists.
730730

731-
9. Let :math:`\X{data}^?` be the optional :ref:`data instance <syntax-datainst>` :math:`S.\SDATA[\X{da}]`.
731+
9. Let :math:`\X{data}` be the :ref:`data instance <syntax-datainst>` :math:`S.\SDATA[\X{da}]`.
732732

733733
10. Assert: due to :ref:`validation <valid-memory.init>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
734734

@@ -746,11 +746,7 @@ Memory Instructions
746746

747747
a. Return.
748748

749-
17. If :math:`\X{data}^? = \epsilon`, then:
750-
751-
a. Trap.
752-
753-
18. If :math:`cnt = 1`, then:
749+
17. If :math:`cnt = 1`, then:
754750

755751
a. Push the value :math:`\I32.\CONST~dst` to the stack.
756752

@@ -766,21 +762,21 @@ Memory Instructions
766762

767763
f. Return.
768764

769-
19. Push the value :math:`\I32.\CONST~dst` to the stack.
765+
18. Push the value :math:`\I32.\CONST~dst` to the stack.
770766

771-
20. Push the value :math:`\I32.\CONST~src` to the stack.
767+
19. Push the value :math:`\I32.\CONST~src` to the stack.
772768

773-
21. Push the value :math:`\I32.\CONST~1` to the stack.
769+
20. Push the value :math:`\I32.\CONST~1` to the stack.
774770

775-
22. Execute the instruction :math:`\MEMORYINIT~x`.
771+
21. Execute the instruction :math:`\MEMORYINIT~x`.
776772

777-
23. Push the value :math:`\vconst_{\I32}(dst+1)` to the stack.
773+
22. Push the value :math:`\vconst_{\I32}(dst+1)` to the stack.
778774

779-
24. Push the value :math:`\vconst_{\I32}(src+1)` to the stack.
775+
23. Push the value :math:`\vconst_{\I32}(src+1)` to the stack.
780776

781-
25. Push the value :math:`\I32.\CONST~(cnt-1)` to the stack.
777+
24. Push the value :math:`\I32.\CONST~(cnt-1)` to the stack.
782778

783-
26. Execute the instruction :math:`\MEMORYINIT~x`.
779+
25. Execute the instruction :math:`\MEMORYINIT~x`.
784780

785781
.. math::
786782
~\\[-1ex]
@@ -830,13 +826,7 @@ Memory Instructions
830826

831827
4. Assert: due to :ref:`validation <valid-data.drop>`, :math:`S.\SDATA[a]` exists.
832828

833-
5. Let :math:`\X{data}^?` be the optional :ref:`data instance <syntax-datainst>` :math:`S.\SDATA[a]`.
834-
835-
6. If :math:`\X{data}^? = \epsilon`, then:
836-
837-
a. Trap.
838-
839-
7. Replace :math:`S.\SDATA[a]` with :math:`\epsilon`.
829+
5. Replace :math:`S.\SDATA[a]` with the :ref:`data instance <syntax-datainst>` :math:`\{\DIINIT~\epsilon\}`.
840830

841831
.. math::
842832
~\\[-1ex]
@@ -845,16 +835,7 @@ Memory Instructions
845835
S; F; (\DATADROP~x) &\stepto& S'; F; \epsilon
846836
\end{array}
847837
\\ \qquad
848-
\begin{array}[t]{@{}r@{~}l@{}}
849-
(\iff & S.\SDATA[F.\AMODULE.\MIDATAS[x]] \ne \epsilon \\
850-
\wedge & S' = S \with \SDATA[F.\AMODULE.\MIDATAS[x]] = \epsilon) \\
851-
\end{array}
852-
\\[1ex]
853-
\begin{array}{lcl@{\qquad}l}
854-
S; F; (\DATADROP~x) &\stepto& S; F; \TRAP
855-
\end{array}
856-
\\ \qquad
857-
(\otherwise)
838+
(\iff S' = S \with \SDATA[F.\AMODULE.\MIDATAS[x]] = \{ \DIINIT~\epsilon \}) \\
858839
\end{array}
859840
860841
@@ -1089,7 +1070,7 @@ Table Instructions
10891070

10901071
8. Assert: due to :ref:`validation <valid-table.init>`, :math:`S.\SELEM[\X{ea}]` exists.
10911072

1092-
9. Let :math:`\X{elem}^?` be the optional :ref:`element instance <syntax-eleminst>` :math:`S.\SELEM[\X{ea}]`.
1073+
9. Let :math:`\X{elem}` be the :ref:`element instance <syntax-eleminst>` :math:`S.\SELEM[\X{ea}]`.
10931074

10941075
10. Assert: due to :ref:`validation <valid-table.init>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
10951076

@@ -1107,11 +1088,7 @@ Table Instructions
11071088

11081089
a. Return.
11091090

1110-
17. If :math:`\X{elem}^? = \epsilon`, then:
1111-
1112-
a. Trap.
1113-
1114-
18. If :math:`cnt = 1`, then:
1091+
17. If :math:`cnt = 1`, then:
11151092

11161093
a. Push the value :math:`\I32.\CONST~dst` to the stack.
11171094

@@ -1127,21 +1104,21 @@ Table Instructions
11271104

11281105
f. Return.
11291106

1130-
19. Push the value :math:`\I32.\CONST~dst` to the stack.
1107+
18. Push the value :math:`\I32.\CONST~dst` to the stack.
11311108

1132-
20. Push the value :math:`\I32.\CONST~src` to the stack.
1109+
19. Push the value :math:`\I32.\CONST~src` to the stack.
11331110

1134-
21. Push the value :math:`\I32.\CONST~1` to the stack.
1111+
20. Push the value :math:`\I32.\CONST~1` to the stack.
11351112

1136-
22. Execute the instruction :math:`\TABLEINIT~x`.
1113+
21. Execute the instruction :math:`\TABLEINIT~x`.
11371114

1138-
23. Push the value :math:`\vconst_{\I32}(dst+1)` to the stack.
1115+
22. Push the value :math:`\vconst_{\I32}(dst+1)` to the stack.
11391116

1140-
24. Push the value :math:`\vconst_{\I32}(src+1)` to the stack.
1117+
23. Push the value :math:`\vconst_{\I32}(src+1)` to the stack.
11411118

1142-
25. Push the value :math:`\I32.\CONST~(cnt-1)` to the stack.
1119+
24. Push the value :math:`\I32.\CONST~(cnt-1)` to the stack.
11431120

1144-
26. Execute the instruction :math:`\TABLEINIT~x`.
1121+
25. Execute the instruction :math:`\TABLEINIT~x`.
11451122

11461123
.. math::
11471124
~\\[-1ex]
@@ -1191,13 +1168,7 @@ Table Instructions
11911168

11921169
4. Assert: due to :ref:`validation <valid-elem.drop>`, :math:`S.\SELEM[a]` exists.
11931170

1194-
5. Let :math:`\X{elem}^?` be the optional :ref:`elem instance <syntax-eleminst>` :math:`S.\SELEM[a]`.
1195-
1196-
6. If :math:`\X{elem}^? = \epsilon`, then:
1197-
1198-
a. Trap.
1199-
1200-
7. Replace :math:`S.\SELEM[a]` with :math:`\epsilon`.
1171+
5. Replace :math:`S.\SELEM[a]` with the :ref:`element instance <syntax-eleminst>` :math:`\{\EIINIT~\epsilon\}`.
12011172

12021173
.. math::
12031174
~\\[-1ex]
@@ -1206,16 +1177,7 @@ Table Instructions
12061177
S; F; (\ELEMDROP~x) &\stepto& S'; F; \epsilon
12071178
\end{array}
12081179
\\ \qquad
1209-
\begin{array}[t]{@{}r@{~}l@{}}
1210-
(\iff & S.\SELEM[F.\AMODULE.\MIELEMS[x]] \ne \epsilon \\
1211-
\wedge & S' = S \with \SELEM[F.\AMODULE.\MIELEMS[x]] = \epsilon) \\
1212-
\end{array}
1213-
\\[1ex]
1214-
\begin{array}{lcl@{\qquad}l}
1215-
S; F; (\ELEMDROP~x) &\stepto& S; F; \TRAP
1216-
\end{array}
1217-
\\ \qquad
1218-
(\otherwise)
1180+
(\iff S' = S \with \SELEM[F.\AMODULE.\MIELEMS[x]] = \{ \EIINIT~\epsilon \}) \\
12191181
\end{array}
12201182
12211183

‎document/core/exec/runtime.rst

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,6 @@ Store
7575
The *store* represents all global state that can be manipulated by WebAssembly programs.
7676
It consists of the runtime representation of all *instances* of :ref:`functions <syntax-funcinst>`, :ref:`tables <syntax-tableinst>`, :ref:`memories <syntax-meminst>`, and :ref:`globals <syntax-globalinst>`, :ref:`element segments <syntax-eleminst>`, and :ref:`data segments <syntax-datainst>` that have been :ref:`allocated <alloc>` during the life time of the abstract machine. [#gc]_
7777

78-
Element and data segments can be dropped by the owning module, in which case the respective instances are replaced with :math:`\epsilon`.
7978
It is an invariant of the semantics that no element or data instance is :ref:`addressed <syntax-addr>` from anywhere else but the owning module instances.
8079

8180
Syntactically, the store is defined as a :ref:`record <notation-record>` listing the existing instances of each category:
@@ -88,8 +87,8 @@ Syntactically, the store is defined as a :ref:`record <notation-record>` listing
8887
\STABLES & \tableinst^\ast, \\
8988
\SMEMS & \meminst^\ast, \\
9089
\SGLOBALS & \globalinst^\ast, \\
91-
\SELEM & (\eleminst^?)^\ast, \\
92-
\SDATA & (\datainst^?)^\ast ~\} \\
90+
\SELEM & \eleminst^\ast, \\
91+
\SDATA & \datainst^\ast ~\} \\
9392
\end{array}
9493
\end{array}
9594

‎interpreter/exec/eval.ml

Lines changed: 40 additions & 57 deletions
Original file line numberDiff line numberDiff line change
@@ -122,22 +122,16 @@ let mem_oob frame x i n =
122122
(Memory.bound (memory frame.inst x))
123123

124124
let data_oob frame x i n =
125-
match !(data frame.inst x) with
126-
| None -> false
127-
| Some bs ->
128-
I64.gt_u (I64.add (I64_convert.extend_i32_u i) (I64_convert.extend_i32_u n))
129-
(I64.of_int_u (String.length bs))
125+
I64.gt_u (I64.add (I64_convert.extend_i32_u i) (I64_convert.extend_i32_u n))
126+
(I64.of_int_u (String.length !(data frame.inst x)))
130127

131128
let table_oob frame x i n =
132129
I64.gt_u (I64.add (I64_convert.extend_i32_u i) (I64_convert.extend_i32_u n))
133130
(I64_convert.extend_i32_u (Table.size (table frame.inst x)))
134131

135132
let elem_oob frame x i n =
136-
match !(elem frame.inst x) with
137-
| None -> false
138-
| Some es ->
139-
I64.gt_u (I64.add (I64_convert.extend_i32_u i) (I64_convert.extend_i32_u n))
140-
(I64.of_int_u (List.length es))
133+
I64.gt_u (I64.add (I64_convert.extend_i32_u i) (I64_convert.extend_i32_u n))
134+
(I64.of_int_u (List.length !(elem frame.inst x)))
141135

142136
let rec step (c : config) : config =
143137
let {frame; code = vs, es; _} = c in
@@ -220,42 +214,37 @@ let rec step (c : config) : config =
220214
with Global.NotMutable -> Crash.error e.at "write to immutable global"
221215
| Global.Type -> Crash.error e.at "type mismatch at global write")
222216

223-
| TableCopy, I32 0l :: I32 s :: I32 d :: vs' ->
224-
vs', []
225-
226217
| TableCopy, I32 n :: I32 s :: I32 d :: vs'
227218
when table_oob frame (0l @@ e.at) s n || table_oob frame (0l @@ e.at) d n ->
228219
vs', [Trapping (table_error e.at Table.Bounds) @@ e.at]
229220

221+
| TableCopy, I32 0l :: I32 s :: I32 d :: vs' ->
222+
vs', []
223+
230224
(* TODO: turn into small-step, but needs reference values *)
231225
| TableCopy, I32 n :: I32 s :: I32 d :: vs' ->
232226
let tab = table frame.inst (0l @@ e.at) in
233227
(try Table.copy tab d s n; vs', []
234228
with exn -> vs', [Trapping (table_error e.at exn) @@ e.at])
235229

236-
| TableInit x, I32 0l :: I32 s :: I32 d :: vs' ->
237-
vs', []
238-
239230
| TableInit x, I32 n :: I32 s :: I32 d :: vs'
240231
when table_oob frame (0l @@ e.at) d n || elem_oob frame x s n ->
241232
vs', [Trapping (table_error e.at Table.Bounds) @@ e.at]
242233

234+
| TableInit x, I32 0l :: I32 s :: I32 d :: vs' ->
235+
vs', []
236+
243237
(* TODO: turn into small-step, but needs reference values *)
244238
| TableInit x, I32 n :: I32 s :: I32 d :: vs' ->
245239
let tab = table frame.inst (0l @@ e.at) in
246-
(match !(elem frame.inst x) with
247-
| Some es ->
248-
(try Table.init tab es d s n; vs', []
249-
with exn -> vs', [Trapping (table_error e.at exn) @@ e.at])
250-
| None -> vs', [Trapping "element segment dropped" @@ e.at]
251-
)
240+
let seg = !(elem frame.inst x) in
241+
(try Table.init tab seg d s n; vs', []
242+
with exn -> vs', [Trapping (table_error e.at exn) @@ e.at])
252243

253244
| ElemDrop x, vs ->
254245
let seg = elem frame.inst x in
255-
(match !seg with
256-
| Some _ -> seg := None; vs, []
257-
| None -> vs, [Trapping "element segment dropped" @@ e.at]
258-
)
246+
seg := [];
247+
vs, []
259248

260249
| Load {offset; ty; sz; _}, I32 i :: vs' ->
261250
let mem = memory frame.inst (0l @@ e.at) in
@@ -291,13 +280,13 @@ let rec step (c : config) : config =
291280
with Memory.SizeOverflow | Memory.SizeLimit | Memory.OutOfMemory -> -1l
292281
in I32 result :: vs', []
293282

294-
| MemoryFill, I32 0l :: v :: I32 i :: vs' ->
295-
vs', []
296-
297283
| MemoryFill, I32 n :: v :: I32 i :: vs'
298284
when mem_oob frame (0l @@ e.at) i n ->
299285
vs', [Trapping (memory_error e.at Memory.Bounds) @@ e.at]
300286

287+
| MemoryFill, I32 0l :: v :: I32 i :: vs' ->
288+
vs', []
289+
301290
| MemoryFill, I32 n :: v :: I32 i :: vs' ->
302291
vs', List.map (at e.at) [
303292
Plain (Const (I32 i @@ e.at));
@@ -310,13 +299,13 @@ let rec step (c : config) : config =
310299
Plain (MemoryFill);
311300
]
312301

313-
| MemoryCopy, I32 0l :: I32 s :: I32 d :: vs' ->
314-
vs', []
315-
316302
| MemoryCopy, I32 n :: I32 s :: I32 d :: vs'
317303
when mem_oob frame (0l @@ e.at) s n || mem_oob frame (0l @@ e.at) d n ->
318304
vs', [Trapping (memory_error e.at Memory.Bounds) @@ e.at]
319305

306+
| MemoryCopy, I32 0l :: I32 s :: I32 d :: vs' ->
307+
vs', []
308+
320309
| MemoryCopy, I32 n :: I32 s :: I32 d :: vs' when d <= s ->
321310
vs', List.map (at e.at) [
322311
Plain (Const (I32 d @@ e.at));
@@ -345,37 +334,31 @@ let rec step (c : config) : config =
345334
{ty = I32Type; align = 0; offset = 0l; sz = Some Memory.Pack8});
346335
]
347336

348-
| MemoryInit x, I32 0l :: I32 s :: I32 d :: vs' ->
349-
vs', []
350-
351337
| MemoryInit x, I32 n :: I32 s :: I32 d :: vs'
352338
when mem_oob frame (0l @@ e.at) d n || data_oob frame x s n ->
353339
vs', [Trapping (memory_error e.at Memory.Bounds) @@ e.at]
354340

341+
| MemoryInit x, I32 0l :: I32 s :: I32 d :: vs' ->
342+
vs', []
343+
355344
| MemoryInit x, I32 n :: I32 s :: I32 d :: vs' ->
356-
(match !(data frame.inst x) with
357-
| None ->
358-
vs', [Trapping "data segment dropped" @@ e.at]
359-
| Some bs ->
360-
let b = Int32.of_int (Char.code bs.[Int32.to_int s]) in
361-
vs', List.map (at e.at) [
362-
Plain (Const (I32 d @@ e.at));
363-
Plain (Const (I32 b @@ e.at));
364-
Plain (
365-
Store {ty = I32Type; align = 0; offset = 0l; sz = Some Memory.Pack8});
366-
Plain (Const (I32 (I32.add d 1l) @@ e.at));
367-
Plain (Const (I32 (I32.add s 1l) @@ e.at));
368-
Plain (Const (I32 (I32.sub n 1l) @@ e.at));
369-
Plain (MemoryInit x);
370-
]
371-
)
345+
let seg = !(data frame.inst x) in
346+
let b = Int32.of_int (Char.code seg.[Int32.to_int s]) in
347+
vs', List.map (at e.at) [
348+
Plain (Const (I32 d @@ e.at));
349+
Plain (Const (I32 b @@ e.at));
350+
Plain (
351+
Store {ty = I32Type; align = 0; offset = 0l; sz = Some Memory.Pack8});
352+
Plain (Const (I32 (I32.add d 1l) @@ e.at));
353+
Plain (Const (I32 (I32.add s 1l) @@ e.at));
354+
Plain (Const (I32 (I32.sub n 1l) @@ e.at));
355+
Plain (MemoryInit x);
356+
]
372357

373358
| DataDrop x, vs ->
374359
let seg = data frame.inst x in
375-
(match !seg with
376-
| Some _ -> seg := None; vs, []
377-
| None -> vs, [Trapping "data segment dropped" @@ e.at]
378-
)
360+
seg := "";
361+
vs, []
379362

380363
| Const v, vs ->
381364
v.it :: vs, []
@@ -536,11 +519,11 @@ let elem_list inst init =
536519

537520
let create_elem (inst : module_inst) (seg : elem_segment) : elem_inst =
538521
let {etype; einit; _} = seg.it in
539-
ref (Some (elem_list inst einit))
522+
ref (elem_list inst einit)
540523

541524
let create_data (inst : module_inst) (seg : data_segment) : data_inst =
542525
let {dinit; _} = seg.it in
543-
ref (Some dinit)
526+
ref dinit
544527

545528

546529
let add_import (m : module_) (ext : extern) (im : import) (inst : module_inst)

‎interpreter/runtime/instance.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,8 @@ and table_inst = Table.t
1717
and memory_inst = Memory.t
1818
and global_inst = Global.t
1919
and export_inst = Ast.name * extern
20-
and elem_inst = Table.elem list option ref
21-
and data_inst = string option ref
20+
and elem_inst = Table.elem list ref
21+
and data_inst = string ref
2222

2323
and extern =
2424
| ExternFunc of func_inst

0 commit comments

Comments
 (0)