Relax typing of classification instructions; opcode for dataref#184
Relax typing of classification instructions; opcode for dataref#184
Conversation
|
@manoskouk, PTAL. |
manoskouk
left a comment
manoskouk
left a comment
There was a problem hiding this comment.
LGTM with one comment.
proposals/gc/MVP.md
Outdated
| * `br_on_func <labelidx>` branches if a reference is a function | ||
| - `br_on_func $l : [anyref] -> [anyref]` | ||
| - iff `$l : [funcref]` | ||
| - `br_on_func $l : [(ref null ht)] -> [(ref null ht)]` |
There was a problem hiding this comment.
I think the typing of all br_on_* instructions, including br_on_cast, could be further refined to preserve their argument's nullability, similarly to ref.cast.
|
Ah, yes. I included that change, and simplified their typing rules. While at it, I also removed the explicit type index on those instructions, which is no longer consistent with the rest of the language. PTYAL. |
| - and `(type $t) <: ht` | ||
| * `ref.test` tests whether a reference value's [runtime type](#values) is a [runtime subtype](#runtime) of a given RTT | ||
| - `ref.test : [t' (rtt n? $t)] -> [i32]` | ||
| - iff `t' <: dataref` or `t' <: funcref` |
There was a problem hiding this comment.
I am just noticing: Don't we want to be able to cast references directly to concrete types without casting them to dataref or funcref first? If so, this should be ref.test : [anyref (rtt n? $t)] -> [i32], and similarly for ref.cast. In any case, t' <: (ref null data), or we need to make dataref == (ref null data).
There was a problem hiding this comment.
Ah, no, the purpose of introducing the separate classification instructions actually was to simplify the test/cast instructions, so that they only operate on references that are known to have an RTT. Otherwise their function would overlap with the classification instructions. See #150 for more context.
You are right about the null thing, fixed.
| - `br_on_cast $l : [t (rtt n? $t')] -> [t]` | ||
| - iff `$l : [t']` | ||
| - and `t <: dataref` or `t <: funcref` | ||
| - and `(ref $t) <: t'` |
There was a problem hiding this comment.
I think there are some aliased variables here. It should be:
br_on_cast $l : [t1 (rtt n? $t2)] -> [t1]
- iff
$l : [t3] - and
t1 <: (ref null data)ort1 <: funcref(instead,t1 <: anyrefif we go with the above suggestion) - and
(ref $t2) <: t3
There was a problem hiding this comment.
There was a typo in the last line, which should have been (ref $t') (fixed). But I think the others are correct, considering that $t' and t' are different names and in different categories.
rossberg
left a comment
rossberg
left a comment
There was a problem hiding this comment.
Thanks, I pushed a quick fix to the typos you point out.
| - and `(type $t) <: ht` | ||
| * `ref.test` tests whether a reference value's [runtime type](#values) is a [runtime subtype](#runtime) of a given RTT | ||
| - `ref.test : [t' (rtt n? $t)] -> [i32]` | ||
| - iff `t' <: dataref` or `t' <: funcref` |
There was a problem hiding this comment.
Ah, no, the purpose of introducing the separate classification instructions actually was to simplify the test/cast instructions, so that they only operate on references that are known to have an RTT. Otherwise their function would overlap with the classification instructions. See #150 for more context.
You are right about the null thing, fixed.
2 participants
Addresses #180 and #183.