You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
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.
With subtyping, and lacking sufficient type annotations, some operations may require the validation algorithm to compute the least upper bound (lub) or greatest lower bond (glb) of two types to accurately infer an output or input type, respectively. In current Wasm, this comes up with two instructions:
select: the result type is the lub of the two operand types
br_table: the operand type is the glb of the label types
(Similar issues would come up with ops like dup or pick, which might also require a glb of the use edges when the input type is not known a priori, i.e., in unreachable code.)
While lub and glb are easy to compute with the tiny subtyping lattice introduced by this proposal itself, it will not stay that way with future reference extensions (e.g., typed functions or GC types), which will make it both more complex and more costly. In accordance with the design goals for Wasm validation, we should make sure to avoid the need for computing lubs/glbs altogether.
Possible Solution:
For select, the only option seems to be introducing a new type-annotated version, and restricting the pre-existing unannotated version to numeric types for backwards compatibility (fortunately, only trivial subtyping is available on numeric types).
Without going into technical details, the glb cases (br_table, dup, pick) can most easily be avoided by adding a bottom type to the type system (a least type in the subtype lattice). Effectively, this is already present in the MVP validation algorithm, to type unreachable stack slots; promoting it to a proper type itself is a natural generalisation in the presence of subtyping. (Note that this type doesn't need not to be expressible in programs, it's sufficient if it exists in the typing rules.)
restricting the pre-existing unannotated version to numeric types for backwards compatibility (fortunately, only trivial subtyping is available on numeric types).
Just to make this clearer for the broader audience: trivial subtyping for numeric types in wasm means no subtyping between any of the numeric types: there are no implicit conversions or subsumption.
@titzer, right, with the one exception that, technically, a bottom type would of course be a subtype of all numeric types. But that's what actually makes this work.
Activity
titzer commentedon May 8, 2019
I am on board with the proposed solution here.
Just to make this clearer for the broader audience: trivial subtyping for numeric types in wasm means no subtyping between any of the numeric types: there are no implicit conversions or subsumption.
rossberg commentedon May 8, 2019
@titzer, right, with the one exception that, technically, a bottom type would of course be a subtype of all numeric types. But that's what actually makes this work.
Bug 1561513 - Wasm: Restrict existing select instruction to numeric t…
Bug 1561513 - Wasm: Add bottom type and tweak validation algorithm. r…
Bug 1561515 - Wasm: Add typed select instruction. r=lth
Bug 1561513 - Wasm: Restrict existing select instruction to numeric t…
Bug 1561513 - Wasm: Add bottom type and tweak validation algorithm. r…
Bug 1561515 - Wasm: Add typed select instruction. r=lth
Bug 1561513 - Wasm: Restrict existing select instruction to numeric t…
Bug 1561513 - Wasm: Add bottom type and tweak validation algorithm. r…
Bug 1561515 - Wasm: Add typed select instruction. r=lth
Bug 1561513 - Wasm: Restrict existing select instruction to numeric t…
Bug 1561513 - Wasm: Add bottom type and tweak validation algorithm. r…
Bug 1561515 - Wasm: Add typed select instruction. r=lth
Bug 1561513 - Wasm: Restrict existing select instruction to numeric t…
Bug 1561513 - Wasm: Add bottom type and tweak validation algorithm. r…
Bug 1561515 - Wasm: Add typed select instruction. r=lth
Add new `DataCount` section (#42)
rossberg commentedon Nov 23, 2019
Was fixed by $43.