Cranelift: Rewrite or(and(x, y), not(y)) => or(x, not(y))

[fitzgen]

Thanks again to Souper for pointing this one out! cc @regehr

[fitzgen]

cc @itsrainy

[fitzgen]

Builds on top of #5673, only the last commit is relevant to this PR

[cfallin]

LGTM!

[avanhatt]

Our verifier prototype finds the following counterexample for this rule (lightly edited for readability):

simplify (lhs):
#x0000000000000000
#b0

bor (rhs):
#x0000000000000001
#b1

x:
#x0000000000000001
#b1

y:
#x0000000000000002
#b10

z:
#x0000000000000000
#b0

zk:
#x0000000000000000
#b0

[fitzgen]

I believe that this is because the if precondition is buggy. It is just checking whether the constructor succeeds or not, it is not checking if it returned true. Basically ignoring that predicate. (Funnily enough, because u64_eq is pure, the constructor will always succeed! This seems like something the ISLE compiler can check for and reject.) This is a pretty big foot gun with if, IMHO.

Anyways, the predicate needs to be rewritten as (if-let $true ...).

[jameysharp]

That's so cool! I don't understand it but it's awesome. 😆

Here's what's confusing me: The rule should only fire if zk is equal to !y. But in this counterexample, y is 2, so u64_not y is 0xfffffffffffffffd, but zk is 0. Is the verifier missing the if condition? Or is u64_not modeled incorrectly, maybe? (It's supposed to be bitwise-not, but this counterexample would make sense if that were modeled as boolean-not, turning non-zero values into 0.)

Also, what type is this counterexample for? I'd be especially interested if you can find counterexamples for I64 specifically, because I think the rule as-written is wrong for any other width. That said, I'd expect other widths to just fail to match the rule most of the time, rather than ever rewriting incorrectly, so if you find a narrower counterexample it's probably a real issue.

[jameysharp]

Ohhh, Nick's got it right. Although it's because u64_eq is not partial, not because it's pure. (Those flags are independent now.)

We also need to mask both constants down to the appropriate width if we want to make the rule fire on <64-bit types.

[avanhatt]

To restate what @fitzgen realized:

(if (u64_eq zk (u64_not y))) desugars to (if-let _ (u64_eq zk (u64_not y))), which ISLE is perfectly happy to match on. That is, the semantics for if is whether some match is possible, not whether the match is possible and its boolean value is truthy. The verifier models these weird semantics implicitly, since it treats if-let statements as constraints setting the LHS and RHS of the if-let clause to be equal---in this case, happily setting the wildcard to false and considering the rule to have matched.

Right now, this counterexample is for BVs of width 64, and the verifier is complaining that the rule is infeasible (that is, doesn't match) for other widths (which, based on your comment, seems correct?).