diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs index fcc346bd745f..225cb94f4264 100644 --- a/kani-compiler/src/args.rs +++ b/kani-compiler/src/args.rs @@ -74,6 +74,9 @@ pub struct Arguments { /// Enable specific checks. #[clap(long)] pub ub_check: Vec, + /// Ignore storage markers. + #[clap(long)] + pub ignore_storage_markers: bool, } #[derive(Debug, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)] diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 6379a023423f..9a78515fde90 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/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 }, )) => { diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index aeda94168840..36d9e0af2d0e 100644 --- a/kani-driver/src/args/mod.rs +++ b/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, diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 24691943bc0f..07899c8c4899 100644 --- a/kani-driver/src/call_single_file.rs +++ b/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 diff --git a/tests/perf/btreeset/insert_any/Cargo.toml b/tests/perf/btreeset/insert_any/Cargo.toml index 41fa0a2db3ba..66d8ecdddeb1 100644 --- a/tests/perf/btreeset/insert_any/Cargo.toml +++ b/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 } diff --git a/tests/perf/btreeset/insert_multi/Cargo.toml b/tests/perf/btreeset/insert_multi/Cargo.toml index bdd2f4e3528a..44028f8c842d 100644 --- a/tests/perf/btreeset/insert_multi/Cargo.toml +++ b/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 } diff --git a/tests/perf/btreeset/insert_same/Cargo.toml b/tests/perf/btreeset/insert_same/Cargo.toml index 0a4e0f7ee037..465119c74fbe 100644 --- a/tests/perf/btreeset/insert_same/Cargo.toml +++ b/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 } diff --git a/tests/perf/hashset/Cargo.toml b/tests/perf/hashset/Cargo.toml index d0757e11154b..464fba412e6d 100644 --- a/tests/perf/hashset/Cargo.toml +++ b/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 } diff --git a/tools/build-kani/src/sysroot.rs b/tools/build-kani/src/sysroot.rs index 3a6239106826..b831ed0d63a8 100644 --- a/tools/build-kani/src/sysroot.rs +++ b/tools/build-kani/src/sysroot.rs @@ -124,7 +124,14 @@ fn build_kani_lib( "--message-format", "json-diagnostic-rendered-ansi", ]; - let mut rustc_args = vec!["--cfg=kani", "--cfg=kani_sysroot", "-Z", "always-encode-mir"]; + let mut rustc_args = vec![ + "--cfg=kani", + "--cfg=kani_sysroot", + "-Z", + "always-encode-mir", + "-Z", + "mir-enable-passes=-RemoveStorageMarkers", + ]; rustc_args.extend_from_slice(extra_rustc_args); let mut cmd = Command::new("cargo") .env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join("\x1f"))