Uniqueness types in ISLE

[elliottt]

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:

(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 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:

(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. 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:

(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.

[fitzgen]

I think having implicit conversions for anything that has side effects is probably not the right call, so I think actually just removing the Value to Reg etc conversions would be sufficient, and also a whole lot easier.

[elliottt]

That's a good point. The only downside that I can see there is that we'd need to be really careful that we were always introducing the RegMem variants when it makes sense, but that seems pretty manageable.

[cfallin]

@elliottt and I talked about this a bit, and I definitely agree that this is sufficient; the main downside though is that we're getting away from the very clean (rule (lower (iadd a b)) (x64_add a b))-style rules we had. Perhaps less magic is warranted here, indeed. I wonder if removing the sink_inst implicit converter (so the implicit conversions for memory operands) is enough, while leaving Value->Reg intact. (I can convince myself if I squint right that "get the register for a value" is an idempotent operation, which we allow for implicit conversions, while "sink the load" is an operation that includes the side-effect of disallowing one to use the original result register, so should not be an implicit conversion.)

All of that said, there is still a safety issue here where it is possible to write a rule that does both, while affine types allow us to encode the restriction directly. I like that as an aspirational goal, but maybe we don't have to get there in one step.