[Cranelift] (x * y) (==/!=) z --> x (==/!=) (y / z)

[bongjunj]

This add the optimization of (x * y) (==/!=) z --> x (==/!=) (y / z).
y must be odd and divides z for the rule to be correct.

[cfallin]

Could you add "and y and z are constant" to the description here? Otherwise this reads as a fairly odd optimization that is replacing a multiply with a divide, which would ordinarily reduce performance.

Also: why is it necessary that y is odd? Is that because we need it to be mutually prime with the ring's modulus (2^n) so the product doesn't collapse to zero?

[bongjunj]

I've changed the description so that one can read that the division happens in compile time.
Also, the solution X for X * C = D is not unique when C is even in 2^n module arithmetic.
Therefore, it is not safe to say X = D / C

[github-actions]

Subscribe to Label Action

cc @cfallin, @fitzgen

Details

This issue or pull request has been labeled: "cranelift", "isle"

Thus the following users have been cc'd because of the following labels:

• cfallin: isle
• fitzgen: isle

To subscribe or unsubscribe from this label, edit the .github/subscribe-to-label.json configuration file.

Learn more.

[bongjunj]

Could you add "and y and z are constant" to the description here? Otherwise this reads as a fairly odd optimization that is replacing a multiply with a divide, which would ordinarily reduce performance.

Also: why is it necessary that y is odd? Is that because we need it to be mutually prime with the ring's modulus (2^n) so the product doesn't collapse to zero?

To clarify, this is the counterexample obtained by Crocus, when y is relaxed to be any bitvector.
Here, y is even.

Verification failed for <unnamed rule>, width 8
(simplify (ne [cty|8] (imul [ty|32] [x|#x80000002] (iconst_u [ty|32] [y|#x0000000000448102])) (iconst_u [ty|32] [z|#x0000000000890204])))
(if-let ((0) (u64_rem [z|#x0000000000890204] [y|#x0000000000448102]))((true) (u64_ne [y|#x0000000000448102] (0))))=>
(ne [cty|8] [x|#x80000002] (iconst [ty|32] (imm64 (u64_div [z|#x0000000000890204] [y|#x0000000000448102]))))

Furthermore, there is a similar optimization in LLVM, and the optimization requires y to be odd as well.

When y is odd:

define i1 @src(i32 %x) {
#0:
  %mul = mul i32 %x, 7
  %eq = icmp eq i32 %mul, 42
  ret i1 %eq
}
=>
define i1 @src(i32 %x) nofree willreturn memory(none) {
#0:
  %eq = icmp eq i32 %x, 6
  ret i1 %eq
}
Transformation seems to be correct!

When y is even:

----------------------------------------
define i1 @src(i32 %x) {
#0:
  %mul = mul i32 %x, 6
  %eq = icmp eq i32 %mul, 42
  ret i1 %eq
}
=>
define i1 @tgt(i32 %x) {
#0:
  %eq = icmp eq i32 %x, 7
  ret i1 %eq
}
Transformation doesn't verify!

ERROR: Value mismatch

NOTE: The counterexample is unique.

Example:
i32 %x = #x80000007 (2147483655, -2147483641)

Source:
i32 %mul = #x0000002a (42)
i1 %eq = #x1 (1)

Target:
i1 %eq = #x0 (0)
Source value: #x1 (1)
Target value: #x0 (0)

This shows that the optimization violates the semantic equivalence (or refinement) when y is even.

Reference implementation in LLVM: https://github.com/llvm/llvm-project/blob/a257a063c6fdcbc1db897d360c3791d8c4f4e48d/llvm/lib/Transforms/InstCombine/InstCombineCompares.cpp#L2209-L2230

[cfallin]

Yep, that makes sense -- just wanted to get it written down why. Thanks! Happy to merge once the merge conflicts are resolved.