wasmtime / PR #11994 [Cranelift] `(x * y) (==/!=) z --> x... · git-wasmtime

Stream: git-wasmtime

Topic: wasmtime / PR #11994 [Cranelift] `(x * y) (==/!=) z --> x...

Wasmtime GitHub notifications bot (Nov 07 2025 at 01:33):

bongjunj opened PR #11994 from bongjunj:mul_ne_eqv_ne_div to bytecodealliance:main:

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

Wasmtime GitHub notifications bot (Nov 07 2025 at 01:33):

bongjunj requested wasmtime-compiler-reviewers for a review on PR #11994.

Wasmtime GitHub notifications bot (Nov 07 2025 at 01:33):

bongjunj requested cfallin for a review on PR #11994.

Wasmtime GitHub notifications bot (Nov 07 2025 at 01:50):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Nov 07 2025 at 01:50):

cfallin created PR review comment:

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?

Wasmtime GitHub notifications bot (Nov 07 2025 at 02:04):

bongjunj updated PR #11994.

Wasmtime GitHub notifications bot (Nov 07 2025 at 02:05):

bongjunj submitted PR review.

Wasmtime GitHub notifications bot (Nov 07 2025 at 02:05):

bongjunj created PR review comment:

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.

Wasmtime GitHub notifications bot (Nov 07 2025 at 02:05):

bongjunj edited PR review comment.

Wasmtime GitHub notifications bot (Nov 07 2025 at 03:52):

github-actions[bot] commented on PR #11994:

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 <code>.github/subscribe-to-label.json</code> configuration file.

Learn more.
</details>

Wasmtime GitHub notifications bot (Nov 07 2025 at 08:32):

bongjunj commented on PR #11994:

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

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.

Wasmtime GitHub notifications bot (Nov 07 2025 at 08:34):

bongjunj edited a comment on PR #11994:

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

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

Wasmtime GitHub notifications bot (Nov 07 2025 at 08:34):

bongjunj edited a comment on PR #11994:

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

Wasmtime GitHub notifications bot (Nov 07 2025 at 17:44):

cfallin submitted PR review:

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

Wasmtime GitHub notifications bot (Nov 08 2025 at 01:53):

bongjunj updated PR #11994.

Wasmtime GitHub notifications bot (Nov 08 2025 at 01:55):

bongjunj updated PR #11994.

Wasmtime GitHub notifications bot (Nov 08 2025 at 01:58):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Nov 08 2025 at 01:58):

cfallin created PR review comment:

One more request, sorry -- could you add the commutative versions (const * x) for both rules as well?

Wasmtime GitHub notifications bot (Nov 08 2025 at 04:36):

bongjunj updated PR #11994.

Wasmtime GitHub notifications bot (Nov 08 2025 at 04:37):

bongjunj updated PR #11994.

Wasmtime GitHub notifications bot (Nov 08 2025 at 04:38):

bongjunj submitted PR review.

Wasmtime GitHub notifications bot (Nov 08 2025 at 04:38):

bongjunj created PR review comment:

Thanks!

Wasmtime GitHub notifications bot (Nov 08 2025 at 04:58):

bongjunj updated PR #11994.

Wasmtime GitHub notifications bot (Nov 08 2025 at 06:56):

cfallin merged PR #11994.

Last updated: Dec 06 2025 at 06:05 UTC