Slice iter cleanup - #146436
Conversation
This comment has been minimized.
This comment has been minimized.
88ef0cf to
7d88079
Compare
This comment has been minimized.
This comment has been minimized.
9f37d58 to
e62ac74
Compare
|
r? libs |
|
Going to pass this one along. r? libs |
e62ac74 to
62fc4c9
Compare
This comment has been minimized.
This comment has been minimized.
62fc4c9 to
67e3167
Compare
|
@rustbot ready Perhaps a perf run to see if I haven't regressed anything unwittingly? |
| // SAFETY: Nothing else points to or will point to the contents of this slice. | ||
| Some(unsafe { &mut *head }) | ||
| } | ||
| // SAFETY: we have `&mut self`, so are allowed to temporarily materialize a mut slice |
There was a problem hiding this comment.
I'd add that next must not be called if __get_unchecked was called, so invalidating previously returned items does not conflict with TrustedRandomAccess.
There was a problem hiding this comment.
While that is true, I don't see how this particular next method is special in that regard. So would you then like all next methods of iterators that impl TrustedRandomAccess to get such a comment?
67e3167 to
8a668bd
Compare
|
This PR was rebased onto a different master commit. Here's a range-diff highlighting what actually changed. Rebasing is a normal part of keeping PRs up to date, so no action is needed—this note is just to help reviewers. |
|
@joboet Thanks for reviewing so far; your comments have been very helpful! I've removed all uses of overflowing_* and also switched all remaining conditions like |
| if self.v.is_empty() { | ||
| (0, Some(0)) | ||
| } else { | ||
| let n = self.v.len() / self.chunk_size; | ||
| let rem = self.v.len() % self.chunk_size; | ||
| let n = if rem > 0 { n + 1 } else { n }; | ||
| let n = (self.v.len() - 1) / self.chunk_size + 1; | ||
| (n, Some(n)) | ||
| } |
There was a problem hiding this comment.
I changed 4 cases of this manual div_ceil to the real thing..
8a668bd to
b60788e
Compare
|
@bors r+ |
Slice iter cleanup
Rollup of 5 pull requests Successful merges: - #146436 (Slice iter cleanup) - #148250 (array_chunks: slightly improve docs) - #148678 (Merge E0412 into E0425) - #149520 (also introduce Peekable::next_if_map_mut next to next_if_map) - #149538 (std: sys: fs: uefi: Make time in FileAttr optional) r? `@ghost` `@rustbot` modify labels: rollup
Rollup merge of #146436 - hkBst:slice-iter-1, r=joboet Slice iter cleanup
slice iter cleanup: replace checked_sub with saturating_sub Continuation of rust-lang#146436 r? `@joboet`
slice iter cleanup: replace checked_sub with saturating_sub Continuation of rust-lang#146436 r? ``@joboet``
slice iter cleanup: replace checked_sub with saturating_sub Continuation of rust-lang/rust#146436 r? `@joboet`
The `inet::checksum::tests::differential` harness in s2n-quic-core uses `InlineVec<u8, LEN>` under cfg(kani) with `LEN = 16`. On the nightly-2025-12-04 toolchain (rust-lang/rust#146436, "Slice iter cleanup"), this harness's symex/SSA cost grew enough that peak RSS exceeds the 16 GB GH-hosted runner ceiling, producing the "runner has received a shutdown signal" (exit 143) failure mode. Drop LEN to 8 via the existing perf overlay mechanism, which copies files from `tests/perf/overlays/s2n-quic/` into the s2n-quic submodule before the perf suite runs (see `tests/perf/overlays/README.md`). The upstream s2n-quic source remains untouched; only the verification-time state space shrinks. This does not affect Kani's soundness guarantee on the bounded check that still runs: Kani still proves the property for all `InlineVec<u8, 8>` inputs. The trade-off is verification breadth on this specific harness; the property under check is unchanged. Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
The `inet::checksum::tests::differential` harness ships with `kani::unwind(17)`, sized for the upstream `LEN = 16`. After lowering LEN to 8 in the perf overlay (commit 232eb2a), unwind=9 (LEN + 1) is the smallest sufficient bound to fully unroll the inner `chunks_exact(2)` loop and the surrounding slice walk; carrying the upstream value of 17 multiplies CBMC's symex cost on the post-#146436 path tree for no additional verification benefit. This restores baseline perf on this harness when run against nightly-2025-12-04 (rust-lang/rust#146436): Wall: 18 min (killed) -> 131 s (vs 134 s on nightly-2025-12-03) RSS: 6.42 GB -> 3.18 GB (vs 2.81 GB on nightly-2025-12-03) Result: 0 of 5 verified -> 5 of 5 verified Soundness is preserved: `kani::unwind(N)` instructs CBMC to unroll loops up to N iterations and assert the bound is sufficient. With LEN=8 the inner `chunks_exact(2)` loop has at most 4 iterations, so unwind=9 is well above the necessary depth. If LEN ever grows back, the unwinding-assertion will catch it. Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Minimal reproducer for the CBMC symex constant-propagation limitation exposed by rust-lang/rust#146436 ("Slice iter cleanup"): a symbolic-index `split_at` niche-encodes the resulting slice's data pointer as a `(cond ? base : NULL)` select, which defeats folding of the `Option` niche discriminant that `ChunksExact::next` now uses, so `chunks_exact` loops unwind to the `--unwind` bound instead of their true trip count. The `poisoned_chunks_exact` harness produces a far larger SAT instance than the `control_clean` harness for equivalent concrete chunking work; `poisoned_split_at_checked` shows a direct `split_at_checked` loop (no `and_then` closure) is unaffected. All three verify successfully. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
## Summary Upgrades the Rust toolchain from `nightly-2025-12-03` to `nightly-2025-12-04`. That toolchain includes rust-lang/rust#146436 ("Slice iter cleanup"), which triggers a large verification-time/memory regression in Kani's CBMC back-end on the s2n-quic-core `inet::checksum::tests::differential` harness — originally enough to exhaust the 16 GB GitHub-hosted `perf` runner and surface as an unattributable "runner has received a shutdown signal" (exit 143). This PR performs the bump, works around the regression on the affected harness via the perf overlay, adds a regression test that captures the underlying issue, and hardens the `perf` job (including fixing a latent compiletest deadlock) so any future runaway is an attributable test failure rather than a runner kill. ## Root cause #146436 rewrote `core::slice::iter`: `ChunksExact::next` now decides Some/None through `split_at_checked(..).and_then(..)`, i.e. via the niche-encoded (null = None) discriminant of `Option<(&[T], &[T])>`. On the harness's hot path (`write_sized_generic`), a symbolic-index `split_at` makes the slice data pointer a `(cond ? base : NULL)` select, so CBMC's symbolic execution can no longer fold the loop-exit guard and `chunks_exact` unwinds to the `--unwind` bound. With everything else fixed (same Kani, CBMC, solver) and only the toolchain changing, both symex *and* SAT blow up — the encoded problem itself grows, it is not merely more expensive to encode: | | 12-03 | 12-04 | |---|---|---| | Symex | 25 s | 326 s | | SAT variables | 1.7M | 11M | | SAT clauses | 6.3M | 87M | | Total solving | ~166 s | ~858 s | | Peak RSS | 2.3 GB | ~20 GB | ## Changes - **Toolchain bump to `nightly-2025-12-04`** (`rust-toolchain.toml`). - **Shrink the regressing harness via the perf overlay** (submodule untouched): lower `cfg(kani)` `LEN` 16→8 and `kani::unwind` 17→9 (`LEN + 1`, the smallest bound that fully unrolls the loops). `differential` verifies in ~2–3 min again. Sound: unwinding assertions stay on and pass, the property still holds for all `InlineVec<u8, 8>` inputs; only verification breadth (8 vs 16 bytes) narrows. - **Add a regression test** (`tests/kani/Iterator/chunks_exact_split_at.rs`): a freestanding minimal reproducer of the constant-propagation failure. - **Fix a latent compiletest `--timeout` deadlock** (`tools/compiletest`): it waited on the child before draining stdout/stderr, so any test whose output exceeds the pipe buffer hung until the timeout — hanging every perf test once the suite passed `--timeout`. Now drains both pipes on dedicated threads (removes the unused `read2` helper). - **Bound per-test wall time** in `scripts/kani-perf.sh` (`--timeout`, default 2400 s, override via `KANI_PERF_TEST_TIMEOUT`). Sized above the slowest *legitimate* test: s2n-quic-core runs 34 harnesses (~1250 s; the largest is `sync::spsc::tests::alloc_test` ~375 s, not `differential`) — not a regression, as it passes cap-free on main (~2650 s full suite, matching this branch). - **Harden the `perf` job** (`.github/workflows/kani.yml`): fit the `timeout-minutes` budgets and add `nick-fields/retry@v3` for spot-preemption. - **Skip `tests/perf/overlays` in the rustfmt sweep** (`scripts/kani-fmt.sh`): overlay files reference submodule-only sibling `mod`s, so rustfmt can't standalone-parse them. - **Kani copyright header on the overlay** (with upstream attribution). - **Gate debug-only `CallGraph::dump_*` on `cfg(debug_assertions)`** (`kani-compiler/.../reachability.rs`): otherwise release builds trip `dead_code`. ## Not addressed This does not fix the upstream rustc regression itself and does not skip any harness. A deeper fix (a CBMC-side improvement to the niche/`split_at` constant-propagation, or filing the reproducer upstream) is a follow-up; the regression test added here documents the trigger. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Signed-off-by: Felipe R. Monteiro <felisous@amazon.com> Co-authored-by: celinval <35149715+celinval@users.noreply.github.com> Co-authored-by: Michael Tautschnig <tautschn@amazon.com> Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Rollup of 5 pull requests Successful merges: - rust-lang/rust#146436 (Slice iter cleanup) - rust-lang/rust#148250 (array_chunks: slightly improve docs) - rust-lang/rust#148678 (Merge E0412 into E0425) - rust-lang/rust#149520 (also introduce Peekable::next_if_map_mut next to next_if_map) - rust-lang/rust#149538 (std: sys: fs: uefi: Make time in FileAttr optional) r? `@ghost` `@rustbot` modify labels: rollup
No description provided.