From d77365d4650ff493cfbe10701beb75fdfd57745e Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 14 Aug 2024 08:48:29 -0700 Subject: [PATCH 01/15] Avoid corner-cases by grouping instrumentation into basic blocks --- .../src/kani_middle/transform/body.rs | 16 +- .../transform/check_uninit/delayed_ub/mod.rs | 23 +- .../kani_middle/transform/check_uninit/mod.rs | 336 +++++++++++------- .../transform/check_uninit/ptr_uninit/mod.rs | 16 +- .../check_uninit/relevant_instruction.rs | 65 +++- .../kani_middle/transform/kani_intrinsics.rs | 135 ++++--- 6 files changed, 372 insertions(+), 219 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index fa4e5eb1ad97..e050084eaf44 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -310,16 +310,16 @@ impl MutableBody { // Update the source to point at the terminator. *source = SourceInstruction::Terminator { bb: orig_bb }; } - // Make the terminator at `source` point at the new block, - // the terminator of which is a simple Goto instruction. + // Make the terminator at `source` point at the new block, the terminator of which is + // provided by the caller. SourceInstruction::Terminator { bb } => { let current_term = &mut self.blocks.get_mut(*bb).unwrap().terminator; let target_bb = get_mut_target_ref(current_term); let new_target_bb = get_mut_target_ref(&mut new_term); - // Set the new terminator to point where previous terminator pointed. - *new_target_bb = *target_bb; - // Point the current terminator to the new terminator's basic block. - *target_bb = new_bb_idx; + // Swap the targets of the newly inserted terminator and the original one. This is + // an easy way to make the original terminator point to the new basic block with the + // new terminator. + std::mem::swap(new_target_bb, target_bb); // Update the source to point at the terminator. *bb = new_bb_idx; self.blocks.push(BasicBlock { statements: vec![], terminator: new_term }); @@ -503,6 +503,10 @@ impl SourceInstruction { SourceInstruction::Statement { bb, .. } | SourceInstruction::Terminator { bb } => bb, } } + + pub fn is_terminator(&self) -> bool { + matches!(self, SourceInstruction::Terminator { .. }) + } } fn find_instance(tcx: TyCtxt, diagnostic: &str) -> Option { diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs index 6b488569813f..e179947d2777 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs @@ -11,9 +11,8 @@ use crate::kani_middle::{ points_to::{run_points_to_analysis, MemLoc, PointsToGraph}, reachability::CallGraph, transform::{ - body::{CheckType, MutableBody}, - check_uninit::UninitInstrumenter, - BodyTransformation, GlobalPass, TransformationResult, + body::CheckType, check_uninit::UninitInstrumenter, BodyTransformation, GlobalPass, + TransformationResult, }, }; use crate::kani_queries::QueryDb; @@ -112,12 +111,8 @@ impl GlobalPass for DelayedUbPass { // Instrument each instance based on the final targets we found. for instance in instances { - let mut instrumenter = UninitInstrumenter { - check_type: self.check_type.clone(), - mem_init_fn_cache: &mut self.mem_init_fn_cache, - }; // Retrieve the body with all local instrumentation passes applied. - let body = MutableBody::from(transformer.body(tcx, instance)); + let body = transformer.body(tcx, instance); // Instrument for delayed UB. let target_finder = InstrumentationVisitor::new( &global_points_to_graph, @@ -125,12 +120,18 @@ impl GlobalPass for DelayedUbPass { instance, tcx, ); - let (instrumentation_added, body) = - instrumenter.instrument(tcx, body, instance, target_finder); + let (instrumentation_added, body) = UninitInstrumenter::run( + body, + tcx, + instance, + self.check_type.clone(), + &mut self.mem_init_fn_cache, + target_finder, + ); // If some instrumentation has been performed, update the cached body in the local transformer. if instrumentation_added { transformer.cache.entry(instance).and_modify(|transformation_result| { - *transformation_result = TransformationResult::Modified(body.into()); + *transformation_result = TransformationResult::Modified(body); }); } } 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 5c7194f879d1..cca33b902ed9 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -13,8 +13,8 @@ use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use stable_mir::{ mir::{ - mono::Instance, AggregateKind, BasicBlockIdx, ConstOperand, Mutability, Operand, Place, - Rvalue, + mono::Instance, AggregateKind, BasicBlock, BasicBlockIdx, Body, ConstOperand, Mutability, + Operand, Place, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, UnwindAction, }, ty::{FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Ty, TyConst, TyKind, UintTy}, CrateDef, @@ -31,7 +31,7 @@ mod relevant_instruction; mod ty_layout; /// Trait that the instrumentation target providers must implement to work with the instrumenter. -trait TargetFinder { +pub trait TargetFinder { fn find_next( &mut self, body: &MutableBody, @@ -53,27 +53,64 @@ const SKIPPED_DIAGNOSTIC_ITEMS: &[&str] = &[ ]; /// Instruments the code with checks for uninitialized memory, agnostic to the source of targets. -#[derive(Debug)] -pub struct UninitInstrumenter<'a> { - pub check_type: CheckType, +pub struct UninitInstrumenter<'a, 'tcx> { + check_type: CheckType, /// Used to cache FnDef lookups of injected memory initialization functions. - pub mem_init_fn_cache: &'a mut HashMap<&'static str, FnDef>, + mem_init_fn_cache: &'a mut HashMap<&'static str, FnDef>, + tcx: TyCtxt<'tcx>, + /// Set of basic block indices for which analyzing first statement should be skipped. + /// + /// This is necessary because some checks are inserted before the source instruction, which, in + /// turn, gets moved to the next basic block. Hence, we would not need to look at the + /// instruction again as a part of new basic block. However, if the check is inserted after the + /// source instruction, we still need to look at the first statement of the new basic block, so + /// we need to keep track of which basic blocks were created as a part of injecting checks after + /// the source instruction. + skip_first: HashSet, + /// Set of basic blocks that are fully autogenerated and hence need to be skipped for + /// instrumentation. + /// + /// Putting instrumentation into a separate basic block and then skipping it altogether is an + /// easier solution than tracking the position of added statements and terminators since + /// basic blocks do not shift during the instrumentation. + autogenerated_bbs: HashSet, } -impl<'a> UninitInstrumenter<'a> { +impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { + /// Create the instrumenter and run it with the given parameters. + pub(crate) fn run( + body: Body, + tcx: TyCtxt<'tcx>, + instance: Instance, + check_type: CheckType, + mem_init_fn_cache: &'a mut HashMap<&'static str, FnDef>, + target_finder: impl TargetFinder, + ) -> (bool, Body) { + let mut instrumenter = Self { + check_type, + mem_init_fn_cache, + tcx, + skip_first: HashSet::new(), + autogenerated_bbs: HashSet::new(), + }; + let body = MutableBody::from(body); + let (changed, new_body) = instrumenter.instrument(body, instance, target_finder); + (changed, new_body.into()) + } + /// Instrument a body with memory initialization checks, the visitor that generates /// instrumentation targets must be provided via a TF type parameter. fn instrument( &mut self, - tcx: TyCtxt, mut body: MutableBody, instance: Instance, mut target_finder: impl TargetFinder, ) -> (bool, MutableBody) { // Need to break infinite recursion when memory initialization checks are inserted, so the // internal functions responsible for memory initialization are skipped. - if tcx - .get_diagnostic_name(rustc_internal::internal(tcx, instance.def.def_id())) + if self + .tcx + .get_diagnostic_name(rustc_internal::internal(self.tcx, instance.def.def_id())) .map(|diagnostic_name| { SKIPPED_DIAGNOSTIC_ITEMS.contains(&diagnostic_name.to_ident_string().as_str()) }) @@ -84,27 +121,18 @@ impl<'a> UninitInstrumenter<'a> { let orig_len = body.blocks().len(); - // Set of basic block indices for which analyzing first statement should be skipped. - // - // This is necessary because some checks are inserted before the source instruction, which, in - // turn, gets moved to the next basic block. Hence, we would not need to look at the - // instruction again as a part of new basic block. However, if the check is inserted after the - // source instruction, we still need to look at the first statement of the new basic block, so - // we need to keep track of which basic blocks were created as a part of injecting checks after - // the source instruction. - let mut skip_first = HashSet::new(); - // Do not cache body.blocks().len() since it will change as we add new checks. let mut bb_idx = 0; while bb_idx < body.blocks().len() { - if let Some(candidate) = - target_finder.find_next(&body, bb_idx, skip_first.contains(&bb_idx)) - { - self.build_check_for_instruction(tcx, &mut body, candidate, &mut skip_first); - bb_idx += 1 - } else { - bb_idx += 1; - }; + // Skip instrumentation of autogenerated blocks. + if !self.autogenerated_bbs.contains(&bb_idx) { + if let Some(candidate) = + target_finder.find_next(&body, bb_idx, self.skip_first.contains(&bb_idx)) + { + self.build_check_for_instruction(&mut body, candidate); + } + } + bb_idx += 1; } (orig_len != body.blocks().len(), body) } @@ -112,40 +140,39 @@ impl<'a> UninitInstrumenter<'a> { /// Inject memory initialization checks for each operation in an instruction. fn build_check_for_instruction( &mut self, - tcx: TyCtxt, body: &mut MutableBody, instruction: InitRelevantInstruction, - skip_first: &mut HashSet, ) { let mut source = instruction.source; for operation in instruction.before_instruction { - self.build_check_for_operation(tcx, body, &mut source, operation, skip_first); + self.build_check_for_operation(body, &mut source, operation); } for operation in instruction.after_instruction { - self.build_check_for_operation(tcx, body, &mut source, operation, skip_first); + self.build_check_for_operation(body, &mut source, operation); } } /// Inject memory initialization check for an operation. fn build_check_for_operation( &mut self, - tcx: TyCtxt, body: &mut MutableBody, source: &mut SourceInstruction, operation: MemoryInitOp, - skip_first: &mut HashSet, ) { if let MemoryInitOp::Unsupported { reason } | MemoryInitOp::TriviallyUnsafe { reason } = &operation { - collect_skipped(&operation, body, skip_first); - self.inject_assert_false(tcx, body, source, operation.position(), reason); + // If the operation is unsupported or trivially accesses uninitialized memory, encode + // the check as `assert!(false)`. + collect_skipped(operation.position(), source, body, &mut self.skip_first); + self.inject_assert_false(self.tcx, body, source, operation.position(), reason); return; }; - let pointee_ty_info = { - let ptr_operand = operation.mk_operand(body, source); - let ptr_operand_ty = ptr_operand.ty(body.locals()).unwrap(); + let pointee_info = { + // Sanity check: since CBMC memory object primitives only accept pointers, need to + // ensure the correct type. + let ptr_operand_ty = operation.operand_ty(body); let pointee_ty = match ptr_operand_ty.kind() { TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) => pointee_ty, _ => { @@ -154,55 +181,55 @@ impl<'a> UninitInstrumenter<'a> { ) } }; + // Calculate pointee layout for byte-by-byte memory initialization checks. match PointeeInfo::from_ty(pointee_ty) { Ok(type_info) => type_info, Err(_) => { let reason = format!( "Kani currently doesn't support checking memory initialization for pointers to `{pointee_ty}.", ); - collect_skipped(&operation, body, skip_first); - self.inject_assert_false(tcx, body, source, operation.position(), &reason); + collect_skipped(operation.position(), source, body, &mut self.skip_first); + self.inject_assert_false(self.tcx, body, source, operation.position(), &reason); return; } } }; - match operation { + match &operation { MemoryInitOp::CheckSliceChunk { .. } | MemoryInitOp::Check { .. } | MemoryInitOp::CheckRef { .. } => { - self.build_get_and_check(tcx, body, source, operation, pointee_ty_info, skip_first) + self.build_get_and_check(body, source, operation, pointee_info) } MemoryInitOp::SetSliceChunk { .. } | MemoryInitOp::Set { .. } - | MemoryInitOp::SetRef { .. } => { - self.build_set(tcx, body, source, operation, pointee_ty_info, skip_first) - } + | MemoryInitOp::SetRef { .. } => self.build_set(body, source, operation, pointee_info), MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => { unreachable!() } - } + }; } /// Inject a load from memory initialization state and an assertion that all non-padding bytes /// are initialized. fn build_get_and_check( &mut self, - tcx: TyCtxt, body: &mut MutableBody, source: &mut SourceInstruction, operation: MemoryInitOp, pointee_info: PointeeInfo, - skip_first: &mut HashSet, ) { let ret_place = Place { local: body.new_local(Ty::bool_ty(), source.span(body.blocks()), Mutability::Not), projection: vec![], }; - let ptr_operand = operation.mk_operand(body, source); - match pointee_info.layout() { + // Instead of injecting the instrumentation immediately, collect it into a list of + // statements and a terminator to construct a basic block and inject it at the end. + let mut statements = vec![]; + let ptr_operand = operation.mk_operand(body, &mut statements, source); + let terminator = match pointee_info.layout() { PointeeLayout::Sized { layout } => { - let layout_operand = mk_layout_operand(body, source, operation.position(), &layout); + let layout_operand = mk_layout_operand(body, &mut statements, source, &layout); // Depending on whether accessing the known number of elements in the slice, need to // pass is as an argument. let (diagnostic, args) = match &operation { @@ -220,18 +247,24 @@ impl<'a> UninitInstrumenter<'a> { _ => unreachable!(), }; let is_ptr_initialized_instance = resolve_mem_init_fn( - get_mem_init_fn_def(tcx, diagnostic, &mut self.mem_init_fn_cache), + get_mem_init_fn_def(self.tcx, diagnostic, &mut self.mem_init_fn_cache), layout.len(), *pointee_info.ty(), ); - collect_skipped(&operation, body, skip_first); - body.insert_call( - &is_ptr_initialized_instance, - source, - operation.position(), - args, - ret_place.clone(), - ); + Terminator { + kind: TerminatorKind::Call { + func: Operand::Copy(Place::from(body.new_local( + is_ptr_initialized_instance.ty(), + source.span(body.blocks()), + Mutability::Not, + ))), + args, + destination: ret_place.clone(), + target: Some(0), // The current value does not matter, since it will be overwritten in add_bb. + unwind: UnwindAction::Terminate, + }, + span: source.span(body.blocks()), + } } PointeeLayout::Slice { element_layout } => { // Since `str`` is a separate type, need to differentiate between [T] and str. @@ -245,32 +278,43 @@ impl<'a> UninitInstrumenter<'a> { _ => unreachable!(), }; let is_ptr_initialized_instance = resolve_mem_init_fn( - get_mem_init_fn_def(tcx, diagnostic, &mut self.mem_init_fn_cache), + get_mem_init_fn_def(self.tcx, diagnostic, &mut self.mem_init_fn_cache), element_layout.len(), slicee_ty, ); let layout_operand = - mk_layout_operand(body, source, operation.position(), &element_layout); - collect_skipped(&operation, body, skip_first); - body.insert_call( - &is_ptr_initialized_instance, - source, - operation.position(), - vec![ptr_operand.clone(), layout_operand], - ret_place.clone(), - ); + mk_layout_operand(body, &mut statements, source, &element_layout); + Terminator { + kind: TerminatorKind::Call { + func: Operand::Copy(Place::from(body.new_local( + is_ptr_initialized_instance.ty(), + source.span(body.blocks()), + Mutability::Not, + ))), + args: vec![ptr_operand.clone(), layout_operand], + destination: ret_place.clone(), + target: Some(0), // The current value does not matter, since it will be overwritten in add_bb. + unwind: UnwindAction::Terminate, + }, + span: source.span(body.blocks()), + } } PointeeLayout::TraitObject => { - collect_skipped(&operation, body, skip_first); + collect_skipped(operation.position(), source, body, &mut self.skip_first); let reason = "Kani does not support reasoning about memory initialization of pointers to trait objects."; - self.inject_assert_false(tcx, body, source, operation.position(), reason); + self.inject_assert_false(self.tcx, body, source, operation.position(), reason); return; } }; - // Make sure all non-padding bytes are initialized. - collect_skipped(&operation, body, skip_first); - // Find the real operand type for a good error message. + // Construct the basic block and insert it into the body. + collect_skipped(operation.position(), source, body, &mut self.skip_first); + body.insert_bb(BasicBlock { statements, terminator }, source, operation.position()); + self.autogenerated_bbs.insert(body.blocks().len() - 1); + + // Since the check involves a terminator, we cannot add it to the previously constructed + // basic block. Instead, we insert the check after the basic block. + collect_skipped(operation.position(), source, body, &mut self.skip_first); let operand_ty = match &operation { MemoryInitOp::Check { operand } | MemoryInitOp::CheckSliceChunk { operand, .. } @@ -278,7 +322,7 @@ impl<'a> UninitInstrumenter<'a> { _ => unreachable!(), }; body.insert_check( - tcx, + self.tcx, &self.check_type, source, operation.position(), @@ -293,23 +337,24 @@ impl<'a> UninitInstrumenter<'a> { /// non-padding bytes. fn build_set( &mut self, - tcx: TyCtxt, body: &mut MutableBody, source: &mut SourceInstruction, operation: MemoryInitOp, pointee_info: PointeeInfo, - skip_first: &mut HashSet, ) { let ret_place = Place { local: body.new_local(Ty::new_tuple(&[]), source.span(body.blocks()), Mutability::Not), projection: vec![], }; - let ptr_operand = operation.mk_operand(body, source); - let value = operation.expect_value(); - match pointee_info.layout() { + // Instead of injecting the instrumentation immediately, collect it into a list of + // statements and a terminator to construct a basic block and inject it at the end. + let mut statements = vec![]; + let ptr_operand = operation.mk_operand(body, &mut statements, source); + let value = operation.expect_value(); + let terminator = match pointee_info.layout() { PointeeLayout::Sized { layout } => { - let layout_operand = mk_layout_operand(body, source, operation.position(), &layout); + let layout_operand = mk_layout_operand(body, &mut statements, source, &layout); // Depending on whether writing to the known number of elements in the slice, need to // pass is as an argument. let (diagnostic, args) = match &operation { @@ -343,18 +388,24 @@ impl<'a> UninitInstrumenter<'a> { _ => unreachable!(), }; let set_ptr_initialized_instance = resolve_mem_init_fn( - get_mem_init_fn_def(tcx, diagnostic, &mut self.mem_init_fn_cache), + get_mem_init_fn_def(self.tcx, diagnostic, &mut self.mem_init_fn_cache), layout.len(), *pointee_info.ty(), ); - collect_skipped(&operation, body, skip_first); - body.insert_call( - &set_ptr_initialized_instance, - source, - operation.position(), - args, - ret_place, - ); + 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()), + } } PointeeLayout::Slice { element_layout } => { // Since `str`` is a separate type, need to differentiate between [T] and str. @@ -368,33 +419,43 @@ impl<'a> UninitInstrumenter<'a> { _ => unreachable!(), }; let set_ptr_initialized_instance = resolve_mem_init_fn( - get_mem_init_fn_def(tcx, diagnostic, &mut self.mem_init_fn_cache), + get_mem_init_fn_def(self.tcx, diagnostic, &mut self.mem_init_fn_cache), element_layout.len(), slicee_ty, ); let layout_operand = - mk_layout_operand(body, source, operation.position(), &element_layout); - collect_skipped(&operation, body, skip_first); - body.insert_call( - &set_ptr_initialized_instance, - source, - operation.position(), - vec![ - ptr_operand, - layout_operand, - Operand::Constant(ConstOperand { - span: source.span(body.blocks()), - user_ty: None, - const_: MirConst::from_bool(value), - }), - ], - ret_place, - ); + mk_layout_operand(body, &mut statements, source, &element_layout); + Terminator { + kind: TerminatorKind::Call { + func: Operand::Copy(Place::from(body.new_local( + set_ptr_initialized_instance.ty(), + source.span(body.blocks()), + Mutability::Not, + ))), + args: vec![ + ptr_operand, + layout_operand, + Operand::Constant(ConstOperand { + span: source.span(body.blocks()), + user_ty: None, + const_: MirConst::from_bool(value), + }), + ], + destination: ret_place.clone(), + target: Some(0), // The current value does not matter, since it will be overwritten in add_bb. + unwind: UnwindAction::Terminate, + }, + span: source.span(body.blocks()), + } } PointeeLayout::TraitObject => { unreachable!("Cannot change the initialization state of a trait object directly."); } }; + // Construct the basic block and insert it into the body. + collect_skipped(operation.position(), source, body, &mut self.skip_first); + body.insert_bb(BasicBlock { statements, terminator }, source, operation.position()); + self.autogenerated_bbs.insert(body.blocks().len() - 1); } fn inject_assert_false( @@ -430,36 +491,43 @@ impl<'a> UninitInstrumenter<'a> { /// will have the following byte mask `[true, true, true, false]`. pub fn mk_layout_operand( body: &mut MutableBody, + statements: &mut Vec, source: &mut SourceInstruction, - position: InsertPosition, layout_byte_mask: &[bool], ) -> Operand { - Operand::Move(Place { - local: body.insert_assignment( - Rvalue::Aggregate( - AggregateKind::Array(Ty::bool_ty()), - layout_byte_mask - .iter() - .map(|byte| { - Operand::Constant(ConstOperand { - span: source.span(body.blocks()), - user_ty: None, - const_: MirConst::from_bool(*byte), - }) - }) - .collect(), - ), - source, - position, - ), - projection: vec![], - }) + let span = source.span(body.blocks()); + let rvalue = Rvalue::Aggregate( + AggregateKind::Array(Ty::bool_ty()), + layout_byte_mask + .iter() + .map(|byte| { + Operand::Constant(ConstOperand { + span: source.span(body.blocks()), + user_ty: None, + const_: MirConst::from_bool(*byte), + }) + }) + .collect(), + ); + 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); + + Operand::Move(Place { local: result, projection: vec![] }) } /// If injecting a new call to the function before the current statement, need to skip the original /// statement when analyzing it as a part of the new basic block. -fn collect_skipped(operation: &MemoryInitOp, body: &MutableBody, skip_first: &mut HashSet) { - if operation.position() == InsertPosition::Before { +fn collect_skipped( + position: InsertPosition, + source: &SourceInstruction, + body: &MutableBody, + skip_first: &mut HashSet, +) { + if position == InsertPosition::Before + || (position == InsertPosition::After && source.is_terminator()) + { let new_bb_idx = body.blocks().len(); skip_first.insert(new_bb_idx); } diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs index af2753ea7175..37f1d94ed744 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs @@ -62,14 +62,16 @@ impl TransformPass for UninitPass { } // Call a helper that performs the actual instrumentation. - let mut instrumenter = UninitInstrumenter { - check_type: self.check_type.clone(), - mem_init_fn_cache: &mut self.mem_init_fn_cache, - }; - let (instrumentation_added, body) = - instrumenter.instrument(tcx, new_body, instance, CheckUninitVisitor::new()); + let (instrumentation_added, body) = UninitInstrumenter::run( + new_body.into(), + tcx, + instance, + self.check_type.clone(), + &mut self.mem_init_fn_cache, + CheckUninitVisitor::new(), + ); - (changed || instrumentation_added, body.into()) + (changed || instrumentation_added, body) } } 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 3bc5b534a23b..dbee561df516 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 @@ -5,7 +5,10 @@ //! character of instrumentation needed. use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; -use stable_mir::mir::{Mutability, Operand, Place, Rvalue}; +use stable_mir::{ + mir::{Mutability, Operand, Place, Rvalue, Statement, StatementKind}, + ty::Ty, +}; use strum_macros::AsRefStr; /// Memory initialization operations: set or get memory initialization state for a given pointer. @@ -39,27 +42,57 @@ impl MemoryInitOp { /// Produce an operand for the relevant memory initialization related operation. This is mostly /// required so that the analysis can create a new local to take a reference in /// `MemoryInitOp::SetRef`. - pub fn mk_operand(&self, body: &mut MutableBody, source: &mut SourceInstruction) -> Operand { + pub fn mk_operand( + &self, + body: &mut MutableBody, + statements: &mut Vec, + source: &mut SourceInstruction, + ) -> Operand { match self { MemoryInitOp::Check { operand, .. } | MemoryInitOp::Set { operand, .. } | MemoryInitOp::CheckSliceChunk { operand, .. } | MemoryInitOp::SetSliceChunk { operand, .. } => operand.clone(), MemoryInitOp::CheckRef { operand, .. } | MemoryInitOp::SetRef { operand, .. } => { - Operand::Copy(Place { - local: { - let place = match operand { - Operand::Copy(place) | Operand::Move(place) => place, - Operand::Constant(_) => unreachable!(), - }; - body.insert_assignment( - Rvalue::AddressOf(Mutability::Not, place.clone()), - source, - self.position(), - ) - }, - projection: vec![], - }) + 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::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => { + 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, .. } => { + let place = match operand { + Operand::Copy(place) | Operand::Move(place) => place, + Operand::Constant(_) => unreachable!(), + }; + let rvalue = Rvalue::AddressOf(Mutability::Not, place.clone()); + rvalue.ty(body.locals()).unwrap() } MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => { unreachable!() diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index cc748c39a7f5..2b9d6d22f040 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -22,8 +22,8 @@ use crate::kani_queries::QueryDb; use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::Instance; use stable_mir::mir::{ - BinOp, Body, ConstOperand, Operand, Place, Rvalue, Statement, StatementKind, TerminatorKind, - RETURN_LOCAL, + BasicBlock, BinOp, Body, ConstOperand, Mutability, Operand, Place, Rvalue, Statement, + StatementKind, Terminator, TerminatorKind, UnwindAction, RETURN_LOCAL, }; use stable_mir::target::MachineInfo; use stable_mir::ty::{FnDef, MirConst, RigidTy, Ty, TyKind, UintTy}; @@ -164,30 +164,40 @@ impl IntrinsicGeneratorPass { fn is_initialized_body(&mut self, tcx: TyCtxt, body: Body) -> Body { let mut new_body = MutableBody::from(body); new_body.clear_body(TerminatorKind::Return); - - // Initialize return variable with True. let ret_var = RETURN_LOCAL; - let mut terminator = SourceInstruction::Terminator { bb: 0 }; - let span = new_body.locals()[ret_var].span; - let assign = StatementKind::Assign( - Place::from(ret_var), - Rvalue::Use(Operand::Constant(ConstOperand { - span, - user_ty: None, - const_: MirConst::from_bool(true), - })), - ); - let stmt = Statement { kind: assign, span }; - new_body.insert_stmt(stmt, &mut terminator, InsertPosition::Before); + let mut source = SourceInstruction::Terminator { bb: 0 }; + // Short-circut if uninitialized memory checks are not enabled. if !self.arguments.ub_check.contains(&ExtraChecks::Uninit) { - // Short-circut if uninitialized memory checks are not enabled. + // Initialize return variable with True. + let span = new_body.locals()[ret_var].span; + let assign = StatementKind::Assign( + Place::from(ret_var), + Rvalue::Use(Operand::Constant(ConstOperand { + span, + user_ty: None, + const_: MirConst::from_bool(true), + })), + ); + new_body.insert_stmt( + Statement { kind: assign, span }, + &mut source, + InsertPosition::Before, + ); return new_body.into(); } + // Instead of injecting the instrumentation immediately, collect it into a list of + // statements and a terminator to construct a basic block and inject it at the end. + let mut statements = vec![]; + let terminator; + // The first argument type. let arg_ty = new_body.locals()[1].ty; + // Sanity check: since CBMC memory object primitives only accept pointers, need to + // ensure the correct type. let TyKind::RigidTy(RigidTy::RawPtr(target_ty, _)) = arg_ty.kind() else { unreachable!() }; + // Calculate pointee layout for byte-by-byte memory initialization checks. let pointee_info = PointeeInfo::from_ty(target_ty); match pointee_info { Ok(pointee_info) => { @@ -195,6 +205,21 @@ impl IntrinsicGeneratorPass { PointeeLayout::Sized { layout } => { if layout.is_empty() { // Encountered a ZST, so we can short-circut here. + // Initialize return variable with True. + let span = new_body.locals()[ret_var].span; + let assign = StatementKind::Assign( + Place::from(ret_var), + Rvalue::Use(Operand::Constant(ConstOperand { + span, + user_ty: None, + const_: MirConst::from_bool(true), + })), + ); + new_body.insert_stmt( + Statement { kind: assign, span }, + &mut source, + InsertPosition::Before, + ); return new_body.into(); } let is_ptr_initialized_instance = resolve_mem_init_fn( @@ -206,18 +231,28 @@ impl IntrinsicGeneratorPass { layout.len(), *pointee_info.ty(), ); - let layout_operand = mk_layout_operand( - &mut new_body, - &mut terminator, - InsertPosition::Before, - &layout, - ); - new_body.insert_call( - &is_ptr_initialized_instance, - &mut terminator, + let layout_operand = + mk_layout_operand(&mut new_body, &mut statements, &mut source, &layout); + + terminator = Terminator { + kind: TerminatorKind::Call { + func: Operand::Copy(Place::from(new_body.new_local( + is_ptr_initialized_instance.ty(), + source.span(new_body.blocks()), + Mutability::Not, + ))), + args: vec![Operand::Copy(Place::from(1)), layout_operand], + destination: Place::from(ret_var), + target: Some(0), // The current value does not matter, since it will be overwritten in add_bb. + unwind: UnwindAction::Terminate, + }, + span: source.span(new_body.blocks()), + }; + // Construct the basic block and insert it into the body. + new_body.insert_bb( + BasicBlock { statements, terminator }, + &mut source, InsertPosition::Before, - vec![Operand::Copy(Place::from(1)), layout_operand], - Place::from(ret_var), ); } PointeeLayout::Slice { element_layout } => { @@ -238,35 +273,45 @@ impl IntrinsicGeneratorPass { ); let layout_operand = mk_layout_operand( &mut new_body, - &mut terminator, - InsertPosition::Before, + &mut statements, + &mut source, &element_layout, ); - new_body.insert_call( - &is_ptr_initialized_instance, - &mut terminator, + terminator = Terminator { + kind: TerminatorKind::Call { + func: Operand::Copy(Place::from(new_body.new_local( + is_ptr_initialized_instance.ty(), + source.span(new_body.blocks()), + Mutability::Not, + ))), + args: vec![Operand::Copy(Place::from(1)), layout_operand], + destination: Place::from(ret_var), + target: Some(0), // The current value does not matter, since it will be overwritten in add_bb. + unwind: UnwindAction::Terminate, + }, + span: source.span(new_body.blocks()), + }; + // Construct the basic block and insert it into the body. + new_body.insert_bb( + BasicBlock { statements, terminator }, + &mut source, InsertPosition::Before, - vec![Operand::Copy(Place::from(1)), layout_operand], - Place::from(ret_var), ); } PointeeLayout::TraitObject => { let rvalue = Rvalue::Use(Operand::Constant(ConstOperand { const_: MirConst::from_bool(false), - span, + span: source.span(new_body.blocks()), user_ty: None, })); - let result = new_body.insert_assignment( - rvalue, - &mut terminator, - InsertPosition::Before, - ); + let result = + 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 terminator, + &mut source, InsertPosition::Before, result, &reason, @@ -278,18 +323,18 @@ impl IntrinsicGeneratorPass { // We failed to retrieve the type layout. let rvalue = Rvalue::Use(Operand::Constant(ConstOperand { const_: MirConst::from_bool(false), - span, + span: source.span(new_body.blocks()), user_ty: None, })); let result = - new_body.insert_assignment(rvalue, &mut terminator, InsertPosition::Before); + new_body.insert_assignment(rvalue, &mut source, InsertPosition::Before); let reason = format!( "Kani currently doesn't support checking memory initialization of `{target_ty}`. {msg}" ); new_body.insert_check( tcx, &self.check_type, - &mut terminator, + &mut source, InsertPosition::Before, result, &reason, From 63f29b649c0b2a44f68c0298f05b50cc6512415c Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 14 Aug 2024 14:56:00 -0700 Subject: [PATCH 02/15] Implement memory initialization state copy functionality --- .../kani_middle/transform/check_uninit/mod.rs | 37 +++++++- .../check_uninit/ptr_uninit/uninit_visitor.rs | 37 +++----- .../check_uninit/relevant_instruction.rs | 31 ++++++- library/kani/src/mem_init.rs | 40 +++++++++ tests/expected/uninit/copy/copy.rs | 87 +++++++++++++++++++ tests/expected/uninit/copy/expected | 31 +++++++ tests/expected/uninit/intrinsics/expected | 12 +-- .../expected/uninit/intrinsics/intrinsics.rs | 30 ++++++- 8 files changed, 266 insertions(+), 39 deletions(-) create mode 100644 tests/expected/uninit/copy/copy.rs create mode 100644 tests/expected/uninit/copy/expected 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 cca33b902ed9..c951e5835e2d 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -203,7 +203,12 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { } MemoryInitOp::SetSliceChunk { .. } | MemoryInitOp::Set { .. } - | MemoryInitOp::SetRef { .. } => self.build_set(body, source, operation, pointee_info), + | MemoryInitOp::SetRef { .. } => { + self.build_set(body, source, operation, pointee_info) + } + MemoryInitOp::Copy { .. } => { + self.build_copy(body, source, operation, pointee_info) + } MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => { unreachable!() } @@ -458,6 +463,36 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { self.autogenerated_bbs.insert(body.blocks().len() - 1); } + /// Copy memory initialization state from one pointer to the other. + fn build_copy( + &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 PointeeLayout::Sized { layout } = pointee_info.layout() else { unreachable!() }; + 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(), + *pointee_info.ty(), + ); + collect_skipped(operation.position(), source, body, &mut self.skip_first); + let position = operation.position(); + let MemoryInitOp::Copy { from, to, count } = operation else { unreachable!() }; + body.insert_call( + ©_init_state_instance, + source, + position, + vec![from, to, count], + ret_place.clone(), + ); + } + 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 f682f93a261e..910e4d938d41 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 @@ -88,18 +88,12 @@ impl MirVisitor for CheckUninitVisitor { match &stmt.kind { StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping(copy)) => { self.super_statement(stmt, location); - // Source is a *const T and it must be initialized. - self.push_target(MemoryInitOp::CheckSliceChunk { - operand: copy.src.clone(), + // 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(), }); - // Destination is a *mut T so it gets initialized. - self.push_target(MemoryInitOp::SetSliceChunk { - operand: copy.dst.clone(), - count: copy.count.clone(), - value: true, - position: InsertPosition::After, - }); } StatementKind::Assign(place, rvalue) => { // First check rvalue. @@ -219,29 +213,20 @@ impl MirVisitor for CheckUninitVisitor { }); } Intrinsic::Copy => { - self.push_target(MemoryInitOp::CheckSliceChunk { - operand: args[0].clone(), + // Copy memory initialization state from `src` to `dst`. + self.push_target(MemoryInitOp::Copy { + from: args[0].clone(), + to: args[1].clone(), count: args[2].clone(), }); - self.push_target(MemoryInitOp::SetSliceChunk { - operand: args[1].clone(), - count: args[2].clone(), - value: true, - position: InsertPosition::After, - }); } Intrinsic::VolatileCopyMemory | Intrinsic::VolatileCopyNonOverlappingMemory => { - self.push_target(MemoryInitOp::CheckSliceChunk { - operand: args[1].clone(), + self.push_target(MemoryInitOp::Copy { + from: args[1].clone(), + to: args[0].clone(), count: args[2].clone(), }); - self.push_target(MemoryInitOp::SetSliceChunk { - operand: args[0].clone(), - count: args[2].clone(), - value: true, - position: InsertPosition::After, - }); } Intrinsic::TypedSwap => { self.push_target(MemoryInitOp::Check { 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 dbee561df516..aa3df515809e 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 @@ -7,6 +7,7 @@ use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; use stable_mir::{ mir::{Mutability, Operand, Place, Rvalue, Statement, StatementKind}, + ty::RigidTy, ty::Ty, }; use strum_macros::AsRefStr; @@ -36,6 +37,8 @@ pub enum MemoryInitOp { Unsupported { reason: String }, /// Operation that trivially accesses uninitialized memory, results in injecting `assert!(false)`. TriviallyUnsafe { reason: String }, + /// Operation that copies memory initialization state over to another operand. + Copy { from: Operand, to: Operand, count: Operand }, } impl MemoryInitOp { @@ -74,7 +77,9 @@ impl MemoryInitOp { Operand::Copy(Place { local: ref_local, projection: vec![] }) } - MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => { + MemoryInitOp::Copy { .. } + | MemoryInitOp::Unsupported { .. } + | MemoryInitOp::TriviallyUnsafe { .. } => { unreachable!() } } @@ -95,7 +100,22 @@ impl MemoryInitOp { rvalue.ty(body.locals()).unwrap() } MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => { - unreachable!() + unreachable!("operands do not exist for this operation") + } + MemoryInitOp::Copy { from, to, .. } => { + // It does not matter which operand to return for layout generation, since both of + // them have the same pointee type, so we assert that. + let from_kind = from.ty(body.locals()).unwrap().kind(); + let to_kind = to.ty(body.locals()).unwrap().kind(); + + let RigidTy::RawPtr(from_pointee_ty, _) = from_kind.rigid().unwrap().clone() else { + unreachable!() + }; + let RigidTy::RawPtr(to_pointee_ty, _) = to_kind.rigid().unwrap().clone() else { + unreachable!() + }; + assert!(from_pointee_ty == to_pointee_ty); + from_pointee_ty } } } @@ -103,7 +123,8 @@ impl MemoryInitOp { pub fn expect_count(&self) -> Operand { match self { MemoryInitOp::CheckSliceChunk { count, .. } - | MemoryInitOp::SetSliceChunk { count, .. } => count.clone(), + | MemoryInitOp::SetSliceChunk { count, .. } + | MemoryInitOp::Copy { count, .. } => count.clone(), MemoryInitOp::Check { .. } | MemoryInitOp::Set { .. } | MemoryInitOp::CheckRef { .. } @@ -122,7 +143,8 @@ impl MemoryInitOp { | MemoryInitOp::CheckSliceChunk { .. } | MemoryInitOp::CheckRef { .. } | MemoryInitOp::Unsupported { .. } - | MemoryInitOp::TriviallyUnsafe { .. } => unreachable!(), + | MemoryInitOp::TriviallyUnsafe { .. } + | MemoryInitOp::Copy { .. } => unreachable!(), } } @@ -136,6 +158,7 @@ impl MemoryInitOp { | MemoryInitOp::CheckRef { .. } | MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => InsertPosition::Before, + MemoryInitOp::Copy { .. } => InsertPosition::After, } } } diff --git a/library/kani/src/mem_init.rs b/library/kani/src/mem_init.rs index 88847e9c4f3c..3755fc59a510 100644 --- a/library/kani/src/mem_init.rs +++ b/library/kani/src/mem_init.rs @@ -91,6 +91,33 @@ impl MemoryInitializationState { } } + /// Copy memory initialization state by non-deterministically switching the tracked object and + /// adjusting the tracked offset. + pub fn copy( + &mut self, + from_ptr: *const u8, + to_ptr: *const u8, + num_elts: usize, + ) { + let from_obj = crate::mem::pointer_object(from_ptr); + let from_offset = crate::mem::pointer_offset(from_ptr); + + let to_obj = crate::mem::pointer_object(to_ptr); + let to_offset = crate::mem::pointer_offset(to_ptr); + + if self.tracked_object_id == from_obj + && self.tracked_offset >= from_offset + && self.tracked_offset < from_offset + num_elts * LAYOUT_SIZE + { + let should_reset: bool = crate::any(); + if should_reset { + self.tracked_object_id = to_obj; + self.tracked_offset += to_offset - from_offset; + // Note that this preserves the value. + } + } + } + /// Return currently tracked memory initialization state if `ptr` points to the currently /// tracked object and the tracked offset lies within `LAYOUT_SIZE * num_elts` bytes of `ptr`. /// Return `true` otherwise. @@ -281,3 +308,16 @@ fn set_str_ptr_initialized( MEM_INIT_STATE.set_slice(ptr as *const u8, layout, num_elts, value); } } + +/// Copy initialization state of `size_of:: * num_elts` bytes from one pointer to the other. +#[rustc_diagnostic_item = "KaniCopyInitState"] +fn copy_init_state(from: *const T, to: *const T, num_elts: usize) { + if LAYOUT_SIZE == 0 { + return; + } + let (from_ptr, _) = from.to_raw_parts(); + let (to_ptr, _) = to.to_raw_parts(); + unsafe { + MEM_INIT_STATE.copy::(from_ptr as *const u8, to_ptr as *const u8, num_elts); + } +} diff --git a/tests/expected/uninit/copy/copy.rs b/tests/expected/uninit/copy/copy.rs new file mode 100644 index 000000000000..8d8278a6f0b9 --- /dev/null +++ b/tests/expected/uninit/copy/copy.rs @@ -0,0 +1,87 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks + +#[repr(C)] +#[derive(kani::Arbitrary)] +struct S(u32, u8); // 5 bytes of data + 3 bytes of padding. + +#[kani::proof] +/// This checks that reading copied uninitialized bytes fails an assertion. +unsafe fn expose_padding_via_copy() { + let from: S = kani::any(); + let mut to: u64 = kani::any(); + + let from_ptr = &from as *const S; + let to_ptr = &mut to as *mut u64; + + // This should not cause UB since `copy` is untyped. + std::ptr::copy(from_ptr as *const u8, to_ptr as *mut u8, std::mem::size_of::()); + + // This reads uninitialized bytes, which is UB. + let padding: u64 = std::ptr::read(to_ptr); +} + +#[kani::proof] +/// This checks that reading copied uninitialized bytes after a multi-byte copy fails an assertion. +unsafe fn expose_padding_via_non_byte_copy() { + let from: S = kani::any(); + let mut to: u64 = kani::any(); + + let from_ptr = &from as *const S; + let to_ptr = &mut to as *mut u64; + + // This should not cause UB since `copy` is untyped. + std::ptr::copy(from_ptr as *const u64, to_ptr as *mut u64, 1); + + // This reads uninitialized bytes, which is UB. + let padding: u64 = std::ptr::read(to_ptr); +} + +#[kani::proof] +/// This checks that reading copied initialized bytes verifies correctly. +unsafe fn copy_without_padding() { + let from: S = kani::any(); + let mut to: u64 = kani::any(); + + let from_ptr = &from as *const S; + let to_ptr = &mut to as *mut u64; + + // This should not cause UB since `copy` is untyped. + std::ptr::copy(from_ptr as *const u8, to_ptr as *mut u8, std::mem::size_of::()); + + // Since the previous copy only copied 4 bytes, no padding was copied, so no padding is read. + let data: u64 = std::ptr::read(to_ptr); +} + +#[kani::proof] +/// This checks that reading copied initialized bytes after a multi-byte copy verifies correctly. +unsafe fn non_byte_copy_without_padding() { + let from: S = kani::any(); + let mut to: u64 = kani::any(); + + let from_ptr = &from as *const S; + let to_ptr = &mut to as *mut u64; + + // This should not cause UB since `copy` is untyped. + std::ptr::copy(from_ptr as *const u32, to_ptr as *mut u32, 1); + + // Since the previous copy only copied 4 bytes, no padding was copied, so no padding is read. + let data: u64 = std::ptr::read(to_ptr); +} + +#[kani::proof] +/// This checks that reading uninitialized bytes fails an assertion even after copy. +unsafe fn read_after_copy() { + let from: S = kani::any(); + let mut to: u64 = kani::any(); + + let from_ptr = &from as *const S; + let to_ptr = &mut to as *mut u64; + + // This should not cause UB since `copy` is untyped. + std::ptr::copy(from_ptr as *const u8, to_ptr as *mut u8, std::mem::size_of::()); + + // Reading padding from the previous place should be UB even after copy. + let data: u64 = std::ptr::read(from_ptr as *const u64); +} diff --git a/tests/expected/uninit/copy/expected b/tests/expected/uninit/copy/expected new file mode 100644 index 000000000000..a288f9f2856d --- /dev/null +++ b/tests/expected/uninit/copy/expected @@ -0,0 +1,31 @@ +Checking harness read_after_copy... + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u64` + +VERIFICATION:- FAILED + +Checking harness non_byte_copy_without_padding... + +VERIFICATION:- SUCCESSFUL + +Checking harness copy_without_padding... + +VERIFICATION:- SUCCESSFUL + +Checking harness expose_padding_via_non_byte_copy... + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u64` + +VERIFICATION:- FAILED + +Checking harness expose_padding_via_copy... + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u64` + +VERIFICATION:- FAILED + +Summary: +Verification failed for - read_after_copy +Verification failed for - expose_padding_via_non_byte_copy +Verification failed for - expose_padding_via_copy +Complete - 2 successfully verified harnesses, 3 failures, 5 total. diff --git a/tests/expected/uninit/intrinsics/expected b/tests/expected/uninit/intrinsics/expected index cf34d305608b..e428aa605887 100644 --- a/tests/expected/uninit/intrinsics/expected +++ b/tests/expected/uninit/intrinsics/expected @@ -34,19 +34,19 @@ check_compare_bytes.assertion.2\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`" -std::intrinsics::copy::.assertion.1\ +std::ptr::read::.assertion.1\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`" -std::intrinsics::copy_nonoverlapping::.assertion.1\ +std::ptr::read::.assertion.2\ - Status: FAILURE\ - - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`" + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u8`" Summary: Verification failed for - check_typed_swap_safe Verification failed for - check_typed_swap Verification failed for - check_volatile_load Verification failed for - check_compare_bytes -Verification failed for - check_copy -Verification failed for - check_copy_nonoverlapping -Complete - 5 successfully verified harnesses, 6 failures, 11 total. +Verification failed for - check_copy_read +Verification failed for - check_copy_nonoverlapping_read +Complete - 7 successfully verified harnesses, 6 failures, 13 total. diff --git a/tests/expected/uninit/intrinsics/intrinsics.rs b/tests/expected/uninit/intrinsics/intrinsics.rs index aa8a89b7b959..b023853b2fbc 100644 --- a/tests/expected/uninit/intrinsics/intrinsics.rs +++ b/tests/expected/uninit/intrinsics/intrinsics.rs @@ -14,7 +14,20 @@ fn check_copy_nonoverlapping() { let layout = Layout::from_size_align(16, 8).unwrap(); let src: *mut u8 = alloc(layout); let dst: *mut u8 = alloc(layout); - copy_nonoverlapping(src as *const u8, dst, 2); // ~ERROR: Accessing `src` here, which is uninitialized. + // This does not fail, since `copy_nonoverlapping` is untyped. + copy_nonoverlapping(src as *const u8, dst, 2); + } +} + +#[kani::proof] +fn check_copy_nonoverlapping_read() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let src: *mut u8 = alloc(layout); + let dst: *mut u8 = alloc_zeroed(layout); + copy_nonoverlapping(src as *const u8, dst, 2); + // ~ERROR: Accessing `dst` here, which became uninitialized after copy. + let uninit = std::ptr::read(dst); } } @@ -35,7 +48,20 @@ fn check_copy() { let layout = Layout::from_size_align(16, 8).unwrap(); let src: *mut u8 = alloc(layout); let dst: *mut u8 = alloc(layout); - copy(src as *const u8, dst, 2); // ~ERROR: Accessing `src` here, which is uninitialized. + // This does not fail, since `copy` is untyped. + copy(src as *const u8, dst, 2); + } +} + +#[kani::proof] +fn check_copy_read() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let src: *mut u8 = alloc(layout); + let dst: *mut u8 = alloc_zeroed(layout); + copy(src as *const u8, dst, 2); + // ~ERROR: Accessing `dst` here, which became uninitialized after copy. + let uninit = std::ptr::read(dst); } } From 31059978ba0964b0d008614503051ac0bb94d1b6 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Thu, 15 Aug 2024 16:24:53 -0700 Subject: [PATCH 03/15] Support for basic intra-body memory initialization checks for unions --- .../kani_middle/transform/check_uninit/mod.rs | 125 +++++++++++- .../check_uninit/ptr_uninit/uninit_visitor.rs | 74 ++++++- .../check_uninit/relevant_instruction.rs | 188 +++++++++++++----- .../transform/check_uninit/ty_layout.rs | 43 +++- .../kani_middle/transform/kani_intrinsics.rs | 19 ++ library/kani/src/mem_init.rs | 13 ++ tests/expected/uninit/fixme_unions.rs | 60 ++++++ tests/expected/uninit/unions.expected | 12 ++ tests/expected/uninit/unions.rs | 52 +++++ 9 files changed, 517 insertions(+), 69 deletions(-) create mode 100644 tests/expected/uninit/fixme_unions.rs create mode 100644 tests/expected/uninit/unions.expected create mode 100644 tests/expected/uninit/unions.rs 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 c951e5835e2d..ac1359147320 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -203,11 +203,13 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { } MemoryInitOp::SetSliceChunk { .. } | MemoryInitOp::Set { .. } - | MemoryInitOp::SetRef { .. } => { + | MemoryInitOp::SetRef { .. } + | MemoryInitOp::CreateUnion { .. } => { self.build_set(body, source, operation, pointee_info) } - MemoryInitOp::Copy { .. } => { - self.build_copy(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!() @@ -310,6 +312,15 @@ 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. + collect_skipped(operation.position(), source, body, &mut self.skip_first); + 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. @@ -456,6 +467,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. + + // 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 => { + collect_skipped(operation.position(), source, body, &mut self.skip_first); + 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 = "KaniSetPtrInitialized"; + 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. collect_skipped(operation.position(), source, body, &mut self.skip_first); @@ -475,24 +543,65 @@ 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(), + layout_size, *pointee_info.ty(), ); collect_skipped(operation.position(), source, body, &mut self.skip_first); - 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, - position, + operation.position(), vec![from, to, count], ret_place.clone(), ); } + /// 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, "KaniCopyInitStateSingle", &mut self.mem_init_fn_cache), + layout_size, + *pointee_info.ty(), + ); + let (from, to) = operation.mk_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. + collect_skipped(operation.position(), source, body, &mut self.skip_first); + body.insert_bb(BasicBlock { statements, terminator }, source, operation.position()); + self.autogenerated_bbs.insert(body.blocks().len() - 1); + } + 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 910e4d938d41..c3f68d7043dc 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,11 +19,11 @@ use stable_mir::{ alloc::GlobalAlloc, mono::{Instance, InstanceKind}, visit::{Location, PlaceContext}, - BasicBlockIdx, CastKind, LocalDecl, MirVisitor, NonDivergingIntrinsic, Operand, Place, - PointerCoercion, ProjectionElem, Rvalue, Statement, StatementKind, Terminator, - TerminatorKind, + AggregateKind, BasicBlockIdx, 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 { @@ -127,7 +127,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()), @@ -136,6 +136,59 @@ 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); @@ -352,12 +405,13 @@ 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(), + // 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 aa3df515809e..e1817379e179 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,8 +6,7 @@ use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; use stable_mir::{ - mir::{Mutability, Operand, Place, Rvalue, Statement, StatementKind}, - ty::RigidTy, + mir::{FieldIdx, Mutability, Operand, Place, Rvalue, Statement, StatementKind}, ty::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 mk_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!(), @@ -102,20 +152,16 @@ impl MemoryInitOp { MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => { unreachable!("operands do not exist for this operation") } - MemoryInitOp::Copy { from, to, .. } => { + MemoryInitOp::Copy { from, .. } => { // It does not matter which operand to return for layout generation, since both of - // them have the same pointee type, so we assert that. - let from_kind = from.ty(body.locals()).unwrap().kind(); - let to_kind = to.ty(body.locals()).unwrap().kind(); - - let RigidTy::RawPtr(from_pointee_ty, _) = from_kind.rigid().unwrap().clone() else { - unreachable!() - }; - let RigidTy::RawPtr(to_pointee_ty, _) = to_kind.rigid().unwrap().clone() else { - unreachable!() - }; - assert!(from_pointee_ty == to_pointee_ty); - from_pointee_ty + // them have the same pointee type. + 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 +175,8 @@ impl MemoryInitOp { | MemoryInitOp::Set { .. } | MemoryInitOp::CheckRef { .. } | MemoryInitOp::SetRef { .. } + | MemoryInitOp::CreateUnion { .. } + | MemoryInitOp::AssignUnion { .. } | MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => unreachable!(), } @@ -139,12 +187,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 { .. } + | 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 { .. } => unreachable!(), + | MemoryInitOp::Copy { .. } + | MemoryInitOp::AssignUnion { .. } => None, } } @@ -158,7 +224,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 +252,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 2b9d6d22f040..9f3a8a20283d 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -308,6 +308,25 @@ 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..c2a674c51053 100644 --- a/library/kani/src/mem_init.rs +++ b/library/kani/src/mem_init.rs @@ -321,3 +321,16 @@ 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. +#[rustc_diagnostic_item = "KaniCopyInitStateSingle"] +fn copy_init_state_single(from: *const T, to: *const T) { + if LAYOUT_SIZE == 0 { + return; + } + let (from_ptr, _) = from.to_raw_parts(); + let (to_ptr, _) = to.to_raw_parts(); + unsafe { + MEM_INIT_STATE.copy::(from_ptr as *const u8, to_ptr as *const u8, 1); + } +} diff --git a/tests/expected/uninit/fixme_unions.rs b/tests/expected/uninit/fixme_unions.rs new file mode 100644 index 000000000000..b93b58346b62 --- /dev/null +++ b/tests/expected/uninit/fixme_unions.rs @@ -0,0 +1,60 @@ +// 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, +} + +/// Reading padding data via simple union access if union is passed to another function. +#[kani::proof] +unsafe fn cross_function_union() { + unsafe fn helper(u: U) { + let padding = u.b; + } + let u = U { a: 0 }; + helper(u); +} + +/// Reading padding data but a union is via a union from behind a pointer. +#[kani::proof] +unsafe fn pointer_union() { + let u = U { a: 0 }; + let u_ptr = addr_of!(u); + let u1 = *u_ptr; + let padding = u1.b; +} + +#[repr(C)] +struct S { + u: U, +} + +/// Tests uninitialized access if unions are top-level subfields. +#[kani::proof] +unsafe fn union_as_subfields() { + let u = U { a: 0 }; + let s = S { u }; + let s1 = s; + let u1 = s1.u; + let padding = u1.a; +} + +union Outer { + u: U, + a: u32 +} + +/// Tests unions composing with other unions. +#[kani::proof] +unsafe fn uber_union() { + let u = Outer { u: U { b: 0 } }; + let non_padding = u.a; +} diff --git a/tests/expected/uninit/unions.expected b/tests/expected/uninit/unions.expected new file mode 100644 index 000000000000..fc79c9ab833b --- /dev/null +++ b/tests/expected/uninit/unions.expected @@ -0,0 +1,12 @@ +union_complex_subfields.assertion.1\ + - Status: FAILURE\ + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u16`"\ + +basic_union_fail.assertion.1\ + - Status: FAILURE\ + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`" + +Summary: +Verification failed for - union_complex_subfields +Verification failed for - basic_union_fail +Complete - 2 successfully verified harnesses, 2 failures, 4 total. diff --git a/tests/expected/uninit/unions.rs b/tests/expected/uninit/unions.rs new file mode 100644 index 000000000000..8466fd627605 --- /dev/null +++ b/tests/expected/uninit/unions.rs @@ -0,0 +1,52 @@ +// 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_pass() { + let u = U { b: 0 }; + let u1 = u; + let padding = u1.a; +} + +/// Reading padding data via simple union access. +#[kani::proof] +unsafe fn basic_union_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 uninit data via subfields of a union. +#[kani::proof] +unsafe fn union_complex_subfields() { + let u = U1 { a: (0, 0) }; + let non_padding = u.b.1; +} + +/// Tests overwriting data inside unions. +#[kani::proof] +unsafe fn union_update() { + let mut u = U { a: 0 }; + u.b = 0; + let non_padding = u.b; +} + From 50c11147663e395f1d20710b6127497473e03d04 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Fri, 16 Aug 2024 08:30:31 -0700 Subject: [PATCH 04/15] Formatting + error message changes --- .../check_uninit/ptr_uninit/uninit_visitor.rs | 2 +- .../src/kani_middle/transform/kani_intrinsics.rs | 3 ++- tests/expected/uninit/fixme_unions.rs | 4 ++-- tests/expected/uninit/intrinsics/expected | 12 ++++++------ tests/expected/uninit/unions.rs | 1 - 5 files changed, 11 insertions(+), 11 deletions(-) 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 c3f68d7043dc..a4620c845324 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 @@ -171,7 +171,7 @@ impl MirVisitor for CheckUninitVisitor { self.push_target(MemoryInitOp::SetRef { operand: Operand::Copy(place.clone()), value: true, - position: InsertPosition::After + position: InsertPosition::After, }); } } diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index 9f3a8a20283d..4f4f29359515 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -325,7 +325,8 @@ impl IntrinsicGeneratorPass { })); let result = new_body.insert_assignment(rvalue, &mut source, InsertPosition::Before); - let reason: &str = "Kani does not yet support using initialization predicates on unions."; + let reason: &str = + "Kani does not yet support using initialization predicates on unions."; new_body.insert_check( tcx, diff --git a/tests/expected/uninit/fixme_unions.rs b/tests/expected/uninit/fixme_unions.rs index b93b58346b62..7de5f4b8cfb5 100644 --- a/tests/expected/uninit/fixme_unions.rs +++ b/tests/expected/uninit/fixme_unions.rs @@ -37,7 +37,7 @@ struct S { u: U, } -/// Tests uninitialized access if unions are top-level subfields. +/// Tests uninitialized access if unions are top-level subfields. #[kani::proof] unsafe fn union_as_subfields() { let u = U { a: 0 }; @@ -49,7 +49,7 @@ unsafe fn union_as_subfields() { union Outer { u: U, - a: u32 + a: u32, } /// Tests unions composing with other unions. diff --git a/tests/expected/uninit/intrinsics/expected b/tests/expected/uninit/intrinsics/expected index e428aa605887..c6d61b93add9 100644 --- a/tests/expected/uninit/intrinsics/expected +++ b/tests/expected/uninit/intrinsics/expected @@ -1,18 +1,18 @@ -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::read::>.assertion.2\ +std::ptr::write::>.assertion.2\ - 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."\ std::ptr::write::>.assertion.2\ - 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.rs b/tests/expected/uninit/unions.rs index 8466fd627605..5b4dc9e6db1b 100644 --- a/tests/expected/uninit/unions.rs +++ b/tests/expected/uninit/unions.rs @@ -49,4 +49,3 @@ unsafe fn union_update() { u.b = 0; let non_padding = u.b; } - From 5649ad8361f243fceb9f87311dcc2da2c92c5661 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Fri, 16 Aug 2024 11:44:48 -0700 Subject: [PATCH 05/15] Remove accidentally added files --- tests/expected/uninit/copy/copy.rs | 87 ----------------------------- tests/expected/uninit/copy/expected | 31 ---------- 2 files changed, 118 deletions(-) delete mode 100644 tests/expected/uninit/copy/copy.rs delete mode 100644 tests/expected/uninit/copy/expected diff --git a/tests/expected/uninit/copy/copy.rs b/tests/expected/uninit/copy/copy.rs deleted file mode 100644 index 8d8278a6f0b9..000000000000 --- a/tests/expected/uninit/copy/copy.rs +++ /dev/null @@ -1,87 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z uninit-checks - -#[repr(C)] -#[derive(kani::Arbitrary)] -struct S(u32, u8); // 5 bytes of data + 3 bytes of padding. - -#[kani::proof] -/// This checks that reading copied uninitialized bytes fails an assertion. -unsafe fn expose_padding_via_copy() { - let from: S = kani::any(); - let mut to: u64 = kani::any(); - - let from_ptr = &from as *const S; - let to_ptr = &mut to as *mut u64; - - // This should not cause UB since `copy` is untyped. - std::ptr::copy(from_ptr as *const u8, to_ptr as *mut u8, std::mem::size_of::()); - - // This reads uninitialized bytes, which is UB. - let padding: u64 = std::ptr::read(to_ptr); -} - -#[kani::proof] -/// This checks that reading copied uninitialized bytes after a multi-byte copy fails an assertion. -unsafe fn expose_padding_via_non_byte_copy() { - let from: S = kani::any(); - let mut to: u64 = kani::any(); - - let from_ptr = &from as *const S; - let to_ptr = &mut to as *mut u64; - - // This should not cause UB since `copy` is untyped. - std::ptr::copy(from_ptr as *const u64, to_ptr as *mut u64, 1); - - // This reads uninitialized bytes, which is UB. - let padding: u64 = std::ptr::read(to_ptr); -} - -#[kani::proof] -/// This checks that reading copied initialized bytes verifies correctly. -unsafe fn copy_without_padding() { - let from: S = kani::any(); - let mut to: u64 = kani::any(); - - let from_ptr = &from as *const S; - let to_ptr = &mut to as *mut u64; - - // This should not cause UB since `copy` is untyped. - std::ptr::copy(from_ptr as *const u8, to_ptr as *mut u8, std::mem::size_of::()); - - // Since the previous copy only copied 4 bytes, no padding was copied, so no padding is read. - let data: u64 = std::ptr::read(to_ptr); -} - -#[kani::proof] -/// This checks that reading copied initialized bytes after a multi-byte copy verifies correctly. -unsafe fn non_byte_copy_without_padding() { - let from: S = kani::any(); - let mut to: u64 = kani::any(); - - let from_ptr = &from as *const S; - let to_ptr = &mut to as *mut u64; - - // This should not cause UB since `copy` is untyped. - std::ptr::copy(from_ptr as *const u32, to_ptr as *mut u32, 1); - - // Since the previous copy only copied 4 bytes, no padding was copied, so no padding is read. - let data: u64 = std::ptr::read(to_ptr); -} - -#[kani::proof] -/// This checks that reading uninitialized bytes fails an assertion even after copy. -unsafe fn read_after_copy() { - let from: S = kani::any(); - let mut to: u64 = kani::any(); - - let from_ptr = &from as *const S; - let to_ptr = &mut to as *mut u64; - - // This should not cause UB since `copy` is untyped. - std::ptr::copy(from_ptr as *const u8, to_ptr as *mut u8, std::mem::size_of::()); - - // Reading padding from the previous place should be UB even after copy. - let data: u64 = std::ptr::read(from_ptr as *const u64); -} diff --git a/tests/expected/uninit/copy/expected b/tests/expected/uninit/copy/expected deleted file mode 100644 index a288f9f2856d..000000000000 --- a/tests/expected/uninit/copy/expected +++ /dev/null @@ -1,31 +0,0 @@ -Checking harness read_after_copy... - -Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u64` - -VERIFICATION:- FAILED - -Checking harness non_byte_copy_without_padding... - -VERIFICATION:- SUCCESSFUL - -Checking harness copy_without_padding... - -VERIFICATION:- SUCCESSFUL - -Checking harness expose_padding_via_non_byte_copy... - -Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u64` - -VERIFICATION:- FAILED - -Checking harness expose_padding_via_copy... - -Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u64` - -VERIFICATION:- FAILED - -Summary: -Verification failed for - read_after_copy -Verification failed for - expose_padding_via_non_byte_copy -Verification failed for - expose_padding_via_copy -Complete - 2 successfully verified harnesses, 3 failures, 5 total. From f6c0b0529a5d215a975206d04d93f82e477d1d0f Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Thu, 22 Aug 2024 09:34:07 -0400 Subject: [PATCH 06/15] Add annotations to union tests --- tests/expected/uninit/fixme_unions.rs | 26 +++++++++++++------------- tests/expected/uninit/unions.rs | 8 ++++---- 2 files changed, 17 insertions(+), 17 deletions(-) diff --git a/tests/expected/uninit/fixme_unions.rs b/tests/expected/uninit/fixme_unions.rs index 7de5f4b8cfb5..5f1a4d240a01 100644 --- a/tests/expected/uninit/fixme_unions.rs +++ b/tests/expected/uninit/fixme_unions.rs @@ -15,21 +15,21 @@ union U { /// Reading padding data via simple union access if union is passed to another function. #[kani::proof] -unsafe fn cross_function_union() { +unsafe fn cross_function_union_should_fail() { unsafe fn helper(u: U) { - let padding = u.b; + let padding = u.b; // Read 32 bytes from `u`. } - let u = U { a: 0 }; + let u = U { a: 0 }; // `u` is initialized for 16 bytes. helper(u); } /// Reading padding data but a union is via a union from behind a pointer. #[kani::proof] -unsafe fn pointer_union() { - let u = U { a: 0 }; +unsafe fn pointer_union_should_fail() { + let u = U { a: 0 }; // `u` is initialized for 16 bytes. let u_ptr = addr_of!(u); let u1 = *u_ptr; - let padding = u1.b; + let padding = u1.b; // Read 32 bytes from `u`. } #[repr(C)] @@ -39,12 +39,12 @@ struct S { /// Tests uninitialized access if unions are top-level subfields. #[kani::proof] -unsafe fn union_as_subfields() { - let u = U { a: 0 }; +unsafe fn union_as_subfields_should_pass() { + let u = U { a: 0 }; // `u` is initialized for 16 bytes. let s = S { u }; let s1 = s; - let u1 = s1.u; - let padding = u1.a; + let u1 = s1.u; // `u1` is initialized for 16 bytes. + let padding = u1.a; // Read 16 bytes from `u`. } union Outer { @@ -54,7 +54,7 @@ union Outer { /// Tests unions composing with other unions. #[kani::proof] -unsafe fn uber_union() { - let u = Outer { u: U { b: 0 } }; - let non_padding = u.a; +unsafe fn uber_union_should_pass() { + let u = Outer { u: U { b: 0 } }; // `u` is initialized for 32 bytes. + let non_padding = u.a; // Read 32 bytes from `u`. } diff --git a/tests/expected/uninit/unions.rs b/tests/expected/uninit/unions.rs index 5b4dc9e6db1b..16ce182ee526 100644 --- a/tests/expected/uninit/unions.rs +++ b/tests/expected/uninit/unions.rs @@ -15,7 +15,7 @@ union U { /// Simple and correct union access. #[kani::proof] -unsafe fn basic_union_pass() { +unsafe fn basic_union_should_pass() { let u = U { b: 0 }; let u1 = u; let padding = u1.a; @@ -23,7 +23,7 @@ unsafe fn basic_union_pass() { /// Reading padding data via simple union access. #[kani::proof] -unsafe fn basic_union_fail() { +unsafe fn basic_union_should_fail() { let u = U { a: 0 }; let u1 = u; let padding = u1.b; @@ -37,14 +37,14 @@ union U1 { /// Tests accessing uninit data via subfields of a union. #[kani::proof] -unsafe fn union_complex_subfields() { +unsafe fn union_complex_subfields_should_pass() { let u = U1 { a: (0, 0) }; let non_padding = u.b.1; } /// Tests overwriting data inside unions. #[kani::proof] -unsafe fn union_update() { +unsafe fn union_update_should_pass() { let mut u = U { a: 0 }; u.b = 0; let non_padding = u.b; From 8ef14f0b37291001fb4af81061e808e7bd9ec03c Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Thu, 22 Aug 2024 15:25:58 -0400 Subject: [PATCH 07/15] More tests and test fixes --- tests/expected/uninit/unions.expected | 17 +++++++++++------ tests/expected/uninit/unions.rs | 17 ++++++++++++++++- 2 files changed, 27 insertions(+), 7 deletions(-) diff --git a/tests/expected/uninit/unions.expected b/tests/expected/uninit/unions.expected index fc79c9ab833b..05fdac3a8765 100644 --- a/tests/expected/uninit/unions.expected +++ b/tests/expected/uninit/unions.expected @@ -1,12 +1,17 @@ -union_complex_subfields.assertion.1\ +union_update_should_fail.assertion.1\ - Status: FAILURE\ - - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u16`"\ + - 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_fail.assertion.1\ +basic_union_should_fail.assertion.1\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`" Summary: -Verification failed for - union_complex_subfields -Verification failed for - basic_union_fail -Complete - 2 successfully verified harnesses, 2 failures, 4 total. +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 index 16ce182ee526..faf92578aa1e 100644 --- a/tests/expected/uninit/unions.rs +++ b/tests/expected/uninit/unions.rs @@ -35,9 +35,16 @@ union U1 { b: (u32, u16, u8), } -/// Tests accessing uninit data via subfields of a union. +/// 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 non_padding = u.b.1; } @@ -49,3 +56,11 @@ unsafe fn union_update_should_pass() { u.b = 0; let non_padding = u.b; } + +/// Tests overwriting data inside unions. +#[kani::proof] +unsafe fn union_update_should_fail() { + let mut u = U { a: 0 }; + u.a = 0; + let non_padding = u.b; +} From 0f2ed21446a005f42d92588202005d9476c08984 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Thu, 22 Aug 2024 15:57:14 -0400 Subject: [PATCH 08/15] Ensure that intermediate union field accesses are instrumented --- .../check_uninit/ptr_uninit/uninit_visitor.rs | 8 +++++++- tests/expected/uninit/unions.expected | 9 +++++++-- tests/expected/uninit/unions.rs | 12 ++++++------ 3 files changed, 20 insertions(+), 9 deletions(-) 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 745605478505..8b4812fbafa8 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 @@ -407,9 +407,15 @@ impl MirVisitor for CheckUninitVisitor { if intermediate_place.ty(&self.locals).unwrap().kind().is_union() && !ptx.is_mutating() { + // Generate a place which includes all projections until (and including) + // union field access. + let union_field_access_place = Place { + local: place.local, + projection: place.projection[..idx + 1].to_vec(), + }; // Accessing a place inside the union, need to check if it is initialized. self.push_target(MemoryInitOp::CheckRef { - operand: Operand::Copy(place.clone()), + operand: Operand::Copy(union_field_access_place.clone()), }); } } diff --git a/tests/expected/uninit/unions.expected b/tests/expected/uninit/unions.expected index 05fdac3a8765..e0c543a89665 100644 --- a/tests/expected/uninit/unions.expected +++ b/tests/expected/uninit/unions.expected @@ -4,14 +4,19 @@ union_update_should_fail.assertion.1\ union_complex_subfields_should_fail.assertion.1\ - Status: FAILURE\ - - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u16`" + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `(u32, u16, u8)`" basic_union_should_fail.assertion.1\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`" +union_uninit_inside_projection_should_fail.assertion.1\ + - Status: FAILURE\ + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `(u32, u16, u8)`" + Summary: Verification failed for - union_update_should_fail +Verification failed for - union_uninit_inside_projection_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. +Complete - 2 successfully verified harnesses, 4 failures, 6 total. diff --git a/tests/expected/uninit/unions.rs b/tests/expected/uninit/unions.rs index faf92578aa1e..04b00c5ebf10 100644 --- a/tests/expected/uninit/unions.rs +++ b/tests/expected/uninit/unions.rs @@ -35,18 +35,18 @@ union U1 { b: (u32, u16, u8), } -/// Tests accessing initialized data via subfields of a union. +/// Tests accessing uninit data via subfields of a union. #[kani::proof] -unsafe fn union_complex_subfields_should_pass() { +unsafe fn union_complex_subfields_should_fail() { let u = U1 { a: (0, 0) }; - let non_padding = u.b.0; + let non_padding = u.b.1; } -/// Tests accessing uninit data via subfields of a union. +/// Tests accessing uninitialized data inside a place projection. #[kani::proof] -unsafe fn union_complex_subfields_should_fail() { +unsafe fn union_uninit_inside_projection_should_fail() { let u = U1 { a: (0, 0) }; - let non_padding = u.b.1; + let non_padding = u.b.0; } /// Tests overwriting data inside unions. From 188930fa3e1b544c690b656524b64868da550495 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Thu, 22 Aug 2024 16:08:27 -0400 Subject: [PATCH 09/15] Minor changes --- .../kani_middle/transform/check_uninit/mod.rs | 3 ++- .../check_uninit/relevant_instruction.rs | 16 +++++++++++++--- 2 files changed, 15 insertions(+), 4 deletions(-) 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 c83ff14ae985..a10dcf36cf0d 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -425,7 +425,8 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { } PointeeLayout::Union { field_layouts } => { // Writing union data, which could be either creating a union from scratch or - // performing some pointer operations with it. + // 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, 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 d8c46deb887f..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 @@ -7,7 +7,7 @@ use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; use stable_mir::{ mir::{FieldIdx, Mutability, Operand, Place, Rvalue, Statement, StatementKind}, - ty::Ty, + ty::{RigidTy, Ty}, }; use strum_macros::AsRefStr; @@ -152,9 +152,19 @@ impl MemoryInitOp { MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => { unreachable!("operands do not exist for this operation") } - MemoryInitOp::Copy { from, .. } => { + MemoryInitOp::Copy { from, to, .. } => { // It does not matter which operand to return for layout generation, since both of - // them have the same pointee type. + // them have the same pointee type, so we assert that. + let from_kind = from.ty(body.locals()).unwrap().kind(); + let to_kind = to.ty(body.locals()).unwrap().kind(); + + let RigidTy::RawPtr(from_pointee_ty, _) = from_kind.rigid().unwrap().clone() else { + unreachable!() + }; + let RigidTy::RawPtr(to_pointee_ty, _) = to_kind.rigid().unwrap().clone() else { + unreachable!() + }; + assert!(from_pointee_ty == to_pointee_ty); from.ty(body.locals()).unwrap() } MemoryInitOp::AssignUnion { lvalue, .. } => { From 7d37197701a3db034106ac6196d04e08fa2950a1 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Sat, 24 Aug 2024 19:09:04 -0400 Subject: [PATCH 10/15] Disable pointer checks for new instrumentation --- library/kani/src/mem_init.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/library/kani/src/mem_init.rs b/library/kani/src/mem_init.rs index c2a674c51053..eec76b09e7c5 100644 --- a/library/kani/src/mem_init.rs +++ b/library/kani/src/mem_init.rs @@ -310,6 +310,7 @@ fn set_str_ptr_initialized( } /// Copy initialization state of `size_of:: * num_elts` bytes from one pointer to the other. +#[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 { @@ -323,6 +324,7 @@ fn copy_init_state(from: *const T, to: *const T, nu } /// Copy initialization state of `size_of::` bytes from one pointer to the other. +#[kanitool::disable_checks(pointer)] #[rustc_diagnostic_item = "KaniCopyInitStateSingle"] fn copy_init_state_single(from: *const T, to: *const T) { if LAYOUT_SIZE == 0 { From bd9d4f8792790416f2b7a8030c73a11b2a34bd27 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Sat, 24 Aug 2024 19:34:15 -0400 Subject: [PATCH 11/15] Address comments from code review --- library/kani/src/mem_init.rs | 15 +++++---------- tests/expected/uninit/fixme_unions.rs | 19 ++++++++++--------- tests/expected/uninit/unions.rs | 9 ++++++--- 3 files changed, 21 insertions(+), 22 deletions(-) diff --git a/library/kani/src/mem_init.rs b/library/kani/src/mem_init.rs index eec76b09e7c5..a6118c472a92 100644 --- a/library/kani/src/mem_init.rs +++ b/library/kani/src/mem_init.rs @@ -309,7 +309,8 @@ 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) { @@ -323,16 +324,10 @@ fn copy_init_state(from: *const T, to: *const T, nu } } -/// Copy initialization state of `size_of::` bytes from one pointer to the other. +/// 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) { - if LAYOUT_SIZE == 0 { - return; - } - let (from_ptr, _) = from.to_raw_parts(); - let (to_ptr, _) = to.to_raw_parts(); - unsafe { - MEM_INIT_STATE.copy::(from_ptr as *const u8, to_ptr as *const u8, 1); - } + copy_init_state::(from, to, 1); } diff --git a/tests/expected/uninit/fixme_unions.rs b/tests/expected/uninit/fixme_unions.rs index 5f1a4d240a01..8c69cdc01038 100644 --- a/tests/expected/uninit/fixme_unions.rs +++ b/tests/expected/uninit/fixme_unions.rs @@ -3,6 +3,7 @@ // 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; @@ -17,19 +18,19 @@ union U { #[kani::proof] unsafe fn cross_function_union_should_fail() { unsafe fn helper(u: U) { - let padding = u.b; // Read 32 bytes from `u`. + let padding = u.b; // Read 4 bytes from `u`. } - let u = U { a: 0 }; // `u` is initialized for 16 bytes. + let u = U { a: 0 }; // `u` is initialized for 2 bytes. helper(u); } /// Reading padding data but a union is via a union from behind a pointer. #[kani::proof] unsafe fn pointer_union_should_fail() { - let u = U { a: 0 }; // `u` is initialized for 16 bytes. + 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 32 bytes from `u`. + let padding = u1.b; // Read 4 bytes from `u`. } #[repr(C)] @@ -40,11 +41,11 @@ struct S { /// 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 16 bytes. + 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 16 bytes. - let padding = u1.a; // Read 16 bytes from `u`. + let u1 = s1.u; // `u1` is initialized for 2 bytes. + let padding = u1.a; // Read 2 bytes from `u`. } union Outer { @@ -55,6 +56,6 @@ union Outer { /// 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 32 bytes. - let non_padding = u.a; // Read 32 bytes from `u`. + 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/unions.rs b/tests/expected/uninit/unions.rs index 04b00c5ebf10..c542b4362390 100644 --- a/tests/expected/uninit/unions.rs +++ b/tests/expected/uninit/unions.rs @@ -18,7 +18,8 @@ union U { unsafe fn basic_union_should_pass() { let u = U { b: 0 }; let u1 = u; - let padding = u1.a; + let non_padding = u1.a; + assert!(non_padding == 0); } /// Reading padding data via simple union access. @@ -39,10 +40,11 @@ union U1 { #[kani::proof] unsafe fn union_complex_subfields_should_fail() { let u = U1 { a: (0, 0) }; - let non_padding = u.b.1; + let padding = u.b.1; } /// Tests accessing uninitialized data inside a place projection. +/// TODO: this is valid and should pass. #[kani::proof] unsafe fn union_uninit_inside_projection_should_fail() { let u = U1 { a: (0, 0) }; @@ -55,6 +57,7 @@ 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. @@ -62,5 +65,5 @@ unsafe fn union_update_should_pass() { unsafe fn union_update_should_fail() { let mut u = U { a: 0 }; u.a = 0; - let non_padding = u.b; + let padding = u.b; } From 64e21a3cde3253e5bf3fde1a3ca03b41675156cd Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 26 Aug 2024 13:44:49 -0400 Subject: [PATCH 12/15] Revert intermediate place checking since uninitialized intermediate projections do not actually cause UB --- .../check_uninit/ptr_uninit/uninit_visitor.rs | 8 +------- tests/expected/uninit/unions.expected | 9 ++------- tests/expected/uninit/unions.rs | 13 ++++++------- 3 files changed, 9 insertions(+), 21 deletions(-) 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 8b4812fbafa8..745605478505 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 @@ -407,15 +407,9 @@ impl MirVisitor for CheckUninitVisitor { if intermediate_place.ty(&self.locals).unwrap().kind().is_union() && !ptx.is_mutating() { - // Generate a place which includes all projections until (and including) - // union field access. - let union_field_access_place = Place { - local: place.local, - projection: place.projection[..idx + 1].to_vec(), - }; // Accessing a place inside the union, need to check if it is initialized. self.push_target(MemoryInitOp::CheckRef { - operand: Operand::Copy(union_field_access_place.clone()), + operand: Operand::Copy(place.clone()), }); } } diff --git a/tests/expected/uninit/unions.expected b/tests/expected/uninit/unions.expected index e0c543a89665..05fdac3a8765 100644 --- a/tests/expected/uninit/unions.expected +++ b/tests/expected/uninit/unions.expected @@ -4,19 +4,14 @@ union_update_should_fail.assertion.1\ union_complex_subfields_should_fail.assertion.1\ - Status: FAILURE\ - - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `(u32, u16, u8)`" + - 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`" -union_uninit_inside_projection_should_fail.assertion.1\ - - Status: FAILURE\ - - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `(u32, u16, u8)`" - Summary: Verification failed for - union_update_should_fail -Verification failed for - union_uninit_inside_projection_should_fail Verification failed for - union_complex_subfields_should_fail Verification failed for - basic_union_should_fail -Complete - 2 successfully verified harnesses, 4 failures, 6 total. +Complete - 3 successfully verified harnesses, 3 failures, 6 total. diff --git a/tests/expected/uninit/unions.rs b/tests/expected/uninit/unions.rs index c542b4362390..c623f9fcea94 100644 --- a/tests/expected/uninit/unions.rs +++ b/tests/expected/uninit/unions.rs @@ -36,19 +36,18 @@ union U1 { b: (u32, u16, u8), } -/// Tests accessing uninit data via subfields of a union. +/// Tests accessing initialized data via subfields of a union. #[kani::proof] -unsafe fn union_complex_subfields_should_fail() { +unsafe fn union_complex_subfields_should_pass() { let u = U1 { a: (0, 0) }; - let padding = u.b.1; + let non_padding = u.b.0; } -/// Tests accessing uninitialized data inside a place projection. -/// TODO: this is valid and should pass. +/// Tests accessing uninit data via subfields of a union. #[kani::proof] -unsafe fn union_uninit_inside_projection_should_fail() { +unsafe fn union_complex_subfields_should_fail() { let u = U1 { a: (0, 0) }; - let non_padding = u.b.0; + let padding = u.b.1; } /// Tests overwriting data inside unions. From 22ba6cfaf6f5e1e96ddffa09139d774abbc08c3a Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 26 Aug 2024 14:31:00 -0400 Subject: [PATCH 13/15] Fail if dereference is detected in union field projection --- .../transform/check_uninit/ptr_uninit/uninit_visitor.rs | 9 +++++++++ 1 file changed, 9 insertions(+) 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 745605478505..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 @@ -407,6 +407,15 @@ impl MirVisitor for CheckUninitVisitor { if intermediate_place.ty(&self.locals).unwrap().kind().is_union() && !ptx.is_mutating() { + 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()), From 825bd37d0c772bd5a6cbfcdc6916b75a5889e0fa Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 26 Aug 2024 21:07:50 -0400 Subject: [PATCH 14/15] Fix comment typo --- tests/expected/uninit/fixme_unions.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/expected/uninit/fixme_unions.rs b/tests/expected/uninit/fixme_unions.rs index 8c69cdc01038..ec86e5e7e07f 100644 --- a/tests/expected/uninit/fixme_unions.rs +++ b/tests/expected/uninit/fixme_unions.rs @@ -24,7 +24,7 @@ unsafe fn cross_function_union_should_fail() { helper(u); } -/// Reading padding data but a union is via a union from behind a pointer. +/// 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. From d351eb9da9536900e5de6e839e75600c4974ac84 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 26 Aug 2024 21:08:13 -0400 Subject: [PATCH 15/15] Add const str's for diagnostic functions --- .../kani_middle/transform/check_uninit/mod.rs | 59 +++++++++++++------ 1 file changed, 40 insertions(+), 19 deletions(-) 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 a10dcf36cf0d..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. @@ -202,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) @@ -238,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!(), }; @@ -331,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, @@ -344,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, @@ -383,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!(), }; @@ -450,7 +463,7 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { }; let layout = &field_layouts[union_field]; let layout_operand = mk_layout_operand(body, &mut statements, source, layout); - let diagnostic = "KaniSetPtrInitialized"; + let diagnostic = KANI_SET_PTR_INITIALIZED_DIAGNOSTIC; let args = vec![ ptr_operand, layout_operand, @@ -499,7 +512,11 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { }; 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), + get_mem_init_fn_def( + self.tcx, + KANI_COPY_INIT_STATE_DIAGNOSTIC, + &mut self.mem_init_fn_cache, + ), layout_size, *pointee_info.ty(), ); @@ -530,7 +547,11 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { 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, "KaniCopyInitStateSingle", &mut self.mem_init_fn_cache), + get_mem_init_fn_def( + self.tcx, + KANI_COPY_INIT_STATE_SINGLE_DIAGNOSTIC, + &mut self.mem_init_fn_cache, + ), layout_size, *pointee_info.ty(), );