Skip to content

Commit 5af25b5

Browse files
Strongly type differing compiler args for clarity (#4220)
### Context When working on #4211 & #4213, I was initially very confused by all the machinery in [`call_cargo.rs`](https://github.com/model-checking/kani/blob/main/kani-driver/src/call_cargo.rs) and [`call_single_file.rs`](https://github.com/model-checking/kani/blob/main/kani-driver/src/call_single_file.rs) that we used to pass arguments to the different layers of the compiler. The main source of my confusion was that there were many arguments all destined for different places (e.g. cargo, rustc, or kani-compiler) that all had to be encoded in differing ways (e.g. through the `--llvm-args` flag or the `CARGO_ENCODED_RUSTFLAGS` environment variable) but were mixed together sharing the same `String` type and similar-sounding variable names. Although misconfiguration would often be caught at runtime with a section of the compiler complaining about unexpected arguments, this confusion silently bit me a few times where argument names were shared. ### Fix This PR represents an attempt to encode the way arguments target different portions of the compiler into the type system using specific wrapper types for each kind of argument we use. You can convert transparently into these wrapper types, but then can only convert between them or pass them to a cargo command using the proper encoding methods. Although not perfect (you could still convert into the wrong kind of argument wrapper initially), this does seem to add some slight guardrails on the way we call cargo, especially against smaller changes to the existing patterns like the ones I was making in my PRs. It also may make the code easier to parse. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent 210b6c3 commit 5af25b5

File tree

5 files changed

+212
-75
lines changed

5 files changed

+212
-75
lines changed

kani-driver/src/args/cargo.rs

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@
33
//! Module that define parsers that mimic Cargo options.
44
55
use crate::args::ValidateArgs;
6+
use crate::util::args::CargoArg;
67
use clap::error::Error;
7-
use std::ffi::OsString;
88
use std::path::PathBuf;
99

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

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

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

127127
if self.bins {
128128
cargo_args.push("--bins".into());
@@ -168,7 +168,7 @@ pub struct CargoTestArgs {
168168

169169
impl CargoTestArgs {
170170
/// Convert the arguments back to a format that cargo can understand.
171-
pub fn to_cargo_args(&self) -> Vec<OsString> {
171+
pub fn to_cargo_args(&self) -> Vec<CargoArg> {
172172
let mut cargo_args = self.common.to_cargo_args();
173173
cargo_args.append(&mut self.target.to_cargo_args());
174174
cargo_args

kani-driver/src/call_cargo.rs

Lines changed: 23 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -2,13 +2,14 @@
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
use crate::args::VerificationArgs;
5-
use crate::call_single_file::{LibConfig, to_rustc_arg};
5+
use crate::call_single_file::LibConfig;
66
use crate::project::Artifact;
77
use crate::session::{
88
KaniSession, get_cargo_path, lib_folder, lib_no_core_folder, setup_cargo_command,
99
setup_cargo_command_inner,
1010
};
1111
use crate::util;
12+
use crate::util::args::{CargoArg, CommandWrapper as _, KaniArg, PassTo, encode_as_rustc_arg};
1213
use anyhow::{Context, Result, bail};
1314
use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel};
1415
use cargo_metadata::{
@@ -17,7 +18,6 @@ use cargo_metadata::{
1718
};
1819
use kani_metadata::{ArtifactType, CompilerArtifactStub};
1920
use std::collections::HashMap;
20-
use std::ffi::{OsStr, OsString};
2121
use std::fmt::{self, Display};
2222
use std::fs::{self, File};
2323
use std::io::IsTerminal;
@@ -77,13 +77,19 @@ crate-type = ["lib"]
7777
pub fn cargo_build_std(&self, std_path: &Path, krate_path: &Path) -> Result<Vec<Artifact>> {
7878
let lib_path = lib_no_core_folder().unwrap();
7979
let mut rustc_args = self.kani_rustc_flags(LibConfig::new_no_core(lib_path));
80-
rustc_args.push(to_rustc_arg(self.kani_compiler_local_flags()).into());
80+
81+
// In theory, these could be passed just to the local crate rather than all crates,
82+
// but the `cargo build` command we use for building `std` doesn't allow you to pass `rustc`
83+
// arguments, so we have to pass them through the environment variable instead.
84+
rustc_args.push(encode_as_rustc_arg(&self.kani_compiler_local_flags()));
85+
8186
// Ignore global assembly, since `compiler_builtins` has some.
82-
rustc_args.push(
83-
to_rustc_arg(vec!["--ignore-global-asm".to_string(), self.reachability_arg()]).into(),
84-
);
87+
rustc_args.push(encode_as_rustc_arg(&[
88+
KaniArg::from("--ignore-global-asm"),
89+
self.reachability_arg(),
90+
]));
8591

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

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

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

@@ -146,9 +150,9 @@ crate-type = ["lib"]
146150

147151
let lib_path = lib_folder().unwrap();
148152
let mut rustc_args = self.kani_rustc_flags(LibConfig::new(lib_path));
149-
rustc_args.push(to_rustc_arg(self.kani_compiler_dependency_flags()).into());
153+
rustc_args.push(encode_as_rustc_arg(&self.kani_compiler_dependency_flags()));
150154

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

204-
// Convert package args to rustc args for passing
205-
let pkg_args = vec!["--".into(), to_rustc_arg(kani_pkg_args)];
206-
207208
let mut found_target = false;
208209
let packages = self.packages_to_verify(&self.args, &metadata)?;
209210
let mut artifacts = vec![];
@@ -212,14 +213,13 @@ crate-type = ["lib"]
212213
for verification_target in package_targets(&self.args, package) {
213214
let mut cmd =
214215
setup_cargo_command_inner(Some(verification_target.target().name.clone()))?;
215-
cmd.args(&cargo_args)
216+
cmd.pass_cargo_args(&cargo_args)
216217
.args(vec!["-p", &package.id.to_string()])
217218
.args(verification_target.to_args())
218-
.args(&pkg_args)
219+
.arg("--") // Add this delimiter so we start passing args to rustc and not Cargo
219220
.env("RUSTC", &self.kani_compiler)
220-
// Use CARGO_ENCODED_RUSTFLAGS instead of RUSTFLAGS is preferred. See
221-
// https://doc.rust-lang.org/cargo/reference/environment-variables.html
222-
.env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join(OsStr::new("\x1f")))
221+
.pass_rustc_args(&rustc_args, PassTo::AllCrates)
222+
.pass_rustc_arg(encode_as_rustc_arg(&kani_pkg_args), PassTo::OnlyLocalCrate)
223223
// This is only required for stable but is a no-op for nightly channels
224224
.env("RUSTC_BOOTSTRAP", "1")
225225
.env("CARGO_TERM_PROGRESS_WHEN", "never");
@@ -472,7 +472,7 @@ crate-type = ["lib"]
472472
}
473473
}
474474

475-
pub fn cargo_config_args() -> Vec<OsString> {
475+
pub fn cargo_config_args() -> Vec<CargoArg> {
476476
[
477477
"--target",
478478
env!("TARGET"),
@@ -481,7 +481,7 @@ pub fn cargo_config_args() -> Vec<OsString> {
481481
"-Ztarget-applies-to-host",
482482
"--config=host.rustflags=[\"--cfg=kani_host\"]",
483483
]
484-
.map(OsString::from)
484+
.map(CargoArg::from)
485485
.to_vec()
486486
}
487487

kani-driver/src/call_single_file.rs

Lines changed: 25 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -3,14 +3,14 @@
33

44
use anyhow::Result;
55
use kani_metadata::UnstableFeature;
6-
use std::ffi::OsString;
76
use std::path::{Path, PathBuf};
87
use std::process::Command;
98

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

1212
pub struct LibConfig {
13-
args: Vec<OsString>,
13+
args: Vec<RustcArg>,
1414
}
1515

1616
impl LibConfig {
@@ -28,15 +28,15 @@ impl LibConfig {
2828
"--extern",
2929
kani_std_wrapper.as_str(),
3030
]
31-
.map(OsString::from)
31+
.map(RustcArg::from)
3232
.to_vec();
3333
LibConfig { args }
3434
}
3535

3636
pub fn new_no_core(path: PathBuf) -> LibConfig {
3737
LibConfig {
3838
args: ["-L", path.to_str().unwrap(), "--extern", "kani_core"]
39-
.map(OsString::from)
39+
.map(RustcArg::from)
4040
.to_vec(),
4141
}
4242
}
@@ -52,13 +52,13 @@ impl KaniSession {
5252
outdir: &Path,
5353
) -> Result<()> {
5454
let mut kani_args = self.kani_compiler_local_flags();
55-
kani_args.push(format!("--reachability={}", self.reachability_mode()));
55+
kani_args.push(format!("--reachability={}", self.reachability_mode()).into());
5656

5757
let lib_path = lib_folder().unwrap();
5858
let mut rustc_args = self.kani_rustc_flags(LibConfig::new(lib_path));
5959
rustc_args.push(file.into());
6060
rustc_args.push("--out-dir".into());
61-
rustc_args.push(OsString::from(outdir.as_os_str()));
61+
rustc_args.push(RustcArg::from(outdir.as_os_str()));
6262
rustc_args.push("--crate-name".into());
6363
rustc_args.push(crate_name.into());
6464

@@ -79,8 +79,9 @@ impl KaniSession {
7979
// Note that the order of arguments is important. Kani specific flags should precede
8080
// rustc ones.
8181
let mut cmd = Command::new(&self.kani_compiler);
82-
let kani_compiler_args = to_rustc_arg(kani_args);
83-
cmd.arg(kani_compiler_args).args(rustc_args);
82+
83+
cmd.pass_rustc_arg(encode_as_rustc_arg(&kani_args), PassTo::OnlyLocalCrate)
84+
.pass_rustc_args(&rustc_args, PassTo::OnlyLocalCrate);
8485

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

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

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

106107
if self.args.ignore_global_asm {
@@ -112,8 +113,8 @@ impl KaniSession {
112113

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

118119
if self.args.common_args.debug {
119120
flags.push("--log-level=debug".into());
@@ -163,29 +164,29 @@ impl KaniSession {
163164
}
164165

165166
for harness in &self.args.harnesses {
166-
flags.push(format!("--harness {harness}"));
167+
flags.push(format!("--harness {harness}").into());
167168
}
168169

169170
if self.args.exact {
170171
flags.push("--exact".into());
171172
}
172173

173174
if let Some(args) = self.autoharness_compiler_flags.clone() {
174-
flags.extend(args);
175+
flags.extend(args.into_iter().map(KaniArg::from));
175176
}
176177

177-
flags.extend(self.args.common_args.unstable_features.as_arguments().map(str::to_string));
178+
flags.extend(self.args.common_args.unstable_features.as_arguments().map(KaniArg::from));
178179

179180
flags
180181
}
181182

182183
/// This function generates all rustc configurations required by our goto-c codegen.
183-
pub fn kani_rustc_flags(&self, lib_config: LibConfig) -> Vec<OsString> {
184+
pub fn kani_rustc_flags(&self, lib_config: LibConfig) -> Vec<RustcArg> {
184185
let mut flags: Vec<_> = base_rustc_flags(lib_config);
185186
// We only use panic abort strategy for verification since we cannot handle unwind logic.
186187
if self.args.coverage {
187188
flags.extend_from_slice(
188-
&["-C", "instrument-coverage", "-Z", "no-profiler-runtime"].map(OsString::from),
189+
&["-C", "instrument-coverage", "-Z", "no-profiler-runtime"].map(RustcArg::from),
189190
);
190191
}
191192
flags.extend_from_slice(
@@ -202,7 +203,7 @@ impl KaniSession {
202203
// Do not invoke the linker since the compiler will not generate real object files
203204
"-Clinker=echo",
204205
]
205-
.map(OsString::from),
206+
.map(RustcArg::from),
206207
);
207208

208209
if self.args.no_codegen {
@@ -232,7 +233,7 @@ impl KaniSession {
232233
}
233234

234235
/// Common flags used for compiling user code for verification and playback flow.
235-
pub fn base_rustc_flags(lib_config: LibConfig) -> Vec<OsString> {
236+
pub fn base_rustc_flags(lib_config: LibConfig) -> Vec<RustcArg> {
236237
let mut flags = [
237238
"-C",
238239
"overflow-checks=on",
@@ -250,38 +251,24 @@ pub fn base_rustc_flags(lib_config: LibConfig) -> Vec<OsString> {
250251
"-Z",
251252
"crate-attr=register_tool(kanitool)",
252253
]
253-
.map(OsString::from)
254+
.map(RustcArg::from)
254255
.to_vec();
255256

256257
flags.extend(lib_config.args);
257258

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

264265
flags
265266
}
266267

267-
/// This function can be used to convert Kani compiler specific arguments into a rustc one.
268-
/// We currently pass Kani specific arguments using the `--llvm-args` structure which is the
269-
/// hacky mechanism used by other rustc backend to receive arguments unknown to rustc.
270-
///
271-
/// Note that Cargo caching mechanism takes the building context into consideration, which
272-
/// includes the value of the rust flags. By using `--llvm-args`, we ensure that Cargo takes into
273-
/// consideration all arguments that are used to configure Kani compiler. For example, enabling the
274-
/// reachability checks will force recompilation if they were disabled in previous build.
275-
/// For more details on this caching mechanism, see the
276-
/// [fingerprint documentation](https://github.com/rust-lang/cargo/blob/82c3bb79e3a19a5164e33819ef81bfc2c984bc56/src/cargo/core/compiler/fingerprint/mod.rs)
277-
pub fn to_rustc_arg(kani_args: Vec<String>) -> String {
278-
format!(r#"-Cllvm-args={}"#, kani_args.join(" "))
279-
}
280-
281268
/// Function that returns a `--check-version` argument to be added to the compiler flags.
282269
/// This is really just used to force the compiler to recompile everything from scratch when a user
283270
/// upgrades Kani. Cargo currently ignores the codegen backend version.
284271
/// See <https://github.com/model-checking/kani/issues/2140> for more context.
285-
fn check_version() -> String {
286-
format!("--check-version={}", env!("CARGO_PKG_VERSION"))
272+
fn check_version() -> KaniArg {
273+
format!("--check-version={}", env!("CARGO_PKG_VERSION")).into()
287274
}

0 commit comments

Comments
 (0)