error: `compiler_builtins` cannot call functions through upstream monomorphizations

[zjp-CN]

error: `compiler_builtins` cannot call functions through upstream monomorphizations; encountered invalid call from `core::ops::index_range::IndexRange::next_unchecked` to `core::ops::index_range::IndexRange::next_unchecked::kani_contract_mode`
  --> /home/runner/work/distributed-verification/distributed-verification/verify-rust-std/library/core/src/ops/index_range.rs:63:5
   |
63 |     #[cfg_attr(kani, kani::modifies(self))]
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = note: this error originates in the attribute macro `kani::modifies` (in Nightly builds, run with -Z macro-backtrace for more info)

dv fails to compile compiler_builtins at 58b34c8

https://github.com/os-checker/distributed-verification/actions/runs/17088072312/job/48456215614

cc

• -Zbuild-std shouldn't explode on compiler-builtins fragility rust-lang/rust#137222
• Is passing -Clink-dead-code by default still a good idea? rust-fuzz/cargo-fuzz#391
• https://github.com/model-checking/verify-rust-std/pull/451/files#diff-4560688b121853f7240d9741469cc46eafadc5d007b423e8a76e8f0d0de50f75 as the introduction of such annotations
• kani::modifies causes an error that compiler_builtins cannot call functions through upstream monomorphizations model-checking/verify-rust-std#477

But I've checked no -Clink-dead-code is specified anywhere.

---

When the attribute is removed on IndexRange::next_unchecked, all crates compile fine. 🤔
So not sure if this is a regression or something going wrong.

[zjp-CN]

After several hours debuging, it turns out the error is from compiling compiler_builtins crate, instead of libcore:

(but why the error comes from kani attribute in libcore???)

error: `compiler_builtins` cannot call functions through upstream monomorphizations; 
encountered invalid call from `core::ops::index_range::IndexRange::next_unchecked` to `core::ops::index_range::IndexRange::next_unchecked::kani_contract_mode`
   --> /home/gh-zjp-CN/distributed-verification/verify-rust-std/library/core/src/ops/index_range.rs:63:5
    |
 63 |     #[cfg_attr(kani, kani::modifies(self))]
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ in this attribute macro expansion
    |
   ::: /home/gh-zjp-CN/distributed-verification/kani/library/kani_macros/src/lib.rs:427:1
    |
427 | pub fn modifies(attr: TokenStream, item: TokenStream) -> TokenStream {
    | -------------------------------------------------------------------- in this expansion of `#[kani::modifies]`

Mentioned src localtions:

• verify-rust-std/library/core/src/ops/index_range.rs:63:5
• kani/library/kani_macros/src/lib.rs:427:1

[rustc] args=[
    "--crate-name",
    "compiler_builtins",
    "--edition=2024",
    "/home/gh-zjp-CN/distributed-verification/verify-rust-std/library/compiler-builtins/compiler-builtins/src/lib.rs",
    "--error-format=json",
    "--json=diagnostic-rendered-ansi,artifacts,future-incompat",
    "--diagnostic-width=142",
    "--crate-type",
    "lib",
    "--emit=dep-info,metadata,link",
    "-C",
    "embed-bitcode=no",
    "-C",
    "debuginfo=2",
    "--cfg",
    "feature=\"compiler-builtins\"",
    "--cfg",
    "feature=\"default\"",
    "--cfg",
    "feature=\"rustc-dep-of-std\"",
    "--check-cfg",
    "cfg(docsrs,test)",
    "--check-cfg",
    "cfg(feature, values(\"c\", \"compiler-builtins\", \"default\", \"mangled-names\", \"mem\", \"no-asm\", \"no-f16-f128\", \"rustc-dep-of-std\", \"unstable-pu
blic-internals\"))",
    "-C",
    "metadata=c7bad5c9056cfff6",
    "-C",
    "extra-filename=-8d1e20b7ed578fdb",
    "--out-dir",
    "/home/gh-zjp-CN/distributed-verification/tests/dummy-crate/target/debug/deps",
    "-Z",
    "force-unstable-if-unmarked",
    "-L",
    "dependency=/home/gh-zjp-CN/distributed-verification/tests/dummy-crate/target/debug/deps",
    "--extern",
    "core=/home/gh-zjp-CN/distributed-verification/tests/dummy-crate/target/debug/deps/libcore-65823dc2d235ebd6.rmeta",
    "--cap-lints",
    "allow",
    "-Cpanic=abort",
    "-Csymbol-mangling-version=v0",
    "-Coverflow-checks=on",
    "-Zunstable-options",
    "-Ztrim-diagnostic-paths=no",
    "-Zhuman_readable_cgu_names",
    "-Zalways-encode-mir",
    "-Zcrate-attr=feature(register_tool)",
    "-Zcrate-attr=register_tool(kanitool)",
    "-Zub-checks",
    "-Zpanic_abort_tests=yes",
    "-Zmir-enable-passes=-RemoveStorageMarkers",
    "--check-cfg=cfg(kani)",
    "--cfg=kani",
    "-Zmacro-backtrace",
    "-L",
    "/home/gh-zjp-CN/distributed-verification/kani/target/kani/no_core/lib",
    "--extern=kani_core",
    "--cfg",
    "f16_enabled",
    "--cfg",
    "f128_enabled",
    "--cfg",
    "intrinsics_enabled",
    "--cfg",
    "arch_enabled",
    "--cfg",
    "feature=\"unstable-intrinsics\"",
    "--cfg",
    "feature=\"mem-unaligned\"",
    "--check-cfg",
    "cfg(__ashldi3, values(\"optimized-c\"))",
    "--check-cfg",
    "cfg(__ashlsi3, values(\"optimized-c\"))",
    "--check-cfg",
    "cfg(__ashrdi3, values(\"optimized-c\"))",
    "--check-cfg",
    "cfg(__ashrsi3, values(\"optimized-c\"))",
    "--check-cfg",
    "cfg(__bswapsi2, values(\"optimized-c\"))",
    "--check-cfg",
    "cfg(__bswapdi2, values(\"optimized-c\"))",
    "--check-cfg",
    "cfg(__bswapti2, values(\"optimized-c\"))",
...
    "--check-cfg",
    "cfg(__aarch64_swp8_acq_rel, values(\"optimized-c\"))",
    "--check-cfg",
    "cfg(target_feature, values(\"vis3\"))",
    "--check-cfg",
    "cfg(feature, values(\"checked\"))",
    "--check-cfg",
    "cfg(assert_no_panic)",
    "--check-cfg",
    "cfg(thumb)",
    "--check-cfg",
    "cfg(thumb_1)",
    "--check-cfg",
    "cfg(x86_no_sse)",
    "--check-cfg",
    "cfg(f16_enabled)",
    "--check-cfg",
    "cfg(f128_enabled)",
    "--check-cfg",
    "cfg(intrinsics_enabled)",
    "--check-cfg",
    "cfg(arch_enabled)",
    "--check-cfg",
    "cfg(optimizations_enabled)",
    "--check-cfg",
    "cfg(feature, values(\"unstable-public-internals\"))",
    "--check-cfg",
    "cfg(optimizations_enabled)",
    "--check-cfg",
    "cfg(kernel_user_helpers)",
    "--check-cfg",
    "cfg(feature, values(\"mem-unaligned\"))",
]

[zjp-CN]

Normal build-std outputs:

$ __CARGO_TESTS_ONLY_SRC_ROOT=/home/gh-zjp-CN/distributed-verification/verify-rust-std/library cargo build -Zbuild-std=core -j 1
   Compiling proc-macro2 v1.0.101
   Compiling unicode-ident v1.0.18
   Compiling version_check v0.9.5
   Compiling quote v1.0.40
   Compiling proc-macro-error-attr v1.0.4
   Compiling syn v1.0.109
   Compiling proc-macro-error v1.0.4
   Compiling safety v0.1.0 (/home/gh-zjp-CN/distributed-verification/verify-rust-std/library/contracts/safety)
   Compiling syn v2.0.106
   Compiling compiler_builtins v0.1.160 (/home/gh-zjp-CN/distributed-verification/verify-rust-std/library/compiler-builtins/compiler-builtins)
   Compiling core v0.0.0 (/home/gh-zjp-CN/distributed-verification/verify-rust-std/library/core)
   Compiling dummy-crate v0.1.0 (/home/gh-zjp-CN/distributed-verification/tests/dummy-crate)
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 17.12s

While in my case, libcore is compiled successfully. I think compiler_builtins should be compiled before libcore, but from my observation in logging with -j 1, libcore is compiled before compiler_builtins.

[zjp-CN]

Waiting for model-checking/kani#4312 to merge and verify-rust-std to update kani.