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

[interpreter] Simplify zero-len and drop semantics #126

Merged
merged 5 commits into from
Nov 22, 2019
Merged

[interpreter] Simplify zero-len and drop semantics #126

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
aa61164
[interpreter] Simplify zero-len and drop semantics
rossberg Nov 21, 2019
53a4a2d
Update overview
rossberg Nov 21, 2019
d64d5df
[spec] Change drop semantics
rossberg Nov 21, 2019
6086773
[spec] Forgot to adjust prose for *.init ops
rossberg Nov 21, 2019
ab1369e
[test] Update generated tests for OOBs and dropping changes (#131)
eqrion Nov 22, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
86 changes: 24 additions & 62 deletions document/core/exec/instructions.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -728,7 +728,7 @@ Memory Instructions

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

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

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.

Expand All @@ -746,11 +746,7 @@ Memory Instructions

a. Return.

17. If :math:`\X{data}^? = \epsilon`, then:

a. Trap.

18. If :math:`cnt = 1`, then:
17. If :math:`cnt = 1`, then:

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

Expand All @@ -766,21 +762,21 @@ Memory Instructions

f. Return.

19. Push the value :math:`\I32.\CONST~dst` to the stack.
18. Push the value :math:`\I32.\CONST~dst` to the stack.

20. Push the value :math:`\I32.\CONST~src` to the stack.
19. Push the value :math:`\I32.\CONST~src` to the stack.

21. Push the value :math:`\I32.\CONST~1` to the stack.
20. Push the value :math:`\I32.\CONST~1` to the stack.

22. Execute the instruction :math:`\MEMORYINIT~x`.
21. Execute the instruction :math:`\MEMORYINIT~x`.

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

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

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

26. Execute the instruction :math:`\MEMORYINIT~x`.
25. Execute the instruction :math:`\MEMORYINIT~x`.

.. math::
~\\[-1ex]
Expand Down Expand Up @@ -830,13 +826,7 @@ Memory Instructions

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

5. Let :math:`\X{data}^?` be the optional :ref:`data instance <syntax-datainst>` :math:`S.\SDATA[a]`.

6. If :math:`\X{data}^? = \epsilon`, then:

a. Trap.

7. Replace :math:`S.\SDATA[a]` with :math:`\epsilon`.
5. Replace :math:`S.\SDATA[a]` with the :ref:`data instance <syntax-datainst>` :math:`\{\DIINIT~\epsilon\}`.

.. math::
~\\[-1ex]
Expand All @@ -845,16 +835,7 @@ Memory Instructions
S; F; (\DATADROP~x) &\stepto& S'; F; \epsilon
\end{array}
\\ \qquad
\begin{array}[t]{@{}r@{~}l@{}}
(\iff & S.\SDATA[F.\AMODULE.\MIDATAS[x]] \ne \epsilon \\
\wedge & S' = S \with \SDATA[F.\AMODULE.\MIDATAS[x]] = \epsilon) \\
\end{array}
\\[1ex]
\begin{array}{lcl@{\qquad}l}
S; F; (\DATADROP~x) &\stepto& S; F; \TRAP
\end{array}
\\ \qquad
(\otherwise)
(\iff S' = S \with \SDATA[F.\AMODULE.\MIDATAS[x]] = \{ \DIINIT~\epsilon \}) \\
\end{array}


Expand Down Expand Up @@ -1089,7 +1070,7 @@ Table Instructions

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

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

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.

Expand All @@ -1107,11 +1088,7 @@ Table Instructions

a. Return.

17. If :math:`\X{elem}^? = \epsilon`, then:

a. Trap.

18. If :math:`cnt = 1`, then:
17. If :math:`cnt = 1`, then:

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

Expand All @@ -1127,21 +1104,21 @@ Table Instructions

f. Return.

19. Push the value :math:`\I32.\CONST~dst` to the stack.
18. Push the value :math:`\I32.\CONST~dst` to the stack.

20. Push the value :math:`\I32.\CONST~src` to the stack.
19. Push the value :math:`\I32.\CONST~src` to the stack.

21. Push the value :math:`\I32.\CONST~1` to the stack.
20. Push the value :math:`\I32.\CONST~1` to the stack.

22. Execute the instruction :math:`\TABLEINIT~x`.
21. Execute the instruction :math:`\TABLEINIT~x`.

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

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

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

26. Execute the instruction :math:`\TABLEINIT~x`.
25. Execute the instruction :math:`\TABLEINIT~x`.

.. math::
~\\[-1ex]
Expand Down Expand Up @@ -1191,13 +1168,7 @@ Table Instructions

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

5. Let :math:`\X{elem}^?` be the optional :ref:`elem instance <syntax-eleminst>` :math:`S.\SELEM[a]`.

6. If :math:`\X{elem}^? = \epsilon`, then:

a. Trap.

7. Replace :math:`S.\SELEM[a]` with :math:`\epsilon`.
5. Replace :math:`S.\SELEM[a]` with the :ref:`element instance <syntax-eleminst>` :math:`\{\EIINIT~\epsilon\}`.

.. math::
~\\[-1ex]
Expand All @@ -1206,16 +1177,7 @@ Table Instructions
S; F; (\ELEMDROP~x) &\stepto& S'; F; \epsilon
\end{array}
\\ \qquad
\begin{array}[t]{@{}r@{~}l@{}}
(\iff & S.\SELEM[F.\AMODULE.\MIELEMS[x]] \ne \epsilon \\
\wedge & S' = S \with \SELEM[F.\AMODULE.\MIELEMS[x]] = \epsilon) \\
\end{array}
\\[1ex]
\begin{array}{lcl@{\qquad}l}
S; F; (\ELEMDROP~x) &\stepto& S; F; \TRAP
\end{array}
\\ \qquad
(\otherwise)
(\iff S' = S \with \SELEM[F.\AMODULE.\MIELEMS[x]] = \{ \EIINIT~\epsilon \}) \\
\end{array}


Expand Down
5 changes: 2 additions & 3 deletions document/core/exec/runtime.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,6 @@ Store
The *store* represents all global state that can be manipulated by WebAssembly programs.
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]_

Element and data segments can be dropped by the owning module, in which case the respective instances are replaced with :math:`\epsilon`.
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.

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

Expand Down
97 changes: 40 additions & 57 deletions interpreter/exec/eval.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -122,22 +122,16 @@ let mem_oob frame x i n =
(Memory.bound (memory frame.inst x))

let data_oob frame x i n =
match !(data frame.inst x) with
| None -> false
| Some bs ->
I64.gt_u (I64.add (I64_convert.extend_i32_u i) (I64_convert.extend_i32_u n))
(I64.of_int_u (String.length bs))
I64.gt_u (I64.add (I64_convert.extend_i32_u i) (I64_convert.extend_i32_u n))
(I64.of_int_u (String.length !(data frame.inst x)))

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

let elem_oob frame x i n =
match !(elem frame.inst x) with
| None -> false
| Some es ->
I64.gt_u (I64.add (I64_convert.extend_i32_u i) (I64_convert.extend_i32_u n))
(I64.of_int_u (List.length es))
I64.gt_u (I64.add (I64_convert.extend_i32_u i) (I64_convert.extend_i32_u n))
(I64.of_int_u (List.length !(elem frame.inst x)))

let rec step (c : config) : config =
let {frame; code = vs, es; _} = c in
Expand Down Expand Up @@ -220,42 +214,37 @@ 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")

| TableCopy, I32 0l :: I32 s :: I32 d :: vs' ->
vs', []

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

| TableCopy, I32 0l :: I32 s :: I32 d :: vs' ->
vs', []

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

| TableInit x, I32 0l :: I32 s :: I32 d :: vs' ->
vs', []

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

| TableInit x, I32 0l :: I32 s :: I32 d :: vs' ->
vs', []

(* 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
| Some es ->
(try Table.init tab es d s n; vs', []
with exn -> vs', [Trapping (table_error e.at exn) @@ e.at])
| None -> vs', [Trapping "element segment dropped" @@ e.at]
)
let seg = !(elem frame.inst x) in
(try Table.init tab seg d s n; vs', []
with exn -> vs', [Trapping (table_error e.at exn) @@ e.at])

| ElemDrop x, vs ->
let seg = elem frame.inst x in
(match !seg with
| Some _ -> seg := None; vs, []
| None -> vs, [Trapping "element segment dropped" @@ e.at]
)
seg := [];
vs, []

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

| MemoryFill, I32 0l :: v :: I32 i :: vs' ->
vs', []

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

| MemoryFill, I32 0l :: v :: I32 i :: vs' ->
vs', []

| MemoryFill, I32 n :: v :: I32 i :: vs' ->
vs', List.map (at e.at) [
Plain (Const (I32 i @@ e.at));
Expand All @@ -310,13 +299,13 @@ let rec step (c : config) : config =
Plain (MemoryFill);
]

| MemoryCopy, I32 0l :: I32 s :: I32 d :: vs' ->
vs', []

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

| MemoryCopy, I32 0l :: I32 s :: I32 d :: vs' ->
vs', []

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

| MemoryInit x, I32 0l :: I32 s :: I32 d :: vs' ->
vs', []

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

| MemoryInit x, I32 0l :: I32 s :: I32 d :: vs' ->
vs', []

| MemoryInit x, I32 n :: I32 s :: I32 d :: vs' ->
(match !(data frame.inst x) with
| None ->
vs', [Trapping "data segment dropped" @@ e.at]
| Some bs ->
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});
Plain (Const (I32 (I32.add d 1l) @@ e.at));
Plain (Const (I32 (I32.add s 1l) @@ e.at));
Plain (Const (I32 (I32.sub n 1l) @@ e.at));
Plain (MemoryInit x);
]
)
let seg = !(data frame.inst x) in
let b = Int32.of_int (Char.code seg.[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});
Plain (Const (I32 (I32.add d 1l) @@ e.at));
Plain (Const (I32 (I32.add s 1l) @@ e.at));
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
| Some _ -> seg := None; vs, []
| None -> vs, [Trapping "data segment dropped" @@ e.at]
)
seg := "";
vs, []

| Const v, vs ->
v.it :: vs, []
Expand Down Expand Up @@ -536,11 +519,11 @@ let elem_list inst init =

let create_elem (inst : module_inst) (seg : elem_segment) : elem_inst =
let {etype; einit; _} = seg.it in
ref (Some (elem_list inst einit))
ref (elem_list inst einit)

let create_data (inst : module_inst) (seg : data_segment) : data_inst =
let {dinit; _} = seg.it in
ref (Some dinit)
ref dinit


let add_import (m : module_) (ext : extern) (im : import) (inst : module_inst)
Expand Down
4 changes: 2 additions & 2 deletions interpreter/runtime/instance.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,8 @@ and table_inst = Table.t
and memory_inst = Memory.t
and global_inst = Global.t
and export_inst = Ast.name * extern
and elem_inst = Table.elem list option ref
and data_inst = string option ref
and elem_inst = Table.elem list ref
and data_inst = string ref

and extern =
| ExternFunc of func_inst
Expand Down
Loading