Inject pointer validity check when casting raw pointers to references

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 pointer validity when casting pointers to references.
+    /// See https://github.com/model-checking/kani/issues/2975.
+    PtrToRefCast,
 }

kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs

@@ -21,7 +21,8 @@
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{Expr, Location, Stmt, Type};
 use cbmc::InternedString;
-use stable_mir::ty::Span as SpanStable;
+use stable_mir::mir::{Place, ProjectionElem};
+use stable_mir::ty::{Span as SpanStable, TypeAndMut};
 use strum_macros::{AsRefStr, EnumString};
 use tracing::debug;
 
@@ -323,4 +324,63 @@ impl<'tcx> GotocCtx<'tcx> {
 
         self.codegen_assert_assume(cond, PropertyClass::SanityCheck, &assert_msg, loc)
     }
+
+    /// If converting a raw pointer to a reference, &(*ptr), need to inject
+    /// a check to make sure that the pointer points to a valid memory location,
+    /// since dereferencing an invalid pointer is UB in Rust.
+    pub fn codegen_raw_ptr_deref_validity_check(
+        &mut self,
+        place: &Place,
+        loc: &Location,
+    ) -> Option<Stmt> {
+        if let Some(ProjectionElem::Deref) = place.projection.last() {
+            // Create a place without the topmost dereference projection.ß
+            let ptr_place = {
+                let mut ptr_place = place.clone();
+                ptr_place.projection.pop();
+                ptr_place
+            };
+            // Only inject the check if dereferencing a raw pointer.
+            let ptr_place_ty = self.place_ty_stable(&ptr_place);
+            if ptr_place_ty.kind().is_raw_ptr() {
+                // Extract the size of the pointee.
+                let pointee_size = {
+                    let TypeAndMut { ty: pointee_ty, .. } =
+                        ptr_place_ty.kind().builtin_deref(true).unwrap();
+                    let pointee_ty_layout = pointee_ty.layout().unwrap();
+                    pointee_ty_layout.shape().size.bytes()
+                };
+
+                // __CPROVER_r_ok fails if size == 0, so need to explicitly avoid the check.
+                if pointee_size != 0 {
+                    // Encode __CPROVER_r_ok(ptr, size).
+                    // First, generate a CBMC expression representing the pointer.
+                    let ptr = {
+                        let ptr_projection = self.codegen_place_stable(&ptr_place).unwrap();
+                        let place_ty = self.place_ty_stable(place);
+                        if self.use_thin_pointer_stable(place_ty) {
+                            ptr_projection.goto_expr().clone()
+                        } else {
+                            ptr_projection.goto_expr().clone().member("data", &self.symbol_table)
+                        }
+                    };
+                    // Then, generate a __CPROVER_r_ok check.
+                    let raw_ptr_read_ok_expr = Expr::read_ok(
+                        ptr.cast_to(Type::void_pointer()),
+                        Expr::int_constant(pointee_size, Type::size_t()),
+                    )
+                    .cast_to(Type::Bool);
+                    // Finally, assert that the pointer points to a valid memory location.
+                    let raw_ptr_read_ok = self.codegen_assert(
+                        raw_ptr_read_ok_expr,
+                        PropertyClass::SafetyCheck,
+                        "dereference failure: pointer invalid",
+                        *loc,
+                    );
+                    return Some(raw_ptr_read_ok);
+                }
+            }
+        }
+        None
+    }
 }

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;
@@ -721,7 +722,21 @@ impl<'tcx> GotocCtx<'tcx> {
         match rv {
             Rvalue::Use(p) => self.codegen_operand_stable(p),
             Rvalue::Repeat(op, sz) => self.codegen_rvalue_repeat(op, sz, loc),
-            Rvalue::Ref(_, _, p) | Rvalue::AddressOf(_, p) => self.codegen_place_ref_stable(&p),
+            Rvalue::Ref(_, _, p) | Rvalue::AddressOf(_, p) => {
+                let place_ref = self.codegen_place_ref_stable(&p);
+                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),
             // Rust has begun distinguishing "ptr -> num" and "num -> ptr" (providence-relevant casts) but we do not yet:
             // Should we? Tracking ticket: https://github.com/model-checking/kani/issues/1274

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

@@ -337,6 +337,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 Stmt::skip(loc)
             }
             InstanceKind::Shim => {
+                // Since the reference is used right away here, no need to inject a check for pointer validity.
                 let place_ref = self.codegen_place_ref_stable(place);
                 match place_ty.kind() {
                     TyKind::RigidTy(RigidTy::Dynamic(..)) => {

kani-driver/src/call_single_file.rs

@@ -139,6 +139,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())
         }

kani_metadata/src/unstable.rs

@@ -89,6 +89,8 @@ pub enum UnstableFeature {
     ValidValueChecks,
     /// Ghost state and shadow memory APIs.
     GhostState,
+    /// Automatically check that pointers are valid when casting them to references.
+    PtrToRefCastChecks,
     /// Enable an unstable option or subcommand.
     UnstableOptions,
 }

tests/expected/ptr_to_ref_cast/expected

@@ -0,0 +1,75 @@
+Checking harness check_zst_deref...
+
+Status: FAILURE\
+Description: "dereference failure: pointer invalid"\
+in function zst_deref
+
+VERIFICATION:- FAILED
+
+Checking harness check_equal_size_deref...
+
+Status: SUCCESS\
+Description: "dereference failure: pointer invalid"\
+in function equal_size_deref
+
+Status: SUCCESS\
+Description: "dereference failure: pointer invalid"\
+in function equal_size_deref
+
+VERIFICATION:- SUCCESSFUL
+
+Checking harness check_smaller_deref...
+
+Status: SUCCESS\
+Description: "dereference failure: pointer invalid"\
+in function smaller_deref
+
+Status: SUCCESS\
+Description: "dereference failure: pointer invalid"\
+in function smaller_deref
+
+VERIFICATION:- SUCCESSFUL
+
+Checking harness check_larger_deref_struct...
+
+Status: FAILURE\
+Description: "dereference failure: pointer invalid"\
+in function larger_deref_struct
+
+VERIFICATION:- FAILED
+
+Checking harness check_larger_deref_into_ptr...
+
+Status: FAILURE\
+Description: "dereference failure: pointer invalid"\
+in function larger_deref_into_ptr
+
+VERIFICATION:- FAILED
+
+Checking harness check_larger_deref...
+
+Status: FAILURE\
+Description: "dereference failure: pointer invalid"\
+in function larger_deref
+
+VERIFICATION:- FAILED
+
+Checking harness check_store...
+
+Status: FAILURE\
+Description: "dereference failure: pointer invalid"\
+in function Store::<'_, 3>::from
+
+Status: SUCCESS\
+Description: "assertion failed: broken.data.len() == 3"\
+in function check_store
+
+VERIFICATION:- FAILED
+
+Summary:
+Verification failed for - check_zst_deref
+Verification failed for - check_larger_deref_struct
+Verification failed for - check_larger_deref_into_ptr
+Verification failed for - check_larger_deref
+Verification failed for - check_store
+Complete - 2 successfully verified harnesses, 5 failures, 7 total.

tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs

@@ -0,0 +1,140 @@
+// 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).
+
+// 1. Original example.
+
+struct Store<'a, const LEN: usize> {
+    data: [&'a i128; LEN],
+}
+
+impl<'a, const LEN: usize> Store<'a, LEN> {
+    pub fn from(var: &i64) -> Self {
+        let ref1: *const i64 = var;
+        let ref2: *const i128 = ref1 as *const i128;
+        unsafe {
+            Store { data: [&*ref2; LEN] } // ---- THIS LINE SHOULD FAIL
+        }
+    }
+}
+
+#[kani::proof]
+pub fn check_store() {
+    let val = 1;
+    let broken = Store::<3>::from(&val);
+    assert_eq!(broken.data.len(), 3)
+}
+
+// 2. Make sure the error is raised when casting to a simple type of a larger size.
+
+pub fn larger_deref(var: &i64) {
+    let ref1: *const i64 = var;
+    let ref2: *const i128 = ref1 as *const i128;
+    let ref3: &i128 = unsafe { &*ref2 }; // ---- THIS LINE SHOULD FAIL
+}
+
+#[kani::proof]
+pub fn check_larger_deref() {
+    let var: i64 = kani::any();
+    larger_deref(&var);
+}
+
+// 3. Make sure the error is raised when casting to a simple type of a larger size and storing the result in a pointer.
+
+pub fn larger_deref_into_ptr(var: &i64) {
+    let ref1: *const i64 = var;
+    let ref2: *const i128 = ref1 as *const i128;
+    let ref3: *const i128 = unsafe { &*ref2 }; // ---- THIS LINE SHOULD FAIL
+}
+
+#[kani::proof]
+pub fn check_larger_deref_into_ptr() {
+    let var: i64 = kani::any();
+    larger_deref_into_ptr(&var);
+}
+
+// 4. Make sure the error is raised when casting to a struct of a larger size.
+
+#[derive(kani::Arbitrary)]
+struct Foo {
+    a: u8,
+}
+
+#[derive(kani::Arbitrary)]
+struct Bar {
+    a: u8,
+    b: u64,
+    c: u64,
+}
+
+pub fn larger_deref_struct(var: &Foo) {
+    let ref1: *const Foo = var;
+    let ref2: *const Bar = ref1 as *const Bar;
+    let ref3: &Bar = unsafe { &*ref2 }; // ---- THIS LINE SHOULD FAIL
+}
+
+#[kani::proof]
+pub fn check_larger_deref_struct() {
+    let var: Foo = kani::any();
+    larger_deref_struct(&var);
+}
+
+// 5. Make sure the error is not raised if the target size is smaller.
+
+pub fn smaller_deref(var: &i64, var_struct: &Bar) {
+    let ref1: *const i64 = var;
+    let ref2: *const i32 = ref1 as *const i32;
+    let ref3: &i32 = unsafe { &*ref2 };
+
+    let ref1_struct: *const Bar = var_struct;
+    let ref2_struct: *const Foo = ref1_struct as *const Foo;
+    let ref3_struct: &Foo = unsafe { &*ref2_struct };
+}
+
+#[kani::proof]
+pub fn check_smaller_deref() {
+    let var: i64 = kani::any();
+    let var_struct: Bar = kani::any();
+    smaller_deref(&var, &var_struct);
+}
+
+// 6. Make sure the error is not raised if the target size is the same.
+
+pub fn equal_size_deref(var: &i64, var_struct: &Foo) {
+    let ref1: *const i64 = var;
+    let ref2: &i64 = unsafe { &*ref1 };
+
+    let ref1_struct: *const Foo = var_struct;
+    let ref2_struct: &Foo = unsafe { &*ref1_struct };
+}
+
+#[kani::proof]
+pub fn check_equal_size_deref() {
+    let var: i64 = kani::any();
+    let var_struct: Foo = kani::any();
+    equal_size_deref(&var, &var_struct);
+}
+
+// 7. Make sure the check works with ZSTs.
+
+#[derive(kani::Arbitrary)]
+struct Zero;
+
+pub fn zst_deref(var_struct: &Foo, var_zst: &Zero) {
+    let ref1_struct: *const Foo = var_struct;
+    let ref2_struct: *const Zero = ref1_struct as *const Zero;
+    let ref3_struct: &Zero = unsafe { &*ref2_struct };
+
+    let ref1_zst: *const Zero = var_zst;
+    let ref2_zst: *const Foo = ref1_zst as *const Foo;
+    let ref3_zst: &Foo = unsafe { &*ref2_zst }; // ---- THIS LINE SHOULD FAIL
+}
+
+#[kani::proof]
+pub fn check_zst_deref() {
+    let var_struct: Foo = kani::any();
+    let var_zst: Zero = kani::any();
+    zst_deref(&var_struct, &var_zst);
+}

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"

tests/std-checks/core/ptr.expected

@@ -1,3 +1,4 @@
 Summary:
 Verification failed for - ptr::verify::check_replace_unit
-Complete - 5 successfully verified harnesses, 1 failures, 6 total.
+Verification failed for - ptr::verify::check_as_ref_dangling
+Complete - 4 successfully verified harnesses, 2 failures, 6 total.