diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index c378232192..d9b6a35487 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -237,7 +237,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co :ref:`Memory Instances ` :math:`\{ \MITYPE~\limits, \MIDATA~b^\ast \}` ...................................................................................... -* The :ref:`memory type ` :math:`\{\LMIN~n, \LMAX~m^?\}` must be :ref:`valid `. +* The :ref:`memory type ` :math:`\limits` must be :ref:`valid `. * The length of :math:`b^\ast` must equal :math:`\limits.\LMIN` multiplied by the :ref:`page size ` :math:`64\,\F{Ki}`. diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index c253a17eda..6b0280603c 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -1256,7 +1256,7 @@ Table Instructions .. math:: \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; \TABLESIZE~x &\stepto& S; F; (\I32.\CONST~\X{sz}) + S; F; (\TABLESIZE~x) &\stepto& S; F; (\I32.\CONST~\X{sz}) \end{array} \\ \qquad (\iff |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM| = \X{sz}) \\ @@ -1288,19 +1288,21 @@ Table Instructions 10. Pop the value :math:`\val` from the stack. -11. Either, try :ref:`growing ` :math:`\X{table}` by :math:`n` entries with initialization value :math:`\val`: +11. Let :math:`\X{err}` be the |i32| value :math:`2^{32}-1`, for which :math:`\signed_{32}(\X{err})` is :math:`-1`. + +12. Either, try :ref:`growing ` :math:`\X{table}` by :math:`n` entries with initialization value :math:`\val`: a. If it succeeds, push the value :math:`\I32.\CONST~\X{sz}` to the stack. - b. Else, push the value :math:`\I32.\CONST~(-1)` to the stack. + b. Else, push the value :math:`\I32.\CONST~\X{err}` to the stack. -12. Or, push the value :math:`\I32.\CONST~(-1)` to the stack. +13. Or, push the value :math:`\I32.\CONST~\X{err}` to the stack. .. math:: ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; \val~(\I32.\CONST~n)~\TABLEGROW~x &\stepto& S'; F; (\I32.\CONST~\X{sz}) + S; F; \val~(\I32.\CONST~n)~(\TABLEGROW~x) &\stepto& S'; F; (\I32.\CONST~\X{sz}) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -1310,7 +1312,7 @@ Table Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~n)~\TABLEGROW~x &\stepto& S; F; (\I32.\CONST~{-1}) + S; F; (\I32.\CONST~n)~(\TABLEGROW~x) &\stepto& S; F; (\I32.\CONST~\signed_{32}^{-1}(-1)) \end{array} \end{array} @@ -1511,7 +1513,7 @@ Table Instructions \quad\stepto \\ \qquad S; F; \begin{array}[t]{@{}l@{}} - (\I32.\CONST~d+n-1)~(\I32.\CONST~s+n-1)~(\TABLEGET~y)~(\TABLESET~x) \\ + (\I32.\CONST~d+n)~(\I32.\CONST~s+n)~(\TABLEGET~y)~(\TABLESET~x) \\ (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\TABLECOPY~x~y) \\ \end{array} \\ \qquad @@ -1722,7 +1724,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~k)~(t.\LOAD({N}\K{\_}\sx)^?~\memarg) &\stepto& S; F; \TRAP + S; F; (\I32.\CONST~i)~(t.\LOAD({N}\K{\_}\sx)^?~\memarg) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -1783,7 +1785,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~k)~(\V128.\LOAD{M}\K{x}N\K{\_}\sx~\memarg) &\stepto& S; F; \TRAP + S; F; (\I32.\CONST~i)~(\V128.\LOAD{M}\K{x}N\K{\_}\sx~\memarg) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -1840,7 +1842,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~k)~(\V128.\LOAD{N}\K{\_splat}~\memarg) &\stepto& S; F; \TRAP + S; F; (\I32.\CONST~i)~(\V128.\LOAD{N}\K{\_splat}~\memarg) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -1895,7 +1897,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~k)~(\V128.\LOAD{N}\K{\_zero}~\memarg) &\stepto& S; F; \TRAP + S; F; (\I32.\CONST~i)~(\V128.\LOAD{N}\K{\_zero}~\memarg) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -1957,7 +1959,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~k)~(\V128.\CONST~v)~(\V128.\LOAD{N}\K{\_lane}~\memarg~x) &\stepto& S; F; \TRAP + S; F; (\I32.\CONST~i)~(\V128.\CONST~v)~(\V128.\LOAD{N}\K{\_lane}~\memarg~x) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -2034,7 +2036,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~k)~(t.\CONST~c)~(t.\STORE{N}^?~\memarg) &\stepto& S; F; \TRAP + S; F; (\I32.\CONST~i)~(t.\CONST~c)~(t.\STORE{N}^?~\memarg) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -2091,7 +2093,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~k)~(\V128.\CONST~c)~(\V128.\STORE{N}\K{\_lane}~\memarg~x) &\stepto& S; F; \TRAP + S; F; (\I32.\CONST~i)~(\V128.\CONST~c)~(\V128.\STORE{N}\K{\_lane}~\memarg~x) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -2368,8 +2370,8 @@ Memory Instructions \quad\stepto \\ \qquad S; F; \begin{array}[t]{@{}l@{}} - (\I32.\CONST~d+n-1) \\ - (\I32.\CONST~s+n-1)~(\I32\K{.}\LOAD\K{8\_u}~\{ \OFFSET~0, \ALIGN~0 \}) \\ + (\I32.\CONST~d+n) \\ + (\I32.\CONST~s+n)~(\I32\K{.}\LOAD\K{8\_u}~\{ \OFFSET~0, \ALIGN~0 \}) \\ (\I32\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}) \\ (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~\MEMORYCOPY \\ \end{array} @@ -2679,7 +2681,7 @@ Control Instructions :math:`\BRTABLE~l^\ast~l_N` ........................... -1. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +1. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. 2. Pop the value :math:`\I32.\CONST~i` from the stack. @@ -2858,22 +2860,22 @@ Exiting :math:`\instr^\ast` with label :math:`L` When the end of a block is reached without a jump or trap aborting it, then the following steps are performed. -1. Let :math:`m` be the number of values on the top of the stack. +1. Let :math:`n` be the number of values on the top of the stack. -2. Pop the values :math:`\val^m` from the stack. +2. Pop the values :math:`\val^n` from the stack. -3. Assert: due to :ref:`validation `, the label :math:`L` is now on the top of the stack. +3. Assert: due to :ref:`validation `, the label :math:`L` is now on the top of the stack and has arity :math:`n`. 4. Pop the label from the stack. -5. Push :math:`\val^m` back to the stack. +5. Push :math:`\val^n` back to the stack. 6. Jump to the position after the |END| of the :ref:`structured control instruction ` associated with the label :math:`L`. .. math:: ~\\[-1ex] \begin{array}{lcl@{\qquad}l} - \LABEL_n\{\instr^\ast\}~\val^m~\END &\stepto& \val^m + \LABEL_n\{\instr^\ast\}~\val^n~\END &\stepto& \val^n \end{array} .. note:: diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 149a53a8be..9ee7eccc9c 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -30,18 +30,18 @@ or *external references* pointing to an uninterpreted form of :ref:`extern addre .. math:: \begin{array}{llcl} - \production{(number)} & \num &::=& + \production{number} & \num &::=& \I32.\CONST~\i32 \\&&|& \I64.\CONST~\i64 \\&&|& \F32.\CONST~\f32 \\&&|& \F64.\CONST~\f64 \\ - \production{(vector)} & \vecc &::=& + \production{vector} & \vecc &::=& \V128.\CONST~\i128 \\ - \production{(reference)} & \reff &::=& + \production{reference} & \reff &::=& \REFNULL~t \\&&|& \REFFUNCADDR~\funcaddr \\&&|& \REFEXTERNADDR~\externaddr \\ - \production{(value)} & \val &::=& + \production{value} & \val &::=& \num ~|~ \vecc ~|~ \reff \\ \end{array} @@ -79,7 +79,7 @@ It is either a sequence of :ref:`values ` or a :ref:`trap ` listing .. math:: \begin{array}{llll} - \production{(store)} & \store &::=& \{~ + \production{store} & \store &::=& \{~ \begin{array}[t]{l@{~}ll} \SFUNCS & \funcinst^\ast, \\ \STABLES & \tableinst^\ast, \\ @@ -157,21 +157,21 @@ In addition, an :ref:`embedder ` may supply an uninterpreted set of *h .. math:: \begin{array}{llll} - \production{(address)} & \addr &::=& + \production{address} & \addr &::=& 0 ~|~ 1 ~|~ 2 ~|~ \dots \\ - \production{(function address)} & \funcaddr &::=& + \production{function address} & \funcaddr &::=& \addr \\ - \production{(table address)} & \tableaddr &::=& + \production{table address} & \tableaddr &::=& \addr \\ - \production{(memory address)} & \memaddr &::=& + \production{memory address} & \memaddr &::=& \addr \\ - \production{(global address)} & \globaladdr &::=& + \production{global address} & \globaladdr &::=& \addr \\ - \production{(element address)} & \elemaddr &::=& + \production{element address} & \elemaddr &::=& \addr \\ - \production{(data address)} & \dataaddr &::=& + \production{data address} & \dataaddr &::=& \addr \\ - \production{(extern address)} & \externaddr &::=& + \production{extern address} & \externaddr &::=& \addr \\ \end{array} @@ -204,7 +204,7 @@ and collects runtime representations of all entities that are imported, defined, .. math:: \begin{array}{llll} - \production{(module instance)} & \moduleinst &::=& \{ + \production{module instance} & \moduleinst &::=& \{ \begin{array}[t]{l@{~}ll} \MITYPES & \functype^\ast, \\ \MIFUNCS & \funcaddr^\ast, \\ @@ -238,10 +238,10 @@ The module instance is used to resolve references to other definitions during ex .. math:: \begin{array}{llll} - \production{(function instance)} & \funcinst &::=& + \production{function instance} & \funcinst &::=& \{ \FITYPE~\functype, \FIMODULE~\moduleinst, \FICODE~\func \} \\ &&|& \{ \FITYPE~\functype, \FIHOSTCODE~\hostfunc \} \\ - \production{(host function)} & \hostfunc &::=& \dots \\ + \production{host function} & \hostfunc &::=& \dots \\ \end{array} A *host function* is a function expressed outside WebAssembly but passed to a :ref:`module ` as an :ref:`import `. @@ -268,7 +268,7 @@ It records its :ref:`type ` and holds a vector of :ref:`refere .. math:: \begin{array}{llll} - \production{(table instance)} & \tableinst &::=& + \production{table instance} & \tableinst &::=& \{ \TITYPE~\tabletype, \TIELEM~\vec(\reff) \} \\ \end{array} @@ -292,7 +292,7 @@ It records its :ref:`type ` and holds a vector of :ref:`bytes ` and holds an individual :ref:`val .. math:: \begin{array}{llll} - \production{(global instance)} & \globalinst &::=& + \production{global instance} & \globalinst &::=& \{ \GITYPE~\globaltype, \GIVALUE~\val \} \\ \end{array} @@ -338,7 +338,7 @@ It holds a vector of references and their common :ref:`type `. .. math:: \begin{array}{llll} - \production{(element instance)} & \eleminst &::=& + \production{element instance} & \eleminst &::=& \{ \EITYPE~\reftype, \EIELEM~\vec(\reff) \} \\ \end{array} @@ -356,7 +356,7 @@ It holds a vector of :ref:`bytes `. .. math:: \begin{array}{llll} - \production{(data instance)} & \datainst &::=& + \production{data instance} & \datainst &::=& \{ \DIDATA~\vec(\byte) \} \\ \end{array} @@ -374,7 +374,7 @@ It defines the export's :ref:`name ` and the associated :ref:`exter .. math:: \begin{array}{llll} - \production{(export instance)} & \exportinst &::=& + \production{export instance} & \exportinst &::=& \{ \EINAME~\name, \EIVALUE~\externval \} \\ \end{array} @@ -392,7 +392,7 @@ It is an :ref:`address ` denoting either a :ref:`function instance .. math:: \begin{array}{llcl} - \production{(external value)} & \externval &::=& + \production{external value} & \externval &::=& \EVFUNC~\funcaddr \\&&|& \EVTABLE~\tableaddr \\&&|& \EVMEM~\memaddr \\&&|& @@ -456,7 +456,7 @@ Labels carry an argument arity :math:`n` and their associated branch *target*, w .. math:: \begin{array}{llll} - \production{(label)} & \label &::=& + \production{label} & \label &::=& \LABEL_n\{\instr^\ast\} \\ \end{array} @@ -485,9 +485,9 @@ and a reference to the function's own :ref:`module instance ` .. math:: \begin{array}{llll} - \production{(activation)} & \X{activation} &::=& + \production{activation} & \X{activation} &::=& \FRAME_n\{\frame\} \\ - \production{(frame)} & \frame &::=& + \production{frame} & \frame &::=& \{ \ALOCALS~\val^\ast, \AMODULE~\moduleinst \} \\ \end{array} @@ -529,7 +529,7 @@ In order to express the reduction of :ref:`traps `, :ref:`calls `, the .. math:: \begin{array}{llll} - \production{(block contexts)} & \XB^0 &::=& + \production{block contexts} & \XB^0 &::=& \val^\ast~[\_]~\instr^\ast \\ - \production{(block contexts)} & \XB^{k+1} &::=& + \production{block contexts} & \XB^{k+1} &::=& \val^\ast~\LABEL_n\{\instr^\ast\}~\XB^k~\END~\instr^\ast \\ \end{array} @@ -624,9 +624,9 @@ that operates relative to a current :ref:`frame ` referring to the .. math:: \begin{array}{llcl} - \production{(configuration)} & \config &::=& + \production{configuration} & \config &::=& \store; \thread \\ - \production{(thread)} & \thread &::=& + \production{thread} & \thread &::=& \frame; \instr^\ast \\ \end{array} @@ -645,7 +645,7 @@ Finally, the following definition of *evaluation context* and associated structu .. math:: \begin{array}{llll} - \production{(evaluation contexts)} & E &::=& + \production{evaluation contexts} & E &::=& [\_] ~|~ \val^\ast~E~\instr^\ast ~|~ \LABEL_n\{\instr^\ast\}~E~\END \\ diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index b2d5fd13b8..afcda69c01 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1625,7 +1625,7 @@ Constant Expressions \qquad \frac{ }{ - C \vdashinstrconst \REFNULL \const + C \vdashinstrconst \REFNULL~t \const } \qquad \frac{