This repository was archived by the owner on Nov 3, 2021. It is now read-only.
Repository navigation
This repository was archived by the owner on Nov 3, 2021. It is now read-only.
Typeability Bug in Reference Implementation #111
Description
If I'm reading this code correctly, the reference interpretation incorrectly accepts this invalid instruction sequence:
(unreachable)
(select)
(ref.is_null funcref) ;; specific reference type doesn't matter
The issue is that select is polymorphic with respect to numeric types only. So while the result type of select after unreachable is unknown, it must at least be a numeric type. As such, it cannot be used for any instruction expecting a reference type.
The reference interpreter seems to fail to incorporate this reasoning. Instead of using value_type option, the reference interpreter seems to need to use an ADT with an additional nullary case that represents only unknown numeric types.
Activity
rossberg commentedon Sep 16, 2020
Good catch. This actually is another fall-out from our removal of subtyping. :( (Formerly, unreachable was typed with bottom, such that it was correct to accept this.)
RossTate commentedon Sep 16, 2020
Oh whoa, I never even realized there had been a bottom value type. (It wasn't mentioned in the overview.) That causes problems as well.
rossberg commentedon Sep 16, 2020
It was purely a spec-internal type, not expressible in the program itself. I actually mentioned it to you some time ago, and you didn't see any issues. See my presentation from the June '19 F2F meeting for the motivation.
RossTate commentedon Sep 16, 2020
I understand. There's a difference between a bottom value type and a bottom state/result type. I thought you were referring to the latter concept. Sorry for the misunderstanding.
rossberg commentedon Sep 30, 2020
Closed via #116.