tqchen opened a new pull request, #19638:
URL: https://github.com/apache/tvm/pull/19638
## Summary
Phase out `src/arith/scalable_expression.{h,cc}`. The arith layer no longer
attempts to prove anything about scalable vectors — proofs that depended on
`Target::Current()` are removed. Scalable vectors remain a first-class concept;
arith just doesn't reason about their lengths.
## Use-site summary
Only 16 call sites total across 7 symbols (9 live, 7 proof-related).
| Symbol | Live callers (kept) | Proof callers (deleted) | New home |
|---|---|---|---|
| `ExtractVscaleFactor` | 4 × `arith/rewrite_simplify.cc` + 2 ×
`tirx/ir/expr.cc` | — | file-local in each |
| `IsVScaleCall` | 1 × `tirx/op/op.cc` + 1 ×
`tirx/transform/vectorize_loop.cc` | — | inline at use sites |
| `ContainsVscaleCall` | 4 × `arith/rewrite_simplify.cc` + 1 ×
`s_tir/schedule/ir_comparator.cc` | — | inline at use sites |
| `TargetHasVLA` | 2 × `tirx/transform/vectorize_loop.cc` | analyzer.cc +
const_int_bound.cc | local in vectorize_loop.cc |
| `GetVScaleValues` | 1 × `target/llvm/codegen_aarch64.cc` | analyzer.cc +
const_int_bound.cc | inlined at codegen_aarch64 |
| `CanProveVscaleExpressionFromKnownValues` | — | analyzer.cc | DELETE |
| `SubstituteVScaleWithKnownValue` | — | internal only | DELETE |
## Changes (6 commits)
1. Move `ExtractVscaleFactor` to file-local anonymous-namespace helpers in
`rewrite_simplify.cc` and `tirx/ir/expr.cc`. Function is small; per-file
duplication is cleaner than a shared header.
2. Inline `IsVScaleCall` / `ContainsVscaleCall` / `TargetHasVLA` at call
sites (1-3 line predicates, anonymous-namespace per consumer `.cc`).
3. Drop the scalable-vector proof scaffolding from `arith/analyzer.cc`
(substitution-proof loop) and `arith/const_int_bound.cc` (vscale branch).
`vscale()` calls fall back to `Everything()` — no special bound narrowing.
4. Delete `scalable_expression.{h,cc}`. Inline the `GetVScaleValues` body at
`codegen_aarch64.cc` (computes `max_val = vector_width / 8` floor-rounded to a
power of two for the LLVM `vscale_range` attribute).
5. Mark `pytest.mark.xfail` on 19 tests that relied on the deleted
substitution-proof loop.
6. `pre-commit` line-length cleanup.
## Compatibility / intentional regression
This is a hard break for any consumer of the deleted symbols. They were
already in a private header (`src/arith/scalable_expression.h`, not under
`include/`).
19 tests that proved vscale-bearing inequalities on SVE / RVV are xfailed.
The proofs were target-dependent and the new policy is that arith does not
attempt them.
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
To unsubscribe, e-mail: [email protected]
For queries about this service, please contact Infrastructure at:
[email protected]
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]