Toolchain update 06-01-2025

[remi-delmas-3000]

Please review commit by commit, as each commit propagates an upstream change:

• SourceRegion was moved from MIR to the LLVM backend and made private, I recreated the type and functionality locally to preserve our handling of regions in coverage assertions,
• Propagated changes to the representation of uninhabited enums (with no variants),
• Propagated remove of RValue::Len(place) from MIR (still present in stable MIR, so I used PtrMetadata(Copy(place)) to translate Len(place) back from StableMIR to MIR).
• Propagated addition of UnsafeBinder enum variant (WIP in rustc, no clear semantics yet, left as TODO)

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[qinheping]

Could you also include the information about related upstream commits?

[remi-delmas-3000]

Could you also include the information about related upstream commits?

Each commit message contains the link to the upstream change

[remi-delmas-3000]

All tests passing now

[celinval]

Looks good to me. Thanks!

[qinheping]

LGTM

[remi-delmas-3000]

Reverting from using LineInfo from stable MIR back to using our own SourceRegion as they seem to represent different things:

https://github.com/Zalathar/rust/blob/aced4dcf1047aab08b769b34fae9d4ba7de87f04/compiler/rustc_codegen_llvm/src/coverageinfo/mapgen/spans.rs#L1[…]C33
https://github.com/rust-lang/rust/blob/6afee111c2faf86ba884ea748967130abad37b52/compiler/rustc_smir/src/rustc_smir/context.rs#L300

1 |// Copyright Kani Contributors
2 |// SPDX-License-Identifier: Apache-2.0 OR MIT
3 |
4 |//! Checks that `check_assert` is fully covered. At present, the coverage for
5 |//! this test reports an uncovered single-column region at the end of the `if`
6 |//! statement: <https://github.com/model-checking/kani/issues/3455>
7 |
8 |#[kani::proof]
9 |fn check_assert() {
10|    let x: u32 = kani::any_where(|val| *val == 5);
11|    if x > 3 {
12|        assert!(x > 4);
13|    }
14|}

SUMMARY:
 ** 0 of 7 failed

VERIFICATION:- SUCCESSFUL

Source-based code coverage results:
// using SourceRegion
test.rs (check_assert)
 * 9:1 - 10:34 COVERED
 * 11:14 - 13:6 COVERED
 * 13:5 - 13:6 UNCOVERED <--- difference here

test.rs (check_assert::{closure#0})
 * 10:40 - 10:49 COVERED

 // using LineInfo
 test.rs (check_assert)
 * 9:1 - 10:34 COVERED
 * 11:14 - 13:6 COVERED
 * 13:6 - 13:6 UNCOVERED <--- difference here

test.rs (check_assert::{closure#0})
 * 10:40 - 10:49 COVERED

with LineInfo we get 13:6 - 13:6 for the lone closing brace on line 13, SourceRegion gives 13:5 - 13:6.
I'm sticking with SourceRegion for now to preserve the interface to LLVM coverage formatting tool used by kani-coverage. Differences could be on the interpretation of the interval as inclusive or non-inclusive of the upper bound, or the units used for columns (in SourceRegion column indices are in bytes, for line info it could be number of characters).