Stream: git-wasmtime

Topic: wasmtime / issue #6095 ISLE: rewrite `and`/`or` of `icmp`

Wasmtime GitHub notifications bot (Mar 24 2023 at 01:39):

jameysharp commented on issue #6095:

I think we can factor these rules in a different way to reduce a bunch of the duplication. But I haven't figured out the details. I was fiddling with ideas like the following, though I'm not sure if this actually turns out any shorter:

(decl pure partial eq_implies (Value Value Value) bool)
(rule (eq_implies x y (eq x y)) $true)
(rule (eq_implies x y (eq y x)) $true)
(rule (eq_implies x y (ule x y)) $true)
(rule (eq_implies x y (uge x y)) $true)
(rule (eq_implies x y (sle x y)) $true)
(rule (eq_implies x y (sge x y)) $true)
(rule (eq_implies x y (ne x y)) $false)
(rule (eq_implies x y (ne y x)) $false)
(rule (eq_implies x y (ult x y)) $false)
(rule (eq_implies x y (ugt x y)) $false)
(rule (eq_implies x y (slt x y)) $false)
(rule (eq_implies x y (sgt x y)) $false)

(decl pure partial ult_implies (Value Value Value) bool)
(rule (ult_implies x y (eq x y)) $false)
(rule (ult_implies x y (eq y x)) $false)
(rule (ult_implies x y (ne x y)) $true)
(rule (ult_implies x y (ne y x)) $true)
(rule (ult_implies x y (ult x y)) $true)
(rule (ult_implies x y (ule x y)) $true)
(rule (ult_implies x y (uge x y)) $false)
(rule (ult_implies x y (ugt x y)) $false)

(rule (simplify (band ty (eq x y) other))
  (if-let $true (eq_implies x y other))
  (subsume (iconst ty 1)))

(rule (simplify (band ty other (eq x y)))
  (if-let $true (eq_implies x y other))
  (subsume (iconst ty 1)))

(rule (simplify (band ty (eq x y) other))
  (if-let $false (eq_implies x y other))
  (subsume (iconst ty 0)))

Wasmtime GitHub notifications bot (Mar 24 2023 at 02:16):

Kmeakin commented on issue #6095:

I think we can factor these rules in a different way to reduce a bunch of the duplication. But I haven't figured out the details. I was fiddling with ideas like the following, though I'm not sure if this actually turns out any shorter:

I think this would work out to being basically the same length. We could remove half the cases by adding rules to make band and bor commutative. Not sure if that would lead to a performance penalty though.

Wasmtime GitHub notifications bot (Mar 26 2023 at 08:06):

jameysharp commented on issue #6095:

I've been unable to let go of this and just enjoy my weekend, so:

Can we do it this way? Decompose both condition codes into separate "less than", "equal to", and "greater than" booleans, then pairwise apply "and"/"or" to the booleans according to whether the comparisons were combined with band or bor, and finally compose the booleans back into a condition code.

(decl pure decompose_intcc (IntCC) u64)
(rule (decompose_intcc IntCC.Equal) 1)
(rule (decompose_intcc IntCC.UnsignedLessThan) 2)
(rule (decompose_intcc IntCC.UnsignedLessThanOrEqual) 3)
(rule (decompose_intcc IntCC.UnsignedGreaterThan) 4)
(rule (decompose_intcc IntCC.UnsignedGreaterThanOrEqual) 5)
(rule (decompose_intcc IntCC.NotEqual) 6)

(decl pure partial compose_intcc (u64) IntCC)
; inverse of `decompose_intcc`

(rule (simplify (band ty (icmp ty cc1 x y) (icmp ty cc2 x y)))
  (if-let cc (compose_intcc (u64_and (decompose_intcc cc1) (decompose_intcc cc2))))
  (icmp ty cc x y))
(rule (simplify (band ty (icmp ty cc1 x y) (icmp ty cc2 x y)))
  (if-let 0 (u64_and (decompose_intcc cc1) (decompose_intcc cc2)))
  (subsume (iconst ty (imm64 0))))

(rule (simplify (bor ty (icmp ty cc1 x y) (icmp ty cc2 x y)))
  (if-let cc (compose_intcc (u64_or (decompose_intcc cc1) (decompose_intcc cc2))))
  (icmp ty cc x y))
(rule (simplify (bor ty (icmp ty cc1 x y) (icmp ty cc2 x y)))
  (if-let 7 (u64_or (decompose_intcc cc1) (decompose_intcc cc2)))
  (subsume (iconst ty (imm64 1))))

That doesn't handle signedness but I think fixing that shouldn't be too much more involved.

Adding the cases where one of the comparisons has its operands flipped (icmp ty cc2 y x) should be easy to handle this way too; we just need to use intcc_reverse on cc2.

Also I think this extends in the obvious way to xor, which may not be important but seems nice to have.

Wasmtime GitHub notifications bot (Mar 26 2023 at 18:09):

jameysharp commented on issue #6095:

The signedness condition can work in a similar way:

(decl pure intcc_class (IntCC) u64)
(rule (intcc_class IntCC.UnsignedLessThan) 0b01)
(rule (intcc_class IntCC.UnsignedLessThanEqual) 0b01)
(rule (intcc_class IntCC.UnsignedGreaterThan) 0b01)
(rule (intcc_class IntCC.UnsignedGreaterThanEqual) 0b01)
(rule (intcc_class IntCC.SignedLessThan) 0b10)
(rule (intcc_class IntCC.SignedLessThanEqual) 0b10)
(rule (intcc_class IntCC.SignedGreaterThan) 0b10)
(rule (intcc_class IntCC.SignedGreaterThanEqual) 0b10)
(rule (intcc_class IntCC.Equal) 0b11)
(rule (intcc_class IntCC.NotEqual) 0b11)

(decl pure intcc_comparable (IntCC IntCC) Unit)
(rule (intcc_comparable x y)
  (if-let (u64_nonzero _) (u64_and (intcc_class x) (intcc_class y)))
  (unit))

Then add (if-let _ (intcc_comparable cc1 cc2)) to the simplify rules that I wrote out earlier.

The decompose_intcc rules might be easier to understand with binary literals instead of decimal, too: Equal is 0b001, LessThan is 0b010, LessThanOrEqual is 0b011, etc. At the least all of this needs comments identifying which bit means what; I just wanted to write it out quickly to illustrate the idea.

Wasmtime GitHub notifications bot (Mar 26 2023 at 18:41):

cfallin commented on issue #6095:

That's a really incredibly neat way of seeing the rewrite!

I was trying to work out for myself why it should work, since it's non-obvious (at least to me!) why AND of the bitfield representation should be AND of the icmp results. I think both OR and AND work because of the following (let's take just unsigneds for now):

• An IntCC condition is a disjunction (OR) of up to three "fundamental" comparisons: e.g. UnsignedLessThanOrEqual is logically LessThan OR Equal.
• As such, your three-bit encoding could be seen as a Boolean polynomial that describes the icmp result. Take x := LT, y := EQ, z: GT, then one might have icmp(..) = x + y (011) or icmp(..) = x + z (101) or just icmp(..) = y (010).
• The OR of the icmp results is then the OR of these polynomials, and Boolean logic tells us that they add in exactly the way that the OR of the bitfield representation would give us. So if result = icmp(cc1, ..) + icmp(cc2, ..) and we have the substitutions result = (x + y) + (x + z), then we get result = x + y + z and convert that back into a condition code.
  • Incidentally, x + y + z here reduces to constant true which corresponds to your special-case rule for 7!
• The AND is where it gets interesting! This looks like: result = icmp(cc1, ..) * icmp(cc2, ..) = (x + y) * (x + z), and AND distributes over OR so we can do the binomial expansion x*x + x*z + y*x + y*z, then use identities (x AND x = x) and a fact about our inputs, namely that x, y, and z are disjoint (x AND z = 0, y AND z = 0, x AND y = 0), to realize that the simplified product x is exactly the sum of terms that appear in both sides of the product. That's the bitwise AND.

The above line of reasoning doesn't quite work directly for XOR (XOR does not distribute over OR in general) but I think given the disjointness property one could argue that it does in this case.

Wasmtime GitHub notifications bot (Mar 26 2023 at 20:14):

jameysharp commented on issue #6095:

That's a nice way to prove it! I was thinking about it differently, by conditioning on the actual relationship between the inputs. For example, assume that x is less than y. Then and-of-icmp is true iff both icmp conditions include less-than. Similar reasoning applies to the case where x is equal to y, for any other boolean operator, and so on.

On further thought I think there are even more concise ways to factor this:

(decl pure partial intcc_comparable (IntCC IntCC) bool)
(rule (intcc_comparable x y)
  (if-let (u64_nonzero class) (u64_and (intcc_class x) (intcc_class y)))
  (u64_eq 0b10 class))

(decl pure compose_icmp (Type u64 bool Value Value) Value)
(rule (compose_icmp ty 0 _ _ _) (subsume (iconst ty (imm64 0))))
(rule (compose_icmp ty 1 _ x y) (icmp ty IntCC.Equal x y))
(rule (compose_icmp ty 2 $false x y) (icmp ty IntCC.UnsignedLessThan x y))
(rule (compose_icmp ty 2 $true x y) (icmp ty IntCC.SignedLessThan x y))
; ...
(rule (compose_icmp ty 6 _ x y) (icmp ty IntCC.NotEqual x y))
(rule (compose_icmp ty 7 _ _ _) (subsume (iconst ty (imm64 1))))

(rule (simplify (band ty (icmp ty cc1 x y) (icmp ty cc2 x y)))
  (if-let signed (intcc_comparable cc1 cc2))
  (compose_icmp ty (u64_and (decompose_intcc cc1) (decompose_intcc cc2)) signed x y))

(rule (simplify (bor ty (icmp ty cc1 x y) (icmp ty cc2 x y)))
  (if-let signed (intcc_comparable cc1 cc2))
  (compose_icmp ty (u64_or (decompose_intcc cc1) (decompose_intcc cc2)) signed x y))

Wasmtime GitHub notifications bot (Mar 28 2023 at 01:05):

Kmeakin commented on issue #6095:

Thank you @jameysharp and @cfallin. I have updated the patch with your contributions

Wasmtime GitHub notifications bot (Mar 28 2023 at 01:30):

jameysharp commented on issue #6095:

Nice! This means the changes to prelude.isle and the various corresponding Rust sources are no longer necessary, right?

I meant to ask before: could you commit the script you used to generate the tests too? We have precedent for that in cranelift/filetests/filetests/wasm/load-store/make-load-store-tests.sh.

Also, I guess now we need to either merge #6111 before finishing this PR, or decide we want these tests to not check the full output and back out the precise-output changes. I haven't thought about this enough to have an opinion on that question yet.

Wasmtime GitHub notifications bot (Mar 28 2023 at 01:42):

Kmeakin commented on issue #6095:

Nice! This means the changes to prelude.isle and the various corresponding Rust sources are no longer necessary, right?

Good point, I forgot to remove those

I meant to ask before: could you commit the script you used to generate the tests too? We have precedent for that in cranelift/filetests/filetests/wasm/load-store/make-load-store-tests.sh.

I used a rust program but I can convert it to a shell script

Also, I guess now we need to either merge #6111 before finishing this PR, or decide we want these tests to not check the full output and back out the precise-output changes. I haven't thought about this enough to have an opinion on that question yet.

I would prefer to wait for #6111

Wasmtime GitHub notifications bot (Mar 28 2023 at 01:50):

jameysharp commented on issue #6095:

You can remove the changes in cranelift/codegen/src/ir/condcodes.rs too, right?

And the changes in cranelift/codegen/src/isle_prelude.rs aren't necessary; I think I prefer the existing way. If somebody added a condition code for some reason, using a wildcard match here hides potential bugs.

Last updated: Dec 23 2024 at 12:05 UTC