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

Commit

Permalink
[spec] First go at specification (#3)
Browse files Browse the repository at this point in the history
  • Loading branch information
@rossberg
rossberg authored Apr 4, 2018
1 parent 1d7785d commit 1f29a8e
Show file tree
Hide file tree
Showing 19 changed files with 967 additions and 206 deletions.
71 changes: 54 additions & 17 deletions document/core/appendix/algorithm.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,15 +21,49 @@ The algorithm is expressed in typed pseudo code whose semantics is intended to b
Data Structures
~~~~~~~~~~~~~~~

Types are representable as an enumeration.
In addition to the plain types from the WebAssembly validation semantics, an extended notion of operand type includes a bottom type `Unknown` that is used as the type of :ref:`polymorphic <polymorphism>` operands.

A simple subtyping check can be defined on these types.
In addition, corresponding functions computing the join (least upper bound) and meet (greatest lower bound) of two types are used.
Because there is no top type, a join does not exist in all cases.
Similarly, a meet must always be defined on known value types that exclude the auxiliary bottom type `Unknown`,
hence a meet does not exist in all cases either.
A type error is encountered if a join or meet is required when it does not exist.

.. code-block:: pseudo
type val_type = I32 | I64 | F32 | F64 | Anyref | Anyfunc | Anyeqref | Nullref
type opd_type = val_type | Unknown
func is_ref(t : opd_type) : bool =
return t = Anyref || t = Anyfunc || t = Anyeqref || t = Nullref
func matches(t1 : opd_type, t2 : opd_type) : bool =
return t1 = t2 || t1 = Unknown ||
(t1 = Nullref && is_ref(t2)) || (is_ref(t1) && t2 = Anyref)
func join(t1 : opd_type, t2 : opd_type) : opd_type =
if (t1 = t2) return t1
if (matches(t1, t2)) return t2
if (matches(t2, t1)) return t1
error_if(not (is_ref(t1) && is_ref(t2)))
return Anyref
func meet(t1 : val_type, t2 : val_type) : val_type =
if (t1 = t2) return t1
if (matches(t1, t2)) return t1
if (matches(t2, t1)) return t2
error_if(not (is_ref(t1) && is_ref(t2)))
return Nullref
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 opd_stack = stack(opd_type)
type ctrl_stack = stack(ctrl_frame)
type ctrl_frame = {
Expand Down Expand Up @@ -58,20 +92,17 @@ However, these variables are not manipulated directly by the main checking funct

.. code-block:: pseudo
func push_opd(type : val_type | Unknown) =
func push_opd(type : opd_type) =
opds.push(type)
func pop_opd() : val_type | Unknown =
func pop_opd() : opd_type =
if (opds.size() = ctrls[0].height && ctrls[0].unreachable) return Unknown
error_if(opds.size() = ctrls[0].height)
return opds.pop()
func pop_opd(expect : val_type | Unknown) : val_type | Unknown =
func pop_opd(expect : val_type) =
let actual = pop_opd()
if (actual = Unknown) return expect
if (expect = Unknown) return actual
error_if(actual =/= expect)
return actual
error_if(not matches(actual, expect))
func push_opds(types : list(val_type)) = foreach (t in types) push_opd(t)
func pop_opds(types : list(val_type)) = foreach (t in reverse(types)) pop_opd(t)
Expand All @@ -83,9 +114,8 @@ But first, a special case is handled where the block contains no known operands,
That can occur after an unconditional branch, when the stack is typed :ref:`polymorphically <polymorphism>`.
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 more specific type is returned.
A second function for popping an operand takes an expected (known) type, which the actual operand type is checked against.
The types may differ by subtyping, inlcuding the case where the actual type is unknown.

Finally, there are accumulative functions for pushing or popping multiple operand types.

Expand Down Expand Up @@ -150,14 +180,19 @@ Other instructions are checked in a similar manner.
pop_opd(I32)
push_opd(I32)
case (ref.eq)
pop_opd(Anyeqref)
pop_opd(Anyeqref)
push_opd(I32)
case (drop)
pop_opd()
case (select)
pop_opd(I32)
let t1 = pop_opd()
let t2 = pop_opd(t1)
push_opd(t2)
let t2 = pop_opd()
push_opd(join(t1, t2))
   case (unreachable)
      unreachable()
Expand Down Expand Up @@ -193,10 +228,12 @@ Other instructions are checked in a similar manner.
   case (br_table n* m)
      error_if(ctrls.size() < m)
var ts = ctrls[m].label_types
      foreach (n in n*)
        error_if(ctrls.size() < n || ctrls[n].label_types =/= ctrls[m].label_types)
        error_if(ctrls.size() < n)
ts := meet(ts, ctrls[n].label_types)
pop_opd(I32)
      pop_opds(ctrls[m].label_types)
      pop_opds(ts)
      unreachable()
.. note::
Expand Down
25 changes: 22 additions & 3 deletions document/core/appendix/index-instructions.rst
View file
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:`[\ANYEQREF~\ANYEQREF] \to [\I32]` :ref:`validation <valid-ref_eq>` :ref:`execution <exec-ref_eq>`
=================================== ================ ========================================== ======================================== ===============================================================

9 changes: 5 additions & 4 deletions document/core/appendix/index-rules.rst
View file
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:`External type <match-externtype>` :math:`\vdashexterntypematch \externtype_1 \matches \externtype_2`
:ref:`Value type <match-valtype>` :math:`\vdashvaltypematch \valtype_1 \matchesvaltype \valtype_2`
:ref:`External type <match-externtype>` :math:`\vdashexterntypematch \externtype_1 \matchesexterntype \externtype_2`
:ref:`Limits <match-limits>` :math:`\vdashlimitsmatch \limits_1 \matcheslimits \limits_2`
=============================================== ===============================================================================


Expand Down
18 changes: 10 additions & 8 deletions document/core/appendix/index-types.rst
View file
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>` |ANYEQREF| :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
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
Loading

0 comments on commit 1f29a8e

Please sign in to comment.