Unified handling for unstable command line flags across compiler and driver (rust-lang#2719)

Co-authored-by: Felipe R. Monteiro <[email protected]>

Author: JustusAdam

Cargo.lock

@@ -549,6 +549,7 @@ dependencies = [
 name = "kani_metadata"
 version = "0.36.0"
 dependencies = [
+ "clap",
  "cprover_bindings",
  "serde",
  "strum 0.25.0",

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<UnstableFeatures>,
-}
-
-#[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 {

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,

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` \

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.

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"] }

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 {

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<UnstableFeature>,
+}
+
+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<Item = &str> {
+        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)
+    }
+}