Skip to content

Strongly type differing compiler args for clarity #4220

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 6 commits into from
Jul 22, 2025
Merged

Strongly type differing compiler args for clarity #4220

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
69d5258
create separate arg types for clarity
AlexanderPortland Jul 10, 2025
5a978e1
minor feedback addressed
AlexanderPortland Jul 18, 2025
366e33f
fix overwriting of env vars w/ `PassTo::AllCrates`
AlexanderPortland Jul 21, 2025
20e59b1
add module-level documentation
AlexanderPortland Jul 21, 2025
33409fb
make `to_rustc_arg` more generic & rename
AlexanderPortland Jul 21, 2025
ebe349e
Merge remote-tracking branch 'origin/main' into typed-args
AlexanderPortland Jul 22, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions kani-driver/src/args/cargo.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@
//! Module that define parsers that mimic Cargo options.

use crate::args::ValidateArgs;
use crate::util::args::CargoArg;
use clap::error::Error;
use std::ffi::OsString;
use std::path::PathBuf;

/// Arguments that Kani pass down into Cargo essentially uninterpreted.
Expand Down Expand Up @@ -61,8 +61,8 @@ impl CargoCommonArgs {

/// Convert the arguments back to a format that cargo can understand.
/// Note that the `exclude` option requires special processing and it's not included here.
pub fn to_cargo_args(&self) -> Vec<OsString> {
let mut cargo_args: Vec<OsString> = vec![];
pub fn to_cargo_args(&self) -> Vec<CargoArg> {
let mut cargo_args: Vec<CargoArg> = vec![];
if self.all_features {
cargo_args.push("--all-features".into());
}
Expand Down Expand Up @@ -117,12 +117,12 @@ pub struct CargoTargetArgs {

impl CargoTargetArgs {
/// Convert the arguments back to a format that cargo can understand.
pub fn to_cargo_args(&self) -> Vec<OsString> {
pub fn to_cargo_args(&self) -> Vec<CargoArg> {
let mut cargo_args = self
.bin
.iter()
.map(|binary| format!("--bin={binary}").into())
.collect::<Vec<OsString>>();
.collect::<Vec<CargoArg>>();

if self.bins {
cargo_args.push("--bins".into());
Expand Down Expand Up @@ -168,7 +168,7 @@ pub struct CargoTestArgs {

impl CargoTestArgs {
/// Convert the arguments back to a format that cargo can understand.
pub fn to_cargo_args(&self) -> Vec<OsString> {
pub fn to_cargo_args(&self) -> Vec<CargoArg> {
let mut cargo_args = self.common.to_cargo_args();
cargo_args.append(&mut self.target.to_cargo_args());
cargo_args
Expand Down
46 changes: 23 additions & 23 deletions kani-driver/src/call_cargo.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,13 +2,14 @@
// SPDX-License-Identifier: Apache-2.0 OR MIT

use crate::args::VerificationArgs;
use crate::call_single_file::{LibConfig, to_rustc_arg};
use crate::call_single_file::LibConfig;
use crate::project::Artifact;
use crate::session::{
KaniSession, get_cargo_path, lib_folder, lib_no_core_folder, setup_cargo_command,
setup_cargo_command_inner,
};
use crate::util;
use crate::util::args::{CargoArg, CommandWrapper as _, KaniArg, PassTo, encode_as_rustc_arg};
use anyhow::{Context, Result, bail};
use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel};
use cargo_metadata::{
Expand All @@ -17,7 +18,6 @@ use cargo_metadata::{
};
use kani_metadata::{ArtifactType, CompilerArtifactStub};
use std::collections::HashMap;
use std::ffi::{OsStr, OsString};
use std::fmt::{self, Display};
use std::fs::{self, File};
use std::io::IsTerminal;
Expand Down Expand Up @@ -77,13 +77,19 @@ crate-type = ["lib"]
pub fn cargo_build_std(&self, std_path: &Path, krate_path: &Path) -> Result<Vec<Artifact>> {
let lib_path = lib_no_core_folder().unwrap();
let mut rustc_args = self.kani_rustc_flags(LibConfig::new_no_core(lib_path));
rustc_args.push(to_rustc_arg(self.kani_compiler_local_flags()).into());

// In theory, these could be passed just to the local crate rather than all crates,
// but the `cargo build` command we use for building `std` doesn't allow you to pass `rustc`
// arguments, so we have to pass them through the environment variable instead.
rustc_args.push(encode_as_rustc_arg(&self.kani_compiler_local_flags()));

// Ignore global assembly, since `compiler_builtins` has some.
rustc_args.push(
to_rustc_arg(vec!["--ignore-global-asm".to_string(), self.reachability_arg()]).into(),
);
rustc_args.push(encode_as_rustc_arg(&[
KaniArg::from("--ignore-global-asm"),
self.reachability_arg(),
]));

let mut cargo_args: Vec<OsString> = vec!["build".into()];
let mut cargo_args: Vec<CargoArg> = vec!["build".into()];
cargo_args.append(&mut cargo_config_args());

// Configuration needed to parse cargo compilation status.
Expand All @@ -103,12 +109,10 @@ crate-type = ["lib"]

// Since we are verifying the standard library, we set the reachability to all crates.
let mut cmd = setup_cargo_command()?;
cmd.args(&cargo_args)
cmd.pass_cargo_args(&cargo_args)
.current_dir(krate_path)
.env("RUSTC", &self.kani_compiler)
// Use CARGO_ENCODED_RUSTFLAGS instead of RUSTFLAGS is preferred. See
// https://doc.rust-lang.org/cargo/reference/environment-variables.html
.env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join(OsStr::new("\x1f")))
.pass_rustc_args(&rustc_args, PassTo::AllCrates)
.env("CARGO_TERM_PROGRESS_WHEN", "never")
.env("__CARGO_TESTS_ONLY_SRC_ROOT", full_path.as_os_str());

Expand Down Expand Up @@ -146,9 +150,9 @@ crate-type = ["lib"]

let lib_path = lib_folder().unwrap();
let mut rustc_args = self.kani_rustc_flags(LibConfig::new(lib_path));
rustc_args.push(to_rustc_arg(self.kani_compiler_dependency_flags()).into());
rustc_args.push(encode_as_rustc_arg(&self.kani_compiler_dependency_flags()));

let mut cargo_args: Vec<OsString> = vec!["rustc".into()];
let mut cargo_args: Vec<CargoArg> = vec!["rustc".into()];
if let Some(path) = &self.args.cargo.manifest_path {
cargo_args.push("--manifest-path".into());
cargo_args.push(path.into());
Expand Down Expand Up @@ -201,9 +205,6 @@ crate-type = ["lib"]
let mut kani_pkg_args = vec![self.reachability_arg()];
kani_pkg_args.extend(self.kani_compiler_local_flags());

// Convert package args to rustc args for passing
let pkg_args = vec!["--".into(), to_rustc_arg(kani_pkg_args)];

let mut found_target = false;
let packages = self.packages_to_verify(&self.args, &metadata)?;
let mut artifacts = vec![];
Expand All @@ -212,14 +213,13 @@ crate-type = ["lib"]
for verification_target in package_targets(&self.args, package) {
let mut cmd =
setup_cargo_command_inner(Some(verification_target.target().name.clone()))?;
cmd.args(&cargo_args)
cmd.pass_cargo_args(&cargo_args)
.args(vec!["-p", &package.id.to_string()])
.args(verification_target.to_args())
.args(&pkg_args)
.arg("--") // Add this delimiter so we start passing args to rustc and not Cargo
.env("RUSTC", &self.kani_compiler)
// Use CARGO_ENCODED_RUSTFLAGS instead of RUSTFLAGS is preferred. See
// https://doc.rust-lang.org/cargo/reference/environment-variables.html
.env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join(OsStr::new("\x1f")))
.pass_rustc_args(&rustc_args, PassTo::AllCrates)
.pass_rustc_arg(encode_as_rustc_arg(&kani_pkg_args), PassTo::OnlyLocalCrate)
// This is only required for stable but is a no-op for nightly channels
.env("RUSTC_BOOTSTRAP", "1")
.env("CARGO_TERM_PROGRESS_WHEN", "never");
Expand Down Expand Up @@ -473,7 +473,7 @@ crate-type = ["lib"]
}
}

pub fn cargo_config_args() -> Vec<OsString> {
pub fn cargo_config_args() -> Vec<CargoArg> {
[
"--target",
env!("TARGET"),
Expand All @@ -482,7 +482,7 @@ pub fn cargo_config_args() -> Vec<OsString> {
"-Ztarget-applies-to-host",
"--config=host.rustflags=[\"--cfg=kani_host\"]",
]
.map(OsString::from)
.map(CargoArg::from)
.to_vec()
}

Expand Down
61 changes: 24 additions & 37 deletions kani-driver/src/call_single_file.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,14 +3,14 @@

use anyhow::Result;
use kani_metadata::UnstableFeature;
use std::ffi::OsString;
use std::path::{Path, PathBuf};
use std::process::Command;

use crate::session::{KaniSession, lib_folder};
use crate::util::args::{CommandWrapper, KaniArg, PassTo, RustcArg, encode_as_rustc_arg};

pub struct LibConfig {
args: Vec<OsString>,
args: Vec<RustcArg>,
}

impl LibConfig {
Expand All @@ -28,15 +28,15 @@ impl LibConfig {
"--extern",
kani_std_wrapper.as_str(),
]
.map(OsString::from)
.map(RustcArg::from)
.to_vec();
LibConfig { args }
}

pub fn new_no_core(path: PathBuf) -> LibConfig {
LibConfig {
args: ["-L", path.to_str().unwrap(), "--extern", "kani_core"]
.map(OsString::from)
.map(RustcArg::from)
.to_vec(),
}
}
Expand All @@ -52,13 +52,13 @@ impl KaniSession {
outdir: &Path,
) -> Result<()> {
let mut kani_args = self.kani_compiler_local_flags();
kani_args.push(format!("--reachability={}", self.reachability_mode()));
kani_args.push(format!("--reachability={}", self.reachability_mode()).into());

let lib_path = lib_folder().unwrap();
let mut rustc_args = self.kani_rustc_flags(LibConfig::new(lib_path));
rustc_args.push(file.into());
rustc_args.push("--out-dir".into());
rustc_args.push(OsString::from(outdir.as_os_str()));
rustc_args.push(RustcArg::from(outdir.as_os_str()));
rustc_args.push("--crate-name".into());
rustc_args.push(crate_name.into());

Expand All @@ -79,8 +79,9 @@ impl KaniSession {
// Note that the order of arguments is important. Kani specific flags should precede
// rustc ones.
let mut cmd = Command::new(&self.kani_compiler);
let kani_compiler_args = to_rustc_arg(kani_args);
cmd.arg(kani_compiler_args).args(rustc_args);

cmd.pass_rustc_arg(encode_as_rustc_arg(&kani_args), PassTo::OnlyLocalCrate)
.pass_rustc_args(&rustc_args, PassTo::OnlyLocalCrate);

// This is only required for stable but is a no-op for nightly channels
cmd.env("RUSTC_BOOTSTRAP", "1");
Expand All @@ -94,13 +95,13 @@ impl KaniSession {
}

/// Create a compiler option that represents the reachability mode.
pub fn reachability_arg(&self) -> String {
format!("--reachability={}", self.reachability_mode())
pub fn reachability_arg(&self) -> KaniArg {
format!("--reachability={}", self.reachability_mode()).into()
}

/// The `kani-compiler`-specific arguments that should be passed when building all crates,
/// including dependencies.
pub fn kani_compiler_dependency_flags(&self) -> Vec<String> {
pub fn kani_compiler_dependency_flags(&self) -> Vec<KaniArg> {
let mut flags = vec![check_version()];

if self.args.ignore_global_asm {
Expand All @@ -112,8 +113,8 @@ impl KaniSession {

/// The `kani-compiler`-specific arguments that should be passed only to the local crate
/// being compiled.
pub fn kani_compiler_local_flags(&self) -> Vec<String> {
let mut flags = vec![];
pub fn kani_compiler_local_flags(&self) -> Vec<KaniArg> {
let mut flags: Vec<KaniArg> = vec![];

if self.args.common_args.debug {
flags.push("--log-level=debug".into());
Expand Down Expand Up @@ -163,21 +164,21 @@ impl KaniSession {
}

if let Some(args) = self.autoharness_compiler_flags.clone() {
flags.extend(args);
flags.extend(args.into_iter().map(KaniArg::from));
}

flags.extend(self.args.common_args.unstable_features.as_arguments().map(str::to_string));
flags.extend(self.args.common_args.unstable_features.as_arguments().map(KaniArg::from));

flags
}

/// This function generates all rustc configurations required by our goto-c codegen.
pub fn kani_rustc_flags(&self, lib_config: LibConfig) -> Vec<OsString> {
pub fn kani_rustc_flags(&self, lib_config: LibConfig) -> Vec<RustcArg> {
let mut flags: Vec<_> = base_rustc_flags(lib_config);
// We only use panic abort strategy for verification since we cannot handle unwind logic.
if self.args.coverage {
flags.extend_from_slice(
&["-C", "instrument-coverage", "-Z", "no-profiler-runtime"].map(OsString::from),
&["-C", "instrument-coverage", "-Z", "no-profiler-runtime"].map(RustcArg::from),
);
}
flags.extend_from_slice(
Expand All @@ -194,7 +195,7 @@ impl KaniSession {
// Do not invoke the linker since the compiler will not generate real object files
"-Clinker=echo",
]
.map(OsString::from),
.map(RustcArg::from),
);

if self.args.no_codegen {
Expand Down Expand Up @@ -224,7 +225,7 @@ impl KaniSession {
}

/// Common flags used for compiling user code for verification and playback flow.
pub fn base_rustc_flags(lib_config: LibConfig) -> Vec<OsString> {
pub fn base_rustc_flags(lib_config: LibConfig) -> Vec<RustcArg> {
let mut flags = [
"-C",
"overflow-checks=on",
Expand All @@ -242,38 +243,24 @@ pub fn base_rustc_flags(lib_config: LibConfig) -> Vec<OsString> {
"-Z",
"crate-attr=register_tool(kanitool)",
]
.map(OsString::from)
.map(RustcArg::from)
.to_vec();

flags.extend(lib_config.args);

// e.g. compiletest will set 'compile-flags' here and we should pass those down to rustc
// and we fail in `tests/kani/Match/match_bool.rs`
if let Ok(str) = std::env::var("RUSTFLAGS") {
flags.extend(str.split(' ').map(OsString::from));
flags.extend(str.split(' ').map(RustcArg::from));
}

flags
}

/// This function can be used to convert Kani compiler specific arguments into a rustc one.
/// We currently pass Kani specific arguments using the `--llvm-args` structure which is the
/// hacky mechanism used by other rustc backend to receive arguments unknown to rustc.
///
/// Note that Cargo caching mechanism takes the building context into consideration, which
/// includes the value of the rust flags. By using `--llvm-args`, we ensure that Cargo takes into
/// consideration all arguments that are used to configure Kani compiler. For example, enabling the
/// reachability checks will force recompilation if they were disabled in previous build.
/// For more details on this caching mechanism, see the
/// [fingerprint documentation](https://github.com/rust-lang/cargo/blob/82c3bb79e3a19a5164e33819ef81bfc2c984bc56/src/cargo/core/compiler/fingerprint/mod.rs)
pub fn to_rustc_arg(kani_args: Vec<String>) -> String {
format!(r#"-Cllvm-args={}"#, kani_args.join(" "))
}

/// Function that returns a `--check-version` argument to be added to the compiler flags.
/// This is really just used to force the compiler to recompile everything from scratch when a user
/// upgrades Kani. Cargo currently ignores the codegen backend version.
/// See <https://github.com/model-checking/kani/issues/2140> for more context.
fn check_version() -> String {
format!("--check-version={}", env!("CARGO_PKG_VERSION"))
fn check_version() -> KaniArg {
format!("--check-version={}", env!("CARGO_PKG_VERSION")).into()
}
14 changes: 6 additions & 8 deletions kani-driver/src/concrete_playback/playback.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,9 +8,9 @@ use crate::args::playback_args::{CargoPlaybackArgs, KaniPlaybackArgs, MessageFor
use crate::call_cargo::cargo_config_args;
use crate::call_single_file::{LibConfig, base_rustc_flags};
use crate::session::{InstallType, lib_playback_folder, setup_cargo_command};
use crate::util::args::{CargoArg, CommandWrapper, PassTo, RustcArg};
use crate::{session, util};
use anyhow::Result;
use std::ffi::OsString;
use std::ops::Deref;
use std::path::{Path, PathBuf};
use std::process::Command;
Expand Down Expand Up @@ -72,7 +72,7 @@ fn build_test(install: &InstallType, args: &KaniPlaybackArgs) -> Result<PathBuf>

let mut rustc_args = base_rustc_flags(LibConfig::new(lib_playback_folder()?));
rustc_args.push("--test".into());
rustc_args.push(OsString::from(&args.input));
rustc_args.push(RustcArg::from(&args.input));
rustc_args.push(format!("--crate-name={TEST_BIN_NAME}").into());

if args.playback.common_opts.verbose() {
Expand All @@ -84,7 +84,7 @@ fn build_test(install: &InstallType, args: &KaniPlaybackArgs) -> Result<PathBuf>
}

let mut cmd = Command::new(install.kani_compiler()?);
cmd.args(rustc_args);
cmd.pass_rustc_args(&rustc_args, PassTo::OnlyLocalCrate);

session::run_terminal(&args.playback.common_opts, cmd)?;

Expand All @@ -97,7 +97,7 @@ fn cargo_test(args: CargoPlaybackArgs) -> Result<()> {
let mut cmd = setup_cargo_command()?;

let rustc_args = base_rustc_flags(LibConfig::new(lib_playback_folder()?));
let mut cargo_args: Vec<OsString> = vec!["test".into()];
let mut cargo_args: Vec<CargoArg> = vec!["test".into()];

if args.playback.common_opts.verbose() {
cargo_args.push("-vv".into());
Expand All @@ -123,11 +123,9 @@ fn cargo_test(args: CargoPlaybackArgs) -> Result<()> {
}

// Arguments that will only be passed to the target package.
cmd.args(&cargo_args)
cmd.pass_cargo_args(&cargo_args)
.env("RUSTC", &install.kani_compiler()?)
// Use CARGO_ENCODED_RUSTFLAGS instead of RUSTFLAGS is preferred. See
// https://doc.rust-lang.org/cargo/reference/environment-variables.html
.env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join(&OsString::from("\x1f")))
.pass_rustc_args(&rustc_args, PassTo::AllCrates)
.env("CARGO_TERM_PROGRESS_WHEN", "never");

session::run_terminal(&args.playback.common_opts, cmd)?;
Expand Down
Loading
Loading