[Transform][Arith] ConstrSet::Populate ordering is load-bearing in two incompatible directions (eager Analyzer::Bind snapshots)

Summary

ConstrSet::Populate (in src/transform/common/constr_visitor.h) replays a lexically-collected list of binds and predicates into a fresh arith::Analyzer. The replay order turns out to be load-bearing in two incompatible directions:

• Program order (current upstream behavior, rationale documented since #2805) is required so that a bind evaluated under a preceding predicate captures the tightened bound.
• Binds-first (what our downstream Ascend fork carries) is required so that a predicate held in a bound boolean var can be expanded back into the condition it represents, even after Merge / RenameFrom scrambled the definition order.

Both orderings are workarounds for the same root cause: arith::Analyzer::Bind eagerly snapshots the value's integer bounds at bind time and never re-evaluates them. We would like to converge on one shared implementation instead of carrying a downstream divergence, and we have empirical data plus three candidate fixes below. We are happy to send a PR once a direction is agreed on.

Background

ConstrVisitor (introduced in #1622, used by ThreadSync since #1631, extended with snapshot mode in #3174) collects two kinds of entries while walking the IR:

• binds — v = expr (flat Bind) or v ∈ range (thread_extent), and
• predicates — branch conditions, asserts, assumes.

ConstrSet::Populate replays them into an analyzer so passes can ask CanProve questions (cross-thread race checks, and in our fork, sync-flag allocation).

The two analyzer entry points have opposite information-flow requirements:

• Analyzer::Bind(v, expr) eagerly evaluates and caches the value's bounds at bind time (vendored TVM, src/arith/analyzer.cc):

  cpp复制

  void Analyzer::Bind(const Var& var, const PrimExpr& expr, bool allow_override) {
    ...
    this->const_int_bound.Update(var, this->const_int_bound(new_expr), allow_override);
    this->modular_set.Update(var, this->modular_set(new_expr), allow_override);
    ...
  }

  So a bind wants every predicate that constrains its value to be entered before it.

• EnterConstraint(pred) digests the predicate at entry. If pred is a bound boolean var (cond where cond = (i < n) is a bind), the analyzer can only digest it after simplification expands it — which requires the bind to be installed before the predicate.

No single static order satisfies both once the sequence is scrambled.

The two orderings and where each one is needed

Program order (upstream, since #2805)

if (tx < 64) {     // predicate P: tx < 64
  v = tx;          // bind B: v = tx
}

Collected order [P, B]. Program-order replay enters tx < 64 first, so Bind(v, tx) snapshots v ∈ [0, 63]. Binds-first replay snapshots v with only the thread-extent bound (e.g. [0, 255]) and the cached bound never tightens afterwards. This is exactly the comment in the current code:

Keep program order: Analyzer::Bind evaluates the bounds and modular set of the value at bind time, so entering the binds first would widen them -- a v = tx inside if tx < 64 would lose its upper bound.

Binds-first (our downstream fork)

Our control-flow normalization (while-loop modeling for the Ascend backend) names branch conditions:

cond = (i < n)     // bind B
if (cond) { ... }  // predicate P

In straight-line collection B precedes P and program order works fine too. The problem appears when constraint sets are merged: our auto-schedule flag allocation merges per-task ConstrSets (Merge appends the other set's entries), so a predicate cond originating from set A can end up before the bind cond = (i < n) originating from set B. Program-order replay then enters an opaque boolean the analyzer cannot use; the guard fact is effectively lost, guard disjointness becomes unprovable, and flag-slot reuse is rejected. Nine of our downstream tests fail with program order and pass with binds-first.

Note this also requires simplifying the predicate at entry (EnterConstraint(analyzer.Simplify(c.value), ...) in Constr::Populate) so the bound boolean actually expands — a second small delta we carry.

Empirical evidence

• We ran the entire upstream testing/python/transform suite under both orderings (including the thread-sync tests added by #2805) on our runners: the results are identical per test. As far as current upstream tests are concerned, the two orderings are indistinguishable — presumably because CanProve queries on the v = tx pattern can still succeed through the rewrite path (v → tx substitution plus the scoped constraint) even when the cached const_int_bound is wide.
• Our downstream suite strictly requires binds-first (9 failures otherwise, all in sync-flag allocation on merged constraint sets).

So today the divergence costs upstream nothing observable, but we would much rather delete it than depend on that remaining true.

A minimal illustration of the root cause

arith::Analyzer a;
a.Bind(tx, Range(0, 256));                 // tx ∈ [0,255]
a.Bind(v, tx);                             // eager snapshot: v ∈ [0,255]
{
  With<arith::ConstraintContext> ctx(&a, tx < 64);
  a.const_int_bound(tx);                   // [0,63]  — evaluated on demand, fresh
  a.const_int_bound(v);                    // [0,255] — bind-time snapshot, stale
}

v ≡ tx yet their bounds disagree under the same constraint stack. Every ordering debate in Populate is downstream of this premature evaluation.

Candidate fixes, ranked by invasiveness

1. Dependency-aware ordering in Merge (preferred, least invasive). Keep program order within each source set, and topologically hoist a bind before any predicate that references its var when concatenating sets. Binds cannot form cycles in SSA form, so the order always exists. Straight-line behavior (the #2805 guarantee) is untouched; only scrambled merged sequences are repaired. We can send a PR for this, together with the Simplify-at-entry change and regression tests for the merged-set case.
2. Two-phase Populate (binds first, then predicates). Simplest; it is what we run today, and per the evidence above it does not change any current upstream test outcome. Downside: it silently gives up the bind-time tightening guarantee that #2805 documented, and that guarantee may be protecting untested cases.
3. Lazy / re-evaluable Bind in arith::Analyzer (root fix, heaviest). Store the definition rather than the bound snapshot, and evaluate bounds on demand under the constraint stack active at query time (memoized per constraint epoch). This dissolves the ordering question entirely, but it touches a hot path (const_int_bound inside Simplify) in vendored TVM and has a large blast radius; we mention it for completeness rather than as a near-term proposal.

What we would like from this issue

• Confirm whether the #2805 program-order guarantee protects any scenario beyond the documented v = tx example (we could not find a discriminating test).
• Pick a direction between (1) and (2). We will follow up with a PR including the merged-set regression tests either way.