Add alignment checks

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

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,
                 }
             }

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

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 };
+    }
+}

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.

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