From 6a4fcf383f8ed3ade68b03ac3e9995a4857984ee Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 21 Jul 2026 22:16:44 +0000 Subject: [PATCH] Do not inject macro overrides into external dependencies Kani's macro-override injection (#[macro_use] extern crate std as _kani_std_macros, introduced in #4643) places the assert!/panic!/... overrides in the macro_use-prelude scope of every std crate compiled by kani-compiler. That scope silently shadows the standard prelude, but is ambiguous (E0659) against an explicit glob import of the same macro name. External crates may legitimately contain such imports: libc's internal prelude re-exports core::assert and its modules glob-import that prelude, and as of libc 0.2.188 (published 2026-07-21) it also calls assert! in such a module, breaking compilation of every crate graph containing it: error[E0659]: `assert` is ambiguous --> .../libc-0.2.188/src/types.rs:73:5 Restrict the injection to local crates: cargo passes --cap-lints allow exactly for non-local (registry/git) dependencies, so use Session::opts.lint_cap as the discriminator. External dependencies then use the real assert!/panic!/... macros, which Kani models soundly - consistent with no_std dependencies, which never had the overrides. Local path/workspace dependencies and standalone kani builds keep the overrides, preserving the reachability/message behavior pinned by the assert-reach and stubbing-ws-packages tests. The existing cargo-kani/libc test (with its floating libc = "0.2" requirement) covers the regression: it fails against libc 0.2.188 without this change and passes with it, as does the full cargo-kani suite (71 tests). Resolves: #4665 Co-authored-by: Kiro --- kani-compiler/src/kani_compiler.rs | 14 ++++++++++++++ library/std/src/lib.rs | 5 +++-- 2 files changed, 17 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 88b996f6a2d..94510e24427 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -170,6 +170,20 @@ impl Callbacks for KaniCompiler { // injecting `extern crate std` there would pull in a *second* `std` // (and `core`), causing duplicate-lang-item errors (E0152). && compiler.sess.opts.externs.get("std").is_some() + // Do not inject into external (registry/git) dependencies: the + // `#[macro_use]` scope is ambiguous (E0659) with an explicit glob + // import of the same macro name, and external crates may + // legitimately do that (e.g. libc >= 0.2.188 re-exports + // `core::assert` in an internal prelude that its modules + // glob-import, and calls `assert!`). External dependencies thus + // use the real `assert!`/`panic!`/... macros, which Kani models + // soundly, consistent with `no_std` dependencies which never had + // the overrides. Cargo passes `--cap-lints allow` exactly for + // non-local dependencies, so use that as the discriminator (like + // rustc's `Session::opts` consumers do for dependency-only + // behavior); local path/workspace crates and standalone `kani` + // builds keep the overrides. + && compiler.sess.opts.lint_cap.is_none() { inject_kani_macro_overrides(compiler, krate); } diff --git a/library/std/src/lib.rs b/library/std/src/lib.rs index 915f7275ea1..694e2eb4b1e 100644 --- a/library/std/src/lib.rs +++ b/library/std/src/lib.rs @@ -32,8 +32,9 @@ pub mod prelude { // Kani's versions here makes `#![no_std]` dependencies that import this prelude // explicitly (`extern crate std; use std::prelude::v1::*;`, e.g. lazy_static) // ambiguous against the injected core prelude (E0659). Instead, kani-compiler - // injects those overrides only into the crate under verification (see - // kani_compiler's macro-override injection). The print family is defined in this + // injects those overrides only into local crates, not external (registry/git) + // dependencies (see kani_compiler's macro-override injection). The print family + // is defined in this // crate (std) with no core-prelude counterpart, so overriding it here is safe and // applies everywhere (dependencies included), which is important so that a // dependency's `println!` does not run real formatting/IO during verification.