Delete obsolete stubs for Vec and related options (rust-lang#2770)

Author: zhassan-aws

CHANGELOG.md

@@ -4,6 +4,11 @@ This file contains notable changes (e.g. breaking changes, major changes, etc.)
 
 This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards.
 
+## [0.37.0]
+
+### Major Changes
+* Delete obsolete stubs for `Vec` and related options ([pull request](https://github.com/model-checking/kani/pull/2770) by @zhassan-aws) 
+
 ## [0.36.0]
 
 ## What's Changed

kani-driver/src/args/mod.rs

@@ -226,18 +226,6 @@ pub struct VerificationArgs {
     #[arg(short, long, hide = true, requires("enable_unstable"))]
     pub jobs: Option<Option<usize>>,
 
-    // Hide option till https://github.com/model-checking/kani/issues/697 is
-    // fixed.
-    /// Use abstractions for the standard library.
-    /// This is an experimental feature and requires `--enable-unstable` to be used
-    #[arg(long, hide = true, requires("enable_unstable"))]
-    pub use_abs: bool,
-    // Hide option till https://github.com/model-checking/kani/issues/697 is
-    // fixed.
-    /// Choose abstraction for modules of standard library if available
-    #[arg(long, default_value = "std", ignore_case = true, hide = true, value_enum)]
-    pub abs_type: AbstractionType,
-
     /// Enable extra pointer checks such as invalid pointers in relation operations and pointer
     /// arithmetic overflow.
     /// This feature is unstable and it may yield false counter examples. It requires
@@ -374,32 +362,6 @@ pub enum OutputFormat {
     Old,
 }
 
-#[derive(Clone, Debug, PartialEq, Eq, ValueEnum)]
-pub enum AbstractionType {
-    Std,
-    Kani,
-    // Clap defaults to `c-ffi`
-    CFfi,
-    // Clap defaults to `no-back`
-    NoBack,
-}
-impl std::fmt::Display for AbstractionType {
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        match self {
-            Self::Std => f.write_str("std"),
-            Self::Kani => f.write_str("kani"),
-            Self::CFfi => f.write_str("c-ffi"),
-            Self::NoBack => f.write_str("no-back"),
-        }
-    }
-}
-#[cfg(test)]
-impl AbstractionType {
-    pub fn variants() -> Vec<&'static str> {
-        vec!["std", "kani", "c-ffi", "no-back"]
-    }
-}
-
 #[derive(Debug, clap::Args)]
 pub struct CheckArgs {
     // Rust argument parsers (/clap) don't have the convenient '--flag' and '--no-flag' boolean pairs, so approximate
@@ -818,18 +780,6 @@ mod tests {
         };
     }
 
-    #[test]
-    fn check_abs_type() {
-        // Since we manually implemented this, consistency check it
-        for t in AbstractionType::variants() {
-            assert_eq!(t, format!("{}", AbstractionType::from_str(t, false).unwrap()));
-        }
-        check_opt!("--abs-type std", false, abs_type, AbstractionType::Std);
-        check_opt!("--abs-type kani", false, abs_type, AbstractionType::Kani);
-        check_opt!("--abs-type c-ffi", false, abs_type, AbstractionType::CFfi);
-        check_opt!("--abs-type no-back", false, abs_type, AbstractionType::NoBack);
-    }
-
     #[test]
     fn check_dry_run_fails() {
         // We don't support --dry-run anymore but we print a friendly reminder for now.
@@ -865,11 +815,6 @@ mod tests {
         StandaloneArgs::try_parse_from(args.split(' '))
     }
 
-    #[test]
-    fn check_abs_unstable() {
-        check_unstable_flag!("--use-abs", use_abs);
-    }
-
     #[test]
     fn check_restrict_vtable_unstable() {
         check_unstable_flag!("--restrict-vtable", restrict_vtable);

kani-driver/src/call_goto_cc.rs

@@ -6,7 +6,6 @@ use std::ffi::OsString;
 use std::path::{Path, PathBuf};
 use std::process::Command;
 
-use crate::args::AbstractionType;
 use crate::session::KaniSession;
 
 impl KaniSession {
@@ -17,15 +16,6 @@ impl KaniSession {
         args.extend(inputs.iter().map(|x| x.clone().into_os_string()));
         args.extend(self.args.c_lib.iter().map(|x| x.clone().into_os_string()));
 
-        // Special case hack for handling the "c-ffi" abs-type
-        if self.args.use_abs && self.args.abs_type == AbstractionType::CFfi {
-            let vec = self.kani_c_stubs.join("vec/vec.c");
-            let hashset = self.kani_c_stubs.join("hashset/hashset.c");
-
-            args.push(vec.into_os_string());
-            args.push(hashset.into_os_string());
-        }
-
         // TODO think about this: kani_lib_c is just an empty c file. Maybe we could just
         // create such an empty file ourselves instead of having to look up this path.
         args.push(self.kani_lib_c.clone().into_os_string());

kani-driver/src/call_single_file.rs

@@ -125,14 +125,6 @@ impl KaniSession {
             ]
             .map(OsString::from),
         );
-        if self.args.use_abs {
-            flags.push("-Z".into());
-            flags.push("force-unstable-if-unmarked=yes".into()); // ??
-            flags.push("--cfg=use_abs".into());
-            flags.push("--cfg".into());
-            let abs_type = format!("abs_type={}", self.args.abs_type.to_string().to_lowercase());
-            flags.push(abs_type.into());
-        }
 
         if let Some(seed_opt) = self.args.randomize_layout {
             flags.push("-Z".into());

kani-driver/src/session.rs

@@ -35,8 +35,6 @@ pub struct KaniSession {
     pub kani_compiler: PathBuf,
     /// The location we found 'kani_lib.c'
     pub kani_lib_c: PathBuf,
-    /// The location we found the Kani C stub .c files
-    pub kani_c_stubs: PathBuf,
 
     /// The temporary files we littered that need to be cleaned up at the end of execution
     pub temporaries: Mutex<Vec<PathBuf>>,
@@ -62,7 +60,6 @@ impl KaniSession {
             codegen_tests: false,
             kani_compiler: install.kani_compiler()?,
             kani_lib_c: install.kani_lib_c()?,
-            kani_c_stubs: install.kani_c_stubs()?,
             temporaries: Mutex::new(vec![]),
         })
     }
@@ -339,10 +336,6 @@ impl InstallType {
         self.base_path_with("library/kani/kani_lib.c")
     }
 
-    pub fn kani_c_stubs(&self) -> Result<PathBuf> {
-        self.base_path_with("library/kani/stubs/C")
-    }
-
     /// A common case is that our repo and release bundle have the same `subpath`
     fn base_path_with(&self, subpath: &str) -> Result<PathBuf> {
         let path = match self {