Systematic ptr/ref transmute handling

kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs

@@ -4,7 +4,7 @@
 //! This module contains the visitor responsible for collecting initial analysis targets for delayed
 //! UB instrumentation.
 
-use crate::kani_middle::transform::check_uninit::ty_layout::tys_layout_compatible;
+use crate::kani_middle::transform::check_uninit::ty_layout::tys_layout_equal_to_size;
 use stable_mir::{
     mir::{
         alloc::GlobalAlloc,
@@ -66,12 +66,18 @@ impl MirVisitor for InitialTargetVisitor {
             let operand_ty = operand.ty(self.body.locals()).unwrap();
             match kind {
                 CastKind::Transmute | CastKind::PtrToPtr => {
-                    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) {
+                    let operand_ty_kind = operand_ty.kind();
+                    let from_ty = match operand_ty_kind.rigid().unwrap() {
+                        RigidTy::RawPtr(ty, _) | RigidTy::Ref(_, ty, _) => Some(ty),
+                        _ => None,
+                    };
+                    let ty_kind = ty.kind();
+                    let to_ty = match ty_kind.rigid().unwrap() {
+                        RigidTy::RawPtr(ty, _) | RigidTy::Ref(_, ty, _) => Some(ty),
+                        _ => None,
+                    };
+                    if let (Some(from_ty), Some(to_ty)) = (from_ty, to_ty) {
+                        if !tys_layout_equal_to_size(from_ty, to_ty) {
                             self.push_operand(operand);
                         }
                     }

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

@@ -7,7 +7,7 @@ use crate::kani_middle::transform::{
     body::{InsertPosition, MutableBody, SourceInstruction},
     check_uninit::{
         relevant_instruction::{InitRelevantInstruction, MemoryInitOp},
-        ty_layout::tys_layout_compatible,
+        ty_layout::tys_layout_compatible_to_size,
         TargetFinder,
     },
 };
@@ -477,14 +477,37 @@ impl MirVisitor for CheckUninitVisitor {
                     }
                 }
                 CastKind::Transmute => {
-                    let operand_ty = operand.ty(&&self.locals).unwrap();
-                    if !tys_layout_compatible(&operand_ty, &ty) {
+                    let operand_ty = operand.ty(&self.locals).unwrap();
+                    if !tys_layout_compatible_to_size(&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(),
                         });
+                    } else if let (
+                        TyKind::RigidTy(RigidTy::Ref(_, from_ty, _)),
+                        TyKind::RigidTy(RigidTy::Ref(_, to_ty, _)),
+                    ) = (operand_ty.kind(), ty.kind())
+                    {
+                        if !tys_layout_compatible_to_size(&from_ty, &to_ty) {
+                            // Since references are supposed to always be initialized for its type,
+                            // transmuting between two references of incompatible layout is UB.
+                            self.push_target(MemoryInitOp::TriviallyUnsafe {
+                                reason: "Transmuting between references pointing to types of incompatible layouts."
+                                    .to_string(),
+                            });
+                        }
+                    } else if let (
+                        TyKind::RigidTy(RigidTy::RawPtr(from_ty, _)),
+                        TyKind::RigidTy(RigidTy::Ref(_, to_ty, _)),
+                    ) = (operand_ty.kind(), ty.kind())
+                    {
+                        // Assert that we can only cast this way if types are the same.
+                        assert!(from_ty == to_ty);
+                        // When transmuting from a raw pointer to a reference, need to check that
+                        // the value pointed by the raw pointer is initialized.
+                        self.push_target(MemoryInitOp::Check { operand: operand.clone() });
                     }
                 }
                 _ => {}

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

@@ -335,9 +335,21 @@ fn data_bytes_for_ty(
     }
 }
 
-/// Returns true if `to_ty` has a smaller or equal size and the same padding bytes as `from_ty` up until
-/// its size.
-pub fn tys_layout_compatible(from_ty: &Ty, to_ty: &Ty) -> bool {
+/// Returns true if `to_ty` has a smaller or equal size and padding bytes in `from_ty` are padding
+/// bytes in `to_ty`.
+pub fn tys_layout_compatible_to_size(from_ty: &Ty, to_ty: &Ty) -> bool {
+    tys_layout_cmp_to_size(from_ty, to_ty, |from_byte, to_byte| from_byte || !to_byte)
+}
+
+/// Returns true if `to_ty` has a smaller or equal size and padding bytes in `from_ty` are padding
+/// bytes in `to_ty`.
+pub fn tys_layout_equal_to_size(from_ty: &Ty, to_ty: &Ty) -> bool {
+    tys_layout_cmp_to_size(from_ty, to_ty, |from_byte, to_byte| from_byte == to_byte)
+}
+
+/// Returns true if `to_ty` has a smaller or equal size and comparator function returns true for all
+/// byte initialization value pairs up to size.
+fn tys_layout_cmp_to_size(from_ty: &Ty, to_ty: &Ty, cmp: impl Fn(bool, bool) -> bool) -> bool {
     // Retrieve layouts to assess compatibility.
     let from_ty_info = PointeeInfo::from_ty(*from_ty);
     let to_ty_info = PointeeInfo::from_ty(*to_ty);
@@ -357,8 +369,8 @@ pub fn tys_layout_compatible(from_ty: &Ty, to_ty: &Ty) -> bool {
             // 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
+                    // Run comparator on each pair.
+                    cmp(*from_ty_layout_byte, *to_ty_layout_byte)
                 },
             ) {
                 return true;