Set kani-compiler's required rustc flags unconditionally#4601
Open
lovesegfault wants to merge 2 commits into
Open
Set kani-compiler's required rustc flags unconditionally#4601lovesegfault wants to merge 2 commits into
lovesegfault wants to merge 2 commits into
Conversation
kani's MIR analysis and goto-c codegen require abort-on-panic, checked overflow, v0 mangling, encoded MIR, storage markers, and cfg(kani). These were previously passed as CLI flags by kani-driver via an internal, undocumented function. A caller that omitted one - a build system driving kani-compiler directly, or a contributor running RUSTC=kani-compiler cargo build to debug - previously got a verification result that was incorrect (silently, for --cfg=kani / -Coverflow-checks=on / -Zmir-enable-passes) or a hard error (for the rest). Now kani-compiler appends them itself. Appended after the caller's args so they're non-overridable (last-flag-wins for scalar -C/-Z options). -Clinker is deliberately excluded - a build system that needs a real linker for rlib output would have it clobbered. -Zcrate-attr is deliberately excluded - rustc errors on duplicate registration, and cargo kani already passes it; omitting it is a loud compile error, not silent unsoundness.
github-actions
Bot
added
Z-EndToEndBenchCI
Invokes kani-compiler directly with the minimal flag set (install paths,
--reachability, --kani-compiler, -Zunstable-options, -Zcrate-attr) and
asserts a #[cfg(kani)]-gated harness appears in the metadata. Without the
new defaults, --cfg=kani would be unset, the harness module would be
invisible, and the metadata would have 0 proof_harnesses - a vacuous
result with nothing verified.
Verified red-first: against a kani-compiler without the change, the same
invocation errors immediately ('Kani can only handle abort panic
strategy'); with the change, the harness compiles and appears.
lovesegfault
force-pushed
the
compiler-defaults
branch
from
e59f7a0 to
919d5b6
Compare
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
1 participant
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.
kani-compiler requires a specific set of rustc flags for its MIR analysis and goto-c codegen to be correct:
-Cpanic=abort,-Coverflow-checks=on,-Csymbol-mangling-version=v0,-Zalways-encode-mir,-Zpanic_abort_tests=yes,-Zmir-enable-passes=-RemoveStorageMarkers,--cfg=kani,--check-cfg=cfg(kani). Today they are derived inside kani-driver (base_rustc_flags()/kani_rustc_flags(), both private) and threaded through cargo's RUSTFLAGS. Anyone invokingkani-compileroutside that path — a build system that compiles withRUSTC=kani-compilerdirectly, or a contributor runningRUSTC=kani-compiler cargo buildto debug a codegen issue — has to re-derive the flag set from kani-driver source, and the failure modes range from a hard error (missing-Cpanic=abort, see #692) to a silently-wrong result. Missing--cfg=kaniis the worst case: any#[cfg(kani)]-gated harness module just doesn't compile and the metadata reports zero harnesses, a vacuous pass with nothing verified.Append the flags in
kani_compiler::run(), afteris_kani_compiler()has confirmed kani mode and stripped the marker arg. Forcargo kanithis is idempotent — scalar-C/-Zflags are last-flag-wins and--cfg/--check-cfgare additive. For any other caller the compiler now enforces the correct values regardless of what they passed.Deliberately not included:
-Clinker=echo(would clobber a real linker a build system needs for rlib output),-Zcrate-attr=feature(register_tool)/-Zcrate-attr=register_tool(kanitool)(rustc errors on a duplicate registration, andcargo kanialready passes them — appending would break everycargo kaniinvocation; omitting them is a loudunrecognized tool kanitool, not silent unsoundness), and the conditional and diagnostic-format flags that encode session intent.The
script-based-pretest invokeskani-compilerdirectly with only install paths,--kani-compiler,-Zcrate-attr, and a reachability flag — none of the eight defaults — and asserts the#[cfg(kani)]-gated harness still appears in the metadata. Verified by reverting the change and re-running: the same invocation then errors immediately on the missingpanic=abort.