Remove experimental unsound features (rust-lang#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
 }
 

kani-compiler/src/parser.rs

@@ -11,10 +11,6 @@ homepage = "https://github.com/model-checking/kani"
 repository = "https://github.com/model-checking/kani"
 publish = false
 
-[features]
-unsound_experiments = []
-
-
 [dependencies]
 kani_metadata = { path = "../kani_metadata" }
 cargo_metadata = "0.15.0"

kani-compiler/src/unsound_experiments/arg_parser.rs

@@ -1,8 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-#[cfg(feature = "unsound_experiments")]
-use crate::unsound_experiments::UnsoundExperimentArgs;
 use crate::util::warning;
 use kani_metadata::CbmcSolver;
 
@@ -124,10 +122,6 @@ pub struct KaniArgs {
     #[command(flatten)]
     pub checks: CheckArgs,
 
-    #[cfg(feature = "unsound_experiments")]
-    #[command(flatten)]
-    pub unsound_experiments: UnsoundExperimentArgs,
-
     /// Entry point for verification (symbol name).
     /// This is an unstable feature. Consider using --harness instead
     #[arg(long, hide = true, requires("enable_unstable"))]

kani-compiler/src/unsound_experiments/mod.rs

@@ -103,9 +103,6 @@ impl KaniSession {
         // rustc driver is invoked.
         flags.push("--goto-c".into());
 
-        #[cfg(feature = "unsound_experiments")]
-        flags.extend(self.args.unsound_experiments.process_args());
-
         flags
     }
 

kani-compiler/src/unsound_experiments/zero_init.rs

@@ -204,9 +204,6 @@ impl KaniSession {
 
         self.stubbing_statuses(results);
 
-        #[cfg(feature = "unsound_experiments")]
-        self.args.unsound_experiments.print_warnings();
-
         if failing > 0 {
             // Failure exit code without additional error message
             drop(self);

kani-driver/Cargo.toml

@@ -34,9 +34,6 @@ mod project;
 mod session;
 mod util;
 
-#[cfg(feature = "unsound_experiments")]
-mod unsound_experiments;
-
 /// The main function for the `kani-driver`.
 /// The driver can be invoked via `cargo kani` and `kani` commands, which determines what kind of
 /// project should be verified.

kani-driver/src/args.rs

@@ -2,9 +2,6 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
-# To enable "unsound_experimental features, run as follows:
-# `KANI_ENABLE_UNSOUND_EXPERIMENTS=1 scripts/kani-regression.sh`
-
 if [[ -z $KANI_REGRESSION_KEEP_GOING ]]; then
   set -o errexit
 fi
@@ -30,9 +27,7 @@ check_kissat_version.sh
 ${SCRIPT_DIR}/kani-fmt.sh --check
 
 # Build all packages in the workspace
-if [[ "" != "${KANI_ENABLE_UNSOUND_EXPERIMENTS-}" ]]; then
-  cargo build-dev -- --features unsound_experiments
-elif [[ "" != "${KANI_ENABLE_WRITE_JSON_SYMTAB-}" ]]; then
+if [[ "" != "${KANI_ENABLE_WRITE_JSON_SYMTAB-}" ]]; then
   cargo build-dev -- --features write_json_symtab
 else
   cargo build-dev
@@ -59,12 +54,6 @@ TESTS=(
     "kani-fixme kani-fixme"
 )
 
-if [[ "" != "${KANI_ENABLE_UNSOUND_EXPERIMENTS-}" ]]; then
-  TESTS+=("unsound_experiments kani")
-else
-  TESTS+=("no_unsound_experiments expected")
-fi
-
 # Build compiletest and print configuration. We pick suite / mode combo so there's no test.
 echo "--- Compiletest configuration"
 cargo run -p compiletest --quiet -- --suite kani --mode cargo-kani --dry-run --verbose