Clarifying ref.is_null matching validation #547
-
|
I'd like to understand the following excerpt:
does (ref null bot) -> (i32) |
Beta Was this translation helpful? Give feedback.
Replies: 1 comment 1 reply
-
|
The type bot is a valid heap type — and (ref null bot) hence a valid reference type — so the rule would allow picking it. However, that choice usually isn't useful as an input type, since there are no actual values of that type and hence this would normally not allow successfully typing an instruction sequence in which this instruction occurs. You need something that is a supertype of the actual operand type, not a subtype. In the usual algorithmic implementation of validation, you always know what's on the operand stack, so you just take that type directly. See the spec's Appendix for an implementation sketch. |
Beta Was this translation helpful? Give feedback.
-
|
Cheers for clarification, especially the algorithm as I didn't know that existed and was purely working off the primary validation section of the spec (and trying to reverse engineer the ocaml interpreter 😅 ). Interestingly I have (somehow) arrived at a similar algorithm to what the spec describes, the difference is I statically resolve an instructiontype for each instruction and have a function which takes the context and a stream of instruction types and does the checking against the op stack. The problem I'm having is that my implement of instructiontype follows the spec literally and is a tuple of resulttypes, and the value types in these result types are unable to encode the concept of top and thus communicate to the function that we should accept any heap type. I guess I could add top to my encoding 🤔 but maybe I'm going to bump into more problems with this impl later down the line |
Beta Was this translation helpful? Give feedback.
The type bot is a valid heap type — and (ref null bot) hence a valid reference type — so the rule would allow picking it. However, that choice usually isn't useful as an input type, since there are no actual values of that type and hence this would normally not allow successfully typing an instruction sequence in which this instruction occurs. You need something that is a supertype of the actual operand type, not a subtype.
In the usual algorithmic implementation of validation, you always know what's on the operand stack, so you just take that type directly. See the spec's Appendix for an implementation sketch.