wasmtime / PR #5676 Cranelift: Rewrite `or(and(x, y), not... · git-wasmtime

Stream: git-wasmtime

Topic: wasmtime / PR #5676 Cranelift: Rewrite `or(and(x, y), not...

Wasmtime GitHub notifications bot (Jan 31 2023 at 20:59):

fitzgen opened PR #5676 from or-and-y-with-not-y to main:

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

Wasmtime GitHub notifications bot (Jan 31 2023 at 20:59):

fitzgen requested cfallin for a review on PR #5676.

Wasmtime GitHub notifications bot (Jan 31 2023 at 21:20):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Jan 31 2023 at 21:28):

fitzgen updated PR #5676 from or-and-y-with-not-y to main.

Wasmtime GitHub notifications bot (Jan 31 2023 at 21:29):

fitzgen has enabled auto merge for PR #5676.

Wasmtime GitHub notifications bot (Jan 31 2023 at 21:30):

jameysharp submitted PR review.

Wasmtime GitHub notifications bot (Jan 31 2023 at 21:30):

jameysharp submitted PR review.

Wasmtime GitHub notifications bot (Jan 31 2023 at 21:30):

jameysharp created PR review comment:

I think there's an equivalent version of this rule where the bnot is inside the band, and the operand to bor is the uninverted value.

Wasmtime GitHub notifications bot (Jan 31 2023 at 21:30):

jameysharp created PR review comment:

Could you duplicate the egraph filetests so there's a second version of each one with the operands to bor flipped? I suspect some of these will pass but maybe not all of them.

Wasmtime GitHub notifications bot (Jan 31 2023 at 21:30):

jameysharp created PR review comment:

Do the check lines do anything in runtests?

Wasmtime GitHub notifications bot (Jan 31 2023 at 21:50):

fitzgen has disabled auto merge for PR #5676.

Wasmtime GitHub notifications bot (Jan 31 2023 at 21:58):

fitzgen updated PR #5676 from or-and-y-with-not-y to main.

Wasmtime GitHub notifications bot (Jan 31 2023 at 21:58):

fitzgen submitted PR review.

Wasmtime GitHub notifications bot (Jan 31 2023 at 21:58):

fitzgen created PR review comment:

We talked, decided this was one rabbit hole too deep.

Wasmtime GitHub notifications bot (Jan 31 2023 at 21:59):

fitzgen has enabled auto merge for PR #5676.

Wasmtime GitHub notifications bot (Jan 31 2023 at 22:44):

fitzgen merged PR #5676.

Wasmtime GitHub notifications bot (Feb 01 2023 at 17:34):

avanhatt submitted PR review.

Wasmtime GitHub notifications bot (Feb 01 2023 at 17:34):

avanhatt created PR review comment:

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

Wasmtime GitHub notifications bot (Feb 01 2023 at 17:53):

fitzgen submitted PR review.

Wasmtime GitHub notifications bot (Feb 01 2023 at 17:53):

fitzgen created PR review comment:

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

Wasmtime GitHub notifications bot (Feb 01 2023 at 18:10):

jameysharp submitted PR review.

Wasmtime GitHub notifications bot (Feb 01 2023 at 18:10):

jameysharp created PR review comment:

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

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.

Wasmtime GitHub notifications bot (Feb 01 2023 at 18:15):

jameysharp submitted PR review.

Wasmtime GitHub notifications bot (Feb 01 2023 at 18:15):

jameysharp created PR review comment:

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.

Wasmtime GitHub notifications bot (Feb 01 2023 at 18:16):

avanhatt created PR review comment:

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 matches these weird semantics, since it treats if-let statements as constraints setting the LHS and RHS of the statement 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?).

Wasmtime GitHub notifications bot (Feb 01 2023 at 18:16):

avanhatt submitted PR review.

Wasmtime GitHub notifications bot (Feb 01 2023 at 18:19):

avanhatt edited PR review comment.

Last updated: Nov 22 2024 at 16:03 UTC