Black arts of verifying libcore/libstd

[zjp-CN]

Command in kani's cargo_build_std

src: cargo_build_std

[kani-driver/src/call_cargo.rs:113:9] &cmd = Command {
    program: "cargo",
    args: [
        "cargo",
        "+nightly-2025-04-21-x86_64-unknown-linux-gnu",
        "build",
        "--target",
        "x86_64-unknown-linux-gnu",
        "-Zhost-config",
        "-Ztarget-applies-to-host",
        "--config=host.rustflags=[\"--cfg=kani_host\"]",
        "--message-format",
        "json-diagnostic-rendered-ansi",
        "-Z",
        "build-std=panic_abort,core,std",
    ],
    env: CommandEnv {
        clear: false,
        vars: {
            "CARGO_ENCODED_RUSTFLAGS": Some(
                "-C\u{1f}overflow-checks=on\u{1f}-Z\u{1f}unstable-options\u{1f}-Z\u{1f}trim-diagnostic-paths=no\u{1f}-Z\u{1f}human_readable_cg
u_names\u{1f}-Z\u{1f}always-encode-mir\u{1f}--cfg=kani\u{1f}-Z\u{1f}crate-attr=feature(register_tool)\u{1f}-Z\u{1f}crate-attr=register_tool(ka
nitool)\u{1f}-L\u{1f}/home/zjp/rust/distributed-verification/kani/target/kani/no_core/lib\u{1f}--extern\u{1f}kani_core\u{1f}-C\u{1f}panic=abor
t\u{1f}-C\u{1f}symbol-mangling-version=v0\u{1f}-Z\u{1f}panic_abort_tests=yes\u{1f}-Z\u{1f}mir-enable-passes=-RemoveStorageMarkers\u{1f}--check
-cfg=cfg(kani)\u{1f}-Clinker=echo\u{1f}--kani-compiler\u{1f}-Cllvm-args=--check-version=0.61.0 --log-level=warn --assertion-reach-checks --ena
ble-stubbing -Z list -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts\u{1f}-Cllvm-args=--reachability=harnesses
\u{1f}-Cllvm-args=--ignore-global-asm",
            ),
            "CARGO_TERM_PROGRESS_WHEN": Some(
                "never",
            ),
            "RUSTC": Some(
                "/home/zjp/rust/distributed-verification/kani/target/kani/bin/kani-compiler",
            ),
            "__CARGO_TESTS_ONLY_SRC_ROOT": Some(
                "/home/zjp/rust/verify-rust-std/library",
            ),
        },
    },
    cwd: Some(
        "/home/zjp/rust/verify-rust-std/target/kani_verify_std",
    ),
    create_pidfd: false,
}

Custom Rustc Driver

A cli that wraps argument handling and forwards them to the Rust compiler.

The driver directly calls rustc by only emitting rustc arguments, but can have its own arguments besides rustc ones.

Kani injects its own dependencies through rustc arguments:

distributed-verification/src/main.rs

Lines 39 to 52 in 3325e49

	"--cfg=kani",
	"-Zcrate-attr=feature(register_tool)",
	"-Zcrate-attr=register_tool(kanitool)",
	"--sysroot",
	&kani_path,
	"-L",
	&format!("{kani_path}/lib"),
	"--extern",
	"kani",
	"--extern",
	&format!("noprelude:std={kani_path}/lib/libstd.rlib"),
	"-Zunstable-options",
	"-Zalways-encode-mir",
	"-Zmir-enable-passes=-RemoveStorageMarkers",

Cargo Unstable Flags

• -Zbuild-std=core,std: compile the standard library itself as part of a crate graph compilation through Cargo
• -Zhost-config -Ztarget-applies-to-host: pass flags to host build targets such as build scripts
  • kani needs to pass #[cfg(kani_host)], so an extra config --config=host.rustflags=[\"--cfg=kani_host\"] is set; see kani#3244 and kani build process

Cargo Environment Variables

Doc: https://doc.rust-lang.org/cargo/reference/environment-variables.html#environment-variables-cargo-reads

• RUSTC=path/to/driver: the bridge between a driver and cargo to invoke the driver after invoking cargo
• CARGO_ENCODED_RUSTFLAGS: an OsString with arguments separated by 0x1f
• CARGO_TERM_PROGRESS_WHEN=never: don't show progress bar

Cargo Internals

The undocumented stuff that are only known among cargo developers.

• __CARGO_TESTS_ONLY_SRC_ROOT=path/to/verify-rust-std/library: a path to rustc's library folder
  • in distributed-verification tool, call stable_mir::find_crates("core") to get Crate of libcore and filter in FnDefs annotated with kanitool

Json Messages

https://doc.rust-lang.org/cargo/reference/external-tools.html

--message-format and cargo_metadata::Message::parse_stream

[zjp-CN]

Thus distributed-verfication has a similar wrapper based on these tricks to reuse kani's libcore and libstd and know kani contracts in core/std.