-
Notifications
You must be signed in to change notification settings - Fork 69
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Validation of instructions (plus some infra and fixes) #377
Conversation
Note: Cast instructions do _not_ require the operand's source type to be a supertype of the target type. It can also be a "sibling" in the same hierarchy, i.e., they only need to have a common supertype (in practice, it is sufficient to test that both types share the same top heap type.). Allowing so is necessary to maintain subtype substitutability, i.e., the ability to maintain well-typedness when operands are replaced by subtypes. | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why is this no longer necessary / true / helpful?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It was primarily meant as an explanation why the earlier rules had this seemingly weird side condition about a common supertype, instead of requiring that the (explicit) target type has to be a subtype of the (implicit) source type. Since the source type is now explicit as well, and the "real" operand type no longer occurs in the rule itself (but can be weakened separately via subsumption), I though that the explanation became both confusing and unnecessary.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fair enough. I think a call-out like this is probably still helpful since folks might not be thinking about subsumption when trying to understand the rules, but of course we cannot add an unbounded number of such helpful notes.
document/core/valid/instructions.rst
Outdated
|
||
* The :ref:`reference type <syntax-reftype>` :math:`\X{rt}` must be :ref:`valid <valid-reftype>`. | ||
|
||
* Then the instruction is valid with type :math:`[\X{rt}'] \to [\I32]` for any :ref:`valid <valid-reftype>` :ref:`reference type <syntax-reftype>` that :ref:`matches <match-reftype>` :math:`\X{rt}`. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is it fine to leave it implicit that the mentioned "valid reference type that matches rt
" is rt'
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah, no, that was a typo. Fixed.
document/core/valid/instructions.rst
Outdated
* Let :math:`t^\ast` be the concatenation of all :math:`t_i`. | ||
|
||
* Then the instruction is valid with type :math:`[t^\ast] \to [(\REF~x)]`. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
* Let :math:`t^\ast` be the concatenation of all :math:`t_i`. | |
* Then the instruction is valid with type :math:`[t^\ast] \to [(\REF~x)]`. | |
* Then the instruction is valid with type :math:`[] \to [(\REF~x)]`. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yep.
document/core/valid/instructions.rst
Outdated
|
||
* Let :math:`t` be the :ref:`value type <syntax-valtype>` :math:`\unpacktype(\storagetype)`. | ||
|
||
* The extension :math:`\sx` must be present of and only if :math:`t` is different from :math:`\storagetype`. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
* The extension :math:`\sx` must be present of and only if :math:`t` is different from :math:`\storagetype`. | |
* The extension :math:`\sx` must be present if and only if :math:`t` is different from :math:`\storagetype`. |
Why spec this condition as opposed to "if and only if :math:\storagetype
is i8
or i16
"? The latter seems more straightforward.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fair enough, changed.
document/core/valid/instructions.rst
Outdated
|
||
* Let :math:`t` be the :ref:`value type <syntax-valtype>` :math:`\unpacktype(\storagetype)`. | ||
|
||
* The extension :math:`\sx` must be present of and only if :math:`t` is different from :math:`\storagetype`. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
* The extension :math:`\sx` must be present of and only if :math:`t` is different from :math:`\storagetype`. | |
* The extension :math:`\sx` must be present if and only if :math:`t` is different from :math:`\storagetype`. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fixed (and changed like above).
document/core/valid/instructions.rst
Outdated
:math:`\I31GET\K{\_}\sx` | ||
........................ | ||
|
||
* The instruction is valid with type :math:`[(\REF~\I31)] \to [\I32]`. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
* The instruction is valid with type :math:`[(\REF~\I31)] \to [\I32]`. | |
* The instruction is valid with type :math:`[(\REF~\NULL~\I31)] \to [\I32]`. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fixed.
document/core/valid/instructions.rst
Outdated
.. math:: | ||
\frac{ | ||
}{ | ||
C \vdashinstr \I31GET\K{\_}\sx : [(\REF~\I31)] \to [\I32] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
C \vdashinstr \I31GET\K{\_}\sx : [(\REF~\I31)] \to [\I32] | |
C \vdashinstr \I31GET\K{\_}\sx : [(\REF~\NULL~\I31)] \to [\I32] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fixed.
Co-authored-by: Thomas Lively <tlively@google.com>
@conrad-watt, ping. |
@conrad-watt, ping. |
document/core/valid/instructions.rst
Outdated
|
||
.. math:: | ||
\frac{ | ||
\expand(C.\CTYPES[x]) = \TSTRUCT~(\MVAR~\X{st}) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
\expand(C.\CTYPES[x]) = \TSTRUCT~(\MVAR~\X{st}) | |
\expand(C.\CTYPES[x]) = \TARRAY~(\MVAR~\X{st}) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fixed.
Recursive Types | ||
~~~~~~~~~~~~~~~ | ||
|
||
*Recursive types* denote a group of mutually recursive :ref:`structured types <syntax-strtype>`, each of which can optionally declare a list of supertypes that it :ref:`matches <match-strtype>`. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
match-strtype
here, and a few others elsewhere (references to syntax-type-dyn
, syntax-type-aggregate
, valid-rectype
, match-deftype
) give "label undefined" warnings when I try to build the PDF, although I guess these are coming in one of the follow-up PRs?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, they come with #382.
@@ -255,6 +255,7 @@ | |||
.. |structtype| mathdef:: \xref{syntax/types}{syntax-structtype}{\X{structtype}} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
line 229 above (can't comment directly):
.. |TFINAL| mathdef:: \xref{syntax/types}{syntax-subtype}{\K{filan}}
should "filan" be "final"?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fixed.
document/core/syntax/types.rst
Outdated
.. note:: | ||
This definition computes an approximation of the reference type that is inhabited by all values from :math:`\X{rt}_1` except those from :math:`\X{rt}_2`. | ||
Since the type system does not have general union types, | ||
the defnition only affects the presence of null and cannot express the absence of other values. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
typo: "defnition"
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fixed.
document/core/valid/modules.rst
Outdated
|
||
.. math:: | ||
\frac{ | ||
C.\CTYPES[x] = \functype | ||
C.\CTYPES[x] = \TFUNC~\functype |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
should there be an expand
here, or is this covered by the todo below?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah, no, fixed.
document/core/valid/types.rst
Outdated
@@ -169,7 +169,7 @@ Block Types | |||
|
|||
.. math:: | |||
\frac{ | |||
C.\CTYPES[\typeidx] = [t_1^\ast] \toF [t_2^\ast] | |||
C.\CTYPES[\typeidx] = \TFUNC~[t_1^\ast] \toF [t_2^\ast] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
similarly, should there be an expand here?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fixed.
document/core/valid/instructions.rst
Outdated
|
||
* The :ref:`reference type <syntax-reftype>` :math:`\X{rt}` must be :ref:`valid <valid-reftype>`. | ||
|
||
* Then the instruction is valid with type :math:`[\X{rt}'] \to [\I32]` for any :ref:`valid <valid-reftype>` :ref:`reference type <syntax-reftype>` :math:`\X{rt}'` that :ref:`matches <match-reftype>` :math:`\X{rt}`. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I read \X{rt} \matchesreftype \X{rt}'
as "rt
matches rt'
". Is it ok that the prose states this relationship in the "opposite" direction (similar below)?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No, that was a bug. Fixed here and for ref.cast.
@@ -1491,6 +1924,84 @@ Control Instructions | |||
} | |||
|
|||
|
|||
.. _valid-br_on_cast: | |||
|
|||
:math:`\BRONCAST~l~\X{rt}_1~\X{rt}_2` |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do all of the below match the decisions made (or pending) in #381?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This PR reflects what's currently in MVP.md. Updating it is a separate action item blocked on #381.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
lgtm
Syntax of type definitions and validation rules for instructions, plus some adjustments for the syntax changes.
Does not yet specify how the type environment is populated with deftypes.