From 5120b0251f9fc31ba36e77fdc6bb09c2c2d02da9 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Tue, 4 Jun 2024 14:41:20 -0700 Subject: [PATCH] Put the extra check behind an unstable feature flag --- kani-compiler/src/args.rs | 3 +++ .../codegen_cprover_gotoc/codegen/rvalue.rs | 19 +++++++++++------- kani-driver/src/call_single_file.rs | 4 ++++ kani_metadata/src/unstable.rs | 2 ++ tests/expected/ptr_to_ref_cast/expected | 20 +++++++++---------- .../ptr_to_ref_cast/ptr_to_ref_cast.rs | 1 + tests/std-checks/core/Cargo.toml | 2 +- 7 files changed, 33 insertions(+), 18 deletions(-) diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs index 225cb94f4264..7a57976a7168 100644 --- a/kani-compiler/src/args.rs +++ b/kani-compiler/src/args.rs @@ -85,4 +85,7 @@ pub enum ExtraChecks { /// Check that produced values are valid except for uninitialized values. /// See https://github.com/model-checking/kani/issues/920. Validity, + /// Check that pointer is valid before casting it to reference. + /// See https://github.com/model-checking/kani/issues/2975. + PtrToRefCast, } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 86852011288a..89a50971243b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -1,6 +1,7 @@ // 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; @@ -723,13 +724,17 @@ 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); - 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, - ), - None => place_ref, + 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, + ), + None => place_ref, + } + } else { + place_ref } } Rvalue::Len(p) => self.codegen_rvalue_len(p), diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 1c8d63d6d87a..76859b58fd77 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.common_args.unstable_features.contains(UnstableFeature::PtrToRefCastChecks) { + flags.push("--ub-check=ptr_to_ref_cast".into()) + } + if self.args.ignore_locals_lifetime { flags.push("--ignore-storage-markers".into()) } diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index d7b73678a836..0b503c2d2349 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -89,6 +89,8 @@ pub enum UnstableFeature { ValidValueChecks, /// Ghost state and shadow memory APIs GhostState, + /// Pointer validity checks when casting pointer to reference. + PtrToRefCastChecks, } impl UnstableFeature { diff --git a/tests/expected/ptr_to_ref_cast/expected b/tests/expected/ptr_to_ref_cast/expected index 497141f2a5c3..85d83c067aca 100644 --- a/tests/expected/ptr_to_ref_cast/expected +++ b/tests/expected/ptr_to_ref_cast/expected @@ -2,7 +2,7 @@ Checking harness check_zst_deref... Status: FAILURE Description: "dereferencing a pointer to invalid memory location" -Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:131:35 in function zst_deref +Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:132:35 in function zst_deref VERIFICATION:- FAILED @@ -10,11 +10,11 @@ Checking harness check_equal_size_deref... Status: SUCCESS Description: "dereferencing a pointer to invalid memory location" -Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:106:31 in function equal_size_deref +Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:107:31 in function equal_size_deref Status: SUCCESS Description: "dereferencing a pointer to invalid memory location" -Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:109:38 in function equal_size_deref +Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:110:38 in function equal_size_deref VERIFICATION:- SUCCESSFUL @@ -22,11 +22,11 @@ Checking harness check_smaller_deref... Status: SUCCESS Description: "dereferencing a pointer to invalid memory location" -Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:88:31 in function smaller_deref +Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:89:31 in function smaller_deref Status: SUCCESS Description: "dereferencing a pointer to invalid memory location" -Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:92:38 in function smaller_deref +Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:93:38 in function smaller_deref VERIFICATION:- SUCCESSFUL @@ -34,7 +34,7 @@ Checking harness check_larger_deref_struct... Status: FAILURE Description: "dereferencing a pointer to invalid memory location" -Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:74:31 in function larger_deref_struct +Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:75:31 in function larger_deref_struct VERIFICATION:- FAILED @@ -42,7 +42,7 @@ Checking harness check_larger_deref_into_ptr... Status: FAILURE Description: "dereferencing a pointer to invalid memory location" -Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:48:38 in function larger_deref_into_ptr +Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:49:38 in function larger_deref_into_ptr VERIFICATION:- FAILED @@ -50,7 +50,7 @@ Checking harness check_larger_deref... Status: FAILURE Description: "dereferencing a pointer to invalid memory location" -Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:34:32 in function larger_deref +Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:35:32 in function larger_deref VERIFICATION:- FAILED @@ -58,11 +58,11 @@ Checking harness check_store... Status: FAILURE Description: "dereferencing a pointer to invalid memory location" -Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:17:28 in function Store::<'_, 3>::from +Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:18:28 in function Store::<'_, 3>::from Status: SUCCESS Description: "assertion failed: broken.data.len() == 3" -Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:26:5 in function check_store +Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:27:5 in function check_store VERIFICATION:- FAILED 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 e04ac9cd3169..3b713a34d967 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,5 +1,6 @@ // 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 9cacaa1368e3..f6e1645c3a39 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 } +unstable = { function-contracts = true, mem-predicates = true, ptr-to-ref-cast-checks = true } [package.metadata.kani.flags] output-format = "terse"