diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index fa4e5eb1ad97..24fe5d8b2b2e 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 }); @@ -484,7 +484,7 @@ impl CheckType { } /// We store the index of an instruction to avoid borrow checker issues and unnecessary copies. -#[derive(Copy, Clone, Debug)] +#[derive(Copy, Clone, Debug, PartialEq, Eq)] pub enum SourceInstruction { Statement { idx: usize, bb: BasicBlockIdx }, Terminator { bb: BasicBlockIdx }, diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs index f295fc76d4bf..25059297d3d5 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs @@ -18,20 +18,15 @@ use rustc_middle::ty::TyCtxt; use stable_mir::mir::{ mono::Instance, visit::{Location, PlaceContext}, - BasicBlockIdx, MirVisitor, Operand, Place, Rvalue, Statement, Terminator, + MirVisitor, Operand, Place, Rvalue, Statement, Terminator, }; use std::collections::HashSet; pub struct InstrumentationVisitor<'a, 'tcx> { - /// Whether we should skip the next instruction, since it might've been instrumented already. - /// When we instrument an instruction, we partition the basic block, and the instruction that - /// may trigger UB becomes the first instruction of the basic block, which we need to skip - /// later. - skip_next: bool, - /// The instruction being visited at a given point. - current: SourceInstruction, - /// The target instruction that should be verified. - pub target: Option, + /// All target instructions in the body. + targets: Vec, + /// Current analysis target, eventually needs to be added to a list of all targets. + current_target: InitRelevantInstruction, /// Aliasing analysis data. points_to: &'a PointsToGraph<'tcx>, /// The list of places we should be looking for, ignoring others @@ -41,17 +36,16 @@ pub struct InstrumentationVisitor<'a, 'tcx> { } impl<'a, 'tcx> TargetFinder for InstrumentationVisitor<'a, 'tcx> { - fn find_next( - &mut self, - body: &MutableBody, - bb: BasicBlockIdx, - skip_first: bool, - ) -> Option { - self.skip_next = skip_first; - self.current = SourceInstruction::Statement { idx: 0, bb }; - self.target = None; - self.visit_basic_block(&body.blocks()[bb]); - self.target.clone() + fn find_all(mut self, body: &MutableBody) -> Vec { + for (bb_idx, bb) in body.blocks().iter().enumerate() { + self.current_target = InitRelevantInstruction { + source: SourceInstruction::Statement { idx: 0, bb: bb_idx }, + before_instruction: vec![], + after_instruction: vec![], + }; + self.visit_basic_block(bb); + } + self.targets } } @@ -63,43 +57,55 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> { tcx: TyCtxt<'tcx>, ) -> Self { Self { - skip_next: false, - current: SourceInstruction::Statement { idx: 0, bb: 0 }, - target: None, + targets: vec![], + current_target: InitRelevantInstruction { + source: SourceInstruction::Statement { idx: 0, bb: 0 }, + before_instruction: vec![], + after_instruction: vec![], + }, points_to, analysis_targets, current_instance, tcx, } } + fn push_target(&mut self, source_op: MemoryInitOp) { - let target = self.target.get_or_insert_with(|| InitRelevantInstruction { - source: self.current, - after_instruction: vec![], - before_instruction: vec![], - }); - target.push_operation(source_op); + self.current_target.push_operation(source_op); } } impl<'a, 'tcx> MirVisitor for InstrumentationVisitor<'a, 'tcx> { fn visit_statement(&mut self, stmt: &Statement, location: Location) { - if self.skip_next { - self.skip_next = false; - } else if self.target.is_none() { - // Check all inner places. - self.super_statement(stmt, location); - } + self.super_statement(stmt, location); // Switch to the next statement. - let SourceInstruction::Statement { idx, bb } = self.current else { unreachable!() }; - self.current = SourceInstruction::Statement { idx: idx + 1, bb }; + if let SourceInstruction::Statement { idx, bb } = self.current_target.source { + self.targets.push(self.current_target.clone()); + self.current_target = InitRelevantInstruction { + source: SourceInstruction::Statement { idx: idx + 1, bb }, + after_instruction: vec![], + before_instruction: vec![], + }; + } else { + unreachable!() + } } fn visit_terminator(&mut self, term: &Terminator, location: Location) { - if !(self.skip_next || self.target.is_some()) { - self.current = SourceInstruction::Terminator { bb: self.current.bb() }; - self.super_terminator(term, location); + if let SourceInstruction::Statement { bb, .. } = self.current_target.source { + // We don't have to push the previous target, since it already happened in the statement + // handling code. + self.current_target = InitRelevantInstruction { + source: SourceInstruction::Terminator { bb }, + after_instruction: vec![], + before_instruction: vec![], + }; + } else { + unreachable!() } + self.super_terminator(term, location); + // Push the current target from the terminator onto the list. + self.targets.push(self.current_target.clone()); } fn visit_rvalue(&mut self, rvalue: &Rvalue, location: Location) { 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 0a0d3c786ea9..88d906aa3134 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -13,13 +13,13 @@ 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, Body, ConstOperand, Mutability, Operand, Place, + Rvalue, Statement, StatementKind, Terminator, TerminatorKind, UnwindAction, }, ty::{FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Ty, TyConst, TyKind, UintTy}, CrateDef, }; -use std::collections::{HashMap, HashSet}; +use std::collections::HashMap; pub use delayed_ub::DelayedUbPass; pub use ptr_uninit::UninitPass; @@ -31,13 +31,8 @@ mod relevant_instruction; mod ty_layout; /// Trait that the instrumentation target providers must implement to work with the instrumenter. -trait TargetFinder { - fn find_next( - &mut self, - body: &MutableBody, - bb: BasicBlockIdx, - skip_first: bool, - ) -> Option; +pub trait TargetFinder { + fn find_all(self, body: &MutableBody) -> Vec; } // Function bodies of those functions will not be instrumented as not to cause infinite recursion. @@ -53,27 +48,42 @@ 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>, } -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 }; + 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, + 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()) }) @@ -83,28 +93,9 @@ 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; - }; + for instruction in target_finder.find_all(&body).into_iter().rev() { + let source = instruction.source; + self.build_check_for_instruction(&mut body, instruction, source); } (orig_len != body.blocks().len(), body) } @@ -112,40 +103,38 @@ 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, + mut source: SourceInstruction, ) { - 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)`. + 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,58 +143,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); + 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::Copy { .. } => { - self.build_copy(tcx, body, source, operation, pointee_ty_info, skip_first) - } + | 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!() } - } + }; } /// 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 { @@ -223,18 +209,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. @@ -248,32 +240,39 @@ 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); 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. + body.insert_bb(BasicBlock { statements, terminator }, source, operation.position()); + + // 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. let operand_ty = match &operation { MemoryInitOp::Check { operand } | MemoryInitOp::CheckSliceChunk { operand, .. } @@ -281,7 +280,7 @@ impl<'a> UninitInstrumenter<'a> { _ => unreachable!(), }; body.insert_check( - tcx, + self.tcx, &self.check_type, source, operation.position(), @@ -296,23 +295,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 { @@ -346,18 +346,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. @@ -371,44 +377,50 @@ 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. + body.insert_bb(BasicBlock { statements, terminator }, source, operation.position()); } /// Copy memory initialization state from one pointer to the other. fn build_copy( &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), @@ -416,11 +428,10 @@ impl<'a> UninitInstrumenter<'a> { }; let PointeeLayout::Sized { layout } = pointee_info.layout() else { unreachable!() }; let copy_init_state_instance = resolve_mem_init_fn( - get_mem_init_fn_def(tcx, "KaniCopyInitState", &mut self.mem_init_fn_cache), + get_mem_init_fn_def(self.tcx, "KaniCopyInitState", &mut self.mem_init_fn_cache), layout.len(), *pointee_info.ty(), ); - collect_skipped(&operation, body, skip_first); let position = operation.position(); let MemoryInitOp::Copy { from, to, count } = operation else { unreachable!() }; body.insert_call( @@ -465,39 +476,30 @@ 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); -/// 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 { - let new_bb_idx = body.blocks().len(); - skip_first.insert(new_bb_idx); - } + Operand::Move(Place { local: result, projection: vec![] }) } /// Retrieve a function definition by diagnostic string, caching the result. 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/ptr_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs index 1afb151a09b5..a1689bdfe8c4 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,42 +19,32 @@ 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, + CastKind, LocalDecl, MirVisitor, NonDivergingIntrinsic, Operand, Place, PointerCoercion, + ProjectionElem, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, }, ty::{ConstantKind, RigidTy, TyKind}, }; pub struct CheckUninitVisitor { locals: Vec, - /// Whether we should skip the next instruction, since it might've been instrumented already. - /// When we instrument an instruction, we partition the basic block, and the instruction that - /// may trigger UB becomes the first instruction of the basic block, which we need to skip - /// later. - skip_next: bool, - /// The instruction being visited at a given point. - current: SourceInstruction, - /// The target instruction that should be verified. - pub target: Option, - /// The basic block being visited. - bb: BasicBlockIdx, + /// All target instructions in the body. + targets: Vec, + /// Current analysis target, eventually needs to be added to a list of all targets. + current_target: InitRelevantInstruction, } impl TargetFinder for CheckUninitVisitor { - fn find_next( - &mut self, - body: &MutableBody, - bb: BasicBlockIdx, - skip_first: bool, - ) -> Option { + fn find_all(mut self, body: &MutableBody) -> Vec { self.locals = body.locals().to_vec(); - self.skip_next = skip_first; - self.current = SourceInstruction::Statement { idx: 0, bb }; - self.target = None; - self.bb = bb; - self.visit_basic_block(&body.blocks()[bb]); - self.target.clone() + for (bb_idx, bb) in body.blocks().iter().enumerate() { + self.current_target = InitRelevantInstruction { + source: SourceInstruction::Statement { idx: 0, bb: bb_idx }, + before_instruction: vec![], + after_instruction: vec![], + }; + self.visit_basic_block(bb); + } + self.targets } } @@ -62,286 +52,289 @@ impl CheckUninitVisitor { pub fn new() -> Self { Self { locals: vec![], - skip_next: false, - current: SourceInstruction::Statement { idx: 0, bb: 0 }, - target: None, - bb: 0, + targets: vec![], + current_target: InitRelevantInstruction { + source: SourceInstruction::Statement { idx: 0, bb: 0 }, + before_instruction: vec![], + after_instruction: vec![], + }, } } fn push_target(&mut self, source_op: MemoryInitOp) { - let target = self.target.get_or_insert_with(|| InitRelevantInstruction { - source: self.current, - after_instruction: vec![], - before_instruction: vec![], - }); - target.push_operation(source_op); + self.current_target.push_operation(source_op); } } impl MirVisitor for CheckUninitVisitor { fn visit_statement(&mut self, stmt: &Statement, location: Location) { - if self.skip_next { - self.skip_next = false; - } else if self.target.is_none() { - // Leave it as an exhaustive match to be notified when a new kind is added. - match &stmt.kind { - StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping(copy)) => { - self.super_statement(stmt, location); - // The copy is untyped, so we should copy memory initialization state from `src` - // to `dst`. - self.push_target(MemoryInitOp::Copy { - from: copy.src.clone(), - to: copy.dst.clone(), - count: copy.count.clone(), - }); - } - StatementKind::Assign(place, rvalue) => { - // First check rvalue. - self.visit_rvalue(rvalue, location); - // Check whether we are assigning into a dereference (*ptr = _). - if let Some(place_without_deref) = try_remove_topmost_deref(place) { - // First, check that we are not dereferencing extra pointers along the way - // (e.g., **ptr = _). If yes, check whether these pointers are initialized. - let mut place_to_add_projections = - Place { local: place_without_deref.local, projection: vec![] }; - for projection_elem in place_without_deref.projection.iter() { - // If the projection is Deref and the current type is raw pointer, check - // if it points to initialized memory. - if *projection_elem == ProjectionElem::Deref { - if let TyKind::RigidTy(RigidTy::RawPtr(..)) = - place_to_add_projections.ty(&&self.locals).unwrap().kind() - { - self.push_target(MemoryInitOp::Check { - operand: Operand::Copy(place_to_add_projections.clone()), - }); - }; - } - place_to_add_projections.projection.push(projection_elem.clone()); - } - if place_without_deref.ty(&&self.locals).unwrap().kind().is_raw_ptr() { - self.push_target(MemoryInitOp::Set { - operand: Operand::Copy(place_without_deref), - value: true, - position: InsertPosition::After, - }); + // Leave it as an exhaustive match to be notified when a new kind is added. + match &stmt.kind { + StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping(copy)) => { + self.super_statement(stmt, location); + // The copy is untyped, so we should copy memory initialization state from `src` + // to `dst`. + self.push_target(MemoryInitOp::Copy { + from: copy.src.clone(), + to: copy.dst.clone(), + count: copy.count.clone(), + }); + } + StatementKind::Assign(place, rvalue) => { + // First check rvalue. + self.visit_rvalue(rvalue, location); + // Check whether we are assigning into a dereference (*ptr = _). + if let Some(place_without_deref) = try_remove_topmost_deref(place) { + // First, check that we are not dereferencing extra pointers along the way + // (e.g., **ptr = _). If yes, check whether these pointers are initialized. + let mut place_to_add_projections = + Place { local: place_without_deref.local, projection: vec![] }; + for projection_elem in place_without_deref.projection.iter() { + // If the projection is Deref and the current type is raw pointer, check + // if it points to initialized memory. + if *projection_elem == ProjectionElem::Deref { + if let TyKind::RigidTy(RigidTy::RawPtr(..)) = + place_to_add_projections.ty(&&self.locals).unwrap().kind() + { + self.push_target(MemoryInitOp::Check { + operand: Operand::Copy(place_to_add_projections.clone()), + }); + }; } + place_to_add_projections.projection.push(projection_elem.clone()); } - // Check whether Rvalue creates a new initialized pointer previously not captured inside shadow memory. - if place.ty(&&self.locals).unwrap().kind().is_raw_ptr() { - if let Rvalue::AddressOf(..) = rvalue { - self.push_target(MemoryInitOp::Set { - operand: Operand::Copy(place.clone()), - value: true, - position: InsertPosition::After, - }); - } + if place_without_deref.ty(&&self.locals).unwrap().kind().is_raw_ptr() { + self.push_target(MemoryInitOp::Set { + operand: Operand::Copy(place_without_deref), + value: true, + position: InsertPosition::After, + }); } } - StatementKind::Deinit(place) => { - self.super_statement(stmt, location); - self.push_target(MemoryInitOp::Set { - operand: Operand::Copy(place.clone()), - value: false, - position: InsertPosition::After, - }); + // Check whether Rvalue creates a new initialized pointer previously not captured inside shadow memory. + if place.ty(&&self.locals).unwrap().kind().is_raw_ptr() { + if let Rvalue::AddressOf(..) = rvalue { + self.push_target(MemoryInitOp::Set { + operand: Operand::Copy(place.clone()), + value: true, + position: InsertPosition::After, + }); + } } - StatementKind::FakeRead(_, _) - | StatementKind::SetDiscriminant { .. } - | StatementKind::StorageLive(_) - | StatementKind::StorageDead(_) - | StatementKind::Retag(_, _) - | StatementKind::PlaceMention(_) - | StatementKind::AscribeUserType { .. } - | StatementKind::Coverage(_) - | StatementKind::ConstEvalCounter - | StatementKind::Intrinsic(NonDivergingIntrinsic::Assume(_)) - | StatementKind::Nop => self.super_statement(stmt, location), } + StatementKind::Deinit(place) => { + self.super_statement(stmt, location); + self.push_target(MemoryInitOp::Set { + operand: Operand::Copy(place.clone()), + value: false, + position: InsertPosition::After, + }); + } + StatementKind::FakeRead(_, _) + | StatementKind::SetDiscriminant { .. } + | StatementKind::StorageLive(_) + | StatementKind::StorageDead(_) + | StatementKind::Retag(_, _) + | StatementKind::PlaceMention(_) + | StatementKind::AscribeUserType { .. } + | StatementKind::Coverage(_) + | StatementKind::ConstEvalCounter + | StatementKind::Intrinsic(NonDivergingIntrinsic::Assume(_)) + | StatementKind::Nop => self.super_statement(stmt, location), + } + // Switch to the next statement. + if let SourceInstruction::Statement { idx, bb } = self.current_target.source { + self.targets.push(self.current_target.clone()); + self.current_target = InitRelevantInstruction { + source: SourceInstruction::Statement { idx: idx + 1, bb }, + after_instruction: vec![], + before_instruction: vec![], + }; + } else { + unreachable!() } - let SourceInstruction::Statement { idx, bb } = self.current else { unreachable!() }; - self.current = SourceInstruction::Statement { idx: idx + 1, bb }; } fn visit_terminator(&mut self, term: &Terminator, location: Location) { - if !(self.skip_next || self.target.is_some()) { - self.current = SourceInstruction::Terminator { bb: self.bb }; - // Leave it as an exhaustive match to be notified when a new kind is added. - match &term.kind { - TerminatorKind::Call { func, args, destination, .. } => { - self.super_terminator(term, location); - let instance = match try_resolve_instance(&self.locals, func) { - Ok(instance) => instance, - Err(reason) => { - self.super_terminator(term, location); - self.push_target(MemoryInitOp::Unsupported { reason }); - return; + if let SourceInstruction::Statement { bb, .. } = self.current_target.source { + // We don't have to push the previous target, since it already happened in the statement + // handling code. + self.current_target = InitRelevantInstruction { + source: SourceInstruction::Terminator { bb }, + after_instruction: vec![], + before_instruction: vec![], + }; + } else { + unreachable!() + } + // Leave it as an exhaustive match to be notified when a new kind is added. + match &term.kind { + TerminatorKind::Call { func, args, destination, .. } => { + self.super_terminator(term, location); + let instance = match try_resolve_instance(&self.locals, func) { + Ok(instance) => instance, + Err(reason) => { + self.super_terminator(term, location); + self.push_target(MemoryInitOp::Unsupported { reason }); + return; + } + }; + match instance.kind { + InstanceKind::Intrinsic => { + match Intrinsic::from_instance(&instance) { + intrinsic_name if can_skip_intrinsic(intrinsic_name.clone()) => { + /* Intrinsics that can be safely skipped */ + } + Intrinsic::AtomicAnd(_) + | Intrinsic::AtomicCxchg(_) + | Intrinsic::AtomicCxchgWeak(_) + | Intrinsic::AtomicLoad(_) + | Intrinsic::AtomicMax(_) + | Intrinsic::AtomicMin(_) + | Intrinsic::AtomicNand(_) + | Intrinsic::AtomicOr(_) + | Intrinsic::AtomicStore(_) + | Intrinsic::AtomicUmax(_) + | Intrinsic::AtomicUmin(_) + | Intrinsic::AtomicXadd(_) + | Intrinsic::AtomicXchg(_) + | Intrinsic::AtomicXor(_) + | Intrinsic::AtomicXsub(_) => { + self.push_target(MemoryInitOp::Check { operand: args[0].clone() }); + } + Intrinsic::CompareBytes => { + self.push_target(MemoryInitOp::CheckSliceChunk { + operand: args[0].clone(), + count: args[2].clone(), + }); + self.push_target(MemoryInitOp::CheckSliceChunk { + operand: args[1].clone(), + count: args[2].clone(), + }); + } + Intrinsic::Copy => { + // The copy is untyped, so we should 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(), + }); + } + Intrinsic::VolatileCopyMemory + | Intrinsic::VolatileCopyNonOverlappingMemory => { + // The copy is untyped, so we should copy initialization state + // from `src` to `dst`. Note that the `dst` comes before `src` + // in this case. + self.push_target(MemoryInitOp::Copy { + from: args[1].clone(), + to: args[0].clone(), + count: args[2].clone(), + }); + } + Intrinsic::TypedSwap => { + self.push_target(MemoryInitOp::Check { operand: args[0].clone() }); + self.push_target(MemoryInitOp::Check { operand: args[1].clone() }); + } + Intrinsic::VolatileLoad | Intrinsic::UnalignedVolatileLoad => { + self.push_target(MemoryInitOp::Check { operand: args[0].clone() }); + } + Intrinsic::VolatileStore => { + self.push_target(MemoryInitOp::Set { + operand: args[0].clone(), + value: true, + position: InsertPosition::After, + }); + } + Intrinsic::WriteBytes => { + self.push_target(MemoryInitOp::SetSliceChunk { + operand: args[0].clone(), + count: args[2].clone(), + value: true, + position: InsertPosition::After, + }) + } + intrinsic => { + self.push_target(MemoryInitOp::Unsupported { + reason: format!("Kani does not support reasoning about memory initialization of intrinsic `{intrinsic:?}`."), + }); + } } - }; - match instance.kind { - InstanceKind::Intrinsic => { - match Intrinsic::from_instance(&instance) { - intrinsic_name if can_skip_intrinsic(intrinsic_name.clone()) => { - /* Intrinsics that can be safely skipped */ - } - Intrinsic::AtomicAnd(_) - | Intrinsic::AtomicCxchg(_) - | Intrinsic::AtomicCxchgWeak(_) - | Intrinsic::AtomicLoad(_) - | Intrinsic::AtomicMax(_) - | Intrinsic::AtomicMin(_) - | Intrinsic::AtomicNand(_) - | Intrinsic::AtomicOr(_) - | Intrinsic::AtomicStore(_) - | Intrinsic::AtomicUmax(_) - | Intrinsic::AtomicUmin(_) - | Intrinsic::AtomicXadd(_) - | Intrinsic::AtomicXchg(_) - | Intrinsic::AtomicXor(_) - | Intrinsic::AtomicXsub(_) => { - self.push_target(MemoryInitOp::Check { - operand: args[0].clone(), - }); - } - Intrinsic::CompareBytes => { - self.push_target(MemoryInitOp::CheckSliceChunk { - operand: args[0].clone(), - count: args[2].clone(), - }); - self.push_target(MemoryInitOp::CheckSliceChunk { - operand: args[1].clone(), - count: args[2].clone(), - }); - } - Intrinsic::Copy => { - // The copy is untyped, so we should 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(), - }); - } - Intrinsic::VolatileCopyMemory - | Intrinsic::VolatileCopyNonOverlappingMemory => { - // The copy is untyped, so we should copy initialization state - // from `src` to `dst`. Note that the `dst` comes before `src` - // in this case. - self.push_target(MemoryInitOp::Copy { - from: args[1].clone(), - to: args[0].clone(), - count: args[2].clone(), - }); - } - Intrinsic::TypedSwap => { - self.push_target(MemoryInitOp::Check { - operand: args[0].clone(), - }); - self.push_target(MemoryInitOp::Check { - operand: args[1].clone(), - }); - } - Intrinsic::VolatileLoad | Intrinsic::UnalignedVolatileLoad => { - self.push_target(MemoryInitOp::Check { - operand: args[0].clone(), - }); + } + InstanceKind::Item => { + if instance.is_foreign_item() { + match instance.name().as_str() { + "alloc::alloc::__rust_alloc" | "alloc::alloc::__rust_realloc" => { + /* Memory is uninitialized, nothing to do here. */ } - Intrinsic::VolatileStore => { - self.push_target(MemoryInitOp::Set { - operand: args[0].clone(), + "alloc::alloc::__rust_alloc_zeroed" => { + /* Memory is initialized here, need to update shadow memory. */ + self.push_target(MemoryInitOp::SetSliceChunk { + operand: Operand::Copy(destination.clone()), + count: args[0].clone(), value: true, position: InsertPosition::After, }); } - Intrinsic::WriteBytes => { + "alloc::alloc::__rust_dealloc" => { + /* Memory is uninitialized here, need to update shadow memory. */ self.push_target(MemoryInitOp::SetSliceChunk { operand: args[0].clone(), - count: args[2].clone(), - value: true, + count: args[1].clone(), + value: false, position: InsertPosition::After, - }) - } - intrinsic => { - self.push_target(MemoryInitOp::Unsupported { - reason: format!("Kani does not support reasoning about memory initialization of intrinsic `{intrinsic:?}`."), - }); - } - } - } - InstanceKind::Item => { - if instance.is_foreign_item() { - match instance.name().as_str() { - "alloc::alloc::__rust_alloc" - | "alloc::alloc::__rust_realloc" => { - /* Memory is uninitialized, nothing to do here. */ - } - "alloc::alloc::__rust_alloc_zeroed" => { - /* Memory is initialized here, need to update shadow memory. */ - self.push_target(MemoryInitOp::SetSliceChunk { - operand: Operand::Copy(destination.clone()), - count: args[0].clone(), - value: true, - position: InsertPosition::After, - }); - } - "alloc::alloc::__rust_dealloc" => { - /* Memory is uninitialized here, need to update shadow memory. */ - self.push_target(MemoryInitOp::SetSliceChunk { - operand: args[0].clone(), - count: args[1].clone(), - value: false, - position: InsertPosition::After, - }); - } - _ => {} + }); } + _ => {} } } - _ => {} } + _ => {} } - TerminatorKind::Drop { place, .. } => { - self.super_terminator(term, location); - let place_ty = place.ty(&&self.locals).unwrap(); - - // When drop is codegen'ed for types that could define their own dropping - // behavior, a reference is taken to the place which is later implicitly coerced - // to a pointer. Hence, we need to bless this pointer as initialized. - match place - .ty(&&self.locals) - .unwrap() - .kind() - .rigid() - .expect("should be working with monomorphized code") - { - RigidTy::Adt(..) | RigidTy::Dynamic(_, _, _) => { - self.push_target(MemoryInitOp::SetRef { - operand: Operand::Copy(place.clone()), - value: true, - position: InsertPosition::Before, - }); - } - _ => {} - } + } + TerminatorKind::Drop { place, .. } => { + self.super_terminator(term, location); + let place_ty = place.ty(&&self.locals).unwrap(); - if place_ty.kind().is_raw_ptr() { - self.push_target(MemoryInitOp::Set { + // When drop is codegen'ed for types that could define their own dropping + // behavior, a reference is taken to the place which is later implicitly coerced + // to a pointer. Hence, we need to bless this pointer as initialized. + match place + .ty(&&self.locals) + .unwrap() + .kind() + .rigid() + .expect("should be working with monomorphized code") + { + RigidTy::Adt(..) | RigidTy::Dynamic(_, _, _) => { + self.push_target(MemoryInitOp::SetRef { operand: Operand::Copy(place.clone()), - value: false, - position: InsertPosition::After, + value: true, + position: InsertPosition::Before, }); } + _ => {} + } + + if place_ty.kind().is_raw_ptr() { + self.push_target(MemoryInitOp::Set { + operand: Operand::Copy(place.clone()), + value: false, + position: InsertPosition::After, + }); } - TerminatorKind::Goto { .. } - | TerminatorKind::SwitchInt { .. } - | TerminatorKind::Resume - | TerminatorKind::Abort - | TerminatorKind::Return - | TerminatorKind::Unreachable - | TerminatorKind::Assert { .. } - | TerminatorKind::InlineAsm { .. } => self.super_terminator(term, location), } + TerminatorKind::Goto { .. } + | TerminatorKind::SwitchInt { .. } + | TerminatorKind::Resume + | TerminatorKind::Abort + | TerminatorKind::Return + | TerminatorKind::Unreachable + | TerminatorKind::Assert { .. } + | TerminatorKind::InlineAsm { .. } => self.super_terminator(term, location), } + // Push the current target from the terminator onto the list. + self.targets.push(self.current_target.clone()); } fn visit_place(&mut self, place: &Place, ptx: PlaceContext, location: Location) { 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 cc5a27e09925..05826969262d 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,9 @@ use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; use stable_mir::{ - mir::{Mutability, Operand, Place, Rvalue}, + mir::{Mutability, Operand, Place, Rvalue, Statement, StatementKind}, ty::RigidTy, + ty::Ty, }; use strum_macros::AsRefStr; @@ -44,27 +45,59 @@ 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::Copy { .. } + | 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!("operands do not exist for this operation") @@ -82,7 +115,7 @@ impl MemoryInitOp { unreachable!() }; assert!(from_pointee_ty == to_pointee_ty); - from.clone() + from.ty(body.locals()).unwrap() } } } diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index cc748c39a7f5..dd804b7379f2 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,39 @@ 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![]; + // 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 +204,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 +230,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); + + let 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 +272,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, + let 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 +322,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, diff --git a/tests/expected/uninit/multiple-instrumentations.expected b/tests/expected/uninit/multiple-instrumentations.expected new file mode 100644 index 000000000000..153024dc692b --- /dev/null +++ b/tests/expected/uninit/multiple-instrumentations.expected @@ -0,0 +1,20 @@ +multiple_instrumentations_different_vars.assertion.3\ + - Status: FAILURE\ + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" + +multiple_instrumentations_different_vars.assertion.4\ + - Status: FAILURE\ + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`" + +multiple_instrumentations.assertion.2\ + - Status: FAILURE\ + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" + +multiple_instrumentations.assertion.3\ + - Status: FAILURE\ + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" + +Summary: +Verification failed for - multiple_instrumentations_different_vars +Verification failed for - multiple_instrumentations +Complete - 0 successfully verified harnesses, 2 failures, 2 total. diff --git a/tests/expected/uninit/multiple-instrumentations.rs b/tests/expected/uninit/multiple-instrumentations.rs new file mode 100644 index 000000000000..8f61bb82b6d6 --- /dev/null +++ b/tests/expected/uninit/multiple-instrumentations.rs @@ -0,0 +1,42 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks + +/// Ensure instrumentation works correctly when a single instruction gets multiple instrumentations. +#[kani::proof] +fn multiple_instrumentations() { + unsafe { + let mut value: u128 = 0; + // Cast between two pointers of different padding. + let ptr = &mut value as *mut _ as *mut (u8, u32, u64); + *ptr = (4, 4, 4); + // Here, instrumentation is added 2 times before the function call and 1 time after. + value = helper_1(value, value); + } +} + +fn helper_1(a: u128, b: u128) -> u128 { + a + b +} + +/// Ensure instrumentation works correctly when a single instruction gets multiple instrumentations +/// (and variables are different). +#[kani::proof] +fn multiple_instrumentations_different_vars() { + unsafe { + let mut a: u128 = 0; + let mut b: u64 = 0; + // Cast between two pointers of different padding. + let ptr_a = &mut a as *mut _ as *mut (u8, u32, u64); + *ptr_a = (4, 4, 4); + // Cast between two pointers of different padding. + let ptr_b = &mut b as *mut _ as *mut (u8, u32); + *ptr_b = (4, 4); + // Here, instrumentation is added 2 times before the function call and 1 time after. + a = helper_2(a, b); + } +} + +fn helper_2(a: u128, b: u64) -> u128 { + a + (b as u128) +}