Put the extra check behind an unstable feature flag

model-checking · Jun 5, 2024 · 5120b02 · 5120b02
1 parent 4561d35
commit 5120b02
Show file tree

Hide file tree

Showing 7 changed files with 33 additions and 18 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -2,67 +2,67 @@ 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
 
 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
 
 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
 
 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
 
 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
 
 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
 
 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
@@ -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
@@ -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"