Set kani-compiler's required rustc flags unconditionally#4601
Set kani-compiler's required rustc flags unconditionally#4601lovesegfault wants to merge 4 commits into
Conversation
github-actions
Bot
added
Z-EndToEndBenchCI
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.
There was a problem hiding this comment.
ah, nice catch, i added coverage for this in the compiler_defaults test. the fixture now carries a deliberately undeclared cfg as a negative control :)
FWIW this is the same encoding kani-driver has always passed (base_rustc_flags()), and rustc's getopts CLI treats --flag=value and --flag value identically
| # 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.
There was a problem hiding this comment.
i added the conflict case, a second invocation now passes -Cpanic=unwind -Coverflow-checks=off -Csymbol-mangling-version=legacy and must behave identically to the minimal one :)
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.
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.
The compiler_defaults test showed --cfg=kani takes effect (the gated harness appears in the metadata) but only showed --check-cfg=cfg(kani) is accepted: if rustc silently dropped the flag, the test still passed. Add a deliberately undeclared cfg to the fixture as a negative control. Its unexpected_cfgs warning proves cfg checking is active — rustc only checks cfg names when at least one --check-cfg argument is present, and the test passes none besides kani-compiler's default — and #[cfg(kani)] drawing no warning proves `kani` is the name the single-token `--flag=value` encoding registered. No-Verification-Needed: test-only plus doc-comment changes
919d5b6 to
0187f43
Compare
The compiler_defaults test proved the required flags are supplied when the caller omits them, but not that they win when the caller passes conflicting values - the non-overridability the defaults exist for. Add a second case passing -Cpanic=unwind, -Coverflow-checks=off, and -Csymbol-mangling-version=legacy that must behave identically to the minimal case. Each winner is observable without running CBMC: kani-compiler's own session gates hard-error when the panic strategy is not abort or overflow checks are off, so the conflict case exiting 0 proves both resolved to the required values; a #[cfg(panic = "abort")]-gated harness backstops the metadata count should those gates ever move; and every harness mangled_name must carry v0's _R prefix, which a winning legacy conflict would flip. Both cases now run through a shared run_case helper, and the metadata checks guard against a missing/duplicated metadata file and an empty harness list instead of passing vacuously. No-Verification-Needed: test-only change
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.