fix[next]: symbolic domain union for empty domains#2673
Draft
tehrengruber wants to merge 1 commit into
Draft
Conversation
tehrengruber
marked this pull request as draft
June 23, 2026 18:28
tehrengruber
changed the title
tehrengruber
force-pushed
the
fix_concat_where
branch
from
June 29, 2026 12:06
01e7cb8 to
3630fbc
Compare
tehrengruber
changed the base branch from
main
to
fix_concat_where_static_domains
June 29, 2026 12:07
Re-applies the symbolic-domain handling (guarded let-bindings in domain reductions, gtfn/roundtrip InfinityLiteral lowering) on top of the static-domains base. The domain union/intersection tests in test_domain_utils are unified into a single 'static_domains' parametrization: the symbolic result is evaluated by binding its bounds to concrete values via a 'let', inlining and constant folding, so it collapses to the same concrete domain as the static case.
tehrengruber
force-pushed
the
fix_concat_where_static_domains
branch
from
July 1, 2026 09:01
cc072a8 to
2a19d8a
Compare
tehrengruber
force-pushed
the
fix_concat_where
branch
from
July 1, 2026 09:02
3630fbc to
ee96be7
Compare
tehrengruber
added a commit
that referenced
this pull request
Jul 2, 2026
Domain inference computes the union of two domains as the per-dimension convex hull: ``` union(A, B) = [ min(A.start, B.start), max(A.stop, B.stop) [ ``` This is wrong when the inputs are empty (`start >= stop`). The union of two empty domains should stay empty, but `min`/`max` produces a non-empty range: - `A = [10, 10[` (empty) - `B = [11, 11[` (empty) ``` union(A, B) = [ min(10, 11), max(10, 11) [ = [10, 11[ ``` so two empty domains wrongly union to the non-empty `[10, 11[`. This shows up in practice with `concat_where`: a branch that is never selected produces an empty domain, and previously the empty range leaked into the `min`/`max` and over-approximated the inferred domain (#2205). **Fix** An empty domain is the identity element of union, so empty ranges are dropped before folding rather than fed into `min`/`max` (`_reduce_ranges` in `domain_utils.py`). The union of only empty domains then correctly stays empty. **Scope** This PR only handles static domains — concrete integer bounds, where emptiness is decidable. The symbolic case (runtime-sized bounds like `[0, n[`, where emptiness can't be decided at compile time and empty ranges must instead be guarded with conditional expressions) is considerably more involved and is left to a follow-up. A prototype implementation can be found in #2673.
tehrengruber
added a commit
that referenced
this pull request
Jul 14, 2026
## Problem `_reduce_ranges` in `domain_utils.py` is shared by `domain_union` and `domain_intersection`: ```python _range_union = functools.partial(_reduce_ranges, start_reduce_op=im.minimum, stop_reduce_op=im.maximum) _range_intersection = functools.partial(_reduce_ranges, start_reduce_op=im.maximum, stop_reduce_op=im.minimum) ``` #2677 taught it to drop statically empty ranges before folding. That is correct for the **union**, where an empty range is the identity element, but wrong for the **intersection**, where an empty range is the *absorbing* element. Dropping the empty range from an intersection returns the remaining range instead of staying empty: ``` [1, 1[ & [0, 10[ -> [0, 10[ # should be empty [1, 1[ & [0, inf[ -> [0, inf[ # should be empty ``` The second form is reached in practice: `promote_domain` fills non-condition dimensions with `[-inf, inf[`, and `_infer_concat_where` intersects that with the target domain. If the target range is statically empty, the half-infinite range survives verbatim and an `InfinityLiteral` leaks into the inferred domain. ## Symptoms Both show up in ICON4Py with `concat_where` over a statically-known-empty vertical range (a Rayleigh damping layer of zero thickness, where the layer bound is bound as a compile-time static arg): - **gtfn** — the leaked `InfinityLiteral` reaches `itir_to_gtfn_ir._make_domain`: ``` TypeError: 'BinaryExpr.lhs' must be <class '...gtfn_ir_common.Expr'> (got 'InfinityLiteral.POSITIVE' which is a <class '...iterator.ir.InfinityLiteral'>). ``` - **dace** — `gtir_to_sdfg_concat_where` calls `domain_intersection(source_domain, output_domain)` directly at lowering time, with finite bounds. No infinity, no crash: a scalar `concat_where` branch whose range is empty (`[1, 1[`) is widened to the full output domain (`[1, 10[`), so the constant branch is broadcast over the whole domain and silently overwrites the real values. The dace case is a silent wrong-results bug, so it is worth backporting alongside the crash. ## Fix Split the two operations. The union keeps dropping empty ranges; the intersection returns the empty range directly. Emptiness remains decidable only for static ranges — non-static ranges may not be empty, as before. Also restores the constant folding that #2677 skipped in the single-surviving-range case. ## Testing - Two regression tests in `test_domain_utils.py` covering the finite and the half-infinite case. Both fail on `main`. - `tests/next_tests/unit_tests/` A/B'd with and without the change: no new failures. - Verified against ICON4Py (C2SM/icon4py#1350): the gtfn `TypeError` and the dace `diff_multfac_n2w` mismatch both disappear, and the previously-failing GAUSS3D driver integration test passes. Follow-up on #2677, related to #2205. The symbolic (non-static) case is still left to #2673. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Hannes Vogt <claude@mail.havogt.de> Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com> Co-authored-by: Till Ehrengruber <till.ehrengruber@cscs.ch>
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
1 participant
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.
Superseeds #2670
I didn't read the tests yet.