Upstream simplifier rule verification tool - #9334
Open
abadams wants to merge 6 commits into
Open
Conversation
A port of apps/super_simplify from the super_simplify_v3 branch, where it had been left to bit-rot since 2021. filter_rewrite_rules takes a file of proposed simplifier rules in Simplify_*.cpp syntax and checks each one with z3 for correctness, against a reduction order for termination, and against the other rules for subsumption. super_simplify searches for the smallest expression equivalent to a given one by CEGIS. Dropped synthesize_predicate.cpp and the tools that depended on it. Both of its entry points were only reachable from disabled branches, and it was built on internal Simplify APIs that would have forced the app to build against src/ rather than an installed Halide. The predicate synthesis that filter_rewrite_rules actually uses is implemented inline and is unaffected. Also fixed, in the course of getting it running again: - z3 no longer tags models with "model", so every counterexample came back empty. - fold() in a rule aborted the SMT conversion. - Rules z3 disproved were still emitted as good rules. - bvumod is not an SMT-LIB operator, so unsigned mod produced invalid SMT2. - Integer division and modulo are Euclidean at every width in Halide, but the narrow-integer encoding used raw bvsmod and a floor-division bvsdiv, and handled neither division by zero. Verified against div_imp/mod_imp on all 65536 int8 operand pairs. - An unmodelled intrinsic in one rule aborted the whole run. - The parser had no unary minus, and could not reparse a Select as boolean. The parser's precedence ladder is now a precedence-climbing loop over a table of operators, which drops the pushback stack it used to thread between levels. Verified by reparsing every rule in src/Simplify_*.cpp and diffing: the only change is that && and || are left-associative, as in C++. Tested by ctest under the label simplifier_rule_verifier, and by make test. Both skip when z3 isn't installed, so the macOS CI job that builds apps now installs it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
A remainder always lies in [0, |c1|), so for c2 outside that range the left hand side is false while the right hand side need not be. The rule relied on the bounds analysis in Simplify_EQ having already folded such comparisons away, which it does, so this changes no behaviour. It makes the rule stand on its own rather than on the order of the passes around it. Found by apps/simplifier_rule_verifier, which checks rules in isolation. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
All but one predate the port. The search for a free wildcard name, used when demoting a constant wildcard that appears in neither a fold nor a predicate, tested against a copy of the rule taken before any substitution. Every constant wildcard therefore picked the same name and they collapsed into one variable, so the rule written out was not the rule that had been checked. Given rewrite(select(u, x + c0, x + c1), x + select(u, c0, c1)) it emitted select(x, y + z, z + y) -> select(x, y, y) + z, which is false. Parsing a bit-vector out of a z3 model shifted by up to 64 to find the sign bit, which is undefined and in practice took the sign-extend branch every time, so any counterexample mentioning a variable of 32 bits or wider was reported wrong. It also built every binding as an Int(32) regardless of the variable's real type. Both now come from the types the query was built with, which also lets z3's names for let-bound subexpressions be filtered by lookup rather than by guessing that anything starting with 't' is one. Variables of type Int(64) were declared as bit-vectors while their operators were emitted as unbounded-Int ones, so z3 rejected the query and the rule was silently classed unverifiable. likely and likely_if_innermost were not understood by the SMT conversion, so rules mentioning them were emitted without ever being checked. They only carry a branch hint, so the conversion now sees through them, as it does for fold. The parser was also turning likely_if_innermost into likely, quietly changing such rules on round-trip. all_possible_exprs_that_compute_associative_op_helper was missing the bail-out that its sibling has, so a long enough chain of terms would shift past the width of an int and exhaust memory well before that. consume() read a byte before checking it was in bounds. The binding map threaded through predicate synthesis was left over from the dropped synthesize_predicate, and was shadowed by the inner declarations that replaced it, so the code substituting it back into the rule did nothing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The Linux buildbots already build and test every app, so the rule verifier gets its coverage there. Installing z3 on the macOS runner only added load to a machine that's already oversubscribed, for a second set of the same results. Without z3 the tests aren't registered at all, so the macOS apps build is unaffected. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
satisfy() has to see through likely and likely_if_innermost, since they don't change the value and z3 has no notion of them. IROperator.h already has a helper for exactly that, so use it on the whole expression instead of special-casing the two intrinsics in the SMT conversion's Call visitor. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The original app used the ThreadPool in src/, which isn't part of the public API, so the port replaced it with a small index-based work queue. There's an equivalent in tools/halide_thread_pool.h with the same async() interface, which apps can reach through Halide::Tools, so use that instead. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
alexreinking
approved these changes
Aug 13, 2026
Member
Author
|
TODO: Check this doesn't take too long in CI |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #9334 +/- ##
==========================================
- Coverage 70.02% 69.97% -0.06%
==========================================
Files 258 258
Lines 78214 78240 +26
Branches 19038 19047 +9
==========================================
- Hits 54773 54748 -25
- Misses 17786 17809 +23
- Partials 5655 5683 +28 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
Member
Looks fine to me: |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
We formally verify our simplifier rules, but the tool for doing this was stashed in an old out-of-date branch around 5 years old. I had claude bring it up to date and recheck all the rules. This PR puts it in main as an app and tests it in CI. The existing rules all verified except for one that was only correct due to some surrounding context. It's better if the rules are correct without needing context, so I had it add a term to the predicate.
Lots of code, but almost all of it is confined to an app.