[spec] Add missing subtype rule for exn

[ShinWonho]

I noticed that subtype rule for exn appears to be missing.

I have added the rule.

[rossberg]

Thanks, this was indeed missing from the SpecTec formulation as well. I just added it there.

However, I also noticed that the rules for noexn and noextern are vacuous this way, since there is no other ht between the top and bottom type. So these two rules need to be noexn <: exn and noextern <: extern. Could you fix that for this PR as well?

[rossberg]

Thanks!

[ShinWonho]

I have a question.
I think the interpreter code should be changed accordingly.

(* current code *)
let rec match_heap_type c t1 t2 =
  match t1, t2 with
  ...
  | NoExnHT, t -> match_heap_type c t ExnHT
  | NoExternHT, t -> match_heap_type c t ExternHT

This code is current implementation of subtype of heap type.
And it should be fixed like below:

(* fixed code *)
let rec match_heap_type c t1 t2 =
  match t1, t2 with
  ...
  | NoExnHT, ExnHT -> true
  | NoExternHT, ExternHT -> true

Is it make sense?

[rossberg]

Yes, you are right. And there should be a test for it. Can I interest you in adding that? :)

[ShinWonho]

Sure! Actually, I'm currently working on testing subtypes. I'll create another PR for that.

[ShinWonho]

I realized that subtyping between noexn and exn, as well as between noextern and extern, already exists in test/core/ref_null.wast:

(module  
  ...  
  (global $nullexn nullexnref (ref.null noexn))  
  (global $nullextern nullexternref (ref.null noextern))  
  ...  
)

For these to be valid globals, ref.null noexn and ref.null noextern must have types nullexnref and nullexternref, respectively.
This holds due to the value typing relation:

• By null reference typing, ref.null noexn and ref.null noextern have types ref null noexn and ref null noextern.
• By subsumption, these types become ref null exn and ref null extern.

Thus, it tests subtyping between noexn and exn, as well as between noextern and extern, within subsumption.

Would you consider adding more test cases?

P.S. I noticed that null reference typing is missing the noexn case. I will add it.

[rossberg]

Ah, no, note that nullex[ter]nref is short for (ref null noex[ter]n), so these globals do not actually exercise any subtyping.

[ShinWonho]

Apologies, I provided the wrong example.
Here is the correct example for testing subtype in test/core/ref_null.wast 44-46:

  (global exnref (ref.null noexn))
  (global externref (ref.null noextern))

[rossberg]

Ah right, and actually, my earlier comment about the existing rules being vacuous was nonsense: they still work, by reducing the goal to reflexivity of the top type. Otherwise the interpreter would not have succeeded on these tests. :)

[ShinWonho]

In that case, would updating the interpreter code be sufficient?

[rossberg]

Not even that, the interpreter is alright already. We could also revert the change in the spec I asked you for, but both versions are correct.

[ShinWonho]

Oh, I see. Thanks for the comments!