From e3d1568e9bcb3b6c1538bff368c4ab6095cd8e09 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 26 Apr 2024 12:05:04 +0000 Subject: [PATCH] Revert #3080 except for std enablement --- kani-compiler/src/args.rs | 3 --- .../src/codegen_cprover_gotoc/codegen/statement.rs | 8 ++------ kani-driver/src/args/mod.rs | 8 -------- kani-driver/src/call_single_file.rs | 4 ---- tests/perf/btreeset/insert_any/Cargo.toml | 5 ----- tests/perf/btreeset/insert_multi/Cargo.toml | 5 ----- tests/perf/btreeset/insert_same/Cargo.toml | 5 ----- tests/perf/hashset/Cargo.toml | 5 ----- 8 files changed, 2 insertions(+), 41 deletions(-) diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs index 225cb94f4264..fcc346bd745f 100644 --- a/kani-compiler/src/args.rs +++ b/kani-compiler/src/args.rs @@ -74,9 +74,6 @@ 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 6f3a8923c4b6..ee69f1173e42 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -76,9 +76,7 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_set_discriminant(dest_ty, dest_expr, *variant_index, location) } StatementKind::StorageLive(var_id) => { - if self.queries.args().ignore_storage_markers - || !self.current_fn().is_address_taken_local(*var_id) - { + if !self.current_fn().is_address_taken_local(*var_id) { Stmt::skip(location) } else { let global_dead_object = self.ensure_global_var( @@ -102,9 +100,7 @@ impl<'tcx> GotocCtx<'tcx> { } } StatementKind::StorageDead(var_id) => { - if self.queries.args().ignore_storage_markers - || !self.current_fn().is_address_taken_local(*var_id) - { + if !self.current_fn().is_address_taken_local(*var_id) { Stmt::skip(location) } else { let global_dead_object = self.ensure_global_var( diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 36d9e0af2d0e..aeda94168840 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -252,14 +252,6 @@ 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 07899c8c4899..24691943bc0f 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -105,10 +105,6 @@ 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 66d8ecdddeb1..41fa0a2db3ba 100644 --- a/tests/perf/btreeset/insert_any/Cargo.toml +++ b/tests/perf/btreeset/insert_any/Cargo.toml @@ -9,8 +9,3 @@ 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 44028f8c842d..bdd2f4e3528a 100644 --- a/tests/perf/btreeset/insert_multi/Cargo.toml +++ b/tests/perf/btreeset/insert_multi/Cargo.toml @@ -9,8 +9,3 @@ 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 465119c74fbe..0a4e0f7ee037 100644 --- a/tests/perf/btreeset/insert_same/Cargo.toml +++ b/tests/perf/btreeset/insert_same/Cargo.toml @@ -9,8 +9,3 @@ 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 464fba412e6d..d0757e11154b 100644 --- a/tests/perf/hashset/Cargo.toml +++ b/tests/perf/hashset/Cargo.toml @@ -12,8 +12,3 @@ 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 }