Skip to content

Commit

Permalink
[spec] Correctly account for subtyping in global/table instances (Web…
Browse files Browse the repository at this point in the history 
…Assembly#39)

* Make types explicit in global/table/memory instances
* Allow global/table values/elements to be subtypes
* Simplify externval typing
  • Loading branch information
@rossberg
rossberg authored Apr 23, 2019
1 parent 05672b0 commit 09dccac
Show file tree
Hide file tree
Showing 6 changed files with 144 additions and 113 deletions.
42 changes: 18 additions & 24 deletions document/core/appendix/embedding.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -280,15 +280,13 @@ Functions
:math:`\F{func\_type}(\store, \funcaddr) : \functype`
.....................................................

1. Assert: the :ref:`external value <syntax-externval>` :math:`\EVFUNC~\funcaddr` is :ref:`valid <valid-externval>` with :ref:`external type <syntax-externtype>` :math:`\ETFUNC~\functype`.
1. Return :math:`S.\SFUNCS[a].\FITYPE`.

2. Return :math:`\functype`.

3. Post-condition: :math:`\functype` is :ref:`valid <valid-functype>`.
2. Post-condition: the returned :ref:`function type <syntax-functype>` is :ref:`valid <valid-functype>`.

.. math::
\begin{array}{lclll}
\F{func\_type}(S, a) &=& \X{ft} && (\iff S \vdashexternval \EVFUNC~a : \ETFUNC~\X{ft}) \\
\F{func\_type}(S, a) &=& S.\SFUNCS[a].\FITYPE \\
\end{array}
Expand Down Expand Up @@ -345,15 +343,13 @@ Tables
:math:`\F{table\_type}(\store, \tableaddr) : \tabletype`
........................................................

1. Assert: the :ref:`external value <syntax-externval>` :math:`\EVTABLE~\tableaddr` is :ref:`valid <valid-externval>` with :ref:`external type <syntax-externtype>` :math:`\ETTABLE~\tabletype`.

2. Return :math:`\tabletype`.
1. Return :math:`S.\STABLES[a].\TITYPE`.

3. Post-condition: :math:`\tabletype` is :math:`valid <valid-tabletype>`.
2. Post-condition: the returned :ref:`table type <syntax-tabletype>` is :math:`valid <valid-tabletype>`.

.. math::
\begin{array}{lclll}
\F{table\_type}(S, a) &=& \X{tt} && (\iff S \vdashexternval \EVTABLE~a : \ETTABLE~\X{tt}) \\
\F{table\_type}(S, a) &=& S.\STABLES[a].\TITYPE \\
\end{array}
Expand Down Expand Up @@ -459,15 +455,13 @@ Memories
:math:`\F{mem\_type}(\store, \memaddr) : \memtype`
..................................................

1. Assert: the :ref:`external value <syntax-externval>` :math:`\EVMEM~\memaddr` is :ref:`valid <valid-externval>` with :ref:`external type <syntax-externtype>` :math:`\ETMEM~\memtype`.

2. Return :math:`\memtype`.
1. Return :math:`S.\SMEMS[a].\MITYPE`.

3. Post-condition: :math:`\memtype` is :math:`valid <valid-memtype>`.
2. Post-condition: the returned :ref:`memory type <syntax-memtype>` is :math:`valid <valid-memtype>`.

.. math::
\begin{array}{lclll}
\F{mem\_type}(S, a) &=& \X{mt} && (\iff S \vdashexternval \EVMEM~a : \ETMEM~\X{mt}) \\
\F{mem\_type}(S, a) &=& S.\SMEMS[a].\MITYPE \\
\end{array}
Expand Down Expand Up @@ -574,15 +568,13 @@ Globals
:math:`\F{global\_type}(\store, \globaladdr) : \globaltype`
...........................................................

1. Assert: the :ref:`external value <syntax-externval>` :math:`\EVGLOBAL~\globaladdr` is :ref:`valid <valid-externval>` with :ref:`external type <syntax-externtype>` :math:`\ETGLOBAL~\globaltype`.
1. Return :math:`S.\SGLOBALS[a].\GITYPE`.

2. Return :math:`\globaltype`.

3. Post-condition: :math:`\globaltype` is :math:`valid <valid-globaltype>`.
2. Post-condition: the returned :ref:`global type <syntax-globaltype>` is :math:`valid <valid-globaltype>`.

.. math::
\begin{array}{lclll}
\F{global\_type}(S, a) &=& \X{gt} && (\iff S \vdashexternval \EVGLOBAL~a : \ETGLOBAL~\X{gt}) \\
\F{global\_type}(S, a) &=& S.\SGLOBALS[a].\GITYPE \\
\end{array}
Expand All @@ -608,15 +600,17 @@ Globals

1. Let :math:`\X{gi}` be the :ref:`global instance <syntax-globalinst>` :math:`\store.\SGLOBALS[\globaladdr]`.

2. If :math:`\X{gi}.\GIMUT` is not :math:`\MVAR`, then return :math:`\ERROR`.
2. Let :math:`\mut~t` be the structure of the :ref:`global type <syntax-globaltype>` :math:`\X{gi}.\GITYPE`.

3. Replace :math:`\X{gi}.\GIVALUE` with the :ref:`value <syntax-val>` :math:`\val`.
3. If :math:`\mut` is not :math:`\MVAR`, then return :math:`\ERROR`.

4. Return the updated store.
4. Replace :math:`\X{gi}.\GIVALUE` with the :ref:`value <syntax-val>` :math:`\val`.

5. Return the updated store.

.. math::
~ \\
\begin{array}{lclll}
\F{global\_write}(S, a, v) &=& S' && (\iff S.\SGLOBALS[a].\GIMUT = \MVAR \wedge S' = S \with \SGLOBALS[a].\GIVALUE = v) \\
\F{global\_write}(S, a, v) &=& S' && (\iff S.\SGLOBALS[a].\GITYPE = \MVAR~t \wedge S' = S \with \SGLOBALS[a].\GIVALUE = v) \\
\F{global\_write}(S, a, v) &=& \ERROR && (\otherwise) \\
\end{array}
3 changes: 3 additions & 0 deletions document/core/appendix/index-rules.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,10 @@ Matching
=============================================== ===============================================================================
Construct Judgement
=============================================== ===============================================================================
:ref:`Number type <match-numtype>` :math:`\vdashnumtypematch \numtype_1 \matchesvaltype \numtype_2`
:ref:`Reference type <match-reftype>` :math:`\vdashreftypematch \reftype_1 \matchesvaltype \reftype_2`
:ref:`Value type <match-valtype>` :math:`\vdashvaltypematch \valtype_1 \matchesvaltype \valtype_2`
:ref:`Result type <match-resulttype>` :math:`\vdashresulttypematch [t_1^?] \matchesresulttype [t_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
85 changes: 53 additions & 32 deletions document/core/appendix/properties.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -196,59 +196,80 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
.. index:: table type, table instance, limits, function address
.. _valid-tableinst:

:ref:`Table Instances <syntax-tableinst>` :math:`\{ \TIELEM~(\X{fa}^?)^n, \TIMAX~m^? \}`
..............................................................................................
:ref:`Table Instances <syntax-tableinst>` :math:`\{ \TITYPE~(\limits~t), \TIELEM~\reff^\ast \}`
...............................................................................................

* For each optional :ref:`function address <syntax-funcaddr>` :math:`\X{fa}^?_i` in the table elements :math:`(\X{fa}^?)^n`:
* The :ref:`table type <syntax-tabletype>` :math:`\limits~t` must be :ref:`valid <valid-tabletype>`.

* Either :math:`\X{fa}^?_i` is empty.
* The length of :math:`\reff^\ast` must equal :math:`\limits.\LMIN`.

* Or the :ref:`external value <syntax-externval>` :math:`\EVFUNC~\X{fa}` must be :ref:`valid <valid-externval-func>` with some :ref:`external type <syntax-externtype>` :math:`\ETFUNC~\X{ft}`.
* For each :ref:`reference <syntax-ref>` :math:`\reff_i` in the table elements :math:`\reff^n`:

* The :ref:`limits <syntax-limits>` :math:`\{\LMIN~n, \LMAX~m^?\}` must be :ref:`valid <valid-limits>`.
* The :ref:`reference <syntax-ref>` :math:`\reff_i` must be :ref:`valid <valid-ref>` with some :ref:`reference type <syntax-reftype>` :math:`t'_i`.

* Then the table instance is valid with :ref:`table type <syntax-tabletype>` :math:`\{\LMIN~n, \LMAX~m^?\}~\FUNCREF`.
* The :ref:`reference type <syntax-reftype>` :math:`t'_i` must :ref:`match <match-reftype>` the :ref:`reference type <syntax-reftype>` :math:`t`.

* Then the table instance is valid with :ref:`table type <syntax-tabletype>` :math:`\limits~t`.

.. math::
\frac{
((S \vdash \EVFUNC~\X{fa} : \ETFUNC~\functype)^?)^n
\vdashtabletype \limits~t \ok
\qquad
n = \limits.\LMIN
\qquad
\vdashlimits \{\LMIN~n, \LMAX~m^?\} \ok
(S \vdash \reff : t')^n
\qquad
(\vdashreftypematch t' \matchesvaltype t)^n
}{
S \vdashtableinst \{ \TIELEM~(\X{fa}^?)^n, \TIMAX~m^? \} : \{\LMIN~n, \LMAX~m^?\}~\FUNCREF
S \vdashtableinst \{ \TITYPE~(\limits~t), \TIELEM~\reff^n \} : \limits~t
}
.. index:: memory type, memory instance, limits, byte
.. _valid-meminst:

:ref:`Memory Instances <syntax-meminst>` :math:`\{ \MIDATA~b^n, \MIMAX~m^? \}`
..............................................................................
:ref:`Memory Instances <syntax-meminst>` :math:`\{ \MITYPE~\limits, \MIDATA~b^\ast \}`
......................................................................................

* The :ref:`memory type <syntax-memtype>` :math:`\{\LMIN~n, \LMAX~m^?\}` must be :ref:`valid <valid-memtype>`.

* The :ref:`limits <syntax-limits>` :math:`\{\LMIN~n, \LMAX~m^?\}` must be :ref:`valid <valid-limits>`.
* The length of :math:`b^\ast` must equal :math:`\limits.\LMIN` multiplied by the :ref:`page size <page-size>` :math:`64\,\F{Ki}`.

* Then the memory instance is valid with :ref:`memory type <syntax-memtype>` :math:`\{\LMIN~n, \LMAX~m^?\}`.
* Then the memory instance is valid with :ref:`memory type <syntax-memtype>` :math:`\limits`.

.. math::
\frac{
\vdashlimits \{\LMIN~n, \LMAX~m^?\} \ok
\vdashmemtype \limits \ok
\qquad
n = \limits.\LMIN \cdot 64\,\F{Ki}
}{
S \vdashmeminst \{ \MIDATA~b^n, \MIMAX~m^? \} : \{\LMIN~n, \LMAX~m^?\}
S \vdashmeminst \{ \MITYPE~\limits, \MIDATA~b^n \} : \limits
}
.. index:: global type, global instance, value, mutability
.. _valid-globalinst:

:ref:`Global Instances <syntax-globalinst>` :math:`\{ \GIVALUE~(t.\CONST~c), \GIMUT~\mut \}`
............................................................................................
:ref:`Global Instances <syntax-globalinst>` :math:`\{ \GITYPE~(\mut~t), \GIVALUE~\val \}`
.........................................................................................

* The :ref:`global type <syntax-globaltype>` :math:`\mut~t` must be :ref:`valid <valid-globaltype>`.

* The :ref:`value <syntax-val>` :math:`\val` must be :ref:`valid <valid-val>` with some :ref:`value type <syntax-valtype>` :math:`t'`.

* The global instance is valid with :ref:`global type <syntax-globaltype>` :math:`\mut~t`.
* The :ref:`value type <syntax-valtype>` :math:`t'` must :ref:`match <match-valtype>` the :ref:`value type <syntax-valtype>` :math:`t`.

* Then the global instance is valid with :ref:`global type <syntax-globaltype>` :math:`\mut~t`.

.. math::
\frac{
\vdashglobaltype \mut~t \ok
\qquad
S \vdashval \val : t'
\qquad
\vdashvaltypematch t' \matchesvaltype t
}{
S \vdashglobalinst \{ \GIVALUE~(t.\CONST~c), \GIMUT~\mut \} : \mut~t
S \vdashglobalinst \{ \GITYPE~(\mut~t), \GIVALUE~\val \} : \mut~t
}
Expand Down Expand Up @@ -508,7 +529,7 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
:math:`\INITELEM~\tableaddr~o~x^n`
..................................

* The :ref:`external table value <syntax-externval>` :math:`\EVTABLE~\tableaddr` must be :ref:`valid <valid-externval-table>` with some :ref:`external table type <syntax-externtype>` :math:`\ETTABLE~\limits~\FUNCREF`.
* The :ref:`external table value <syntax-externval>` :math:`\EVTABLE~\tableaddr` must be :ref:`valid <valid-externval-table>` with some :ref:`external table type <syntax-externtype>` :math:`\ETTABLE~(\limits~\FUNCREF)`.

* The index :math:`o + n` must be smaller than or equal to :math:`\limits.\LMIN`.

Expand Down Expand Up @@ -676,15 +697,15 @@ a store state :math:`S'` extends state :math:`S`, written :math:`S \extendsto S'
:ref:`Table Instance <syntax-tableinst>` :math:`\tableinst`
...........................................................

* The length of :math:`\tableinst.\TIELEM` must not shrink.
* The :ref:`table type <syntax-tabletype>` :math:`\tableinst.\TITYPE` must remain unchanged.

* The value of :math:`\tableinst.\TIMAX` must remain unchanged.
* The length of :math:`\tableinst.\TIELEM` must not shrink.

.. math::
\frac{
n_1 \leq n_2
}{
\vdashtableinstextends \{\TIELEM~(\X{fa}_1^?)^{n_1}, \TIMAX~m\} \extendsto \{\TIELEM~(\X{fa}_2^?)^{n_2}, \TIMAX~m\}
\vdashtableinstextends \{\TITYPE~\X{tt}, \TIELEM~(\X{fa}_1^?)^{n_1}\} \extendsto \{\TITYPE~\X{tt}, \TIELEM~(\X{fa}_2^?)^{n_2}\}
}
Expand All @@ -694,15 +715,15 @@ a store state :math:`S'` extends state :math:`S`, written :math:`S \extendsto S'
:ref:`Memory Instance <syntax-meminst>` :math:`\meminst`
........................................................

* The length of :math:`\meminst.\MIDATA` must not shrink.
* The :ref:`memory type <syntax-memtype>` :math:`\meminst.\MITYPE` must remain unchanged.

* The value of :math:`\meminst.\MIMAX` must remain unchanged.
* The length of :math:`\meminst.\MIDATA` must not shrink.

.. math::
\frac{
n_1 \leq n_2
}{
\vdashmeminstextends \{\MIDATA~b_1^{n_1}, \MIMAX~m\} \extendsto \{\MIDATA~b_2^{n_2}, \MIMAX~m\}
\vdashmeminstextends \{\MITYPE~\X{mt}, \MIDATA~b_1^{n_1}\} \extendsto \{\MITYPE~\X{mt}, \MIDATA~b_2^{n_2}\}
}
Expand All @@ -712,17 +733,17 @@ a store state :math:`S'` extends state :math:`S`, written :math:`S \extendsto S'
:ref:`Global Instance <syntax-globalinst>` :math:`\globalinst`
..............................................................

* The :ref:`mutability <syntax-mut>` :math:`\globalinst.\GIMUT` must remain unchanged.
* The :ref:`global type <syntax-globaltype>` :math:`\globalinst.\GITYPE` must remain unchanged.

* The :ref:`value type <syntax-valtype>` of the :ref:`value <syntax-val>` :math:`\globalinst.\GIVALUE` must remain unchanged.
* Let :math:`\mut~t` be the structure of :math:`\globalinst.\GITYPE`.

* If :math:`\globalinst.\GIMUT` is |MCONST|, then the :ref:`value <syntax-val>` :math:`\globalinst.\GIVALUE` must remain unchanged.
* If :math:`\mut` is |MCONST|, then the :ref:`value <syntax-val>` :math:`\globalinst.\GIVALUE` must remain unchanged.

.. math::
\frac{
\mut = \MVAR \vee c_1 = c_2
\mut = \MVAR \vee \val_1 = \val_2
}{
\vdashglobalinstextends \{\GIVALUE~(t.\CONST~c_1), \GIMUT~\mut\} \extendsto \{\GIVALUE~(t.\CONST~c_2), \GIMUT~\mut\}
\vdashglobalinstextends \{\GITYPE~(\mut~t), \GIVALUE~\val_1\} \extendsto \{\GITYPE~(\mut~t), \GIVALUE~\val_2\}
}
Expand Down
Loading

0 comments on commit 09dccac

Please # to comment.