Add change_type() directive with reduction-aware overflow checks - #9257
Add change_type() directive with reduction-aware overflow checks#9257alexreinking wants to merge 11 commits into
Conversation
75752de to
6f0a76e
Compare
Codecov Report❌ Patch coverage is Additional details and impacted files@@ Coverage Diff @@
## main #9257 +/- ##
==========================================
- Coverage 70.02% 69.90% -0.12%
==========================================
Files 258 259 +1
Lines 77953 78426 +473
Branches 18979 19132 +153
==========================================
+ Hits 54585 54825 +240
- Misses 17753 17824 +71
- Partials 5615 5777 +162 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
f352290 to
0fdc17c
Compare
53d147e to
085bf96
Compare
085bf96 to
9458298
Compare
5376049 to
daf9049
Compare
| // guaranteed not to overflow. Safety is monotonic in the term count, so use | ||
| // ConstantInterval's overflow-aware arithmetic in a binary search rather than | ||
| // duplicating its endpoint math here. | ||
| int64_t maximum_safe_term_count(const ConstantInterval &accumulator, |
There was a problem hiding this comment.
Is this just (limit.min - accumulator.max) / step.max ?
There was a problem hiding this comment.
Not quite — accumulator, step, and limit are all general intervals here, not single points, and step's sign isn't fixed (a difference reduction negates the term, and even a single call's term range can straddle zero). That means the binding constraint can be the upper limit, the lower limit, or both, and a single division can't combine both endpoints' worst cases safely — it also breaks if step's interval contains zero. Rather than hand-deriving and separately overflow-hardening the endpoint math for every sign/zero combination, the binary search just reuses ConstantInterval's already-audited overflow-safe +/*, so limit.contains(accumulator + step * ConstantInterval(0, n)) is trivially correct for any sign combination. Added a comment (now on maximum_safe_term_count) explaining this.
There was a problem hiding this comment.
^ Quoting Claude here and elsewhere.
There was a problem hiding this comment.
Maybe ((limit - accumulator)/step).min then?
daf9049 to
4e4989d
Compare
4e4989d to
4237483
Compare
4237483 to
db7edbe
Compare
db7edbe to
fc7e2ad
Compare
fc7e2ad to
36cf0e2
Compare
36cf0e2 to
fb4dce3
Compare
64e0afe to
4f708ad
Compare
Add Func::change_type(Type, unsafe), which changes the type at which a Func computes and stores its values. It works eagerly at schedule time by splitting the Func in two: a returned intermediate that copies the Func's definitions but accumulates at the new type (inserting casts, preferring integer forms like widening_mul over float round-trips), and the original Func, rewritten in place into an inline wrapper that casts the intermediate's result back to the original type so every existing consumer is unaffected. Safety is validated with the bounds machinery: for an integer target, change_type() bounds the accumulator by combining the per-term value range (constant_integer_bounds augmented by FuncValueBounds) with the reduction extent. Statically-safe cases pass silently; a case provable only under a runtime precondition (symbolic RDom extent) records that condition, which a new lowering pass (add_type_change_checks, modeled on add_split_factor_checks) injects into the pipeline's assertion block and no_asserts strips. Otherwise change_type() errors unless unsafe=true. Supporting changes: Function::clear_definition() to redefine a Func in place as the wrapper; FuncSchedule carries the injected type_change_checks; get_associative_identity() for retyped reduction identities; StrictifyFloat treats int<->float casts as strict so change_type() won't strip a user's strict_cast. Adds as_binary_operands()/make_binary_op() and select_binary_operand() as reusable binary-operator helpers, placed early in Func.cpp (alongside project_rdom()) so hoist_invariants() can reuse all three without redefining them. Adds a Python binding.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
change_type_prove_safe() was only invoked for integer targets, so retyping a reduction to a float type got no safety check at all. Run it for float targets too, bounding the accumulation against the largest integer the target can represent exactly (e.g. 2048 for float16) rather than its full dynamic range. Also fixes bounds_of() to recover the exact integer value of a leaf that retype_leaf() constant-folded directly into a float literal (e.g. a seed of 0), which it previously treated as unbounded. Adds test coverage for float targets, and for sum-then-clamp, sum-scan, and histogram reductions confirming the existing extent-based bound is conservative for those shapes too.
…_integer_bounds Replace the eager cache_call_bounds() prewarming pass with an optional FuncValueBounds parameter on constant_integer_bounds() and lossless_cast(), consulted lazily when either function hits a Call::Halide node. Also add a codegen test verifying that a change_type() retype from float to Int(32) reaches CodeGen_ARM's dot-product instruction selection. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
4f708ad to
4c3a4e6
Compare
| } | ||
|
|
||
| ConstantInterval covering_constant_interval(const Interval &in) { | ||
| ConstantInterval ci = ConstantInterval::everything(); |
There was a problem hiding this comment.
Suggest taking constant_integer_bounds of in.min and in.max and constructing the constant interval that goes from the min of the min to the max of the max
| // the float round-trip is dead weight. This also exposes an integer form | ||
| // (e.g. cast<f32>(widening_mul(a, b)) -> widening_mul(a, b)) that | ||
| // lossless_cast() can retype without a detour through float, which f32 | ||
| // can't always undo. A strict_cast is a Call, not a Cast, and is left alone. |
There was a problem hiding this comment.
Please mention in the comment something about lossless_cast uses Type::can_represent to decide if it can strip an outer cast, which is strict math, not fast-math semantics. Otherwise this would be covered by the case below.
|
|
||
| // Retype a whole definition value to type `t`, retargeting a direct | ||
| // self-reference from `fname` to `dst` and retyping the other operand as the | ||
| // increment. The direct-call restriction keeps the recurrence visible to the |
There was a problem hiding this comment.
Please clarify that the direct-call restriction means that we're only matching the form f(...) = f(..) OP (something not referencing f) or its commutative flip. Not cases where there are calls to f anywhere other than one side of the top level.
| // self-reference from `fname` to `dst` and retyping the other operand as the | ||
| // increment. The direct-call restriction keeps the recurrence visible to the | ||
| // overflow proof. | ||
| Expr retype_value(const Expr &e, const string &fname, const Function &dst, Type t, |
There was a problem hiding this comment.
I think the recursion is making this needlessly complex, because it has to be depth 1 anyway. Could just extract the self-reference, unpack it as a call, then call retype_leaf on the other child.
Adds a new
.change_type()directive to Halide that takes a typeSand replaces a funcFof typeTwith:Where
e' : Sis a type-adjusted version ofe : Tsuch thate = cast(T, e').We use
FuncValueBoundsandlossless_castto ensure that the replaced type will not perturb values in the pipeline. The directive is aware of reductions and will add runtime asserts to ensure that accumulations are not too long if the extent cannot be proven sufficiently short.When constructing
e',change_typemight adjust the form to use widening intrinsics. For instance, the result of changing the type off32(i8a) * f32(i8b)to Int32 would becast<int32>(widening_mul(i8a, i8b)), which is bitwise exact.A prototype of this was written over several sessions involving several LLMs. I probably wrote as much prompt as code was produced, and I feel that the ultimate implementation is more mine than any LLM's. The tests were written by machine outright, however.
Breaking changes
None: this is a new directive.
Checklist
Stack created with GitHub Stacks CLI • Give Feedback 💬