diff --git a/Cargo.lock b/Cargo.lock index 4a9982b30efe..935dfc467d1f 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -549,6 +549,7 @@ dependencies = [ name = "kani_metadata" version = "0.36.0" dependencies = [ + "clap", "cprover_bindings", "serde", "strum 0.25.0", diff --git a/kani-driver/src/args/common.rs b/kani-driver/src/args/common.rs index a4325ca610fa..d4ac0a61bd17 100644 --- a/kani-driver/src/args/common.rs +++ b/kani-driver/src/args/common.rs @@ -2,7 +2,8 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! Define arguments that should be common to all subcommands in Kani. use crate::args::ValidateArgs; -use clap::{error::Error, error::ErrorKind, ValueEnum}; +use clap::{error::Error, error::ErrorKind}; +pub use kani_metadata::{EnabledUnstableFeatures, UnstableFeature}; /// Common Kani arguments that we expect to be included in most subcommands. #[derive(Debug, clap::Args)] @@ -26,26 +27,8 @@ pub struct CommonArgs { pub dry_run: bool, /// Enable an unstable feature. - #[arg(short = 'Z', num_args(1), value_name = "UNSTABLE_FEATURE")] - pub unstable_features: Vec, -} - -#[derive(Copy, Clone, Debug, PartialEq, Eq, ValueEnum, strum_macros::Display)] -#[strum(serialize_all = "kebab-case")] -pub enum UnstableFeatures { - /// Allow replacing certain items with stubs (mocks). - /// See [RFC-0002](https://model-checking.github.io/kani/rfc/rfcs/0002-function-stubbing.html) - Stubbing, - /// Generate a C-like file equivalent to input program used for debugging purpose. - GenC, - /// Allow Kani to link against C code. - CFfi, - /// Enable concrete playback flow. - ConcretePlayback, - /// Enable Kani's unstable async library. - AsyncLib, - /// Enable line coverage instrumentation/reports - LineCoverage, + #[clap(flatten)] + pub unstable_features: EnabledUnstableFeatures, } impl ValidateArgs for CommonArgs { diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 8be6bceab921..04c64dd574da 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -349,7 +349,7 @@ impl VerificationArgs { /// Is experimental stubbing enabled? pub fn is_stubbing_enabled(&self) -> bool { self.enable_stubbing - || self.common_args.unstable_features.contains(&UnstableFeatures::Stubbing) + || self.common_args.unstable_features.contains(UnstableFeature::Stubbing) } } @@ -628,7 +628,7 @@ impl ValidateArgs for VerificationArgs { } if self.concrete_playback.is_some() - && !self.common_args.unstable_features.contains(&UnstableFeatures::ConcretePlayback) + && !self.common_args.unstable_features.contains(UnstableFeature::ConcretePlayback) { if self.common_args.enable_unstable { print_deprecated(&self.common_args, "--enable-unstable", "-Z concrete-playback"); @@ -642,7 +642,7 @@ impl ValidateArgs for VerificationArgs { } if !self.c_lib.is_empty() - && !self.common_args.unstable_features.contains(&UnstableFeatures::CFfi) + && !self.common_args.unstable_features.contains(UnstableFeature::CFfi) { if self.common_args.enable_unstable { print_deprecated(&self.common_args, "`--enable-unstable`", "-Z c-ffi"); @@ -656,7 +656,7 @@ impl ValidateArgs for VerificationArgs { } if self.coverage - && !self.common_args.unstable_features.contains(&UnstableFeatures::LineCoverage) + && !self.common_args.unstable_features.contains(UnstableFeature::LineCoverage) { return Err(Error::raw( ErrorKind::MissingRequiredArgument, diff --git a/kani-driver/src/args/playback_args.rs b/kani-driver/src/args/playback_args.rs index eabeaae72a9d..c47b81515953 100644 --- a/kani-driver/src/args/playback_args.rs +++ b/kani-driver/src/args/playback_args.rs @@ -3,7 +3,7 @@ //! Implements the subcommand handling of the playback subcommand use crate::args::cargo::CargoTestArgs; -use crate::args::common::UnstableFeatures; +use crate::args::common::UnstableFeature; use crate::args::{CommonArgs, ValidateArgs}; use clap::error::ErrorKind; use clap::{Error, Parser, ValueEnum}; @@ -87,7 +87,7 @@ impl ValidateArgs for KaniPlaybackArgs { impl ValidateArgs for PlaybackArgs { fn validate(&self) -> Result<(), Error> { self.common_opts.validate()?; - if !self.common_opts.unstable_features.contains(&UnstableFeatures::ConcretePlayback) { + if !self.common_opts.unstable_features.contains(UnstableFeature::ConcretePlayback) { return Err(Error::raw( ErrorKind::MissingRequiredArgument, "The `playback` subcommand is unstable and requires `-Z concrete-playback` \ diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 30cdf88db835..6e51d120dda3 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -100,13 +100,7 @@ impl KaniSession { flags.push("--coverage-checks".into()); } - flags.extend( - self.args - .common_args - .unstable_features - .iter() - .map(|feature| format!("--unstable={feature}")), - ); + flags.extend(self.args.common_args.unstable_features.as_arguments().map(str::to_string)); // This argument will select the Kani flavour of the compiler. It will be removed before // rustc driver is invoked. diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml index e581ae2c7cd4..6ff170849d66 100644 --- a/kani_metadata/Cargo.toml +++ b/kani_metadata/Cargo.toml @@ -15,3 +15,4 @@ serde = {version = "1", features = ["derive"]} cbmc = { path = "../cprover_bindings", package = "cprover_bindings" } strum = "0.25.0" strum_macros = "0.25.2" +clap = { version = "4.1.3", features = ["derive"] } diff --git a/kani_metadata/src/lib.rs b/kani_metadata/src/lib.rs index 7da3cbb94121..fa5a8828b6be 100644 --- a/kani_metadata/src/lib.rs +++ b/kani_metadata/src/lib.rs @@ -1,6 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +extern crate clap; + use std::{collections::HashSet, path::PathBuf}; use serde::{Deserialize, Serialize}; @@ -13,8 +15,11 @@ pub use vtable::*; pub mod artifact; mod cbmc_solver; mod harness; +pub mod unstable; mod vtable; +pub use unstable::{EnabledUnstableFeatures, UnstableFeature}; + /// The structure of `.kani-metadata.json` files, which are emitted for each crate #[derive(Debug, Clone, Serialize, Deserialize)] pub struct KaniMetadata { diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs new file mode 100644 index 000000000000..6cd3816103ef --- /dev/null +++ b/kani_metadata/src/unstable.rs @@ -0,0 +1,119 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Unified handling of unstable-feature flags across Kani. +//! +//! The central types are [`UnstableFeature`], which describes a single feature +//! and is intended as a small, cheap enum that is [`Copy`]. +//! [`EnabledUnstableFeatures`] then describes which [`UnstableFeature`]s are +//! enabled. +//! +//! To check if a feature is enabled use [`EnabledUnstableFeatures::contains`]. +//! +//! ### Parsing +//! +//! [`EnabledUnstableFeatures`] is intended to be used with the [`clap`] +//! "derive" API. You can directly drop it into a command line arguments struct +//! like so: +//! +//! ``` +//! # use kani_metadata::unstable::*; +//! use clap::Parser; +//! +//! #[derive(Parser)] +//! struct MyCmdArgs { +//! // ... +//! #[clap(flatten)] +//! unstable: EnabledUnstableFeatures, +//! } +//! ``` +//! +//! Which will add the long form `--unstable feature-name` and short form `-Z +//! feature-name` options to your argument parser. +//! +//! **Note:** [`clap`] internally uses a unique name (string) to refer to each +//! argument or group, which is usually derived from the field name. +//! [`EnabledUnstableFeatures`] uses the internal name +//! `"enabled_unstable_features"` which may therefore not be used (as a field +//! name) in the embedding argument struct, e.g. `MyCmdArgs`. +//! +//! ### Reusing +//! +//! You can turn an [`UnstableFeature`] back into it's command line +//! representation. This should be done with +//! [`EnabledUnstableFeatures::as_arguments`], which returns an iterator that, +//! when passed to e.g. [`std::process::Command::args`] will enable those +//! features in the subsequent call. +//! +//! You can also serialize a single feature with +//! [`UnstableFeature::as_argument`]. +//! +//! Both of these methods return values that are ready for direct usage on the +//! command line, e.g one or more `-Z feature-name`. If you need only the +//! serialized name of the feature use [`UnstableFeature::as_ref`]. + +/// A single unstable feature. This is where you should register your own if you +/// are adding new ones, e.g. as part of the RFC process. +/// +/// For usage see the [module level documentation][self]. +#[derive( + Copy, + Clone, + Debug, + PartialEq, + Eq, + clap::ValueEnum, + strum_macros::Display, + strum_macros::AsRefStr +)] +#[strum(serialize_all = "kebab-case")] +pub enum UnstableFeature { + /// Allow replacing certain items with stubs (mocks). + /// See [RFC-0002](https://model-checking.github.io/kani/rfc/rfcs/0002-function-stubbing.html) + Stubbing, + /// Generate a C-like file equivalent to input program used for debugging purpose. + GenC, + /// Allow Kani to link against C code. + CFfi, + /// Enable concrete playback flow. + ConcretePlayback, + /// Enable Kani's unstable async library. + AsyncLib, + /// Enable line coverage instrumentation/reports. + LineCoverage, +} + +impl UnstableFeature { + /// Serialize this feature into a format in which it can be passed on the + /// command line. Note that this already includes the `-Z` prefix, if you + /// require only the serialized feature name use [`Self::as_ref`]. + pub fn as_argument(&self) -> [&str; 2] { + ["-Z", self.as_ref()] + } +} + +/// An opaque collection of unstable features that is enabled on this session. +/// Used to unify handling of unstable command line arguments across the +/// compiler and the driver. +/// +/// For usage see the [module level documentation][self]. +#[derive(clap::Args, Debug)] +pub struct EnabledUnstableFeatures { + #[clap(short = 'Z', long = "unstable", num_args(1), value_name = "UNSTABLE_FEATURE")] + enabled_unstable_features: Vec, +} + +impl EnabledUnstableFeatures { + /// The preferred way to serialize these unstable features back into a + /// format that can be used as command line arguments fo an invocation of + /// e.g. the compiler. + /// + /// See also the [module level documentation][self]. + pub fn as_arguments(&self) -> impl Iterator { + self.enabled_unstable_features.iter().flat_map(|f| f.as_argument()) + } + + /// Is this feature enabled? + pub fn contains(&self, feature: UnstableFeature) -> bool { + self.enabled_unstable_features.contains(&feature) + } +}