From e88fec12c34906d68416a40a5739129e21817264 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Wed, 11 Sep 2024 16:02:02 -0700
Subject: [PATCH 1/7] Instrument validity checks for pointer to reference casts
 for slices and str's

---
 .../codegen_cprover_gotoc/codegen/assert.rs   | 66 +++++++++----------
 .../codegen/intrinsic.rs                      |  8 +--
 .../codegen_cprover_gotoc/codegen/rvalue.rs   |  7 +-
 tests/expected/ptr_to_ref_cast/slice/expected |  6 ++
 tests/expected/ptr_to_ref_cast/slice/test.rs  | 36 ++++++++++
 tests/expected/ptr_to_ref_cast/str/expected   |  5 ++
 tests/expected/ptr_to_ref_cast/str/test.rs    | 16 +++++
 .../kani/Projection/slice_slice_projection.rs |  1 +
 8 files changed, 106 insertions(+), 39 deletions(-)
 create mode 100644 tests/expected/ptr_to_ref_cast/slice/expected
 create mode 100644 tests/expected/ptr_to_ref_cast/slice/test.rs
 create mode 100644 tests/expected/ptr_to_ref_cast/str/expected
 create mode 100644 tests/expected/ptr_to_ref_cast/str/test.rs

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
index 72ccb95cf97b..9c9fccc59fdf 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
@@ -23,10 +23,12 @@ use cbmc::goto_program::{Expr, Location, Stmt, Type};
 use cbmc::InternedString;
 use rustc_middle::mir::coverage::SourceRegion;
 use stable_mir::mir::{Place, ProjectionElem};
-use stable_mir::ty::{Span as SpanStable, TypeAndMut};
+use stable_mir::ty::{Span as SpanStable, Ty};
 use strum_macros::{AsRefStr, EnumString};
 use tracing::debug;
 
+use super::intrinsic::SizeAlign;
+
 /// Classifies the type of CBMC `assert`, as different assertions can have different semantics (e.g. cover)
 ///
 /// Each property class should justify its existence with a note about the special handling it recieves.
@@ -333,6 +335,8 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn codegen_raw_ptr_deref_validity_check(
         &mut self,
         place: &Place,
+        place_ref: Expr,
+        place_ref_ty: Ty,
         loc: &Location,
     ) -> Option<Stmt> {
         if let Some(ProjectionElem::Deref) = place.projection.last() {
@@ -346,41 +350,35 @@ impl<'tcx> GotocCtx<'tcx> {
             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()
-                };
+                let SizeAlign { size: sz, .. } =
+                    self.size_and_align_of_dst(place_ref_ty, place_ref);
 
+                // 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, *loc).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()), sz.clone())
+                        .cast_to(Type::Bool);
                 // __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, *loc).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);
-                }
+                let sz_typ = sz.typ().clone();
+                let raw_ptr_read_ok_expr = sz.eq(sz_typ.zero()).or(raw_ptr_read_ok_expr);
+                // 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
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 421d79e943c4..1b4c0174d5ed 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -18,9 +18,9 @@ use stable_mir::mir::{BasicBlockIdx, Operand, Place};
 use stable_mir::ty::{GenericArgs, RigidTy, Span, Ty, TyKind, UintTy};
 use tracing::debug;
 
-struct SizeAlign {
-    size: Expr,
-    align: Expr,
+pub struct SizeAlign {
+    pub size: Expr,
+    pub align: Expr,
 }
 
 enum VTableInfo {
@@ -1291,7 +1291,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// This function computes the size and alignment of a dynamically-sized type.
     /// The implementations follows closely the SSA implementation found in
     /// `rustc_codegen_ssa::glue::size_and_align_of_dst`.
-    fn size_and_align_of_dst(&mut self, ty: Ty, arg: Expr) -> SizeAlign {
+    pub fn size_and_align_of_dst(&mut self, ty: Ty, arg: Expr) -> SizeAlign {
         let layout = self.layout_of_stable(ty);
         let usizet = Type::size_t();
         if !layout.is_unsized() {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index e8f1424f09a3..694df0c37311 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -738,7 +738,12 @@ impl<'tcx> GotocCtx<'tcx> {
             Rvalue::Ref(_, _, p) | Rvalue::AddressOf(_, p) => {
                 let place_ref = self.codegen_place_ref_stable(&p, loc);
                 let place_ref_type = place_ref.typ().clone();
-                match self.codegen_raw_ptr_deref_validity_check(&p, &loc) {
+                match self.codegen_raw_ptr_deref_validity_check(
+                    &p,
+                    place_ref.clone(),
+                    self.place_ty_stable(p),
+                    &loc,
+                ) {
                     Some(ptr_validity_check_expr) => Expr::statement_expression(
                         vec![ptr_validity_check_expr, place_ref.as_stmt(loc)],
                         place_ref_type,
diff --git a/tests/expected/ptr_to_ref_cast/slice/expected b/tests/expected/ptr_to_ref_cast/slice/expected
new file mode 100644
index 000000000000..247690bb038b
--- /dev/null
+++ b/tests/expected/ptr_to_ref_cast/slice/expected
@@ -0,0 +1,6 @@
+Status: FAILURE\
+Description: "dereference failure: pointer invalid"\
+
+Verification failed for - check_with_byte_add
+Verification failed for - check_with_metadata
+Complete - 1 successfully verified harnesses, 2 failures, 3 total.
diff --git a/tests/expected/ptr_to_ref_cast/slice/test.rs b/tests/expected/ptr_to_ref_cast/slice/test.rs
new file mode 100644
index 000000000000..8526d0bf1c7f
--- /dev/null
+++ b/tests/expected/ptr_to_ref_cast/slice/test.rs
@@ -0,0 +1,36 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#![feature(set_ptr_value)]
+
+//! This test checks that Kani detects UB resulting from converting a raw
+//! pointer to a reference when the metadata is not valid.
+
+// Generate invalid fat pointer by combining the metadata.
+#[kani::proof]
+fn check_with_metadata_fail() {
+    let short = [0u32; 2];
+    let long = [0u32; 10];
+    let ptr = &short as *const [u32];
+    // This should trigger UB since the slice is not valid for the new length.
+    let fake_long = unsafe { &*ptr.with_metadata_of(&long) };
+    assert_eq!(fake_long.len(), long.len());
+}
+
+#[kani::proof]
+fn check_with_byte_add_fail() {
+    let data = [5u8; 5];
+    let ptr = &data as *const [u8];
+    // This should trigger UB since the metadata does not get adjusted.
+    let val = unsafe { &*ptr.byte_add(1) };
+    assert_eq!(val.len(), data.len());
+}
+
+#[kani::proof]
+fn check_with_byte_add_sub_pass() {
+    let data = [5u8; 5];
+    let ptr = &data as *const [u8];
+    let offset = kani::any_where(|i| *i < 100);
+    // This should pass since the resulting metadata is valid
+    let val = unsafe { &*ptr.byte_add(offset).byte_sub(offset) };
+    assert_eq!(val.len(), data.len());
+}
diff --git a/tests/expected/ptr_to_ref_cast/str/expected b/tests/expected/ptr_to_ref_cast/str/expected
new file mode 100644
index 000000000000..420f12073eae
--- /dev/null
+++ b/tests/expected/ptr_to_ref_cast/str/expected
@@ -0,0 +1,5 @@
+Status: FAILURE\
+Description: "dereference failure: pointer invalid"\
+
+VERIFICATION:- FAILED
+Verification failed for - check_with_metadata
diff --git a/tests/expected/ptr_to_ref_cast/str/test.rs b/tests/expected/ptr_to_ref_cast/str/test.rs
new file mode 100644
index 000000000000..137034e34327
--- /dev/null
+++ b/tests/expected/ptr_to_ref_cast/str/test.rs
@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#![feature(set_ptr_value)]
+
+//! This test checks that Kani detects UB resulting from converting a raw
+//! pointer to a reference when the metadata is not valid.
+
+#[kani::proof]
+fn check_with_metadata_fail() {
+    let short = "sh";
+    let long = "longer";
+    let ptr = short as *const str;
+    // This should trigger UB since the slice is not valid for the new length.
+    let fake_long = unsafe { &*ptr.with_metadata_of(long) };
+    assert_eq!(fake_long.len(), long.len());
+}
diff --git a/tests/kani/Projection/slice_slice_projection.rs b/tests/kani/Projection/slice_slice_projection.rs
index 6e1cf42af4e7..efe1f5f2d65b 100644
--- a/tests/kani/Projection/slice_slice_projection.rs
+++ b/tests/kani/Projection/slice_slice_projection.rs
@@ -1,5 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
 // kani-flags: --default-unwind 5
 
 //! This test case checks the usage of slices of slices (&[&[T]]).

From b2473698c299e5dd783dbdf611903c470845116a Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Mon, 16 Sep 2024 16:55:01 -0700
Subject: [PATCH 2/7] Fix slice test

---
 tests/kani/Projection/slice_slice_projection.rs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tests/kani/Projection/slice_slice_projection.rs b/tests/kani/Projection/slice_slice_projection.rs
index efe1f5f2d65b..350c3839cbc6 100644
--- a/tests/kani/Projection/slice_slice_projection.rs
+++ b/tests/kani/Projection/slice_slice_projection.rs
@@ -8,7 +8,8 @@ use std::mem::size_of_val;
 
 /// Structure with a raw string (i.e.: [char]).
 struct MyStr {
-    header: u16,
+    header_0: u8,
+    header_1: u8,
     data: str,
 }
 
@@ -27,7 +28,6 @@ impl MyStr {
 fn sanity_check_my_str() {
     let mut buf = String::from("123456");
     let my_str = MyStr::new(&mut buf);
-    my_str.header = 0;
 
     assert_eq!(size_of_val(my_str), 6);
     assert_eq!(my_str.data.len(), 4);
@@ -55,6 +55,6 @@ fn check_size_of_val() {
     let mut buf_1 = String::from("001");
     let my_slice = &[MyStr::new(&mut buf_0), MyStr::new(&mut buf_1)];
     assert_eq!(size_of_val(my_slice), 32); // Slice of 2 fat pointers.
-    assert_eq!(size_of_val(my_slice[0]), 4); // Size of a fat pointer.
+    assert_eq!(size_of_val(my_slice[0]), 3); // Size of a fat pointer.
     assert_eq!(size_of_val(&my_slice[0].data), 1); // Size of str.
 }

From 3ddffa57a0303bda2bfb2e697e54ecb0430a581e Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Mon, 16 Sep 2024 18:17:45 -0700
Subject: [PATCH 3/7] Update tests/kani/Projection/slice_slice_projection.rs

Remove fail flag
---
 tests/kani/Projection/slice_slice_projection.rs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/tests/kani/Projection/slice_slice_projection.rs b/tests/kani/Projection/slice_slice_projection.rs
index 350c3839cbc6..6bfa62c2f6df 100644
--- a/tests/kani/Projection/slice_slice_projection.rs
+++ b/tests/kani/Projection/slice_slice_projection.rs
@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-verify-fail
 // kani-flags: --default-unwind 5
 
 //! This test case checks the usage of slices of slices (&[&[T]]).

From 5d28fe4bf1a4256af6b4df5df8acba958c971973 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Wed, 11 Sep 2024 16:02:02 -0700
Subject: [PATCH 4/7] Instrument validity checks for pointer to reference casts
 for slices and str's

---
 .../codegen_cprover_gotoc/codegen/assert.rs   | 66 +++++++++----------
 .../codegen/intrinsic.rs                      |  8 +--
 .../codegen_cprover_gotoc/codegen/rvalue.rs   |  7 +-
 tests/expected/ptr_to_ref_cast/slice/expected |  6 ++
 tests/expected/ptr_to_ref_cast/slice/test.rs  | 36 ++++++++++
 tests/expected/ptr_to_ref_cast/str/expected   |  5 ++
 tests/expected/ptr_to_ref_cast/str/test.rs    | 16 +++++
 .../kani/Projection/slice_slice_projection.rs |  1 +
 8 files changed, 106 insertions(+), 39 deletions(-)
 create mode 100644 tests/expected/ptr_to_ref_cast/slice/expected
 create mode 100644 tests/expected/ptr_to_ref_cast/slice/test.rs
 create mode 100644 tests/expected/ptr_to_ref_cast/str/expected
 create mode 100644 tests/expected/ptr_to_ref_cast/str/test.rs

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
index 72ccb95cf97b..9c9fccc59fdf 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
@@ -23,10 +23,12 @@ use cbmc::goto_program::{Expr, Location, Stmt, Type};
 use cbmc::InternedString;
 use rustc_middle::mir::coverage::SourceRegion;
 use stable_mir::mir::{Place, ProjectionElem};
-use stable_mir::ty::{Span as SpanStable, TypeAndMut};
+use stable_mir::ty::{Span as SpanStable, Ty};
 use strum_macros::{AsRefStr, EnumString};
 use tracing::debug;
 
+use super::intrinsic::SizeAlign;
+
 /// Classifies the type of CBMC `assert`, as different assertions can have different semantics (e.g. cover)
 ///
 /// Each property class should justify its existence with a note about the special handling it recieves.
@@ -333,6 +335,8 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn codegen_raw_ptr_deref_validity_check(
         &mut self,
         place: &Place,
+        place_ref: Expr,
+        place_ref_ty: Ty,
         loc: &Location,
     ) -> Option<Stmt> {
         if let Some(ProjectionElem::Deref) = place.projection.last() {
@@ -346,41 +350,35 @@ impl<'tcx> GotocCtx<'tcx> {
             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()
-                };
+                let SizeAlign { size: sz, .. } =
+                    self.size_and_align_of_dst(place_ref_ty, place_ref);
 
+                // 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, *loc).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()), sz.clone())
+                        .cast_to(Type::Bool);
                 // __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, *loc).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);
-                }
+                let sz_typ = sz.typ().clone();
+                let raw_ptr_read_ok_expr = sz.eq(sz_typ.zero()).or(raw_ptr_read_ok_expr);
+                // 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
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 421d79e943c4..1b4c0174d5ed 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -18,9 +18,9 @@ use stable_mir::mir::{BasicBlockIdx, Operand, Place};
 use stable_mir::ty::{GenericArgs, RigidTy, Span, Ty, TyKind, UintTy};
 use tracing::debug;
 
-struct SizeAlign {
-    size: Expr,
-    align: Expr,
+pub struct SizeAlign {
+    pub size: Expr,
+    pub align: Expr,
 }
 
 enum VTableInfo {
@@ -1291,7 +1291,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// This function computes the size and alignment of a dynamically-sized type.
     /// The implementations follows closely the SSA implementation found in
     /// `rustc_codegen_ssa::glue::size_and_align_of_dst`.
-    fn size_and_align_of_dst(&mut self, ty: Ty, arg: Expr) -> SizeAlign {
+    pub fn size_and_align_of_dst(&mut self, ty: Ty, arg: Expr) -> SizeAlign {
         let layout = self.layout_of_stable(ty);
         let usizet = Type::size_t();
         if !layout.is_unsized() {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index e8f1424f09a3..694df0c37311 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -738,7 +738,12 @@ impl<'tcx> GotocCtx<'tcx> {
             Rvalue::Ref(_, _, p) | Rvalue::AddressOf(_, p) => {
                 let place_ref = self.codegen_place_ref_stable(&p, loc);
                 let place_ref_type = place_ref.typ().clone();
-                match self.codegen_raw_ptr_deref_validity_check(&p, &loc) {
+                match self.codegen_raw_ptr_deref_validity_check(
+                    &p,
+                    place_ref.clone(),
+                    self.place_ty_stable(p),
+                    &loc,
+                ) {
                     Some(ptr_validity_check_expr) => Expr::statement_expression(
                         vec![ptr_validity_check_expr, place_ref.as_stmt(loc)],
                         place_ref_type,
diff --git a/tests/expected/ptr_to_ref_cast/slice/expected b/tests/expected/ptr_to_ref_cast/slice/expected
new file mode 100644
index 000000000000..247690bb038b
--- /dev/null
+++ b/tests/expected/ptr_to_ref_cast/slice/expected
@@ -0,0 +1,6 @@
+Status: FAILURE\
+Description: "dereference failure: pointer invalid"\
+
+Verification failed for - check_with_byte_add
+Verification failed for - check_with_metadata
+Complete - 1 successfully verified harnesses, 2 failures, 3 total.
diff --git a/tests/expected/ptr_to_ref_cast/slice/test.rs b/tests/expected/ptr_to_ref_cast/slice/test.rs
new file mode 100644
index 000000000000..8526d0bf1c7f
--- /dev/null
+++ b/tests/expected/ptr_to_ref_cast/slice/test.rs
@@ -0,0 +1,36 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#![feature(set_ptr_value)]
+
+//! This test checks that Kani detects UB resulting from converting a raw
+//! pointer to a reference when the metadata is not valid.
+
+// Generate invalid fat pointer by combining the metadata.
+#[kani::proof]
+fn check_with_metadata_fail() {
+    let short = [0u32; 2];
+    let long = [0u32; 10];
+    let ptr = &short as *const [u32];
+    // This should trigger UB since the slice is not valid for the new length.
+    let fake_long = unsafe { &*ptr.with_metadata_of(&long) };
+    assert_eq!(fake_long.len(), long.len());
+}
+
+#[kani::proof]
+fn check_with_byte_add_fail() {
+    let data = [5u8; 5];
+    let ptr = &data as *const [u8];
+    // This should trigger UB since the metadata does not get adjusted.
+    let val = unsafe { &*ptr.byte_add(1) };
+    assert_eq!(val.len(), data.len());
+}
+
+#[kani::proof]
+fn check_with_byte_add_sub_pass() {
+    let data = [5u8; 5];
+    let ptr = &data as *const [u8];
+    let offset = kani::any_where(|i| *i < 100);
+    // This should pass since the resulting metadata is valid
+    let val = unsafe { &*ptr.byte_add(offset).byte_sub(offset) };
+    assert_eq!(val.len(), data.len());
+}
diff --git a/tests/expected/ptr_to_ref_cast/str/expected b/tests/expected/ptr_to_ref_cast/str/expected
new file mode 100644
index 000000000000..420f12073eae
--- /dev/null
+++ b/tests/expected/ptr_to_ref_cast/str/expected
@@ -0,0 +1,5 @@
+Status: FAILURE\
+Description: "dereference failure: pointer invalid"\
+
+VERIFICATION:- FAILED
+Verification failed for - check_with_metadata
diff --git a/tests/expected/ptr_to_ref_cast/str/test.rs b/tests/expected/ptr_to_ref_cast/str/test.rs
new file mode 100644
index 000000000000..137034e34327
--- /dev/null
+++ b/tests/expected/ptr_to_ref_cast/str/test.rs
@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#![feature(set_ptr_value)]
+
+//! This test checks that Kani detects UB resulting from converting a raw
+//! pointer to a reference when the metadata is not valid.
+
+#[kani::proof]
+fn check_with_metadata_fail() {
+    let short = "sh";
+    let long = "longer";
+    let ptr = short as *const str;
+    // This should trigger UB since the slice is not valid for the new length.
+    let fake_long = unsafe { &*ptr.with_metadata_of(long) };
+    assert_eq!(fake_long.len(), long.len());
+}
diff --git a/tests/kani/Projection/slice_slice_projection.rs b/tests/kani/Projection/slice_slice_projection.rs
index 6e1cf42af4e7..efe1f5f2d65b 100644
--- a/tests/kani/Projection/slice_slice_projection.rs
+++ b/tests/kani/Projection/slice_slice_projection.rs
@@ -1,5 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
 // kani-flags: --default-unwind 5
 
 //! This test case checks the usage of slices of slices (&[&[T]]).

From 3e345519b759ece3cbb98a01e84a191da5b4c7a6 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Tue, 17 Sep 2024 10:40:17 -0700
Subject: [PATCH 5/7] Add the previously failing test as an expected test

---
 .../expected/ptr_to_ref_cast/invalid/expected |  8 +++
 .../expected/ptr_to_ref_cast/invalid/test.rs  | 58 +++++++++++++++++++
 2 files changed, 66 insertions(+)
 create mode 100644 tests/expected/ptr_to_ref_cast/invalid/expected
 create mode 100644 tests/expected/ptr_to_ref_cast/invalid/test.rs

diff --git a/tests/expected/ptr_to_ref_cast/invalid/expected b/tests/expected/ptr_to_ref_cast/invalid/expected
new file mode 100644
index 000000000000..df4b8143d2aa
--- /dev/null
+++ b/tests/expected/ptr_to_ref_cast/invalid/expected
@@ -0,0 +1,8 @@
+MyStr::new.safety_check\
+Status: FAILURE\
+Description: "dereference failure: pointer invalid"\
+in function MyStr::new
+
+Verification failed for - check_size_of_val
+Verification failed for - check_slice_my_str
+Complete - 1 successfully verified harnesses, 2 failures, 3 total.
diff --git a/tests/expected/ptr_to_ref_cast/invalid/test.rs b/tests/expected/ptr_to_ref_cast/invalid/test.rs
new file mode 100644
index 000000000000..50d2c8dd05e8
--- /dev/null
+++ b/tests/expected/ptr_to_ref_cast/invalid/test.rs
@@ -0,0 +1,58 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test case checks the usage of slices of slices (&[&[T]]).
+use std::mem::size_of_val;
+
+/// Structure with a raw string (i.e.: [char]).
+struct MyStr {
+    header: u16,
+    data: str,
+}
+
+impl MyStr {
+    /// This creates a MyStr from a byte slice.
+    fn new(original: &mut String) -> &mut Self {
+        let buf = original.get_mut(..).unwrap();
+        assert!(size_of_val(buf) > 2, "This requires at least 2 bytes");
+        let unsized_len = buf.len() - 2;
+        let ptr = std::ptr::slice_from_raw_parts_mut(buf.as_mut_ptr(), unsized_len);
+        unsafe { &mut *(ptr as *mut Self) }
+    }
+}
+
+#[kani::proof]
+fn sanity_check_my_str() {
+    let mut buf = String::from("123456");
+    let my_str = MyStr::new(&mut buf);
+    my_str.header = 0;
+
+    assert_eq!(size_of_val(my_str), 6);
+    assert_eq!(my_str.data.len(), 4);
+    assert_eq!(my_str.data.chars().nth(0), Some('3'));
+    assert_eq!(my_str.data.chars().nth(3), Some('6'));
+}
+
+#[kani::proof]
+fn check_slice_my_str() {
+    let mut buf_0 = String::from("000");
+    let mut buf_1 = String::from("001");
+    let my_slice = &[MyStr::new(&mut buf_0), MyStr::new(&mut buf_1)];
+    assert_eq!(my_slice.len(), 2);
+
+    assert_eq!(my_slice[0].data.len(), 1);
+    assert_eq!(my_slice[1].data.len(), 1);
+
+    assert_eq!(my_slice[0].data.chars().nth(0), Some('0'));
+    assert_eq!(my_slice[1].data.chars().nth(0), Some('1'));
+}
+
+#[kani::proof]
+fn check_size_of_val() {
+    let mut buf_0 = String::from("000");
+    let mut buf_1 = String::from("001");
+    let my_slice = &[MyStr::new(&mut buf_0), MyStr::new(&mut buf_1)];
+    assert_eq!(size_of_val(my_slice), 32); // Slice of 2 fat pointers.
+    assert_eq!(size_of_val(my_slice[0]), 4); // Size of a fat pointer.
+    assert_eq!(size_of_val(&my_slice[0].data), 1); // Size of str.
+}

From e1dd44af944e7090839855405ebd1d7ae57f1b49 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Tue, 17 Sep 2024 11:25:50 -0700
Subject: [PATCH 6/7] Re-remove kani-verify-fail

---
 tests/kani/Projection/slice_slice_projection.rs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/tests/kani/Projection/slice_slice_projection.rs b/tests/kani/Projection/slice_slice_projection.rs
index 350c3839cbc6..6bfa62c2f6df 100644
--- a/tests/kani/Projection/slice_slice_projection.rs
+++ b/tests/kani/Projection/slice_slice_projection.rs
@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-verify-fail
 // kani-flags: --default-unwind 5
 
 //! This test case checks the usage of slices of slices (&[&[T]]).

From 47811273c88689757db0f5a03b80518430b0a6c8 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Tue, 17 Sep 2024 15:09:19 -0700
Subject: [PATCH 7/7] Add alignment checks

---
 .../codegen_cprover_gotoc/codegen/assert.rs   | 13 +++++++++---
 .../codegen_cprover_gotoc/codegen/rvalue.rs   | 16 ++++++++++-----
 .../ptr_to_ref_cast/alignment/expected        |  4 ++++
 .../ptr_to_ref_cast/alignment/test.rs         | 20 +++++++++++++++++++
 tests/expected/ptr_to_ref_cast/slice/expected |  4 ++--
 tests/expected/ptr_to_ref_cast/str/expected   |  2 +-
 6 files changed, 48 insertions(+), 11 deletions(-)
 create mode 100644 tests/expected/ptr_to_ref_cast/alignment/expected
 create mode 100644 tests/expected/ptr_to_ref_cast/alignment/test.rs

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
index 9c9fccc59fdf..c81d60e40d42 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
@@ -338,7 +338,7 @@ impl<'tcx> GotocCtx<'tcx> {
         place_ref: Expr,
         place_ref_ty: Ty,
         loc: &Location,
-    ) -> Option<Stmt> {
+    ) -> Option<(Stmt, Stmt)> {
         if let Some(ProjectionElem::Deref) = place.projection.last() {
             // Create a place without the topmost dereference projection.ß
             let ptr_place = {
@@ -350,7 +350,7 @@ impl<'tcx> GotocCtx<'tcx> {
             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 SizeAlign { size: sz, .. } =
+                let SizeAlign { size: sz, align } =
                     self.size_and_align_of_dst(place_ref_ty, place_ref);
 
                 // Encode __CPROVER_r_ok(ptr, size).
@@ -364,6 +364,13 @@ impl<'tcx> GotocCtx<'tcx> {
                         ptr_projection.goto_expr().clone().member("data", &self.symbol_table)
                     }
                 };
+                // Then generate an alignment check
+                let align_ok =
+                    ptr.clone().cast_to(Type::size_t()).rem(align).eq(Type::size_t().zero());
+                let align_check = self.codegen_assert_assume(align_ok, PropertyClass::SafetyCheck,
+                    "misaligned pointer to reference cast: address must be a multiple of its type's \
+                    alignment", *loc);
+
                 // Then, generate a __CPROVER_r_ok check.
                 let raw_ptr_read_ok_expr =
                     Expr::read_ok(ptr.cast_to(Type::void_pointer()), sz.clone())
@@ -378,7 +385,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     "dereference failure: pointer invalid",
                     *loc,
                 );
-                return Some(raw_ptr_read_ok);
+                return Some((align_check, raw_ptr_read_ok));
             }
         }
         None
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index 694df0c37311..7abd949357ff 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -744,11 +744,17 @@ impl<'tcx> GotocCtx<'tcx> {
                     self.place_ty_stable(p),
                     &loc,
                 ) {
-                    Some(ptr_validity_check_expr) => Expr::statement_expression(
-                        vec![ptr_validity_check_expr, place_ref.as_stmt(loc)],
-                        place_ref_type,
-                        loc,
-                    ),
+                    Some((ptr_alignment_check_expr, ptr_validity_check_expr)) => {
+                        Expr::statement_expression(
+                            vec![
+                                ptr_alignment_check_expr,
+                                ptr_validity_check_expr,
+                                place_ref.as_stmt(loc),
+                            ],
+                            place_ref_type,
+                            loc,
+                        )
+                    }
                     None => place_ref,
                 }
             }
diff --git a/tests/expected/ptr_to_ref_cast/alignment/expected b/tests/expected/ptr_to_ref_cast/alignment/expected
new file mode 100644
index 000000000000..c7d8f5109e21
--- /dev/null
+++ b/tests/expected/ptr_to_ref_cast/alignment/expected
@@ -0,0 +1,4 @@
+check_misaligned_ptr_cast_fail.safety_check\
+Status: FAILURE\
+Description: "misaligned pointer to reference cast: address must be a multiple of its type's alignment"\
+in function check_misaligned_ptr_cast_fail
diff --git a/tests/expected/ptr_to_ref_cast/alignment/test.rs b/tests/expected/ptr_to_ref_cast/alignment/test.rs
new file mode 100644
index 000000000000..5e0a18a79da7
--- /dev/null
+++ b/tests/expected/ptr_to_ref_cast/alignment/test.rs
@@ -0,0 +1,20 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks that Kani detects UB resulting from converting a raw
+//! pointer to a reference when the pointer is not properly aligned.
+
+#[repr(align(4))]
+#[derive(Clone, Copy)]
+struct AlignedI32(i32);
+
+#[kani::proof]
+fn check_misaligned_ptr_cast_fail() {
+    let data = AlignedI32(42);
+    let ptr = &data as *const AlignedI32;
+
+    unsafe {
+        let misaligned = ptr.byte_add(1);
+        let x = unsafe { &*misaligned };
+    }
+}
diff --git a/tests/expected/ptr_to_ref_cast/slice/expected b/tests/expected/ptr_to_ref_cast/slice/expected
index 247690bb038b..8a8b39f8594e 100644
--- a/tests/expected/ptr_to_ref_cast/slice/expected
+++ b/tests/expected/ptr_to_ref_cast/slice/expected
@@ -1,6 +1,6 @@
 Status: FAILURE\
 Description: "dereference failure: pointer invalid"\
 
-Verification failed for - check_with_byte_add
-Verification failed for - check_with_metadata
+Verification failed for - check_with_byte_add_fail
+Verification failed for - check_with_metadata_fail
 Complete - 1 successfully verified harnesses, 2 failures, 3 total.
diff --git a/tests/expected/ptr_to_ref_cast/str/expected b/tests/expected/ptr_to_ref_cast/str/expected
index 420f12073eae..e2de069eb399 100644
--- a/tests/expected/ptr_to_ref_cast/str/expected
+++ b/tests/expected/ptr_to_ref_cast/str/expected
@@ -2,4 +2,4 @@ Status: FAILURE\
 Description: "dereference failure: pointer invalid"\
 
 VERIFICATION:- FAILED
-Verification failed for - check_with_metadata
+Verification failed for - check_with_metadata_fail