Detect same-name symbols with differing SymPy assumptions - #2486
Draft
ThrudPrimrose wants to merge 11 commits into
Draft
Detect same-name symbols with differing SymPy assumptions#2486ThrudPrimrose wants to merge 11 commits into
ThrudPrimrose wants to merge 11 commits into
Conversation
SymPy folds assumptions into symbol identity, so one name spelled two ways is two distinct objects: index arithmetic does not cancel and dependence predicates silently answer wrong. Report it at validation and when a symbol is registered, behind an opt-in experimental config flag, default off.
SymPy folds assumptions into symbol identity, so one name spelled two ways is two distinct objects: index arithmetic does not cancel and dependence predicates silently answer wrong. The frontend minted loop iterators with bound-derived nonnegative/positive assumptions, and with unestablished ones passed as an explicit None, both of which differ from the plain symbol every reparse yields. Mint the canonical spelling instead; subset covering re-derives nonnegativity in subsets.nng. Validation now rejects a collision unconditionally, walking the SDFG once and deriving assumptions only for distinct objects that share a name.
SymPy folds assumptions into symbol identity, so `dace.symbol('N',
positive=True)` in an annotated shape is a different object from the bare N
that reparsing a subset or a map range yields. Both spellings then coexist and
index arithmetic over them stops cancelling, silently. tests/library/pblas
pgemm hits this through public API.
Symbols stored in an SDFG are now always bare. Assumptions move to a new
SDFG.symbol_assumptions registry, written only through
update_symbol_assumptions, which refines monotonically and rejects
contradictions; add_symbol is unchanged. assume_symbols re-mints them
transiently where a proof needs the facts.
Validation rejects a stored assumed symbol unconditionally.
The undefined sentinel is spelled "?", which validate_name rejects, so re-minting it as a bare symbol raised NameError for every descriptor with an undefined shape. It carries no assumptions and cannot be declared, so it has nothing to contribute to the registry.
A pass minting dace.symbol('Px', positive=True) into a map range left the assumed
spelling in the graph, while add_datadesc absorbs the same name off the transient it
mints beside it. The two spellings are distinct SymPy objects, so the collision check
rejected the SDFG -- samples/simple/mandelbrot.py under the transformation tester.
Normalize where a map range is stored, not per transformation: RangeProperty bares
the bounds through a new symbolic.bare_symbols. Assumptions stay reachable through
SDFG.symbol_assumptions and assume_symbols.
Range parses each bound through one seam, so that is where the always-bare
invariant sits: start, end, step, tile, Indices elements and what replace()
substitutes in. A caller minting dace.symbol('N', positive=True) into a memlet
or a map range can no longer split the name. Drops the RangeProperty guard the
deeper seam subsumes, and bare_symbols now returns its argument untouched when
it is already bare and skips numbers outright.
The Range JSON round-trip test asserted the assumption survived; a Range never
holds one now, so it asserts the bare spelling and the dtype instead.
assume_symbols re-minted a symbol per query, and dace symbols deliberately bypass sympy's cache, so the assumption closure was rebuilt every time. Mint through an lru_cache and xreplace rather than subs: the keys are the stored objects, so nothing needs matching.
A map or consume parameter is scope-local: its range is what is known about it, and nothing hoists that into SDFG.symbol_assumptions. Reusing the name of a symbol the registry holds facts about therefore makes every reapplication site assume those facts of the wrong symbol. Reusing a parameter name across disjoint scopes stays legal and silent.
Negative tests build collisions the way passes really do -- desc.shape assigned behind the coercing seam -- instead of hand-writing Range.ranges. New: a memlet subset built from an assumed symbol stores the bare one while the fact lands in the registry; assume_symbols folds Max, sqrt and inequalities exactly as the declared symbol did; parameters stay scope-local across the three scope rules.
ThrudPrimrose
added a commit
that referenced
this pull request
Aug 11, 2026
set_symbol_nonnegative_assumptions stamped nonnegative=True symbols through replace_dict. Post-#2486 every subset/map-range store bares its bounds, so the stamp survived only in descriptor shapes/strides -- exactly the two-spelling state the now-mergeable collision check rejects. Record the fact in SDFG.symbol_assumptions instead (the registry absorb_symbol_assumptions also feeds); proof sites re-apply it transiently via sdfg.assume_symbols. The registry doubles as the convergence memory _names_still_plain scanned stores for, so that walk is gone. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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.
Problem
SymPy folds assumptions into symbol identity.
symbol('i', integer=True)andsymbol('i', integer=True, nonnegative=True)are two distinct objects, even though the name denotes one value in an SDFG. This has been the root cause of many problems. This issue preventsloop2mapfrom failing, serialization having undeterministic behavior and many more...As a first step I propose follwing:
What this adds
Three functions in
dace/sdfg/validation.py:symbol_assumption_spellings(sdfg)walks array shapes/strides/offsets, map ranges, memlet subsets, loop init/update/condition and interstate edge conditions/assignments, and returns, per symbol name, every assumption set it is spelled with and where.symbol_assumption_collisions(sdfg, name=None)filters that to names with more than one spelling.check_symbol_assumption_collisions(sdfg, name=None)raisesInvalidSDFGErroron those, reporting only the assumptions the variants disagree on.Two call sites, both gated on
experimental.check_symbol_assumption_collisions, default false:validate_sdfg, whole-SDFG.SDFG.add_symbol, scoped to the name being registered and checked before the name lands insymbols.Tests
tests/sdfg/validation/symbol_assumption_collision_test.py, 6 tests: single spelling passes, two spellings are reported with both locations and only the distinguishing assumption in the message, the name filter,validatehonors the flag in both positions,add_symboltrips before registering and still accepts a clean name, and the flag defaults to off.