Add --no-assert-overrides escape hatch for macro-override conflicts - #4687
Open
tautschnig wants to merge 1 commit into
Open
Add --no-assert-overrides escape hatch for macro-override conflicts#4687tautschnig wants to merge 1 commit into
tautschnig wants to merge 1 commit into
Conversation
github-actions
Bot
added
Z-EndToEndBenchCI
Contributor
There was a problem hiding this comment.
Pull request overview
This PR adds an escape-hatch flag, --no-assert-overrides, to avoid rustc E0659 macro ambiguity errors caused by Kani’s macro-override injection (notably in crates that glob-import a prelude re-exporting core::assert, such as libc patterns). The flag keeps verification sound by falling back to standard macros (assertion failures still surface as panics), while preserving the current default behavior for users who don’t opt in.
Changes:
- Add
--no-assert-overridestokani-driverCLI and forward it tokani-compiler. - Teach
kani-compilerto skip injecting Kani macro overrides when the flag is set. - Add a script-based regression test reproducing the libc-style glob-vs-outer macro ambiguity and validating behavior with/without the flag.
Reviewed changes
Copilot reviewed 9 out of 9 changed files in this pull request and generated 1 comment.
Show a summary per file
| File | Description |
|---|---|
| tests/script-based-pre/cargo_no_assert_overrides/src/lib.rs | Minimal crate reproducer for the E0659 ambiguity and a failing harness to confirm soundness when overrides are disabled. |
| tests/script-based-pre/cargo_no_assert_overrides/no-assert-overrides.sh | Script-based test driver: expects E0659 without the flag; runs verification with the flag. |
| tests/script-based-pre/cargo_no_assert_overrides/no-assert-overrides.expected | Expected key output lines for both runs (ambiguity error + verification failure summary). |
| tests/script-based-pre/cargo_no_assert_overrides/config.yml | Registers the script-based test and expected exit code. |
| tests/script-based-pre/cargo_no_assert_overrides/Cargo.toml | Declares the test crate and configures cfg(kani) checking. |
| kani-driver/src/call_single_file.rs | Forwards --no-assert-overrides into the compiler argument list for single-file mode. |
| kani-driver/src/args/mod.rs | Introduces the new CLI flag in VerificationArgs with user-facing documentation. |
| kani-compiler/src/kani_compiler.rs | Adds a new compiler-side switch and gates macro-override injection on it. |
| kani-compiler/src/args.rs | Adds --no-assert-overrides to kani-compiler’s argument parser. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
169
to
172
| if !self.build_std | ||
| && !self.no_assert_overrides | ||
| && !attr::contains_name(&krate.attrs, sym::no_std) | ||
| && !attr::contains_name(&krate.attrs, sym::no_core) |
Kani injects '#[macro_use] extern crate std as _kani_std_macros;' so that its assert!/panic!/... overrides shadow the prelude macros. rustc's restricted shadowing makes a glob import of the same macro name ambiguous with the macro_use prelude (E0659, hard error, kind GlobVsOuter), so crates that glob-import a module re-exporting core::assert cannot compile under Kani. PR model-checking#4666 already skips the injection for external dependencies, but the same pattern in the crate under verification (e.g. verifying libc itself, whose prelude! macro re-exports core::assert) still fails. Add a --no-assert-overrides flag that skips the injection for the local crate too. Verification remains sound: assertion failures are reported as generic panics rather than with the original condition/message. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
fix-macro-overrides-optout
branch
from
July 29, 2026 00:42
27508d1 to
f9b9e2f
Compare
feliperodri
approved these changes
Jul 29, 2026
Comment on lines
+5
to
+8
| echo "[without flag]" | ||
| cargo kani 2>&1 | grep -m1 'E0659' | ||
| echo "[with flag]" | ||
| cargo kani --no-assert-overrides |
Contributor
There was a problem hiding this comment.
Wouldn't this produce false positives? This only checks that E0659 appears somewhere in output, not that the first run actually failed for the intended ambiguity. If output format shifts, or another E0659 appears, the test can pass for the wrong reason, right? Also, there’s no explicit exit-status assertion for the first command. So maybe we could:
- non-zero exit from
cargo kaniwithout the flag, and - output contains the specific ambiguity text (
assert is ambiguous/GlobVsOutermarker if stable). - Use
set -euo pipefailfor script reliability.
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
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.
Description
Adds a
--no-assert-overridesflag that skips injecting Kani's macro overrides (assert!,panic!, ...) into the crate under verification.Kani injects
#[macro_use] extern crate std as _kani_std_macros;so that its overrides shadow the prelude macros. rustc's restricted-shadowing rule makes a glob import of the same macro name ambiguous against the macro_use prelude — E0659 with kindGlobVsOuter, which is a hard error with no lint-level escape. Crates that glob-import a module re-exportingcore::asserttherefore cannot compile under Kani. #4666 already skips the injection for external dependencies, but the same pattern in the crate under verification still fails: verifying libc itself (whoseprelude!macro re-exportscore::assertinto an internal prelude that its modules glob-import) fails witherror[E0659]: `assert` is ambiguous(this is #1597 / the primary-crate remainder of #4665).With the flag, verification remains sound — assertion failures are still detected, just reported as generic panics without the original condition/message, matching how external and
no_stddependencies already behave since #4666. The flag is an escape hatch rather than a default change; the error-message-preserving behavior is untouched for everyone else.Found while evaluating
kani autoharnesson the top-100 crates.io crates, where libc 0.2.189 fails to build. With this flag (plus #4682 for itsno_std-ness), libc compiles cleanly under Kani.Testing
New script-based test
cargo_no_assert_overridesreproducing the libc pattern (macro-generated prelude re-exportingcore::assert, glob-imported by a module callingassert!): asserts E0659 without the flag, successful compilation with it, and that an intentionally failing assertion still fails verification (soundness of the degraded mode).kani-driverunit tests and formatting pass; manually verified libc 0.2.189 compiles undercargo kani --no-assert-overrides.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.