Mitigate invalid transmute when checking memory initialization

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

@@ -142,9 +142,11 @@ impl UninitPass {
         operation: MemoryInitOp,
         skip_first: &mut HashSet<usize>,
     ) {
-        if let MemoryInitOp::Unsupported { reason } = &operation {
+        if let MemoryInitOp::Unsupported { reason } | MemoryInitOp::TriviallyUnsafe { reason } =
+            &operation
+        {
             collect_skipped(&operation, body, skip_first);
-            self.unsupported_check(tcx, body, source, operation.position(), reason);
+            self.inject_assert_false(tcx, body, source, operation.position(), reason);
             return;
         };
 
@@ -166,7 +168,7 @@ impl UninitPass {
                         "Kani currently doesn't support checking memory initialization for pointers to `{pointee_ty}.",
                     );
                     collect_skipped(&operation, body, skip_first);
-                    self.unsupported_check(tcx, body, source, operation.position(), &reason);
+                    self.inject_assert_false(tcx, body, source, operation.position(), &reason);
                     return;
                 }
             }
@@ -181,7 +183,7 @@ impl UninitPass {
             | MemoryInitOp::SetRef { .. } => {
                 self.build_set(tcx, body, source, operation, pointee_ty_info, skip_first)
             }
-            MemoryInitOp::Unsupported { .. } => {
+            MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => {
                 unreachable!()
             }
         }
@@ -266,7 +268,7 @@ impl UninitPass {
             PointeeLayout::TraitObject => {
                 collect_skipped(&operation, body, skip_first);
                 let reason = "Kani does not support reasoning about memory initialization of pointers to trait objects.";
-                self.unsupported_check(tcx, body, source, operation.position(), reason);
+                self.inject_assert_false(tcx, body, source, operation.position(), reason);
                 return;
             }
         };
@@ -392,7 +394,7 @@ impl UninitPass {
         };
     }
 
-    fn unsupported_check(
+    fn inject_assert_false(
         &self,
         tcx: TyCtxt,
         body: &mut MutableBody,

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

@@ -37,6 +37,8 @@ pub enum MemoryInitOp {
     SetRef { operand: Operand, value: bool, position: InsertPosition },
     /// Unsupported memory initialization operation.
     Unsupported { reason: String },
+    /// Operation that trivially accesses uninitialized memory, results in injecting `assert!(false)`.
+    TriviallyUnsafe { reason: String },
 }
 
 impl MemoryInitOp {
@@ -63,7 +65,9 @@ impl MemoryInitOp {
                 },
                 projection: vec![],
             }),
-            MemoryInitOp::Unsupported { .. } => unreachable!(),
+            MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => {
+                unreachable!()
+            }
         }
     }
 
@@ -74,7 +78,8 @@ impl MemoryInitOp {
             MemoryInitOp::Check { .. }
             | MemoryInitOp::Set { .. }
             | MemoryInitOp::SetRef { .. }
-            | MemoryInitOp::Unsupported { .. } => unreachable!(),
+            | MemoryInitOp::Unsupported { .. }
+            | MemoryInitOp::TriviallyUnsafe { .. } => unreachable!(),
         }
     }
 
@@ -85,7 +90,8 @@ impl MemoryInitOp {
             | MemoryInitOp::SetRef { value, .. } => *value,
             MemoryInitOp::Check { .. }
             | MemoryInitOp::CheckSliceChunk { .. }
-            | MemoryInitOp::Unsupported { .. } => unreachable!(),
+            | MemoryInitOp::Unsupported { .. }
+            | MemoryInitOp::TriviallyUnsafe { .. } => unreachable!(),
         }
     }
 
@@ -96,7 +102,8 @@ impl MemoryInitOp {
             | MemoryInitOp::SetRef { position, .. } => *position,
             MemoryInitOp::Check { .. }
             | MemoryInitOp::CheckSliceChunk { .. }
-            | MemoryInitOp::Unsupported { .. } => InsertPosition::Before,
+            | MemoryInitOp::Unsupported { .. }
+            | MemoryInitOp::TriviallyUnsafe { .. } => InsertPosition::Before,
         }
     }
 }
@@ -581,6 +588,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::TriviallyUnsafe {
+                            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.
+}