diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 4a3b9fb0e6..63e17be482 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -192,13 +192,26 @@ Reference Instructions .. _exec-ref.null: -:math:`\REFNULL~\X{ht}` +:math:`\REFNULL~x` ....................... -1. Push the value :math:`\REFNULL~\X{ht}` to the stack. +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +2. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. + +3. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. + +4. Push the value :math:`\REFNULL~\deftype` to the stack. + +.. math:: + \begin{array}{lcl@{\qquad}l} + F; (\REFNULL~x) &\stepto& F; (\REFNULL~\deftype) + & (\iff \deftype = F.\AMODULE.\MITYPES[x]) \\ + \end{array} .. note:: - No formal reduction rule is required for this instruction, since the |REFNULL| instruction is already a :ref:`value `. + No formal reduction rule is required for the case |REFNULL| |ABSHEAPTYPE|, + since the instruction form is already a :ref:`value `. .. _exec-ref.func: @@ -428,33 +441,35 @@ Reference Instructions :math:`\STRUCTNEW~x` .................... -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. -2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. +2. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. -3. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is a :ref:`structure type `. +3. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. -4. Let :math:`\TSTRUCT~\X{ft}^\ast` be the :ref:`expanded ` :ref:`structure type ` of :math:`\deftype`. +4. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is a :ref:`structure type `. -5. Let :math:`n` be the length of the :ref:`field type ` sequence :math:`\X{ft}^\ast`. +5. Let :math:`\TSTRUCT~\X{ft}^\ast` be the :ref:`expanded ` :ref:`structure type ` of :math:`\deftype`. -6. Assert: due to :ref:`validation `, :math:`n` :ref:`values ` are on the top of the stack. +6. Let :math:`n` be the length of the :ref:`field type ` sequence :math:`\X{ft}^\ast`. -7. Pop the :math:`n` values :math:`\val^\ast` from the stack. +7. Assert: due to :ref:`validation `, :math:`n` :ref:`values ` are on the top of the stack. + +8. Pop the :math:`n` values :math:`\val^\ast` from the stack. -8. For every value :math:`\val_i` in :math:`\val^\ast` and corresponding :ref:`field type ` :math:`\X{ft}_i` in :math:`\X{ft}^\ast`: +9. For every value :math:`\val_i` in :math:`\val^\ast` and corresponding :ref:`field type ` :math:`\X{ft}_i` in :math:`\X{ft}^\ast`: a. Let :math:`\fieldval_i` be the result of computing :math:`\packval_{\X{ft}_i}(\val_i))`. -9. Let :math:`\fieldval^\ast` the concatenation of all field values :math:`\fieldval_i`. +10. Let :math:`\fieldval^\ast` the concatenation of all field values :math:`\fieldval_i`. -10. Let :math:`\X{si}` be the :ref:`structure instance ` :math:`\{\SITYPE~\deftype, \SIFIELDS~\fieldval^\ast\}`. +11. Let :math:`\X{si}` be the :ref:`structure instance ` :math:`\{\SITYPE~\deftype, \SIFIELDS~\fieldval^\ast\}`. -11. Let :math:`a` be the length of :math:`S.\SSTRUCTS`. +12. Let :math:`a` be the length of :math:`S.\SSTRUCTS`. -12. Append :math:`\X{si}` to :math:`S.\SSTRUCTS`. +13. Append :math:`\X{si}` to :math:`S.\SSTRUCTS`. -13. Push the :ref:`structure reference ` :math:`\REFSTRUCTADDR~a` to the stack. +14. Push the :ref:`structure reference ` :math:`\REFSTRUCTADDR~a` to the stack. .. math:: \begin{array}{lcl@{\qquad}l} @@ -473,17 +488,19 @@ Reference Instructions :math:`\STRUCTNEWDEFAULT~x` ........................... -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +2. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. -2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. +3. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. -3. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is a :ref:`structure type `. +4. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is a :ref:`structure type `. -4. Let :math:`\TSTRUCT~\X{ft}^\ast` be the :ref:`expanded ` :ref:`structure type ` of :math:`\deftype`. +5. Let :math:`\TSTRUCT~\X{ft}^\ast` be the :ref:`expanded ` :ref:`structure type ` of :math:`\deftype`. -5. Let :math:`n` be the length of the :ref:`field type ` sequence :math:`\X{ft}^\ast`. +6. Let :math:`n` be the length of the :ref:`field type ` sequence :math:`\X{ft}^\ast`. -6. For every :ref:`field type ` :math:`\X{ft}_i` in :math:`\X{ft}^\ast`: +7. For every :ref:`field type ` :math:`\X{ft}_i` in :math:`\X{ft}^\ast`: a. Let :math:`t_i` be the :ref:`value type ` :math:`\unpacktype(\X{ft}_i)`. @@ -491,7 +508,7 @@ Reference Instructions c. Push the :ref:`value ` :math:`\default_{t_i}` to the stack. -7. Execute the instruction :math:`(\STRUCTNEW~x)`. +8. Execute the instruction :math:`(\STRUCTNEW~x)`. .. math:: \begin{array}{lcl@{\qquad}l} @@ -521,35 +538,37 @@ Reference Instructions :math:`\STRUCTGET\K{\_}\sx^?~x~y` ................................. -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +2. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. -2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. +3. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. -3. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is a :ref:`structure type ` with at least :math:`y + 1` fields. +4. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is a :ref:`structure type ` with at least :math:`y + 1` fields. -4. Let :math:`\TSTRUCT~\X{ft}^\ast` be the :ref:`expanded ` :ref:`structure type ` of :math:`\deftype`. +5. Let :math:`\TSTRUCT~\X{ft}^\ast` be the :ref:`expanded ` :ref:`structure type ` of :math:`\deftype`. -5. Let :math:`\X{ft}_y` be the :math:`y`-th :ref:`field type ` of :math:`\X{ft}^\ast`. +6. Let :math:`\X{ft}_y` be the :math:`y`-th :ref:`field type ` of :math:`\X{ft}^\ast`. -6. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. +7. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. -7. Pop the value :math:`\reff` from the stack. +8. Pop the value :math:`\reff` from the stack. -8. If :math:`\reff` is :math:`\REFNULL~t`, then: +9. If :math:`\reff` is :math:`\REFNULL~t`, then: a. Trap. -9. Assert: due to :ref:`validation `, a :math:`\reff` is a :ref:`structure reference `. +10. Assert: due to :ref:`validation `, a :math:`\reff` is a :ref:`structure reference `. -10. Let :math:`\REFSTRUCTADDR~a` be the reference value :math:`\reff`. +11. Let :math:`\REFSTRUCTADDR~a` be the reference value :math:`\reff`. -11. Assert: due to :ref:`validation `, the :ref:`structure instance ` :math:`S.\SSTRUCTS[a]` exists and has at least :math:`y + 1` fields. +12. Assert: due to :ref:`validation `, the :ref:`structure instance ` :math:`S.\SSTRUCTS[a]` exists and has at least :math:`y + 1` fields. -12. Let :math:`\fieldval` be the :ref:`field value ` :math:`S.\SSTRUCTS[a].\SIFIELDS[y]`. +13. Let :math:`\fieldval` be the :ref:`field value ` :math:`S.\SSTRUCTS[a].\SIFIELDS[y]`. -13. Let :math:`\val` be the result of computing :math:`\unpackval^{\sx^?}_{\X{ft}_y}(\fieldval))`. +14. Let :math:`\val` be the result of computing :math:`\unpackval^{\sx^?}_{\X{ft}_y}(\fieldval))`. -14. Push the value :math:`\val` to the stack. +15. Push the value :math:`\val` to the stack. .. math:: \begin{array}{lcl@{\qquad}l} @@ -568,37 +587,39 @@ Reference Instructions :math:`\STRUCTSET~x~y` ...................... -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. -2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. +2. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. -3. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is a :ref:`structure type ` with at least :math:`y + 1` fields. +3. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. -4. Let :math:`\TSTRUCT~\X{ft}^\ast` be the :ref:`expanded ` :ref:`structure type ` of :math:`\deftype`. +4. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is a :ref:`structure type ` with at least :math:`y + 1` fields. -5. Let :math:`\X{ft}_y` be the :math:`y`-th :ref:`field type ` of :math:`\X{ft}^\ast`. +5. Let :math:`\TSTRUCT~\X{ft}^\ast` be the :ref:`expanded ` :ref:`structure type ` of :math:`\deftype`. -6. Assert: due to :ref:`validation `, a :ref:`value ` is on the top of the stack. +6. Let :math:`\X{ft}_y` be the :math:`y`-th :ref:`field type ` of :math:`\X{ft}^\ast`. -7. Pop the value :math:`\val` from the stack. +7. Assert: due to :ref:`validation `, a :ref:`value ` is on the top of the stack. -8. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. +8. Pop the value :math:`\val` from the stack. -9. Pop the value :math:`\reff` from the stack. +9. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. -10. If :math:`\reff` is :math:`\REFNULL~t`, then: +10. Pop the value :math:`\reff` from the stack. + +11. If :math:`\reff` is :math:`\REFNULL~t`, then: a. Trap. -11. Assert: due to :ref:`validation `, a :math:`\reff` is a :ref:`structure reference `. +12. Assert: due to :ref:`validation `, a :math:`\reff` is a :ref:`structure reference `. -12. Let :math:`\REFSTRUCTADDR~a` be the reference value :math:`\reff`. +13. Let :math:`\REFSTRUCTADDR~a` be the reference value :math:`\reff`. -13. Assert: due to :ref:`validation `, the :ref:`structure instance ` :math:`S.\SSTRUCTS[a]` exists and has at least :math:`y + 1` fields. +14. Assert: due to :ref:`validation `, the :ref:`structure instance ` :math:`S.\SSTRUCTS[a]` exists and has at least :math:`y + 1` fields. -14. Let :math:`\fieldval` be the result of computing :math:`\packval_{\X{ft}_y}(\val))`. +15. Let :math:`\fieldval` be the result of computing :math:`\packval_{\X{ft}_y}(\val))`. -15. Replace the :ref:`field value ` :math:`S.\SSTRUCTS[a].\SIFIELDS[y]` with :math:`\fieldval`. +16. Replace the :ref:`field value ` :math:`S.\SSTRUCTS[a].\SIFIELDS[y]` with :math:`\fieldval`. .. math:: \begin{array}{lcl@{\qquad}l} @@ -652,25 +673,27 @@ Reference Instructions :math:`\ARRAYNEWDEFAULT~x` .......................... -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +2. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. -2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. +3. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. -3. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is an :ref:`array type `. +4. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is an :ref:`array type `. -4. Let :math:`\TARRAY~\X{ft}` be the :ref:`expanded ` :ref:`array type ` of :math:`\deftype`. +5. Let :math:`\TARRAY~\X{ft}` be the :ref:`expanded ` :ref:`array type ` of :math:`\deftype`. -5. Assert: due to :ref:`validation `, a :ref:`value ` of type :math:`\I32` is on the top of the stack. +6. Assert: due to :ref:`validation `, a :ref:`value ` of type :math:`\I32` is on the top of the stack. -6. Pop the value :math:`\I32.\CONST~n` from the stack. +7. Pop the value :math:`\I32.\CONST~n` from the stack. -7. Let :math:`t` be the :ref:`value type ` :math:`\unpacktype(\X{ft})`. +8. Let :math:`t` be the :ref:`value type ` :math:`\unpacktype(\X{ft})`. -8. Assert: due to :ref:`validation `, :math:`\default_t` is defined. +9. Assert: due to :ref:`validation `, :math:`\default_t` is defined. -9. Push the :ref:`value ` :math:`\default_t` to the stack :math:`n` times. +10. Push the :ref:`value ` :math:`\default_t` to the stack :math:`n` times. -10. Execute the instruction :math:`(\ARRAYNEWFIXED~x~n)`. +11. Execute the instruction :math:`(\ARRAYNEWFIXED~x~n)`. .. math:: \begin{array}{lcl@{\qquad}l} @@ -699,31 +722,33 @@ Reference Instructions :math:`\ARRAYNEWFIXED~x~n` .......................... -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +2. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. -2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. +3. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. -3. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is a :ref:`array type `. +4. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is a :ref:`array type `. -4. Let :math:`\TARRAY~\X{ft}` be the :ref:`expanded ` :ref:`array type ` of :math:`\deftype`. +5. Let :math:`\TARRAY~\X{ft}` be the :ref:`expanded ` :ref:`array type ` of :math:`\deftype`. -5. Assert: due to :ref:`validation `, :math:`n` :ref:`values ` are on the top of the stack. +6. Assert: due to :ref:`validation `, :math:`n` :ref:`values ` are on the top of the stack. -6. Pop the :math:`n` values :math:`\val^\ast` from the stack. +7. Pop the :math:`n` values :math:`\val^\ast` from the stack. -7. For every value :math:`\val_i` in :math:`\val^\ast`: +8. For every value :math:`\val_i` in :math:`\val^\ast`: a. Let :math:`\fieldval_i` be the result of computing :math:`\packval_{\X{ft}}(\val_i))`. -8. Let :math:`\fieldval^\ast` be the concatenation of all field values :math:`\fieldval_i`. +9. Let :math:`\fieldval^\ast` be the concatenation of all field values :math:`\fieldval_i`. -9. Let :math:`\X{ai}` be the :ref:`array instance ` :math:`\{\AITYPE~\deftype, \AIFIELDS~\fieldval^\ast\}`. +10. Let :math:`\X{ai}` be the :ref:`array instance ` :math:`\{\AITYPE~\deftype, \AIFIELDS~\fieldval^\ast\}`. -10. Let :math:`a` be the length of :math:`S.\SARRAYS`. +11. Let :math:`a` be the length of :math:`S.\SARRAYS`. -11. Append :math:`\X{ai}` to :math:`S.\SARRAYS`. +12. Append :math:`\X{ai}` to :math:`S.\SARRAYS`. -12. Push the :ref:`array reference ` :math:`\REFARRAYADDR~a` to the stack. +13. Push the :ref:`array reference ` :math:`\REFARRAYADDR~a` to the stack. .. math:: \begin{array}{lcl@{\qquad}l} @@ -742,41 +767,43 @@ Reference Instructions :math:`\ARRAYNEWDATA~x~y` ......................... -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. -2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. +2. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. -3. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is an :ref:`array type `. +3. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. -4. Let :math:`\TARRAY~\X{ft}` be the :ref:`expanded ` :ref:`array type ` of :math:`\deftype`. +4. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is an :ref:`array type `. -5. Assert: due to :ref:`validation `, the :ref:`data address ` :math:`F.\AMODULE.\MIDATAS[y]` exists. +5. Let :math:`\TARRAY~\X{ft}` be the :ref:`expanded ` :ref:`array type ` of :math:`\deftype`. -6. Let :math:`\X{da}` be the :ref:`data address ` :math:`F.\AMODULE.\MIDATAS[y]`. +6. Assert: due to :ref:`validation `, the :ref:`data address ` :math:`F.\AMODULE.\MIDATAS[y]` exists. -7. Assert: due to :ref:`validation `, the :ref:`data instance ` :math:`S.\SDATAS[\X{da}]` exists. +7. Let :math:`\X{da}` be the :ref:`data address ` :math:`F.\AMODULE.\MIDATAS[y]`. -8. Let :math:`\datainst` be the :ref:`data instance ` :math:`S.\SDATAS[\X{da}]`. +8. Assert: due to :ref:`validation `, the :ref:`data instance ` :math:`S.\SDATAS[\X{da}]` exists. -9. Assert: due to :ref:`validation `, two :ref:`values ` of type :math:`\I32` are on the top of the stack. +9. Let :math:`\datainst` be the :ref:`data instance ` :math:`S.\SDATAS[\X{da}]`. -10. Pop the value :math:`\I32.\CONST~n` from the stack. +10. Assert: due to :ref:`validation `, two :ref:`values ` of type :math:`\I32` are on the top of the stack. -11. Pop the value :math:`\I32.\CONST~s` from the stack. +11. Pop the value :math:`\I32.\CONST~n` from the stack. + +12. Pop the value :math:`\I32.\CONST~s` from the stack. -12. Assert: due to :ref:`validation `, the :ref:`field type ` :math:`\X{ft}` has a defined :ref:`bit width `. +13. Assert: due to :ref:`validation `, the :ref:`field type ` :math:`\X{ft}` has a defined :ref:`bit width `. -13. Let :math:`z` be the :ref:`bit width ` of :ref:`field type ` :math:`\X{ft}` divided by eight. +14. Let :math:`z` be the :ref:`bit width ` of :ref:`field type ` :math:`\X{ft}` divided by eight. -14. If the sum of :math:`s` and :math:`n` times :math:`z` is larger than the length of :math:`\datainst.\DIDATA`, then: +15. If the sum of :math:`s` and :math:`n` times :math:`z` is larger than the length of :math:`\datainst.\DIDATA`, then: a. Trap. -15. Let :math:`b^\ast` be the :ref:`byte ` sequence :math:`\datainst.\DIDATA[s \slice n \cdot z]`. +16. Let :math:`b^\ast` be the :ref:`byte ` sequence :math:`\datainst.\DIDATA[s \slice n \cdot z]`. -16. Let :math:`t` be the :ref:`value type ` :math:`\unpacktype(\X{ft})`. +17. Let :math:`t` be the :ref:`value type ` :math:`\unpacktype(\X{ft})`. -17. For each consecutive subsequence :math:`{b'}^n` of :math:`b^\ast`: +18. For each consecutive subsequence :math:`{b'}^n` of :math:`b^\ast`: a. Assert: due to :ref:`validation `, :math:`\bytes_{\X{ft}}` is defined. @@ -784,7 +811,7 @@ Reference Instructions c. Push the value :math:`t.\CONST~c_i` to the stack. -18. Execute the instruction :math:`(\ARRAYNEWFIXED~x~n)`. +19. Execute the instruction :math:`(\ARRAYNEWFIXED~x~n)`. .. math:: ~\\[-1ex] @@ -811,29 +838,31 @@ Reference Instructions :math:`\ARRAYNEWELEM~x~y` ......................... -1. Assert: due to :ref:`validation `, the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[y]` exists. +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. -2. Let :math:`\X{ea}` be the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[y]`. +2. Assert: due to :ref:`validation `, the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[y]` exists. -3. Assert: due to :ref:`validation `, the :ref:`element instance ` :math:`S.\SELEMS[\X{ea}]` exists. +3. Let :math:`\X{ea}` be the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[y]`. -4. Let :math:`\eleminst` be the :ref:`element instance ` :math:`S.\SELEMS[\X{ea}]`. +4. Assert: due to :ref:`validation `, the :ref:`element instance ` :math:`S.\SELEMS[\X{ea}]` exists. -5. Assert: due to :ref:`validation `, two :ref:`values ` of type :math:`\I32` are on the top of the stack. +5. Let :math:`\eleminst` be the :ref:`element instance ` :math:`S.\SELEMS[\X{ea}]`. -6. Pop the value :math:`(\I32.\CONST~n)` from the stack. +6. Assert: due to :ref:`validation `, two :ref:`values ` of type :math:`\I32` are on the top of the stack. -7. Pop the value :math:`(\I32.\CONST~s)` from the stack. +7. Pop the value :math:`(\I32.\CONST~n)` from the stack. -8. If the sum of :math:`s` and :math:`n` is larger than the length of :math:`\eleminst.\EIELEM`, then: +8. Pop the value :math:`(\I32.\CONST~s)` from the stack. + +9. If the sum of :math:`s` and :math:`n` is larger than the length of :math:`\eleminst.\EIELEM`, then: a. Trap. -9. Let :math:`\reff^\ast` be the :ref:`reference ` sequence :math:`\eleminst.\EIELEM[s \slice n]`. +10. Let :math:`\reff^\ast` be the :ref:`reference ` sequence :math:`\eleminst.\EIELEM[s \slice n]`. -10. Push the references :math:`\reff^\ast` to the stack. +11. Push the references :math:`\reff^\ast` to the stack. -11. Execute the instruction :math:`(\ARRAYNEWFIXED~x~n)`. +12. Execute the instruction :math:`(\ARRAYNEWFIXED~x~n)`. .. math:: ~\\[-1ex] @@ -856,41 +885,43 @@ Reference Instructions :math:`\ARRAYGET\K{\_}\sx^?~x` .............................. -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. -2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. +2. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. -3. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is an :ref:`array type `. +3. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. -4. Let :math:`\TARRAY~\X{ft}` be the :ref:`expanded ` :ref:`array type ` of :math:`\deftype`. +4. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is an :ref:`array type `. -5. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. +5. Let :math:`\TARRAY~\X{ft}` be the :ref:`expanded ` :ref:`array type ` of :math:`\deftype`. -6. Pop the value :math:`\I32.\CONST~i` from the stack. +6. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. -7. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. +7. Pop the value :math:`\I32.\CONST~i` from the stack. -8. Pop the value :math:`\reff` from the stack. +8. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. -9. If :math:`\reff` is :math:`\REFNULL~t`, then: +9. Pop the value :math:`\reff` from the stack. + +10. If :math:`\reff` is :math:`\REFNULL~t`, then: a. Trap. -10. Assert: due to :ref:`validation `, :math:`\reff` is an :ref:`array reference `. +11. Assert: due to :ref:`validation `, :math:`\reff` is an :ref:`array reference `. -11. Let :math:`\REFARRAYADDR~a` be the reference value :math:`\reff`. +12. Let :math:`\REFARRAYADDR~a` be the reference value :math:`\reff`. -12. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a]` exists. +13. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a]` exists. -13. If :math:`n` is larger than or equal to the length of :math:`S.\SARRAYS[a].\AIFIELDS`, then: +14. If :math:`n` is larger than or equal to the length of :math:`S.\SARRAYS[a].\AIFIELDS`, then: a. Trap. -14. Let :math:`\fieldval` be the :ref:`field value ` :math:`S.\SARRAYS[a].\AIFIELDS[i]`. +15. Let :math:`\fieldval` be the :ref:`field value ` :math:`S.\SARRAYS[a].\AIFIELDS[i]`. -15. Let :math:`\val` be the result of computing :math:`\unpackval^{\sx^?}_{\X{ft}}(\fieldval))`. +16. Let :math:`\val` be the result of computing :math:`\unpackval^{\sx^?}_{\X{ft}}(\fieldval))`. -16. Push the value :math:`\val` to the stack. +17. Push the value :math:`\val` to the stack. .. math:: ~\\[-1ex] @@ -915,43 +946,45 @@ Reference Instructions :math:`\ARRAYSET~x` ................... -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. -2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. +2. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. -3. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is an :ref:`array type `. +3. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. -4. Let :math:`\TARRAY~\X{ft}` be the :ref:`expanded ` :ref:`array type ` of :math:`\deftype`. +4. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is an :ref:`array type `. -5. Assert: due to :ref:`validation `, a :ref:`value ` is on the top of the stack. +5. Let :math:`\TARRAY~\X{ft}` be the :ref:`expanded ` :ref:`array type ` of :math:`\deftype`. -6. Pop the value :math:`\val` from the stack. +6. Assert: due to :ref:`validation `, a :ref:`value ` is on the top of the stack. -7. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. +7. Pop the value :math:`\val` from the stack. -8. Pop the value :math:`\I32.\CONST~i` from the stack. +8. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. -9. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. +9. Pop the value :math:`\I32.\CONST~i` from the stack. -10. Pop the value :math:`\reff` from the stack. +10. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. -11. If :math:`\reff` is :math:`\REFNULL~t`, then: +11. Pop the value :math:`\reff` from the stack. + +12. If :math:`\reff` is :math:`\REFNULL~t`, then: a. Trap. -12. Assert: due to :ref:`validation `, :math:`\reff` is an :ref:`array reference `. +13. Assert: due to :ref:`validation `, :math:`\reff` is an :ref:`array reference `. -13. Let :math:`\REFARRAYADDR~a` be the reference value :math:`\reff`. +14. Let :math:`\REFARRAYADDR~a` be the reference value :math:`\reff`. -14. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a]` exists. +15. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a]` exists. -15. If :math:`n` is larger than or equal to the length of :math:`S.\SARRAYS[a].\AIFIELDS`, then: +16. If :math:`n` is larger than or equal to the length of :math:`S.\SARRAYS[a].\AIFIELDS`, then: a. Trap. -16. Let :math:`\fieldval` be the result of computing :math:`\packval_{\X{ft}}(\val))`. +17. Let :math:`\fieldval` be the result of computing :math:`\packval_{\X{ft}}(\val))`. -17. Replace the :ref:`field value ` :math:`S.\SARRAYS[a].\AIFIELDS[i]` with :math:`\fieldval`. +18. Replace the :ref:`field value ` :math:`S.\SARRAYS[a].\AIFIELDS[i]` with :math:`\fieldval`. .. math:: ~\\[-1ex] @@ -1092,67 +1125,69 @@ Reference Instructions :math:`\ARRAYCOPY~x~y` ...................... -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[y]` exists. +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +2. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[y]` exists. -2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[y]`. +3. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[y]`. -3. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is an :ref:`array type `. +4. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is an :ref:`array type `. -4. Let :math:`\TARRAY~\mut~\X{st}` be the :ref:`expanded ` :ref:`array type ` :math:`\deftype`. +5. Let :math:`\TARRAY~\mut~\X{st}` be the :ref:`expanded ` :ref:`array type ` :math:`\deftype`. -5. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. +6. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. -6. Pop the value :math:`\I32.\CONST~n` from the stack. +7. Pop the value :math:`\I32.\CONST~n` from the stack. -7. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. +8. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. -8. Pop the value :math:`\I32.\CONST~s` from the stack. +9. Pop the value :math:`\I32.\CONST~s` from the stack. -9. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~y)` is on the top of the stack. +10. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~y)` is on the top of the stack. -10. Pop the value :math:`\reff_2` from the stack. +11. Pop the value :math:`\reff_2` from the stack. -11. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. +12. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. -12. Pop the value :math:`\I32.\CONST~d` from the stack. +13. Pop the value :math:`\I32.\CONST~d` from the stack. -13. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. +14. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. -14. Pop the value :math:`\reff_1` from the stack. +15. Pop the value :math:`\reff_1` from the stack. -15. If :math:`\reff_1` is :math:`\REFNULL~t`, then: +16. If :math:`\reff_1` is :math:`\REFNULL~t`, then: a. Trap. -16. Assert: due to :ref:`validation `, :math:`\reff_1` is an :ref:`array reference `. +17. Assert: due to :ref:`validation `, :math:`\reff_1` is an :ref:`array reference `. -17. Let :math:`\REFARRAYADDR~a_1` be the reference value :math:`\reff_1`. +18. Let :math:`\REFARRAYADDR~a_1` be the reference value :math:`\reff_1`. -18. If :math:`\reff_2` is :math:`\REFNULL~t`, then: +19. If :math:`\reff_2` is :math:`\REFNULL~t`, then: a. Trap. -19. Assert: due to :ref:`validation `, :math:`\reff_2` is an :ref:`array reference `. +20. Assert: due to :ref:`validation `, :math:`\reff_2` is an :ref:`array reference `. -20. Let :math:`\REFARRAYADDR~a_2` be the reference value :math:`\reff_2`. +21. Let :math:`\REFARRAYADDR~a_2` be the reference value :math:`\reff_2`. -21. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_1]` exists. +22. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_1]` exists. -22. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_2]` exists. +23. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_2]` exists. -23. If :math:`d + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_1].\AIFIELDS`, then: +24. If :math:`d + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_1].\AIFIELDS`, then: a. Trap. -24. If :math:`s + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_2].\AIFIELDS`, then: +25. If :math:`s + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_2].\AIFIELDS`, then: a. Trap. -25. If :math:`n = 0`, then: +26. If :math:`n = 0`, then: a. Return. -26. If :math:`d \leq s`, then: +27. If :math:`d \leq s`, then: a. Push the value :math:`\REFARRAYADDR~a_1` to the stack. @@ -1178,7 +1213,7 @@ Reference Instructions l. Push the value :math:`\I32.\CONST~(s+1)` to the stack. -27. Else: +28. Else: a. Push the value :math:`\REFARRAYADDR~a_1` to the stack. @@ -1204,24 +1239,24 @@ Reference Instructions l. Push the value :math:`\I32.\CONST~s` to the stack. -28. Push the value :math:`\I32.\CONST~(n-1)` to the stack. +29. Push the value :math:`\I32.\CONST~(n-1)` to the stack. -29. Execute the instruction :math:`\ARRAYCOPY~x~y`. +30. Execute the instruction :math:`\ARRAYCOPY~x~y`. .. math:: ~\\[-1ex] \begin{array}{l} - S; (\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) + S; F; (\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) + S; F; (\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) + S; F; (\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\ARRAYCOPY~x~y) \quad\stepto \\ \quad \begin{array}[t]{@{}l@{}} @@ -1233,7 +1268,7 @@ Reference Instructions \\ \qquad (\otherwise, \iff d \leq s \land F.\AMODULE.\MITYPES[y] = \TARRAY~\mut~\X{st}) \\ \\[1ex] - S; (\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\ARRAYCOPY~x~y) + S; F; (\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\ARRAYCOPY~x~y) \quad\stepto \\ \quad \begin{array}[t]{@{}l@{}} @@ -1245,9 +1280,9 @@ Reference Instructions \\ \qquad (\otherwise, \iff d > s \land F.\AMODULE.\MITYPES[y] = \TARRAY~\mut~\X{st}) \\ \\[1ex] - S; (\REFNULL~t)~(\I32.\CONST~d)~\val~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \quad\stepto\quad \TRAP + S; F; (\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 + S; F; \val~(\I32.\CONST~d)~(\REFNULL~t)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \quad\stepto\quad \TRAP \end{array} Where: @@ -1266,85 +1301,87 @@ Where: :math:`\ARRAYINITDATA~x~y` .......................... -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +2. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. -2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. +3. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. -3. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is an :ref:`array type `. +4. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is an :ref:`array type `. -4. Let :math:`\TARRAY~\X{ft}` be the :ref:`expanded ` :ref:`array type ` :math:`\deftype`. +5. Let :math:`\TARRAY~\X{ft}` be the :ref:`expanded ` :ref:`array type ` :math:`\deftype`. -5. Assert: due to :ref:`validation `, the :ref:`data address ` :math:`F.\AMODULE.\MIDATAS[y]` exists. +6. Assert: due to :ref:`validation `, the :ref:`data address ` :math:`F.\AMODULE.\MIDATAS[y]` exists. -6. Let :math:`\X{da}` be the :ref:`data address ` :math:`F.\AMODULE.\MIDATAS[y]`. +7. Let :math:`\X{da}` be the :ref:`data address ` :math:`F.\AMODULE.\MIDATAS[y]`. -7. Assert: due to :ref:`validation `, the :ref:`data instance ` :math:`S.\SDATAS[\X{da}]` exists. +8. Assert: due to :ref:`validation `, the :ref:`data instance ` :math:`S.\SDATAS[\X{da}]` exists. -8. Let :math:`\datainst` be the :ref:`data instance ` :math:`S.\SDATAS[\X{da}]`. +9. Let :math:`\datainst` be the :ref:`data instance ` :math:`S.\SDATAS[\X{da}]`. -9. Assert: due to :ref:`validation `, three values of type :math:`\I32` are on the top of the stack. +10. Assert: due to :ref:`validation `, three values of type :math:`\I32` are on the top of the stack. -10. Pop the value :math:`\I32.\CONST~n` from the stack. +11. Pop the value :math:`\I32.\CONST~n` from the stack. -11. Pop the value :math:`\I32.\CONST~s` from the stack. +12. Pop the value :math:`\I32.\CONST~s` from the stack. -12. Pop the value :math:`\I32.\CONST~d` from the stack. +13. Pop the value :math:`\I32.\CONST~d` from the stack. -13. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. +14. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. -14. Pop the value :math:`\reff` from the stack. +15. Pop the value :math:`\reff` from the stack. -15. If :math:`\reff` is :math:`\REFNULL~t`, then: +16. If :math:`\reff` is :math:`\REFNULL~t`, then: a. Trap. -16. Assert: due to :ref:`validation `, :math:`\reff` is an :ref:`array reference `. +17. Assert: due to :ref:`validation `, :math:`\reff` is an :ref:`array reference `. -17. Let :math:`\REFARRAYADDR~a` be the reference value :math:`\reff`. +18. Let :math:`\REFARRAYADDR~a` be the reference value :math:`\reff`. -18. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a]` exists. +19. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a]` exists. -19. If :math:`d + n` is larger than or equal to the length of :math:`S.\SARRAYS[a].\AIFIELDS`, then: +20. If :math:`d + n` is larger than or equal to the length of :math:`S.\SARRAYS[a].\AIFIELDS`, then: a. Trap. -20. Assert: due to :ref:`validation `, the :ref:`field type ` :math:`\X{ft}` has a defined :ref:`bit width `. +21. Assert: due to :ref:`validation `, the :ref:`field type ` :math:`\X{ft}` has a defined :ref:`bit width `. -21. Let :math:`z` be the :ref:`bit width ` of :ref:`field type ` :math:`\X{ft}` divided by eight. +22. Let :math:`z` be the :ref:`bit width ` of :ref:`field type ` :math:`\X{ft}` divided by eight. -22. If the sum of :math:`s` and :math:`n` times :math:`z` is larger than the length of :math:`\datainst.\DIDATA`, then: +23. If the sum of :math:`s` and :math:`n` times :math:`z` is larger than the length of :math:`\datainst.\DIDATA`, then: a. Trap. -23. If :math:`n = 0`, then: +24. If :math:`n = 0`, then: a. Return. -24. Let :math:`b^\ast` be the :ref:`byte ` sequence :math:`\datainst.\DIDATA[s \slice z]`. +25. Let :math:`b^\ast` be the :ref:`byte ` sequence :math:`\datainst.\DIDATA[s \slice z]`. -25. Let :math:`t` be the :ref:`value type ` :math:`\unpacktype(\X{ft})`. +26. Let :math:`t` be the :ref:`value type ` :math:`\unpacktype(\X{ft})`. -26. Assert: due to :ref:`validation `, :math:`\bytes_{\X{ft}}` is defined. +27. Assert: due to :ref:`validation `, :math:`\bytes_{\X{ft}}` is defined. -27. Let :math:`c` be the constant for which :math:`\bytes_{\X{ft}}(c)` is :math:`b^\ast`. +28. Let :math:`c` be the constant for which :math:`\bytes_{\X{ft}}(c)` is :math:`b^\ast`. -28. Push the value :math:`\REFARRAYADDR~a` to the stack. +29. Push the value :math:`\REFARRAYADDR~a` to the stack. -29. Push the value :math:`\I32.\CONST~d` to the stack. +30. Push the value :math:`\I32.\CONST~d` to the stack. -30. Push the value :math:`t.\CONST~c` to the stack. +31. Push the value :math:`t.\CONST~c` to the stack. -31. Execute the instruction :math:`\ARRAYSET~x`. +32. Execute the instruction :math:`\ARRAYSET~x`. -32. Push the value :math:`\REFARRAYADDR~a` to the stack. +33. Push the value :math:`\REFARRAYADDR~a` to the stack. -33. Push the value :math:`\I32.\CONST~(d+1)` to the stack. +34. Push the value :math:`\I32.\CONST~(d+1)` to the stack. -34. Push the value :math:`\I32.\CONST~(s+z)` to the stack. +35. Push the value :math:`\I32.\CONST~(s+z)` to the stack. -35. Push the value :math:`\I32.\CONST~(n-1)` to the stack. +36. Push the value :math:`\I32.\CONST~(n-1)` to the stack. -36. Execute the instruction :math:`\ARRAYINITDATA~x~y`. +37. Execute the instruction :math:`\ARRAYINITDATA~x~y`. .. math:: ~\\[-1ex] @@ -1385,75 +1422,77 @@ Where: :math:`\ARRAYINITELEM~x~y` .......................... -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +2. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. -2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. +3. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. -3. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is an :ref:`array type `. +4. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is an :ref:`array type `. -4. Let :math:`\TARRAY~\X{ft}` be the :ref:`expanded ` :ref:`array type ` :math:`\deftype`. +5. Let :math:`\TARRAY~\X{ft}` be the :ref:`expanded ` :ref:`array type ` :math:`\deftype`. -5. Assert: due to :ref:`validation `, the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[y]` exists. +6. Assert: due to :ref:`validation `, the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[y]` exists. -6. Let :math:`\X{ea}` be the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[y]`. +7. Let :math:`\X{ea}` be the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[y]`. -7. Assert: due to :ref:`validation `, the :ref:`element instance ` :math:`S.\SELEMS[\X{ea}]` exists. +8. Assert: due to :ref:`validation `, the :ref:`element instance ` :math:`S.\SELEMS[\X{ea}]` exists. -8. Let :math:`\eleminst` be the :ref:`element instance ` :math:`S.\SELEMS[\X{ea}]`. +9. Let :math:`\eleminst` be the :ref:`element instance ` :math:`S.\SELEMS[\X{ea}]`. -9. Assert: due to :ref:`validation `, three values of type :math:`\I32` are on the top of the stack. +10. Assert: due to :ref:`validation `, three values of type :math:`\I32` are on the top of the stack. -10. Pop the value :math:`\I32.\CONST~n` from the stack. +11. Pop the value :math:`\I32.\CONST~n` from the stack. -11. Pop the value :math:`\I32.\CONST~s` from the stack. +12. Pop the value :math:`\I32.\CONST~s` from the stack. -12. Pop the value :math:`\I32.\CONST~d` from the stack. +13. Pop the value :math:`\I32.\CONST~d` from the stack. -13. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. +14. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. -14. Pop the value :math:`\reff` from the stack. +15. Pop the value :math:`\reff` from the stack. -15. If :math:`\reff` is :math:`\REFNULL~t`, then: +16. If :math:`\reff` is :math:`\REFNULL~t`, then: a. Trap. -16. Assert: due to :ref:`validation `, :math:`\reff` is an :ref:`array reference `. +17. Assert: due to :ref:`validation `, :math:`\reff` is an :ref:`array reference `. -17. Let :math:`\REFARRAYADDR~a` be the reference value :math:`\reff`. +18. Let :math:`\REFARRAYADDR~a` be the reference value :math:`\reff`. -18. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a]` exists. +19. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a]` exists. -19. If :math:`d + n` is larger than or equal to the length of :math:`S.\SARRAYS[a].\AIFIELDS`, then: +20. If :math:`d + n` is larger than or equal to the length of :math:`S.\SARRAYS[a].\AIFIELDS`, then: a. Trap. -20. If :math:`s + n` is larger than or equal to the length of :math:`\eleminst.\EIELEM`, then: +21. If :math:`s + n` is larger than or equal to the length of :math:`\eleminst.\EIELEM`, then: a. Trap. -21. If :math:`n = 0`, then: +22. If :math:`n = 0`, then: a. Return. -22. Let :math:`\reff'` be the :ref:`reference value ` :math:`\eleminst.\EIELEM[s]`. +23. Let :math:`\reff'` be the :ref:`reference value ` :math:`\eleminst.\EIELEM[s]`. -23. Push the value :math:`\REFARRAYADDR~a` to the stack. +24. Push the value :math:`\REFARRAYADDR~a` to the stack. -24. Push the value :math:`\I32.\CONST~d` to the stack. +25. Push the value :math:`\I32.\CONST~d` to the stack. -25. Push the value :math:`\reff'` to the stack. +26. Push the value :math:`\reff'` to the stack. -26. Execute the instruction :math:`\ARRAYSET~x`. +27. Execute the instruction :math:`\ARRAYSET~x`. -27. Push the value :math:`\REFARRAYADDR~a` to the stack. +28. Push the value :math:`\REFARRAYADDR~a` to the stack. -28. Push the value :math:`\I32.\CONST~(d+1)` to the stack. +29. Push the value :math:`\I32.\CONST~(d+1)` to the stack. -29. Push the value :math:`\I32.\CONST~(s+1)` to the stack. +30. Push the value :math:`\I32.\CONST~(s+1)` to the stack. -30. Push the value :math:`\I32.\CONST~(n-1)` to the stack. +31. Push the value :math:`\I32.\CONST~(n-1)` to the stack. -31. Execute the instruction :math:`\ARRAYINITELEM~x~y`. +32. Execute the instruction :math:`\ARRAYINITELEM~x~y`. .. math:: ~\\[-1ex] diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index e0f0753734..f7b17be31c 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -47,7 +47,7 @@ Any of the aformentioned references can furthermore be wrapped up as an *externa \production{vector} & \vecc &::=& \V128.\CONST~\i128 \\ \production{reference} & \reff &::=& - \REFNULL~t \\&&|& + \REFNULL~(\absheaptype~|~\deftype) \\&&|& \REFI31NUM~\u31 \\&&|& \REFSTRUCTADDR~\structaddr \\&&|& \REFARRAYADDR~\arrayaddr \\&&|& diff --git a/interpreter/dune b/interpreter/dune index 9a853921db..e221bea7a1 100644 --- a/interpreter/dune +++ b/interpreter/dune @@ -6,7 +6,8 @@ ; Wasm REPL every time in all the dependencies. ; We exclude the 'wast' module as it is only used for the JS build. ; 'smallint' is a separate test module. - (modules :standard \ main wasm smallint wast)) + (modules :standard \ main wasm smallint wast) + (libraries menhirLib)) (executable (public_name wasm) @@ -43,7 +44,7 @@ (chdir %{workspace_root} (run %{bin:ocamllex} -ml -q -o %{target} %{deps})))) - (ocamlyacc + (menhir (modules parser))) (env diff --git a/interpreter/dune-project b/interpreter/dune-project index 0d15135d31..8392b339f5 100644 --- a/interpreter/dune-project +++ b/interpreter/dune-project @@ -3,6 +3,8 @@ (name wasm) (generate_opam_files true) +(using menhir 2.1) +(implicit_transitive_deps false) (license Apache-2.0) @@ -17,4 +19,5 @@ (synopsis "Library to read and write WebAssembly (Wasm) files and manipulate their AST") (tags (wasm webassembly spec interpreter)) (depends - (ocaml (>= 4.12)))) + (ocaml (>= 4.12)) + (menhir (>= 20220210)))) diff --git a/interpreter/jslib/wast.ml b/interpreter/jslib/wast.ml index 2f5a3d65a1..bc7edef074 100644 --- a/interpreter/jslib/wast.ml +++ b/interpreter/jslib/wast.ml @@ -4,12 +4,12 @@ open Wasm open Js_of_ocaml -let _ = +let () = Js.export "WebAssemblyText" (object%js (_self) method encode (s : Js.js_string Js.t) : (Typed_array.arrayBuffer Js.t) = - let def = Parse.string_to_definition (Js.to_string s) in + let _, def = Parse.Module.parse_string (Js.to_string s) in let bs = match def.Source.it with | Script.Textual m -> Encode.encode m diff --git a/interpreter/script/js.ml b/interpreter/script/js.ml index 1ac6e6db8b..3ba0abae9f 100644 --- a/interpreter/script/js.ml +++ b/interpreter/script/js.ml @@ -545,7 +545,8 @@ let rec of_definition def = | Textual m -> of_bytes (Encode.encode m) | Encoded (_, bs) -> of_bytes bs | Quoted (_, s) -> - try of_definition (Parse.string_to_definition s) with Parse.Syntax _ -> + try of_definition (snd (Parse.Module.parse_string s)) + with Parse.Syntax _ -> of_bytes "" let of_wrapper mods x_opt name wrap_action wrap_assertion at = @@ -620,7 +621,7 @@ let of_command mods cmd = match def.it with | Textual m -> m | Encoded (_, bs) -> Decode.decode "binary" bs - | Quoted (_, s) -> unquote (Parse.string_to_definition s) + | Quoted (_, s) -> unquote (snd (Parse.Module.parse_string s)) in bind mods x_opt (unquote def); "let " ^ current_var mods ^ " = instance(" ^ of_definition def ^ ");\n" ^ (if x_opt = None then "" else diff --git a/interpreter/script/run.ml b/interpreter/script/run.ml index 9a11c0aa72..d7576df9cb 100644 --- a/interpreter/script/run.ml +++ b/interpreter/script/run.ml @@ -119,17 +119,20 @@ let input_from get_script run = | Assert (at, msg) -> error at "assertion failure" msg | Abort _ -> false -let input_script start name lexbuf run = - input_from (fun _ -> Parse.parse name lexbuf start) run +let input_script name lexbuf run = + input_from (fun () -> Parse.Script.parse name lexbuf) run + +let input_script1 name lexbuf run = + input_from (fun () -> Parse.Script1.parse name lexbuf) run let input_sexpr name lexbuf run = - input_from (fun _ -> - let var_opt, def = Parse.parse name lexbuf Parse.Module in + input_from (fun () -> + let var_opt, def = Parse.Module.parse name lexbuf in [Module (var_opt, def) @@ no_region]) run let input_binary name buf run = let open Source in - input_from (fun _ -> + input_from (fun () -> [Module (None, Encoded (name, buf) @@ no_region) @@ no_region]) run let input_sexpr_file input file run = @@ -163,8 +166,8 @@ let input_file file run = dispatch_file_ext input_binary_file (input_sexpr_file input_sexpr) - (input_sexpr_file (input_script Parse.Script)) - (input_sexpr_file (input_script Parse.Script)) + (input_sexpr_file input_script) + (input_sexpr_file input_script) input_js_file file run @@ -172,7 +175,7 @@ let input_string string run = trace ("Running (\"" ^ String.escaped string ^ "\")..."); let lexbuf = Lexing.from_string string in trace "Parsing..."; - input_script Parse.Script "string" lexbuf run + input_script "string" lexbuf run (* Interactive *) @@ -196,7 +199,7 @@ let lexbuf_stdin buf len = let input_stdin run = let lexbuf = Lexing.from_function lexbuf_stdin in let rec loop () = - let success = input_script Parse.Script1 "stdin" lexbuf run in + let success = input_script1 "stdin" lexbuf run in if not success then Lexing.flush_input lexbuf; if Lexing.(lexbuf.lex_curr_pos >= lexbuf.lex_buffer_len - 1) then continuing := false; @@ -316,7 +319,7 @@ let rec run_definition def : Ast.module_ = Decode.decode name bs | Quoted (_, s) -> trace "Parsing quote..."; - let def' = Parse.string_to_definition s in + let _, def' = Parse.Module.parse_string s in run_definition def' let run_action act : Value.t list = diff --git a/interpreter/script/script.ml b/interpreter/script/script.ml index 7b73aec19c..088038e2f9 100644 --- a/interpreter/script/script.ml +++ b/interpreter/script/script.ml @@ -66,8 +66,6 @@ and meta' = and script = command list -exception Syntax of Source.region * string - let () = let type_of_ref' = !Value.type_of_ref' in diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml index 812eed5672..94a20ce2a3 100644 --- a/interpreter/text/arrange.ml +++ b/interpreter/text/arrange.ml @@ -803,14 +803,14 @@ let definition mode x_opt def = match def.it with | Textual m -> m | Encoded (_, bs) -> Decode.decode "" bs - | Quoted (_, s) -> unquote (Parse.string_to_definition s) + | Quoted (_, s) -> unquote (snd (Parse.Module.parse_string s)) in module_with_var_opt x_opt (unquote def) | `Binary -> let rec unquote def = match def.it with | Textual m -> Encode.encode m | Encoded (_, bs) -> Encode.encode (Decode.decode "" bs) - | Quoted (_, s) -> unquote (Parse.string_to_definition s) + | Quoted (_, s) -> unquote (snd (Parse.Module.parse_string s)) in binary_module_with_var_opt x_opt (unquote def) | `Original -> match def.it with diff --git a/interpreter/text/lexer.mll b/interpreter/text/lexer.mll index 50f1af7cfe..bbcee6269d 100644 --- a/interpreter/text/lexer.mll +++ b/interpreter/text/lexer.mll @@ -14,7 +14,7 @@ let region lexbuf = let right = convert_pos (Lexing.lexeme_end_p lexbuf) in {left = left; right = right} -let error lexbuf msg = raise (Script.Syntax (region lexbuf, msg)) +let error lexbuf msg = raise (Parse_error.Syntax (region lexbuf, msg)) let error_nest start lexbuf msg = lexbuf.Lexing.lex_start_p <- start; error lexbuf msg diff --git a/interpreter/text/parse.ml b/interpreter/text/parse.ml index e09955525c..14da6079ac 100644 --- a/interpreter/text/parse.ml +++ b/interpreter/text/parse.ml @@ -1,32 +1,52 @@ -type 'a start = - | Module : (Script.var option * Script.definition) start - | Script : Script.script start - | Script1 : Script.script start - -exception Syntax = Script.Syntax - -let parse' name lexbuf start = - lexbuf.Lexing.lex_curr_p <- - {lexbuf.Lexing.lex_curr_p with Lexing.pos_fname = name}; - try start Lexer.token lexbuf - with Syntax (region, s) -> - let region' = if region <> Source.no_region then region else - {Source.left = Lexer.convert_pos lexbuf.Lexing.lex_start_p; - Source.right = Lexer.convert_pos lexbuf.Lexing.lex_curr_p} in - raise (Syntax (region', s)) - -let parse (type a) name lexbuf : a start -> a = function - | Module -> parse' name lexbuf Parser.module1 - | Script -> parse' name lexbuf Parser.script - | Script1 -> parse' name lexbuf Parser.script1 - -let string_to start s = - let lexbuf = Lexing.from_string s in - parse "string" lexbuf start - -let string_to_script s = string_to Script s -let string_to_definition s = snd (string_to Module s) -let string_to_module s = - match (string_to_definition s).Source.it with - | Script.Textual m -> m - | _ -> assert false +exception Syntax = Parse_error.Syntax + +module type S = +sig + type t + val parse : string -> Lexing.lexbuf -> t + val parse_file : string -> t + val parse_string : string -> t + val parse_channel : in_channel -> t +end + +let provider buf () = + let tok = Lexer.token buf in + let start = Lexing.lexeme_start_p buf in + let stop = Lexing.lexeme_end_p buf in + tok, start, stop + +let convert_pos buf = + { Source.left = Lexer.convert_pos buf.Lexing.lex_start_p; + Source.right = Lexer.convert_pos buf.Lexing.lex_curr_p + } + +let make (type a) (start : _ -> _ -> a) : (module S with type t = a) = + (module struct + type t = a + + let parse name buf = + Lexing.set_filename buf name; + try + MenhirLib.Convert.Simplified.traditional2revised start (provider buf) + with + | Parser.Error -> + raise (Syntax (convert_pos buf, "unexpected token")) + | Syntax (region, s) when region <> Source.no_region -> + raise (Syntax (convert_pos buf, s)) + + let parse_string s = + parse "string" (Lexing.from_string ~with_positions:true s) + + let parse_channel oc = + parse "channel" (Lexing.from_channel ~with_positions:true oc) + + let parse_file name = + let oc = open_in name in + Fun.protect ~finally:(fun () -> close_in oc) (fun () -> + parse name (Lexing.from_channel ~with_positions:true oc) + ) + end) + +module Module = (val make Parser.module1) +module Script = (val make Parser.script) +module Script1 = (val make Parser.script1) diff --git a/interpreter/text/parse.mli b/interpreter/text/parse.mli index a7b79f957b..e3d1e654fa 100644 --- a/interpreter/text/parse.mli +++ b/interpreter/text/parse.mli @@ -1,12 +1,14 @@ -type 'a start = - | Module : (Script.var option * Script.definition) start - | Script : Script.script start - | Script1 : Script.script start - exception Syntax of Source.region * string -val parse : string -> Lexing.lexbuf -> 'a start -> 'a (* raises Syntax *) +module type S = +sig + type t + val parse : string -> Lexing.lexbuf -> t + val parse_file : string -> t + val parse_string : string -> t + val parse_channel : in_channel -> t +end -val string_to_script : string -> Script.script (* raises Syntax *) -val string_to_definition : string -> Script.definition (* raises Syntax *) -val string_to_module : string -> Ast.module_ (* raises Syntax *) +module Module : S with type t = Script.var option * Script.definition +module Script1 : S with type t = Script.script +module Script : S with type t = Script.script diff --git a/interpreter/text/parse_error.ml b/interpreter/text/parse_error.ml new file mode 100644 index 0000000000..eb46c0ede3 --- /dev/null +++ b/interpreter/text/parse_error.ml @@ -0,0 +1,3 @@ +(* This is here since both Lexer, Parser, and Parse need it, + * but menhir cannot create a Parser that exports it. *) +exception Syntax of Source.region * string diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index c1b623ed8e..3747df8964 100644 --- a/interpreter/text/parser.mly +++ b/interpreter/text/parser.mly @@ -8,11 +8,7 @@ open Script (* Error handling *) -let error at msg = raise (Script.Syntax (at, msg)) - -let parse_error msg = - error Source.no_region - (if msg = "syntax error" then "unexpected token" else msg) +let error at msg = raise (Parse_error.Syntax (at, msg)) (* Position handling *) @@ -299,7 +295,7 @@ let inline_tag_type (c : context) (TagT ht) at = %token Ast.instr'> STRUCT_NEW ARRAY_NEW ARRAY_GET %token STRUCT_SET %token Ast.idx -> Ast.instr'> STRUCT_GET -%token ARRAY_NEW ARRAY_NEW_FIXED ARRAY_NEW_ELEM ARRAY_NEW_DATA +%token ARRAY_NEW_FIXED ARRAY_NEW_ELEM ARRAY_NEW_DATA %token ARRAY_SET ARRAY_LEN %token ARRAY_COPY ARRAY_FILL ARRAY_INIT_DATA ARRAY_INIT_ELEM %token EXTERN_CONVERT @@ -502,10 +498,6 @@ num : | INT { $1 @@ at () } | FLOAT { $1 @@ at () } -num_list: - | /* empty */ { [] } - | num num_list { $1 :: $2 } - var : | NAT { let at = at () in fun c lookup -> nat32 $1 at @@ at } | VAR { let at = at () in fun c lookup -> lookup c ($1 @@ at) @@ at } @@ -577,6 +569,7 @@ plain_instr : { fun c -> let xs, x = Lib.List.split_last ($2 c label :: $3 c label) in br_table xs x } | BR_ON_NULL var { fun c -> $1 ($2 c label) } + | BR_ON_NON_NULL var { fun c -> br_on_non_null ($2 c label) } | BR_ON_CAST var ref_type ref_type { fun c -> $1 ($2 c label) ($3 c) ($4 c) } | RETURN { fun c -> return } | CALL var { fun c -> call ($2 c func) } @@ -652,14 +645,14 @@ plain_instr : | UNARY { fun c -> $1 } | BINARY { fun c -> $1 } | CONVERT { fun c -> $1 } - | VEC_CONST VEC_SHAPE num_list { let at = at () in fun c -> fst (vec $1 $2 $3 at) } + | VEC_CONST VEC_SHAPE list(num) { let at = at () in fun c -> fst (vec $1 $2 $3 at) } | VEC_UNARY { fun c -> $1 } | VEC_BINARY { fun c -> $1 } | VEC_TERNARY { fun c -> $1 } | VEC_TEST { fun c -> $1 } | VEC_SHIFT { fun c -> $1 } | VEC_BITMASK { fun c -> $1 } - | VEC_SHUFFLE num_list { let at = at () in fun c -> i8x16_shuffle (shuffle_lit $2 at) } + | VEC_SHUFFLE list(num) { let at = at () in fun c -> i8x16_shuffle (shuffle_lit $2 at) } | VEC_SPLAT { fun c -> $1 } | VEC_EXTRACT NAT { let at = at () in fun c -> $1 (vec_lane_index $2 at) } | VEC_REPLACE NAT { let at = at () in fun c -> $1 (vec_lane_index $2 at) } @@ -825,7 +818,6 @@ block_result_body : { fun c -> let FuncT (ts1, ts2), es = $5 c in FuncT (ts1, snd $3 c @ ts2), es } - expr : /* Sugar */ | LPAR expr1 RPAR { let at = at () in fun c -> let es, e' = $2 c in es @ [e' @@ at] } @@ -1060,10 +1052,10 @@ func_body : | LPAR LOCAL local_type_list RPAR func_body { let at3 = ati 3 in fun c -> anon_locals c (fst $3) at3; let f = $5 c in - {f with locals = snd $3 c @ f.locals} } + {f with locals = snd $3 c @ f.Ast.locals} } | LPAR LOCAL bind_var local_type RPAR func_body /* Sugar */ { fun c -> ignore (bind_local c $3); let f = $6 c in - {f with locals = $4 c :: f.locals} } + {f with locals = $4 c :: f.Ast.locals} } local_type : | val_type { let at = at () in fun c -> {ltype = $1 c} @@ at } @@ -1397,12 +1389,12 @@ module_fields1 : { fun c -> let ef = $1 c in let mff = $2 c in fun () -> let mf = mff () in fun () -> let elems = ef () in let m = mf () in - {m with elems = elems :: m.elems} } + {m with elems = elems :: m.Ast.elems} } | data module_fields { fun c -> let df = $1 c in let mff = $2 c in fun () -> let mf = mff () in fun () -> let data = df () in let m = mf () in - {m with datas = data :: m.datas} } + {m with datas = data :: m.Ast.datas} } | start module_fields { fun c -> let mff = $2 c in fun () -> let mf = mff () in @@ -1422,12 +1414,11 @@ module_fields1 : fun () -> let m = mf () in {m with exports = $1 c :: m.exports} } -module_var_opt : - | /* empty */ { None } - | VAR { Some ($1 @@ at ()) } /* Sugar */ +module_var : + | VAR { $1 @@ at () } /* Sugar */ module_ : - | LPAR MODULE module_var_opt module_fields RPAR + | LPAR MODULE option(module_var) module_fields RPAR { $3, Textual ($4 (empty_context ()) () () @@ at ()) @@ at () } inline_module : /* Sugar */ @@ -1439,23 +1430,23 @@ inline_module1 : /* Sugar */ /* Scripts */ -script_var_opt : - | /* empty */ { None } - | VAR { Some ($1 @@ at ()) } /* Sugar */ +script_var : + | VAR { $1 @@ at () } /* Sugar */ script_module : | module_ { $1 } - | LPAR MODULE module_var_opt BIN string_list RPAR + | LPAR MODULE option(module_var) BIN string_list RPAR { $3, Encoded ("binary:" ^ string_of_pos (at()).left, $5) @@ at() } - | LPAR MODULE module_var_opt QUOTE string_list RPAR + | LPAR MODULE option(module_var) QUOTE string_list RPAR { $3, Quoted ("quote:" ^ string_of_pos (at()).left, $5) @@ at() } action : - | LPAR INVOKE module_var_opt name literal_list RPAR + | LPAR INVOKE option(module_var) name list(literal) RPAR { Invoke ($3, $4, $5) @@ at () } - | LPAR GET module_var_opt name RPAR + | LPAR GET option(module_var) name RPAR { Get ($3, $4) @@ at() } + assertion : | LPAR ASSERT_MALFORMED script_module STRING RPAR { AssertMalformed (snd $3, $4) @@ at () } @@ -1465,7 +1456,7 @@ assertion : { AssertUnlinkable (snd $3, $4) @@ at () } | LPAR ASSERT_TRAP script_module STRING RPAR { AssertUninstantiable (snd $3, $4) @@ at () } - | LPAR ASSERT_RETURN action result_list RPAR { AssertReturn ($3, $4) @@ at () } + | LPAR ASSERT_RETURN action list(result) RPAR { AssertReturn ($3, $4) @@ at () } | LPAR ASSERT_TRAP action STRING RPAR { AssertTrap ($3, $4) @@ at () } | LPAR ASSERT_EXCEPTION action STRING RPAR { AssertException ($3, $4) @@ at () } | LPAR ASSERT_SUSPENSION action STRING RPAR { AssertSuspension ($3, $4) @@ at () } @@ -1475,24 +1466,20 @@ cmd : | action { Action $1 @@ at () } | assertion { Assertion $1 @@ at () } | script_module { Module (fst $1, snd $1) @@ at () } - | LPAR REGISTER name module_var_opt RPAR { Register ($3, $4) @@ at () } + | LPAR REGISTER name option(module_var) RPAR { Register ($3, $4) @@ at () } | meta { Meta $1 @@ at () } -cmd_list : - | /* empty */ { [] } - | cmd cmd_list { $1 :: $2 } - meta : - | LPAR SCRIPT script_var_opt cmd_list RPAR { Script ($3, $4) @@ at () } - | LPAR INPUT script_var_opt STRING RPAR { Input ($3, $4) @@ at () } - | LPAR OUTPUT script_var_opt STRING RPAR { Output ($3, Some $4) @@ at () } - | LPAR OUTPUT script_var_opt RPAR { Output ($3, None) @@ at () } + | LPAR SCRIPT option(script_var) list(cmd) RPAR { Script ($3, $4) @@ at () } + | LPAR INPUT option(script_var) STRING RPAR { Input ($3, $4) @@ at () } + | LPAR OUTPUT option(script_var) STRING RPAR { Output ($3, Some $4) @@ at () } + | LPAR OUTPUT option(script_var) RPAR { Output ($3, None) @@ at () } literal_num : | LPAR CONST num RPAR { snd (num $2 $3) } literal_vec : - | LPAR VEC_CONST VEC_SHAPE num_list RPAR { snd (vec $2 $3 $4 (at ())) } + | LPAR VEC_CONST VEC_SHAPE list(num) RPAR { snd (vec $2 $3 $4 (at ())) } literal_ref : | LPAR REF_NULL heap_type RPAR { Value.NullRef ($3 (empty_context ())) } @@ -1504,18 +1491,10 @@ literal : | literal_vec { Value.Vec $1 @@ at () } | literal_ref { Value.Ref $1 @@ at () } -literal_list : - | /* empty */ { [] } - | literal literal_list { $1 :: $2 } - numpat : | num { fun sh -> vec_lane_lit sh $1.it $1.at } | NAN { fun sh -> vec_lane_nan sh $1 (ati 3) } -numpat_list: - | /* empty */ { [] } - | numpat numpat_list { $1 :: $2 } - result : | literal_num { NumResult (NumPat ($1 @@ at())) @@ at () } | LPAR CONST NAN RPAR { NumResult (NanPat (nanop $2 ($3 @@ ati 3))) @@ at () } @@ -1528,17 +1507,13 @@ result : | LPAR REF_NULL RPAR { RefResult NullPat @@ at () } | LPAR REF_FUNC RPAR { RefResult (RefTypePat FuncHT) @@ at () } | LPAR REF_EXTERN RPAR { RefResult (RefTypePat ExternHT) @@ at () } - | LPAR VEC_CONST VEC_SHAPE numpat_list RPAR + | LPAR VEC_CONST VEC_SHAPE list(numpat) RPAR { if V128.num_lanes $3 <> List.length $4 then error (at ()) "wrong number of lane literals"; VecResult (VecPat (Value.V128 ($3, List.map (fun lit -> lit $3) $4))) @@ at () } -result_list : - | /* empty */ { [] } - | result result_list { $1 :: $2 } - script : - | cmd_list EOF { $1 } + | list(cmd) EOF { $1 } | inline_module1 EOF { [Module (None, $1) @@ at ()] } /* Sugar */ script1 : diff --git a/interpreter/wasm.opam b/interpreter/wasm.opam index 5d5984106c..ad8b60af23 100644 --- a/interpreter/wasm.opam +++ b/interpreter/wasm.opam @@ -11,6 +11,7 @@ bug-reports: "https://github.com/WebAssembly/spec/issues" depends: [ "dune" {>= "2.9"} "ocaml" {>= "4.12"} + "menhir" {>= "20220210"} "odoc" {with-doc} ] build: [