Skip analyzing pointers to trait objects for now

kani-compiler/src/kani_middle/transform/body.rs

@@ -123,21 +123,6 @@ impl MutableBody {
         self.new_assignment(rvalue, where_to, insert_position)
     }
 
-    /// Transmute to a raw pointer of `*mut type` and return a new local where that value is stored.
-    pub fn new_cast_transmute(
-        &mut self,
-        from: Operand,
-        pointee_ty: Ty,
-        mutability: Mutability,
-        where_to: &mut SourceInstruction,
-        insert_position: InsertPosition,
-    ) -> Local {
-        assert!(from.ty(self.locals()).unwrap().kind().is_raw_ptr());
-        let target_ty = Ty::new_ptr(pointee_ty, mutability);
-        let rvalue = Rvalue::Cast(CastKind::Transmute, from, target_ty);
-        self.new_assignment(rvalue, where_to, insert_position)
-    }
-
     /// Add a new assignment for the given binary operation.
     ///
     /// Return the local where the result is saved.

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

@@ -94,11 +94,7 @@ impl UninitPass {
         let mut source = instruction.source;
         for operation in operations {
             match &operation {
-                SourceOp::Unsupported { unsupported_instruction, place } => {
-                    let place_ty = place.ty(body.locals()).unwrap();
-                    let reason = format!(
-                        "Kani currently doesn't support checking memory initialization using instruction `{unsupported_instruction}` for type `{place_ty}`",
-                    );
+                SourceOp::Unsupported { reason } => {
                     self.unsupported_check(tcx, body, &mut source, operation.position(), &reason);
                     continue;
                 }
@@ -174,20 +170,7 @@ impl UninitPass {
                             )
                             .unwrap()
                         }
-                        TyKind::RigidTy(RigidTy::Dynamic(..)) => Instance::resolve(
-                            find_fn_def(tcx, "KaniShadowMemoryGetDynamic").unwrap(),
-                            &GenericArgs(vec![
-                                GenericArgKind::Const(
-                                    Const::try_from_uint(
-                                        type_layout.as_byte_layout().len() as u128,
-                                        UintTy::Usize,
-                                    )
-                                    .unwrap(),
-                                ),
-                                GenericArgKind::Type(pointee_ty),
-                            ]),
-                        )
-                        .unwrap(),
+                        TyKind::RigidTy(RigidTy::Dynamic(..)) => continue, // Any layout is valid when dereferencing a pointer to `dyn Trait`.
                         _ => Instance::resolve(
                             find_fn_def(tcx, "KaniShadowMemoryGet").unwrap(),
                             &GenericArgs(vec![
@@ -249,20 +232,7 @@ impl UninitPass {
                             )
                             .unwrap()
                         }
-                        TyKind::RigidTy(RigidTy::Dynamic(..)) => Instance::resolve(
-                            find_fn_def(tcx, "KaniShadowMemorySetDynamic").unwrap(),
-                            &GenericArgs(vec![
-                                GenericArgKind::Const(
-                                    Const::try_from_uint(
-                                        type_layout.as_byte_layout().len() as u128,
-                                        UintTy::Usize,
-                                    )
-                                    .unwrap(),
-                                ),
-                                GenericArgKind::Type(pointee_ty),
-                            ]),
-                        )
-                        .unwrap(),
+                        TyKind::RigidTy(RigidTy::Dynamic(..)) => continue, // Any layout is valid when dereferencing a pointer to `dyn Trait`.
                         _ => Instance::resolve(
                             find_fn_def(tcx, "KaniShadowMemorySet").unwrap(),
                             &GenericArgs(vec![

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

@@ -36,7 +36,7 @@ impl TypeLayout {
                     offset: 0,
                     size: match ty.layout().unwrap().shape().fields {
                         FieldsShape::Array { stride, count } if count == 0 => stride,
-                        _ => MachineSize::from_bits(8),
+                        _ => MachineSize::from_bits(0),
                     },
                 };
                 let ty_size = data_bytes.size.bytes();

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

@@ -3,8 +3,9 @@ use stable_mir::mir::alloc::GlobalAlloc;
 use stable_mir::mir::mono::{Instance, InstanceKind};
 use stable_mir::mir::visit::{Location, PlaceContext};
 use stable_mir::mir::{
-    BasicBlockIdx, Constant, LocalDecl, MirVisitor, Mutability, NonDivergingIntrinsic, Operand,
-    Place, ProjectionElem, Rvalue, Statement, StatementKind, Terminator, TerminatorKind,
+    BasicBlockIdx, CastKind, Constant, LocalDecl, MirVisitor, Mutability, NonDivergingIntrinsic,
+    Operand, Place, PointerCoercion, ProjectionElem, Rvalue, Statement, StatementKind, Terminator,
+    TerminatorKind,
 };
 use stable_mir::ty::{Const, ConstantKind, RigidTy, Span, TyKind, UintTy};
 use strum_macros::AsRefStr;
@@ -15,7 +16,7 @@ pub enum SourceOp {
     Set { place: Place, count: Operand, value: bool },
     BlessConst { constant: Constant, count: Operand, value: bool },
     BlessRef { place: Place, count: Operand, value: bool },
-    Unsupported { place: Place, unsupported_instruction: String },
+    Unsupported { reason: String },
 }
 
 impl SourceOp {
@@ -109,14 +110,14 @@ fn try_remove_topmost_deref(place: &Place) -> Option<Place> {
     }
 }
 
-/// Retrieve instance for the given function operand.
-///
-/// This will panic if the operand is not a function or if it cannot be resolved.
-fn expect_instance(locals: &[LocalDecl], func: &Operand) -> Instance {
+/// Try retrieving instance for the given function operand.
+fn try_resolve_instance(locals: &[LocalDecl], func: &Operand) -> Result<Instance, String> {
     let ty = func.ty(locals).unwrap();
     match ty.kind() {
-        TyKind::RigidTy(RigidTy::FnDef(def, args)) => Instance::resolve(def, &args).unwrap(),
-        _ => unreachable!(),
+        TyKind::RigidTy(RigidTy::FnDef(def, args)) => Ok(Instance::resolve(def, &args).unwrap()),
+        _ => Err(format!(
+            "Kani does not support reasoning about memory initialization of arguments to `{ty:?}`."
+        )),
     }
 }
 
@@ -225,7 +226,14 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
             match &term.kind {
                 TerminatorKind::Call { func, args, destination, .. } => {
                     self.super_terminator(term, location);
-                    let instance = expect_instance(self.locals, func);
+                    let instance = match try_resolve_instance(self.locals, func) {
+                        Ok(instance) => instance,
+                        Err(reason) => {
+                            self.super_terminator(term, location);
+                            self.push_target(SourceOp::Unsupported { reason });
+                            return;
+                        }
+                    };
                     match instance.kind {
                         InstanceKind::Intrinsic => {
                             match instance.intrinsic_name().unwrap().as_str() {
@@ -354,8 +362,7 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
                         && (!ptx.is_mutating() || place.projection.len() > idx + 1)
                     {
                         self.push_target(SourceOp::Unsupported {
-                            unsupported_instruction: "union access".to_string(),
-                            place: intermediate_place.clone(),
+                            reason: "Kani does not support reasoning about memory initialization of unions.".to_string(),
                         });
                     }
                 }
@@ -398,4 +405,16 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
         }
         self.super_operand(operand, location);
     }
+
+    fn visit_rvalue(&mut self, rvalue: &Rvalue, location: Location) {
+        match rvalue {
+            Rvalue::Cast(CastKind::PointerCoercion(PointerCoercion::Unsize), _, _) => {
+                self.push_target(SourceOp::Unsupported {
+                    reason: "Kani does not support reasoning about memory initialization of unsized pointers.".to_string(),
+                });
+            }
+            _ => {}
+        };
+        self.super_rvalue(rvalue, location);
+    }
 }

library/kani/src/shadow.rs

@@ -27,8 +27,6 @@
 //! }
 //! ```
 
-use std::ptr::DynMetadata;
-
 const MAX_NUM_OBJECTS: usize = 1024;
 const MAX_OBJECT_SIZE: usize = 64;
 
@@ -177,32 +175,3 @@ pub fn __kani_global_sm_set_slice<const N: usize, T: ?Sized>(
     let n = n * meta;
     __kani_global_sm_set_inner(ptr, layout, n, value);
 }
-
-// This method should only be called if T is known to be a trait object.
-#[rustc_diagnostic_item = "KaniShadowMemoryGetDynamic"]
-pub fn __kani_global_sm_get_dynamic<const N: usize, T: ?Sized>(
-    ptr: *const T,
-    layout: [bool; N],
-    n: usize,
-) -> bool {
-    let (ptr, meta) = ptr.to_raw_parts();
-    let meta: DynMetadata<T> = unsafe { std::mem::transmute_copy(&meta) };
-    // The pointee type is a dyn Trait, more than `n` objects can be accessed.
-    let n = n * meta.size_of();
-    __kani_global_sm_get_inner(ptr, layout, n)
-}
-
-// This method should only be called if T is known to be a trait object.
-#[rustc_diagnostic_item = "KaniShadowMemorySetDynamic"]
-pub fn __kani_global_sm_set_dynamic<const N: usize, T: ?Sized>(
-    ptr: *const T,
-    layout: [bool; N],
-    n: usize,
-    value: bool,
-) {
-    let (ptr, meta) = ptr.to_raw_parts();
-    let meta: DynMetadata<T> = unsafe { std::mem::transmute_copy(&meta) };
-    // The pointee type is a slice, more than `n` objects can be accessed.
-    let n = n * meta.size_of();
-    __kani_global_sm_set_inner(ptr, layout, n, value);
-}