[interpreter] Descriptor type validation - #66
Conversation
| let DescT (ut1, ut2, ct) = dt in | ||
| let DescT (ut1', ut2', ct') = dt' in | ||
| match ut1, ut1' with | ||
| | (Some ut1, Some ut1') -> |
There was a problem hiding this comment.
@rossberg, I'm trying to validate that if dt <: dt', then we also have ut1 <: ut1', where ut1 and ut1' are the types described by dt and dt'.
I have this working in some cases, but it's super ugly and it breaks in other cases. Specifically, the idx_of_typeuse ut on line 178 fails when the four types are all in the same rec group because in that case it is a Rec rather than an idx.
Do you have a suggestion about how to do these checks more generally and cleanly?
There was a problem hiding this comment.
Oh yes, defining that isn't going to be straightforward, due to all the mutual recursion going on. I'll probably have to think about it. Unfortunately, I just arrived at ICFP/OOPSLA today, so might lack the quiet moment this week and the next. But yeah, assuming you can extract indices is not going to work.
Check that descriptor and described types are properly paired, are structs, and follow the subtyping rules.
589cc59 to
ace53e5
Compare
|
@rossberg, this works now and is ready for review. |
|
Landing now to be able to use the tests downstream, but happy to address any feedback in a follow-up. |
| | (None, None) -> (); | ||
| match ut2, ut2' with |
There was a problem hiding this comment.
I think you fell for one of OCaml's syntax traps: this doesn't mean what you probably think it does. You want to put some parens around the prior match, otherwise this match is just part of the last branch.
So currently, the conditions on ut2/ut2' are not actually checked in the presence of a descriptor clause, nor the ones on ct/ct'. That may also suggest that we lack sufficient negative tests.
| | (Some _, None) | (None, None) -> (); | ||
| require (match_comptype c.types ct ct') at ("sub type " ^ I32.to_string_u x ^ |
| match_heaptype c (UseHT (Inexact, ut1)) (UseHT (Inexact, (Def dt2))) | ||
| ) uts1 | ||
|
|
||
| let match_typeuse c ut1 ut2 (rt1 : rectype) (rt2 : rectype) = |
There was a problem hiding this comment.
Passing in the rectypes looks like a hack to me. Any such side information should rather come from the context.
In the formal rules (e.g. in SpecTec), the context has another component recs, which bind recusive type indices. So far, this wasn't needed in the interpreter, as it was only needed to validate rolled deftypes, which only occurs in the soundness proof. Hence the interpreter omits it. But perhaps a version of this is what's needed here?
But I'm rather confused why that should be the case. Where are the rec type indices actually coming from that can enter this function? AFAICS, all calls either use unrolled or not yet rolled arguments, so I would expect no rec type index to occur. If you asserted false for them, would this fail?
There was a problem hiding this comment.
Indeed, it looks like everything still works out if the Rec i cases assert false. I guess I didn't consider that it would be ok for match_typeuse to be partial, and therefore had to pass rt1 and rt2 in to handle the recursive cases.
I am very curious about what the rest of this sentence will be :) |
Update `check_desctype_sub` with the feedback from #66.
Ha, it probably was something like "I'm not sure if the Rec case should be needed", but then I decided to put that inline. :) |
Update `check_desctype_sub` with the feedback from #66.
2 participants
Check that descriptor and described types are properly paired, are
structs, and follow the subtyping rules.