Predicates on patterns

[stoklund]

Suppose we want to compare 8-bit ints on a 32-bit RISC:

widen32.legalize(
    a << icmp('ult', x, y),
    Rtl(
        wx << uextend.i32(x),
        wy << uextend.i32(y),
        a << icmp('ult', wx, wy),
    ))

We want to generalize this pattern, but this transformation is only valid for the unsigned or sign-neutral condition codes, so this is wrong:

widen32.legalize(
    a << icmp(cc, x, y),
    Rtl(
        wx << uextend.i32(x),
        wy << uextend.i32(y),
        a << icmp(cc, wx, wy),
    ))

We need a way of specifying a predicate on the immediate cc. Ideally, this mechanism should share representation with the instruction predicates already supported by instruction encodings.

(Also note that the first example doesn't work either—we can't even require a fixed immediate value in the input pattern.)

[d1m0]

This could also be useful for specifying the semantics of instructions like icmp. For example, one way to specify the semantics of icmp is by having a separate transform for each concrete condition code. E.g.:

icmp.set_semantics(
    (c << icmp(ult, x, y),
     Rtl(...
         bvc << bvult (bvx, bvy),
         ...)),
    (c << icmp(eq, x, y),
     Rtl(...
         bvc << bveq (bvx, bvy),
         ...)),
...

This is a little simpler since SMTLIB doesn't have a single bvcmp with condition codes, but has separate functions for each comparison. It is simpler to show this mapping from condition codes -> bv comparison functions directly in the semantics specification, rather than adding our own 'bvcmp' and hiding the mapping inside smtlib.py

[stoklund]

I just landed a change that enables parts of this. See Apply.inst_predicate. This currently supports bound type variables and concrete constant values for immediate operands.

[bjorn3]

The new backend framework doesn't use legalizations as much as the old backend.