Repository navigation
Merge subtree update for toolchain nightly-2026-09-25 - #687
Merged
Merged
Conversation
…nna-kruppe Stabilize `Vec::from_fn` Tracking issue: rust-lang#149698.
…iangfei2009 Improve into_slice_range inlining and add #[track_caller] This is a solution to rust-lang#157909. I think the root problem is that LLVM sees the many non-inlinable calls to `slice_index_fail` and decides that the function must be a bad inlining candidate. So I've shunted all the logic for reporting the right error into a single cold function and improved `try_into_slice_range` so that we only have to write all these checks once.
…=nia-e Stabilize `core::mem::DropGuard` Closes rust-lang#144426. This PR stabilizes `core::mem::DropGuard`, as per the comment in rust-lang#144426 (comment): > [nia-e]: We discussed this in today's libs meeting - DropGuard is a good name, and we agreed dismiss is Good Enough & better than the other options. Feel free to send a stabilisation PR & ask us to open FCP there! Thanks! r? @nia-e
Update doc expect messages in sync module following style guide Updates user-facing docs in the `sync` module following the style guide.
Signed-off-by: Amirhossein Akhlaghpour <m9.akhlaghpoor@gmail.com>
linux reports an address length one byte past sockaddr_un when the path fills sun_path without a NUL, which made address() slice out of bounds since e96993c. cap the length at the size of sockaddr_un.
…sync-fmt Run cargo fmt on JOSH syncs
feliperodri
added
Maintenance
…-lints Fix new Cargo lints
…k-Simulacrum std::net: clamp multicast ttl value to u8 max. on some platforms the underlying type is c_uchar, values above 255 would silently truncate.
lint ineffective #[unstable] annotations on re-exports Refs rust-lang#161153 https://rust-lang.zulipchat.com/#narrow/channel/219381-t-libs/topic/stability.20attributes.20on.20imports.20.26.20cargo-semver-checks/with/616818373
Constify more Iterator and DoubleEndedIterator functions required for Range Extracted from rust-lang#156216 Consitfies functions required for `const impl Iterator for Range`. r? clarfonthey
Autoharness on #687 failed 15 Step functions. Causes: - Misplaced contracts: upstream inserted forward_overflowing between our #[requires] and forward_unchecked in the AsciiChar, Ipv4Addr and Ipv6Addr impls. The textual merge (already in the nightly-2026-08-21 sync) left each contract on the safe forward_overflowing, so forward_unchecked was verified with no precondition at all. Move them back. - NonZero<T> got Step impls in this sync with no contracts; add them from the SAFETY comments (start + n doesn't overflow; start - n doesn't overflow or hit zero). - Two contracts were weaker than their SAFETY comments, which only showed up once they were actually checked: - AsciiChar::forward_unchecked: the result must be ASCII (<= 127), not just fit in a u8; from_u8_unchecked's b <= 127 check failed otherwise. - char::forward_unchecked: the result must be a valid char (<= char::MAX after skipping the surrogate range), not just fit in a u32; e.g. start = '\u{10FFFF}', count = 1 satisfied the old contract. All 44 Step forward/backward_unchecked functions verify locally under autoharness with Kani main. No harness stubs these contracts.
…for now - __rdl_dealloc/__rdl_realloc: autoharness used to skip them (no Arbitrary for *mut u8); Kani main now checks them, and their contracts only require a power-of-two alignment, so an arbitrary pointer reaches free/realloc. Exclude them until the contracts say ptr came from the allocator (#712). - unicode::unicode_data::conversions::to_*: since the Unicode tables were regenerated they take 53-612 s locally, exceed the 10m timeout on macOS, and the ubuntu runner died while verifying them.
Member
|
CodeQL is safe to ignore here. Of the 1,014 open alerts in files this PR touches, 1,003 are in |
Member
feliperodri
approved these changes
Oct 5, 2026
feliperodri
assigned
tautschnig and
rajath-mk and unassigned
feliperodri,
tautschnig and
rajath-mk
rajath-mk
approved these changes
Oct 5, 2026
This was referenced Oct 7, 2026
jrey8343
added a commit
to jrey8343/verify-rust-std
that referenced
this pull request
Oct 7, 2026
main's nightly-2026-09-25 sync (model-checking#687) routes one-byte needles to a new StrSearcherImpl::Byte(ByteNeedle) variant with its own arms in next, next_back, next_match and next_match_back, rewrote the Two-Way reject walks to str::ceil/floor_char_boundary, and made the Two-Way inner compare loops read through get_unchecked. The type invariant C gains a Byte clause (and n >= 2 on the Two-Way arm, which new() now guarantees), verify_str_searcher_new covers the new variant, and six verify_byte_step_* harnesses prove the inductive step for every public method on it. Shipped code is untouched. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MqLN2C9EzETaAMVsU7XsoC
feliperodri
added a commit
to feliperodri/kani
that referenced
this pull request
Oct 14, 2026
…h64 (model-checking#4964) On aarch64, `core` failed to compile under Kani, so `kani autoharness --std` failed in the `Kani Metrics (macos-latest)` job of model-checking/verify-rust-std#687. There were three separate crashes, each hidden behind the one before it. This PR fixes all three. **1. Lowering an SVE tuple type (model-checking#4963).** rustc lays out a tuple of scalable vectors, such as `svint32x4_t(svint32_t, svint32_t, svint32_t, svint32_t)`, as one `SimdScalableVector` whose `FieldsShape` holds a single offset, however many vectors it holds. `codegen_struct_fields` asserted that every field has an offset. `codegen_struct` now sends these tuples to `codegen_scalable_vector_tuple_fields`, which places the member vectors back to back. A scalable vector has no size fixed at compile time; rustc sizes it at its minimum (128 bits) and Kani does the same, so the struct adds up to the size rustc reports. **2. Building an SVE tuple value.** With (1) fixed, autoharness creates these tuples through `kani::any`, and `codegen_rvalue_aggregate` ordered the operands by the same single offset, so it passed one value for a four-field struct. For scalable vectors the operands now follow declaration order, which is the order of the fields from (1). Source code can't construct these types (rustc rejects it), so this only matters for Kani-synthesized MIR. **3. Non-power-of-two `Simd`.** `core::simd::Simd` is now `#[repr(simd, packed)]`. For a packed vector whose lane count isn't a power of two, such as `Simd<i16, 12>`, rustc's layout is `BackendRepr::Memory` (no padding) rather than `SimdVector`, and `codegen_vector` treated that as unreachable. In `core` this is hit by the NEON conversion `From<int16x4x3_t> for Simd<i16, 12>`. It isn't aarch64-specific: any harness using such a `Simd` crashed Kani on every architecture. `codegen_vector` now takes the lane count and lane type from the type (`simd_size_and_type`). CBMC aligns vectors to 1 and Kani adds struct padding itself, so a 12-lane vector has the same size and field offsets rustc gives the packed type. The SIMD intrinsics already read lanes from the type, not the layout, so nothing else changes. **What this does not do.** SVE operations are still unsupported. They are now reported as unsupported constructs on the harnesses that reach them instead of aborting the crate, e.g. `call to LLVM intrinsic llvm.aarch64.sve.ld4.sret.nxv4i32` or `sve_tuple_get is not currently supported`. Two places still read field offsets from the layout and would see only the first member of an SVE tuple: the `-Z uninit-checks` and `-Z valid-value-checks` layout code. Neither crashes; they're incomplete for these types. **Testing.** - New `tests/script-based-pre/autoharness_sve_tuple`: autoharness over functions taking and returning `svint32x2_t`/`svint32x4_t`. The pass-through functions verify, and the ones calling unsupported SVE operations fail their own harness while the run completes. It fails on `main` with the crash from model-checking#4963. It runs only on aarch64 and exits early elsewhere, since SVE doesn't exist on other targets. - New `tests/kani/SIMD/non_power_of_two_lanes.rs`: arithmetic and lane indexing on `Simd<i16, 12>`, a `Simd<u8, 3>` mask, transmutes, size and `offset_of!` in a `repr(C)` struct, and pointer lanes. It crashes on `main`. I checked that wrong assertions in it fail, so it isn't vacuous. - `kani` suite `SIMD` and `Intrinsics`, `expected` `simd` and `script-based-pre` `simd` pass on macOS arm64, except `kani/SIMD/simd_bitmask_equiv.rs`, which fails the same way on unmodified `main` on that machine. fmt and clippy are clean. - Full standard library: `kani autoharness -Z autoharness -Z mem-predicates --list --std ./library` on the nightly-2026-09-25 `library/` (with `kani_lib!` injected into `core`) on macOS arm64 completes with exit 0 and lists 30,034 automatic harnesses. On `main` it crashes in `svld4_s32`. - Not run: the full regression suite, and the run against verify-rust-std's own `library/`. Resolves model-checking#4963 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
2 tasks done
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
20 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR merges library subtree updates from 2026-02-05 (rust-lang/rust@db3e99b) to 2026-09-25 (rust-lang/rust@f7575a9) (inclusive) into main.
It was opened automatically for nightly-2026-08-21 and has since been moved forward to nightly-2026-09-25, the toolchain of Kani
main, which this repository's toolchain is coupled to. Kani is pinned tomain(1640445d), which carries the autoharness fixes this sync needed (model-checking/kani#4819, rust-lang#4848, rust-lang#4869, rust-lang#4801, rust-lang#4927, rust-lang#4951). Flux is pinned tomain(849ef7c3, flux-rs/flux#1802).Known open items:
linked_list.rsandraw_vecconflict with the upstream changes and still need updating.Verify contracts with goto-transcoder: ESBMC segfaults on contracts generated by Kanimain(goto-transcoder: ESBMC 7.10 segfaults reading contracts generated by Kani main (CBMC 6.11) #708).Do not remove or edit the following annotations:
git-subtree-dir: library
git-subtree-split: 066e3de