Skip to content

Commit

Permalink
[spec] Rename memory instructions (#720)
Browse files Browse the repository at this point in the history
  • Loading branch information
rossberg authored Apr 4, 2018
1 parent 04a9b6e commit b3de271
Show file tree
Hide file tree
Showing 33 changed files with 159 additions and 159 deletions.
4 changes: 2 additions & 2 deletions document/core/appendix/index-instructions.rst
Original file line number Diff line number Diff line change
Expand Up @@ -70,8 +70,8 @@ Instruction Binary Opcode Type
:math:`\I64.\STORE\K{8}~\memarg` :math:`\hex{3C}` :math:`[\I32~\I64] \to []` :ref:`validation <valid-storen>` :ref:`execution <exec-storen>`
:math:`\I64.\STORE\K{16}~\memarg` :math:`\hex{3D}` :math:`[\I32~\I64] \to []` :ref:`validation <valid-storen>` :ref:`execution <exec-storen>`
:math:`\I64.\STORE\K{32}~\memarg` :math:`\hex{3E}` :math:`[\I32~\I64] \to []` :ref:`validation <valid-storen>` :ref:`execution <exec-storen>`
:math:`\CURRENTMEMORY` :math:`\hex{3F}` :math:`[] \to [\I32]` :ref:`validation <valid-current_memory>` :ref:`execution <exec-current_memory>`
:math:`\GROWMEMORY` :math:`\hex{40}` :math:`[\I32] \to [\I32]` :ref:`validation <valid-grow_memory>` :ref:`execution <exec-grow_memory>`
:math:`\MEMORYSIZE` :math:`\hex{3F}` :math:`[] \to [\I32]` :ref:`validation <valid-memory.size>` :ref:`execution <exec-memory.size>`
:math:`\MEMORYGROW` :math:`\hex{40}` :math:`[\I32] \to [\I32]` :ref:`validation <valid-memory.grow>` :ref:`execution <exec-memory.grow>`
:math:`\I32.\CONST~\i32` :math:`\hex{41}` :math:`[] \to [\I32]` :ref:`validation <valid-const>` :ref:`execution <exec-const>`
:math:`\I64.\CONST~\i64` :math:`\hex{42}` :math:`[] \to [\I64]` :ref:`validation <valid-const>` :ref:`execution <exec-const>`
:math:`\F32.\CONST~\f32` :math:`\hex{43}` :math:`[] \to [\F32]` :ref:`validation <valid-const>` :ref:`execution <exec-const>`
Expand Down
10 changes: 5 additions & 5 deletions document/core/binary/instructions.rst
Original file line number Diff line number Diff line change
Expand Up @@ -124,8 +124,8 @@ Each variant of :ref:`memory instruction <syntax-instr-memory>` is encoded with
.. _binary-loadn:
.. _binary-store:
.. _binary-storen:
.. _binary-current_memory:
.. _binary-grow_memory:
.. _binary-memory.size:
.. _binary-memory.grow:

.. math::
\begin{array}{llclll}
Expand Down Expand Up @@ -155,12 +155,12 @@ Each variant of :ref:`memory instruction <syntax-instr-memory>` is encoded with
\hex{3C}~~m{:}\Bmemarg &\Rightarrow& \I64.\STORE\K{8}~m \\ &&|&
\hex{3D}~~m{:}\Bmemarg &\Rightarrow& \I64.\STORE\K{16}~m \\ &&|&
\hex{3E}~~m{:}\Bmemarg &\Rightarrow& \I64.\STORE\K{32}~m \\ &&|&
\hex{3F}~~\hex{00} &\Rightarrow& \CURRENTMEMORY \\ &&|&
\hex{40}~~\hex{00} &\Rightarrow& \GROWMEMORY \\
\hex{3F}~~\hex{00} &\Rightarrow& \MEMORYSIZE \\ &&|&
\hex{40}~~\hex{00} &\Rightarrow& \MEMORYGROW \\
\end{array}
.. note::
In future versions of WebAssembly, the additional zero bytes occurring in the encoding of the |CURRENTMEMORY| and |GROWMEMORY| instructions may be used to index additional memories.
In future versions of WebAssembly, the additional zero bytes occurring in the encoding of the |MEMORYSIZE| and |MEMORYGROW| instructions may be used to index additional memories.


.. index:: numeric instruction
Expand Down
28 changes: 14 additions & 14 deletions document/core/exec/instructions.rst
Original file line number Diff line number Diff line change
Expand Up @@ -533,18 +533,18 @@ Memory Instructions
\end{array}
.. _exec-current_memory:
.. _exec-memory.size:

:math:`\CURRENTMEMORY`
......................
:math:`\MEMORYSIZE`
...................

1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.

2. Assert: due to :ref:`validation <valid-current_memory>`, :math:`F.\AMODULE.\MIMEMS[0]` exists.
2. Assert: due to :ref:`validation <valid-memory.size>`, :math:`F.\AMODULE.\MIMEMS[0]` exists.

3. Let :math:`a` be the :ref:`memory address <syntax-memaddr>` :math:`F.\AMODULE.\MIMEMS[0]`.

4. Assert: due to :ref:`validation <valid-current_memory>`, :math:`S.\SMEMS[a]` exists.
4. Assert: due to :ref:`validation <valid-memory.size>`, :math:`S.\SMEMS[a]` exists.

5. Let :math:`\X{mem}` be the :ref:`memory instance <syntax-meminst>` :math:`S.\SMEMS[a]`.

Expand All @@ -555,31 +555,31 @@ Memory Instructions
.. math::
\begin{array}{l}
\begin{array}{lcl@{\qquad}l}
S; F; \CURRENTMEMORY &\stepto& S; F; (\I32.\CONST~\X{sz})
S; F; \MEMORYSIZE &\stepto& S; F; (\I32.\CONST~\X{sz})
\end{array}
\\ \qquad
(\iff |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA| = \X{sz}\cdot64\,\F{Ki}) \\
\end{array}
.. _exec-grow_memory:
.. _exec-memory.grow:

:math:`\GROWMEMORY`
:math:`\MEMORYGROW`
...................

1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.

2. Assert: due to :ref:`validation <valid-grow_memory>`, :math:`F.\AMODULE.\MIMEMS[0]` exists.
2. Assert: due to :ref:`validation <valid-memory.grow>`, :math:`F.\AMODULE.\MIMEMS[0]` exists.

3. Let :math:`a` be the :ref:`memory address <syntax-memaddr>` :math:`F.\AMODULE.\MIMEMS[0]`.

4. Assert: due to :ref:`validation <valid-grow_memory>`, :math:`S.\SMEMS[a]` exists.
4. Assert: due to :ref:`validation <valid-memory.grow>`, :math:`S.\SMEMS[a]` exists.

5. Let :math:`\X{mem}` be the :ref:`memory instance <syntax-meminst>` :math:`S.\SMEMS[a]`.

6. Let :math:`\X{sz}` be the length of :math:`S.\SMEMS[a]` divided by the :ref:`page size <page-size>`.

7. Assert: due to :ref:`validation <valid-grow_memory>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
7. Assert: due to :ref:`validation <valid-memory.grow>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.

8. Pop the value :math:`\I32.\CONST~n` from the stack.

Expand All @@ -595,7 +595,7 @@ Memory Instructions
~\\[-1ex]
\begin{array}{l}
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~n)~\GROWMEMORY &\stepto& S'; F; (\I32.\CONST~\X{sz})
S; F; (\I32.\CONST~n)~\MEMORYGROW &\stepto& S'; F; (\I32.\CONST~\X{sz})
\end{array}
\\ \qquad
\begin{array}[t]{@{}r@{~}l@{}}
Expand All @@ -605,12 +605,12 @@ Memory Instructions
\end{array}
\\[1ex]
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~n)~\GROWMEMORY &\stepto& S; F; (\I32.\CONST~{-1})
S; F; (\I32.\CONST~n)~\MEMORYGROW &\stepto& S; F; (\I32.\CONST~{-1})
\end{array}
\end{array}
.. note::
The |GROWMEMORY| instruction is non-deterministic.
The |MEMORYGROW| instruction is non-deterministic.
It may either succeed, returning the old memory size :math:`\X{sz}`,
or fail, returning :math:`{-1}`.
Failure *must* occur if the referenced memory instance has a maximum size defined that would be exceeded.
Expand Down
8 changes: 4 additions & 4 deletions document/core/syntax/instructions.rst
Original file line number Diff line number Diff line change
Expand Up @@ -240,8 +240,8 @@ Instructions in this group are concerned with linear :ref:`memory <syntax-mem>`.
\K{i}\X{nn}\K{.}\STORE\K{8}~\memarg ~|~
\K{i}\X{nn}\K{.}\STORE\K{16}~\memarg ~|~
\K{i64.}\STORE\K{32}~\memarg \\&&|&
\CURRENTMEMORY \\&&|&
\GROWMEMORY \\
\MEMORYSIZE \\&&|&
\MEMORYGROW \\
\end{array}
Memory is accessed with |LOAD| and |STORE| instructions for the different :ref:`value types <syntax-valtype>`.
Expand All @@ -256,8 +256,8 @@ A :ref:`trap <trap>` results if any of the accessed memory bytes lies outside th
.. note::
Future version of WebAssembly might provide memory instructions with 64 bit address ranges.

The |CURRENTMEMORY| instruction returns the current size of a memory.
The |GROWMEMORY| instruction grows memory by a given delta and returns the previous size, or :math:`-1` if enough memory cannot be allocated.
The |MEMORYSIZE| instruction returns the current size of a memory.
The |MEMORYGROW| instruction grows memory by a given delta and returns the previous size, or :math:`-1` if enough memory cannot be allocated.
Both instructions operate in units of :ref:`page size <page-size>`.

.. note::
Expand Down
8 changes: 4 additions & 4 deletions document/core/text/instructions.rst
Original file line number Diff line number Diff line change
Expand Up @@ -173,8 +173,8 @@ Memory Instructions
.. _text-loadn:
.. _text-store:
.. _text-storen:
.. _text-current_memory:
.. _text-grow_memory:
.. _text-memory.size:
.. _text-memory.grow:

The offset and alignment immediates to memory instructions are optional.
The offset defaults to :math:`\T{0}`, the alignment to the storage size of the respective memory access, which is its *natural alignment*.
Expand Down Expand Up @@ -214,8 +214,8 @@ Lexically, an |Toffset| or |Talign| phrase is considered a single :ref:`keyword
\text{i64.store8}~~m{:}\Tmemarg_1 &\Rightarrow& \I64.\STORE\K{8}~m \\ &&|&
\text{i64.store16}~~m{:}\Tmemarg_2 &\Rightarrow& \I64.\STORE\K{16}~m \\ &&|&
\text{i64.store32}~~m{:}\Tmemarg_4 &\Rightarrow& \I64.\STORE\K{32}~m \\ &&|&
\text{current\_memory} &\Rightarrow& \CURRENTMEMORY \\ &&|&
\text{grow\_memory} &\Rightarrow& \GROWMEMORY \\
\text{memory.size} &\Rightarrow& \MEMORYSIZE \\ &&|&
\text{memory.grow} &\Rightarrow& \MEMORYGROW \\
\end{array}
Expand Down
4 changes: 2 additions & 2 deletions document/core/util/macros.def
Original file line number Diff line number Diff line change
Expand Up @@ -325,8 +325,8 @@

.. |LOAD| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{load}}
.. |STORE| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{store}}
.. |CURRENTMEMORY| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{current\_memory}}
.. |GROWMEMORY| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{grow\_memory}}
.. |MEMORYSIZE| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{memory.size}}
.. |MEMORYGROW| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{memory.grow}}

.. |CONST| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{const}}
.. |EQZ| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{eqz}}
Expand Down
14 changes: 7 additions & 7 deletions document/core/valid/instructions.rst
Original file line number Diff line number Diff line change
Expand Up @@ -389,10 +389,10 @@ Memory Instructions
}
.. _valid-current_memory:
.. _valid-memory.size:

:math:`\CURRENTMEMORY`
......................
:math:`\MEMORYSIZE`
...................

* The memory :math:`C.\CMEMS[0]` must be defined in the context.

Expand All @@ -402,13 +402,13 @@ Memory Instructions
\frac{
C.\CMEMS[0] = \memtype
}{
C \vdashinstr \CURRENTMEMORY : [] \to [\I32]
C \vdashinstr \MEMORYSIZE : [] \to [\I32]
}
.. _valid-grow_memory:
.. _valid-memory.grow:

:math:`\GROWMEMORY`
:math:`\MEMORYGROW`
...................

* The memory :math:`C.\CMEMS[0]` must be defined in the context.
Expand All @@ -419,7 +419,7 @@ Memory Instructions
\frac{
C.\CMEMS[0] = \memtype
}{
C \vdashinstr \GROWMEMORY : [\I32] \to [\I32]
C \vdashinstr \MEMORYGROW : [\I32] \to [\I32]
}
Expand Down
4 changes: 2 additions & 2 deletions interpreter/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -225,8 +225,8 @@ op:
set_global <var>
<val_type>.load((8|16|32)_<sign>)? <offset>? <align>?
<val_type>.store(8|16|32)? <offset>? <align>?
current_memory
grow_memory
memory.size
memory.grow
<val_type>.const <value>
<val_type>.<unop>
<val_type>.<binop>
Expand Down
4 changes: 2 additions & 2 deletions interpreter/binary/decode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -289,10 +289,10 @@ let rec instr s =

| 0x3f ->
expect 0x00 s "zero flag expected";
current_memory
memory_size
| 0x40 ->
expect 0x00 s "zero flag expected";
grow_memory
memory_grow

| 0x41 -> i32_const (at vs32 s)
| 0x42 -> i64_const (at vs64 s)
Expand Down
38 changes: 19 additions & 19 deletions interpreter/binary/encode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -171,27 +171,27 @@ let encode m =
| Load ({ty = I64Type; sz = None; _} as mo) -> op 0x29; memop mo
| Load ({ty = F32Type; sz = None; _} as mo) -> op 0x2a; memop mo
| Load ({ty = F64Type; sz = None; _} as mo) -> op 0x2b; memop mo
| Load ({ty = I32Type; sz = Some (Mem8, SX); _} as mo) ->
| Load ({ty = I32Type; sz = Some (Pack8, SX); _} as mo) ->
op 0x2c; memop mo
| Load ({ty = I32Type; sz = Some (Mem8, ZX); _} as mo) ->
| Load ({ty = I32Type; sz = Some (Pack8, ZX); _} as mo) ->
op 0x2d; memop mo
| Load ({ty = I32Type; sz = Some (Mem16, SX); _} as mo) ->
| Load ({ty = I32Type; sz = Some (Pack16, SX); _} as mo) ->
op 0x2e; memop mo
| Load ({ty = I32Type; sz = Some (Mem16, ZX); _} as mo) ->
| Load ({ty = I32Type; sz = Some (Pack16, ZX); _} as mo) ->
op 0x2f; memop mo
| Load {ty = I32Type; sz = Some (Mem32, _); _} ->
| Load {ty = I32Type; sz = Some (Pack32, _); _} ->
assert false
| Load ({ty = I64Type; sz = Some (Mem8, SX); _} as mo) ->
| Load ({ty = I64Type; sz = Some (Pack8, SX); _} as mo) ->
op 0x30; memop mo
| Load ({ty = I64Type; sz = Some (Mem8, ZX); _} as mo) ->
| Load ({ty = I64Type; sz = Some (Pack8, ZX); _} as mo) ->
op 0x31; memop mo
| Load ({ty = I64Type; sz = Some (Mem16, SX); _} as mo) ->
| Load ({ty = I64Type; sz = Some (Pack16, SX); _} as mo) ->
op 0x32; memop mo
| Load ({ty = I64Type; sz = Some (Mem16, ZX); _} as mo) ->
| Load ({ty = I64Type; sz = Some (Pack16, ZX); _} as mo) ->
op 0x33; memop mo
| Load ({ty = I64Type; sz = Some (Mem32, SX); _} as mo) ->
| Load ({ty = I64Type; sz = Some (Pack32, SX); _} as mo) ->
op 0x34; memop mo
| Load ({ty = I64Type; sz = Some (Mem32, ZX); _} as mo) ->
| Load ({ty = I64Type; sz = Some (Pack32, ZX); _} as mo) ->
op 0x35; memop mo
| Load {ty = F32Type | F64Type; sz = Some _; _} ->
assert false
Expand All @@ -200,16 +200,16 @@ let encode m =
| Store ({ty = I64Type; sz = None; _} as mo) -> op 0x37; memop mo
| Store ({ty = F32Type; sz = None; _} as mo) -> op 0x38; memop mo
| Store ({ty = F64Type; sz = None; _} as mo) -> op 0x39; memop mo
| Store ({ty = I32Type; sz = Some Mem8; _} as mo) -> op 0x3a; memop mo
| Store ({ty = I32Type; sz = Some Mem16; _} as mo) -> op 0x3b; memop mo
| Store {ty = I32Type; sz = Some Mem32; _} -> assert false
| Store ({ty = I64Type; sz = Some Mem8; _} as mo) -> op 0x3c; memop mo
| Store ({ty = I64Type; sz = Some Mem16; _} as mo) -> op 0x3d; memop mo
| Store ({ty = I64Type; sz = Some Mem32; _} as mo) -> op 0x3e; memop mo
| Store ({ty = I32Type; sz = Some Pack8; _} as mo) -> op 0x3a; memop mo
| Store ({ty = I32Type; sz = Some Pack16; _} as mo) -> op 0x3b; memop mo
| Store {ty = I32Type; sz = Some Pack32; _} -> assert false
| Store ({ty = I64Type; sz = Some Pack8; _} as mo) -> op 0x3c; memop mo
| Store ({ty = I64Type; sz = Some Pack16; _} as mo) -> op 0x3d; memop mo
| Store ({ty = I64Type; sz = Some Pack32; _} as mo) -> op 0x3e; memop mo
| Store {ty = F32Type | F64Type; sz = Some _; _} -> assert false

| CurrentMemory -> op 0x3f; u8 0x00
| GrowMemory -> op 0x40; u8 0x00
| MemorySize -> op 0x3f; u8 0x00
| MemoryGrow -> op 0x40; u8 0x00

| Const {it = I32 c; _} -> op 0x41; vs32 c
| Const {it = I64 c; _} -> op 0x42; vs64 c
Expand Down
4 changes: 2 additions & 2 deletions interpreter/exec/eval.ml
Original file line number Diff line number Diff line change
Expand Up @@ -214,11 +214,11 @@ let rec step (c : config) : config =
vs', []
with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]);

| CurrentMemory, vs ->
| MemorySize, vs ->
let mem = memory frame.inst (0l @@ e.at) in
I32 (Memory.size mem) :: vs, []

| GrowMemory, I32 delta :: vs' ->
| MemoryGrow, I32 delta :: vs' ->
let mem = memory frame.inst (0l @@ e.at) in
let old_size = Memory.size mem in
let result =
Expand Down
18 changes: 9 additions & 9 deletions interpreter/runtime/memory.ml
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ type size = int32 (* number of pages *)
type address = int64
type offset = int32

type mem_size = Mem8 | Mem16 | Mem32
type pack_size = Pack8 | Pack16 | Pack32
type extension = SX | ZX

type memory' = (int, int8_unsigned_elt, c_layout) Array1.t
Expand All @@ -22,10 +22,10 @@ exception OutOfMemory

let page_size = 0x10000L (* 64 KiB *)

let mem_size = function
| Mem8 -> 1
| Mem16 -> 2
| Mem32 -> 4
let packed_size = function
| Pack8 -> 1
| Pack16 -> 2
| Pack32 -> 4

let within_limits n = function
| None -> true
Expand Down Expand Up @@ -126,17 +126,17 @@ let extend x n = function
| SX -> let sh = 64 - 8 * n in Int64.(shift_right (shift_left x sh) sh)

let load_packed sz ext mem a o t =
assert (mem_size sz <= Types.size t);
let n = mem_size sz in
assert (packed_size sz <= Types.size t);
let n = packed_size sz in
let x = extend (loadn mem a o n) n ext in
match t with
| I32Type -> I32 (Int64.to_int32 x)
| I64Type -> I64 x
| _ -> raise Type

let store_packed sz mem a o v =
assert (mem_size sz <= Types.size (Values.type_of v));
let n = mem_size sz in
assert (packed_size sz <= Types.size (Values.type_of v));
let n = packed_size sz in
let x =
match v with
| I32 x -> Int64.of_int32 x
Expand Down
8 changes: 4 additions & 4 deletions interpreter/runtime/memory.mli
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ type size = int32 (* number of pages *)
type address = int64
type offset = int32

type mem_size = Mem8 | Mem16 | Mem32
type pack_size = Pack8 | Pack16 | Pack32
type extension = SX | ZX

exception Type
Expand All @@ -18,7 +18,7 @@ exception SizeLimit
exception OutOfMemory

val page_size : int64
val mem_size : mem_size -> int
val packed_size : pack_size -> int

val alloc : memory_type -> memory (* raises SizeOverflow, OutOfMemory *)
val type_of : memory -> memory_type
Expand All @@ -37,8 +37,8 @@ val load_value :
val store_value :
memory -> address -> offset -> value -> unit (* raises Bounds *)
val load_packed :
mem_size -> extension -> memory -> address -> offset -> value_type -> value
pack_size -> extension -> memory -> address -> offset -> value_type -> value
(* raises Type, Bounds *)
val store_packed :
mem_size -> memory -> address -> offset -> value -> unit
pack_size -> memory -> address -> offset -> value -> unit
(* raises Type, Bounds *)
Loading

0 comments on commit b3de271

Please sign in to comment.