Skip to content

Fix NonNegativeResultAnalysis square rule to compare Values not defining ops#2649

Open
kimjune01 wants to merge 1 commit into
EnzymeAD:mainfrom
kimjune01:fix/nonneg-square-value-identity-2648
Open

Fix NonNegativeResultAnalysis square rule to compare Values not defining ops#2649
kimjune01 wants to merge 1 commit into
EnzymeAD:mainfrom
kimjune01:fix/nonneg-square-value-identity-2648

Conversation

@kimjune01

Copy link
Copy Markdown
Contributor

Fixes #2648.

NonNegativeResultAnalysis's "(mul a a) is always non-negative" rule compared the operands' defining ops rather than the operands themselves:

auto lhsOp = mulOp.getLhs().getDefiningOp();
auto rhsOp = mulOp.getRhs().getDefiningOp();
if (lhsOp == rhsOp) return State::GUARANTEED;

Two distinct block arguments both have a nullptr defining op, so null == null wrongly proved mul(%arg0, %arg1) non-negative -- even though the product is negative whenever the args have opposite signs. Any consumer of guaranteedNonNegativeResult could then mis-fire (e.g. AbsPositiveSimplify dropping an abs that is actually load-bearing).

The fix compares the operand Values directly, which is what "same value squared" actually means:

if (mulOp.getLhs() == mulOp.getRhs()) return State::GUARANTEED;

This is strictly stricter -- it only removes unsound proofs, never adds new ones. The existing mul(%arg0, %arg0) cases in abspositive.mlir (test3/4/7) still fold, since %arg0 == %arg0.

Added test9 in abspositive.mlir: abs(mul(%arg0, %arg1)) of two distinct block args must keep its abs (fails on the pre-fix analysis, passes after).

Found while implementing the non-negativity gate in #2576.

…ing ops

The (mul a a) non-negativity rule compared the operands' defining ops. Two
distinct block arguments both have a null defining op, so null == null wrongly
proved mul(%arg0, %arg1) non-negative even when the product can be negative.
Compare the operand Values directly instead, and add a regression test.

Fixes EnzymeAD#2648
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

NonNegativeResultAnalysis wrongly proves mul(x, y) non-negative

2 participants