Update array.copy semantics to handle packed types #416
Conversation
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.
|
Current dependencies on/for this PR: This comment was auto-generated by Graphite. |
document/core/exec/instructions.rst
Outdated
| \land & (\X{get} = \ARRAYGET~y \vee \X{get} = \ARRAYGETU~y) \\ | ||
| \land & (F.\AMODULE.\MITYPES[x] = \TARRAY~\mut~\packedtype \Longleftrightarrow \X{get} = \ARRAYGETU~y)) |
There was a problem hiding this comment.
Can you think of a better way to express this? Is there a better symbol to use for bidirectional implication than \Longleftrightarrow?
There was a problem hiding this comment.
The symbol would be correct. But I would suggest to factor out the choice of get into an auxiliary function which does a case distinction on the storage type, i.e., something like
getfield(valtype) = array.get
getfield(packedtype) = array.get_u
There was a problem hiding this comment.
Thanks, I've written this up now. PTAL!
document/core/exec/instructions.rst
Outdated
| @@ -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 <valid-array.init_data>`, the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[y]` exists. | |||
There was a problem hiding this comment.
| 1. Assert: due to :ref:`validation <valid-array.init_data>`, the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[y]` exists. | |
| 1. Assert: due to :ref:`validation <valid-array.copy>`, the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[y]` exists. |
document/core/exec/instructions.rst
Outdated
|
|
||
| 2. Pop the value :math:`n` from the stack. | ||
| 3. Assert: due to :ref:`validation <valid-array.init_data>`, the :ref:`expansion <aux-expand-deftype>` of :math:`\deftype` is an :ref:`array type <syntax-arraytype>`. |
There was a problem hiding this comment.
| 3. Assert: due to :ref:`validation <valid-array.init_data>`, the :ref:`expansion <aux-expand-deftype>` of :math:`\deftype` is an :ref:`array type <syntax-arraytype>`. | |
| 3. Assert: due to :ref:`validation <valid-array.copy>`, the :ref:`expansion <aux-expand-deftype>` of :math:`\deftype` is an :ref:`array type <syntax-arraytype>`. |
document/core/exec/instructions.rst
Outdated
| \land & (\X{get} = \ARRAYGET~y \vee \X{get} = \ARRAYGETU~y) \\ | ||
| \land & (F.\AMODULE.\MITYPES[x] = \TARRAY~\mut~\packedtype \Longleftrightarrow \X{get} = \ARRAYGETU~y)) |
There was a problem hiding this comment.
The symbol would be correct. But I would suggest to factor out the choice of get into an auxiliary function which does a case distinction on the storage type, i.e., something like
getfield(valtype) = array.get
getfield(packedtype) = array.get_u
document/core/exec/instructions.rst
Outdated
|
|
||
| a. Let :math:`\X{get}` be the instruction :math:`\ARRAYGET~y`. | ||
| 6. Pop the value :math:`n` from the stack. |
There was a problem hiding this comment.
| 6. Pop the value :math:`n` from the stack. | |
| 6. Pop the value :math:`\I32.\CONST~n` from the stack. |
document/core/exec/instructions.rst
Outdated
| 8. Pop the value :math:`n` from the stack. | ||
|
|
||
| 9. Assert: due to :ref:`validation <valid-array.copy>`, a :ref:`value <syntax-val>` of :ref:`type <syntax-valtype>` :math:`\I32` is on the top of the stack. | ||
| 8. Pop the value :math:`s` from the stack. |
There was a problem hiding this comment.
| 8. Pop the value :math:`s` from the stack. | |
| 8. Pop the value :math:`\I32.\CONST~s` from the stack. |
document/core/exec/instructions.rst
Outdated
|
|
||
| 13. Assert: due to :ref:`validation <valid-array.copy>`, a :ref:`value <syntax-val>` of :ref:`type <syntax-valtype>` :math:`\I32` is on the top of the stack. | ||
| 12. Pop the value :math:`d` from the stack. |
There was a problem hiding this comment.
| 12. Pop the value :math:`d` from the stack. | |
| 12. Pop the value :math:`(\I32.\CONST~d)` from the stack. |
| \begin{array}{lll} | ||
| \getfield(\valtype) &=& \ARRAYGET \\ | ||
| \getfield(\packedtype) &=& \ARRAYGETU \\ | ||
| \end{array} |
There was a problem hiding this comment.
I'd move this next to the rules (as a "where:" sort of thing), since it is local helper for that specific rule only.
|
Comments addressed. I also updated the formatting of the side conditions now that they are shorter. |
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.