diff --git a/document/binary/instructions.rst b/document/binary/instructions.rst index 945b391e8b..fb64b6634c 100644 --- a/document/binary/instructions.rst +++ b/document/binary/instructions.rst @@ -37,7 +37,7 @@ Control Instructions .. math:: \begin{array}{llclll} - \production{instructions} & \Binstr &::=& + \production{instruction} & \Binstr &::=& \hex{00} &\Rightarrow& \UNREACHABLE \\ &&|& \hex{01} &\Rightarrow& \NOP \\ &&|& \hex{02}~~\X{rt}{:}\Bblocktype~~(\X{in}{:}\Binstr)^\ast~~\hex{0B} @@ -77,7 +77,7 @@ Parametric Instructions .. math:: \begin{array}{llclll} - \production{instructions} & \Binstr &::=& \dots \\ &&|& + \production{instruction} & \Binstr &::=& \dots \\ &&|& \hex{1A} &\Rightarrow& \DROP \\ &&|& \hex{1B} &\Rightarrow& \SELECT \\ \end{array} @@ -101,7 +101,7 @@ Variable Instructions .. math:: \begin{array}{llclll} - \production{instructions} & \Binstr &::=& \dots \\ &&|& + \production{instruction} & \Binstr &::=& \dots \\ &&|& \hex{20}~~x{:}\Blocalidx &\Rightarrow& \GETLOCAL~x \\ &&|& \hex{21}~~x{:}\Blocalidx &\Rightarrow& \SETLOCAL~x \\ &&|& \hex{22}~~x{:}\Blocalidx &\Rightarrow& \TEELOCAL~x \\ &&|& @@ -131,9 +131,9 @@ Each variant of :ref:`memory instruction ` is encoded with .. math:: \begin{array}{llclll} - \production{memory arguments} & \Bmemarg &::=& + \production{memory argument} & \Bmemarg &::=& a{:}\Bu32~~o{:}\Bu32 &\Rightarrow& \{ \ALIGN~a,~\OFFSET~o \} \\ - \production{instructions} & \Binstr &::=& \dots \\ &&|& + \production{instruction} & \Binstr &::=& \dots \\ &&|& \hex{28}~~m{:}\Bmemarg &\Rightarrow& \I32.\LOAD~m \\ &&|& \hex{29}~~m{:}\Bmemarg &\Rightarrow& \I64.\LOAD~m \\ &&|& \hex{2A}~~m{:}\Bmemarg &\Rightarrow& \F32.\LOAD~m \\ &&|& @@ -181,7 +181,7 @@ The |CONST| instructions are followed by the respective literal. .. math:: \begin{array}{llclll} - \production{instructions} & \Binstr &::=& \dots \\&&|& + \production{instruction} & \Binstr &::=& \dots \\&&|& \hex{41}~~n{:}\Bi32 &\Rightarrow& \I32.\CONST~n \\ &&|& \hex{42}~~n{:}\Bi64 &\Rightarrow& \I64.\CONST~n \\ &&|& \hex{43}~~z{:}\Bf32 &\Rightarrow& \F32.\CONST~z \\ &&|& @@ -195,7 +195,7 @@ All other numeric instructions are plain opcodes without any immediates. .. math:: \begin{array}{llclll} - \production{instructions} & \Binstr &::=& \dots && \phantom{thisshouldbeenough} \\&&|& + \production{instruction} & \Binstr &::=& \dots && \phantom{thisshouldbeenough} \\&&|& \hex{45} &\Rightarrow& \I32.\EQZ \\ &&|& \hex{46} &\Rightarrow& \I32.\EQ \\ &&|& \hex{47} &\Rightarrow& \I32.\NE \\ &&|& @@ -211,7 +211,7 @@ All other numeric instructions are plain opcodes without any immediates. .. math:: \begin{array}{llclll} - \phantom{\production{instructions}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& + \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& \hex{50} &\Rightarrow& \I64.\EQZ \\ &&|& \hex{51} &\Rightarrow& \I64.\EQ \\ &&|& \hex{52} &\Rightarrow& \I64.\NE \\ &&|& @@ -227,7 +227,7 @@ All other numeric instructions are plain opcodes without any immediates. .. math:: \begin{array}{llclll} - \phantom{\production{instructions}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& + \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& \hex{5B} &\Rightarrow& \F32.\EQ \\ &&|& \hex{5C} &\Rightarrow& \F32.\NE \\ &&|& \hex{5D} &\Rightarrow& \F32.\LT \\ &&|& @@ -238,7 +238,7 @@ All other numeric instructions are plain opcodes without any immediates. .. math:: \begin{array}{llclll} - \phantom{\production{instructions}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& + \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& \hex{61} &\Rightarrow& \F64.\EQ \\ &&|& \hex{62} &\Rightarrow& \F64.\NE \\ &&|& \hex{63} &\Rightarrow& \F64.\LT \\ &&|& @@ -252,7 +252,7 @@ All other numeric instructions are plain opcodes without any immediates. .. math:: \begin{array}{llclll} - \phantom{\production{instructions}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& + \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& \hex{67} &\Rightarrow& \I32.\CLZ \\ &&|& \hex{68} &\Rightarrow& \I32.\CTZ \\ &&|& \hex{69} &\Rightarrow& \I32.\POPCNT \\ &&|& @@ -275,7 +275,7 @@ All other numeric instructions are plain opcodes without any immediates. .. math:: \begin{array}{llclll} - \phantom{\production{instructions}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& + \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& \hex{79} &\Rightarrow& \I64.\CLZ \\ &&|& \hex{7A} &\Rightarrow& \I64.\CTZ \\ &&|& \hex{7B} &\Rightarrow& \I64.\POPCNT \\ &&|& @@ -298,7 +298,7 @@ All other numeric instructions are plain opcodes without any immediates. .. math:: \begin{array}{llclll} - \phantom{\production{instructions}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& + \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& \hex{8B} &\Rightarrow& \F32.\ABS \\ &&|& \hex{8C} &\Rightarrow& \F32.\NEG \\ &&|& \hex{8D} &\Rightarrow& \F32.\CEIL \\ &&|& @@ -317,7 +317,7 @@ All other numeric instructions are plain opcodes without any immediates. .. math:: \begin{array}{llclll} - \phantom{\production{instructions}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& + \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& \hex{99} &\Rightarrow& \F64.\ABS \\ &&|& \hex{9A} &\Rightarrow& \F64.\NEG \\ &&|& \hex{9B} &\Rightarrow& \F64.\CEIL \\ &&|& @@ -338,7 +338,7 @@ All other numeric instructions are plain opcodes without any immediates. .. math:: \begin{array}{llclll} - \phantom{\production{instructions}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& + \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& \hex{A7} &\Rightarrow& \I32.\WRAP\K{/}\I64 \\ &&|& \hex{A8} &\Rightarrow& \I32.\TRUNC\K{\_s/}\F32 \\ &&|& \hex{A9} &\Rightarrow& \I32.\TRUNC\K{\_u/}\F32 \\ &&|& @@ -380,6 +380,6 @@ Expressions .. math:: \begin{array}{llclll} - \production{instructions} & \Bexpr &::=& + \production{expression} & \Bexpr &::=& (\X{in}{:}\Binstr)^\ast~~\hex{0B} &\Rightarrow& \X{in}^\ast~\END \\ \end{array} diff --git a/document/binary/modules.rst b/document/binary/modules.rst index 4431f17841..bd20c8be73 100644 --- a/document/binary/modules.rst +++ b/document/binary/modules.rst @@ -40,13 +40,13 @@ All :ref:`indices ` are encoded with their respective |U32| value. .. math:: \begin{array}{llclll} - \production{type indices} & \Btypeidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{function indices} & \Bfuncidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{table indices} & \Btableidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{memory indices} & \Bmemidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{global indices} & \Bglobalidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{local indices} & \Blocalidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{label indices} & \Blabelidx &::=& l{:}\Bu32 &\Rightarrow& l \\ + \production{type index} & \Btypeidx &::=& x{:}\Bu32 &\Rightarrow& x \\ + \production{function index} & \Bfuncidx &::=& x{:}\Bu32 &\Rightarrow& x \\ + \production{table index} & \Btableidx &::=& x{:}\Bu32 &\Rightarrow& x \\ + \production{memory index} & \Bmemidx &::=& x{:}\Bu32 &\Rightarrow& x \\ + \production{global index} & \Bglobalidx &::=& x{:}\Bu32 &\Rightarrow& x \\ + \production{local index} & \Blocalidx &::=& x{:}\Bu32 &\Rightarrow& x \\ + \production{label index} & \Blabelidx &::=& l{:}\Bu32 &\Rightarrow& l \\ \end{array} @@ -69,7 +69,7 @@ The following parameterized grammar rule defines the generic structure of a sect .. math:: \begin{array}{llclll@{\qquad}l} - \production{sections} & \Bsection_N(\B{B}) &::=& + \production{section} & \Bsection_N(\B{B}) &::=& N{:}\Bbyte~~\X{size}{:}\Bu32~~\X{cont}{:}\B{B} &\Rightarrow& \X{cont} & (\X{size} = ||\B{B}||) \\ &&|& \epsilon &\Rightarrow& \epsilon @@ -98,7 +98,7 @@ Their contents consist of a :ref:`name ` further identifying the cu .. math:: \begin{array}{llclll} - \production{custom sections} & \Bcustomsec &::=& + \production{custom section} & \Bcustomsec &::=& \Bsection_0(\Bcustom) \\ \production{custom data} & \Bcustom &::=& \Bname~~\Bbyte^\ast \\ @@ -123,7 +123,7 @@ It decodes into a vector of :ref:`function types ` that represe .. math:: \begin{array}{llclll} - \production{type sections} & \Btypesec &::=& + \production{type section} & \Btypesec &::=& \X{ft}^\ast{:\,}\Bsection_1(\Bvec(\Bfunctype)) &\Rightarrow& \X{ft}^\ast \\ \end{array} @@ -143,12 +143,12 @@ It decodes into a vector of :ref:`imports ` that represent the |I .. math:: \begin{array}{llclll} - \production{import sections} & \Bimportsec &::=& + \production{import section} & \Bimportsec &::=& \X{im}^\ast{:}\Bsection_2(\Bvec(\Bimport)) &\Rightarrow& \X{im}^\ast \\ - \production{imports} & \Bimport &::=& + \production{import} & \Bimport &::=& \X{mod}{:}\Bname~~\X{nm}{:}\Bname~~d{:}\Bimportdesc &\Rightarrow& \{ \MODULE~\X{mod}, \NAME~\X{nm}, \DESC~d \} \\ - \production{import descriptions} & \Bimportdesc &::=& + \production{import description} & \Bimportdesc &::=& \hex{00}~~x{:}\Btypeidx &\Rightarrow& \FUNC~x \\ &&|& \hex{01}~~\X{tt}{:}\Btabletype &\Rightarrow& \TABLE~\X{tt} \\ &&|& \hex{02}~~\X{mt}{:}\Bmemtype &\Rightarrow& \MEM~\X{mt} \\ &&|& @@ -172,7 +172,7 @@ The |LOCALS| and |BODY| fields of the respective functions are encoded separatel .. math:: \begin{array}{llclll} - \production{function sections} & \Bfuncsec &::=& + \production{function section} & \Bfuncsec &::=& x^\ast{:}\Bsection_3(\Bvec(\Btypeidx)) &\Rightarrow& x^\ast \\ \end{array} @@ -192,9 +192,9 @@ It decodes into a vector of :ref:`tables ` that represent the |TAB .. math:: \begin{array}{llclll} - \production{table sections} & \Btablesec &::=& + \production{table section} & \Btablesec &::=& \X{tab}^\ast{:}\Bsection_4(\Bvec(\Btable)) &\Rightarrow& \X{tab}^\ast \\ - \production{tables} & \Btable &::=& + \production{table} & \Btable &::=& \X{tt}{:}\Btabletype &\Rightarrow& \{ \TYPE~\X{tt} \} \\ \end{array} @@ -214,9 +214,9 @@ It decodes into a vector of :ref:`memories ` that represent the |MEM .. math:: \begin{array}{llclll} - \production{memory sections} & \Bmemsec &::=& + \production{memory section} & \Bmemsec &::=& \X{mem}^\ast{:}\Bsection_5(\Bvec(\Bmem)) &\Rightarrow& \X{mem}^\ast \\ - \production{memories} & \Bmem &::=& + \production{memory} & \Bmem &::=& \X{mt}{:}\Bmemtype &\Rightarrow& \{ \TYPE~\X{mt} \} \\ \end{array} @@ -236,9 +236,9 @@ It decodes into a vector of :ref:`globals ` that represent the |G .. math:: \begin{array}{llclll} - \production{global sections} & \Bglobalsec &::=& + \production{global section} & \Bglobalsec &::=& \X{glob}^\ast{:}\Bsection_6(\Bvec(\Bglobal)) &\Rightarrow& \X{glob}^\ast \\ - \production{globals} & \Bglobal &::=& + \production{global} & \Bglobal &::=& \X{gt}{:}\Bglobaltype~~e{:}\Bexpr &\Rightarrow& \{ \TYPE~\X{gt}, \INIT~e \} \\ \end{array} @@ -259,12 +259,12 @@ It decodes into a vector of :ref:`exports ` that represent the |E .. math:: \begin{array}{llclll} - \production{export sections} & \Bexportsec &::=& + \production{export section} & \Bexportsec &::=& \X{ex}^\ast{:}\Bsection_7(\Bvec(\Bexport)) &\Rightarrow& \X{ex}^\ast \\ - \production{exports} & \Bexport &::=& + \production{export} & \Bexport &::=& \X{nm}{:}\Bname~~d{:}\Bexportdesc &\Rightarrow& \{ \NAME~\X{nm}, \DESC~d \} \\ - \production{export descriptions} & \Bexportdesc &::=& + \production{export description} & \Bexportdesc &::=& \hex{00}~~x{:}\Bfuncidx &\Rightarrow& \FUNC~x \\ &&|& \hex{01}~~x{:}\Btableidx &\Rightarrow& \TABLE~x \\ &&|& \hex{02}~~x{:}\Bmemidx &\Rightarrow& \MEM~x \\ &&|& @@ -288,9 +288,9 @@ It decodes into an optional :ref:`start function ` that represents .. math:: \begin{array}{llclll} - \production{start sections} & \Bstartsec &::=& + \production{start section} & \Bstartsec &::=& \X{st}^?{:}\Bsection_8(\Bstart) &\Rightarrow& \X{st}^? \\ - \production{start functions} & \Bstart &::=& + \production{start function} & \Bstart &::=& x{:}\Bfuncidx &\Rightarrow& \{ \FUNC~x \} \\ \end{array} @@ -312,9 +312,9 @@ It decodes into a vector of :ref:`element segments ` that represent .. math:: \begin{array}{llclll} - \production{element sections} & \Belemsec &::=& + \production{element section} & \Belemsec &::=& \X{seg}^\ast{:}\Bsection_9(\Bvec(\Belem)) &\Rightarrow& \X{seg} \\ - \production{element segments} & \Belem &::=& + \production{element segment} & \Belem &::=& x{:}\Btableidx~~e{:}\Bexpr~~y^\ast{:}\Bvec(\Bfuncidx) &\Rightarrow& \{ \TABLE~x, \OFFSET~e, \INIT~y^\ast \} \\ \end{array} @@ -352,13 +352,13 @@ denoting *count* locals of the same value type. .. math:: \begin{array}{llclll@{\qquad}l} - \production{code sections} & \Bcodesec &::=& + \production{code section} & \Bcodesec &::=& \X{code}^\ast{:}\Bsection_{10}(\Bvec(\Bcode)) &\Rightarrow& \X{code}^\ast \\ \production{code} & \Bcode &::=& \X{size}{:}\Bu32~~\X{code}{:}\Bfunc &\Rightarrow& \X{code} & (\X{size} = ||\Bfunc||) \\ - \production{functions} & \Bfunc &::=& + \production{function} & \Bfunc &::=& (t^\ast)^\ast{:}\Bvec(\Blocals)~~e{:}\Bexpr &\Rightarrow& \F{concat}((t^\ast)^\ast), e^\ast & (|\F{concat}((t^\ast)^\ast)| < 2^{32}) \\ @@ -392,9 +392,9 @@ It decodes into a vector of :ref:`data segments ` that represent th .. math:: \begin{array}{llclll} - \production{data sections} & \Bdatasec &::=& + \production{data section} & \Bdatasec &::=& \X{seg}^\ast{:}\Bsection_{11}(\Bvec(\Bdata)) &\Rightarrow& \X{seg} \\ - \production{data segments} & \Bdata &::=& + \production{data segment} & \Bdata &::=& x{:}\Bmemidx~~e{:}\Bexpr~~b^\ast{:}\Bvec(\Bbyte) &\Rightarrow& \{ \MEM~x, \OFFSET~e, \INIT~b^\ast \} \\ \end{array} @@ -425,7 +425,7 @@ The lengths of vectors produced by the (possibly empty) :ref:`function ` occurring in the binary format .. math:: \begin{array}{llclll@{\qquad\qquad}l} - \production{result types} & \Bblocktype &::=& + \production{result type} & \Bblocktype &::=& \hex{40} &\Rightarrow& [] \\ &&|& t{:}\Bvaltype &\Rightarrow& [t] \\ \end{array} @@ -64,7 +64,7 @@ Function Types .. math:: \begin{array}{llclll@{\qquad\qquad}l} - \production{function types} & \Bfunctype &::=& + \production{function type} & \Bfunctype &::=& \hex{60}~~t_1^\ast{:\,}\Bvec(\Bvaltype)~~t_2^\ast{:\,}\Bvec(\Bvaltype) &\Rightarrow& [t_1^\ast] \to [t_2^\ast] \\ \end{array} @@ -100,7 +100,7 @@ Memory Types .. math:: \begin{array}{llclll@{\qquad\qquad}l} - \production{memory types} & \Bmemtype &::=& + \production{memory type} & \Bmemtype &::=& \X{lim}{:}\Blimits &\Rightarrow& \X{lim} \\ \end{array} @@ -120,9 +120,9 @@ Table Types .. math:: \begin{array}{llclll} - \production{table types} & \Btabletype &::=& + \production{table type} & \Btabletype &::=& \X{et}{:}\Belemtype~~\X{lim}{:}\Blimits &\Rightarrow& \X{lim}~\X{et} \\ - \production{element types} & \Belemtype &::=& + \production{element type} & \Belemtype &::=& \hex{70} &\Rightarrow& \ANYFUNC \\ \end{array} @@ -141,9 +141,9 @@ Global Types .. math:: \begin{array}{llclll} - \production{global types} & \Bglobaltype &::=& + \production{global type} & \Bglobaltype &::=& t{:}\Bvaltype~~m{:}\Bmut &\Rightarrow& m~t \\ \production{mutability} & \Bmut &::=& - \hex{00} &\Rightarrow& \CONST \\ &&|& - \hex{01} &\Rightarrow& \MUT \\ + \hex{00} &\Rightarrow& \MCONST \\ &&|& + \hex{01} &\Rightarrow& \MVAR \\ \end{array} diff --git a/document/binary/values.rst b/document/binary/values.rst index b2abed9ffa..8a4366501c 100644 --- a/document/binary/values.rst +++ b/document/binary/values.rst @@ -19,7 +19,7 @@ Bytes .. math:: \begin{array}{llcll@{\qquad}l} - \production{bytes} & \Bbyte &::=& + \production{byte} & \Bbyte &::=& \hex{00} &\Rightarrow& \hex{00} \\ &&|&& \dots \\ &&|& \hex{FF} &\Rightarrow& \hex{FF} \\ @@ -49,9 +49,9 @@ As an additional constraint, the total number of bytes encoding a value of type .. math:: \begin{array}{llclll@{\qquad}l} - \production{unsigned integers} & \BuX{N} &::=& + \production{unsigned integer} & \BuX{N} &::=& n{:}\Bbyte &\Rightarrow& n & (n < 2^7 \wedge n < 2^N) \\ &&|& - n{:}\Bbyte~~m{:}\BuX{N-7} &\Rightarrow& + n{:}\Bbyte~~m{:}\BuX{(N\B{-7})} &\Rightarrow& 2^7\cdot m + (n-2^7) & (n \geq 2^7 \wedge N > 7) \\ \end{array} @@ -60,19 +60,19 @@ As an additional constraint, the total number of bytes encoding a value of type .. math:: \begin{array}{llclll@{\qquad}l} - \production{signed integers} & \BsX{N} &::=& + \production{signed integer} & \BsX{N} &::=& n{:}\Bbyte &\Rightarrow& n & (n < 2^6 \wedge n < 2^{N-1}) \\ &&|& n{:}\Bbyte &\Rightarrow& n-2^7 & (2^6 \leq n < 2^7 \wedge n \geq 2^7-2^{N-1}) \\ &&|& - n{:}\Bbyte~~m{:}\BsX{N-7} &\Rightarrow& + n{:}\Bbyte~~m{:}\BsX{(N\B{-7})} &\Rightarrow& 2^7\cdot m + (n-2^7) & (n \geq 2^7 \wedge N > 7) \\ \end{array} -:ref:`Uninterpreted integers ` are always encoded as signed integers. +:ref:`Uninterpreted integers ` are encoded as signed integers. .. math:: \begin{array}{llclll@{\qquad\qquad}l} - \production{uninterpreted integers} & \BiX{N} &::=& - n{:}\BsX{N} &\Rightarrow& n + \production{uninterpreted integer} & \BiX{N} &::=& + n{:}\BsX{N} &\Rightarrow& i & (n = \signed_{\iX{N}}(i)) \end{array} .. note:: @@ -99,7 +99,7 @@ Floating-Point .. math:: \begin{array}{llclll@{\qquad\qquad}l} - \production{floating-point numbers} & \BfX{N} &::=& + \production{floating-point number} & \BfX{N} &::=& b^\ast{:\,}\Bbyte^{N/8} &\Rightarrow& \F{reverse}(b^\ast) \\ \end{array} @@ -118,7 +118,7 @@ Vectors .. math:: \begin{array}{llclll@{\qquad\qquad}l} - \production{vectors} & \Bvec(\B{B}) &::=& + \production{vector} & \Bvec(\B{B}) &::=& n{:}\Bu32~~(x{:}\B{B})^n &\Rightarrow& x^n \\ \end{array} @@ -135,13 +135,13 @@ Names .. math:: \begin{array}{llclll@{\qquad}l} - \production{names} & \Bname &::=& + \production{name} & \Bname &::=& n{:}\Bu32~~(\X{uc}{:}\Bcodepoint)^\ast &\Rightarrow& \X{uc}^\ast & (|\Bcodepoint^\ast| = n) \\ - \production{code points} & \Bcodepoint &::=& + \production{code point} & \Bcodepoint &::=& \X{uv}{:}\Bcodeval_N &\Rightarrow& \X{uv} & (\X{uv} \geq N \wedge (\X{uv} < \unicode{D800} \vee \unicode{E000} \leq \X{uv} < \unicode{110000})) \\ - \production{code values} & \Bcodeval_N &::=& + \production{code value} & \Bcodeval_N &::=& b_1{:}\Bbyte &\Rightarrow& b_1 & (b_1 < \hex{80} \wedge N = \unicode{00}) \\ &&|& diff --git a/document/execution/conventions.rst b/document/execution/conventions.rst new file mode 100644 index 0000000000..81d1c9f276 --- /dev/null +++ b/document/execution/conventions.rst @@ -0,0 +1,131 @@ +.. index:: ! execution, stack, store + +Conventions +----------- + +WebAssembly code is *executed* when :ref:`instantiating ` a module or :ref:`invoking ` an :ref:`exported ` function on the resulting module :ref:`instance `. + +Execution behavior is defined in terms of an *abstract machine* that models the *program state*. +It includes a *stack*, which records operand values and control constructs, and an abstract *store* containing global state. + +For each instruction, there is a rule that specifies the effect of its execution on the program state. +Furthermore, there are rules describing the instantiation of a module. +As with :ref:`validation `, all rules are given in two *equivalent* forms: + +1. In *prose*, describing the execution in intuitive form. +2. In *formal notation*, describing the rule in mathematical form. + +.. note:: + As with validation, the prose and formal rules are equivalent, + so that understanding of the formal notation is *not* required to read this specification. + The formalism offers a more concise description in notation that is used widely in programming languages semantics and is readily amenable to mathematical proof. + +:ref:`Store `, :ref:`stack `, and other *runtime structure*, such as :ref:`module instances `, are made precise in terms of additional auxiliary :ref:`syntax `. + + +.. _exec-notation-textual: + +Prose Notation +~~~~~~~~~~~~~~ + +Execution is specified by stylised, step-wise rules for each :ref:`instruction ` of the :ref:`abstract syntax `. +The following conventions are adopted in stating these rules. + +* The execution rules implicitly assume a given :ref:`store ` :math:`S`. + +* The execution rules also assume the presence of an implicit :ref:`stack ` + that is modified by *pushing* or *popping* + :ref:`values `, :ref:`labels `, and :ref:`frames `. + +* Certain rules require the stack to contain at least one frame, + which is referred to as the *current* frame. + +* Both the store and the current frame are mutated by *replacing* some of its components. + Such replacement is assumed to apply globally. + +* The execution of an instruction may *trap*, + in which case the entire computation is aborted and no further modifications to the store are performed by it. (Other computations can still be initiated afterwards.) + +* The execution of an instruction may also end in a *jump* to a designated target, + which defines the next instruction to execute. + +* Execution can *enter* and *exit* :ref:`instruction sequences ` in a block-like fashion. + +* :ref:`Instruction sequences ` are implicitly executed in order, unless a trap or jump occurs. + +* In various places the rules contain *assertions* expressing crucial invariants about the program state, with indications why these are known to hold. + + +.. _exec-notation: +.. index:: ! reduction rules, ! configuration + +Formal Notation +~~~~~~~~~~~~~~~ + +.. note:: + This section gives a brief explanation of the notation for specifying execution formally. + For the interested reader, a more thorough introduction can be found in respective text books. [#tapl]_ + +The formal execution rules use a standard approach for specifying operational semantics, rendering them into *reduction rules*. +Every rule has the following general form: + +.. math:: + \X{configuration} \quad\stepto\quad \X{configuration} + +A *configuration* is a syntactic description of a program state. +Each rule specifies one *step* of execution. +As long as there is at most one reduction rule applicable to a given configuration, reduction -- and thereby execution -- is *deterministic*. +WebAssembly has only very few exceptions to this, which are noted explicitly in this specification. + +For WebAssembly, a configuration is a tuple :math:`(S; F; \instr^\ast)` consisting of the current :ref:`store ` :math:`S`, the :ref:`call frame ` :math:`F` of the current function, and the sequence of :ref:`instructions ` that is to be executed. + +To avoid unnecessary clutter, the store :math:`S` and the frame :math:`F` are omitted from reduction rules that do not touch them. + +There is no separate representation of the :ref:`stack `. +Instead, it is conveniently represented as part of the configuration's instruction sequence. +In particular, :ref:`values ` are defined to coincide with |CONST| instructions, +and a sequence of |CONST| instructions can be interpreted as an operand "stack". + +.. note:: + For example, the :ref:`reduction rule ` for the :math:`\I32.\ADD` instruction could be given as follows: + + .. math:: + (\I32.\CONST~n_1)~(\I32.\CONST~n_2)~\I32.\ADD \quad\stepto\quad (\I32.\CONST~(n_1 + n_2) \mod 2^{32}) + + Per this rule, two |CONST| instructions and the |ADD| instruction itself are removed from the instruction stream and replaced with one new |CONST| instruction. + This can be interpreted as popping two value off the stack and pushing the result. + + When no result is produced, an instruction reduces to the empty sequence: + + .. math:: + \NOP \quad\stepto\quad \epsilon + +:ref:`Labels