Skip to content

Commit

Permalink
Spec syntax, text, binary, and execution for bulk array ops (#387)
Browse files Browse the repository at this point in the history
  • Loading branch information
@tlively
tlively authored Jun 27, 2023
1 parent e74f030 commit 2b7d386
Show file tree
Hide file tree
Showing 5 changed files with 196 additions and 4 deletions.
8 changes: 8 additions & 0 deletions document/core/binary/instructions.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -122,6 +122,10 @@ Generic :ref:`reference instructions <syntax-instr-ref>` are represented by sing
.. _binary-array.get_u:
.. _binary-array.set:
.. _binary-array.len:
.. _binary-array.fill:
.. _binary-array.copy:
.. _binary-array.init_data:
.. _binary-array.init_elem:
.. _binary-i31.new:
.. _binary-i31.get_s:
.. _binary-i31.get_u:
Expand All @@ -144,13 +148,15 @@ Generic :ref:`reference instructions <syntax-instr-ref>` are represented by sing
\hex{FB}~~4{:}\Bu32~~x{:}\Btypeidx~~i{:}\Bu32 &\Rightarrow& \STRUCTGETS~x~i \\ &&|&
\hex{FB}~~5{:}\Bu32~~x{:}\Btypeidx~~i{:}\Bu32 &\Rightarrow& \STRUCTGETU~x~i \\ &&|&
\hex{FB}~~6{:}\Bu32~~x{:}\Btypeidx~~i{:}\Bu32 &\Rightarrow& \STRUCTSET~x~i \\ &&|&
\hex{FB}~~16{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \ARRAYFILL~x \\ &&|&
\hex{FB}~~17{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \ARRAYNEW~x \\ &&|&
\hex{FB}~~18{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \ARRAYNEWDEFAULT~x \\ &&|&
\hex{FB}~~19{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \ARRAYGET~x \\ &&|&
\hex{FB}~~20{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \ARRAYGETS~x \\ &&|&
\hex{FB}~~21{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \ARRAYGETU~x \\ &&|&
\hex{FB}~~22{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \ARRAYSET~x \\ &&|&
\hex{FB}~~23{:}\Bu32 &\Rightarrow& \ARRAYLEN \\ &&|&
\hex{FB}~~24{:}\Bu32~~x{:}\Btypeidx~~y{:}\Btypeidx &\Rightarrow& \ARRAYCOPY~x~y \\ &&|&
\hex{FB}~~25{:}\Bu32~~x{:}\Btypeidx~~n{:}\Bu32 &\Rightarrow& \ARRAYNEWFIXED~x~n \\ &&|&
\hex{FB}~~27{:}\Bu32~~x{:}\Btypeidx~~y{:}\Bdataidx &\Rightarrow& \ARRAYNEWDATA~x~y \\ &&|&
\hex{FB}~~28{:}\Bu32~~x{:}\Btypeidx~~y{:}\Belemidx &\Rightarrow& \ARRAYNEWELEM~x~y \\ &&|&
Expand All @@ -161,6 +167,8 @@ Generic :ref:`reference instructions <syntax-instr-ref>` are represented by sing
\hex{FB}~~65{:}\Bu32~~\X{ht}{:}\Bheaptype &\Rightarrow& \REFCAST~(\REF~\X{ht}) \\ &&|&
\hex{FB}~~72{:}\Bu32~~\X{ht}{:}\Bheaptype &\Rightarrow& \REFTEST~(\REF~\NULL~\X{ht}) \\ &&|&
\hex{FB}~~73{:}\Bu32~~\X{ht}{:}\Bheaptype &\Rightarrow& \REFCAST~(\REF~\NULL~\X{ht}) \\ &&|&
\hex{FB}~~84{:}\Bu32~~x{:}\Btypeidx~~y{:}\Bdataidx &\Rightarrow& \ARRAYINITDATA~x~y \\ &&|&
\hex{FB}~~85{:}\Bu32~~x{:}\Btypeidx~~y{:}\Belemidx &\Rightarrow& \ARRAYINITELEM~x~y \\ &&|&
\hex{FB}~~112{:}\Bu32 &\Rightarrow& \EXTERNINTERNALIZE \\ &&|&
\hex{FB}~~113{:}\Bu32 &\Rightarrow& \EXTERNEXTERNALIZE \\
\end{array}
Expand Down
163 changes: 163 additions & 0 deletions document/core/exec/instructions.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -686,6 +686,169 @@ Reference Instructions
\end{array}
.. _exec-array.fill:

:math:`\ARRAYFILL~\typeidx`
...........................

.. todo:: Prose

.. math::
~\\[-1ex]
\begin{array}{l}
S; (\REFARRAYADDR~a)~(\I32.\CONST~d)~\val~(\I32.\CONST~n)~(\ARRAYFILL~x)
\quad\stepto\quad \TRAP
\\ \qquad
(\iff d + n > |S.\SARRAYS[a].\AIFIELDS|)
\\[1ex]
S; (\REFARRAYADDR~a)~(\I32.\CONST~d)~\val~(\I32.\CONST~0)~(\ARRAYFILL~x)
\quad\stepto\quad S; \epsilon
\\ \qquad
(\otherwise)
\\[1ex]
S; (\REFARRAYADDR~a)~(\I32.\CONST~d)~\val~(\I32.\CONST~n+1)~(\ARRAYFILL~x)
\quad\stepto
\\ \quad S;
\begin{array}[t]{@{}l@{}}
(\REFARRAYADDR~a)~(\I32.\CONST~d)~\val~(\ARRAYSET~x) \\
(\REFARRAYADDR~a)~(\I32.\CONST~d+1)~\val~(\I32.\CONST~n)~(\ARRAYFILL~x) \\
\end{array}
\\ \qquad
(\otherwise)
\\[1ex]
S; (\REFNULL~t)~(\I32.\CONST~d)~\val~(\I32.\CONST~n)~(\ARRAYFILL~x) \quad\stepto\quad \TRAP
\end{array}
.. _exec-array.copy:

:math:`\ARRAYCOPY~\typeidx~\typeidx`
....................................

.. todo:: Prose

.. todo:: Handle packed fields correctly via array.get_u instead of array.get

.. math::
~\\[-1ex]
\begin{array}{l}
S; (\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y)
\quad\stepto\quad \TRAP
\\ \qquad
(\iff d + n > |S.\SARRAYS[a_1].\AIFIELDS| \vee s + n > |S.\SARRAYS[a_2].\AIFIELDS|)
\\[1ex]
S; (\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\ARRAYCOPY~x~y)
\quad\stepto\quad S; \epsilon
\\ \qquad
(\otherwise)
\\[1ex]
S; (\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\ARRAYCOPY~x~y)
\quad\stepto
\\ \quad S;
\begin{array}[t]{@{}l@{}}
(\REFARRAYADDR~a_1)~(\I32.\CONST~d) \\
(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\ARRAYGET~y) \\
(\ARRAYSET~x) \\
(\REFARRAYADDR~a_1)~(\I32.\CONST~d+1)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \\
\end{array}
\\ \qquad
(\otherwise, \iff d \leq s)
\\[1ex]
S; (\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\ARRAYCOPY~x~y)
\quad\stepto
\\ \quad S;
\begin{array}[t]{@{}l@{}}
(\REFARRAYADDR~a_1)~(\I32.\CONST~d+n) \\
(\REFARRAYADDR~a_2)~(\I32.\CONST~s+n)~(\ARRAYGET~y) \\
(\ARRAYSET~x) \\
(\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \\
\end{array}
\\ \qquad
(\otherwise, \iff d > s)
\\[1ex]
S; (\REFNULL~t)~(\I32.\CONST~d)~\val~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \quad\stepto\quad \TRAP
\\[1ex]
S; \val~(\I32.\CONST~d)~(\REFNULL~t)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \quad\stepto\quad \TRAP
\end{array}
.. _exec-array.init_data:

:math:`\ARRAYINITDATA~\typeidx~\dataidx`
........................................

.. todo:: Prose

.. math::
~\\[-1ex]
\begin{array}{l}
S; F; (\REFARRAYADDR~a)~(\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYINITDATA~x~y) \quad\stepto\quad \TRAP
\\ \qquad
\begin{array}[t]{@{}r@{~}l@{}}
(\iff & d + n > |S.\SARRAYS[a].\AIFIELDS| \\
\vee & (F.\AMODULE.\MITYPES[x] = \TARRAY~\X{ft} \land
s + n\cdot|\X{ft}| > |S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA|))
\end{array}
\\[1ex]
S; F; (\REFARRAYADDR~a)~(\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\ARRAYINITDATA~x~y)
\quad\stepto\quad S; F; \epsilon
\\ \qquad
(\otherwise)
\\[1ex]
S; F; (\REFARRAYADDR~a)~(\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\ARRAYINITDATA~x~y)
\quad\stepto
\\ \quad S; F;
\begin{array}[t]{@{}l@{}}
(\REFARRAYADDR~a)~(\I32.\CONST~d)~(t.\CONST i)~(\ARRAYSET~x) \\
(\REFARRAYADDR~a)~(\I32.\CONST~d+1)~(\I32.\CONST~s+|\X{ft}|)~(\I32.\CONST~n)~(\ARRAYINITDATA~x~y) \\
\end{array}
\\ \qquad
\begin{array}[t]{@{}r@{~}l@{}}
(\otherwise, \iff & F.\AMODULE.\MITYPES[x] = \TARRAY~\X{ft} \\
\land & t = \unpacktype(\X{ft}) \\
\land & \bytes_{\X{ft}}(i) = S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA[s \slice |\X{ft}|]
\end{array}
\\[1ex]
S; F; (\REFNULL~t)~(\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYINITDATA~x~y) \quad\stepto\quad \TRAP
\end{array}
.. _exec-array.init_elem:

:math:`\ARRAYINITELEM~\typeidx~\elemidx`
........................................

.. todo:: Prose

.. math::
~\\[-1ex]
\begin{array}{l}
S; F; (\REFARRAYADDR~a)~(\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYINITELEM~x~y) \quad\stepto\quad \TRAP
\\ \qquad
\begin{array}[t]{@{}r@{~}l@{}}
(\iff & d + n > |S.\SARRAYS[a].\AIFIELDS| \\
\vee & s + n > |S.\SELEMS[F.\AMODULE.\MIELEMS[y]].\EIELEM|)
\end{array}
\\[1ex]
S; F; (\REFARRAYADDR~a)~(\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\ARRAYINITELEM~x~y)
\quad\stepto\quad S; F; \epsilon
\\ \qquad
(\otherwise)
\\[1ex]
S; F; (\REFARRAYADDR~a)~(\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\ARRAYINITELEM~x~y)
\quad\stepto
\\ \quad S; F;
\begin{array}[t]{@{}l@{}}
(\REFARRAYADDR~a)~(\I32.\CONST~d)~\REF~(\ARRAYSET~x) \\
(\REFARRAYADDR~a)~(\I32.\CONST~d+1)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\ARRAYINITELEM~x~y) \\
\end{array}
\\ \qquad
(\otherwise, \iff \REF = S.\SELEMS[F.\AMODULE.\MIELEMS[y]].\EIELEM[s])
\\[1ex]
S; F; (\REFNULL~t)~(\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYINITELEM~x~y) \quad\stepto\quad \TRAP
\end{array}
.. _exec-extern.externalize:

:math:`\EXTERNEXTERNALIZE`
Expand Down
17 changes: 13 additions & 4 deletions document/core/syntax/instructions.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -478,6 +478,10 @@ while the latter performs a downcast and :ref:`traps <trap>` if the operand's ty
.. _syntax-array.get_u:
.. _syntax-array.set:
.. _syntax-array.len:
.. _syntax-array.fill:
.. _syntax-array.copy:
.. _syntax-array.init_data:
.. _syntax-array.init_elem:
.. _syntax-i31.new:
.. _syntax-i31.get_s:
.. _syntax-i31.get_u:
Expand Down Expand Up @@ -508,9 +512,13 @@ Instructions in this group are concerned with creating and accessing :ref:`refer
\ARRAYNEWDATA~\typeidx~\dataidx \\&&|&
\ARRAYNEWELEM~\typeidx~\elemidx \\&&|&
\ARRAYGET~\typeidx \\&&|&
\ARRAYGET(\K{\_}\sx~\typeidx \\&&|&
\ARRAYGET\K{\_}\sx~\typeidx \\&&|&
\ARRAYSET~\typeidx \\&&|&
\ARRAYLEN \\&&|&
\ARRAYFILL~\typeidx \\&&|&
\ARRAYCOPY~\typeidx~\typeidx \\&&|&
\ARRAYINITDATA~\typeidx~\dataidx \\&&|&
\ARRAYINITELEM~\typeidx~\elemidx \\&&|&
\I31NEW \\&&|&
\I31GET\K{\_}\sx \\&&|&
\EXTERNINTERNALIZE \\&&|&
Expand All @@ -523,10 +531,11 @@ allowing for different sign extension modes in the case of :ref:`packed <syntax-

Similarly, :ref:`arrays <syntax-arraytype>` can be allocated either with an explicit initialization operand or a default value.
Furthermore, |ARRAYNEWFIXED| allocates an array with statically fixed size,
and |ARRAYNEWDATA| and |ARRAYNEWELEM| allocate an array and initialize it from a :ref:`data <syntax-data>` or :ref:`element <syntax-elem>` segement, respectively.
The remaining array instructions access individual slots,
and |ARRAYNEWDATA| and |ARRAYNEWELEM| allocate an array and initialize it from a :ref:`data <syntax-data>` or :ref:`element <syntax-elem>` segment, respectively.
|ARRAYGET|, |ARRAYGETS|, |ARRAYGETU|, and |ARRAYSET| access individual slots,
again allowing for different sign extension modes in the case of a :ref:`packed <syntax-packedtype>` storage type.
Last, |ARRAYLEN| produces the length of an array.
|ARRAYLEN| produces the length of an array.
|ARRAYFILL| fills a specified slice of an array with a given value and |ARRAYCOPY|, |ARRAYINITDATA|, and |ARRAYINITELEM| copy elements to a specified slice of an array from a given array, data segment, or element segment, respectively.

The instructions |I31NEW| and :math:`\I31GET\K{\_}\sx` convert between type |I31| and an unboxed :ref:`scalar <syntax-i31>`.

Expand Down
8 changes: 8 additions & 0 deletions document/core/text/instructions.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -195,6 +195,10 @@ Reference Instructions
.. _text-array.get_u:
.. _text-array.set:
.. _text-array.len:
.. _text-array.fill:
.. _text-array.copy:
.. _text-array.init_data:
.. _text-array.init_elem:
.. _text-i31.new:
.. _text-i31.get_s:
.. _text-i31.get_u:
Expand Down Expand Up @@ -229,6 +233,10 @@ Reference Instructions
\text{array.get\_s}~~x{:}\Ttypeidx_I &\Rightarrow& \ARRAYGETS~x \\ &&|&
\text{array.set}~~x{:}\Ttypeidx_I &\Rightarrow& \ARRAYSET~x \\ &&|&
\text{array.len} &\Rightarrow& \ARRAYLEN \\ &&|&
\text{array.fill}~~x{:}\Ttypeidx_I &\Rightarrow& \ARRAYFILL~x \\ &&|&
\text{array.copy}~~x{:}\Ttypeidx_I~~y{:}\Ttypeidx_I &\Rightarrow& \ARRAYCOPY~x~y \\ &&|&
\text{array.init\_data}~~x{:}\Ttypeidx_I~~y{:}\Tdataidx_I &\Rightarrow& \ARRAYINITDATA~x~y \\ &&|&
\text{array.init\_elem}~~x{:}\Ttypeidx_I~~y{:}\Telemidx_I &\Rightarrow& \ARRAYINITELEM~x~y \\ &&|&
\text{i31.new} &\Rightarrow& \I31NEW \\ &&|&
\text{i31.get\_u} &\Rightarrow& \I31GETU \\ &&|&
\text{i31.get\_s} &\Rightarrow& \I31GETS \\ &&|&
Expand Down
4 changes: 4 additions & 0 deletions document/core/util/macros.def
View file
Original file line number Diff line number Diff line change
Expand Up @@ -482,6 +482,10 @@
.. |ARRAYGETU| mathdef:: \xref{syntax/instructions}{syntax-instr-array}{\K{array.get\_u}}
.. |ARRAYSET| mathdef:: \xref{syntax/instructions}{syntax-instr-array}{\K{array.set}}
.. |ARRAYLEN| mathdef:: \xref{syntax/instructions}{syntax-instr-array}{\K{array.len}}
.. |ARRAYFILL| mathdef:: \xref{syntax/instructions}{syntax-instr-aray}{\K{array.fill}}
.. |ARRAYCOPY| mathdef:: \xref{syntax/instructions}{syntax-instr-aray}{\K{array.copy}}
.. |ARRAYINITDATA| mathdef:: \xref{syntax/instructions}{syntax-instr-aray}{\K{array.init\_data}}
.. |ARRAYINITELEM| mathdef:: \xref{syntax/instructions}{syntax-instr-aray}{\K{array.init\_elem}}

.. |I31NEW| mathdef:: \xref{syntax/instructions}{syntax-instr-i31}{\K{i31.new}}
.. |I31GET| mathdef:: \xref{syntax/instructions}{syntax-instr-i31}{\K{i31.get}}
Expand Down

0 comments on commit 2b7d386

Please sign in to comment.