re-strengthen output null knowledge in cast instructions #347
Conversation
intended to address remaining concerns in #342
|
This PR reverts to the old formulations of the |
|
Unfortunately I'm on vacation away from my main setup and can't add/run tests. Happy for someone else to take over this PR if tests would be a blocker. |
|
@conrad-watt, would you be able to add a TODO about implementing and testing these new rules once the type annotation discussion in #342 is resolved? Given the discussion today, I think that would be enough to get this landed. |
|
done |
There was a problem hiding this comment.
Please do not land this without sync'ing up tests and reference interpreter, as I normally do with changes like this. This is very complicated and we'll need good test coverage to proceed with it.
Note that this also makes us lose principal types, AFAICS, see comment below. I'm not sure yet how I feel about that.
| - `ref.cast null? ht : [(ref null ht')] -> [(ref null? ht)]` | ||
| - iff `ht <: tht` and `ht' <: tht` where `tht` is a common super type |
There was a problem hiding this comment.
| - `ref.cast null? ht : [(ref null ht')] -> [(ref null? ht)]` | |
| - iff `ht <: tht` and `ht' <: tht` where `tht` is a common super type | |
| - `ref.cast null? ht : [(ref null ht')] -> [(ref null2? ht)]` | |
| - iff `ht <: tht` and `ht' <: tht` where `tht` is a common super type | |
| - and `null? = null2?` |
(Uses of ? are independent per se, they need to be forced equal explicitly.)
| - and `rt <: trt` and `rt' <: trt` for some `trt` | ||
| - and `(ref null4? ht) <: t'` | ||
| - and `ht <: tht` and `ht' <: tht` where `tht` is a common super type | ||
| - and `null? = null4? =/= null2? \/ null2? = null3? = null4? = epsilon` |
There was a problem hiding this comment.
Wow, this is pretty complicated. I had to write out the full matrix to understand what a forward validation algorithm would have to do:
t' null null3 null2 null4
0 0 0 _ 0
0 0 1 1 0
0 1 0 0 0
0 1 1 invalid
1 0 0 _ 0
1 0 1 1 0
1 1 0 0 _
1 1 1 0 1
where _ means undetermined, in the case of null2 that implies picking 0 as principal. We need good test coverage for this.
This is even more complex if you didn't do a forward algorithm. In particular, there are no principal types in general, i.e., without having null3. I have to say that I feel uncomfortable about that.
There was a problem hiding this comment.
I wonder if there isn't a cleaner way to express the side conditions in terms of meets/joins on nullability?
There was a problem hiding this comment.
Can you explain more about what you mean about principal types and non-forward algorithms here?
There was a problem hiding this comment.
@tlively, in a type system with subtyping you usually want the principal types property, i.e., the property that, given an environment for identifiers, any expression (correspondingly, an instruction sequence in Wasm) has a most precise type. With the above rule for null that is no longer the case: e.g., (br_on_cast $l $t) where $l : (ref $t) has two possible types, (ref $t) -> (ref $t) and (ref null $t) -> (ref null $t), neither of which is more precise than the other. You'll need to already know either the input or the output type to decide. When you do full "forward" validation like in engine you have the former, but that's not necessarily the case in other circumstances or tools doing static analysis.
So, yeah, this is in fact exactly the same problem as with the missing heap type annotation. I was wrong in the meeting when I said that we wouldn't need to annotate the null flag for the source type. If we want to fix the annotation problem, we need two ref types, not just two heap types. Something like:
- `br_on_cast $l rt1 rt2 : [t0* rt1] -> [t0* rt1']`
- iff `$l : [t0* t']`
- and `rt2 <: t'`
- and `rt1 <: trt` and `rt2 <: trt` where `trt` is a common super type
- and `rt1 = null1? ht1` and `rt2 = null2? ht2` and `rt1' = (null1? /\ ~null2?) ht1'`
There was a problem hiding this comment.
Thanks, that makes sense. I guess it would be nice in principle to always have a principle type so that an optimization like outlining could uniquely determine a function type to assign to outlined code fragments. But on the other hand, an optimizer/analyzer could also easily work around the lack of type annotations by looking at the context. In fact, we'll have to (and want to!) do this workaround in Binaryen anyway since we intentionally do not preserve these accessor type annotations in our IR.
|
After some subsequent discussions (notably #381), this PR is now stale. |
intended to address remaining concerns in #342