From 72ec02b63a8f7225e92d04dfa12647b1c95b6e4c Mon Sep 17 00:00:00 2001 From: Bernardo Meurer Date: Wed, 20 May 2026 09:11:48 -0400 Subject: [PATCH 1/2] Set kani-compiler's required rustc flags unconditionally 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. --- kani-compiler/src/kani_compiler.rs | 85 +++++++++++++++++++++++++++++- 1 file changed, 84 insertions(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 3f2b3d0c772..dfe13e9c82f 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -32,9 +32,52 @@ use rustc_public::rustc_internal; use rustc_session::config::ErrorOutputType; use tracing::debug; +/// rustc flags kani-compiler requires for correct verification semantics, set +/// unconditionally on every kani-mode invocation. kani's MIR analysis and +/// goto-c codegen assume abort-on-panic, checked overflow, v0 mangling, +/// encoded MIR, storage markers, and `cfg(kani)`. `cargo kani` already passes +/// these (`kani_rustc_flags()` in kani-driver); for that path appending is +/// idempotent — scalar `-C`/`-Z` flags are last-flag-wins and `--cfg`/ +/// `--check-cfg` are additive. For any other caller — a build system that +/// drives kani-compiler directly, or a contributor running +/// `RUSTC=kani-compiler cargo build` to debug — omitting one of these flags +/// previously produced an incorrect or failed verification: missing +/// `--cfg=kani` is a vacuous 0-harness pass, missing `-Coverflow-checks=on` +/// or `-Zmir-enable-passes` proves a different program (silent), and the +/// rest are hard errors. Now the compiler enforces the correct values. +/// +/// Appended (not prepended): rustc is last-flag-wins for scalar `-C`/`-Z` +/// options, so appending after the caller's args makes these non-overridable. +/// +/// Deliberately NOT included: +/// - `-Clinker=echo` — would clobber a real linker a build system provides +/// for rlib output (last-flag-wins). +/// - `-Zcrate-attr=feature(register_tool)` / `-Zcrate-attr=register_tool(kanitool)` +/// — `-Zcrate-attr` ERRORS on a duplicate registration. `cargo kani` already +/// passes these via `base_rustc_flags()`; appending again would break every +/// `cargo kani` invocation (`error: tool 'kanitool' was already registered`). +/// Omitting them is a loud compile error (`unrecognized tool kanitool`), not +/// silent unsoundness — caller responsibility is acceptable here. +/// - Conditional flags (`-Cinstrument-coverage`, `-Zno-codegen`, +/// `-Cdebug-assertions=off`, `-Zrandomize-layout`) — encode session intent; +/// the caller chooses them. +/// - Diagnostic-format flags (`-Ztrim-diagnostic-paths`, `-Zhuman_readable_cgu_names`, +/// `-Zunstable-options`) — caller preferences, not invariants. +const KANI_REQUIRED_RUSTC_ARGS: &[&str] = &[ + "-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)", +]; + /// Run the Kani flavour of the compiler. /// This may require multiple runs of the rustc driver ([`rustc_driver::run_compiler`]). -pub fn run(args: Vec) { +pub fn run(mut args: Vec) { + args.extend(KANI_REQUIRED_RUSTC_ARGS.iter().map(|s| s.to_string())); let mut kani_compiler = KaniCompiler::new(); kani_compiler.run(args); } @@ -134,3 +177,43 @@ impl Callbacks for KaniCompiler { Compilation::Continue } } + +#[cfg(test)] +mod tests { + use super::KANI_REQUIRED_RUSTC_ARGS; + + /// The required-flags list must never include a linker override — a build + /// system that needs a real linker for rlib output would have it silently + /// clobbered (last-flag-wins). + #[test] + fn required_args_do_not_clobber_linker() { + assert!( + !KANI_REQUIRED_RUSTC_ARGS.iter().any(|f| f.starts_with("-Clinker")), + "KANI_REQUIRED_RUSTC_ARGS must not set -Clinker (build systems own that)" + ); + } + + /// The soundness invariants kani's MIR analysis assumes. + #[test] + fn required_args_cover_soundness_invariants() { + for must_have in + ["-Cpanic=abort", "-Coverflow-checks=on", "-Zalways-encode-mir", "--cfg=kani"] + { + assert!( + KANI_REQUIRED_RUSTC_ARGS.contains(&must_have), + "missing soundness-critical flag: {must_have}" + ); + } + } + + /// `-Zcrate-attr` errors on duplicate registration. `cargo kani` already + /// passes `-Z crate-attr=...`; including it here would break every + /// `cargo kani` invocation with `error: tool 'kanitool' was already registered`. + #[test] + fn required_args_do_not_duplicate_crate_attr() { + assert!( + !KANI_REQUIRED_RUSTC_ARGS.iter().any(|f| f.contains("crate-attr")), + "KANI_REQUIRED_RUSTC_ARGS must not include -Zcrate-attr (cargo kani passes it; rustc errors on duplicate)" + ); + } +} From 919d5b686333b1da32bebbe7d8716dfc519899ef Mon Sep 17 00:00:00 2001 From: Bernardo Meurer Date: Wed, 20 May 2026 09:11:56 -0400 Subject: [PATCH 2/2] Add integration test for kani-compiler default rustc flags 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. --- .../compiler_defaults.expected | 2 + .../compiler_defaults/compiler_defaults.sh | 67 +++++++++++++++++++ .../compiler_defaults/config.yml | 5 ++ .../compiler_defaults/fixture.rs | 16 +++++ 4 files changed, 90 insertions(+) create mode 100644 tests/script-based-pre/compiler_defaults/compiler_defaults.expected create mode 100755 tests/script-based-pre/compiler_defaults/compiler_defaults.sh create mode 100644 tests/script-based-pre/compiler_defaults/config.yml create mode 100644 tests/script-based-pre/compiler_defaults/fixture.rs diff --git a/tests/script-based-pre/compiler_defaults/compiler_defaults.expected b/tests/script-based-pre/compiler_defaults/compiler_defaults.expected new file mode 100644 index 00000000000..2fe43817379 --- /dev/null +++ b/tests/script-based-pre/compiler_defaults/compiler_defaults.expected @@ -0,0 +1,2 @@ +[TEST] kani-compiler exited 0 +[TEST] proof_harnesses: 1 diff --git a/tests/script-based-pre/compiler_defaults/compiler_defaults.sh b/tests/script-based-pre/compiler_defaults/compiler_defaults.sh new file mode 100755 index 00000000000..7626106ac09 --- /dev/null +++ b/tests/script-based-pre/compiler_defaults/compiler_defaults.sh @@ -0,0 +1,67 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# Test that kani-compiler sets its required rustc flags unconditionally. +# +# Invoke kani-compiler directly with the MINIMAL flag set — install paths, +# the routing marker (--kani-compiler), the kanitool namespace registration +# (-Zcrate-attr — NOT a default because it errors on duplicate registration), +# and an intent flag (--reachability) — and assert a #[cfg(kani)]-gated +# harness appears in the metadata. Without the defaults, --cfg=kani would be +# unset, the harness module would be invisible, and the metadata would have +# 0 proof_harnesses: a vacuous "verification" with nothing verified. + +set -eu + +OUTDIR="tmp_compiler_defaults" +rm -rf "${OUTDIR}" +mkdir "${OUTDIR}" + +# Locate kani-compiler and the kani sysroot in the dev build: `cargo build-dev` +# populates target/kani/ (KANI_SYSROOT in .cargo/config.toml) with bin/ and +# lib/, mirroring the release install layout. Same pattern as +# std_codegen/codegen_std.sh. KANI_HOME is what `kani` itself passes as +# --sysroot: LibConfig::new() uses the parent of the lib/ folder. +KANI_DIR=$(git rev-parse --show-toplevel) +KANI_HOME="${KANI_DIR}/target/kani" +KANI_COMPILER="${KANI_HOME}/bin/kani-compiler" +KANI_LIB="${KANI_HOME}/lib" + +[[ -x "${KANI_COMPILER}" ]] || { + echo "ERROR: kani-compiler not found at ${KANI_COMPILER}" + echo "Run 'cargo build-dev' first." + exit 1 +} + +# 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. +"${KANI_COMPILER}" \ + --kani-compiler \ + --crate-type lib \ + --crate-name fixture \ + --out-dir "${OUTDIR}" \ + --sysroot "${KANI_HOME}" \ + -L "${KANI_LIB}" \ + -Z unstable-options \ + --extern kani \ + --extern noprelude:std="${KANI_LIB}/libstd.rlib" \ + -Z crate-attr="feature(register_tool)" \ + -Z crate-attr="register_tool(kanitool)" \ + -Cllvm-args=--reachability=harnesses \ + fixture.rs + +echo "[TEST] kani-compiler exited 0" + +# The metadata must list the #[cfg(kani)]-gated harness — proves --cfg=kani +# was set internally. +META=$(ls "${OUTDIR}"/*.kani-metadata.json) +HARNESSES=$(jq '.proof_harnesses | length' "${META}") +echo "[TEST] proof_harnesses: ${HARNESSES}" + +rm -rf "${OUTDIR}" diff --git a/tests/script-based-pre/compiler_defaults/config.yml b/tests/script-based-pre/compiler_defaults/config.yml new file mode 100644 index 00000000000..4ab0c253ea3 --- /dev/null +++ b/tests/script-based-pre/compiler_defaults/config.yml @@ -0,0 +1,5 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: compiler_defaults.sh +expected: compiler_defaults.expected +exit_code: 0 diff --git a/tests/script-based-pre/compiler_defaults/fixture.rs b/tests/script-based-pre/compiler_defaults/fixture.rs new file mode 100644 index 00000000000..d1f4b8e698b --- /dev/null +++ b/tests/script-based-pre/compiler_defaults/fixture.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! A `#[cfg(kani)]`-gated harness. If kani-compiler sets `--cfg=kani` as a +//! default, the harness compiles; if not, the module is invisible and 0 +//! harnesses appear in the metadata — a vacuous "verification" with nothing +//! verified. + +#[cfg(kani)] +mod verify { + #[kani::proof] + fn check_with_defaults() { + let x: u8 = kani::any(); + assert_eq!(x.wrapping_mul(1), x); + } +}