Skip to content

Conversation

@alexreinking
Copy link
Member

A bit of a hopeful title. Adds a fuzz test for the simplifier to check idempotency, which currently fails. This arose from trying to understand the simplifier and encountering a simplify(simplify(...)) in TrimNoOps.cpp.

@alexreinking alexreinking requested a review from abadams October 10, 2025 20:03
@alexreinking
Copy link
Member Author

alexreinking commented Oct 10, 2025

A few more failures:

    (uint32)bitwise_and(uint32(uint1(uint32(b)) && uint1(uint32(a))), uint32((uint1)0 || (uint1)1))
 -> (uint32(uint1(b) && uint1(a)) % (uint32)2)
 -> uint32(uint1(b) && uint1(a))
    ((int16x4)bitwise_or((int16x4)bitwise_not(x4((int16)-29114)), (int16x4)bitwise_not(int16x4(x4(uint1(int16(b))) && uint1x4(x2(x2(int16(a))))))) == ramp(x2((int16)23452), ramp(int16(d), int16(d), 2), 2))
 -> (ramp(x2((int16)23452), ramp(int16(d), int16(d), 2), 2) == x4((int16)-1))
 -> (ramp(x2((int16)23453), ramp(int16(d), int16(d), 2), 2) == x4((int16)0))
    (x3(x2(10)) == ramp(ramp(-59, b, 3), ramp(b, e, 3), 2))
 -> (ramp(ramp(-59, b, 3), ramp(b, e, 3), 2) == x6(10))
 -> (ramp(ramp(-69, b, 3), ramp(b, e, 3), 2) == x6(0))
    ((uint32)bitwise_or((uint32)bitwise_not(uint32(c)), (uint32)bitwise_not((uint32)2491006738 - (uint32)3727955724)) != ((uint32)2366790925*uint32(uint1(uint32(uint1(uint32(d)) && uint1(uint32((uint1)0 || (uint1)0)))) || uint1(uint32(uint1((uint32)bitwise_and((uint32)2615464650, uint32(a))) && (uint1)1)))))
 -> ((uint32)bitwise_or((uint32)bitwise_not(uint32(c)), (uint32)1236948985) != (uint32(uint1((uint32)bitwise_and((uint32)2615464650, uint32(a))))*(uint32)2366790925))
 -> (uint1)1
    (-65 == select(a != c, -21, a))
 -> (select(a == c, a, -21) == -65)
 -> ((a == c) && (a == -65))

@abadams abadams self-assigned this Oct 10, 2025
@abadams
Copy link
Member

abadams commented Oct 22, 2025

For posterity I'll write more about what this PR does in its current state. Initially we thought this was just a matter of adding calls to mutate() around certain return paths instead of just returning them as-is. But to resolve the issue I had to do a few more things.

  • give the EQ simplifier its own set of rules, instead of relying on the Sub visitor. These were formally verified in the infinite integers, except for the rules around ramp and broadcast. I derived them by going through the Sub rules and pulling out all the things that seemed useful.

  • ExprInfo needed to be accurate in the cases where we return without remutating. It has to match what the ExprInfo would be if the output Expr were remutated. So for example if an expression simplifies to a subexpression, we have to faithfully return the ExprInfo for the subexpression. If the ExprInfo is not also idempotent in this way, then the simplifier is not idempotent, because in many places constraints from the ExprInfo cause simplifications to occur.

  • Deriving bits known from bounds got simpler and tighter. If you have bounds, and the min and max share some leading bits, then all values in between those bounds have the same leading bits. This is more powerful than the logic about things being positive having leading zeros, etc. This was necessary to get tight ExprInfo through the bitwise op call nodes.

  • There was a bug in solve_for_outer/inner_interval where it forgot that bool-valued Select nodes can exist. Fixing this was necessary for this PR to generate IR that's at least as good as main on all the apps.

  • fuzz_simplify had no coverage of abs, but we have simplification rules around abs, so I added it. There are undoubtedly many more things we need to add to fuzz_simplify

@abadams abadams merged commit 602a5c0 into main Oct 22, 2025
18 of 19 checks passed
@alexreinking alexreinking deleted the simplify/idempotency branch October 22, 2025 18:13
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.

2 participants