bytecodealliance / bytecodealliance/wasmtime
Uniqueness types in ISLE
- Dominant language
- Rust
- Stars
- 18.6k
- Forks
- 1.8k
- Avg merge
- 1d 18h
- Merged PRs (30d)
- 126
Description
#### Feature
When working on lowerings in ISLE, it's convenient to rely on implicit conversions to de-clutter the implementation. However this can hide bugs, as in the following example:
```scheme
(decl x64_palignr (Xmm XmmMem u8 OperandSize) Xmm)
(convert Value Xmm put_in_xmm)
(convert Value XmmMem put_in_xmm_mem)
(decl swiden_high (Value) Inst)
(extractor
(swiden_high x)
(inst_data (InstructionData.Unary (Opcode.SwidenHigh) x))
)
(rule (lower (has_type $I16X8 (swiden_high val @ (value_type $I8X16))))
(x64_pmovsxbw (x64_palignr val val 8 (OperandSize.Size32))))
```
In this example, `val` has type `Value`, but is used with `x64_palignr` at two different types: `Xmm` and `XmmMem`. Defined elsewhere are two conversions, one from `Value -> Xmm` and one from `Value -> XmmMem` that will potentially sink a load into this use if the `Value` is only used once at the clif level. Because the `swiden_high` instruction has only one argument, using it twice in its lowering could produce a bug where `val` is sunk into the `XmmMem` arg and also used as the `Xmm` argument, yielding a panic during register allocation.
One approach to solving this problem would be to not permit a `Value` to be converted into an `Xmm` or `XmmMem` more than one time. This could be accomplished by adding an annotation to arguments to ISLE declarations, indicating which arguments must be used uniquely. The [clean language](https://www.mbsd.cs.ru.nl/publications/papers/cleanbook/CleanBookI.pdf) uses `!` for this, so you could imagine the signature of the `swiden_high` extractor changing to the following to indicate that `Value` may only be used once:
```scheme
(decl swiden_high (!Value) Inst)
(extractor
(swiden_high x)
(inst_data (InstructionData.Unary (Opcode.SwidenHigh) x))
)
```
Another approach would be to allow functions to be marked as explicitly consuming their inputs from the typing environment, using an annotation like in the [Mezzo language](http://gallium.inria.fr/blog/introduction-to-mezzo/). In this case we would want to mark both `put_in_xmm` and `put_in_xmm_mem` as consuming their arguments, so let's use `@` as a straw-man sigil:
```scheme
(decl put_in_xmm (@Value) Xmm)
(decl put_in_xmm_mem (@Value) XmmMem)
```
We would get two benefits from this approach: we could call other functions on `val` before it was used with either of the functions that convert it to an `Xmm` or `XmmReg`, and it would be an error to try to call both of those functions on the same value. The initial example of `(x64_palignr val val ...)` would become a type error, as the two uses of `val` would lead to independent applications of `put_in_xmm` and `put_in_xmm_mem`, both of which consume their arguments.
#### Benefit
Adding some form of uniqueness typing to ISLE would help us to avoid bugs where the api has a notion of uniqueness that right now must be preserved manually. In the case of the example above, this would help us to enforce that sinking a load into another instruction does not lead to situations where the result of that original load is also expected to be in a register.
#### Alternatives
We can add assertions to require that we respect the invariants of the underlying apis that the ISLE code interacts with, or refactor those underlying apis to track sinkable loads on the vcode instead of the clif.
Contributor guide
Assessment
This issue has not been assessed yet.