Set kani-compiler's required rustc flags unconditionally

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<String>) {
+pub fn run(mut args: Vec<String>) {
+    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)"
+        );
+    }
+}

tests/script-based-pre/compiler_defaults/compiler_defaults.expected

@@ -0,0 +1,2 @@
+[TEST] kani-compiler exited 0
+[TEST] proof_harnesses: 1

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}"

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

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);
+    }
+}