Per-SDFG symbol registry with explicit facts

dace/autodiff/data_forwarding/store.py

@@ -540,11 +540,10 @@ def _get_assign_tasklet(
                 memlet_access_iterators.append(str(element[0]))
             else:
                 # This is a range tuple we need to add an iterator for
-                # Create a random new free symbol
-                free_symbol = forward_state.sdfg.find_new_symbol("si")
-
-                # Add the new symbol here so that find_new_symbol doesn't return it again
-                forward_state.sdfg.add_symbol(free_symbol, dtypes.int64)
+                # A map parameter that neither the SDFG nor an earlier dimension uses
+                free_symbol, index = "si", 0
+                while free_symbol in param_dict or forward_state.sdfg.is_name_used(free_symbol):
+                    free_symbol, index = f"si_{index}", index + 1
                 memlet_access_iterators.append(free_symbol)
                 param_dict.update({free_symbol: element})
 

dace/autodiff/utils.py

@@ -98,12 +98,10 @@ def connector_symbol(name: str, dtype: dtypes.typeclass | None = None) -> symbol
 
     Always a ``symbolic.symbol``, never a bare ``sympy.Symbol``: the two compare unequal while
     still substituting for one another, which is what makes ``diff()`` return a silent zero.
-    ``integer=None`` where the dtype is unknown, so that ``symbol``'s int32 default does not
-    assert an integer assumption the declaration never made.
     """
     if isinstance(dtype, dtypes.typeclass):
         return symbolic.symbol(name, dtype)
-    return symbolic.symbol(name, integer=None)
+    return symbolic.symbol(name)
 
 
 def backward_symbol_mapping(nested_sdfg: SDFG, parent_state: SDFGState) -> dict[str, symbolic.symbol]:
@@ -460,9 +458,8 @@ def code_to_exprs(
                 raise AutoDiffException(f"Expected connector '{conn}' to be in indexed objects map for pointer type")
             indexed_objects_code += f"    {conn} = sp.IndexedBase('{conn}')\n"
             for idx in indexed_objects_map[conn]:
-                idx_sym = connector_symbol(idx, symbols.get(idx) or tasklet.in_connectors.get(idx))
-                # An Idx label must be integral, so a non-integer declaration cannot supply one.
-                symbol_table[idx] = sp.Idx(idx_sym if idx_sym.is_integer else symbolic.symbol(idx))
+                # An index of an SDFG symbol keeps its entry; sympy indexes an IndexedBase by any expression
+                symbol_table.setdefault(idx, connector_symbol(idx))
                 indexed_objects_code += f"    {idx} = {SYMBOL_TABLE_GLOBAL}['{idx}']\n"
 
     code_fn = """

dace/codegen/compiled_sdfg.py

@@ -245,6 +245,15 @@ def __init__(self, sdfg, lib: ReloadableDLL, argnames: list[str] | None = None):
         # Present exactly when a GPU target emitted its init/exit pair, which is a sharper test than
         # the ``has_gpu_code`` heuristic below.
         self._gpu_last_error = self.get_exported_function("__dace_gpu_last_error", restype=ctypes.c_int)
+        # Avoid import loop
+        from dace.sdfg.symbol_repo import program_assumptions
+
+        # The orders proofs took from symbol scales, checked against the symbol values of every call
+        self._assumptions = program_assumptions(sdfg)
+        self._check_assumptions = (
+            lib.get_symbol(f"__dace_check_assumptions_{sdfg.name}", restype=ctypes.c_int) if self._assumptions else None
+        )
+        self._initarg_names: tuple[str, ...] = ()
 
         # Cache SDFG return values
         self._return_syms: dict[str, Any] = None
@@ -608,6 +617,10 @@ def fast_call(
             # Call initializer function if necessary, then SDFG
             if self._initialized is False:
                 self._lib.load()
+            # Checked with the library loaded: a failed call unloads it
+            if self._check_assumptions is not None:
+                self._raise_on_broken_assumption(initargs)
+            if self._initialized is False:
                 self._initialize(initargs)
 
             with hooks.invoke_compiled_sdfg_call_hooks(self, callargs):
@@ -628,6 +641,22 @@ def fast_call(
             self._initialized = False
             raise
 
+    def _raise_on_broken_assumption(self, initargs: Sequence[Any]) -> None:
+        """Raises if the symbol values break an order a transformation took from the symbol scales."""
+        broken = self._check_assumptions(*initargs)
+        if broken == 0:
+            return
+        relation = self._assumptions[broken - 1]
+        values = ", ".join(
+            f"{name}={getattr(value, 'value', value)}"
+            for name, value in zip(self._initarg_names, initargs)
+            if name in symbolic.relation_names(relation)
+        )
+        raise ValueError(
+            f'"{self._sdfg.name}" was optimized assuming {relation.lhs} < {relation.rhs} (SMALL symbols are much '
+            f"smaller than the others), which does not hold for {values}"
+        )
+
     def __del__(self):
         if self._initialized is True:
             self.finalize()
@@ -722,6 +751,7 @@ def construct_arguments(self, *args: Any, **kwargs: Any) -> tuple[tuple[Any], tu
         )
         newargs = tuple(carg for carg, _aname in callparams)
         initargs = tuple(carg for carg, aname in callparams if aname in symbols)
+        self._initarg_names = tuple(aname for _carg, aname in callparams if aname in symbols)
 
         return (newargs, initargs)
 

dace/codegen/instrumentation/data/data_report.py

@@ -118,15 +118,16 @@ def __getitem__(self, item: str) -> ArrayLike | Number | list[ArrayLike] | list[
                 nparr, view = self._read_array_file(file, npdtype)
                 self.loaded_values[item, i] = nparr
                 results.append(view)
-        elif item in self.sdfg.symbols:
-            dtype: dtypes.typeclass = self.sdfg.symbols[item]
-            npdtype = dtype.as_numpy_dtype()
+        else:
+            # The dump saves the symbols each state defines, which include loop variables and map parameters
+            types = {name: dtype for state in self.sdfg.states() for name, dtype in state.defined_symbols().items()}
+            if item not in types:
+                raise KeyError(f"Item {item} not found in report")
+            npdtype = types[item].as_numpy_dtype()
             for i, file in enumerate(filenames):
                 val = self._read_symbol_file(file, npdtype)
                 self.loaded_values[item, i] = val
                 results.append(val)
-        else:
-            raise KeyError(f"Item {item} not found in report")
 
         if len(results) == 1:
             return results[0]

dace/codegen/targets/cpp.py

@@ -31,7 +31,7 @@
 from dace.sdfg import SDFG, SDFGState, is_devicelevel_gpu, nodes, propagation
 from dace.sdfg import graph as gr
 from dace.sdfg import utils as sdutil
-from dace.sdfg.state import ControlFlowRegion, StateSubgraphView
+from dace.sdfg.state import ControlFlowRegion, StateSubgraphView, SymbolResolver
 
 if TYPE_CHECKING:
     from dace.codegen.dispatcher import TargetDispatcher
@@ -424,7 +424,7 @@ def reshape_strides(subset, strides, original_strides, copy_shape):
     reduced_tile_sizes += [1] * (dims - len(reduced_tile_sizes))  # Pad the remainder with 1s to maintain dimensions.
 
     reshaped_copy = copy_shape + [ts for ts in subset.tile_sizes if ts != 1]
-    reshaped_copy[: len(copy_shape)] = [s // ts for s, ts in zip(copy_shape, reduced_tile_sizes)]
+    reshaped_copy[: len(copy_shape)] = [symbolic.int_floor(s, ts) for s, ts in zip(copy_shape, reduced_tile_sizes)]
 
     new_strides = [0] * len(reshaped_copy)
     elements_remaining = functools.reduce(sp.Mul, copy_shape, 1)
@@ -697,6 +697,8 @@ def _check_neighbor_conflicts(dfg, edge):
     Returns True if there are no conflicts, False if there may be.
     """
     outer = propagation.propagate_memlet(dfg, edge.data, edge.dst, False)
+    # The propagated subsets are outside the map
+    facts = SymbolResolver().facts_at(dfg, dfg.entry_node(edge.dst))
     siblings = dfg.in_edges(edge.dst)
     for sibling in siblings:
         if sibling is edge:
@@ -705,7 +707,7 @@ def _check_neighbor_conflicts(dfg, edge):
             continue
         # Check if there is definitely no overlap in the propagated memlet
         sibling_outer = propagation.propagate_memlet(dfg, sibling.data, edge.dst, False)
-        if subsets.intersects(outer.subset, sibling_outer.subset) == False:
+        if subsets.intersects(outer.subset, sibling_outer.subset, facts) is symbolic.Truth.FALSE:
             # In that case, continue
             continue
 
@@ -798,9 +800,10 @@ def is_write_conflicted_with_reason(dfg, edge, datanode=None, sdfg_schedule=None
         dst = sdutil.get_last_view_node(dfg, dst) or dst
 
         if dfg.in_degree(dst) > 0:
+            facts = SymbolResolver().facts_at(dfg, dst)
             for x, y in itertools.combinations(dfg.in_edges(dst), 2):
                 x, y = x.data.subset, y.data.subset
-                if subsets.intersects(x, y):
+                if subsets.intersects(x, y, facts) is symbolic.Truth.TRUE:
                     return dst
 
         # If this is a nested SDFG and the access leads outside

dace/codegen/targets/cuda.py

@@ -2796,7 +2796,7 @@ def generate_kernel_scope(
         # Generate all index arguments for kernel grid
         krange = subsets.Range(kernel_map.range[::-1])
         kdims = krange.size()
-        dsym = [symbolic.symbol("__DAPB%d" % i, nonnegative=True, integer=True) for i in range(len(krange))]
+        dsym = [symbolic.symbol("__DAPB%d" % i) for i in range(len(krange))]
         bidx = krange.coord_at(dsym)
 
         # handle dynamic map inputs
@@ -2893,7 +2893,7 @@ def generate_kernel_scope(
                 condition = ""
 
                 # Optimize conditions if they are always true
-                if i >= 3 or (dsym[i] >= minel) != True:
+                if i >= 3 or not _index_starts_at(dsym[i], minel):
                     condition += f"{v} >= {_topy(minel)}"
                 # The grid of the distributed dimension is padded to a multiple of the number of
                 # chiplets, so its trailing blocks always have to be masked out
@@ -3185,10 +3185,7 @@ def generate_devicelevel_scope(
 
                 device_map_range = subsets.Range(scope_map.range[::-1])
                 device_map_dims = device_map_range.size()
-                dsym = [
-                    symbolic.symbol("__DAPB%d" % i, nonnegative=True, integer=True)
-                    for i in range(len(device_map_range))
-                ]
+                dsym = [symbolic.symbol("__DAPB%d" % i) for i in range(len(device_map_range))]
                 bidx = device_map_range.coord_at(dsym)
 
                 # handle dynamic map inputs
@@ -3262,7 +3259,7 @@ def generate_devicelevel_scope(
                     condition = ""
 
                     # Optimize conditions if they are always true
-                    if i >= 3 or (dsym[i] >= minel) != True:
+                    if i >= 3 or not _index_starts_at(dsym[i], minel):
                         condition += f"{v} >= {_topy(minel)}"
                     if (
                         i >= 3
@@ -3315,7 +3312,7 @@ def generate_devicelevel_scope(
                 brange = subsets.Range(scope_map.range[::-1])
                 kdims = brange.size()
                 dsym = [
-                    symbolic.symbol("__DAPT%d" % i, nonnegative=True, integer=True) - off
+                    symbolic.symbol("__DAPT%d" % i) - off
                     for i, off in zip(range(len(brange)), extra_gdim_offsets[scope_map])
                 ]
                 gdims = len(self._kernel_map.params)
@@ -3352,7 +3349,7 @@ def generate_devicelevel_scope(
                     #############################################
 
                     # Block range start
-                    if i >= 3 or (dsym[i] >= minel) != True:
+                    if i >= 3 or not _index_starts_at(dsym[i], minel):
                         condition += f"{v} >= {_topy(minel)}"
 
                     # Special case: block size is exactly the range of the map (0:b)
@@ -3389,7 +3386,7 @@ def generate_devicelevel_scope(
 
             brange = subsets.Range(scope_map.range[::-1])
             kdims = brange.size()
-            dsym = [symbolic.symbol("__DAPT%d" % i, nonnegative=True, integer=True) for i in range(len(brange))]
+            dsym = [symbolic.symbol("__DAPT%d" % i) for i in range(len(brange))]
             dsym_end = [d + (bs * rng[2]) - 1 for d, bs, rng in zip(dsym, self._block_dims, brange)]
             tidx = brange.coord_at(dsym)
 
@@ -3434,7 +3431,7 @@ def generate_devicelevel_scope(
                 #############################################
 
                 # Block range start
-                if i >= 3 or (dsym[i] >= minel) != True:
+                if i >= 3 or not _index_starts_at(dsym[i], minel):
                     condition += f"{v} >= {_topy(minel)}"
 
                 # Special case: block size is exactly the range of the map (0:b)
@@ -3759,6 +3756,14 @@ def emit_interstate_variable_declaration(
 # Helper functions and classes
 
 
+def _index_starts_at(index: sympy.Expr, begin: sympy.Expr) -> bool:
+    """Whether a grid index (of ``__DAPB*`` block and ``__DAPT*`` thread index symbols, which count up from zero)
+    provably never falls below ``begin``."""
+    names = frozenset(s.name for s in index.free_symbols if s.name.startswith(("__DAPB", "__DAPT")))
+    from_zero = [symbolic.Relation(symbolic.RelationKind.LE, sympy.Integer(0), symbolic.symbol(name)) for name in names]
+    return symbolic.provably_le(begin, index, symbolic.Facts(from_zero, names))
+
+
 def _topy(arr):
     """Converts an array of symbolic variables (or one) to C++ strings."""
     if not isinstance(arr, list):

dace/codegen/targets/framecode.py

@@ -1,6 +1,5 @@
 # Copyright 2019-2026 ETH Zurich and the DaCe authors. All rights reserved.
 import collections
-import copy
 import pathlib
 import re
 from typing import Any
@@ -19,6 +18,7 @@
 from dace.sdfg import scope as sdscope
 from dace.sdfg.analysis import cfg as cfg_analysis
 from dace.sdfg.state import AbstractControlFlowRegion, ControlFlowBlock, ControlFlowRegion, LoopRegion, SymbolResolver
+from dace.sdfg.symbol_repo import assumption_check, program_assumptions
 from dace.sdfg.type_inference import infer_expr_type
 from dace.transformation.passes.analysis import StateReachability, loop_analysis
 
@@ -342,12 +342,22 @@ def generate_footer(self, sdfg: SDFG, global_stream: CodeIOStream, callsite_stre
                     sdfg,
                 )
 
+        # The orders proofs took from symbol scales; init refuses symbol values that break one
+        assumptions = program_assumptions(sdfg)
+        if assumptions:
+            readable = {name for name in self.free_symbols(sdfg) if not name.startswith("__dace")}
+            callsite_stream.write(assumption_check(sdfg.name, initparams, assumptions, readable), sdfg)
+
         callsite_stream.write(
             f"""
 DACE_EXPORTED {mangle_dace_state_struct_name(sdfg)} *__dace_init_{sdfg.name}({initparams})
 {{""",
             sdfg,
         )
+        if assumptions:
+            callsite_stream.write(
+                f"    if (__dace_check_assumptions_{sdfg.name}({initparamnames}) != 0) return nullptr;\n", sdfg
+            )
 
         # Invoke all instrumentation providers
         for instr in self._dispatcher.instrumentation.values():
@@ -598,7 +608,7 @@ def dispatch_state(state: SDFGState) -> str:
             states_generated.add(state)  # For sanity check
             return stream.getvalue()
 
-        callsite_stream.write(cflow.control_flow_region_to_code(sdfg, dispatch_state, self, sdfg.symbols), sdfg)
+        callsite_stream.write(cflow.control_flow_region_to_code(sdfg, dispatch_state, self, dict(sdfg.symbols)), sdfg)
 
         opbar.done()
 
@@ -1061,7 +1071,7 @@ def generate_code(
                 self.dispatcher.defined_vars.add(cname, disp.DefinedType.Scalar, ctype.dtype.ctype)
 
         # Allocate inter-state variables
-        global_symbols = copy.deepcopy(sdfg.symbols)
+        global_symbols = dict(sdfg.symbols)
         global_symbols.update({aname: arr.dtype for aname, arr in sdfg.arrays.items()})
         interstate_symbols = {}
         for cfr in sdfg.all_control_flow_regions():

dace/config_schema.yml

@@ -85,15 +85,6 @@ required:
                     "for" and "while" from state transitions, allowing
                     code generators to generate appropriate code.
 
-            symbolic_positive:
-                type: bool
-                default: true
-                title: Treat all symbolic expressions as positive
-                description: >
-                    Every expression in which a symbolic value appears
-                    is treated as strictly positive. This is necessary
-                    for certain Range evaluations using Subgraph Fusion.
-
             match_exception:
                 type: bool
                 default: false