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 88d906aa3134..0130c00d1a71 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -35,16 +35,29 @@ pub trait TargetFinder { fn find_all(self, body: &MutableBody) -> Vec; } +const KANI_IS_PTR_INITIALIZED_DIAGNOSTIC: &str = "KaniIsPtrInitialized"; +const KANI_SET_PTR_INITIALIZED_DIAGNOSTIC: &str = "KaniSetPtrInitialized"; +const KANI_IS_SLICE_CHUNK_PTR_INITIALIZED_DIAGNOSTIC: &str = "KaniIsSliceChunkPtrInitialized"; +const KANI_SET_SLICE_CHUNK_PTR_INITIALIZED_DIAGNOSTIC: &str = "KaniSetSliceChunkPtrInitialized"; +const KANI_IS_SLICE_PTR_INITIALIZED_DIAGNOSTIC: &str = "KaniIsSlicePtrInitialized"; +const KANI_SET_SLICE_PTR_INITIALIZED_DIAGNOSTIC: &str = "KaniSetSlicePtrInitialized"; +const KANI_IS_STR_PTR_INITIALIZED_DIAGNOSTIC: &str = "KaniIsStrPtrInitialized"; +const KANI_SET_STR_PTR_INITIALIZED_DIAGNOSTIC: &str = "KaniSetStrPtrInitialized"; +const KANI_COPY_INIT_STATE_DIAGNOSTIC: &str = "KaniCopyInitState"; +const KANI_COPY_INIT_STATE_SINGLE_DIAGNOSTIC: &str = "KaniCopyInitStateSingle"; + // Function bodies of those functions will not be instrumented as not to cause infinite recursion. const SKIPPED_DIAGNOSTIC_ITEMS: &[&str] = &[ - "KaniIsPtrInitialized", - "KaniSetPtrInitialized", - "KaniIsSliceChunkPtrInitialized", - "KaniSetSliceChunkPtrInitialized", - "KaniIsSlicePtrInitialized", - "KaniSetSlicePtrInitialized", - "KaniIsStrPtrInitialized", - "KaniSetStrPtrInitialized", + KANI_IS_PTR_INITIALIZED_DIAGNOSTIC, + KANI_SET_PTR_INITIALIZED_DIAGNOSTIC, + KANI_IS_SLICE_CHUNK_PTR_INITIALIZED_DIAGNOSTIC, + KANI_SET_SLICE_CHUNK_PTR_INITIALIZED_DIAGNOSTIC, + KANI_IS_SLICE_PTR_INITIALIZED_DIAGNOSTIC, + KANI_SET_SLICE_PTR_INITIALIZED_DIAGNOSTIC, + KANI_IS_STR_PTR_INITIALIZED_DIAGNOSTIC, + KANI_SET_STR_PTR_INITIALIZED_DIAGNOSTIC, + KANI_COPY_INIT_STATE_DIAGNOSTIC, + KANI_COPY_INIT_STATE_SINGLE_DIAGNOSTIC, ]; /// Instruments the code with checks for uninitialized memory, agnostic to the source of targets. @@ -164,8 +177,14 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { } MemoryInitOp::SetSliceChunk { .. } | MemoryInitOp::Set { .. } - | MemoryInitOp::SetRef { .. } => self.build_set(body, source, operation, pointee_info), + | MemoryInitOp::SetRef { .. } + | MemoryInitOp::CreateUnion { .. } => { + self.build_set(body, source, operation, pointee_info) + } MemoryInitOp::Copy { .. } => self.build_copy(body, source, operation, pointee_info), + MemoryInitOp::AssignUnion { .. } => { + self.build_assign_union(body, source, operation, pointee_info) + } MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => { unreachable!() } @@ -196,12 +215,12 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { // pass is as an argument. let (diagnostic, args) = match &operation { MemoryInitOp::Check { .. } | MemoryInitOp::CheckRef { .. } => { - let diagnostic = "KaniIsPtrInitialized"; + let diagnostic = KANI_IS_PTR_INITIALIZED_DIAGNOSTIC; let args = vec![ptr_operand.clone(), layout_operand]; (diagnostic, args) } MemoryInitOp::CheckSliceChunk { .. } => { - let diagnostic = "KaniIsSliceChunkPtrInitialized"; + let diagnostic = KANI_IS_SLICE_CHUNK_PTR_INITIALIZED_DIAGNOSTIC; let args = vec![ptr_operand.clone(), layout_operand, operation.expect_count()]; (diagnostic, args) @@ -232,10 +251,10 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { // Since `str`` is a separate type, need to differentiate between [T] and str. let (slicee_ty, diagnostic) = match pointee_info.ty().kind() { TyKind::RigidTy(RigidTy::Slice(slicee_ty)) => { - (slicee_ty, "KaniIsSlicePtrInitialized") + (slicee_ty, KANI_IS_SLICE_PTR_INITIALIZED_DIAGNOSTIC) } TyKind::RigidTy(RigidTy::Str) => { - (Ty::unsigned_ty(UintTy::U8), "KaniIsStrPtrInitialized") + (Ty::unsigned_ty(UintTy::U8), KANI_IS_STR_PTR_INITIALIZED_DIAGNOSTIC) } _ => unreachable!(), }; @@ -266,6 +285,14 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { self.inject_assert_false(self.tcx, body, source, operation.position(), reason); return; } + PointeeLayout::Union { .. } => { + // Here we are reading from a pointer to a union. + // TODO: we perhaps need to check that the union at least contains an intersection + // of all layouts initialized. + let reason = "Interaction between raw pointers and unions is not yet supported."; + self.inject_assert_false(self.tcx, body, source, operation.position(), reason); + return; + } }; // Construct the basic block and insert it into the body. @@ -317,7 +344,7 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { // pass is as an argument. let (diagnostic, args) = match &operation { MemoryInitOp::Set { .. } | MemoryInitOp::SetRef { .. } => { - let diagnostic = "KaniSetPtrInitialized"; + let diagnostic = KANI_SET_PTR_INITIALIZED_DIAGNOSTIC; let args = vec![ ptr_operand, layout_operand, @@ -330,7 +357,7 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { (diagnostic, args) } MemoryInitOp::SetSliceChunk { .. } => { - let diagnostic = "KaniSetSliceChunkPtrInitialized"; + let diagnostic = KANI_SET_SLICE_CHUNK_PTR_INITIALIZED_DIAGNOSTIC; let args = vec![ ptr_operand, layout_operand, @@ -369,10 +396,10 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { // Since `str`` is a separate type, need to differentiate between [T] and str. let (slicee_ty, diagnostic) = match pointee_info.ty().kind() { TyKind::RigidTy(RigidTy::Slice(slicee_ty)) => { - (slicee_ty, "KaniSetSlicePtrInitialized") + (slicee_ty, KANI_SET_SLICE_PTR_INITIALIZED_DIAGNOSTIC) } TyKind::RigidTy(RigidTy::Str) => { - (Ty::unsigned_ty(UintTy::U8), "KaniSetStrPtrInitialized") + (Ty::unsigned_ty(UintTy::U8), KANI_SET_STR_PTR_INITIALIZED_DIAGNOSTIC) } _ => unreachable!(), }; @@ -409,6 +436,63 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { PointeeLayout::TraitObject => { unreachable!("Cannot change the initialization state of a trait object directly."); } + PointeeLayout::Union { field_layouts } => { + // Writing union data, which could be either creating a union from scratch or + // performing some pointer operations with it. If we are creating a union from + // scratch, an operation will contain a union field. + + // TODO: If we don't have a union field, we are either creating a pointer to a union + // or assigning to one. In the former case, it is safe to return from this function, + // since the union must be already tracked (on creation and update). In the latter + // case, we should have been using union assignment instead. Nevertheless, this is + // currently mitigated by injecting `assert!(false)`. + let union_field = match operation.union_field() { + Some(field) => field, + None => { + let reason = + "Interaction between raw pointers and unions is not yet supported."; + self.inject_assert_false( + self.tcx, + body, + source, + operation.position(), + reason, + ); + return; + } + }; + let layout = &field_layouts[union_field]; + let layout_operand = mk_layout_operand(body, &mut statements, source, layout); + let diagnostic = KANI_SET_PTR_INITIALIZED_DIAGNOSTIC; + let args = vec![ + ptr_operand, + layout_operand, + Operand::Constant(ConstOperand { + span: source.span(body.blocks()), + user_ty: None, + const_: MirConst::from_bool(value), + }), + ]; + let set_ptr_initialized_instance = resolve_mem_init_fn( + get_mem_init_fn_def(self.tcx, diagnostic, &mut self.mem_init_fn_cache), + layout.len(), + *pointee_info.ty(), + ); + Terminator { + kind: TerminatorKind::Call { + func: Operand::Copy(Place::from(body.new_local( + set_ptr_initialized_instance.ty(), + source.span(body.blocks()), + Mutability::Not, + ))), + args, + destination: ret_place.clone(), + target: Some(0), // this will be overriden in add_bb + unwind: UnwindAction::Terminate, + }, + span: source.span(body.blocks()), + } + } }; // Construct the basic block and insert it into the body. body.insert_bb(BasicBlock { statements, terminator }, source, operation.position()); @@ -426,14 +510,19 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { local: body.new_local(Ty::new_tuple(&[]), source.span(body.blocks()), Mutability::Not), projection: vec![], }; - let PointeeLayout::Sized { layout } = pointee_info.layout() else { unreachable!() }; + let layout_size = pointee_info.layout().maybe_size().unwrap(); let copy_init_state_instance = resolve_mem_init_fn( - get_mem_init_fn_def(self.tcx, "KaniCopyInitState", &mut self.mem_init_fn_cache), - layout.len(), + get_mem_init_fn_def( + self.tcx, + KANI_COPY_INIT_STATE_DIAGNOSTIC, + &mut self.mem_init_fn_cache, + ), + layout_size, *pointee_info.ty(), ); let position = operation.position(); - let MemoryInitOp::Copy { from, to, count } = operation else { unreachable!() }; + let (from, to) = operation.expect_copy_operands(); + let count = operation.expect_count(); body.insert_call( ©_init_state_instance, source, @@ -443,6 +532,49 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { ); } + /// Copy memory initialization state from one union variable to another. + fn build_assign_union( + &mut self, + body: &mut MutableBody, + source: &mut SourceInstruction, + operation: MemoryInitOp, + pointee_info: PointeeInfo, + ) { + let ret_place = Place { + local: body.new_local(Ty::new_tuple(&[]), source.span(body.blocks()), Mutability::Not), + projection: vec![], + }; + let mut statements = vec![]; + let layout_size = pointee_info.layout().maybe_size().unwrap(); + let copy_init_state_instance = resolve_mem_init_fn( + get_mem_init_fn_def( + self.tcx, + KANI_COPY_INIT_STATE_SINGLE_DIAGNOSTIC, + &mut self.mem_init_fn_cache, + ), + layout_size, + *pointee_info.ty(), + ); + let (from, to) = operation.expect_assign_union_operands(body, &mut statements, source); + let terminator = Terminator { + kind: TerminatorKind::Call { + func: Operand::Copy(Place::from(body.new_local( + copy_init_state_instance.ty(), + source.span(body.blocks()), + Mutability::Not, + ))), + args: vec![from, to], + destination: ret_place.clone(), + target: Some(0), // this will be overriden in add_bb + unwind: UnwindAction::Terminate, + }, + span: source.span(body.blocks()), + }; + + // Construct the basic block and insert it into the body. + body.insert_bb(BasicBlock { statements, terminator }, source, operation.position()); + } + fn inject_assert_false( &self, tcx: TyCtxt, 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 a1689bdfe8c4..207005dafb27 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 @@ -19,10 +19,11 @@ use stable_mir::{ alloc::GlobalAlloc, mono::{Instance, InstanceKind}, visit::{Location, PlaceContext}, - CastKind, LocalDecl, MirVisitor, NonDivergingIntrinsic, Operand, Place, PointerCoercion, - ProjectionElem, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, + AggregateKind, CastKind, LocalDecl, MirVisitor, NonDivergingIntrinsic, Operand, Place, + PointerCoercion, ProjectionElem, Rvalue, Statement, StatementKind, Terminator, + TerminatorKind, }, - ty::{ConstantKind, RigidTy, TyKind}, + ty::{AdtKind, ConstantKind, RigidTy, TyKind}, }; pub struct CheckUninitVisitor { @@ -112,7 +113,7 @@ 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 place.ty(&self.locals).unwrap().kind().is_raw_ptr() { if let Rvalue::AddressOf(..) = rvalue { self.push_target(MemoryInitOp::Set { operand: Operand::Copy(place.clone()), @@ -121,6 +122,58 @@ impl MirVisitor for CheckUninitVisitor { }); } } + + // TODO: add support for ADTs which could have unions as subfields. Currently, + // if a union as a subfield is detected, `assert!(false)` will be injected from + // the type layout code. + let is_inside_union = { + let mut contains_union = false; + let mut place_to_add_projections = + Place { local: place.local, projection: vec![] }; + for projection_elem in place.projection.iter() { + if place_to_add_projections.ty(&self.locals).unwrap().kind().is_union() { + contains_union = true; + break; + } + place_to_add_projections.projection.push(projection_elem.clone()); + } + contains_union + }; + + // Need to copy some information about union initialization, since lvalue is + // either a union or a field inside a union. + if is_inside_union { + if let Rvalue::Use(operand) = rvalue { + // This is a union-to-union assignment, so we need to copy the + // initialization state. + if place.ty(&self.locals).unwrap().kind().is_union() { + self.push_target(MemoryInitOp::AssignUnion { + lvalue: place.clone(), + rvalue: operand.clone(), + }); + } else { + // This is assignment to a field of a union. + self.push_target(MemoryInitOp::SetRef { + operand: Operand::Copy(place.clone()), + value: true, + position: InsertPosition::After, + }); + } + } + } + + // Create a union from scratch as an aggregate. We handle it here because we + // need to know which field is getting assigned. + if let Rvalue::Aggregate(AggregateKind::Adt(adt_def, _, _, _, union_field), _) = + rvalue + { + if adt_def.kind() == AdtKind::Union { + self.push_target(MemoryInitOp::CreateUnion { + operand: Operand::Copy(place.clone()), + field: union_field.unwrap(), // Safe to unwrap because we know this is a union. + }); + } + } } StatementKind::Deinit(place) => { self.super_statement(stmt, location); @@ -350,12 +403,22 @@ impl MirVisitor for CheckUninitVisitor { }); } } - ProjectionElem::Field(idx, target_ty) => { - if target_ty.kind().is_union() - && (!ptx.is_mutating() || place.projection.len() > idx + 1) + ProjectionElem::Field(_, _) => { + if intermediate_place.ty(&self.locals).unwrap().kind().is_union() + && !ptx.is_mutating() { - self.push_target(MemoryInitOp::Unsupported { - reason: "Kani does not support reasoning about memory initialization of unions.".to_string(), + let contains_deref_projection = + { place.projection.iter().any(|elem| *elem == ProjectionElem::Deref) }; + if contains_deref_projection { + // We do not currently support having a deref projection in the same + // place as union field access. + self.push_target(MemoryInitOp::Unsupported { + reason: "Kani does not yet support performing a dereference on a union field".to_string(), + }); + } + // Accessing a place inside the union, need to check if it is initialized. + self.push_target(MemoryInitOp::CheckRef { + operand: Operand::Copy(place.clone()), }); } } diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs b/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs index 05826969262d..6120f2d3d4c4 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs @@ -6,9 +6,8 @@ use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; use stable_mir::{ - mir::{Mutability, Operand, Place, Rvalue, Statement, StatementKind}, - ty::RigidTy, - ty::Ty, + mir::{FieldIdx, Mutability, Operand, Place, Rvalue, Statement, StatementKind}, + ty::{RigidTy, Ty}, }; use strum_macros::AsRefStr; @@ -17,28 +16,65 @@ use strum_macros::AsRefStr; pub enum MemoryInitOp { /// Check memory initialization of data bytes in a memory region starting from the pointer /// `operand` and of length `sizeof(operand)` bytes. - Check { operand: Operand }, + Check { + operand: Operand, + }, /// Set memory initialization state of data bytes in a memory region starting from the pointer /// `operand` and of length `sizeof(operand)` bytes. - Set { operand: Operand, value: bool, position: InsertPosition }, + Set { + operand: Operand, + value: bool, + position: InsertPosition, + }, /// Check memory initialization of data bytes in a memory region starting from the pointer /// `operand` and of length `count * sizeof(operand)` bytes. - CheckSliceChunk { operand: Operand, count: Operand }, + CheckSliceChunk { + operand: Operand, + count: Operand, + }, /// Set memory initialization state of data bytes in a memory region starting from the pointer /// `operand` and of length `count * sizeof(operand)` bytes. - SetSliceChunk { operand: Operand, count: Operand, value: bool, position: InsertPosition }, + SetSliceChunk { + operand: Operand, + count: Operand, + value: bool, + position: InsertPosition, + }, /// Set memory initialization of data bytes in a memory region starting from the reference to /// `operand` and of length `sizeof(operand)` bytes. - CheckRef { operand: Operand }, + CheckRef { + operand: Operand, + }, /// Set memory initialization of data bytes in a memory region starting from the reference to /// `operand` and of length `sizeof(operand)` bytes. - SetRef { operand: Operand, value: bool, position: InsertPosition }, + SetRef { + operand: Operand, + value: bool, + position: InsertPosition, + }, /// Unsupported memory initialization operation. - Unsupported { reason: String }, + Unsupported { + reason: String, + }, /// Operation that trivially accesses uninitialized memory, results in injecting `assert!(false)`. - TriviallyUnsafe { reason: String }, + TriviallyUnsafe { + reason: String, + }, /// Operation that copies memory initialization state over to another operand. - Copy { from: Operand, to: Operand, count: Operand }, + Copy { + from: Operand, + to: Operand, + count: Operand, + }, + + AssignUnion { + lvalue: Place, + rvalue: Operand, + }, + CreateUnion { + operand: Operand, + field: FieldIdx, + }, } impl MemoryInitOp { @@ -56,28 +92,13 @@ impl MemoryInitOp { | MemoryInitOp::Set { operand, .. } | MemoryInitOp::CheckSliceChunk { operand, .. } | MemoryInitOp::SetSliceChunk { operand, .. } => operand.clone(), - MemoryInitOp::CheckRef { operand, .. } | MemoryInitOp::SetRef { operand, .. } => { - let span = source.span(body.blocks()); - - let ref_local = { - let place = match operand { - Operand::Copy(place) | Operand::Move(place) => place, - Operand::Constant(_) => unreachable!(), - }; - let rvalue = Rvalue::AddressOf(Mutability::Not, place.clone()); - let ret_ty = rvalue.ty(body.locals()).unwrap(); - let result = body.new_local(ret_ty, span, Mutability::Not); - let stmt = Statement { - kind: StatementKind::Assign(Place::from(result), rvalue), - span, - }; - statements.push(stmt); - result - }; - - Operand::Copy(Place { local: ref_local, projection: vec![] }) + MemoryInitOp::CheckRef { operand, .. } + | MemoryInitOp::SetRef { operand, .. } + | MemoryInitOp::CreateUnion { operand, .. } => { + mk_ref(operand, body, statements, source) } MemoryInitOp::Copy { .. } + | MemoryInitOp::AssignUnion { .. } | MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => { unreachable!() @@ -85,13 +106,42 @@ impl MemoryInitOp { } } + /// A helper to access operands of copy operation. + pub fn expect_copy_operands(&self) -> (Operand, Operand) { + match self { + MemoryInitOp::Copy { from, to, .. } => (from.clone(), to.clone()), + _ => unreachable!(), + } + } + + /// A helper to access operands of union assign, automatically creates references to them. + pub fn expect_assign_union_operands( + &self, + body: &mut MutableBody, + statements: &mut Vec, + source: &mut SourceInstruction, + ) -> (Operand, Operand) { + match self { + MemoryInitOp::AssignUnion { lvalue, rvalue } => { + let lvalue_as_operand = Operand::Copy(lvalue.clone()); + ( + mk_ref(rvalue, body, statements, source), + mk_ref(&lvalue_as_operand, body, statements, source), + ) + } + _ => unreachable!(), + } + } + pub fn operand_ty(&self, body: &MutableBody) -> Ty { match self { MemoryInitOp::Check { operand, .. } | MemoryInitOp::Set { operand, .. } | MemoryInitOp::CheckSliceChunk { operand, .. } | MemoryInitOp::SetSliceChunk { operand, .. } => operand.ty(body.locals()).unwrap(), - MemoryInitOp::SetRef { operand, .. } | MemoryInitOp::CheckRef { operand, .. } => { + MemoryInitOp::SetRef { operand, .. } + | MemoryInitOp::CheckRef { operand, .. } + | MemoryInitOp::CreateUnion { operand, .. } => { let place = match operand { Operand::Copy(place) | Operand::Move(place) => place, Operand::Constant(_) => unreachable!(), @@ -117,6 +167,12 @@ impl MemoryInitOp { assert!(from_pointee_ty == to_pointee_ty); from.ty(body.locals()).unwrap() } + MemoryInitOp::AssignUnion { lvalue, .. } => { + // It does not matter which operand to return for layout generation, since both of + // them have the same pointee type. + let address_of = Rvalue::AddressOf(Mutability::Not, lvalue.clone()); + address_of.ty(body.locals()).unwrap() + } } } @@ -129,6 +185,8 @@ impl MemoryInitOp { | MemoryInitOp::Set { .. } | MemoryInitOp::CheckRef { .. } | MemoryInitOp::SetRef { .. } + | MemoryInitOp::CreateUnion { .. } + | MemoryInitOp::AssignUnion { .. } | MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => unreachable!(), } @@ -139,12 +197,30 @@ impl MemoryInitOp { MemoryInitOp::Set { value, .. } | MemoryInitOp::SetSliceChunk { value, .. } | MemoryInitOp::SetRef { value, .. } => *value, + MemoryInitOp::CreateUnion { .. } => true, MemoryInitOp::Check { .. } | MemoryInitOp::CheckSliceChunk { .. } | MemoryInitOp::CheckRef { .. } | MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } - | MemoryInitOp::Copy { .. } => unreachable!(), + | MemoryInitOp::Copy { .. } + | MemoryInitOp::AssignUnion { .. } => unreachable!(), + } + } + + pub fn union_field(&self) -> Option { + match self { + MemoryInitOp::CreateUnion { field, .. } => Some(*field), + MemoryInitOp::Check { .. } + | MemoryInitOp::CheckSliceChunk { .. } + | MemoryInitOp::CheckRef { .. } + | MemoryInitOp::Set { .. } + | MemoryInitOp::SetSliceChunk { .. } + | MemoryInitOp::SetRef { .. } + | MemoryInitOp::Unsupported { .. } + | MemoryInitOp::TriviallyUnsafe { .. } + | MemoryInitOp::Copy { .. } + | MemoryInitOp::AssignUnion { .. } => None, } } @@ -158,7 +234,9 @@ impl MemoryInitOp { | MemoryInitOp::CheckRef { .. } | MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => InsertPosition::Before, - MemoryInitOp::Copy { .. } => InsertPosition::After, + MemoryInitOp::Copy { .. } + | MemoryInitOp::AssignUnion { .. } + | MemoryInitOp::CreateUnion { .. } => InsertPosition::After, } } } @@ -184,3 +262,29 @@ impl InitRelevantInstruction { } } } + +/// A helper to generate instrumentation for taking a reference to a given operand. Returns the +/// operand which is a reference and stores all instrumentation in the statements vector passed. +fn mk_ref( + operand: &Operand, + body: &mut MutableBody, + statements: &mut Vec, + source: &mut SourceInstruction, +) -> Operand { + let span = source.span(body.blocks()); + + let ref_local = { + let place = match operand { + Operand::Copy(place) | Operand::Move(place) => place, + Operand::Constant(_) => unreachable!(), + }; + let rvalue = Rvalue::AddressOf(Mutability::Not, place.clone()); + let ret_ty = rvalue.ty(body.locals()).unwrap(); + let result = body.new_local(ret_ty, span, Mutability::Not); + let stmt = Statement { kind: StatementKind::Assign(Place::from(result), rvalue), span }; + statements.push(stmt); + result + }; + + Operand::Copy(Place { local: ref_local, projection: vec![] }) +} diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs index 8a162d5944d3..dac130f11545 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs @@ -6,7 +6,7 @@ use stable_mir::{ abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape}, target::{MachineInfo, MachineSize}, - ty::{AdtKind, IndexedVal, RigidTy, Ty, TyKind, UintTy}, + ty::{AdtKind, IndexedVal, RigidTy, Ty, TyKind, UintTy, VariantIdx}, CrateDef, }; @@ -43,10 +43,26 @@ pub enum PointeeLayout { Sized { layout: Layout }, /// Layout of slices, *const/mut str is included in this case and treated as *const/mut [u8]. Slice { element_layout: Layout }, + /// Layout of unions, which are shared storage for multiple fields of potentially different layouts. + Union { field_layouts: Vec }, /// Trait objects have an arbitrary layout. TraitObject, } +impl PointeeLayout { + /// Returns the size of the layout, if available. + pub fn maybe_size(&self) -> Option { + match self { + PointeeLayout::Sized { layout } => Some(layout.len()), + PointeeLayout::Slice { element_layout } => Some(element_layout.len()), + PointeeLayout::Union { field_layouts } => { + Some(field_layouts.iter().map(|field_layout| field_layout.len()).max().unwrap()) + } + PointeeLayout::TraitObject => None, + } + } +} + pub struct PointeeInfo { pointee_ty: Ty, layout: PointeeLayout, @@ -56,6 +72,25 @@ impl PointeeInfo { pub fn from_ty(ty: Ty) -> Result { match ty.kind() { TyKind::RigidTy(rigid_ty) => match rigid_ty { + RigidTy::Adt(adt_def, args) if adt_def.kind() == AdtKind::Union => { + assert!(adt_def.variants().len() == 1); + let fields: Result<_, _> = adt_def + .variant(VariantIdx::to_val(0)) + .unwrap() + .fields() + .into_iter() + .map(|field_def| { + let ty = field_def.ty_with_args(&args); + let size_in_bytes = ty.layout().unwrap().shape().size.bytes(); + data_bytes_for_ty(&MachineInfo::target(), ty, 0) + .map(|data_chunks| generate_byte_mask(size_in_bytes, data_chunks)) + }) + .collect(); + Ok(PointeeInfo { + pointee_ty: ty, + layout: PointeeLayout::Union { field_layouts: fields? }, + }) + } RigidTy::Str => { let slicee_ty = Ty::unsigned_ty(UintTy::U8); let size_in_bytes = slicee_ty.layout().unwrap().shape().size.bytes(); @@ -330,7 +365,7 @@ fn data_bytes_for_ty( | RigidTy::Dynamic(_, _, _) => Err(format!("Unsupported {ty:?}")), } } - FieldsShape::Union(_) => Err(format!("Unsupported {ty:?}")), + FieldsShape::Union(_) => Err(format!("Unions as fields of unions are unsupported {ty:?}")), FieldsShape::Array { .. } => Ok(vec![]), } } @@ -357,12 +392,12 @@ fn tys_layout_cmp_to_size(from_ty: &Ty, to_ty: &Ty, cmp: impl Fn(bool, bool) -> let from_ty_layout = match from_ty_info.layout() { PointeeLayout::Sized { layout } => layout, PointeeLayout::Slice { element_layout } => element_layout, - PointeeLayout::TraitObject => return false, + PointeeLayout::TraitObject | PointeeLayout::Union { .. } => 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, + PointeeLayout::TraitObject | PointeeLayout::Union { .. } => return false, }; // Ensure `to_ty_layout` does not have a larger size. if to_ty_layout.len() <= from_ty_layout.len() { diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index dd804b7379f2..9210c43fb163 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -307,6 +307,26 @@ impl IntrinsicGeneratorPass { new_body.insert_assignment(rvalue, &mut source, InsertPosition::Before); let reason: &str = "Kani does not support reasoning about memory initialization of pointers to trait objects."; + new_body.insert_check( + tcx, + &self.check_type, + &mut source, + InsertPosition::Before, + result, + &reason, + ); + } + PointeeLayout::Union { .. } => { + let rvalue = Rvalue::Use(Operand::Constant(ConstOperand { + const_: MirConst::from_bool(false), + span: source.span(new_body.blocks()), + user_ty: None, + })); + let result = + new_body.insert_assignment(rvalue, &mut source, InsertPosition::Before); + let reason: &str = + "Kani does not yet support using initialization predicates on unions."; + new_body.insert_check( tcx, &self.check_type, diff --git a/library/kani/src/mem_init.rs b/library/kani/src/mem_init.rs index 3755fc59a510..a6118c472a92 100644 --- a/library/kani/src/mem_init.rs +++ b/library/kani/src/mem_init.rs @@ -309,7 +309,9 @@ fn set_str_ptr_initialized( } } -/// Copy initialization state of `size_of:: * num_elts` bytes from one pointer to the other. +/// Copy initialization state of `size_of:: * num_elts` bytes from one pointer to the other. Note +/// that in this case `LAYOUT_SIZE == size_of::`. +#[kanitool::disable_checks(pointer)] #[rustc_diagnostic_item = "KaniCopyInitState"] fn copy_init_state(from: *const T, to: *const T, num_elts: usize) { if LAYOUT_SIZE == 0 { @@ -321,3 +323,11 @@ fn copy_init_state(from: *const T, to: *const T, nu MEM_INIT_STATE.copy::(from_ptr as *const u8, to_ptr as *const u8, num_elts); } } + +/// Copy initialization state of `size_of::` bytes from one pointer to the other. Note that in +/// this case `LAYOUT_SIZE == size_of::`. +#[kanitool::disable_checks(pointer)] +#[rustc_diagnostic_item = "KaniCopyInitStateSingle"] +fn copy_init_state_single(from: *const T, to: *const T) { + copy_init_state::(from, to, 1); +} diff --git a/tests/expected/uninit/fixme_unions.rs b/tests/expected/uninit/fixme_unions.rs new file mode 100644 index 000000000000..ec86e5e7e07f --- /dev/null +++ b/tests/expected/uninit/fixme_unions.rs @@ -0,0 +1,61 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks + +//! Tests for handling potentially uninitialized memory access via unions. +//! TODO: add a `.expected` file for this test. + +use std::ptr::addr_of; + +#[repr(C)] +#[derive(Clone, Copy)] +union U { + a: u16, + b: u32, +} + +/// Reading padding data via simple union access if union is passed to another function. +#[kani::proof] +unsafe fn cross_function_union_should_fail() { + unsafe fn helper(u: U) { + let padding = u.b; // Read 4 bytes from `u`. + } + let u = U { a: 0 }; // `u` is initialized for 2 bytes. + helper(u); +} + +/// Reading padding data but a union is behind a pointer. +#[kani::proof] +unsafe fn pointer_union_should_fail() { + let u = U { a: 0 }; // `u` is initialized for 2 bytes. + let u_ptr = addr_of!(u); + let u1 = *u_ptr; + let padding = u1.b; // Read 4 bytes from `u`. +} + +#[repr(C)] +struct S { + u: U, +} + +/// Tests uninitialized access if unions are top-level subfields. +#[kani::proof] +unsafe fn union_as_subfields_should_pass() { + let u = U { a: 0 }; // `u` is initialized for 2 bytes. + let s = S { u }; + let s1 = s; + let u1 = s1.u; // `u1` is initialized for 2 bytes. + let padding = u1.a; // Read 2 bytes from `u`. +} + +union Outer { + u: U, + a: u32, +} + +/// Tests unions composing with other unions. +#[kani::proof] +unsafe fn uber_union_should_pass() { + let u = Outer { u: U { b: 0 } }; // `u` is initialized for 4 bytes. + let non_padding = u.a; // Read 4 bytes from `u`. +} diff --git a/tests/expected/uninit/intrinsics/expected b/tests/expected/uninit/intrinsics/expected index 33392337c30b..b5555785e8af 100644 --- a/tests/expected/uninit/intrinsics/expected +++ b/tests/expected/uninit/intrinsics/expected @@ -1,10 +1,10 @@ -std::ptr::read::>.assertion.1\ +std::ptr::write::>.assertion.1\ - Status: FAILURE\ - - Description: "Kani currently doesn't support checking memory initialization for pointers to `std::mem::MaybeUninit." + - Description: "Interaction between raw pointers and unions is not yet supported." std::ptr::write::>.assertion.1\ - Status: FAILURE\ - - Description: "Kani currently doesn't support checking memory initialization for pointers to `std::mem::MaybeUninit." + - Description: "Interaction between raw pointers and unions is not yet supported."\ check_typed_swap.assertion.1\ - Status: FAILURE\ diff --git a/tests/expected/uninit/unions.expected b/tests/expected/uninit/unions.expected new file mode 100644 index 000000000000..05fdac3a8765 --- /dev/null +++ b/tests/expected/uninit/unions.expected @@ -0,0 +1,17 @@ +union_update_should_fail.assertion.1\ + - Status: FAILURE\ + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`" + +union_complex_subfields_should_fail.assertion.1\ + - Status: FAILURE\ + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u16`" + +basic_union_should_fail.assertion.1\ + - Status: FAILURE\ + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`" + +Summary: +Verification failed for - union_update_should_fail +Verification failed for - union_complex_subfields_should_fail +Verification failed for - basic_union_should_fail +Complete - 3 successfully verified harnesses, 3 failures, 6 total. diff --git a/tests/expected/uninit/unions.rs b/tests/expected/uninit/unions.rs new file mode 100644 index 000000000000..c623f9fcea94 --- /dev/null +++ b/tests/expected/uninit/unions.rs @@ -0,0 +1,68 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks + +//! Tests for handling potentially uninitialized memory access via unions. + +use std::ptr::addr_of; + +#[repr(C)] +#[derive(Clone, Copy)] +union U { + a: u16, + b: u32, +} + +/// Simple and correct union access. +#[kani::proof] +unsafe fn basic_union_should_pass() { + let u = U { b: 0 }; + let u1 = u; + let non_padding = u1.a; + assert!(non_padding == 0); +} + +/// Reading padding data via simple union access. +#[kani::proof] +unsafe fn basic_union_should_fail() { + let u = U { a: 0 }; + let u1 = u; + let padding = u1.b; +} + +#[repr(C)] +union U1 { + a: (u32, u8), + b: (u32, u16, u8), +} + +/// Tests accessing initialized data via subfields of a union. +#[kani::proof] +unsafe fn union_complex_subfields_should_pass() { + let u = U1 { a: (0, 0) }; + let non_padding = u.b.0; +} + +/// Tests accessing uninit data via subfields of a union. +#[kani::proof] +unsafe fn union_complex_subfields_should_fail() { + let u = U1 { a: (0, 0) }; + let padding = u.b.1; +} + +/// Tests overwriting data inside unions. +#[kani::proof] +unsafe fn union_update_should_pass() { + let mut u = U { a: 0 }; + u.b = 0; + let non_padding = u.b; + assert!(non_padding == 0); +} + +/// Tests overwriting data inside unions. +#[kani::proof] +unsafe fn union_update_should_fail() { + let mut u = U { a: 0 }; + u.a = 0; + let padding = u.b; +}