Add an unstable option to revert to old, unsound behavior

kani-compiler/src/args.rs

@@ -74,6 +74,9 @@ pub struct Arguments {
     /// Enable specific checks.
     #[clap(long)]
     pub ub_check: Vec<ExtraChecks>,
+    /// Ignore storage markers.
+    #[clap(long)]
+    pub ignore_storage_markers: bool,
 }
 
 #[derive(Debug, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)]

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

@@ -76,9 +76,19 @@ impl<'tcx> GotocCtx<'tcx> {
                 self.codegen_set_discriminant(dest_ty, dest_expr, *variant_index, location)
             }
             StatementKind::StorageLive(var_id) => {
-                Stmt::decl(self.codegen_local(*var_id), None, location)
+                if self.queries.args().ignore_storage_markers {
+                    Stmt::skip(location)
+                } else {
+                    Stmt::decl(self.codegen_local(*var_id), None, location)
+                }
+            }
+            StatementKind::StorageDead(var_id) => {
+                if self.queries.args().ignore_storage_markers {
+                    Stmt::skip(location)
+                } else {
+                    Stmt::dead(self.codegen_local(*var_id), location)
+                }
             }
-            StatementKind::StorageDead(var_id) => Stmt::dead(self.codegen_local(*var_id), location),
             StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping(
                 CopyNonOverlapping { src, dst, count },
             )) => {

kani-driver/src/args/mod.rs

@@ -252,6 +252,14 @@ pub struct VerificationArgs {
     #[arg(long, hide_short_help = true, requires("enable_unstable"))]
     pub ignore_global_asm: bool,
 
+    /// Ignore lifetimes of local variables. This effectively extends their
+    /// lifetimes to the function scope, and hence may cause Kani to miss
+    /// undefined behavior resulting from using the variable after it dies.
+    /// This option may impact the soundness of the analysis and may cause false
+    /// proofs and/or counterexamples
+    #[arg(long, hide_short_help = true, requires("enable_unstable"))]
+    pub ignore_locals_lifetime: bool,
+
     /// Write the GotoC symbol table to a file in JSON format instead of goto binary format.
     #[arg(long, hide_short_help = true)]
     pub write_json_symtab: bool,

kani-driver/src/call_single_file.rs

@@ -105,6 +105,10 @@ impl KaniSession {
             flags.push("--ub-check=validity".into())
         }
 
+        if self.args.ignore_locals_lifetime {
+            flags.push("--ignore-storage-markers".into())
+        }
+
         flags.extend(self.args.common_args.unstable_features.as_arguments().map(str::to_string));
 
         // This argument will select the Kani flavour of the compiler. It will be removed before

tests/perf/btreeset/insert_any/Cargo.toml

@@ -9,3 +9,8 @@ edition = "2021"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
+
+# Temporarily ignore the handling of storage markers till
+# https://github.com/model-checking/kani/issues/3099 is fixed
+[package.metadata.kani]
+flags = { ignore-locals-lifetime = true, enable-unstable = true }

tests/perf/btreeset/insert_multi/Cargo.toml

@@ -9,3 +9,8 @@ edition = "2021"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
+
+# Temporarily ignore the handling of storage markers till
+# https://github.com/model-checking/kani/issues/3099 is fixed
+[package.metadata.kani]
+flags = { ignore-locals-lifetime = true, enable-unstable = true }

tests/perf/btreeset/insert_same/Cargo.toml

@@ -9,3 +9,8 @@ edition = "2021"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
+
+# Temporarily ignore the handling of storage markers till
+# https://github.com/model-checking/kani/issues/3099 is fixed
+[package.metadata.kani]
+flags = { ignore-locals-lifetime = true, enable-unstable = true }

tests/perf/btreeset/insert_same/src/main.rs

@@ -5,6 +5,7 @@
 //! The test is from <https://github.com/model-checking/kani/issues/2022>
 //! With CBMC's default solver (minisat), it takes ~517 seconds
 //! With Kissat 3.0.0, it takes ~22 seconds
+//! It started failing after <https://github.com/model-checking/kani/pull/3080>
 
 use std::collections::BTreeSet;
 

tests/perf/hashset/Cargo.toml

@@ -12,3 +12,8 @@ description = "Verify HashSet basic behavior"
 
 [package.metadata.kani.unstable]
 stubbing = true
+
+# Temporarily ignore the handling of storage markers till
+# https://github.com/model-checking/kani/issues/3099 is fixed
+[package.metadata.kani]
+flags = { ignore-locals-lifetime = true, enable-unstable = true }