|
| 1 | +// Copyright Kani Contributors |
| 2 | +// SPDX-License-Identifier: Apache-2.0 OR MIT |
| 3 | +//! Module that define parsers that mimic Cargo options. |
| 4 | +
|
| 5 | +use crate::args::ValidateArgs; |
| 6 | +use clap::error::Error; |
| 7 | +use std::ffi::OsString; |
| 8 | +use std::path::PathBuf; |
| 9 | + |
| 10 | +/// Arguments that Kani pass down into Cargo essentially uninterpreted. |
| 11 | +/// These generally have to do with selection of packages or activation of features. |
| 12 | +/// These do not (currently) include cargo args that kani pays special attention to: |
| 13 | +/// for instance, we keep `--tests` and `--target-dir` elsewhere. |
| 14 | +#[derive(Debug, Default, clap::Args)] |
| 15 | +pub struct CargoCommonArgs { |
| 16 | + /// Activate all package features |
| 17 | + #[arg(long)] |
| 18 | + pub all_features: bool, |
| 19 | + /// Do not activate the `default` feature |
| 20 | + #[arg(long)] |
| 21 | + pub no_default_features: bool, |
| 22 | + |
| 23 | + // This tolerates spaces too, but we say "comma" only because this is the least error-prone approach... |
| 24 | + /// Comma separated list of package features to activate |
| 25 | + #[arg(short = 'F', long)] |
| 26 | + features: Vec<String>, |
| 27 | + |
| 28 | + /// Path to Cargo.toml |
| 29 | + #[arg(long, name = "PATH")] |
| 30 | + pub manifest_path: Option<PathBuf>, |
| 31 | + |
| 32 | + /// Build all packages in the workspace |
| 33 | + #[arg(long)] |
| 34 | + pub workspace: bool, |
| 35 | + |
| 36 | + /// Run Kani on the specified packages. |
| 37 | + #[arg(long, short, conflicts_with("workspace"), num_args(1..))] |
| 38 | + pub package: Vec<String>, |
| 39 | + |
| 40 | + /// Exclude the specified packages |
| 41 | + #[arg(long, short, requires("workspace"), conflicts_with("package"), num_args(1..))] |
| 42 | + pub exclude: Vec<String>, |
| 43 | +} |
| 44 | + |
| 45 | +impl CargoCommonArgs { |
| 46 | + /// Parse the string we're given into a list of feature names |
| 47 | + /// |
| 48 | + /// clap can't do this for us because it accepts multiple different delimeters |
| 49 | + pub fn features(&self) -> Vec<String> { |
| 50 | + let mut result = Vec::new(); |
| 51 | + |
| 52 | + for s in &self.features { |
| 53 | + for piece in s.split(&[' ', ',']) { |
| 54 | + result.push(piece.to_owned()); |
| 55 | + } |
| 56 | + } |
| 57 | + result |
| 58 | + } |
| 59 | + |
| 60 | + /// Convert the arguments back to a format that cargo can understand. |
| 61 | + /// Note that the `exclude` option requires special processing and it's not included here. |
| 62 | + pub fn to_cargo_args(&self) -> Vec<OsString> { |
| 63 | + let mut cargo_args: Vec<OsString> = vec![]; |
| 64 | + if self.all_features { |
| 65 | + cargo_args.push("--all-features".into()); |
| 66 | + } |
| 67 | + |
| 68 | + if self.no_default_features { |
| 69 | + cargo_args.push("--no-default-features".into()); |
| 70 | + } |
| 71 | + |
| 72 | + let features = self.features(); |
| 73 | + if !features.is_empty() { |
| 74 | + cargo_args.push(format!("--features={}", features.join(",")).into()); |
| 75 | + } |
| 76 | + |
| 77 | + if let Some(path) = &self.manifest_path { |
| 78 | + cargo_args.push("--manifest-path".into()); |
| 79 | + cargo_args.push(path.into()); |
| 80 | + } |
| 81 | + if self.workspace { |
| 82 | + cargo_args.push("--workspace".into()) |
| 83 | + } |
| 84 | + |
| 85 | + cargo_args.extend(self.package.iter().map(|pkg| format!("-p={pkg}").into())); |
| 86 | + cargo_args |
| 87 | + } |
| 88 | +} |
| 89 | + |
| 90 | +/// Leave it for Cargo to validate these for now. |
| 91 | +impl ValidateArgs for CargoCommonArgs { |
| 92 | + fn validate(&self) -> Result<(), Error> { |
| 93 | + Ok(()) |
| 94 | + } |
| 95 | +} |
| 96 | + |
| 97 | +/// Arguments that Kani pass down into Cargo test essentially uninterpreted. |
| 98 | +#[derive(Debug, Default, clap::Args)] |
| 99 | +pub struct CargoTestArgs { |
| 100 | + /// Test only the specified binary target. |
| 101 | + #[arg(long)] |
| 102 | + pub bin: Vec<String>, |
| 103 | + |
| 104 | + /// Test all binaries. |
| 105 | + #[arg(long)] |
| 106 | + pub bins: bool, |
| 107 | + |
| 108 | + /// Test only the package's library unit tests. |
| 109 | + #[arg(long)] |
| 110 | + pub lib: bool, |
| 111 | + |
| 112 | + /// Arguments to pass down to Cargo |
| 113 | + #[command(flatten)] |
| 114 | + pub common: CargoCommonArgs, |
| 115 | +} |
| 116 | + |
| 117 | +impl CargoTestArgs { |
| 118 | + /// Convert the arguments back to a format that cargo can understand. |
| 119 | + pub fn to_cargo_args(&self) -> Vec<OsString> { |
| 120 | + let mut cargo_args = self.common.to_cargo_args(); |
| 121 | + |
| 122 | + if self.bins { |
| 123 | + cargo_args.push("--bins".into()); |
| 124 | + } |
| 125 | + |
| 126 | + if self.lib { |
| 127 | + cargo_args.push("--lib".into()); |
| 128 | + } |
| 129 | + |
| 130 | + cargo_args.extend(self.bin.iter().map(|binary| format!("--bin={binary}").into())); |
| 131 | + cargo_args |
| 132 | + } |
| 133 | +} |
| 134 | + |
| 135 | +/// Leave it for Cargo to validate these for now. |
| 136 | +impl ValidateArgs for CargoTestArgs { |
| 137 | + fn validate(&self) -> Result<(), Error> { |
| 138 | + self.common.validate() |
| 139 | + } |
| 140 | +} |
0 commit comments