[water] verify index expr step/strire are positive#1051
[water] verify index expr step/strire are positive#1051ftynse wants to merge 1 commit intousers/ftynse/non-unit-stepfrom
Conversation
Add a verifier that index expression step and stride are strictly positive to avoid semantically undefined behavior (what does it mean to have a 0-element piece of the tensor? stride zero is hidden broadcasting, negative stride is hidden reversal, both are deterimental to dependence analysis). Closes #1012. Signed-off-by: Alex Zinenko <git@ozinenko.com>
ftynse
requested review from
Copilot and
martin-luecke
and removed request for
Copilot
There was a problem hiding this comment.
Pull request overview
Adds verification to reject semantically undefined Wave index mappings by requiring index-expression step and stride to be strictly positive when they can be folded to a concrete value (with hyperparameters substituted), improving correctness for dependence analysis.
Changes:
- Add Wave dialect verification for strictly-positive
step/strideand retain “at most one non-unit step” enforcement when foldable. - Add MLIR negative tests covering zero/negative
stepandstride. - Update ElementsPerThread inference commentary and adjust an inference test setup.
Reviewed changes
Copilot reviewed 4 out of 4 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
water/lib/Dialect/Wave/IR/WaveDialect.cpp |
Introduces verifier helpers to enforce positive step/stride and integrates them into dialect verification flow. |
water/test/Dialect/Wave/ops-invalid.mlir |
Adds invalid IR tests asserting new verifier diagnostics for zero/negative step/stride. |
water/lib/Dialect/Wave/Transforms/InferTypes.cpp |
Updates TODO commentary around redundancy with verifiers and hyperparameter presence. |
water/test/Dialect/Wave/propagate-elements-per-thread.mlir |
Adjusts a test function’s attributes related to hyperparameters for inference-pass behavior. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| if (failed(verifyIndexStepAndStride(op, hyperparams))) | ||
| return WalkResult::interrupt(); |
There was a problem hiding this comment.
verifyIndexStepAndStride is only invoked while verifying the presence of the wave.hyperparameters attribute. This means ops without wave.hyperparameters can still contain an index mapping with constant step/stride <= 0 (which evaluateMapWithHyperparams can fold even without hyperparams), and they will pass verification. To fully enforce the “step/stride must be strictly positive” rule, consider running this check from the HasWaveIndexMapping trait verifier (verifyWaveIndexMappings) and using an empty/default hyperparam set when none is provided (similar to verifyIndexElementsPerThread).
martin-luecke
left a comment
martin-luecke
left a comment
There was a problem hiding this comment.
LGTM, just typos
- typo in PR title: strire → stride
- typo in body: deterimental → detrimental
Add a verifier that index expression step and stride are strictly
positive to avoid semantically undefined behavior (what does it mean to
have a 0-element piece of the tensor? stride zero is hidden
broadcasting, negative stride is hidden reversal, both are deterimental
to dependence analysis).
Closes #1012.