From eb05f74e62b56889da93ccf13131a8c715a14298 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Sat, 17 Aug 2024 12:23:10 -0700 Subject: [PATCH] Stop using visitor for instrumentation target finding --- .../delayed_ub/instrumentation_visitor.rs | 201 +++++++++-- .../kani_middle/transform/check_uninit/mod.rs | 14 +- .../check_uninit/ptr_uninit/uninit_visitor.rs | 323 +++++++++++------- 3 files changed, 373 insertions(+), 165 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs index f6354b827c37..3ede2988f143 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs @@ -16,9 +16,8 @@ use crate::kani_middle::{ }; use rustc_middle::ty::TyCtxt; use stable_mir::mir::{ - mono::Instance, - visit::{Location, PlaceContext}, - BasicBlock, MirVisitor, Operand, Place, Rvalue, + mono::Instance, BasicBlock, CopyNonOverlapping, InlineAsmOperand, NonDivergingIntrinsic, + Operand, Place, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, }; use std::collections::HashSet; @@ -33,6 +32,13 @@ pub struct InstrumentationVisitor<'a, 'tcx> { tcx: TyCtxt<'tcx>, } +enum PlaceOperation { + Read, + Write, + Deinit, + Noop, +} + impl<'a, 'tcx> TargetFinder for InstrumentationVisitor<'a, 'tcx> { fn find_next( &mut self, @@ -44,14 +50,11 @@ impl<'a, 'tcx> TargetFinder for InstrumentationVisitor<'a, 'tcx> { SourceInstruction::Statement { idx, bb } => { let BasicBlock { statements, .. } = &body.blocks()[bb]; let stmt = &statements[idx]; - self.visit_statement(stmt, self.__location_hack_remove_before_merging(stmt.span)) + self.check_statement(stmt) } SourceInstruction::Terminator { bb } => { let BasicBlock { terminator, .. } = &body.blocks()[bb]; - self.visit_terminator( - terminator, - self.__location_hack_remove_before_merging(terminator.span), - ) + self.check_terminator(terminator) } } self.target.clone() @@ -76,17 +79,152 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> { } } -impl<'a, 'tcx> MirVisitor for InstrumentationVisitor<'a, 'tcx> { - fn visit_rvalue(&mut self, rvalue: &Rvalue, location: Location) { +impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> { + fn check_statement(&mut self, stmt: &Statement) { + let Statement { kind, .. } = stmt; + match kind { + StatementKind::Assign(place, rvalue) => { + self.check_place(place, PlaceOperation::Write); + self.check_rvalue(rvalue); + } + StatementKind::FakeRead(_, place) => { + // According to the compiler docs, "When executed at runtime this is a nop." For + // more info, see + // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.StatementKind.html#variant.FakeRead, + self.check_place(place, PlaceOperation::Noop); + } + StatementKind::SetDiscriminant { place, .. } => { + self.check_place(place, PlaceOperation::Write); + } + StatementKind::Deinit(place) => { + self.check_place(place, PlaceOperation::Deinit); + } + StatementKind::Retag(_, place) => { + // According to the compiler docs, "These statements are currently only interpreted + // by miri and only generated when -Z mir-emit-retag is passed." For more info, see + // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.StatementKind.html#variant.Retag, + self.check_place(place, PlaceOperation::Noop); + } + StatementKind::PlaceMention(place) => { + // According to the compiler docs, "When executed at runtime, this computes the + // given place, but then discards it without doing a load." For more info, see + // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.StatementKind.html#variant.PlaceMention, + self.check_place(place, PlaceOperation::Noop); + } + StatementKind::AscribeUserType { place, .. } => { + // According to the compiler docs, "When executed at runtime this is a nop." For + // more info, see + // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.StatementKind.html#variant.AscribeUserType, + self.check_place(place, PlaceOperation::Noop); + } + + StatementKind::Intrinsic(intrisic) => match intrisic { + NonDivergingIntrinsic::Assume(operand) => { + self.check_operand(operand); + } + NonDivergingIntrinsic::CopyNonOverlapping(CopyNonOverlapping { + src, + dst, + count, + }) => { + self.check_operand(src); + self.check_operand(dst); + self.check_operand(count); + } + }, + StatementKind::StorageLive(_) + | StatementKind::StorageDead(_) + | StatementKind::Coverage(_) + | StatementKind::ConstEvalCounter + | StatementKind::Nop => {} + } + } + + fn check_terminator(&mut self, term: &Terminator) { + let Terminator { kind, .. } = term; + match kind { + TerminatorKind::Goto { .. } + | TerminatorKind::Resume + | TerminatorKind::Abort + | TerminatorKind::Unreachable + | TerminatorKind::Return => {} + TerminatorKind::Assert { cond, .. } => { + self.check_operand(cond); + } + TerminatorKind::Drop { place, .. } => { + // According to the documentation, "After drop elaboration: Drop terminators are a + // complete nop for types that have no drop glue. For other types, Drop terminators + // behave exactly like a call to core::mem::drop_in_place with a pointer to the + // given place." Since we check arguments when instrumenting function calls, perhaps + // we need to check that one, too. For more info, see: + // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.TerminatorKind.html#variant.Drop + self.check_place(place, PlaceOperation::Read); + } + TerminatorKind::Call { func, args, destination, target: _, unwind: _ } => { + self.check_operand(func); + for arg in args { + self.check_operand(arg); + } + self.check_place(destination, PlaceOperation::Write); + } + TerminatorKind::InlineAsm { operands, .. } => { + for op in operands { + let InlineAsmOperand { in_value, out_place, raw_rpr: _ } = op; + if let Some(input) = in_value { + self.check_operand(input); + } + if let Some(output) = out_place { + self.check_place(output, PlaceOperation::Write); + } + } + } + TerminatorKind::SwitchInt { discr, .. } => { + self.check_operand(discr); + } + } + } + + fn check_rvalue(&mut self, rvalue: &Rvalue) { match rvalue { - Rvalue::AddressOf(..) | Rvalue::Ref(..) => { - // These operations are always legitimate for us. + Rvalue::AddressOf(_, place) | Rvalue::Ref(_, _, place) => { + self.check_place(place, PlaceOperation::Noop); + } + Rvalue::Aggregate(_, operands) => { + for op in operands { + self.check_operand(op); + } + } + Rvalue::BinaryOp(_, lhs, rhs) | Rvalue::CheckedBinaryOp(_, lhs, rhs) => { + self.check_operand(lhs); + self.check_operand(rhs); + } + Rvalue::Cast(_, op, _) + | Rvalue::Repeat(op, _) + | Rvalue::ShallowInitBox(op, ..) + | Rvalue::UnaryOp(_, op) + | Rvalue::Use(op) => { + self.check_operand(op); + } + Rvalue::CopyForDeref(place) | Rvalue::Discriminant(place) | Rvalue::Len(place) => { + self.check_place(place, PlaceOperation::Read); + } + Rvalue::ThreadLocalRef(..) | Rvalue::NullaryOp(..) => {} + } + } + + fn check_operand(&mut self, operand: &Operand) { + match operand { + Operand::Copy(place) | Operand::Move(place) => { + self.check_place(place, PlaceOperation::Read) + } + Operand::Constant(_) => { + // Those should be safe to skip, as they are either constants or statics. In the + // latter case, we handle them in regular uninit visior } - _ => self.super_rvalue(rvalue, location), } } - fn visit_place(&mut self, place: &Place, ptx: PlaceContext, location: Location) { + fn check_place(&mut self, place: &Place, place_operation: PlaceOperation) { // Match the place by whatever it is pointing to and find an intersection with the targets. if self .points_to @@ -95,18 +233,31 @@ impl<'a, 'tcx> MirVisitor for InstrumentationVisitor<'a, 'tcx> { .next() .is_some() { - // If we are mutating the place, initialize it. - if ptx.is_mutating() { - self.push_target(MemoryInitOp::SetRef { - operand: Operand::Copy(place.clone()), - value: true, - position: InsertPosition::After, - }); - } else { - // Otherwise, check its initialization. - self.push_target(MemoryInitOp::CheckRef { operand: Operand::Copy(place.clone()) }); + match place_operation { + PlaceOperation::Write => { + // If we are mutating the place, initialize it. + self.push_target(MemoryInitOp::SetRef { + operand: Operand::Copy(place.clone()), + value: true, + position: InsertPosition::After, + }) + } + PlaceOperation::Deinit => { + // If we are mutating the place, initialize it. + self.push_target(MemoryInitOp::SetRef { + operand: Operand::Copy(place.clone()), + value: false, + position: InsertPosition::After, + }) + } + PlaceOperation::Read => { + // Otherwise, check its initialization. + self.push_target(MemoryInitOp::CheckRef { + operand: Operand::Copy(place.clone()), + }); + } + PlaceOperation::Noop => {} } } - self.super_place(place, ptx, location) } } diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs index 95e15a21fba0..50b640cfcb54 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -13,12 +13,10 @@ use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use stable_mir::{ mir::{ - mono::Instance, visit::Location, AggregateKind, BasicBlock, Body, ConstOperand, Mutability, - Operand, Place, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, UnwindAction, - }, - ty::{ - FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Span, Ty, TyConst, TyKind, UintTy, + mono::Instance, AggregateKind, BasicBlock, Body, ConstOperand, Mutability, Operand, Place, + Rvalue, Statement, StatementKind, Terminator, TerminatorKind, UnwindAction, }, + ty::{FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Ty, TyConst, TyKind, UintTy}, CrateDef, }; use std::collections::HashMap; @@ -39,12 +37,6 @@ pub trait TargetFinder { body: &MutableBody, source: &SourceInstruction, ) -> Option; - - /// TODO: This is just a temporary fix to unblock me because I couldn't create Location - /// directly. Perhaps we need to make a change in StableMIR to allow creating Location. - fn __location_hack_remove_before_merging(&self, span: Span) -> Location { - unsafe { std::mem::transmute(span) } - } } // Function bodies of those functions will not be instrumented as not to cause infinite recursion. diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs index 9f6b2a881e71..d6d125aeeb79 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs @@ -18,10 +18,9 @@ use stable_mir::{ mir::{ alloc::GlobalAlloc, mono::{Instance, InstanceKind}, - visit::{Location, PlaceContext}, - BasicBlock, CastKind, LocalDecl, MirVisitor, NonDivergingIntrinsic, Operand, Place, - PointerCoercion, ProjectionElem, Rvalue, Statement, StatementKind, Terminator, - TerminatorKind, + BasicBlock, CastKind, CopyNonOverlapping, InlineAsmOperand, LocalDecl, + NonDivergingIntrinsic, Operand, Place, PointerCoercion, ProjectionElem, Rvalue, Statement, + StatementKind, Terminator, TerminatorKind, }, ty::{ConstantKind, RigidTy, TyKind}, }; @@ -44,14 +43,11 @@ impl TargetFinder for CheckUninitVisitor { SourceInstruction::Statement { idx, bb } => { let BasicBlock { statements, .. } = &body.blocks()[bb]; let stmt = &statements[idx]; - self.visit_statement(stmt, self.__location_hack_remove_before_merging(stmt.span)) + self.check_statement(stmt) } SourceInstruction::Terminator { bb } => { let BasicBlock { terminator, .. } = &body.blocks()[bb]; - self.visit_terminator( - terminator, - self.__location_hack_remove_before_merging(terminator.span), - ) + self.check_terminator(terminator) } } self.target.clone() @@ -72,23 +68,28 @@ impl CheckUninitVisitor { } } -impl MirVisitor for CheckUninitVisitor { - fn visit_statement(&mut self, stmt: &Statement, location: Location) { +impl CheckUninitVisitor { + /// Check the statement and find all potential instrumentation targets. + fn check_statement(&mut self, stmt: &Statement) { // Leave it as an exhaustive match to be notified when a new kind is added. match &stmt.kind { - StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping(copy)) => { - self.super_statement(stmt, location); + StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping( + CopyNonOverlapping { src, dst, count }, + )) => { + self.check_operand(src); + self.check_operand(dst); + self.check_operand(count); // The copy is untyped, so we should copy memory initialization state from `src` // to `dst`. self.push_target(MemoryInitOp::Copy { - from: copy.src.clone(), - to: copy.dst.clone(), - count: copy.count.clone(), + from: src.clone(), + to: dst.clone(), + count: count.clone(), }); } StatementKind::Assign(place, rvalue) => { // First check rvalue. - self.visit_rvalue(rvalue, location); + self.check_rvalue(rvalue); // Check whether we are assigning into a dereference (*ptr = _). if let Some(place_without_deref) = try_remove_topmost_deref(place) { // First, check that we are not dereferencing extra pointers along the way @@ -99,8 +100,8 @@ impl MirVisitor for CheckUninitVisitor { // If the projection is Deref and the current type is raw pointer, check // if it points to initialized memory. if *projection_elem == ProjectionElem::Deref { - if let TyKind::RigidTy(RigidTy::RawPtr(..)) = - place_to_add_projections.ty(&&self.locals).unwrap().kind() + if let TyKind::RigidTy(RigidTy::RawPtr(_, _)) = + place_to_add_projections.ty(&self.locals).unwrap().kind() { self.push_target(MemoryInitOp::Check { operand: Operand::Copy(place_to_add_projections.clone()), @@ -109,7 +110,7 @@ impl MirVisitor for CheckUninitVisitor { } place_to_add_projections.projection.push(projection_elem.clone()); } - if place_without_deref.ty(&&self.locals).unwrap().kind().is_raw_ptr() { + if place_without_deref.ty(&self.locals).unwrap().kind().is_raw_ptr() { self.push_target(MemoryInitOp::Set { operand: Operand::Copy(place_without_deref), value: true, @@ -118,8 +119,8 @@ impl MirVisitor for CheckUninitVisitor { } } // Check whether Rvalue creates a new initialized pointer previously not captured inside shadow memory. - if place.ty(&&self.locals).unwrap().kind().is_raw_ptr() { - if let Rvalue::AddressOf(..) = rvalue { + if place.ty(&self.locals).unwrap().kind().is_raw_ptr() { + if let Rvalue::AddressOf(_, _) = rvalue { self.push_target(MemoryInitOp::Set { operand: Operand::Copy(place.clone()), value: true, @@ -129,36 +130,44 @@ impl MirVisitor for CheckUninitVisitor { } } StatementKind::Deinit(place) => { - self.super_statement(stmt, location); + self.check_place(place); self.push_target(MemoryInitOp::Set { operand: Operand::Copy(place.clone()), value: false, position: InsertPosition::After, }); } - StatementKind::FakeRead(_, _) - | StatementKind::SetDiscriminant { .. } - | StatementKind::StorageLive(_) + StatementKind::FakeRead(_, place) + | StatementKind::SetDiscriminant { place, .. } + | StatementKind::Retag(_, place) + | StatementKind::PlaceMention(place) + | StatementKind::AscribeUserType { place, .. } => { + self.check_place(place); + } + StatementKind::Intrinsic(NonDivergingIntrinsic::Assume(operand)) => { + self.check_operand(operand); + } + StatementKind::StorageLive(_) | StatementKind::StorageDead(_) - | StatementKind::Retag(_, _) - | StatementKind::PlaceMention(_) - | StatementKind::AscribeUserType { .. } | StatementKind::Coverage(_) | StatementKind::ConstEvalCounter - | StatementKind::Intrinsic(NonDivergingIntrinsic::Assume(_)) - | StatementKind::Nop => self.super_statement(stmt, location), + | StatementKind::Nop => {} } } - fn visit_terminator(&mut self, term: &Terminator, location: Location) { + /// Check the terminator and find all potential instrumentation targets. + fn check_terminator(&mut self, term: &Terminator) { // Leave it as an exhaustive match to be notified when a new kind is added. match &term.kind { TerminatorKind::Call { func, args, destination, .. } => { - self.super_terminator(term, location); + self.check_operand(func); + for arg in args { + self.check_operand(arg); + } + self.check_place(destination); let instance = match try_resolve_instance(&self.locals, func) { Ok(instance) => instance, Err(reason) => { - self.super_terminator(term, location); self.push_target(MemoryInitOp::Unsupported { reason }); return; } @@ -277,20 +286,20 @@ impl MirVisitor for CheckUninitVisitor { } } TerminatorKind::Drop { place, .. } => { - self.super_terminator(term, location); - let place_ty = place.ty(&&self.locals).unwrap(); + self.check_place(place); + let place_ty = place.ty(&self.locals).unwrap(); // When drop is codegen'ed for types that could define their own dropping // behavior, a reference is taken to the place which is later implicitly coerced // to a pointer. Hence, we need to bless this pointer as initialized. match place - .ty(&&self.locals) + .ty(&self.locals) .unwrap() .kind() .rigid() .expect("should be working with monomorphized code") { - RigidTy::Adt(..) | RigidTy::Dynamic(_, _, _) => { + RigidTy::Adt(_, _) | RigidTy::Dynamic(_, _, _) => { self.push_target(MemoryInitOp::SetRef { operand: Operand::Copy(place.clone()), value: true, @@ -309,121 +318,177 @@ impl MirVisitor for CheckUninitVisitor { } } TerminatorKind::Goto { .. } - | TerminatorKind::SwitchInt { .. } | TerminatorKind::Resume | TerminatorKind::Abort | TerminatorKind::Return - | TerminatorKind::Unreachable - | TerminatorKind::Assert { .. } - | TerminatorKind::InlineAsm { .. } => self.super_terminator(term, location), - } - } - - fn visit_place(&mut self, place: &Place, ptx: PlaceContext, location: Location) { - for (idx, elem) in place.projection.iter().enumerate() { - let intermediate_place = - Place { local: place.local, projection: place.projection[..idx].to_vec() }; - match elem { - ProjectionElem::Deref => { - let ptr_ty = intermediate_place.ty(&self.locals).unwrap(); - if ptr_ty.kind().is_raw_ptr() { - self.push_target(MemoryInitOp::Check { - operand: Operand::Copy(intermediate_place.clone()), - }); + | TerminatorKind::Unreachable => {} + TerminatorKind::SwitchInt { discr, .. } => { + self.check_operand(discr); + } + TerminatorKind::Assert { cond, .. } => { + self.check_operand(cond); + } + TerminatorKind::InlineAsm { operands, .. } => { + for op in operands { + let InlineAsmOperand { in_value, out_place, raw_rpr: _ } = op; + if let Some(input) = in_value { + self.check_operand(input); } - } - ProjectionElem::Field(idx, target_ty) => { - if target_ty.kind().is_union() - && (!ptx.is_mutating() || place.projection.len() > idx + 1) - { - self.push_target(MemoryInitOp::Unsupported { - reason: "Kani does not support reasoning about memory initialization of unions.".to_string(), - }); + if let Some(output) = out_place { + self.check_place(output); } } - ProjectionElem::Index(_) - | ProjectionElem::ConstantIndex { .. } - | ProjectionElem::Subslice { .. } => { - /* For a slice to be indexed, it should be valid first. */ - } - ProjectionElem::Downcast(_) => {} - ProjectionElem::OpaqueCast(_) => {} - ProjectionElem::Subtype(_) => {} } } - self.super_place(place, ptx, location) } - fn visit_operand(&mut self, operand: &Operand, location: Location) { - if let Operand::Constant(constant) = operand { - if let ConstantKind::Allocated(allocation) = constant.const_.kind() { - for (_, prov) in &allocation.provenance.ptrs { - if let GlobalAlloc::Static(_) = GlobalAlloc::from(prov.0) { - if constant.ty().kind().is_raw_ptr() { - // If a static is a raw pointer, need to mark it as initialized. - self.push_target(MemoryInitOp::Set { - operand: Operand::Constant(constant.clone()), - value: true, - position: InsertPosition::Before, - }); - } - }; + /// Check the rvalue and find all potential instrumentation targets. + fn check_rvalue(&mut self, rvalue: &Rvalue) { + match rvalue { + Rvalue::Aggregate(_, operands) => { + for op in operands { + self.check_operand(op); } } - } - self.super_operand(operand, location); - } - - fn visit_rvalue(&mut self, rvalue: &Rvalue, location: Location) { - 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 { + Rvalue::BinaryOp(_, lhs, rhs) | Rvalue::CheckedBinaryOp(_, lhs, rhs) => { + self.check_operand(lhs); + self.check_operand(rhs); + } + Rvalue::AddressOf(_, place) + | Rvalue::CopyForDeref(place) + | Rvalue::Discriminant(place) + | Rvalue::Len(place) + | Rvalue::Ref(_, _, place) => { + self.check_place(place); + } + Rvalue::ShallowInitBox(op, _) + | Rvalue::UnaryOp(_, op) + | Rvalue::Use(op) + | Rvalue::Repeat(op, _) => { + self.check_operand(op); + } + Rvalue::NullaryOp(_, _) | Rvalue::ThreadLocalRef(_) => {} + Rvalue::Cast(cast_kind, op, ty) => { + self.check_operand(op); + match cast_kind { + // We currently do not support soundly reasoning about trait objects, so need to + // notify the user. + 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::Transmute => { - 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. + CastKind::Transmute => { + let operand_ty = op.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: op.clone() }); } - } 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() }); } + _ => {} + } + } + } + } + + /// Check if one of the place projections involves dereferencing a raw pointer, which is an + /// instrumentation target , or union access, which is currently not supported. + fn check_place(&mut self, place: &Place) { + for (idx, elem) in place.projection.iter().enumerate() { + let intermediate_place = + Place { local: place.local, projection: place.projection[..idx].to_vec() }; + self.check_projection_elem(elem, intermediate_place) + } + } + + /// Check if the projection involves dereferencing a raw pointer, which is an instrumentation + /// target, or union access, which is currently not supported. + fn check_projection_elem( + &mut self, + projection_elem: &ProjectionElem, + intermediate_place: Place, + ) { + match projection_elem { + ProjectionElem::Deref => { + let ptr_ty = intermediate_place.ty(&self.locals).unwrap(); + if ptr_ty.kind().is_raw_ptr() { + self.push_target(MemoryInitOp::Check { + operand: Operand::Copy(intermediate_place.clone()), + }); } - _ => {} } - }; - self.super_rvalue(rvalue, location); + ProjectionElem::Field(_, _) => { + if intermediate_place.ty(&self.locals).unwrap().kind().is_union() { + self.push_target(MemoryInitOp::Unsupported { + reason: + "Kani does not support reasoning about memory initialization of unions." + .to_string(), + }); + } + } + ProjectionElem::Index(_) + | ProjectionElem::ConstantIndex { .. } + | ProjectionElem::Subslice { .. } => { + /* For a slice to be indexed, it should be valid first. */ + } + ProjectionElem::Downcast(_) => {} + ProjectionElem::OpaqueCast(_) => {} + ProjectionElem::Subtype(_) => {} + } + } + + /// Check if the operand is a static to initialize it or else check its associated place. + fn check_operand(&mut self, operand: &Operand) { + match operand { + Operand::Copy(place) | Operand::Move(place) => self.check_place(place), + Operand::Constant(constant) => { + if let ConstantKind::Allocated(allocation) = constant.const_.kind() { + for (_, prov) in &allocation.provenance.ptrs { + if let GlobalAlloc::Static(_) = GlobalAlloc::from(prov.0) { + if constant.ty().kind().is_raw_ptr() { + // If a static is a raw pointer, need to mark it as initialized. + self.push_target(MemoryInitOp::Set { + operand: Operand::Constant(constant.clone()), + value: true, + position: InsertPosition::Before, + }); + } + }; + } + } + } + } } }