Mitigate invalid transmute when checking memory initialization

kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs

@@ -581,6 +581,29 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
                         }
                     }
                 }
+                CastKind::Transmute => {
+                    let operand_ty = operand.ty(&self.locals).unwrap();
+                    if let (
+                        RigidTy::RawPtr(from_ty, Mutability::Mut),
+                        RigidTy::RawPtr(to_ty, Mutability::Mut),
+                    ) = (operand_ty.kind().rigid().unwrap(), ty.kind().rigid().unwrap())
+                    {
+                        if !tys_layout_compatible(from_ty, to_ty) {
+                            // If casting from a mutable pointer to a mutable pointer with different
+                            // layouts, delayed UB could occur.
+                            self.push_target(MemoryInitOp::Unsupported {
+                                reason: "Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB.".to_string(),
+                            });
+                        }
+                    } else if !tys_layout_compatible(&operand_ty, &ty) {
+                        // If transmuting between two types of incompatible layouts, padding
+                        // bytes are exposed, which is UB.
+                        self.push_target(MemoryInitOp::Unsupported {
+                            reason: "Transmuting between types of incompatible layouts."
+                                .to_string(),
+                        });
+                    }
+                }
                 _ => {}
             }
         };

tests/expected/uninit/delayed-ub-transmute/delayed-ub-transmute.rs

@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z uninit-checks
+
+/// Checks that Kani rejects mutable pointer casts between types of different padding.
+#[kani::proof]
+fn invalid_value() {
+    unsafe {
+        let mut value: u128 = 0;
+        let ptr: *mut (u8, u32, u64) = std::mem::transmute(&mut value as *mut _);
+        *ptr = (4, 4, 4); // This assignment itself does not cause UB...
+        let c: u128 = value; // ...but this reads a padding value!
+    }
+}

tests/expected/uninit/delayed-ub-transmute/expected

@@ -0,0 +1,5 @@
+Failed Checks: Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB.
+
+VERIFICATION:- FAILED
+
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.

tests/expected/uninit/transmute-padding/expected

@@ -0,0 +1,5 @@
+Failed Checks: Transmuting between types of incompatible layouts.
+
+VERIFICATION:- FAILED
+
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.

tests/expected/uninit/transmute-padding/transmute_padding.rs

@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z uninit-checks
+
+// 5 bytes of data + 3 bytes of padding.
+#[repr(C)]
+#[derive(kani::Arbitrary)]
+struct S(u32, u8);
+
+/// Checks that Kani catches an attempt to access padding of a struct using transmute.
+#[kani::proof]
+fn check_uninit_padding() {
+    let s = kani::any();
+    access_padding(s);
+}
+
+fn access_padding(s: S) {
+    let _padding: u64 = unsafe { std::mem::transmute(s) }; // ~ERROR: padding bytes are uninitialized, so reading them is UB.
+}