diff --git a/.github/workflows/verify-std-check.yml b/.github/workflows/verify-std-check.yml index 1bad09cd3c6d..6935b2bb4073 100644 --- a/.github/workflows/verify-std-check.yml +++ b/.github/workflows/verify-std-check.yml @@ -59,7 +59,7 @@ jobs: continue-on-error: true run: | kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \ - -Z mem-predicates -Z ptr-to-ref-cast-checks + -Z mem-predicates # If the head failed, check if it's a new failure. - name: Checkout base @@ -77,7 +77,7 @@ jobs: continue-on-error: true run: | kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \ - -Z mem-predicates -Z ptr-to-ref-cast-checks + -Z mem-predicates - name: Compare PR results if: steps.check-head.outcome != 'success' && steps.check-head.outcome != steps.check-base.outcome diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs index 3efc5c0f4f61..3fa74b0e5aba 100644 --- a/kani-compiler/src/args.rs +++ b/kani-compiler/src/args.rs @@ -82,9 +82,6 @@ pub enum ExtraChecks { /// Check that produced values are valid except for uninitialized values. /// See https://github.com/model-checking/kani/issues/920. Validity, - /// Check pointer validity when casting pointers to references. - /// See https://github.com/model-checking/kani/issues/2975. - PtrToRefCast, /// Check for using uninitialized memory. Uninit, } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 4883c608f482..a30eeb7639ce 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -1,7 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use crate::args::ExtraChecks; use crate::codegen_cprover_gotoc::codegen::place::ProjectedPlace; use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable; use crate::codegen_cprover_gotoc::codegen::PropertyClass; @@ -730,18 +729,14 @@ impl<'tcx> GotocCtx<'tcx> { Rvalue::Repeat(op, sz) => self.codegen_rvalue_repeat(op, sz, loc), Rvalue::Ref(_, _, p) | Rvalue::AddressOf(_, p) => { let place_ref = self.codegen_place_ref_stable(&p, loc); - if self.queries.args().ub_check.contains(&ExtraChecks::PtrToRefCast) { - let place_ref_type = place_ref.typ().clone(); - match self.codegen_raw_ptr_deref_validity_check(&p, &loc) { - Some(ptr_validity_check_expr) => Expr::statement_expression( - vec![ptr_validity_check_expr, place_ref.as_stmt(loc)], - place_ref_type, - loc, - ), - None => place_ref, - } - } else { - place_ref + let place_ref_type = place_ref.typ().clone(); + match self.codegen_raw_ptr_deref_validity_check(&p, &loc) { + Some(ptr_validity_check_expr) => Expr::statement_expression( + vec![ptr_validity_check_expr, place_ref.as_stmt(loc)], + place_ref_type, + loc, + ), + None => place_ref, } } Rvalue::Len(p) => self.codegen_rvalue_len(p, loc), diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index bbeb5bfa417d..4b30fe877507 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -135,10 +135,6 @@ impl KaniSession { flags.push("--ub-check=validity".into()) } - if self.args.common_args.unstable_features.contains(UnstableFeature::PtrToRefCastChecks) { - flags.push("--ub-check=ptr_to_ref_cast".into()) - } - if self.args.common_args.unstable_features.contains(UnstableFeature::UninitChecks) { // Automatically enable shadow memory, since the version of uninitialized memory checks // without non-determinism depends on it. diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index 68e4fba28819..120ab0a9e55c 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -89,8 +89,6 @@ pub enum UnstableFeature { ValidValueChecks, /// Ghost state and shadow memory APIs. GhostState, - /// Automatically check that pointers are valid when casting them to references. - PtrToRefCastChecks, /// Automatically check that uninitialized memory is not used. UninitChecks, /// Enable an unstable option or subcommand. diff --git a/tests/expected/dangling-ptr-println/main.rs b/tests/expected/dangling-ptr-println/main.rs index a83afa6f8313..04328c92cb52 100644 --- a/tests/expected/dangling-ptr-println/main.rs +++ b/tests/expected/dangling-ptr-println/main.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ptr-to-ref-cast-checks //! These tests check that Kani correctly detects dangling pointer dereference inside println macro. //! Related issue: . diff --git a/tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs b/tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs index 3b713a34d967..e04ac9cd3169 100644 --- a/tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs +++ b/tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ptr-to-ref-cast-checks //! This test case checks that raw pointer validity is checked before converting it to a reference, e.g., &(*ptr). diff --git a/tests/std-checks/core/Cargo.toml b/tests/std-checks/core/Cargo.toml index f6e1645c3a39..9cacaa1368e3 100644 --- a/tests/std-checks/core/Cargo.toml +++ b/tests/std-checks/core/Cargo.toml @@ -7,7 +7,7 @@ edition = "2021" description = "This crate contains contracts and harnesses for core library" [package.metadata.kani] -unstable = { function-contracts = true, mem-predicates = true, ptr-to-ref-cast-checks = true } +unstable = { function-contracts = true, mem-predicates = true } [package.metadata.kani.flags] output-format = "terse"