forked from model-checking/kani
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Unified handling for unstable command line flags across compiler and …
…driver (model-checking#2719) Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>
- Loading branch information
1 parent
dd2003b
commit 9cd3de1
Showing
8 changed files
with
137 additions
and
34 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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) | ||
| } | ||
| } |