Finish deprecating --enable-unstable, --restrict-vtable, and --write-json-symtab

kani-driver/src/args/common.rs

@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! Define arguments that should be common to all subcommands in Kani.
-use crate::args::{ValidateArgs, print_deprecated};
+use crate::args::ValidateArgs;
 use clap::{error::Error, error::ErrorKind};
 pub use kani_metadata::{EnabledUnstableFeatures, UnstableFeature};
 
@@ -18,7 +18,7 @@ pub struct CommonArgs {
     #[arg(long, short, default_value_if("debug", "true", Some("true")))]
     pub verbose: bool,
     /// Enable usage of unstable options
-    #[arg(long, hide_short_help = true)]
+    #[arg(long, hide = true)]
     pub enable_unstable: bool,
 
     /// We no longer support dry-run. Use `--verbose` to see the commands being printed during
@@ -53,7 +53,12 @@ impl CommonArgs {
         if enabled && !self.unstable_features.contains(required) {
             let z_feature = format!("-Z {required}");
             if self.enable_unstable {
-                print_deprecated(self, "--enable-unstable", &z_feature);
+                return Err(Error::raw(
+                    ErrorKind::ValueValidation,
+                    format!(
+                        "The `--enable-unstable` option is obsolete. Use `{z_feature}` instead.",
+                    ),
+                ));
             } else {
                 return Err(Error::raw(
                     ErrorKind::MissingRequiredArgument,

kani-driver/src/args/mod.rs

@@ -52,6 +52,7 @@ pub fn print_obsolete(verbosity: &CommonArgs, option: &str) {
     }
 }
 
+#[allow(dead_code)]
 pub fn print_deprecated(verbosity: &CommonArgs, option: &str, alternative: &str) {
     if !verbosity.quiet {
         warning(&format!(
@@ -284,7 +285,7 @@ pub struct VerificationArgs {
 
     /// Restrict the targets of virtual table function pointer calls.
     /// This feature is unstable and it requires `-Z restrict-vtable` to be used
-    #[arg(long, hide_short_help = true, conflicts_with = "no_restrict_vtable")]
+    #[arg(long, hide = true, conflicts_with = "no_restrict_vtable")]
     pub restrict_vtable: bool,
     /// Disable restricting the targets of virtual table function pointer calls
     #[arg(long, hide_short_help = true)]
@@ -299,7 +300,7 @@ pub struct VerificationArgs {
     pub ignore_global_asm: bool,
 
     /// Write the GotoC symbol table to a file in JSON format instead of goto binary format.
-    #[arg(long, hide_short_help = true)]
+    #[arg(long, hide = true)]
     pub write_json_symtab: bool,
 
     /// Execute CBMC's sanity checks to ensure the goto-program we generate is correct.
@@ -364,9 +365,8 @@ pub struct VerificationArgs {
 
 impl VerificationArgs {
     pub fn restrict_vtable(&self) -> bool {
-        self.restrict_vtable
-            || (self.common_args.unstable_features.contains(UnstableFeature::RestrictVtable)
-                && !self.no_restrict_vtable)
+        self.common_args.unstable_features.contains(UnstableFeature::RestrictVtable)
+            && !self.no_restrict_vtable
         // if we flip the default, this will become: !self.no_restrict_vtable
     }
 
@@ -589,7 +589,10 @@ impl ValidateArgs for VerificationArgs {
         }
 
         if self.write_json_symtab {
-            print_obsolete(&self.common_args, "--write-json-symtab");
+            return Err(Error::raw(
+                ErrorKind::ValueValidation,
+                "The `--write-json-symtab` option is obsolete.",
+            ));
         }
 
         // TODO: these conflicting flags reflect what's necessary to pass current tests unmodified.
@@ -710,13 +713,11 @@ impl ValidateArgs for VerificationArgs {
         )?;
 
         if self.restrict_vtable {
-            // Deprecated `--restrict-vtable` in favor our `-Z restrict-vtable`.
-            print_deprecated(&self.common_args, "--restrict-vtable", "-Z restrict-vtable");
-            self.common_args.check_unstable(
-                true,
-                "--restrict-vtable",
-                UnstableFeature::RestrictVtable,
-            )?;
+            let z_feature = "-Z restrict-vtable";
+            return Err(Error::raw(
+                ErrorKind::ValueValidation,
+                format!("The `--restrict-vtable` option is obsolete. Use `{z_feature}` instead.",),
+            ));
         }
 
         self.common_args.check_unstable(
@@ -728,13 +729,21 @@ impl ValidateArgs for VerificationArgs {
         if !self.c_lib.is_empty()
             && !self.common_args.unstable_features.contains(UnstableFeature::CFfi)
         {
+            let z_feature = "-Z c-ffi";
             if self.common_args.enable_unstable {
-                print_deprecated(&self.common_args, "`--enable-unstable`", "-Z c-ffi");
+                return Err(Error::raw(
+                    ErrorKind::ValueValidation,
+                    format!(
+                        "The `--enable-unstable` option is obsolete. Use `{z_feature}` instead.",
+                    ),
+                ));
             } else {
                 return Err(Error::raw(
                     ErrorKind::MissingRequiredArgument,
-                    "The `--c-lib` argument is unstable and requires `-Z c-ffi` to enable \
-                unstable C-FFI support.",
+                    format!(
+                        "The `--c-lib` argument is unstable and requires `{z_feature}` to enable \
+                unstable C-FFI support."
+                    ),
                 ));
             }
         }
@@ -1025,8 +1034,13 @@ mod tests {
 
     #[test]
     fn check_restrict_vtable_unstable() {
-        let restrict_vtable = |args: StandaloneArgs| args.verify_opts.restrict_vtable();
-        check("--restrict-vtable", Some(UnstableFeature::RestrictVtable), restrict_vtable);
+        let res = parse_unstable_enabled("--output-format=terse", UnstableFeature::RestrictVtable)
+            .unwrap();
+        assert!(res.verify_opts.restrict_vtable());
+
+        let res = parse_unstable_enabled("--no-restrict-vtable", UnstableFeature::RestrictVtable)
+            .unwrap();
+        assert!(!res.verify_opts.restrict_vtable());
     }
 
     #[test]

kani-driver/src/call_goto_instrument.rs

@@ -76,7 +76,7 @@ impl KaniSession {
         Ok(())
     }
 
-    /// Apply --restrict-vtable to a goto binary.
+    /// Apply -Z restrict-vtable to a goto binary.
     pub fn apply_vtable_restrictions(&self, goto_file: &Path, restrictions: &Path) -> Result<()> {
         let linked_restrictions = alter_extension(goto_file, "linked-restrictions.json");
         self.record_temporary_file(&linked_restrictions);

tests/cargo-kani/asm/global/Cargo.toml

@@ -12,5 +12,5 @@ edition = "2021"
 crate_with_global_asm = { path = "crate_with_global_asm" }
 
 [package.metadata.kani]
-# Issue with MIR Linker on static constant.
-flags = { enable-unstable = true, ignore-global-asm = true }
+flags = { ignore-global-asm = true}
+unstable = { unstable-options = true }

tests/kani/DynTrait/vtable_restrictions_fail_fixme.rs

@@ -6,7 +6,7 @@
 // FIXME until the corresponding CBMC path lands: https://github.com/diffblue/cbmc/pull/6376
 
 // kani-expect-fail
-// kani-flags: --restrict-vtable
+// kani-flags: -Z restrict-vtable
 
 #![feature(core_intrinsics)]
 #![feature(ptr_metadata)]