Remove experimental unsound features (model-checking#2372)

Remove stale option that's no longer being used.

Author: celinval

.github/workflows/kani.yml

@@ -52,25 +52,6 @@ jobs:
           KANI_ENABLE_WRITE_JSON_SYMTAB: 1
         run: ./scripts/kani-regression.sh
 
-  experimental-features-regression:
-    runs-on: ubuntu-20.04
-    env:
-      KANI_ENABLE_UNSOUND_EXPERIMENTS: 1
-    steps:
-      - name: Checkout Kani
-        uses: actions/checkout@v3
-
-      - name: Setup Kani Dependencies
-        uses: ./.github/actions/setup
-        with:
-          os: ubuntu-20.04
-
-      - name: Build Kani
-        run: cargo build-dev
-
-      - name: Execute Kani regression
-        run: ./scripts/kani-regression.sh
-
   perf:
     runs-on: ubuntu-20.04
     steps:

kani-compiler/Cargo.toml

@@ -37,7 +37,6 @@ tracing-tree = "0.2.2"
 default = ['cprover']
 cprover = ['ar', 'cbmc', 'libc', 'num', 'object', 'rustc-demangle', 'serde',
     'serde_json', "strum", "strum_macros"]
-unsound_experiments = ["kani_queries/unsound_experiments"]
 write_json_symtab = []
 
 [package.metadata.rust-analyzer]

kani-compiler/kani_queries/Cargo.toml

@@ -8,9 +8,6 @@ edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
 
-[features]
-unsound_experiments = []
-
 [dependencies]
 tracing = {version = "0.1"}
 strum = {version = "0.24.0"}

kani-compiler/kani_queries/src/lib.rs

@@ -4,12 +4,6 @@
 use std::sync::{Arc, Mutex};
 use strum_macros::{AsRefStr, EnumString, EnumVariantNames};
 
-#[cfg(feature = "unsound_experiments")]
-mod unsound_experiments;
-
-#[cfg(feature = "unsound_experiments")]
-use crate::unsound_experiments::UnsoundExperiments;
-
 #[derive(Debug, Default, Clone, Copy, AsRefStr, EnumString, EnumVariantNames, PartialEq, Eq)]
 #[strum(serialize_all = "snake_case")]
 pub enum ReachabilityType {
@@ -47,11 +41,6 @@ pub trait UserInput {
 
     fn set_stubbing_enabled(&mut self, stubbing_enabled: bool);
     fn get_stubbing_enabled(&self) -> bool;
-
-    #[cfg(feature = "unsound_experiments")]
-    fn get_unsound_experiments(&self) -> UnsoundExperiments;
-    #[cfg(feature = "unsound_experiments")]
-    fn set_unsound_experiments(&mut self, experiments: UnsoundExperiments);
 }
 
 /// This structure should only be used behind a synchronized reference or a snapshot.
@@ -65,8 +54,6 @@ pub struct QueryDb {
     write_json_symtab: bool,
     reachability_analysis: ReachabilityType,
     stubbing_enabled: bool,
-    #[cfg(feature = "unsound_experiments")]
-    unsound_experiments: UnsoundExperiments,
 }
 
 impl QueryDb {
@@ -79,8 +66,6 @@ impl QueryDb {
             write_json_symtab: false,
             reachability_analysis: ReachabilityType::None,
             stubbing_enabled: false,
-            #[cfg(feature = "unsound_experiments")]
-            unsound_experiments: unsound_experiments::UnsoundExperiments { zero_init_vars: false },
         }))
     }
 }
@@ -141,14 +126,4 @@ impl UserInput for QueryDb {
     fn get_write_json_symtab(&self) -> bool {
         self.write_json_symtab
     }
-
-    #[cfg(feature = "unsound_experiments")]
-    fn get_unsound_experiments(&self) -> UnsoundExperiments {
-        self.unsound_experiments
-    }
-
-    #[cfg(feature = "unsound_experiments")]
-    fn set_unsound_experiments(&mut self, experiments: UnsoundExperiments) {
-        self.unsound_experiments = experiments
-    }
 }

kani-compiler/kani_queries/src/unsound_experiments.rs

@@ -263,7 +263,6 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Our model of GotoC has a similar statement, which is later lowered
     /// to assigning a Nondet in CBMC, with a comment specifying that it
     /// corresponds to a Deinit.
-    #[cfg(not(feature = "unsound_experiments"))]
     fn codegen_deinit(&mut self, place: &Place<'tcx>, loc: Location) -> Stmt {
         let dst_mir_ty = self.place_ty(place);
         let dst_type = self.codegen_ty(dst_mir_ty);

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

@@ -708,7 +708,6 @@ impl<'tcx> GotocCtx<'tcx> {
     /// By default, returns `None` which leaves the variable uninitilized.
     /// In CBMC, this translates to a NONDET value.
     /// In the future, we might want to replace this with `Poison`.
-    #[cfg(not(feature = "unsound_experiments"))]
     pub fn codegen_default_initializer(&self, _e: &Expr) -> Option<Expr> {
         None
     }

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

@@ -146,11 +146,6 @@ impl Callbacks for KaniCompiler {
             );
             queries.set_reachability_analysis(matches.reachability_type());
 
-            #[cfg(feature = "unsound_experiments")]
-            crate::unsound_experiments::arg_parser::add_unsound_experiment_args_to_queries(
-                queries, &matches,
-            );
-
             // If appropriate, collect and set the stub mapping.
             if matches.get_flag(parser::ENABLE_STUBBING)
                 && queries.get_reachability_analysis() == ReachabilityType::Harnesses

kani-compiler/src/kani_compiler.rs

@@ -36,7 +36,6 @@ mod kani_compiler;
 mod kani_middle;
 mod parser;
 mod session;
-mod unsound_experiments;
 
 use rustc_driver::{RunCompiler, TimePassesCallbacks};
 use std::env;

kani-compiler/src/main.rs

@@ -147,9 +147,6 @@ pub fn parser() -> Command {
                 .action(ArgAction::Set)
                 .help("Pass the kani version to the compiler to ensure cache coherence."),
         );
-    #[cfg(feature = "unsound_experiments")]
-    let app = crate::unsound_experiments::arg_parser::add_unsound_experiments_to_parser(app);
-
     app
 }