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

[spec] First go at specification #3

Merged
merged 8 commits into from
Apr 4, 2018
Merged

[spec] First go at specification #3

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
2bed427
[spec] First go at specification
rossberg Mar 6, 2018
472ff1f
Comments and fixes
rossberg Mar 8, 2018
684e016
Define default values
rossberg Mar 8, 2018
15762fc
Typo
rossberg Mar 13, 2018
71435f4
Comments by Luke
rossberg Mar 15, 2018
29c91d0
Fix br_table
rossberg Mar 15, 2018
3e99426
Tweak
rossberg Mar 23, 2018
b302023
Fix globaltype matching
rossberg Mar 23, 2018
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
19 changes: 15 additions & 4 deletions document/core/appendix/algorithm.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,14 +21,25 @@ The algorithm is expressed in typed pseudo code whose semantics is intended to b
Data Structures
~~~~~~~~~~~~~~~

Types are representable as an enumeration.
A simple subtyping check can be defined on them.

.. code-block:: pseudo

type val_type = I32 | I64 | F32 | F64 | Anyref | Anyfunc | Eqref | Nullref

func is_ref(t : valtype) : bool =
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nit: val_type (function parameter)

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done.

return t = Anyref || t = Anyfunc || t = Eqref

func matches(t1 : val_type, t2 : val_type) : bool =
return t1 = t2 || (t1 = Nullref && is_ref(t2)) || (is_ref(t1) && t2 = Anyref)

The algorithm uses two separate stacks: the *operand stack* and the *control stack*.
The former tracks the :ref:`types <syntax-valtype>` of operand values on the :ref:`stack <stack>`,
the latter surrounding :ref:`structured control instructions <syntax-instr-control>` and their associated :ref:`blocks <syntax-instr-control>`.

.. code-block:: pseudo

type val_type = I32 | I64 | F32 | F64

type opd_stack = stack(val_type | Unknown)

type ctrl_stack = stack(ctrl_frame)
Expand Down Expand Up @@ -70,7 +81,7 @@ However, these variables are not manipulated directly by the main checking funct
let actual = pop_opd()
if (actual = Unknown) return expect
if (expect = Unknown) return actual
error_if(actual =/= expect)
error_if(not matches(actual, expect))
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

IIUC, according to the validation rules, (select (ref.null) (get_table ...) (...)) is supposed to validate, since subtyping is applied to ref.null when validating select with t = anyref. To implement this, I think select now needs special treatment below; I expect taking a meet of the two pop_opd()s.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, good catch! This is not just for nullref, subtyping generally changes the way select needs to be handled. To simplify things, I refactored the pseudo code somewhat to make Unknown act more like a bottom type (which has been your view all along, I think :) ).

While fixing this I realised that subtyping also affects how br_table needs to be handled, so I incorporated respective changes as well.

return actual

func push_opds(types : list(val_type)) = foreach (t in types) push_opd(t)
Expand All @@ -84,7 +95,7 @@ That can occur after an unconditional branch, when the stack is typed :ref:`poly
In that case, an unknown type is returned.

A second function for popping an operand takes an expected type, which the actual operand type is checked against.
The types may differ in case one of them is Unknown.
The types may differ by subtyping or in case one of them is Unknown.
The more specific type is returned.

Finally, there are accumulative functions for pushing or popping multiple operand types.
Expand Down
25 changes: 22 additions & 3 deletions document/core/appendix/index-instructions.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ Instruction Binary Opcode Type
:math:`\BRTABLE~l^\ast~l` :math:`\hex{0E}` :math:`[t_1^\ast~t^?~\I32] \to [t_2^\ast]` :ref:`validation <valid-br_table>` :ref:`execution <exec-br_table>`
:math:`\RETURN` :math:`\hex{0F}` :math:`[t_1^\ast~t^?] \to [t_2^\ast]` :ref:`validation <valid-return>` :ref:`execution <exec-return>`
:math:`\CALL~x` :math:`\hex{10}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation <valid-call>` :ref:`execution <exec-call>`
:math:`\CALLINDIRECT~x` :math:`\hex{11}` :math:`[t_1^\ast~\I32] \to [t_2^\ast]` :ref:`validation <valid-call_indirect>` :ref:`execution <exec-call_indirect>`
:math:`\CALLINDIRECT~x~y` :math:`\hex{11}` :math:`[t_1^\ast~\I32] \to [t_2^\ast]` :ref:`validation <valid-call_indirect>` :ref:`execution <exec-call_indirect>`
(reserved) :math:`\hex{12}`
(reserved) :math:`\hex{13}`
(reserved) :math:`\hex{14}`
Expand All @@ -44,8 +44,8 @@ Instruction Binary Opcode Type
:math:`\TEELOCAL~x` :math:`\hex{22}` :math:`[t] \to [t]` :ref:`validation <valid-tee_local>` :ref:`execution <exec-tee_local>`
:math:`\GETGLOBAL~x` :math:`\hex{23}` :math:`[] \to [t]` :ref:`validation <valid-get_global>` :ref:`execution <exec-get_global>`
:math:`\SETGLOBAL~x` :math:`\hex{24}` :math:`[t] \to []` :ref:`validation <valid-set_global>` :ref:`execution <exec-set_global>`
(reserved) :math:`\hex{25}`
(reserved) :math:`\hex{26}`
:math:`\GETTABLE~x` :math:`\hex{25}` :math:`[\I32] \to [t]` :ref:`validation <valid-get_table>` :ref:`execution <exec-get_table>`
:math:`\SETTABLE~x` :math:`\hex{26}` :math:`[\I32~t] \to []` :ref:`validation <valid-set_table>` :ref:`execution <exec-set_table>`
(reserved) :math:`\hex{27}`
:math:`\I32.\LOAD~\memarg` :math:`\hex{28}` :math:`[\I32] \to [\I32]` :ref:`validation <valid-load>` :ref:`execution <exec-load>`
:math:`\I64.\LOAD~\memarg` :math:`\hex{29}` :math:`[\I32] \to [\I64]` :ref:`validation <valid-load>` :ref:`execution <exec-load>`
Expand Down Expand Up @@ -199,5 +199,24 @@ Instruction Binary Opcode Type
:math:`\I64.\REINTERPRET\K{/}\F64` :math:`\hex{BD}` :math:`[\F64] \to [\I64]` :ref:`validation <valid-cvtop>` :ref:`execution <exec-cvtop>`, :ref:`operator <op-reinterpret>`
:math:`\F32.\REINTERPRET\K{/}\I32` :math:`\hex{BE}` :math:`[\I32] \to [\F32]` :ref:`validation <valid-cvtop>` :ref:`execution <exec-cvtop>`, :ref:`operator <op-reinterpret>`
:math:`\F64.\REINTERPRET\K{/}\I64` :math:`\hex{BF}` :math:`[\I64] \to [\F64]` :ref:`validation <valid-cvtop>` :ref:`execution <exec-cvtop>`, :ref:`operator <op-reinterpret>`
(reserved) :math:`\hex{C0}`
(reserved) :math:`\hex{C1}`
(reserved) :math:`\hex{C2}`
(reserved) :math:`\hex{C3}`
(reserved) :math:`\hex{C4}`
(reserved) :math:`\hex{C5}`
(reserved) :math:`\hex{C6}`
(reserved) :math:`\hex{C7}`
(reserved) :math:`\hex{C8}`
(reserved) :math:`\hex{C9}`
(reserved) :math:`\hex{CA}`
(reserved) :math:`\hex{CB}`
(reserved) :math:`\hex{CC}`
(reserved) :math:`\hex{CD}`
(reserved) :math:`\hex{CE}`
(reserved) :math:`\hex{CF}`
:math:`\REFNULL` :math:`\hex{D0}` :math:`[] \to [\NULLREF]` :ref:`validation <valid-ref_null>` :ref:`execution <exec-ref_null>`
:math:`\REFISNULL` :math:`\hex{D1}` :math:`[\ANYREF] \to [\I32]` :ref:`validation <valid-ref_isnull>` :ref:`execution <exec-ref_isnull>`
:math:`\REFEQ` :math:`\hex{D2}` :math:`[\EQREF~\EQREF] \to [\I32]` :ref:`validation <valid-ref_eq>` :ref:`execution <exec-ref_eq>`
=================================== ================ ========================================== ======================================== ===============================================================

7 changes: 4 additions & 3 deletions document/core/appendix/index-rules.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,14 +71,15 @@ Construct Judgement
=============================================== ===============================================================================


Import Matching
~~~~~~~~~~~~~~~
Matching
~~~~~~~~

=============================================== ===============================================================================
Construct Judgement
=============================================== ===============================================================================
:ref:`Limits <match-limits>` :math:`\vdashlimitsmatch \limits_1 \matches \limits_2`
:ref:`Value type <match-valtype>` :math:`\vdashvaltypematch \valtype_1 \matches \valtype_2`
:ref:`External type <match-externtype>` :math:`\vdashexterntypematch \externtype_1 \matches \externtype_2`
:ref:`Limits <match-limits>` :math:`\vdashlimitsmatch \limits_1 \matches \limits_2`
=============================================== ===============================================================================


Expand Down
18 changes: 10 additions & 8 deletions document/core/appendix/index-types.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,17 +8,19 @@ Index of Types
Category Constructor Binary Opcode
======================================== =========================================== ===============================================================================
:ref:`Type index <syntax-typeidx>` :math:`x` (positive number as |Bs32| or |Bu32|)
:ref:`Value type <syntax-valtype>` |I32| :math:`\hex{7F}` (-1 as |Bs7|)
:ref:`Value type <syntax-valtype>` |I64| :math:`\hex{7E}` (-2 as |Bs7|)
:ref:`Value type <syntax-valtype>` |F32| :math:`\hex{7D}` (-3 as |Bs7|)
:ref:`Value type <syntax-valtype>` |F64| :math:`\hex{7C}` (-4 as |Bs7|)
(reserved) :math:`\hex{7C}` .. :math:`\hex{71}`
:ref:`Element type <syntax-elemtype>` |ANYFUNC| :math:`\hex{70}` (-16 as |Bs7|)
(reserved) :math:`\hex{6F}` .. :math:`\hex{61}`
:ref:`Number type <syntax-numtype>` |I32| :math:`\hex{7F}` (-1 as |Bs7|)
:ref:`Number type <syntax-numtype>` |I64| :math:`\hex{7E}` (-2 as |Bs7|)
:ref:`Number type <syntax-numtype>` |F32| :math:`\hex{7D}` (-3 as |Bs7|)
:ref:`Number type <syntax-numtype>` |F64| :math:`\hex{7C}` (-4 as |Bs7|)
(reserved) :math:`\hex{7B}` .. :math:`\hex{71}`
:ref:`Reference type <syntax-reftype>` |ANYFUNC| :math:`\hex{70}` (-16 as |Bs7|)
:ref:`Reference type <syntax-reftype>` |ANYREF| :math:`\hex{6F}` (-17 as |Bs7|)
:ref:`Reference type <syntax-reftype>` |EQREF| :math:`\hex{6E}` (-18 as |Bs7|)
(reserved) :math:`\hex{6D}` .. :math:`\hex{61}`
:ref:`Function type <syntax-functype>` :math:`[\valtype^\ast] \to [\valtype^\ast]` :math:`\hex{60}` (-32 as |Bs7|)
(reserved) :math:`\hex{5F}` .. :math:`\hex{41}`
:ref:`Result type <syntax-resulttype>` :math:`\epsilon` :math:`\hex{40}` (-64 as |Bs7|)
:ref:`Table type <syntax-tabletype>` :math:`\limits~\elemtype` (none)
:ref:`Table type <syntax-tabletype>` :math:`\limits~\reftype` (none)
:ref:`Memory type <syntax-memtype>` :math:`\limits` (none)
:ref:`Global type <syntax-globaltype>` :math:`\mut~\valtype` (none)
======================================== =========================================== ===============================================================================
53 changes: 49 additions & 4 deletions document/core/binary/instructions.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,17 +54,39 @@ Control Instructions
&\Rightarrow& \BRTABLE~l^\ast~l_N \\ &&|&
\hex{0F} &\Rightarrow& \RETURN \\ &&|&
\hex{10}~~x{:}\Bfuncidx &\Rightarrow& \CALL~x \\ &&|&
\hex{11}~~x{:}\Btypeidx~~\hex{00} &\Rightarrow& \CALLINDIRECT~x \\
\hex{11}~~y{:}\Btypeidx~~x{:}\Btableidx &\Rightarrow& \CALLINDIRECT~x~y \\
\end{array}

.. note::
The |ELSE| opcode :math:`\hex{05}` in the encoding of an |IF| instruction can be omitted if the following instruction sequence is empty.


.. index:: reference instruction
pair: binary format; instruction
.. _binary-instr-ref:

Reference Instructions
~~~~~~~~~~~~~~~~~~~~~~

:ref:`Reference instructions <syntax-instr-ref>` are represented by single byte codes.

.. _binary-ref_null:
.. _binary-ref_isnull:
.. _binary-ref_eq:

.. math::
\begin{array}{llclll}
\production{instruction} & \Binstr &::=& \dots \\ &&|&
\hex{D0} &\Rightarrow& \REFNULL \\ &&|&
\hex{D1} &\Rightarrow& \REFISNULL \\ &&|&
\hex{D2} &\Rightarrow& \REFEQ \\
\end{array}

.. note::
In future versions of WebAssembly, the zero byte occurring in the encoding
of the |CALLINDIRECT| instruction may be used to index additional tables.
These opcode assignments are preliminary.


.. index:: value type, polymorphism
.. index:: parametric instruction, value type, polymorphism
pair: binary format; instruction
.. _binary-instr-parametric:

Expand Down Expand Up @@ -110,6 +132,29 @@ Variable Instructions
\end{array}


.. index:: table instruction, table index
pair: binary format; instruction
.. _binary-instr-table:

Table Instructions
~~~~~~~~~~~~~~~~~~

:ref:`Table instructions <syntax-instr-table>` are represented by single byte codes.

.. _binary-get_table:
.. _binary-set_table:

.. math::
\begin{array}{llclll}
\production{instruction} & \Binstr &::=& \dots \\ &&|&
\hex{25}~~x{:}\Btableidx &\Rightarrow& \GETTABLE~x \\ &&|&
\hex{26}~~x{:}\Btableidx &\Rightarrow& \SETTABLE~x \\
\end{array}

.. note::
These opcode assignments are preliminary.


.. index:: memory instruction, memory index
pair: binary format; instruction
.. _binary-instr-memory:
Expand Down
66 changes: 49 additions & 17 deletions document/core/binary/types.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,27 +5,63 @@
Types
-----

.. index:: value type
pair: binary format; value type
.. _binary-valtype:
.. note::
In future versions of WebAssembly, value types may include types denoted by :ref:`type indices <syntax-typeidx>`.
Thus, the binary format for types corresponds to the encodings of small negative :math:`\xref{binary/values}{binary-sint}{\sN}` values, so that they can coexist with (positive) type indices in the future.

Value Types
~~~~~~~~~~~

:ref:`Value types <syntax-valtype>` are encoded by a single byte.
.. index:: number type
pair: binary format; number type
.. _binary-numtype:

Number Types
~~~~~~~~~~~~

:ref:`Number types <syntax-numtype>` are encoded by a single byte.

.. math::
\begin{array}{llclll@{\qquad\qquad}l}
\production{value type} & \Bvaltype &::=&
\production{number type} & \Bnumtype &::=&
\hex{7F} &\Rightarrow& \I32 \\ &&|&
\hex{7E} &\Rightarrow& \I64 \\ &&|&
\hex{7D} &\Rightarrow& \F32 \\ &&|&
\hex{7C} &\Rightarrow& \F64 \\
\end{array}

.. note::
In future versions of WebAssembly, value types may include types denoted by :ref:`type indices <syntax-typeidx>`.
Thus, the binary format for types corresponds to the encodings of small negative :math:`\xref{binary/values}{binary-sint}{\sN}` values, so that they can coexist with (positive) type indices in the future.

.. index:: reference type
pair: binary format; reference type
.. _binary-reftype:

Reference Types
~~~~~~~~~~~~~~~

:ref:`Reference types <syntax-reftype>` are also encoded by a single byte.

.. math::
\begin{array}{llclll@{\qquad\qquad}l}
\production{reference type} & \Breftype &::=&
\hex{70} &\Rightarrow& \ANYFUNC \\ &&|&
\hex{6F} &\Rightarrow& \ANYREF \\ &&|&
\hex{6E} &\Rightarrow& \EQREF \\
\end{array}


.. index:: value type, number type, reference type
pair: binary format; value type
.. _binary-valtype:

Value Types
~~~~~~~~~~~

:ref:`Value types <syntax-valtype>` are encoded with their respective encoding as a :ref:`number type <binary-numtype>` or :ref:`reference type <binary-reftype>`.

.. math::
\begin{array}{llclll@{\qquad\qquad}l}
\production{value type} & \Bvaltype &::=&
t{:}\Bnumtype &\Rightarrow& t \\ &&|&
t{:}\Breftype &\Rightarrow& t \\
\end{array}


.. index:: result type, value type
Expand Down Expand Up @@ -99,23 +135,19 @@ Memory Types
\end{array}


.. index:: table type, element type, limits
.. index:: table type, reference type, limits
pair: binary format; table type
pair: binary format; element type
.. _binary-elemtype:
.. _binary-tabletype:

Table Types
~~~~~~~~~~~

:ref:`Table types <syntax-tabletype>` are encoded with their :ref:`limits <binary-limits>` and a constant byte indicating their :ref:`element type <syntax-elemtype>`.
:ref:`Table types <syntax-tabletype>` are encoded with their :ref:`limits <binary-limits>` and the encoding of their element :ref:`reference type <syntax-reftype>`.

.. math::
\begin{array}{llclll}
\production{table type} & \Btabletype &::=&
\X{et}{:}\Belemtype~~\X{lim}{:}\Blimits &\Rightarrow& \X{lim}~\X{et} \\
\production{element type} & \Belemtype &::=&
\hex{70} &\Rightarrow& \ANYFUNC \\
\X{et}{:}\Breftype~~\X{lim}{:}\Blimits &\Rightarrow& \X{lim}~\X{et} \\
\end{array}


Expand Down
Loading