Set kani-compiler's required rustc flags unconditionally#4601
Set kani-compiler's required rustc flags unconditionally#4601lovesegfault 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
| "-Zmir-enable-passes=-RemoveStorageMarkers", | ||
| "--cfg=kani", | ||
| "--check-cfg=cfg(kani)", | ||
| ]; |
There was a problem hiding this comment.
Can we confirm that rustc accepts these in this single-token --flag=value form on this path?
The main guarantee of this PR depends on cfg(kani) definitely being enabled. If rustc expects these as separate argv tokens (--cfg, kani and --check-cfg, cfg(kani)), then we may not actually be enforcing the invariant we want here.
If that form is definitely accepted, a test that proves this exact encoding works would make me more confident. Otherwise, I think these should be passed as split tokens instead.
| # Minimal invocation. Deliberately omits every flag KANI_REQUIRED_RUSTC_ARGS | ||
| # now defaults: -Cpanic=abort, -Coverflow-checks=on, -Csymbol-mangling-version, | ||
| # -Zalways-encode-mir, -Zpanic_abort_tests, -Zmir-enable-passes, --cfg=kani, | ||
| # --check-cfg=cfg(kani). What remains is what every caller still has to pass: | ||
| # install paths, the routing marker, -Zunstable-options (gates `--extern | ||
| # noprelude:`), -Zcrate-attr (errors on duplicate so it stays caller-supplied), | ||
| # and the reachability intent. |
There was a problem hiding this comment.
Oh, nice regression test it proves the defaults are added for a minimal direct invocation.
One gap I still see is that the PR rationale depends on kani-compiler enforcing these values unconditionally, including when the caller passes conflicting values. This test currently exercises the “missing flags” case, but not the “conflicting flags” case.
Could we add a case that passes an explicit conflict (for example -Coverflow-checks=off) and verify Kani still behaves with the required value? That would directly test the intended “last-flag-wins” behavior this change relies on.
2 participants
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.