Make Kani reject mutable pointer casts if padding is incompatible and memory initialization is checked (#3332)

This PR introduces layout checks for types to instrument mutable pointer
casts. If two types have incompatible padding (e.g. a padding byte in
one is a data byte in the other or vice-versa), an "unsupported check"
assertion is inserted. This overapproximates for soundness, since the
casts do not cause UB themselves, but an alternative solution involves
tracking every MIR place, which is costly.

Resolves #3324

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: artemagvanian

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

@@ -12,9 +12,11 @@ use stable_mir::mir::{
     NonDivergingIntrinsic, Operand, Place, PointerCoercion, ProjectionElem, Rvalue, Statement,
     StatementKind, Terminator, TerminatorKind,
 };
-use stable_mir::ty::{ConstantKind, MirConst, RigidTy, Span, TyKind, UintTy};
+use stable_mir::ty::{ConstantKind, MirConst, RigidTy, Span, Ty, TyKind, UintTy};
 use strum_macros::AsRefStr;
 
+use super::{PointeeInfo, PointeeLayout};
+
 /// Memory initialization operations: set or get memory initialization state for a given pointer.
 #[derive(AsRefStr, Clone, Debug)]
 pub enum MemoryInitOp {
@@ -540,13 +542,34 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
     }
 
     fn visit_rvalue(&mut self, rvalue: &Rvalue, location: Location) {
-        if let Rvalue::Cast(CastKind::PointerCoercion(PointerCoercion::Unsize), _, ty) = rvalue {
-            if let TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) = ty.kind() {
-                if pointee_ty.kind().is_trait() {
-                    self.push_target(MemoryInitOp::Unsupported {
-                        reason: "Kani does not support reasoning about memory initialization of unsized pointers.".to_string(),
-                    });
+        if let Rvalue::Cast(cast_kind, operand, ty) = rvalue {
+            match cast_kind {
+                CastKind::PointerCoercion(PointerCoercion::Unsize) => {
+                    if let TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) = ty.kind() {
+                        if pointee_ty.kind().is_trait() {
+                            self.push_target(MemoryInitOp::Unsupported {
+                                reason: "Kani does not support reasoning about memory initialization of unsized pointers.".to_string(),
+                            });
+                        }
+                    }
                 }
+                CastKind::PtrToPtr => {
+                    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(),
+                            });
+                        }
+                    }
+                }
+                _ => {}
             }
         };
         self.super_rvalue(rvalue, location);
@@ -711,3 +734,36 @@ fn try_resolve_instance(locals: &[LocalDecl], func: &Operand) -> Result<Instance
         )),
     }
 }
+
+/// Returns true if `to_ty` has a smaller or equal size and the same padding bytes as `from_ty` up until
+/// its size.
+fn tys_layout_compatible(from_ty: &Ty, to_ty: &Ty) -> bool {
+    // Retrieve layouts to assess compatibility.
+    let from_ty_info = PointeeInfo::from_ty(*from_ty);
+    let to_ty_info = PointeeInfo::from_ty(*to_ty);
+    if let (Ok(from_ty_info), Ok(to_ty_info)) = (from_ty_info, to_ty_info) {
+        let from_ty_layout = match from_ty_info.layout() {
+            PointeeLayout::Sized { layout } => layout,
+            PointeeLayout::Slice { element_layout } => element_layout,
+            PointeeLayout::TraitObject => return false,
+        };
+        let to_ty_layout = match to_ty_info.layout() {
+            PointeeLayout::Sized { layout } => layout,
+            PointeeLayout::Slice { element_layout } => element_layout,
+            PointeeLayout::TraitObject => return false,
+        };
+        // Ensure `to_ty_layout` does not have a larger size.
+        if to_ty_layout.len() <= from_ty_layout.len() {
+            // Check data and padding bytes pair-wise.
+            if from_ty_layout.iter().zip(to_ty_layout.iter()).all(
+                |(from_ty_layout_byte, to_ty_layout_byte)| {
+                    // Make sure all data and padding bytes match.
+                    from_ty_layout_byte == to_ty_layout_byte
+                },
+            ) {
+                return true;
+            }
+        }
+    };
+    false
+}

tests/expected/uninit/access-padding-via-cast/expected

@@ -1,4 +1,4 @@
-Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*mut [u8; 4]`
+Failed Checks: Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB.
 
 VERIFICATION:- FAILED
 

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

@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z ghost-state -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 value as *mut _ as *mut (u8, u32, u64);
+        *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/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.