Allow arithmetic in lifted differentiable constraints#12029
Conversation
📝 WalkthroughWalkthroughThis PR updates constraint unification so selected integer and declared-subtype witness comparisons no longer fail the matching path. It also adds an autodiff compute test covering generic wrappers with arithmetic-dependent shape constraints. ChangesConstraint unification behavior change
Autodiff generic-container arithmetic constraint test
Suggested reviewers: 🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 1
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: 10245ead-75df-4da4-89e1-dca7a44628b4
📒 Files selected for processing (2)
source/slang/slang-check-constraint.cpptests/autodiff/generic-container-arithmetic-constraint.slang
| //TEST(compute):COMPARE_COMPUTE_EX(filecheck-buffer=CHECK):-slang -compute -shaderobj -output-using-type | ||
| //TEST(compute, vulkan):COMPARE_COMPUTE_EX(filecheck-buffer=CHECK):-vk -compute -shaderobj -output-using-type | ||
| //TEST(compute):COMPARE_COMPUTE_EX(filecheck-buffer=CHECK):-cuda -compute -shaderobj -output-using-type |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick win
🧩 Analysis chain
🌐 Web query:
Does Slang autodiff bwd_diff work on the CPU (llvm) and interpreter compute targets?
💡 Result:
Yes, Slang's bwd_diff (backward-mode automatic differentiation) is supported on the CPU compute target [1][2]. Slang's automatic differentiation system is designed to be largely target-independent [1]. Development and regression testing for autodiff features—including backward differentiation through complex constructs like dynamic dispatch and generic interfaces—regularly utilize the CPU target (often explicitly via the -cpu flag) to verify correctness [1][2]. Regarding the "interpreter" compute target, Slang's compute targets generally refer to backends capable of executing Slang code. While Slang provides a CPU target that supports execution via C++ or LLVM [3][4], official documentation and development activity indicate that backward differentiation works in these CPU-based execution environments [1][2]. If you are referring to a specific "interpreter" mode, please note that Slang's autodiff functionality is primarily verified against its supported compute backends (CPU, Vulkan, CUDA, etc.) to ensure derivative propagation is consistent across them [1][2]. Summary of key points: - Functionality: bwd_diff is a standard operator in Slang for reverse-mode autodiff [5][6]. - CPU Support: Full support exists for bwd_diff on the CPU target [1][2]. - Reliability: CPU-based testing is a standard practice in the Slang project for validating autodiff logic because the underlying derivative propagation is independent of the compute backend [1].
Citations:
- 1: Add tests for autodiff and dynamic dispatch intersection #10734
- 2: Add regression test for autodiff with generic interface and [BackwardDerivative] #10737
- 3: https://github.com/shader-slang/slang/blob/master/docs/cpu-target.md
- 4: Compiler hangs forever on recursive [BackwardDifferentiable] function #10066
- 5: https://docs.shader-slang.org/en/stable/external/slang/docs/user-guide/07-autodiff.html
- 6: https://github.com/shader-slang/slang/blob/a6deb5ed/docs/user-guide/07-autodiff.md
🏁 Script executed:
#!/bin/bash
set -euo pipefail
echo "== file =="
cat -n tests/autodiff/generic-container-arithmetic-constraint.slang
echo
echo "== nearby autodiff tests using CPU/interpreter =="
rg -n "//TEST(:|\().*(-cpu|INTERPRET|COMPARE_COMPUTE)" tests/autodiff -g '*.slang' || true
echo
echo "== nearby generic-container autodiff tests =="
rg -n "generic-container|arithmetic-constraint|autodiff" tests/autodiff -g '*.slang' || trueRepository: shader-slang/slang
Length of output: 50374
Add a -cpu case for this regression.
This front-end constraint-unification bug is target-independent, and the current directives only exercise Slang/Vulkan/CUDA. A -cpu run would cover the same path without depending on GPU execution.
Sources: Coding guidelines, Learnings
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
78d5b61 to
43c9a07
Compare
There was a problem hiding this comment.
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
source/slang/slang-check-constraint.cpp (1)
3551-3564: 🎯 Functional Correctness | 🟠 Major | ⚡ Quick winDo not let declared-witness hint comparison reject the candidate.
This still returns the result of
TryUnifyTypeson the twosuptypes, so a failed arithmetic hint comparison rejects before the normal substituted witness proof runs. Per the PR objective, this path should mine hints only;GenericArgumentSolver::solveWitnessConstraint()should remain the accept/reject boundary.Suggested fix
- return TryUnifyTypes( + TryUnifyTypes( constraints, unificationOptions, getSup(m_astBuilder, constraintDecl1), getSup(m_astBuilder, constraintDecl2)); + return true;
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: 266736eb-b344-4082-864d-d785b3c8d809
📒 Files selected for processing (2)
source/slang/slang-check-constraint.cpptests/autodiff/generic-container-arithmetic-constraint.slang
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
43c9a07 to
ac959d7
Compare
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
nv-slang-bot
left a comment
nv-slang-bot
left a comment
There was a problem hiding this comment.
Verdict: 🟡 Has issues — 2 gaps (non-blocking)
Thanks for this — it's a small, well-motivated fix with an unusually thorough description, and the change sits at a defensible layer (the inference helper, not a syntax reconstruction or a bespoke arithmetic matcher). On the paths the reviewers could trace, the relaxation looks sound because the witness is re-proved authoritatively downstream. The two asks below are what would make the correctness argument locally verifiable rather than "plausible"; neither is a blocker, and both are things only the author can close.
The two high-value asks
1. Prove the deferral's safety net, and reconcile the description with the code. source/slang/slang-check-constraint.cpp:3544
The integer-value branch of TryUnifyVals now returns true unconditionally for any IntVal/IntVal pair that doesn't decompose into a directly bindable generic value parameter. Previously this path returned okay (i.e. false unless a TryUnifyIntParam binding succeeded), so arithmetic pairs like N+1 vs M+1 reported "no unification"; now they report success and record no constraint.
Two things would make this easy for a reviewer to trust:
- The PR description frames this as a
UnificationOptions::deferDependentIntValProofmode "used only while comparing the supertypes of two declared subtype witnesses." That flag isn't in the current diff — the relaxation is unscoped, so it applies to every caller ofTryUnifyVals(overload resolution,applyExtensionToType, generic-this-type checks), not just the witness recursion. Either re-introduce the scoping so thereturn true;is gated to the declared-subtype-witness path (keeping thefalserejection elsewhere), or update the description to own the broader scope and say why it's safe for the general case. - The new comment states that an unsatisfiable pair like
N+1vsN+2"will be rejected by the later checking/proof path." That's the load-bearing claim, but every case in the new test is a satisfiable constraint, so nothing exercises the rejection. A negative regression — a lifted constraint whose arithmetic genuinely can't hold (e.g. a model whose array size can't satisfy the constraint, orN+1vsN+2for the sameN) that still produces a conformance error — would turn "asserted" into "tested." Naming the exact function that performs that later rejection in the comment would also help.
2. Add a -cpu directive so the regression runs GPU-free. tests/autodiff/generic-container-arithmetic-constraint.slang:1
The fix is entirely in front-end generic-constraint solving, which is target-independent — without the fix these shaders fail to compile on every target, so a CPU config exercises the exact regression. But all three directives target GPU configs (-slang -compute, -vk, -cuda) with no -cpu / //TEST:INTERPRET, so the test is effectively skipped in GPU-less CI. 61 existing tests/autodiff/*.slang files already carry a -cpu line. Suggest adding:
//TEST(compute):COMPARE_COMPUTE_EX(filecheck-buffer=CHECK):-cpu -compute -output-using-type -shaderobj
Minor
Comment slightly overstates the earlier guard. source/slang/slang-check-constraint.cpp:3541
Since distinct constants were already rejected above …
The early guard (line 3516) only rejects when both operands are bare ConstantIntVal. A ConstantIntVal paired with a TypeCastIntVal-wrapped constant, or with a single-constant-term PolynomialIntVal, isn't caught above (the branch doesn't resolve()/fold the operands) and reaches this return true;. Tightening the wording to say precisely which pairs are filtered above (both-ConstantIntVal only) would keep the comment accurate. Non-blocking.
The test itself is genuinely good — it covers addition, subtraction, multiplication, division, remainder, unary negation, parentheses, a dependent default, and multiple model arguments, with both primal and backward checks, and the expected values all verify by hand. The only gap is the rejection side.
reviewed at HEAD ac959d7
🤖 Generated by an automated Slang coworker — may be inaccurate. A human maintainer should verify.
There was a problem hiding this comment.
Verdict: 🟡 Has issues — 3 gap(s), 1 question
This PR makes generic integer-value unification in TryUnifyVals return true (compatible inference hint) instead of false for non-constant IntVal pairs that don't decompose into a direct generic-parameter binding, so a lifted [BackwardDifferentiable] extension whose enclosing constraint contains arithmetic (e.g. float[3 + LatentCount]) can be matched back to the method. The change is sound for the two dominant callers (overload inference ignores the result; applyExtensionToType re-checks with equals), but the residual risk sits in a third caller with no post-solve re-validation, and the test suite covers only the positive direction.
Changes Overview
Generic value unification (source/slang/slang-check-constraint.cpp)
TryUnifyVals: for two non-constantIntVals, still attempts a directTryUnifyIntParambinding on each side, but now returnstrueunconditionally instead of returning whether a binding was made. Distinct-constant rejection (canonicalConstantIntValpairs) and direct value-parameter binding are preserved.
Regression test (tests/autodiff/generic-container-arithmetic-constraint.slang)
- New Vulkan/D3D/CUDA compute test covering primal + backward results for
+,-,*,/,%, unary negation, parentheses, multiple model arguments, and a dependent arithmetic default in a lifted differentiable constraint.
Findings (4 total)
| Severity | Location | Finding |
|---|---|---|
| 🔵 Question | source/slang/slang-check-constraint.cpp:3544 |
canSolveGenericThisTypeCompatibility trusts the new true with no post-solve equals re-check, unlike the other two callers; also TryUnifyIntParam results now silently discarded |
| 🟡 Gap | source/slang/slang-check-constraint.cpp:3541 |
"distinct constants already rejected above" only true for canonical ConstantIntVal pairs — cast-wrapped/unfolded constant mismatches now unify as true |
| 🟡 Gap | tests/autodiff/generic-container-arithmetic-constraint.slang:78 |
No negative test that a genuine arithmetic mismatch is still rejected by the later proof path |
| 🟡 Gap | tests/autodiff/generic-container-arithmetic-constraint.slang:3 |
No CPU/interpreter variant — test is skipped entirely in GPU-less CI |
reviewed: dc08a39 · diff sha256 b62b992e4341
| // inference pass can decide. Since distinct constants were already rejected above, leave | ||
| // unresolved non-constant pairs to the later checking/proof path instead of rejecting them | ||
| // here. | ||
| return true; |
There was a problem hiding this comment.
🔵 Question: return true is re-validated by two of the three callers — confirm the third is safe
The change turns a definite false (no direct binding made) into unconditional true. Tracing the three consumers of this boolean:
- Overload resolution (
slang-check-overload.cpp:~2996) — afalsewas already ignored for non-type-pack args, so the change is inert here. Safe. applyExtensionToType(slang-check-decl.cpp:~16733) — guarded by a finalif (!type->equals(targetType)) return DeclRef<ExtensionDecl>();(~16789), which catches any wrong solve. Safe — and this is the path the new test exercises.canSolveGenericThisTypeCompatibility(slang-check-decl.cpp:~18118) — rejects only onTryUnifyTypes==false, then returnstruewhenevertrySolveGenericArgumentssucceeds, with no post-solveequalsre-check.
The residual risk is concentrated in (3): when two this-types differ only in a value-parameter arithmetic term that this routine cannot bind (e.g. float[1+N] vs float[2+N], where neither side decomposes to a DeclRefIntVal), unification now adds no constraint yet returns true. Whether an incompatible derivative this-type is then accepted depends entirely on whether the solver leaves N unconstrained-but-defaulted (accept — wrong) or unsolved (reject — safe).
The binary decision: is the generic solver intended to be the sole proof for the this-type-compatibility path? If yes, please verify canSolveGenericThisTypeCompatibility cannot succeed with a value parameter left at a default when the two arithmetic terms are genuinely unequal. If that guarantee doesn't hold, mirror the post-solve this-type equals/subtype re-check that applyExtensionToType already has at slang-check-decl.cpp:~16789.
Separately on this block: the two TryUnifyIntParam call results are now discarded. TryUnifyIntParam returns false for reasons unrelated to arithmetic — e.g. !isRelevantGeneric(...) (~3744) or a non-value-param DeclRef (~3797). The comment justifies only the "cannot decompose symbolic arithmetic" case; it does not address a decomposable-but-irrelevant parameter, where the old code returned false and the new code returns true. Worth a sentence on why discarding that result is also correct.
| // Other non-constant integer values are harder: this routine does not solve arithmetic | ||
| // equations or prove symbolic inequality. For example, `N + 1` and `M + 1` may become | ||
| // equal after substitution, while `N + 1` and `N + 2` cannot; both are outside what this | ||
| // inference pass can decide. Since distinct constants were already rejected above, leave |
There was a problem hiding this comment.
🟡 Gap: "distinct constants were already rejected above" only holds for canonical ConstantIntVal pairs
The comment's premise is that the earlier guard rejects mismatched constants. But that guard (lines 3516–3522) fires only when both operands are ConstantIntVal:
if (auto fstIntVal = as<ConstantIntVal>(fst))
if (auto sndIntVal = as<ConstantIntVal>(snd))
return fstIntVal->getValue() == sndIntVal->getValue();A constant that arrives wrapped — TypeCastIntVal(int, ConstantIntVal(3)) — is not a ConstantIntVal, so it skips that guard. The existence of getDeclRefIntValIgnoringCasts (which strips TypeCastIntVal) in this very branch shows cast-wrapped values are expected here. After stripping, the base is a ConstantIntVal, not a DeclRefIntVal, so no binding is attempted and control now falls to the unconditional return true. The same applies to an unfolded PolynomialIntVal/BuiltinOperationIntVal whose sub-terms are all constant but which hasn't resolved to ConstantIntVal. So a mismatched pair like int(3) vs int(5) in one of these non-canonical forms now unifies as true, where the old code returned false.
Suggestion: Before return true, resolve/fold both operands and, when both reduce to constants, compare them and reject on mismatch (the existing arePackCountExpectedCountsEqual/coercePackCountExpectedCountToInt machinery around lines 915–947 already compares int values by canonical value). At minimum, narrow the comment to say only canonical ConstantIntVal-vs-ConstantIntVal mismatches are rejected above, so a future reader doesn't over-trust the guard.
| @@ -0,0 +1,140 @@ | |||
| //TEST(compute):COMPARE_COMPUTE_EX(filecheck-buffer=CHECK):-slang -compute -shaderobj -output-using-type | |||
| //TEST(compute, vulkan):COMPARE_COMPUTE_EX(filecheck-buffer=CHECK):-vk -compute -shaderobj -output-using-type | |||
| //TEST(compute):COMPARE_COMPUTE_EX(filecheck-buffer=CHECK):-cuda -compute -shaderobj -output-using-type | |||
There was a problem hiding this comment.
🟡 Gap: no CPU/interpreter variant — test is skipped entirely in GPU-less CI
The three directives target only D3D (-slang), Vulkan (-vk), and CUDA (-cuda), all of which require a GPU. But the changed code path (TryUnifyVals, front-end generic inference) is entirely target-independent and runs during semantic checking for every target. On GPU-less runners this test is skipped, so the fix gets zero executed coverage there.
Since ~94 existing tests/autodiff/* files already carry a -cpu line, adding a CPU variant is idiomatic and lets GPU-less environments both exercise the inference change and verify the numeric CHECK buffer values at runtime:
//TEST:COMPARE_COMPUTE_EX(filecheck-buffer=CHECK):-cpu -compute -shaderobj -output-using-type
4 participants
Motivation
Consider this example:
A differentiable method is registered by synthesizing generic extensions for its forward- and backward-differentiability conformances. Before this change, the lifted extension for
forwardcould not be applied when an enclosing constraint contained arithmetic such as3 + LatentCountor3 + 6 * SpecularCount. As a result, conformance checking reported that the visibly[BackwardDifferentiable]method did not provide the required differentiability.Proposed solution
Make generic integer-value unification distinguish "known mismatch" from "not decomposed by this helper." Distinct integer constants still fail immediately, and direct generic value parameters still produce ordinary-argument constraints. If both sides are integer values but neither path proves a mismatch or adds a direct binding, unification now returns success without adding a constraint.
This matches how the rest of generic unification is used: it should return
falsewhen it has a definite local mismatch, not when it merely lacks an algebraic proof for dependent expressions. A pair such asN + 1andM + 1might become equal after surrounding generic arguments are known, while a pair such asN + 1andN + 2will be rejected by the later checking/proof path rather than by this inference helper.This keeps the checked semantic values produced by
liftDeclFromGenericContainersas the source of truth. It does not reconstruct arithmetic syntax, add a custom equivalence relation for integer expressions, or weaken final generic-constraint validation.Change summary
SemanticsVisitor::TryUnifyValsso non-constant integer values that cannot be decomposed into a direct generic-parameter binding are treated as compatible inference hints instead of immediate failures.Concepts and vocabulary
Network : IModel<...>.Process report
SemanticsDeclHeaderVisitor::checkDifferentiableCallableCommonsynthesizes differentiability extensions throughextendContainerDecl. Because the method is nested inSampler,liftDeclFromGenericContainersclones the enclosing generic parameters and constraints. The cloned constraint is intentionally expressed using fresh parameters, so the original witness contains arithmetic overLatentCountwhile the lifted witness contains the same canonical arithmetic over a fresh lifted parameter.When
applyExtensionToTypematches the synthesized extension back to the method's function type,TryUnifyTypesreachestryUnifyGenericAppDeclRef. The generic applications include their declared constraint witnesses.TryUnifyValscompares the witnesses' supertypes to discover ordinary-argument relationships and to reject real shape mismatches.Without this change, that recursive comparison fails inside the arithmetic
IntValsub-expression. For example, the repro hitsTryUnifyValswith the witness supertypesIModel<float[N+1]>andIModel<float[N+1]>, and then with their array-size valuesN+1andN+1. The printed expressions are the same, but theirNoperands come from different generic declarations. Because the values arePolynomialIntVal/BuiltinOperationIntValrather than directDeclRefIntVals,getDeclRefIntValIgnoringCastsfinds no parameter on either whole expression and ordinary integer unification used to return false. That false bubbled back through the declared-witness comparison, so the valid lifted extension was discarded before the generic solver could substitute inferred arguments and prove the witness.The input shape is canonical and intentional: lifting must create fresh generic parameters, and
PolynomialIntVal/BuiltinOperationIntValalready preserve and substitute the checked arithmetic correctly. Fixing the producer or rebuilding an expression would create a second representation of the same semantic value. A custom arithmetic matcher would duplicate canonicalization and generic solving. The fix therefore keeps the existing direct-parameter inference path, preserves constant mismatch rejection, and treats all remaining integer-value pairs as potentially unifiable.The regression fails without the
TryUnifyValschange and passes with it. Validation performed:slangtarget built successfully.tests/autodiff/generic-container-arithmetic-constraintpasses with-api vk.-api vk:tests/autodiff/callable-constraint-witness-rollback,tests/autodiff/autodiff-generic-where-clause,tests/bugs/polynomial-int-subst, andtests/autodiff/dynamic-dispatch-autodiff-static-generic-uint.tests/language-feature/genericspasses with-api vk: 149/149 passed, 86 ignored.tests/autodiffVulkan run: 307/309 passed; the two failures are the existingfwd-diff-forceinlinedebug-info checks.git diff --checkpass.