From 028daa2f5ecb84cc118574cd6fca798ca0b1322a Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Thu, 24 Aug 2023 12:16:39 -0700 Subject: [PATCH 1/5] Update array.copy semantics to handle packed types Previously the array.copy semantics were defined in terms of executing array.get on the source array, which is not correct if the source array contains a packed type. Update the semantics prose and formalism to choose between array.get and array.get_u depending on whether the array contents are packed. The interpreter does not need updating because it already handled the difference correctly. --- document/core/exec/instructions.rst | 84 ++++++++++++++++++----------- 1 file changed, 53 insertions(+), 31 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index a3e4d7691..3d6e0770a 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -1120,61 +1120,75 @@ Reference Instructions :math:`\ARRAYCOPY~x~y` ...................... -.. todo:: Handle packed fields correctly via array.get_u instead of array.get +1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[y]` exists. -1. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. +2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[y]`. -2. Pop the value :math:`n` from the stack. +3. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is an :ref:`array type `. -3. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. +4. Let :math:`\TARRAY~\X{ft}` be the :ref:`expanded ` :ref:`array type ` :math:`\deftype`. -4. Pop the value :math:`s` from the stack. +5. If :math:`\X{ft} = \mut~\packedtype`, then: -5. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~y)` is on the top of the stack. + a. Let :math:`\X{get}` be the instruction :math:`\ARRAYGETU~y`. + +6. Else: -6. Pop the value :math:`\reff_2` from the stack. + a. Let :math:`\X{get}` be the instruction :math:`\ARRAYGET~y`. 7. 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:`d` from the stack. +8. Pop the value :math:`n` from the stack. + +9. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. + +10. Pop the value :math:`s` from the stack. + +11. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~y)` is on the top of the stack. + +12. Pop the value :math:`\reff_2` 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. +13. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. -10. Pop the value :math:`\reff_1` from the stack. +14. Pop the value :math:`d` from the stack. -11. If :math:`\reff_1` is :math:`\REFNULL~t`, then: +15. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. + +16. Pop the value :math:`\reff_1` from the stack. + +17. If :math:`\reff_1` is :math:`\REFNULL~t`, then: a. Trap. -12. Assert: due to :ref:`validation `, :math:`\reff_1` is an :ref:`array reference `. +18. Assert: due to :ref:`validation `, :math:`\reff_1` is an :ref:`array reference `. -13. Let :math:`\REFARRAYADDR~a_1` be the reference value :math:`\reff_1`. +19. Let :math:`\REFARRAYADDR~a_1` be the reference value :math:`\reff_1`. -14. If :math:`\reff_2` is :math:`\REFNULL~t`, then: +20. If :math:`\reff_2` is :math:`\REFNULL~t`, then: a. Trap. -15. Assert: due to :ref:`validation `, :math:`\reff_2` is an :ref:`array reference `. +21. Assert: due to :ref:`validation `, :math:`\reff_2` is an :ref:`array reference `. -16. Let :math:`\REFARRAYADDR~a_2` be the reference value :math:`\reff_2`. +22. Let :math:`\REFARRAYADDR~a_2` be the reference value :math:`\reff_2`. -17. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_1]` exists. +23. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_1]` exists. -18. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_2]` exists. +24. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_2]` exists. -19. If :math:`d + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_1].\AIFIELDS`, then: +25. If :math:`d + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_1].\AIFIELDS`, then: a. Trap. -20. If :math:`s + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_2].\AIFIELDS`, then: +26. If :math:`s + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_2].\AIFIELDS`, then: a. Trap. -21. If :math:`n = 0`, then: +27. If :math:`n = 0`, then: a. Return. -22. If :math:`d \leq s`, then: +28. If :math:`d \leq s`, then: a. Push the value :math:`\REFARRAYADDR~a_1` to the stack. @@ -1184,7 +1198,7 @@ Reference Instructions d. Push the value :math:`\I32.\CONST~s` to the stack. - e. Execute the instruction :math:`\ARRAYGET~y`. + e. Execute :math:`\X{get}`. f. Execute the instruction :math:`\ARRAYSET~x`. @@ -1200,7 +1214,7 @@ Reference Instructions l. Push the value :math:`\I32.\CONST~(s+1)` to the stack. -23. Else: +29. Else: a. Push the value :math:`\REFARRAYADDR~a_1` to the stack. @@ -1214,7 +1228,7 @@ Reference Instructions f. Push the value :math:`\I32.\CONST~(s+n-1)` to the stack. - g. Execute the instruction :math:`\ARRAYGET~y`. + g. Execute :math:`\X{get}`. h. Execute the instruction :math:`\ARRAYSET~x`. @@ -1226,9 +1240,9 @@ Reference Instructions l. Push the value :math:`\I32.\CONST~s` to the stack. -24. Push the value :math:`\I32.\CONST~(n-1)` to the stack. +30. Push the value :math:`\I32.\CONST~(n-1)` to the stack. -25. Execute the instruction :math:`\ARRAYCOPY~x~y`. +31. Execute the instruction :math:`\ARRAYCOPY~x~y`. .. math:: ~\\[-1ex] @@ -1248,24 +1262,32 @@ Reference Instructions \\ \quad S; \begin{array}[t]{@{}l@{}} (\REFARRAYADDR~a_1)~(\I32.\CONST~d) \\ - (\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\ARRAYGET~y) \\ + (\REFARRAYADDR~a_2)~(\I32.\CONST~s)~\X{get} \\ (\ARRAYSET~x) \\ (\REFARRAYADDR~a_1)~(\I32.\CONST~d+1)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \\ \end{array} \\ \qquad - (\otherwise, \iff d \leq s) + \begin{array}[t]{@{}r@{~}l@{}} + (\otherwise, \iff & d \leq s \\ + \land & (\X{get} = \ARRAYGET~y \vee \X{get} = \ARRAYGETU~y) \\ + \land & (F.\AMODULE.\MITYPES[x] = \TARRAY~\mut~\packedtype \Longleftrightarrow \X{get} = \ARRAYGETU~y)) + \end{array} \\[1ex] S; (\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\ARRAYCOPY~x~y) \quad\stepto \\ \quad S; \begin{array}[t]{@{}l@{}} (\REFARRAYADDR~a_1)~(\I32.\CONST~d+n) \\ - (\REFARRAYADDR~a_2)~(\I32.\CONST~s+n)~(\ARRAYGET~y) \\ + (\REFARRAYADDR~a_2)~(\I32.\CONST~s+n)~\X{get} \\ (\ARRAYSET~x) \\ (\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \\ \end{array} \\ \qquad - (\otherwise, \iff d > s) + \begin{array}[t]{@{}r@{~}l@{}} + (\otherwise, \iff & d > s \\ + \land & (\X{get} = \ARRAYGET~y \vee \X{get} = \ARRAYGETU~y) \\ + \land & (F.\AMODULE.\MITYPES[x] = \TARRAY~\mut~\packedtype \Longleftrightarrow \X{get} = \ARRAYGETU~y)) + \end{array} \\[1ex] S; (\REFNULL~t)~(\I32.\CONST~d)~\val~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \quad\stepto\quad \TRAP \\[1ex] From 8e3581d5142eaf4aaec6e551dd28cfdb11d11065 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Fri, 8 Sep 2023 16:38:49 -0700 Subject: [PATCH 2/5] getfield meta function --- document/core/exec/instructions.rst | 76 ++++++++++++--------------- document/core/syntax/instructions.rst | 9 ++++ document/core/util/macros.def | 5 ++ 3 files changed, 47 insertions(+), 43 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 3d6e0770a..c7e492ec7 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -1120,75 +1120,67 @@ Reference Instructions :math:`\ARRAYCOPY~x~y` ...................... -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[y]` exists. +1. 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. 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. If :math:`\X{ft} = \mut~\packedtype`, then: +3. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is an :ref:`array type `. - a. Let :math:`\X{get}` be the instruction :math:`\ARRAYGETU~y`. +4. Let :math:`\TARRAY~\mut~\X{st}` be the :ref:`expanded ` :ref:`array type ` :math:`\deftype`. -6. Else: +5. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. - a. Let :math:`\X{get}` be the instruction :math:`\ARRAYGET~y`. +6. Pop the value :math:`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. Pop the value :math:`n` from the stack. - -9. 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:`s` from the stack. -10. Pop the value :math:`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. -11. 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. -12. 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. -13. 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:`d` from the stack. -14. Pop the value :math:`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. -15. 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. -16. Pop the value :math:`\reff_1` from the stack. - -17. If :math:`\reff_1` is :math:`\REFNULL~t`, then: +15. If :math:`\reff_1` is :math:`\REFNULL~t`, then: a. Trap. -18. Assert: due to :ref:`validation `, :math:`\reff_1` is an :ref:`array reference `. +16. Assert: due to :ref:`validation `, :math:`\reff_1` is an :ref:`array reference `. -19. Let :math:`\REFARRAYADDR~a_1` be the reference value :math:`\reff_1`. +17. Let :math:`\REFARRAYADDR~a_1` be the reference value :math:`\reff_1`. -20. If :math:`\reff_2` is :math:`\REFNULL~t`, then: +18. If :math:`\reff_2` is :math:`\REFNULL~t`, then: a. Trap. -21. Assert: due to :ref:`validation `, :math:`\reff_2` is an :ref:`array reference `. +19. Assert: due to :ref:`validation `, :math:`\reff_2` is an :ref:`array reference `. -22. Let :math:`\REFARRAYADDR~a_2` be the reference value :math:`\reff_2`. +20. Let :math:`\REFARRAYADDR~a_2` be the reference value :math:`\reff_2`. -23. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_1]` exists. +21. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_1]` exists. -24. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_2]` exists. +22. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_2]` exists. -25. If :math:`d + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_1].\AIFIELDS`, then: +23. If :math:`d + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_1].\AIFIELDS`, then: a. Trap. -26. If :math:`s + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_2].\AIFIELDS`, then: +24. If :math:`s + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_2].\AIFIELDS`, then: a. Trap. -27. If :math:`n = 0`, then: +25. If :math:`n = 0`, then: a. Return. -28. If :math:`d \leq s`, then: +26. If :math:`d \leq s`, then: a. Push the value :math:`\REFARRAYADDR~a_1` to the stack. @@ -1198,7 +1190,7 @@ Reference Instructions d. Push the value :math:`\I32.\CONST~s` to the stack. - e. Execute :math:`\X{get}`. + e. Execute :math:`\getfield(\X{st})`. f. Execute the instruction :math:`\ARRAYSET~x`. @@ -1214,7 +1206,7 @@ Reference Instructions l. Push the value :math:`\I32.\CONST~(s+1)` to the stack. -29. Else: +27. Else: a. Push the value :math:`\REFARRAYADDR~a_1` to the stack. @@ -1228,7 +1220,7 @@ Reference Instructions f. Push the value :math:`\I32.\CONST~(s+n-1)` to the stack. - g. Execute :math:`\X{get}`. + g. Execute :math:`\getfield(\X{st})`. h. Execute the instruction :math:`\ARRAYSET~x`. @@ -1240,9 +1232,9 @@ Reference Instructions l. Push the value :math:`\I32.\CONST~s` to the stack. -30. Push the value :math:`\I32.\CONST~(n-1)` to the stack. +28. Push the value :math:`\I32.\CONST~(n-1)` to the stack. -31. Execute the instruction :math:`\ARRAYCOPY~x~y`. +29. Execute the instruction :math:`\ARRAYCOPY~x~y`. .. math:: ~\\[-1ex] @@ -1262,15 +1254,14 @@ Reference Instructions \\ \quad S; \begin{array}[t]{@{}l@{}} (\REFARRAYADDR~a_1)~(\I32.\CONST~d) \\ - (\REFARRAYADDR~a_2)~(\I32.\CONST~s)~\X{get} \\ + (\REFARRAYADDR~a_2)~(\I32.\CONST~s)~\getfield(\X{st}) \\ (\ARRAYSET~x) \\ (\REFARRAYADDR~a_1)~(\I32.\CONST~d+1)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \\ \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\otherwise, \iff & d \leq s \\ - \land & (\X{get} = \ARRAYGET~y \vee \X{get} = \ARRAYGETU~y) \\ - \land & (F.\AMODULE.\MITYPES[x] = \TARRAY~\mut~\packedtype \Longleftrightarrow \X{get} = \ARRAYGETU~y)) + \land & F.\AMODULE.\MITYPES[x] = \TARRAY~\mut~\X{st}) \end{array} \\[1ex] S; (\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\ARRAYCOPY~x~y) @@ -1278,15 +1269,14 @@ Reference Instructions \\ \quad S; \begin{array}[t]{@{}l@{}} (\REFARRAYADDR~a_1)~(\I32.\CONST~d+n) \\ - (\REFARRAYADDR~a_2)~(\I32.\CONST~s+n)~\X{get} \\ + (\REFARRAYADDR~a_2)~(\I32.\CONST~s+n)~\getfield(\X{st}) \\ (\ARRAYSET~x) \\ (\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \\ \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\otherwise, \iff & d > s \\ - \land & (\X{get} = \ARRAYGET~y \vee \X{get} = \ARRAYGETU~y) \\ - \land & (F.\AMODULE.\MITYPES[x] = \TARRAY~\mut~\packedtype \Longleftrightarrow \X{get} = \ARRAYGETU~y)) + \land & F.\AMODULE.\MITYPES[x] = \TARRAY~\mut~\X{st}) \end{array} \\[1ex] S; (\REFNULL~t)~(\I32.\CONST~d)~\val~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \quad\stepto\quad \TRAP diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 8d4efe959..e6ff0221e 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -541,6 +541,15 @@ The instructions |I31NEW| and :math:`\I31GET\K{\_}\sx` convert between type |I31 The instructions |EXTERNINTERNALIZE| and |EXTERNEXTERNALIZE| allow lossless conversion between references represented as type :math:`(\REF~\NULL~\EXTERN)`| and as :math:`(\REF~\NULL~\ANY)`. +The following auxiliary function produces an instruction that accesses an array slot for a given :ref:`storage type `. + +.. _aux-getfield: + +.. math:: + \begin{array}{lll} + \getfield(\valtype) &=& \ARRAYGET \\ + \getfield(\packedtype) &=& \ARRAYGETU \\ + \end{array} .. index:: ! parametric instruction, value type pair: abstract syntax; instruction diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 1833fdc98..79ef43076 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -656,6 +656,11 @@ .. |expr| mathdef:: \xref{syntax/instructions}{syntax-expr}{\X{expr}} +.. Instructions, meta functions + +.. |getfield| mathdef:: \xref{syntax/instructions}{aux-getfield}{\F{getfield}} + + .. Binary Format .. ------------- From e04ecbdc592bbd2af19bccce7f508d036fe130ac Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Fri, 8 Sep 2023 17:35:15 -0700 Subject: [PATCH 3/5] move auxiliary function --- document/core/exec/instructions.rst | 10 ++++++++++ document/core/syntax/instructions.rst | 10 ---------- document/core/util/macros.def | 2 +- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index c7e492ec7..66ddd4f12 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -1284,6 +1284,16 @@ Reference Instructions S; \val~(\I32.\CONST~d)~(\REFNULL~t)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \quad\stepto\quad \TRAP \end{array} +Where: + +.. _aux-getfield: + +.. math:: + \begin{array}{lll} + \getfield(\valtype) &=& \ARRAYGET \\ + \getfield(\packedtype) &=& \ARRAYGETU \\ + \end{array} + .. _exec-array.init_data: diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index e6ff0221e..57fafe27e 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -541,16 +541,6 @@ The instructions |I31NEW| and :math:`\I31GET\K{\_}\sx` convert between type |I31 The instructions |EXTERNINTERNALIZE| and |EXTERNEXTERNALIZE| allow lossless conversion between references represented as type :math:`(\REF~\NULL~\EXTERN)`| and as :math:`(\REF~\NULL~\ANY)`. -The following auxiliary function produces an instruction that accesses an array slot for a given :ref:`storage type `. - -.. _aux-getfield: - -.. math:: - \begin{array}{lll} - \getfield(\valtype) &=& \ARRAYGET \\ - \getfield(\packedtype) &=& \ARRAYGETU \\ - \end{array} - .. index:: ! parametric instruction, value type pair: abstract syntax; instruction .. _syntax-instr-parametric: diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 79ef43076..78ded3620 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -658,7 +658,7 @@ .. Instructions, meta functions -.. |getfield| mathdef:: \xref{syntax/instructions}{aux-getfield}{\F{getfield}} +.. |getfield| mathdef:: \xref{exec/instructions}{aux-getfield}{\F{getfield}} From 31444ad90c38008a377b2e4c4db55b446d7d1c27 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Fri, 8 Sep 2023 17:42:48 -0700 Subject: [PATCH 4/5] pop i32.const fixes --- document/core/exec/instructions.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 66ddd4f12..b75b38e97 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -1130,11 +1130,11 @@ Reference Instructions 5. 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:`n` from the stack. +6. 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. Pop the value :math:`s` from the stack. +8. 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. @@ -1142,7 +1142,7 @@ Reference Instructions 11. 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:`d` from the stack. +12. 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. From aa173f6ca4d0b9c35871200ac0edbafd6d09d705 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Fri, 8 Sep 2023 17:47:09 -0700 Subject: [PATCH 5/5] format conditions on single line --- document/core/exec/instructions.rst | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index b75b38e97..82be56270 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -1259,10 +1259,7 @@ Reference Instructions (\REFARRAYADDR~a_1)~(\I32.\CONST~d+1)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \\ \end{array} \\ \qquad - \begin{array}[t]{@{}r@{~}l@{}} - (\otherwise, \iff & d \leq s \\ - \land & F.\AMODULE.\MITYPES[x] = \TARRAY~\mut~\X{st}) - \end{array} + (\otherwise, \iff d \leq s \land F.\AMODULE.\MITYPES[x] = \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) \quad\stepto @@ -1274,10 +1271,7 @@ Reference Instructions (\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \\ \end{array} \\ \qquad - \begin{array}[t]{@{}r@{~}l@{}} - (\otherwise, \iff & d > s \\ - \land & F.\AMODULE.\MITYPES[x] = \TARRAY~\mut~\X{st}) - \end{array} + (\otherwise, \iff d > s \land F.\AMODULE.\MITYPES[x] = \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 \\[1ex]