From b909c8be6de7a3afc7473bd20edbc3f1f82aeab8 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 14 Aug 2024 08:48:29 -0700 Subject: [PATCH 01/12] 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 c378ec50d5ce9cbbbdf88a4f2d666014a72269bb Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Fri, 16 Aug 2024 13:16:36 -0700 Subject: [PATCH 02/12] Backward iteration proof-of-concept --- .../src/kani_middle/transform/body.rs | 4 - .../delayed_ub/instrumentation_visitor.rs | 59 +-- .../kani_middle/transform/check_uninit/mod.rs | 103 ++-- .../check_uninit/ptr_uninit/uninit_visitor.rs | 483 +++++++++--------- .../check_uninit/relevant_instruction.rs | 2 - 5 files changed, 284 insertions(+), 367 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index e050084eaf44..59210bb3e3b2 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -503,10 +503,6 @@ 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/instrumentation_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs index f295fc76d4bf..f6354b827c37 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,18 +18,11 @@ use rustc_middle::ty::TyCtxt; use stable_mir::mir::{ mono::Instance, visit::{Location, PlaceContext}, - BasicBlockIdx, MirVisitor, Operand, Place, Rvalue, Statement, Terminator, + BasicBlock, MirVisitor, Operand, Place, Rvalue, }; 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, /// Aliasing analysis data. @@ -44,13 +37,23 @@ impl<'a, 'tcx> TargetFinder for InstrumentationVisitor<'a, 'tcx> { fn find_next( &mut self, body: &MutableBody, - bb: BasicBlockIdx, - skip_first: bool, + source: &SourceInstruction, ) -> Option { - self.skip_next = skip_first; - self.current = SourceInstruction::Statement { idx: 0, bb }; self.target = None; - self.visit_basic_block(&body.blocks()[bb]); + match *source { + SourceInstruction::Statement { idx, bb } => { + let BasicBlock { statements, .. } = &body.blocks()[bb]; + let stmt = &statements[idx]; + self.visit_statement(stmt, self.__location_hack_remove_before_merging(stmt.span)) + } + SourceInstruction::Terminator { bb } => { + let BasicBlock { terminator, .. } = &body.blocks()[bb]; + self.visit_terminator( + terminator, + self.__location_hack_remove_before_merging(terminator.span), + ) + } + } self.target.clone() } } @@ -62,19 +65,10 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> { current_instance: Instance, tcx: TyCtxt<'tcx>, ) -> Self { - Self { - skip_next: false, - current: SourceInstruction::Statement { idx: 0, bb: 0 }, - target: None, - points_to, - analysis_targets, - current_instance, - tcx, - } + Self { target: None, 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![], }); @@ -83,25 +77,6 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> { } 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); - } - // Switch to the next statement. - 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.current.bb() }; - self.super_terminator(term, location); - } - } - fn visit_rvalue(&mut self, rvalue: &Rvalue, location: Location) { match rvalue { Rvalue::AddressOf(..) | Rvalue::Ref(..) => { 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 d9130719b39f..95e15a21fba0 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,15 @@ use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use stable_mir::{ mir::{ - mono::Instance, AggregateKind, BasicBlock, BasicBlockIdx, Body, ConstOperand, Mutability, + mono::Instance, visit::Location, AggregateKind, BasicBlock, Body, ConstOperand, Mutability, Operand, Place, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, UnwindAction, }, - ty::{FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Ty, TyConst, TyKind, UintTy}, + ty::{ + FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Span, Ty, TyConst, TyKind, UintTy, + }, CrateDef, }; -use std::collections::{HashMap, HashSet}; +use std::collections::HashMap; pub use delayed_ub::DelayedUbPass; pub use ptr_uninit::UninitPass; @@ -35,9 +37,14 @@ pub trait TargetFinder { fn find_next( &mut self, body: &MutableBody, - bb: BasicBlockIdx, - skip_first: bool, + source: &SourceInstruction, ) -> Option; + + /// TODO: This is just a temporary fix to unblock me because I couldn't create Location + /// directly. Perhaps we need to make a change in StableMIR to allow creating Location. + fn __location_hack_remove_before_merging(&self, span: Span) -> Location { + unsafe { std::mem::transmute(span) } + } } // Function bodies of those functions will not be instrumented as not to cause infinite recursion. @@ -58,22 +65,6 @@ pub struct UninitInstrumenter<'a, 'tcx> { /// Used to cache FnDef lookups of injected memory initialization functions. 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, 'tcx> UninitInstrumenter<'a, 'tcx> { @@ -86,13 +77,7 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { 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 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()) @@ -120,19 +105,32 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { } let orig_len = body.blocks().len(); - - // 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() { - // 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); + let mut source = SourceInstruction::Terminator { bb: body.blocks().len() - 1 }; + loop { + if let Some(candidate) = target_finder.find_next(&body, &source) { + self.build_check_for_instruction(&mut body, candidate, source); + } + source = match source { + SourceInstruction::Statement { idx, bb } => { + if bb == 0 && idx == 0 { + break; + } else if idx == 0 { + SourceInstruction::Terminator { bb: bb - 1 } + } else { + SourceInstruction::Statement { idx: idx - 1, bb } + } + } + SourceInstruction::Terminator { bb } => { + let stmt_len = body.blocks()[bb].statements.len(); + if bb == 0 && stmt_len == 0 { + break; + } else if stmt_len == 0 { + SourceInstruction::Terminator { bb: bb - 1 } + } else { + SourceInstruction::Statement { idx: stmt_len - 1, bb } + } } } - bb_idx += 1; } (orig_len != body.blocks().len(), body) } @@ -142,8 +140,8 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { &mut self, body: &mut MutableBody, instruction: InitRelevantInstruction, + mut source: SourceInstruction, ) { - let mut source = instruction.source; for operation in instruction.before_instruction { self.build_check_for_operation(body, &mut source, operation); } @@ -164,7 +162,6 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { { // 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; }; @@ -188,7 +185,6 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { let reason = format!( "Kani currently doesn't support checking memory initialization for pointers to `{pointee_ty}.", ); - collect_skipped(operation.position(), source, body, &mut self.skip_first); self.inject_assert_false(self.tcx, body, source, operation.position(), &reason); return; } @@ -301,7 +297,6 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { } } PointeeLayout::TraitObject => { - 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(self.tcx, body, source, operation.position(), reason); return; @@ -309,13 +304,10 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { }; // 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, .. } @@ -454,9 +446,7 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { } }; // 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); } /// Copy memory initialization state from one pointer to the other. @@ -478,7 +468,6 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { *pointee_info.ty(), ); let position = operation.position(); - collect_skipped(position, source, body, &mut self.skip_first); let MemoryInitOp::Copy { from, to, count } = operation else { unreachable!() }; body.insert_call( ©_init_state_instance, @@ -548,22 +537,6 @@ pub fn mk_layout_operand( 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( - 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); - } -} - /// Retrieve a function definition by diagnostic string, caching the result. pub fn get_mem_init_fn_def( 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 1afb151a09b5..9f6b2a881e71 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,7 +19,7 @@ use stable_mir::{ alloc::GlobalAlloc, mono::{Instance, InstanceKind}, visit::{Location, PlaceContext}, - BasicBlockIdx, CastKind, LocalDecl, MirVisitor, NonDivergingIntrinsic, Operand, Place, + BasicBlock, CastKind, LocalDecl, MirVisitor, NonDivergingIntrinsic, Operand, Place, PointerCoercion, ProjectionElem, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, }, @@ -28,50 +28,43 @@ use stable_mir::{ 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, } impl TargetFinder for CheckUninitVisitor { fn find_next( &mut self, body: &MutableBody, - bb: BasicBlockIdx, - skip_first: bool, + source: &SourceInstruction, ) -> Option { 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]); + match *source { + SourceInstruction::Statement { idx, bb } => { + let BasicBlock { statements, .. } = &body.blocks()[bb]; + let stmt = &statements[idx]; + self.visit_statement(stmt, self.__location_hack_remove_before_merging(stmt.span)) + } + SourceInstruction::Terminator { bb } => { + let BasicBlock { terminator, .. } = &body.blocks()[bb]; + self.visit_terminator( + terminator, + self.__location_hack_remove_before_merging(terminator.span), + ) + } + } self.target.clone() } } impl CheckUninitVisitor { pub fn new() -> Self { - Self { - locals: vec![], - skip_next: false, - current: SourceInstruction::Statement { idx: 0, bb: 0 }, - target: None, - bb: 0, - } + Self { locals: vec![], target: None } } 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![], }); @@ -81,266 +74,248 @@ impl CheckUninitVisitor { 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), } - 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; + // 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), } } diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs b/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs index 05826969262d..d3eb0c1d51dc 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 @@ -168,8 +168,6 @@ impl MemoryInitOp { /// before or after the instruction. #[derive(Clone, Debug)] pub struct InitRelevantInstruction { - /// The instruction that affects the state of the memory. - pub source: SourceInstruction, /// All memory-related operations that should happen after the instruction. pub before_instruction: Vec, /// All memory-related operations that should happen after the instruction. From ff4862ad87ebfc68b134bb97a714c1f99ebe0e0d Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Fri, 16 Aug 2024 14:00:39 -0700 Subject: [PATCH 03/12] Address comments from code review --- kani-compiler/src/kani_middle/transform/kani_intrinsics.rs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index 2b9d6d22f040..dd804b7379f2 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -190,7 +190,6 @@ impl IntrinsicGeneratorPass { // 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; @@ -234,7 +233,7 @@ impl IntrinsicGeneratorPass { let layout_operand = mk_layout_operand(&mut new_body, &mut statements, &mut source, &layout); - terminator = Terminator { + let terminator = Terminator { kind: TerminatorKind::Call { func: Operand::Copy(Place::from(new_body.new_local( is_ptr_initialized_instance.ty(), @@ -277,7 +276,7 @@ impl IntrinsicGeneratorPass { &mut source, &element_layout, ); - terminator = Terminator { + let terminator = Terminator { kind: TerminatorKind::Call { func: Operand::Copy(Place::from(new_body.new_local( is_ptr_initialized_instance.ty(), From eb05f74e62b56889da93ccf13131a8c715a14298 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Sat, 17 Aug 2024 12:23:10 -0700 Subject: [PATCH 04/12] Stop using visitor for instrumentation target finding --- .../delayed_ub/instrumentation_visitor.rs | 201 +++++++++-- .../kani_middle/transform/check_uninit/mod.rs | 14 +- .../check_uninit/ptr_uninit/uninit_visitor.rs | 323 +++++++++++------- 3 files changed, 373 insertions(+), 165 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs index f6354b827c37..3ede2988f143 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs @@ -16,9 +16,8 @@ use crate::kani_middle::{ }; use rustc_middle::ty::TyCtxt; use stable_mir::mir::{ - mono::Instance, - visit::{Location, PlaceContext}, - BasicBlock, MirVisitor, Operand, Place, Rvalue, + mono::Instance, BasicBlock, CopyNonOverlapping, InlineAsmOperand, NonDivergingIntrinsic, + Operand, Place, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, }; use std::collections::HashSet; @@ -33,6 +32,13 @@ pub struct InstrumentationVisitor<'a, 'tcx> { tcx: TyCtxt<'tcx>, } +enum PlaceOperation { + Read, + Write, + Deinit, + Noop, +} + impl<'a, 'tcx> TargetFinder for InstrumentationVisitor<'a, 'tcx> { fn find_next( &mut self, @@ -44,14 +50,11 @@ impl<'a, 'tcx> TargetFinder for InstrumentationVisitor<'a, 'tcx> { SourceInstruction::Statement { idx, bb } => { let BasicBlock { statements, .. } = &body.blocks()[bb]; let stmt = &statements[idx]; - self.visit_statement(stmt, self.__location_hack_remove_before_merging(stmt.span)) + self.check_statement(stmt) } SourceInstruction::Terminator { bb } => { let BasicBlock { terminator, .. } = &body.blocks()[bb]; - self.visit_terminator( - terminator, - self.__location_hack_remove_before_merging(terminator.span), - ) + self.check_terminator(terminator) } } self.target.clone() @@ -76,17 +79,152 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> { } } -impl<'a, 'tcx> MirVisitor for InstrumentationVisitor<'a, 'tcx> { - fn visit_rvalue(&mut self, rvalue: &Rvalue, location: Location) { +impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> { + fn check_statement(&mut self, stmt: &Statement) { + let Statement { kind, .. } = stmt; + match kind { + StatementKind::Assign(place, rvalue) => { + self.check_place(place, PlaceOperation::Write); + self.check_rvalue(rvalue); + } + StatementKind::FakeRead(_, place) => { + // According to the compiler docs, "When executed at runtime this is a nop." For + // more info, see + // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.StatementKind.html#variant.FakeRead, + self.check_place(place, PlaceOperation::Noop); + } + StatementKind::SetDiscriminant { place, .. } => { + self.check_place(place, PlaceOperation::Write); + } + StatementKind::Deinit(place) => { + self.check_place(place, PlaceOperation::Deinit); + } + StatementKind::Retag(_, place) => { + // According to the compiler docs, "These statements are currently only interpreted + // by miri and only generated when -Z mir-emit-retag is passed." For more info, see + // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.StatementKind.html#variant.Retag, + self.check_place(place, PlaceOperation::Noop); + } + StatementKind::PlaceMention(place) => { + // According to the compiler docs, "When executed at runtime, this computes the + // given place, but then discards it without doing a load." For more info, see + // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.StatementKind.html#variant.PlaceMention, + self.check_place(place, PlaceOperation::Noop); + } + StatementKind::AscribeUserType { place, .. } => { + // According to the compiler docs, "When executed at runtime this is a nop." For + // more info, see + // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.StatementKind.html#variant.AscribeUserType, + self.check_place(place, PlaceOperation::Noop); + } + + StatementKind::Intrinsic(intrisic) => match intrisic { + NonDivergingIntrinsic::Assume(operand) => { + self.check_operand(operand); + } + NonDivergingIntrinsic::CopyNonOverlapping(CopyNonOverlapping { + src, + dst, + count, + }) => { + self.check_operand(src); + self.check_operand(dst); + self.check_operand(count); + } + }, + StatementKind::StorageLive(_) + | StatementKind::StorageDead(_) + | StatementKind::Coverage(_) + | StatementKind::ConstEvalCounter + | StatementKind::Nop => {} + } + } + + fn check_terminator(&mut self, term: &Terminator) { + let Terminator { kind, .. } = term; + match kind { + TerminatorKind::Goto { .. } + | TerminatorKind::Resume + | TerminatorKind::Abort + | TerminatorKind::Unreachable + | TerminatorKind::Return => {} + TerminatorKind::Assert { cond, .. } => { + self.check_operand(cond); + } + TerminatorKind::Drop { place, .. } => { + // According to the documentation, "After drop elaboration: Drop terminators are a + // complete nop for types that have no drop glue. For other types, Drop terminators + // behave exactly like a call to core::mem::drop_in_place with a pointer to the + // given place." Since we check arguments when instrumenting function calls, perhaps + // we need to check that one, too. For more info, see: + // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.TerminatorKind.html#variant.Drop + self.check_place(place, PlaceOperation::Read); + } + TerminatorKind::Call { func, args, destination, target: _, unwind: _ } => { + self.check_operand(func); + for arg in args { + self.check_operand(arg); + } + self.check_place(destination, PlaceOperation::Write); + } + TerminatorKind::InlineAsm { operands, .. } => { + for op in operands { + let InlineAsmOperand { in_value, out_place, raw_rpr: _ } = op; + if let Some(input) = in_value { + self.check_operand(input); + } + if let Some(output) = out_place { + self.check_place(output, PlaceOperation::Write); + } + } + } + TerminatorKind::SwitchInt { discr, .. } => { + self.check_operand(discr); + } + } + } + + fn check_rvalue(&mut self, rvalue: &Rvalue) { match rvalue { - Rvalue::AddressOf(..) | Rvalue::Ref(..) => { - // These operations are always legitimate for us. + Rvalue::AddressOf(_, place) | Rvalue::Ref(_, _, place) => { + self.check_place(place, PlaceOperation::Noop); + } + Rvalue::Aggregate(_, operands) => { + for op in operands { + self.check_operand(op); + } + } + Rvalue::BinaryOp(_, lhs, rhs) | Rvalue::CheckedBinaryOp(_, lhs, rhs) => { + self.check_operand(lhs); + self.check_operand(rhs); + } + Rvalue::Cast(_, op, _) + | Rvalue::Repeat(op, _) + | Rvalue::ShallowInitBox(op, ..) + | Rvalue::UnaryOp(_, op) + | Rvalue::Use(op) => { + self.check_operand(op); + } + Rvalue::CopyForDeref(place) | Rvalue::Discriminant(place) | Rvalue::Len(place) => { + self.check_place(place, PlaceOperation::Read); + } + Rvalue::ThreadLocalRef(..) | Rvalue::NullaryOp(..) => {} + } + } + + fn check_operand(&mut self, operand: &Operand) { + match operand { + Operand::Copy(place) | Operand::Move(place) => { + self.check_place(place, PlaceOperation::Read) + } + Operand::Constant(_) => { + // Those should be safe to skip, as they are either constants or statics. In the + // latter case, we handle them in regular uninit visior } - _ => self.super_rvalue(rvalue, location), } } - fn visit_place(&mut self, place: &Place, ptx: PlaceContext, location: Location) { + fn check_place(&mut self, place: &Place, place_operation: PlaceOperation) { // Match the place by whatever it is pointing to and find an intersection with the targets. if self .points_to @@ -95,18 +233,31 @@ impl<'a, 'tcx> MirVisitor for InstrumentationVisitor<'a, 'tcx> { .next() .is_some() { - // If we are mutating the place, initialize it. - if ptx.is_mutating() { - self.push_target(MemoryInitOp::SetRef { - operand: Operand::Copy(place.clone()), - value: true, - position: InsertPosition::After, - }); - } else { - // Otherwise, check its initialization. - self.push_target(MemoryInitOp::CheckRef { operand: Operand::Copy(place.clone()) }); + match place_operation { + PlaceOperation::Write => { + // If we are mutating the place, initialize it. + self.push_target(MemoryInitOp::SetRef { + operand: Operand::Copy(place.clone()), + value: true, + position: InsertPosition::After, + }) + } + PlaceOperation::Deinit => { + // If we are mutating the place, initialize it. + self.push_target(MemoryInitOp::SetRef { + operand: Operand::Copy(place.clone()), + value: false, + position: InsertPosition::After, + }) + } + PlaceOperation::Read => { + // Otherwise, check its initialization. + self.push_target(MemoryInitOp::CheckRef { + operand: Operand::Copy(place.clone()), + }); + } + PlaceOperation::Noop => {} } } - self.super_place(place, ptx, location) } } diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs index 95e15a21fba0..50b640cfcb54 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -13,12 +13,10 @@ use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use stable_mir::{ mir::{ - mono::Instance, visit::Location, AggregateKind, BasicBlock, Body, ConstOperand, Mutability, - Operand, Place, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, UnwindAction, - }, - ty::{ - FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Span, Ty, TyConst, TyKind, UintTy, + mono::Instance, AggregateKind, BasicBlock, Body, ConstOperand, Mutability, Operand, Place, + Rvalue, Statement, StatementKind, Terminator, TerminatorKind, UnwindAction, }, + ty::{FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Ty, TyConst, TyKind, UintTy}, CrateDef, }; use std::collections::HashMap; @@ -39,12 +37,6 @@ pub trait TargetFinder { body: &MutableBody, source: &SourceInstruction, ) -> Option; - - /// TODO: This is just a temporary fix to unblock me because I couldn't create Location - /// directly. Perhaps we need to make a change in StableMIR to allow creating Location. - fn __location_hack_remove_before_merging(&self, span: Span) -> Location { - unsafe { std::mem::transmute(span) } - } } // Function bodies of those functions will not be instrumented as not to cause infinite recursion. diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs index 9f6b2a881e71..d6d125aeeb79 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs @@ -18,10 +18,9 @@ use stable_mir::{ mir::{ alloc::GlobalAlloc, mono::{Instance, InstanceKind}, - visit::{Location, PlaceContext}, - BasicBlock, CastKind, LocalDecl, MirVisitor, NonDivergingIntrinsic, Operand, Place, - PointerCoercion, ProjectionElem, Rvalue, Statement, StatementKind, Terminator, - TerminatorKind, + BasicBlock, CastKind, CopyNonOverlapping, InlineAsmOperand, LocalDecl, + NonDivergingIntrinsic, Operand, Place, PointerCoercion, ProjectionElem, Rvalue, Statement, + StatementKind, Terminator, TerminatorKind, }, ty::{ConstantKind, RigidTy, TyKind}, }; @@ -44,14 +43,11 @@ impl TargetFinder for CheckUninitVisitor { SourceInstruction::Statement { idx, bb } => { let BasicBlock { statements, .. } = &body.blocks()[bb]; let stmt = &statements[idx]; - self.visit_statement(stmt, self.__location_hack_remove_before_merging(stmt.span)) + self.check_statement(stmt) } SourceInstruction::Terminator { bb } => { let BasicBlock { terminator, .. } = &body.blocks()[bb]; - self.visit_terminator( - terminator, - self.__location_hack_remove_before_merging(terminator.span), - ) + self.check_terminator(terminator) } } self.target.clone() @@ -72,23 +68,28 @@ impl CheckUninitVisitor { } } -impl MirVisitor for CheckUninitVisitor { - fn visit_statement(&mut self, stmt: &Statement, location: Location) { +impl CheckUninitVisitor { + /// Check the statement and find all potential instrumentation targets. + fn check_statement(&mut self, stmt: &Statement) { // Leave it as an exhaustive match to be notified when a new kind is added. match &stmt.kind { - StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping(copy)) => { - self.super_statement(stmt, location); + StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping( + CopyNonOverlapping { src, dst, count }, + )) => { + self.check_operand(src); + self.check_operand(dst); + self.check_operand(count); // The copy is untyped, so we should copy memory initialization state from `src` // to `dst`. self.push_target(MemoryInitOp::Copy { - from: copy.src.clone(), - to: copy.dst.clone(), - count: copy.count.clone(), + from: src.clone(), + to: dst.clone(), + count: count.clone(), }); } StatementKind::Assign(place, rvalue) => { // First check rvalue. - self.visit_rvalue(rvalue, location); + self.check_rvalue(rvalue); // Check whether we are assigning into a dereference (*ptr = _). if let Some(place_without_deref) = try_remove_topmost_deref(place) { // First, check that we are not dereferencing extra pointers along the way @@ -99,8 +100,8 @@ impl MirVisitor for CheckUninitVisitor { // If the projection is Deref and the current type is raw pointer, check // if it points to initialized memory. if *projection_elem == ProjectionElem::Deref { - if let TyKind::RigidTy(RigidTy::RawPtr(..)) = - place_to_add_projections.ty(&&self.locals).unwrap().kind() + if let TyKind::RigidTy(RigidTy::RawPtr(_, _)) = + place_to_add_projections.ty(&self.locals).unwrap().kind() { self.push_target(MemoryInitOp::Check { operand: Operand::Copy(place_to_add_projections.clone()), @@ -109,7 +110,7 @@ impl MirVisitor for CheckUninitVisitor { } place_to_add_projections.projection.push(projection_elem.clone()); } - if place_without_deref.ty(&&self.locals).unwrap().kind().is_raw_ptr() { + if place_without_deref.ty(&self.locals).unwrap().kind().is_raw_ptr() { self.push_target(MemoryInitOp::Set { operand: Operand::Copy(place_without_deref), value: true, @@ -118,8 +119,8 @@ impl MirVisitor for CheckUninitVisitor { } } // Check whether Rvalue creates a new initialized pointer previously not captured inside shadow memory. - if place.ty(&&self.locals).unwrap().kind().is_raw_ptr() { - if let Rvalue::AddressOf(..) = rvalue { + if place.ty(&self.locals).unwrap().kind().is_raw_ptr() { + if let Rvalue::AddressOf(_, _) = rvalue { self.push_target(MemoryInitOp::Set { operand: Operand::Copy(place.clone()), value: true, @@ -129,36 +130,44 @@ impl MirVisitor for CheckUninitVisitor { } } StatementKind::Deinit(place) => { - self.super_statement(stmt, location); + self.check_place(place); self.push_target(MemoryInitOp::Set { operand: Operand::Copy(place.clone()), value: false, position: InsertPosition::After, }); } - StatementKind::FakeRead(_, _) - | StatementKind::SetDiscriminant { .. } - | StatementKind::StorageLive(_) + StatementKind::FakeRead(_, place) + | StatementKind::SetDiscriminant { place, .. } + | StatementKind::Retag(_, place) + | StatementKind::PlaceMention(place) + | StatementKind::AscribeUserType { place, .. } => { + self.check_place(place); + } + StatementKind::Intrinsic(NonDivergingIntrinsic::Assume(operand)) => { + self.check_operand(operand); + } + StatementKind::StorageLive(_) | StatementKind::StorageDead(_) - | StatementKind::Retag(_, _) - | StatementKind::PlaceMention(_) - | StatementKind::AscribeUserType { .. } | StatementKind::Coverage(_) | StatementKind::ConstEvalCounter - | StatementKind::Intrinsic(NonDivergingIntrinsic::Assume(_)) - | StatementKind::Nop => self.super_statement(stmt, location), + | StatementKind::Nop => {} } } - fn visit_terminator(&mut self, term: &Terminator, location: Location) { + /// Check the terminator and find all potential instrumentation targets. + fn check_terminator(&mut self, term: &Terminator) { // Leave it as an exhaustive match to be notified when a new kind is added. match &term.kind { TerminatorKind::Call { func, args, destination, .. } => { - self.super_terminator(term, location); + self.check_operand(func); + for arg in args { + self.check_operand(arg); + } + self.check_place(destination); let instance = match try_resolve_instance(&self.locals, func) { Ok(instance) => instance, Err(reason) => { - self.super_terminator(term, location); self.push_target(MemoryInitOp::Unsupported { reason }); return; } @@ -277,20 +286,20 @@ impl MirVisitor for CheckUninitVisitor { } } TerminatorKind::Drop { place, .. } => { - self.super_terminator(term, location); - let place_ty = place.ty(&&self.locals).unwrap(); + self.check_place(place); + let place_ty = place.ty(&self.locals).unwrap(); // When drop is codegen'ed for types that could define their own dropping // behavior, a reference is taken to the place which is later implicitly coerced // to a pointer. Hence, we need to bless this pointer as initialized. match place - .ty(&&self.locals) + .ty(&self.locals) .unwrap() .kind() .rigid() .expect("should be working with monomorphized code") { - RigidTy::Adt(..) | RigidTy::Dynamic(_, _, _) => { + RigidTy::Adt(_, _) | RigidTy::Dynamic(_, _, _) => { self.push_target(MemoryInitOp::SetRef { operand: Operand::Copy(place.clone()), value: true, @@ -309,121 +318,177 @@ impl MirVisitor for CheckUninitVisitor { } } TerminatorKind::Goto { .. } - | TerminatorKind::SwitchInt { .. } | TerminatorKind::Resume | TerminatorKind::Abort | TerminatorKind::Return - | TerminatorKind::Unreachable - | TerminatorKind::Assert { .. } - | TerminatorKind::InlineAsm { .. } => self.super_terminator(term, location), - } - } - - fn visit_place(&mut self, place: &Place, ptx: PlaceContext, location: Location) { - for (idx, elem) in place.projection.iter().enumerate() { - let intermediate_place = - Place { local: place.local, projection: place.projection[..idx].to_vec() }; - match elem { - ProjectionElem::Deref => { - let ptr_ty = intermediate_place.ty(&self.locals).unwrap(); - if ptr_ty.kind().is_raw_ptr() { - self.push_target(MemoryInitOp::Check { - operand: Operand::Copy(intermediate_place.clone()), - }); + | TerminatorKind::Unreachable => {} + TerminatorKind::SwitchInt { discr, .. } => { + self.check_operand(discr); + } + TerminatorKind::Assert { cond, .. } => { + self.check_operand(cond); + } + TerminatorKind::InlineAsm { operands, .. } => { + for op in operands { + let InlineAsmOperand { in_value, out_place, raw_rpr: _ } = op; + if let Some(input) = in_value { + self.check_operand(input); } - } - ProjectionElem::Field(idx, target_ty) => { - if target_ty.kind().is_union() - && (!ptx.is_mutating() || place.projection.len() > idx + 1) - { - self.push_target(MemoryInitOp::Unsupported { - reason: "Kani does not support reasoning about memory initialization of unions.".to_string(), - }); + if let Some(output) = out_place { + self.check_place(output); } } - ProjectionElem::Index(_) - | ProjectionElem::ConstantIndex { .. } - | ProjectionElem::Subslice { .. } => { - /* For a slice to be indexed, it should be valid first. */ - } - ProjectionElem::Downcast(_) => {} - ProjectionElem::OpaqueCast(_) => {} - ProjectionElem::Subtype(_) => {} } } - self.super_place(place, ptx, location) } - fn visit_operand(&mut self, operand: &Operand, location: Location) { - if let Operand::Constant(constant) = operand { - if let ConstantKind::Allocated(allocation) = constant.const_.kind() { - for (_, prov) in &allocation.provenance.ptrs { - if let GlobalAlloc::Static(_) = GlobalAlloc::from(prov.0) { - if constant.ty().kind().is_raw_ptr() { - // If a static is a raw pointer, need to mark it as initialized. - self.push_target(MemoryInitOp::Set { - operand: Operand::Constant(constant.clone()), - value: true, - position: InsertPosition::Before, - }); - } - }; + /// Check the rvalue and find all potential instrumentation targets. + fn check_rvalue(&mut self, rvalue: &Rvalue) { + match rvalue { + Rvalue::Aggregate(_, operands) => { + for op in operands { + self.check_operand(op); } } - } - self.super_operand(operand, location); - } - - fn visit_rvalue(&mut self, rvalue: &Rvalue, location: Location) { - if let Rvalue::Cast(cast_kind, operand, ty) = rvalue { - match cast_kind { - CastKind::PointerCoercion(PointerCoercion::Unsize) => { - if let TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) = ty.kind() { - if pointee_ty.kind().is_trait() { - self.push_target(MemoryInitOp::Unsupported { + Rvalue::BinaryOp(_, lhs, rhs) | Rvalue::CheckedBinaryOp(_, lhs, rhs) => { + self.check_operand(lhs); + self.check_operand(rhs); + } + Rvalue::AddressOf(_, place) + | Rvalue::CopyForDeref(place) + | Rvalue::Discriminant(place) + | Rvalue::Len(place) + | Rvalue::Ref(_, _, place) => { + self.check_place(place); + } + Rvalue::ShallowInitBox(op, _) + | Rvalue::UnaryOp(_, op) + | Rvalue::Use(op) + | Rvalue::Repeat(op, _) => { + self.check_operand(op); + } + Rvalue::NullaryOp(_, _) | Rvalue::ThreadLocalRef(_) => {} + Rvalue::Cast(cast_kind, op, ty) => { + self.check_operand(op); + match cast_kind { + // We currently do not support soundly reasoning about trait objects, so need to + // notify the user. + CastKind::PointerCoercion(PointerCoercion::Unsize) => { + if let TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) = ty.kind() { + if pointee_ty.kind().is_trait() { + self.push_target(MemoryInitOp::Unsupported { reason: "Kani does not support reasoning about memory initialization of unsized pointers.".to_string(), }); + } } } - } - CastKind::Transmute => { - let operand_ty = operand.ty(&self.locals).unwrap(); - if !tys_layout_compatible_to_size(&operand_ty, &ty) { - // If transmuting between two types of incompatible layouts, padding - // bytes are exposed, which is UB. - self.push_target(MemoryInitOp::TriviallyUnsafe { - reason: "Transmuting between types of incompatible layouts." - .to_string(), - }); - } else if let ( - TyKind::RigidTy(RigidTy::Ref(_, from_ty, _)), - TyKind::RigidTy(RigidTy::Ref(_, to_ty, _)), - ) = (operand_ty.kind(), ty.kind()) - { - if !tys_layout_compatible_to_size(&from_ty, &to_ty) { - // Since references are supposed to always be initialized for its type, - // transmuting between two references of incompatible layout is UB. + CastKind::Transmute => { + let operand_ty = op.ty(&self.locals).unwrap(); + if !tys_layout_compatible_to_size(&operand_ty, &ty) { + // If transmuting between two types of incompatible layouts, padding + // bytes are exposed, which is UB. self.push_target(MemoryInitOp::TriviallyUnsafe { + reason: "Transmuting between types of incompatible layouts." + .to_string(), + }); + } else if let ( + TyKind::RigidTy(RigidTy::Ref(_, from_ty, _)), + TyKind::RigidTy(RigidTy::Ref(_, to_ty, _)), + ) = (operand_ty.kind(), ty.kind()) + { + if !tys_layout_compatible_to_size(&from_ty, &to_ty) { + // Since references are supposed to always be initialized for its type, + // transmuting between two references of incompatible layout is UB. + self.push_target(MemoryInitOp::TriviallyUnsafe { reason: "Transmuting between references pointing to types of incompatible layouts." .to_string(), }); + } + } else if let ( + TyKind::RigidTy(RigidTy::RawPtr(from_ty, _)), + TyKind::RigidTy(RigidTy::Ref(_, to_ty, _)), + ) = (operand_ty.kind(), ty.kind()) + { + // Assert that we can only cast this way if types are the same. + assert!(from_ty == to_ty); + // When transmuting from a raw pointer to a reference, need to check that + // the value pointed by the raw pointer is initialized. + self.push_target(MemoryInitOp::Check { operand: op.clone() }); } - } else if let ( - TyKind::RigidTy(RigidTy::RawPtr(from_ty, _)), - TyKind::RigidTy(RigidTy::Ref(_, to_ty, _)), - ) = (operand_ty.kind(), ty.kind()) - { - // Assert that we can only cast this way if types are the same. - assert!(from_ty == to_ty); - // When transmuting from a raw pointer to a reference, need to check that - // the value pointed by the raw pointer is initialized. - self.push_target(MemoryInitOp::Check { operand: operand.clone() }); } + _ => {} + } + } + } + } + + /// Check if one of the place projections involves dereferencing a raw pointer, which is an + /// instrumentation target , or union access, which is currently not supported. + fn check_place(&mut self, place: &Place) { + for (idx, elem) in place.projection.iter().enumerate() { + let intermediate_place = + Place { local: place.local, projection: place.projection[..idx].to_vec() }; + self.check_projection_elem(elem, intermediate_place) + } + } + + /// Check if the projection involves dereferencing a raw pointer, which is an instrumentation + /// target, or union access, which is currently not supported. + fn check_projection_elem( + &mut self, + projection_elem: &ProjectionElem, + intermediate_place: Place, + ) { + match projection_elem { + ProjectionElem::Deref => { + let ptr_ty = intermediate_place.ty(&self.locals).unwrap(); + if ptr_ty.kind().is_raw_ptr() { + self.push_target(MemoryInitOp::Check { + operand: Operand::Copy(intermediate_place.clone()), + }); } - _ => {} } - }; - self.super_rvalue(rvalue, location); + ProjectionElem::Field(_, _) => { + if intermediate_place.ty(&self.locals).unwrap().kind().is_union() { + self.push_target(MemoryInitOp::Unsupported { + reason: + "Kani does not support reasoning about memory initialization of unions." + .to_string(), + }); + } + } + ProjectionElem::Index(_) + | ProjectionElem::ConstantIndex { .. } + | ProjectionElem::Subslice { .. } => { + /* For a slice to be indexed, it should be valid first. */ + } + ProjectionElem::Downcast(_) => {} + ProjectionElem::OpaqueCast(_) => {} + ProjectionElem::Subtype(_) => {} + } + } + + /// Check if the operand is a static to initialize it or else check its associated place. + fn check_operand(&mut self, operand: &Operand) { + match operand { + Operand::Copy(place) | Operand::Move(place) => self.check_place(place), + Operand::Constant(constant) => { + if let ConstantKind::Allocated(allocation) = constant.const_.kind() { + for (_, prov) in &allocation.provenance.ptrs { + if let GlobalAlloc::Static(_) = GlobalAlloc::from(prov.0) { + if constant.ty().kind().is_raw_ptr() { + // If a static is a raw pointer, need to mark it as initialized. + self.push_target(MemoryInitOp::Set { + operand: Operand::Constant(constant.clone()), + value: true, + position: InsertPosition::Before, + }); + } + }; + } + } + } + } } } From cc1798b1f2539cac0ab4ba3fec1b05df43496dd1 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Sat, 17 Aug 2024 12:29:21 -0700 Subject: [PATCH 05/12] Add docstring for `PlaceOperation` --- .../check_uninit/delayed_ub/instrumentation_visitor.rs | 2 ++ 1 file changed, 2 insertions(+) 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 3ede2988f143..1fe9e9bd24db 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 @@ -32,6 +32,8 @@ pub struct InstrumentationVisitor<'a, 'tcx> { tcx: TyCtxt<'tcx>, } +/// This enum differentiates between different reasons to visit a place, yielding different +/// instrumentation injected. enum PlaceOperation { Read, Write, From 38e588d250a63660906be56336a3c5b9087c3d0c Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Sun, 18 Aug 2024 11:16:59 -0700 Subject: [PATCH 06/12] Break down large visitor functions in instrumentation visitors --- .../delayed_ub/instrumentation_visitor.rs | 17 +- .../check_uninit/ptr_uninit/uninit_visitor.rs | 469 ++++++++++-------- 2 files changed, 259 insertions(+), 227 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs index 1fe9e9bd24db..994a571b677b 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 @@ -154,13 +154,7 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> { self.check_operand(cond); } TerminatorKind::Drop { place, .. } => { - // According to the documentation, "After drop elaboration: Drop terminators are a - // complete nop for types that have no drop glue. For other types, Drop terminators - // behave exactly like a call to core::mem::drop_in_place with a pointer to the - // given place." Since we check arguments when instrumenting function calls, perhaps - // we need to check that one, too. For more info, see: - // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.TerminatorKind.html#variant.Drop - self.check_place(place, PlaceOperation::Read); + self.check_place(place, PlaceOperation::Deinit); } TerminatorKind::Call { func, args, destination, target: _, unwind: _ } => { self.check_operand(func); @@ -221,7 +215,8 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> { } Operand::Constant(_) => { // Those should be safe to skip, as they are either constants or statics. In the - // latter case, we handle them in regular uninit visior + // latter case, we handle them in regular uninit visitor, as accessing statics + // requires dereferencing a raw pointer. } } } @@ -237,7 +232,7 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> { { match place_operation { PlaceOperation::Write => { - // If we are mutating the place, initialize it. + // Write to the place initializes it. self.push_target(MemoryInitOp::SetRef { operand: Operand::Copy(place.clone()), value: true, @@ -245,7 +240,7 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> { }) } PlaceOperation::Deinit => { - // If we are mutating the place, initialize it. + // Explicitly deinitialie the place. self.push_target(MemoryInitOp::SetRef { operand: Operand::Copy(place.clone()), value: false, @@ -253,7 +248,7 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> { }) } PlaceOperation::Read => { - // Otherwise, check its initialization. + // When reading from a place, check its initialization. self.push_target(MemoryInitOp::CheckRef { operand: Operand::Copy(place.clone()), }); 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 d6d125aeeb79..456c93ecd9d8 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 @@ -22,7 +22,7 @@ use stable_mir::{ NonDivergingIntrinsic, Operand, Place, PointerCoercion, ProjectionElem, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, }, - ty::{ConstantKind, RigidTy, TyKind}, + ty::{ConstantKind, RigidTy, Ty, TyKind}, }; pub struct CheckUninitVisitor { @@ -90,43 +90,16 @@ impl CheckUninitVisitor { StatementKind::Assign(place, rvalue) => { // First check rvalue. self.check_rvalue(rvalue); - // Check whether we are assigning into a dereference (*ptr = _). - if let Some(place_without_deref) = try_remove_topmost_deref(place) { - // First, check that we are not dereferencing extra pointers along the way - // (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, - }); - } - } - // 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, - }); - } + self.check_dereference_assign(place); + // Check whether Rvalue creates a new initialized pointer previously not captured + // inside shadow memory. + if let Rvalue::AddressOf(_, _) = rvalue { + assert!(place.ty(&self.locals).unwrap().kind().is_raw_ptr()); + self.push_target(MemoryInitOp::Set { + operand: Operand::Copy(place.clone()), + value: true, + position: InsertPosition::After, + }); } } StatementKind::Deinit(place) => { @@ -155,6 +128,38 @@ impl CheckUninitVisitor { } } + /// Check whether we are assigning into a dereference (*ptr = _). + fn check_dereference_assign(&mut self, place: &Place) { + 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 the place is a raw pointer, initialize it. + 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, + }); + } + } + } + /// Check the terminator and find all potential instrumentation targets. fn check_terminator(&mut self, term: &Terminator) { // Leave it as an exhaustive match to be notified when a new kind is added. @@ -174,148 +179,17 @@ impl CheckUninitVisitor { }; 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:?}`."), - }); - } - } + self.check_intrinsic(instance, args); } 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, - }); - } - _ => {} - } - } + self.check_alloc_operations(instance, args, destination); } _ => {} } } TerminatorKind::Drop { place, .. } => { self.check_place(place); - - let place_ty = place.ty(&self.locals).unwrap(); - // When drop is codegen'ed for types that could define their own dropping - // behavior, a reference is taken to the place which is later implicitly coerced - // to a pointer. Hence, we need to bless this pointer as initialized. - match place - .ty(&self.locals) - .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, - }); - } - _ => {} - } - - if place_ty.kind().is_raw_ptr() { - self.push_target(MemoryInitOp::Set { - operand: Operand::Copy(place.clone()), - value: false, - position: InsertPosition::After, - }); - } + self.check_drop(place); } TerminatorKind::Goto { .. } | TerminatorKind::Resume @@ -342,6 +216,155 @@ impl CheckUninitVisitor { } } + /// Check the drop operation to bless dropped types before drop happens and deinitialize them + /// after. + fn check_drop(&mut self, place: &Place) { + // 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. + let place_ty = place.ty(&self.locals).unwrap(); + 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, + }); + } + _ => {} + } + // Deinitialize the place after it is dropped. + if place_ty.kind().is_raw_ptr() { + self.push_target(MemoryInitOp::Set { + operand: Operand::Copy(place.clone()), + value: false, + position: InsertPosition::After, + }); + } + } + + /// Check operations that interact with memory allocator. + fn check_alloc_operations( + &mut self, + instance: Instance, + args: &[Operand], + destination: &Place, + ) { + 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, + }); + } + _ => {} + } + } + } + + /// Check intrinsics that behave equivalently to dereferencing raw pointers or copying memory + /// initialization state. + fn check_intrinsic(&mut self, instance: Instance, args: &[Operand]) { + 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:?}`."), + }); + } + } + } + /// Check the rvalue and find all potential instrumentation targets. fn check_rvalue(&mut self, rvalue: &Rvalue) { match rvalue { @@ -369,56 +392,70 @@ impl CheckUninitVisitor { } Rvalue::NullaryOp(_, _) | Rvalue::ThreadLocalRef(_) => {} Rvalue::Cast(cast_kind, op, ty) => { - self.check_operand(op); - match cast_kind { - // We currently do not support soundly reasoning about trait objects, so need to - // notify the user. - CastKind::PointerCoercion(PointerCoercion::Unsize) => { - if let TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) = ty.kind() { - if pointee_ty.kind().is_trait() { - self.push_target(MemoryInitOp::Unsupported { - reason: "Kani does not support reasoning about memory initialization of unsized pointers.".to_string(), - }); - } - } - } - CastKind::Transmute => { - let operand_ty = op.ty(&self.locals).unwrap(); - if !tys_layout_compatible_to_size(&operand_ty, &ty) { - // If transmuting between two types of incompatible layouts, padding - // bytes are exposed, which is UB. - self.push_target(MemoryInitOp::TriviallyUnsafe { - reason: "Transmuting between types of incompatible layouts." - .to_string(), - }); - } else if let ( - TyKind::RigidTy(RigidTy::Ref(_, from_ty, _)), - TyKind::RigidTy(RigidTy::Ref(_, to_ty, _)), - ) = (operand_ty.kind(), ty.kind()) - { - if !tys_layout_compatible_to_size(&from_ty, &to_ty) { - // Since references are supposed to always be initialized for its type, - // transmuting between two references of incompatible layout is UB. - self.push_target(MemoryInitOp::TriviallyUnsafe { + self.check_cast(cast_kind, op, ty); + } + } + } + + /// Check the cast operation performed as a part of rvalue. This is mainly to catch invalid + /// transmute operations. + fn check_cast(&mut self, cast_kind: &CastKind, op: &Operand, ty: &Ty) { + self.check_operand(op); + match cast_kind { + CastKind::Transmute => { + let operand_ty = op.ty(&self.locals).unwrap(); + if !tys_layout_compatible_to_size(&operand_ty, &ty) { + // If transmuting between two types of incompatible layouts, padding + // bytes are exposed, which is UB. + self.push_target(MemoryInitOp::TriviallyUnsafe { + reason: "Transmuting between types of incompatible layouts.".to_string(), + }); + } else if let ( + TyKind::RigidTy(RigidTy::Ref(_, from_ty, _)), + TyKind::RigidTy(RigidTy::Ref(_, to_ty, _)), + ) = (operand_ty.kind(), ty.kind()) + { + if !tys_layout_compatible_to_size(&from_ty, &to_ty) { + // Since references are supposed to always be initialized for its type, + // transmuting between two references of incompatible layout is UB. + self.push_target(MemoryInitOp::TriviallyUnsafe { reason: "Transmuting between references pointing to types of incompatible layouts." .to_string(), }); - } - } else if let ( - TyKind::RigidTy(RigidTy::RawPtr(from_ty, _)), - TyKind::RigidTy(RigidTy::Ref(_, to_ty, _)), - ) = (operand_ty.kind(), ty.kind()) - { - // Assert that we can only cast this way if types are the same. - assert!(from_ty == to_ty); - // When transmuting from a raw pointer to a reference, need to check that - // the value pointed by the raw pointer is initialized. - self.push_target(MemoryInitOp::Check { operand: op.clone() }); - } } - _ => {} + } else if let ( + TyKind::RigidTy(RigidTy::RawPtr(from_ty, _)), + TyKind::RigidTy(RigidTy::Ref(_, to_ty, _)), + ) = (operand_ty.kind(), ty.kind()) + { + // Assert that we can only cast this way if types are the same. + assert!(from_ty == to_ty); + // When transmuting from a raw pointer to a reference, need to check that + // the value pointed by the raw pointer is initialized. + self.push_target(MemoryInitOp::Check { operand: op.clone() }); + } + } + // We currently do not support soundly reasoning about trait objects, so need to + // notify the user. + CastKind::PointerCoercion(PointerCoercion::Unsize) => { + if let TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) = ty.kind() { + if pointee_ty.kind().is_trait() { + self.push_target(MemoryInitOp::Unsupported { + reason: "Kani does not support reasoning about memory initialization of unsized pointers.".to_string(), + }); + } } } + CastKind::PointerExposeAddress + | CastKind::PointerWithExposedProvenance + | CastKind::DynStar + | CastKind::IntToInt + | CastKind::FloatToInt + | CastKind::FloatToFloat + | CastKind::IntToFloat + | CastKind::PtrToPtr + | CastKind::FnPtrToPtr + | CastKind::PointerCoercion(_) => {} } } From 244e239f592eb2fb0649a17a327ac668adace0e1 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 19 Aug 2024 10:44:18 -0700 Subject: [PATCH 07/12] Revert "Break down large visitor functions in instrumentation visitors" This reverts commit 38e588d250a63660906be56336a3c5b9087c3d0c. --- .../delayed_ub/instrumentation_visitor.rs | 17 +- .../check_uninit/ptr_uninit/uninit_visitor.rs | 469 ++++++++---------- 2 files changed, 227 insertions(+), 259 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs index 994a571b677b..1fe9e9bd24db 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 @@ -154,7 +154,13 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> { self.check_operand(cond); } TerminatorKind::Drop { place, .. } => { - self.check_place(place, PlaceOperation::Deinit); + // According to the documentation, "After drop elaboration: Drop terminators are a + // complete nop for types that have no drop glue. For other types, Drop terminators + // behave exactly like a call to core::mem::drop_in_place with a pointer to the + // given place." Since we check arguments when instrumenting function calls, perhaps + // we need to check that one, too. For more info, see: + // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.TerminatorKind.html#variant.Drop + self.check_place(place, PlaceOperation::Read); } TerminatorKind::Call { func, args, destination, target: _, unwind: _ } => { self.check_operand(func); @@ -215,8 +221,7 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> { } Operand::Constant(_) => { // Those should be safe to skip, as they are either constants or statics. In the - // latter case, we handle them in regular uninit visitor, as accessing statics - // requires dereferencing a raw pointer. + // latter case, we handle them in regular uninit visior } } } @@ -232,7 +237,7 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> { { match place_operation { PlaceOperation::Write => { - // Write to the place initializes it. + // If we are mutating the place, initialize it. self.push_target(MemoryInitOp::SetRef { operand: Operand::Copy(place.clone()), value: true, @@ -240,7 +245,7 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> { }) } PlaceOperation::Deinit => { - // Explicitly deinitialie the place. + // If we are mutating the place, initialize it. self.push_target(MemoryInitOp::SetRef { operand: Operand::Copy(place.clone()), value: false, @@ -248,7 +253,7 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> { }) } PlaceOperation::Read => { - // When reading from a place, check its initialization. + // Otherwise, check its initialization. self.push_target(MemoryInitOp::CheckRef { operand: Operand::Copy(place.clone()), }); 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 456c93ecd9d8..d6d125aeeb79 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs @@ -22,7 +22,7 @@ use stable_mir::{ NonDivergingIntrinsic, Operand, Place, PointerCoercion, ProjectionElem, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, }, - ty::{ConstantKind, RigidTy, Ty, TyKind}, + ty::{ConstantKind, RigidTy, TyKind}, }; pub struct CheckUninitVisitor { @@ -90,16 +90,43 @@ impl CheckUninitVisitor { StatementKind::Assign(place, rvalue) => { // First check rvalue. self.check_rvalue(rvalue); - self.check_dereference_assign(place); - // Check whether Rvalue creates a new initialized pointer previously not captured - // inside shadow memory. - if let Rvalue::AddressOf(_, _) = rvalue { - assert!(place.ty(&self.locals).unwrap().kind().is_raw_ptr()); - self.push_target(MemoryInitOp::Set { - operand: Operand::Copy(place.clone()), - value: true, - position: InsertPosition::After, - }); + // 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, + }); + } + } + // 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::Deinit(place) => { @@ -128,38 +155,6 @@ impl CheckUninitVisitor { } } - /// Check whether we are assigning into a dereference (*ptr = _). - fn check_dereference_assign(&mut self, place: &Place) { - 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 the place is a raw pointer, initialize it. - 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, - }); - } - } - } - /// Check the terminator and find all potential instrumentation targets. fn check_terminator(&mut self, term: &Terminator) { // Leave it as an exhaustive match to be notified when a new kind is added. @@ -179,17 +174,148 @@ impl CheckUninitVisitor { }; match instance.kind { InstanceKind::Intrinsic => { - self.check_intrinsic(instance, args); + 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:?}`."), + }); + } + } } InstanceKind::Item => { - self.check_alloc_operations(instance, args, destination); + 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.check_place(place); - self.check_drop(place); + + let place_ty = place.ty(&self.locals).unwrap(); + // When drop is codegen'ed for types that could define their own dropping + // behavior, a reference is taken to the place which is later implicitly coerced + // to a pointer. Hence, we need to bless this pointer as initialized. + match place + .ty(&self.locals) + .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, + }); + } + _ => {} + } + + 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::Resume @@ -216,155 +342,6 @@ impl CheckUninitVisitor { } } - /// Check the drop operation to bless dropped types before drop happens and deinitialize them - /// after. - fn check_drop(&mut self, place: &Place) { - // 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. - let place_ty = place.ty(&self.locals).unwrap(); - 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, - }); - } - _ => {} - } - // Deinitialize the place after it is dropped. - if place_ty.kind().is_raw_ptr() { - self.push_target(MemoryInitOp::Set { - operand: Operand::Copy(place.clone()), - value: false, - position: InsertPosition::After, - }); - } - } - - /// Check operations that interact with memory allocator. - fn check_alloc_operations( - &mut self, - instance: Instance, - args: &[Operand], - destination: &Place, - ) { - 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, - }); - } - _ => {} - } - } - } - - /// Check intrinsics that behave equivalently to dereferencing raw pointers or copying memory - /// initialization state. - fn check_intrinsic(&mut self, instance: Instance, args: &[Operand]) { - 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:?}`."), - }); - } - } - } - /// Check the rvalue and find all potential instrumentation targets. fn check_rvalue(&mut self, rvalue: &Rvalue) { match rvalue { @@ -392,70 +369,56 @@ impl CheckUninitVisitor { } Rvalue::NullaryOp(_, _) | Rvalue::ThreadLocalRef(_) => {} Rvalue::Cast(cast_kind, op, ty) => { - self.check_cast(cast_kind, op, ty); - } - } - } - - /// Check the cast operation performed as a part of rvalue. This is mainly to catch invalid - /// transmute operations. - fn check_cast(&mut self, cast_kind: &CastKind, op: &Operand, ty: &Ty) { - self.check_operand(op); - match cast_kind { - CastKind::Transmute => { - let operand_ty = op.ty(&self.locals).unwrap(); - if !tys_layout_compatible_to_size(&operand_ty, &ty) { - // If transmuting between two types of incompatible layouts, padding - // bytes are exposed, which is UB. - self.push_target(MemoryInitOp::TriviallyUnsafe { - reason: "Transmuting between types of incompatible layouts.".to_string(), - }); - } else if let ( - TyKind::RigidTy(RigidTy::Ref(_, from_ty, _)), - TyKind::RigidTy(RigidTy::Ref(_, to_ty, _)), - ) = (operand_ty.kind(), ty.kind()) - { - if !tys_layout_compatible_to_size(&from_ty, &to_ty) { - // Since references are supposed to always be initialized for its type, - // transmuting between two references of incompatible layout is UB. - self.push_target(MemoryInitOp::TriviallyUnsafe { - reason: "Transmuting between references pointing to types of incompatible layouts." - .to_string(), + self.check_operand(op); + match cast_kind { + // We currently do not support soundly reasoning about trait objects, so need to + // notify the user. + CastKind::PointerCoercion(PointerCoercion::Unsize) => { + if let TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) = ty.kind() { + if pointee_ty.kind().is_trait() { + self.push_target(MemoryInitOp::Unsupported { + reason: "Kani does not support reasoning about memory initialization of unsized pointers.".to_string(), }); + } + } } - } else if let ( - TyKind::RigidTy(RigidTy::RawPtr(from_ty, _)), - TyKind::RigidTy(RigidTy::Ref(_, to_ty, _)), - ) = (operand_ty.kind(), ty.kind()) - { - // Assert that we can only cast this way if types are the same. - assert!(from_ty == to_ty); - // When transmuting from a raw pointer to a reference, need to check that - // the value pointed by the raw pointer is initialized. - self.push_target(MemoryInitOp::Check { operand: op.clone() }); - } - } - // We currently do not support soundly reasoning about trait objects, so need to - // notify the user. - CastKind::PointerCoercion(PointerCoercion::Unsize) => { - if let TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) = ty.kind() { - if pointee_ty.kind().is_trait() { - self.push_target(MemoryInitOp::Unsupported { - reason: "Kani does not support reasoning about memory initialization of unsized pointers.".to_string(), + CastKind::Transmute => { + let operand_ty = op.ty(&self.locals).unwrap(); + if !tys_layout_compatible_to_size(&operand_ty, &ty) { + // If transmuting between two types of incompatible layouts, padding + // bytes are exposed, which is UB. + self.push_target(MemoryInitOp::TriviallyUnsafe { + reason: "Transmuting between types of incompatible layouts." + .to_string(), }); + } else if let ( + TyKind::RigidTy(RigidTy::Ref(_, from_ty, _)), + TyKind::RigidTy(RigidTy::Ref(_, to_ty, _)), + ) = (operand_ty.kind(), ty.kind()) + { + if !tys_layout_compatible_to_size(&from_ty, &to_ty) { + // Since references are supposed to always be initialized for its type, + // transmuting between two references of incompatible layout is UB. + self.push_target(MemoryInitOp::TriviallyUnsafe { + reason: "Transmuting between references pointing to types of incompatible layouts." + .to_string(), + }); + } + } else if let ( + TyKind::RigidTy(RigidTy::RawPtr(from_ty, _)), + TyKind::RigidTy(RigidTy::Ref(_, to_ty, _)), + ) = (operand_ty.kind(), ty.kind()) + { + // Assert that we can only cast this way if types are the same. + assert!(from_ty == to_ty); + // When transmuting from a raw pointer to a reference, need to check that + // the value pointed by the raw pointer is initialized. + self.push_target(MemoryInitOp::Check { operand: op.clone() }); + } } + _ => {} } } - CastKind::PointerExposeAddress - | CastKind::PointerWithExposedProvenance - | CastKind::DynStar - | CastKind::IntToInt - | CastKind::FloatToInt - | CastKind::FloatToFloat - | CastKind::IntToFloat - | CastKind::PtrToPtr - | CastKind::FnPtrToPtr - | CastKind::PointerCoercion(_) => {} } } From 72a6edf8a892e9f7e4b8640dd6a4aa24e8c05b11 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 19 Aug 2024 10:44:27 -0700 Subject: [PATCH 08/12] Revert "Add docstring for `PlaceOperation`" This reverts commit cc1798b1f2539cac0ab4ba3fec1b05df43496dd1. --- .../check_uninit/delayed_ub/instrumentation_visitor.rs | 2 -- 1 file changed, 2 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs index 1fe9e9bd24db..3ede2988f143 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs @@ -32,8 +32,6 @@ pub struct InstrumentationVisitor<'a, 'tcx> { tcx: TyCtxt<'tcx>, } -/// This enum differentiates between different reasons to visit a place, yielding different -/// instrumentation injected. enum PlaceOperation { Read, Write, From 6a70eae5665e75e4809600eaf3f827411acee1b2 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 19 Aug 2024 10:44:36 -0700 Subject: [PATCH 09/12] Revert "Stop using visitor for instrumentation target finding" This reverts commit eb05f74e62b56889da93ccf13131a8c715a14298. --- .../delayed_ub/instrumentation_visitor.rs | 201 ++--------- .../kani_middle/transform/check_uninit/mod.rs | 14 +- .../check_uninit/ptr_uninit/uninit_visitor.rs | 323 +++++++----------- 3 files changed, 165 insertions(+), 373 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs index 3ede2988f143..f6354b827c37 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs @@ -16,8 +16,9 @@ use crate::kani_middle::{ }; use rustc_middle::ty::TyCtxt; use stable_mir::mir::{ - mono::Instance, BasicBlock, CopyNonOverlapping, InlineAsmOperand, NonDivergingIntrinsic, - Operand, Place, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, + mono::Instance, + visit::{Location, PlaceContext}, + BasicBlock, MirVisitor, Operand, Place, Rvalue, }; use std::collections::HashSet; @@ -32,13 +33,6 @@ pub struct InstrumentationVisitor<'a, 'tcx> { tcx: TyCtxt<'tcx>, } -enum PlaceOperation { - Read, - Write, - Deinit, - Noop, -} - impl<'a, 'tcx> TargetFinder for InstrumentationVisitor<'a, 'tcx> { fn find_next( &mut self, @@ -50,11 +44,14 @@ impl<'a, 'tcx> TargetFinder for InstrumentationVisitor<'a, 'tcx> { SourceInstruction::Statement { idx, bb } => { let BasicBlock { statements, .. } = &body.blocks()[bb]; let stmt = &statements[idx]; - self.check_statement(stmt) + self.visit_statement(stmt, self.__location_hack_remove_before_merging(stmt.span)) } SourceInstruction::Terminator { bb } => { let BasicBlock { terminator, .. } = &body.blocks()[bb]; - self.check_terminator(terminator) + self.visit_terminator( + terminator, + self.__location_hack_remove_before_merging(terminator.span), + ) } } self.target.clone() @@ -79,152 +76,17 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> { } } -impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> { - fn check_statement(&mut self, stmt: &Statement) { - let Statement { kind, .. } = stmt; - match kind { - StatementKind::Assign(place, rvalue) => { - self.check_place(place, PlaceOperation::Write); - self.check_rvalue(rvalue); - } - StatementKind::FakeRead(_, place) => { - // According to the compiler docs, "When executed at runtime this is a nop." For - // more info, see - // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.StatementKind.html#variant.FakeRead, - self.check_place(place, PlaceOperation::Noop); - } - StatementKind::SetDiscriminant { place, .. } => { - self.check_place(place, PlaceOperation::Write); - } - StatementKind::Deinit(place) => { - self.check_place(place, PlaceOperation::Deinit); - } - StatementKind::Retag(_, place) => { - // According to the compiler docs, "These statements are currently only interpreted - // by miri and only generated when -Z mir-emit-retag is passed." For more info, see - // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.StatementKind.html#variant.Retag, - self.check_place(place, PlaceOperation::Noop); - } - StatementKind::PlaceMention(place) => { - // According to the compiler docs, "When executed at runtime, this computes the - // given place, but then discards it without doing a load." For more info, see - // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.StatementKind.html#variant.PlaceMention, - self.check_place(place, PlaceOperation::Noop); - } - StatementKind::AscribeUserType { place, .. } => { - // According to the compiler docs, "When executed at runtime this is a nop." For - // more info, see - // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.StatementKind.html#variant.AscribeUserType, - self.check_place(place, PlaceOperation::Noop); - } - - StatementKind::Intrinsic(intrisic) => match intrisic { - NonDivergingIntrinsic::Assume(operand) => { - self.check_operand(operand); - } - NonDivergingIntrinsic::CopyNonOverlapping(CopyNonOverlapping { - src, - dst, - count, - }) => { - self.check_operand(src); - self.check_operand(dst); - self.check_operand(count); - } - }, - StatementKind::StorageLive(_) - | StatementKind::StorageDead(_) - | StatementKind::Coverage(_) - | StatementKind::ConstEvalCounter - | StatementKind::Nop => {} - } - } - - fn check_terminator(&mut self, term: &Terminator) { - let Terminator { kind, .. } = term; - match kind { - TerminatorKind::Goto { .. } - | TerminatorKind::Resume - | TerminatorKind::Abort - | TerminatorKind::Unreachable - | TerminatorKind::Return => {} - TerminatorKind::Assert { cond, .. } => { - self.check_operand(cond); - } - TerminatorKind::Drop { place, .. } => { - // According to the documentation, "After drop elaboration: Drop terminators are a - // complete nop for types that have no drop glue. For other types, Drop terminators - // behave exactly like a call to core::mem::drop_in_place with a pointer to the - // given place." Since we check arguments when instrumenting function calls, perhaps - // we need to check that one, too. For more info, see: - // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.TerminatorKind.html#variant.Drop - self.check_place(place, PlaceOperation::Read); - } - TerminatorKind::Call { func, args, destination, target: _, unwind: _ } => { - self.check_operand(func); - for arg in args { - self.check_operand(arg); - } - self.check_place(destination, PlaceOperation::Write); - } - TerminatorKind::InlineAsm { operands, .. } => { - for op in operands { - let InlineAsmOperand { in_value, out_place, raw_rpr: _ } = op; - if let Some(input) = in_value { - self.check_operand(input); - } - if let Some(output) = out_place { - self.check_place(output, PlaceOperation::Write); - } - } - } - TerminatorKind::SwitchInt { discr, .. } => { - self.check_operand(discr); - } - } - } - - fn check_rvalue(&mut self, rvalue: &Rvalue) { +impl<'a, 'tcx> MirVisitor for InstrumentationVisitor<'a, 'tcx> { + fn visit_rvalue(&mut self, rvalue: &Rvalue, location: Location) { match rvalue { - Rvalue::AddressOf(_, place) | Rvalue::Ref(_, _, place) => { - self.check_place(place, PlaceOperation::Noop); - } - Rvalue::Aggregate(_, operands) => { - for op in operands { - self.check_operand(op); - } - } - Rvalue::BinaryOp(_, lhs, rhs) | Rvalue::CheckedBinaryOp(_, lhs, rhs) => { - self.check_operand(lhs); - self.check_operand(rhs); - } - Rvalue::Cast(_, op, _) - | Rvalue::Repeat(op, _) - | Rvalue::ShallowInitBox(op, ..) - | Rvalue::UnaryOp(_, op) - | Rvalue::Use(op) => { - self.check_operand(op); - } - Rvalue::CopyForDeref(place) | Rvalue::Discriminant(place) | Rvalue::Len(place) => { - self.check_place(place, PlaceOperation::Read); - } - Rvalue::ThreadLocalRef(..) | Rvalue::NullaryOp(..) => {} - } - } - - fn check_operand(&mut self, operand: &Operand) { - match operand { - Operand::Copy(place) | Operand::Move(place) => { - self.check_place(place, PlaceOperation::Read) - } - Operand::Constant(_) => { - // Those should be safe to skip, as they are either constants or statics. In the - // latter case, we handle them in regular uninit visior + Rvalue::AddressOf(..) | Rvalue::Ref(..) => { + // These operations are always legitimate for us. } + _ => self.super_rvalue(rvalue, location), } } - fn check_place(&mut self, place: &Place, place_operation: PlaceOperation) { + fn visit_place(&mut self, place: &Place, ptx: PlaceContext, location: Location) { // Match the place by whatever it is pointing to and find an intersection with the targets. if self .points_to @@ -233,31 +95,18 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> { .next() .is_some() { - match place_operation { - PlaceOperation::Write => { - // If we are mutating the place, initialize it. - self.push_target(MemoryInitOp::SetRef { - operand: Operand::Copy(place.clone()), - value: true, - position: InsertPosition::After, - }) - } - PlaceOperation::Deinit => { - // If we are mutating the place, initialize it. - self.push_target(MemoryInitOp::SetRef { - operand: Operand::Copy(place.clone()), - value: false, - position: InsertPosition::After, - }) - } - PlaceOperation::Read => { - // Otherwise, check its initialization. - self.push_target(MemoryInitOp::CheckRef { - operand: Operand::Copy(place.clone()), - }); - } - PlaceOperation::Noop => {} + // If we are mutating the place, initialize it. + if ptx.is_mutating() { + self.push_target(MemoryInitOp::SetRef { + operand: Operand::Copy(place.clone()), + value: true, + position: InsertPosition::After, + }); + } else { + // Otherwise, check its initialization. + self.push_target(MemoryInitOp::CheckRef { operand: Operand::Copy(place.clone()) }); } } + self.super_place(place, ptx, location) } } diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs index 50b640cfcb54..95e15a21fba0 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -13,10 +13,12 @@ use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use stable_mir::{ mir::{ - mono::Instance, AggregateKind, BasicBlock, Body, ConstOperand, Mutability, Operand, Place, - Rvalue, Statement, StatementKind, Terminator, TerminatorKind, UnwindAction, + mono::Instance, visit::Location, AggregateKind, BasicBlock, Body, ConstOperand, Mutability, + Operand, Place, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, UnwindAction, + }, + ty::{ + FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Span, Ty, TyConst, TyKind, UintTy, }, - ty::{FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Ty, TyConst, TyKind, UintTy}, CrateDef, }; use std::collections::HashMap; @@ -37,6 +39,12 @@ pub trait TargetFinder { body: &MutableBody, source: &SourceInstruction, ) -> Option; + + /// TODO: This is just a temporary fix to unblock me because I couldn't create Location + /// directly. Perhaps we need to make a change in StableMIR to allow creating Location. + fn __location_hack_remove_before_merging(&self, span: Span) -> Location { + unsafe { std::mem::transmute(span) } + } } // Function bodies of those functions will not be instrumented as not to cause infinite recursion. diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs index d6d125aeeb79..9f6b2a881e71 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs @@ -18,9 +18,10 @@ use stable_mir::{ mir::{ alloc::GlobalAlloc, mono::{Instance, InstanceKind}, - BasicBlock, CastKind, CopyNonOverlapping, InlineAsmOperand, LocalDecl, - NonDivergingIntrinsic, Operand, Place, PointerCoercion, ProjectionElem, Rvalue, Statement, - StatementKind, Terminator, TerminatorKind, + visit::{Location, PlaceContext}, + BasicBlock, CastKind, LocalDecl, MirVisitor, NonDivergingIntrinsic, Operand, Place, + PointerCoercion, ProjectionElem, Rvalue, Statement, StatementKind, Terminator, + TerminatorKind, }, ty::{ConstantKind, RigidTy, TyKind}, }; @@ -43,11 +44,14 @@ impl TargetFinder for CheckUninitVisitor { SourceInstruction::Statement { idx, bb } => { let BasicBlock { statements, .. } = &body.blocks()[bb]; let stmt = &statements[idx]; - self.check_statement(stmt) + self.visit_statement(stmt, self.__location_hack_remove_before_merging(stmt.span)) } SourceInstruction::Terminator { bb } => { let BasicBlock { terminator, .. } = &body.blocks()[bb]; - self.check_terminator(terminator) + self.visit_terminator( + terminator, + self.__location_hack_remove_before_merging(terminator.span), + ) } } self.target.clone() @@ -68,28 +72,23 @@ impl CheckUninitVisitor { } } -impl CheckUninitVisitor { - /// Check the statement and find all potential instrumentation targets. - fn check_statement(&mut self, stmt: &Statement) { +impl MirVisitor for CheckUninitVisitor { + fn visit_statement(&mut self, stmt: &Statement, location: Location) { // Leave it as an exhaustive match to be notified when a new kind is added. match &stmt.kind { - StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping( - CopyNonOverlapping { src, dst, count }, - )) => { - self.check_operand(src); - self.check_operand(dst); - self.check_operand(count); + 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: src.clone(), - to: dst.clone(), - count: count.clone(), + from: copy.src.clone(), + to: copy.dst.clone(), + count: copy.count.clone(), }); } StatementKind::Assign(place, rvalue) => { // First check rvalue. - self.check_rvalue(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 @@ -100,8 +99,8 @@ impl CheckUninitVisitor { // If the projection is Deref and the current type is raw pointer, check // if it points to initialized memory. if *projection_elem == ProjectionElem::Deref { - if let TyKind::RigidTy(RigidTy::RawPtr(_, _)) = - place_to_add_projections.ty(&self.locals).unwrap().kind() + if let TyKind::RigidTy(RigidTy::RawPtr(..)) = + place_to_add_projections.ty(&&self.locals).unwrap().kind() { self.push_target(MemoryInitOp::Check { operand: Operand::Copy(place_to_add_projections.clone()), @@ -110,7 +109,7 @@ impl CheckUninitVisitor { } place_to_add_projections.projection.push(projection_elem.clone()); } - if place_without_deref.ty(&self.locals).unwrap().kind().is_raw_ptr() { + if place_without_deref.ty(&&self.locals).unwrap().kind().is_raw_ptr() { self.push_target(MemoryInitOp::Set { operand: Operand::Copy(place_without_deref), value: true, @@ -119,8 +118,8 @@ impl CheckUninitVisitor { } } // Check whether Rvalue creates a new initialized pointer previously not captured inside shadow memory. - if place.ty(&self.locals).unwrap().kind().is_raw_ptr() { - if let Rvalue::AddressOf(_, _) = rvalue { + if place.ty(&&self.locals).unwrap().kind().is_raw_ptr() { + if let Rvalue::AddressOf(..) = rvalue { self.push_target(MemoryInitOp::Set { operand: Operand::Copy(place.clone()), value: true, @@ -130,44 +129,36 @@ impl CheckUninitVisitor { } } StatementKind::Deinit(place) => { - self.check_place(place); + self.super_statement(stmt, location); self.push_target(MemoryInitOp::Set { operand: Operand::Copy(place.clone()), value: false, position: InsertPosition::After, }); } - StatementKind::FakeRead(_, place) - | StatementKind::SetDiscriminant { place, .. } - | StatementKind::Retag(_, place) - | StatementKind::PlaceMention(place) - | StatementKind::AscribeUserType { place, .. } => { - self.check_place(place); - } - StatementKind::Intrinsic(NonDivergingIntrinsic::Assume(operand)) => { - self.check_operand(operand); - } - StatementKind::StorageLive(_) + StatementKind::FakeRead(_, _) + | StatementKind::SetDiscriminant { .. } + | StatementKind::StorageLive(_) | StatementKind::StorageDead(_) + | StatementKind::Retag(_, _) + | StatementKind::PlaceMention(_) + | StatementKind::AscribeUserType { .. } | StatementKind::Coverage(_) | StatementKind::ConstEvalCounter - | StatementKind::Nop => {} + | StatementKind::Intrinsic(NonDivergingIntrinsic::Assume(_)) + | StatementKind::Nop => self.super_statement(stmt, location), } } - /// Check the terminator and find all potential instrumentation targets. - fn check_terminator(&mut self, term: &Terminator) { + fn visit_terminator(&mut self, term: &Terminator, location: Location) { // Leave it as an exhaustive match to be notified when a new kind is added. match &term.kind { TerminatorKind::Call { func, args, destination, .. } => { - self.check_operand(func); - for arg in args { - self.check_operand(arg); - } - self.check_place(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; } @@ -286,20 +277,20 @@ impl CheckUninitVisitor { } } TerminatorKind::Drop { place, .. } => { - self.check_place(place); + self.super_terminator(term, location); + let place_ty = place.ty(&&self.locals).unwrap(); - let place_ty = place.ty(&self.locals).unwrap(); // When drop is codegen'ed for types that could define their own dropping // behavior, a reference is taken to the place which is later implicitly coerced // to a pointer. Hence, we need to bless this pointer as initialized. match place - .ty(&self.locals) + .ty(&&self.locals) .unwrap() .kind() .rigid() .expect("should be working with monomorphized code") { - RigidTy::Adt(_, _) | RigidTy::Dynamic(_, _, _) => { + RigidTy::Adt(..) | RigidTy::Dynamic(_, _, _) => { self.push_target(MemoryInitOp::SetRef { operand: Operand::Copy(place.clone()), value: true, @@ -318,177 +309,121 @@ impl CheckUninitVisitor { } } TerminatorKind::Goto { .. } + | TerminatorKind::SwitchInt { .. } | TerminatorKind::Resume | TerminatorKind::Abort | TerminatorKind::Return - | TerminatorKind::Unreachable => {} - TerminatorKind::SwitchInt { discr, .. } => { - self.check_operand(discr); - } - TerminatorKind::Assert { cond, .. } => { - self.check_operand(cond); - } - TerminatorKind::InlineAsm { operands, .. } => { - for op in operands { - let InlineAsmOperand { in_value, out_place, raw_rpr: _ } = op; - if let Some(input) = in_value { - self.check_operand(input); + | TerminatorKind::Unreachable + | TerminatorKind::Assert { .. } + | TerminatorKind::InlineAsm { .. } => self.super_terminator(term, location), + } + } + + fn visit_place(&mut self, place: &Place, ptx: PlaceContext, location: Location) { + for (idx, elem) in place.projection.iter().enumerate() { + let intermediate_place = + Place { local: place.local, projection: place.projection[..idx].to_vec() }; + match elem { + ProjectionElem::Deref => { + let ptr_ty = intermediate_place.ty(&self.locals).unwrap(); + if ptr_ty.kind().is_raw_ptr() { + self.push_target(MemoryInitOp::Check { + operand: Operand::Copy(intermediate_place.clone()), + }); } - if let Some(output) = out_place { - self.check_place(output); + } + ProjectionElem::Field(idx, target_ty) => { + if target_ty.kind().is_union() + && (!ptx.is_mutating() || place.projection.len() > idx + 1) + { + self.push_target(MemoryInitOp::Unsupported { + reason: "Kani does not support reasoning about memory initialization of unions.".to_string(), + }); } } + ProjectionElem::Index(_) + | ProjectionElem::ConstantIndex { .. } + | ProjectionElem::Subslice { .. } => { + /* For a slice to be indexed, it should be valid first. */ + } + ProjectionElem::Downcast(_) => {} + ProjectionElem::OpaqueCast(_) => {} + ProjectionElem::Subtype(_) => {} } } + self.super_place(place, ptx, location) } - /// Check the rvalue and find all potential instrumentation targets. - fn check_rvalue(&mut self, rvalue: &Rvalue) { - match rvalue { - Rvalue::Aggregate(_, operands) => { - for op in operands { - self.check_operand(op); + fn visit_operand(&mut self, operand: &Operand, location: Location) { + if let Operand::Constant(constant) = operand { + if let ConstantKind::Allocated(allocation) = constant.const_.kind() { + for (_, prov) in &allocation.provenance.ptrs { + if let GlobalAlloc::Static(_) = GlobalAlloc::from(prov.0) { + if constant.ty().kind().is_raw_ptr() { + // If a static is a raw pointer, need to mark it as initialized. + self.push_target(MemoryInitOp::Set { + operand: Operand::Constant(constant.clone()), + value: true, + position: InsertPosition::Before, + }); + } + }; } } - Rvalue::BinaryOp(_, lhs, rhs) | Rvalue::CheckedBinaryOp(_, lhs, rhs) => { - self.check_operand(lhs); - self.check_operand(rhs); - } - Rvalue::AddressOf(_, place) - | Rvalue::CopyForDeref(place) - | Rvalue::Discriminant(place) - | Rvalue::Len(place) - | Rvalue::Ref(_, _, place) => { - self.check_place(place); - } - Rvalue::ShallowInitBox(op, _) - | Rvalue::UnaryOp(_, op) - | Rvalue::Use(op) - | Rvalue::Repeat(op, _) => { - self.check_operand(op); - } - Rvalue::NullaryOp(_, _) | Rvalue::ThreadLocalRef(_) => {} - Rvalue::Cast(cast_kind, op, ty) => { - self.check_operand(op); - match cast_kind { - // We currently do not support soundly reasoning about trait objects, so need to - // notify the user. - CastKind::PointerCoercion(PointerCoercion::Unsize) => { - if let TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) = ty.kind() { - if pointee_ty.kind().is_trait() { - self.push_target(MemoryInitOp::Unsupported { + } + self.super_operand(operand, location); + } + + fn visit_rvalue(&mut self, rvalue: &Rvalue, location: Location) { + if let Rvalue::Cast(cast_kind, operand, ty) = rvalue { + match cast_kind { + CastKind::PointerCoercion(PointerCoercion::Unsize) => { + if let TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) = ty.kind() { + if pointee_ty.kind().is_trait() { + self.push_target(MemoryInitOp::Unsupported { reason: "Kani does not support reasoning about memory initialization of unsized pointers.".to_string(), }); - } } } - CastKind::Transmute => { - let operand_ty = op.ty(&self.locals).unwrap(); - if !tys_layout_compatible_to_size(&operand_ty, &ty) { - // If transmuting between two types of incompatible layouts, padding - // bytes are exposed, which is UB. + } + CastKind::Transmute => { + let operand_ty = operand.ty(&self.locals).unwrap(); + if !tys_layout_compatible_to_size(&operand_ty, &ty) { + // If transmuting between two types of incompatible layouts, padding + // bytes are exposed, which is UB. + self.push_target(MemoryInitOp::TriviallyUnsafe { + reason: "Transmuting between types of incompatible layouts." + .to_string(), + }); + } else if let ( + TyKind::RigidTy(RigidTy::Ref(_, from_ty, _)), + TyKind::RigidTy(RigidTy::Ref(_, to_ty, _)), + ) = (operand_ty.kind(), ty.kind()) + { + if !tys_layout_compatible_to_size(&from_ty, &to_ty) { + // Since references are supposed to always be initialized for its type, + // transmuting between two references of incompatible layout is UB. self.push_target(MemoryInitOp::TriviallyUnsafe { - reason: "Transmuting between types of incompatible layouts." - .to_string(), - }); - } else if let ( - TyKind::RigidTy(RigidTy::Ref(_, from_ty, _)), - TyKind::RigidTy(RigidTy::Ref(_, to_ty, _)), - ) = (operand_ty.kind(), ty.kind()) - { - if !tys_layout_compatible_to_size(&from_ty, &to_ty) { - // Since references are supposed to always be initialized for its type, - // transmuting between two references of incompatible layout is UB. - self.push_target(MemoryInitOp::TriviallyUnsafe { reason: "Transmuting between references pointing to types of incompatible layouts." .to_string(), }); - } - } else if let ( - TyKind::RigidTy(RigidTy::RawPtr(from_ty, _)), - TyKind::RigidTy(RigidTy::Ref(_, to_ty, _)), - ) = (operand_ty.kind(), ty.kind()) - { - // Assert that we can only cast this way if types are the same. - assert!(from_ty == to_ty); - // When transmuting from a raw pointer to a reference, need to check that - // the value pointed by the raw pointer is initialized. - self.push_target(MemoryInitOp::Check { operand: op.clone() }); } + } else if let ( + TyKind::RigidTy(RigidTy::RawPtr(from_ty, _)), + TyKind::RigidTy(RigidTy::Ref(_, to_ty, _)), + ) = (operand_ty.kind(), ty.kind()) + { + // Assert that we can only cast this way if types are the same. + assert!(from_ty == to_ty); + // When transmuting from a raw pointer to a reference, need to check that + // the value pointed by the raw pointer is initialized. + self.push_target(MemoryInitOp::Check { operand: operand.clone() }); } - _ => {} - } - } - } - } - - /// Check if one of the place projections involves dereferencing a raw pointer, which is an - /// instrumentation target , or union access, which is currently not supported. - fn check_place(&mut self, place: &Place) { - for (idx, elem) in place.projection.iter().enumerate() { - let intermediate_place = - Place { local: place.local, projection: place.projection[..idx].to_vec() }; - self.check_projection_elem(elem, intermediate_place) - } - } - - /// Check if the projection involves dereferencing a raw pointer, which is an instrumentation - /// target, or union access, which is currently not supported. - fn check_projection_elem( - &mut self, - projection_elem: &ProjectionElem, - intermediate_place: Place, - ) { - match projection_elem { - ProjectionElem::Deref => { - let ptr_ty = intermediate_place.ty(&self.locals).unwrap(); - if ptr_ty.kind().is_raw_ptr() { - self.push_target(MemoryInitOp::Check { - operand: Operand::Copy(intermediate_place.clone()), - }); } + _ => {} } - ProjectionElem::Field(_, _) => { - if intermediate_place.ty(&self.locals).unwrap().kind().is_union() { - self.push_target(MemoryInitOp::Unsupported { - reason: - "Kani does not support reasoning about memory initialization of unions." - .to_string(), - }); - } - } - ProjectionElem::Index(_) - | ProjectionElem::ConstantIndex { .. } - | ProjectionElem::Subslice { .. } => { - /* For a slice to be indexed, it should be valid first. */ - } - ProjectionElem::Downcast(_) => {} - ProjectionElem::OpaqueCast(_) => {} - ProjectionElem::Subtype(_) => {} - } - } - - /// Check if the operand is a static to initialize it or else check its associated place. - fn check_operand(&mut self, operand: &Operand) { - match operand { - Operand::Copy(place) | Operand::Move(place) => self.check_place(place), - Operand::Constant(constant) => { - if let ConstantKind::Allocated(allocation) = constant.const_.kind() { - for (_, prov) in &allocation.provenance.ptrs { - if let GlobalAlloc::Static(_) = GlobalAlloc::from(prov.0) { - if constant.ty().kind().is_raw_ptr() { - // If a static is a raw pointer, need to mark it as initialized. - self.push_target(MemoryInitOp::Set { - operand: Operand::Constant(constant.clone()), - value: true, - position: InsertPosition::Before, - }); - } - }; - } - } - } - } + }; + self.super_rvalue(rvalue, location); } } From 58b689a7cd817e9eeb9402f22abb9016911bdc8c Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 19 Aug 2024 12:02:28 -0700 Subject: [PATCH 10/12] Implement collection of all instrumentation targets before instrumentation itself --- .../src/kani_middle/transform/body.rs | 2 +- .../delayed_ub/instrumentation_visitor.rs | 86 ++++++++++++------- .../kani_middle/transform/check_uninit/mod.rs | 49 ++--------- .../check_uninit/ptr_uninit/uninit_visitor.rs | 77 ++++++++++------- .../check_uninit/relevant_instruction.rs | 2 + 5 files changed, 113 insertions(+), 103 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 59210bb3e3b2..24fe5d8b2b2e 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -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 f6354b827c37..b26de868c4d1 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,13 +18,17 @@ use rustc_middle::ty::TyCtxt; use stable_mir::mir::{ mono::Instance, visit::{Location, PlaceContext}, - BasicBlock, MirVisitor, Operand, Place, Rvalue, + MirVisitor, Operand, Place, Rvalue, Statement, Terminator, }; use std::collections::HashSet; pub struct InstrumentationVisitor<'a, 'tcx> { - /// The target instruction that should be verified. - pub target: Option, + /// All target instructions in the body. + targets: Vec, + /// Currently analyzed instruction. + current_instruction: SourceInstruction, + /// 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 @@ -34,27 +38,14 @@ pub struct InstrumentationVisitor<'a, 'tcx> { } impl<'a, 'tcx> TargetFinder for InstrumentationVisitor<'a, 'tcx> { - fn find_next( - &mut self, - body: &MutableBody, - source: &SourceInstruction, - ) -> Option { - self.target = None; - match *source { - SourceInstruction::Statement { idx, bb } => { - let BasicBlock { statements, .. } = &body.blocks()[bb]; - let stmt = &statements[idx]; - self.visit_statement(stmt, self.__location_hack_remove_before_merging(stmt.span)) - } - SourceInstruction::Terminator { bb } => { - let BasicBlock { terminator, .. } = &body.blocks()[bb]; - self.visit_terminator( - terminator, - self.__location_hack_remove_before_merging(terminator.span), - ) - } + fn find_all(&mut self, body: &MutableBody) -> Vec { + for (bb_idx, bb) in body.blocks().iter().enumerate() { + self.current_instruction = SourceInstruction::Statement { idx: 0, bb: bb_idx }; + self.visit_basic_block(bb); } - self.target.clone() + // Push the last current target into the list. + self.targets.push(self.current_target.clone()); + self.targets.clone() } } @@ -65,18 +56,55 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> { current_instance: Instance, tcx: TyCtxt<'tcx>, ) -> Self { - Self { target: None, points_to, analysis_targets, current_instance, tcx } + Self { + targets: vec![], + current_instruction: SourceInstruction::Statement { idx: 0, bb: 0 }, + 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 { - after_instruction: vec![], - before_instruction: vec![], - }); - target.push_operation(source_op); + // If we switched to the next instruction, push the old one onto the list of targets. + if self.current_target.source != self.current_instruction { + self.targets.push(self.current_target.clone()); + self.current_target = InitRelevantInstruction { + source: self.current_instruction, + after_instruction: vec![], + before_instruction: vec![], + }; + } + self.current_target.push_operation(source_op); } } impl<'a, 'tcx> MirVisitor for InstrumentationVisitor<'a, 'tcx> { + fn visit_statement(&mut self, stmt: &Statement, location: Location) { + self.super_statement(stmt, location); + // Switch to the next statement. + if let SourceInstruction::Statement { idx, bb } = self.current_instruction { + self.current_instruction = SourceInstruction::Statement { idx: idx + 1, bb } + } else { + unreachable!() + } + } + + fn visit_terminator(&mut self, term: &Terminator, location: Location) { + if let SourceInstruction::Statement { bb, .. } = self.current_instruction { + self.current_instruction = SourceInstruction::Terminator { bb }; + } else { + unreachable!() + } + self.super_terminator(term, location); + } + fn visit_rvalue(&mut self, rvalue: &Rvalue, location: Location) { match rvalue { Rvalue::AddressOf(..) | Rvalue::Ref(..) => { diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs index 95e15a21fba0..364bc7cc12a7 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -13,12 +13,10 @@ use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use stable_mir::{ mir::{ - mono::Instance, visit::Location, AggregateKind, BasicBlock, Body, ConstOperand, Mutability, - Operand, Place, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, UnwindAction, - }, - ty::{ - FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Span, Ty, TyConst, TyKind, UintTy, + mono::Instance, AggregateKind, BasicBlock, Body, ConstOperand, Mutability, Operand, Place, + Rvalue, Statement, StatementKind, Terminator, TerminatorKind, UnwindAction, }, + ty::{FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Ty, TyConst, TyKind, UintTy}, CrateDef, }; use std::collections::HashMap; @@ -34,17 +32,7 @@ mod ty_layout; /// Trait that the instrumentation target providers must implement to work with the instrumenter. pub trait TargetFinder { - fn find_next( - &mut self, - body: &MutableBody, - source: &SourceInstruction, - ) -> Option; - - /// TODO: This is just a temporary fix to unblock me because I couldn't create Location - /// directly. Perhaps we need to make a change in StableMIR to allow creating Location. - fn __location_hack_remove_before_merging(&self, span: Span) -> Location { - unsafe { std::mem::transmute(span) } - } + fn find_all(&mut self, body: &MutableBody) -> Vec; } // Function bodies of those functions will not be instrumented as not to cause infinite recursion. @@ -105,32 +93,9 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { } let orig_len = body.blocks().len(); - let mut source = SourceInstruction::Terminator { bb: body.blocks().len() - 1 }; - loop { - if let Some(candidate) = target_finder.find_next(&body, &source) { - self.build_check_for_instruction(&mut body, candidate, source); - } - source = match source { - SourceInstruction::Statement { idx, bb } => { - if bb == 0 && idx == 0 { - break; - } else if idx == 0 { - SourceInstruction::Terminator { bb: bb - 1 } - } else { - SourceInstruction::Statement { idx: idx - 1, bb } - } - } - SourceInstruction::Terminator { bb } => { - let stmt_len = body.blocks()[bb].statements.len(); - if bb == 0 && stmt_len == 0 { - break; - } else if stmt_len == 0 { - SourceInstruction::Terminator { bb: bb - 1 } - } else { - SourceInstruction::Statement { idx: stmt_len - 1, bb } - } - } - } + 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) } diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs index 9f6b2a881e71..96c97c3468e9 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,56 +19,60 @@ use stable_mir::{ alloc::GlobalAlloc, mono::{Instance, InstanceKind}, visit::{Location, PlaceContext}, - BasicBlock, 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, - /// The target instruction that should be verified. - pub target: Option, + /// All target instructions in the body. + targets: Vec, + /// Currently analyzed instruction. + current_instruction: SourceInstruction, + /// 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, - source: &SourceInstruction, - ) -> Option { + fn find_all(&mut self, body: &MutableBody) -> Vec { self.locals = body.locals().to_vec(); - self.target = None; - match *source { - SourceInstruction::Statement { idx, bb } => { - let BasicBlock { statements, .. } = &body.blocks()[bb]; - let stmt = &statements[idx]; - self.visit_statement(stmt, self.__location_hack_remove_before_merging(stmt.span)) - } - SourceInstruction::Terminator { bb } => { - let BasicBlock { terminator, .. } = &body.blocks()[bb]; - self.visit_terminator( - terminator, - self.__location_hack_remove_before_merging(terminator.span), - ) - } + for (bb_idx, bb) in body.blocks().iter().enumerate() { + self.current_instruction = SourceInstruction::Statement { idx: 0, bb: bb_idx }; + self.visit_basic_block(bb); } - self.target.clone() + // Push the last current target into the list. + self.targets.push(self.current_target.clone()); + self.targets.clone() } } impl CheckUninitVisitor { pub fn new() -> Self { - Self { locals: vec![], target: None } + Self { + locals: vec![], + targets: vec![], + current_instruction: SourceInstruction::Statement { idx: 0, bb: 0 }, + 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 { - after_instruction: vec![], - before_instruction: vec![], - }); - target.push_operation(source_op); + // If we switched to the next instruction, push the old one onto the list of targets. + if self.current_target.source != self.current_instruction { + self.targets.push(self.current_target.clone()); + self.current_target = InitRelevantInstruction { + source: self.current_instruction, + after_instruction: vec![], + before_instruction: vec![], + }; + } + self.current_target.push_operation(source_op); } } @@ -148,9 +152,20 @@ impl MirVisitor for CheckUninitVisitor { | StatementKind::Intrinsic(NonDivergingIntrinsic::Assume(_)) | StatementKind::Nop => self.super_statement(stmt, location), } + // Switch to the next statement. + if let SourceInstruction::Statement { idx, bb } = self.current_instruction { + self.current_instruction = SourceInstruction::Statement { idx: idx + 1, bb } + } else { + unreachable!() + } } fn visit_terminator(&mut self, term: &Terminator, location: Location) { + if let SourceInstruction::Statement { bb, .. } = self.current_instruction { + self.current_instruction = SourceInstruction::Terminator { bb }; + } 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, .. } => { 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 d3eb0c1d51dc..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 @@ -168,6 +168,8 @@ impl MemoryInitOp { /// before or after the instruction. #[derive(Clone, Debug)] pub struct InitRelevantInstruction { + /// The instruction that affects the state of the memory. + pub source: SourceInstruction, /// All memory-related operations that should happen after the instruction. pub before_instruction: Vec, /// All memory-related operations that should happen after the instruction. From db25dca10dab3293706a1f06573e9ccdb3075f73 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 19 Aug 2024 15:57:29 -0700 Subject: [PATCH 11/12] Address suggestions from code review --- .../delayed_ub/instrumentation_visitor.rs | 45 ++++++++++--------- .../kani_middle/transform/check_uninit/mod.rs | 4 +- .../check_uninit/ptr_uninit/uninit_visitor.rs | 45 ++++++++++--------- 3 files changed, 50 insertions(+), 44 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs index b26de868c4d1..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 @@ -25,8 +25,6 @@ use std::collections::HashSet; pub struct InstrumentationVisitor<'a, 'tcx> { /// All target instructions in the body. targets: Vec, - /// Currently analyzed instruction. - current_instruction: SourceInstruction, /// Current analysis target, eventually needs to be added to a list of all targets. current_target: InitRelevantInstruction, /// Aliasing analysis data. @@ -38,14 +36,16 @@ pub struct InstrumentationVisitor<'a, 'tcx> { } impl<'a, 'tcx> TargetFinder for InstrumentationVisitor<'a, 'tcx> { - fn find_all(&mut self, body: &MutableBody) -> Vec { + fn find_all(mut self, body: &MutableBody) -> Vec { for (bb_idx, bb) in body.blocks().iter().enumerate() { - self.current_instruction = SourceInstruction::Statement { idx: 0, bb: bb_idx }; + self.current_target = InitRelevantInstruction { + source: SourceInstruction::Statement { idx: 0, bb: bb_idx }, + before_instruction: vec![], + after_instruction: vec![], + }; self.visit_basic_block(bb); } - // Push the last current target into the list. - self.targets.push(self.current_target.clone()); - self.targets.clone() + self.targets } } @@ -58,7 +58,6 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> { ) -> Self { Self { targets: vec![], - current_instruction: SourceInstruction::Statement { idx: 0, bb: 0 }, current_target: InitRelevantInstruction { source: SourceInstruction::Statement { idx: 0, bb: 0 }, before_instruction: vec![], @@ -72,15 +71,6 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> { } fn push_target(&mut self, source_op: MemoryInitOp) { - // If we switched to the next instruction, push the old one onto the list of targets. - if self.current_target.source != self.current_instruction { - self.targets.push(self.current_target.clone()); - self.current_target = InitRelevantInstruction { - source: self.current_instruction, - after_instruction: vec![], - before_instruction: vec![], - }; - } self.current_target.push_operation(source_op); } } @@ -89,20 +79,33 @@ impl<'a, 'tcx> MirVisitor for InstrumentationVisitor<'a, 'tcx> { fn visit_statement(&mut self, stmt: &Statement, location: Location) { self.super_statement(stmt, location); // Switch to the next statement. - if let SourceInstruction::Statement { idx, bb } = self.current_instruction { - self.current_instruction = 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 let SourceInstruction::Statement { bb, .. } = self.current_instruction { - self.current_instruction = SourceInstruction::Terminator { bb }; + 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/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs index 364bc7cc12a7..88d906aa3134 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -32,7 +32,7 @@ mod ty_layout; /// Trait that the instrumentation target providers must implement to work with the instrumenter. pub trait TargetFinder { - fn find_all(&mut self, body: &MutableBody) -> Vec; + fn find_all(self, body: &MutableBody) -> Vec; } // Function bodies of those functions will not be instrumented as not to cause infinite recursion. @@ -77,7 +77,7 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { &mut self, 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. 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 96c97c3468e9..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 @@ -29,22 +29,22 @@ pub struct CheckUninitVisitor { locals: Vec, /// All target instructions in the body. targets: Vec, - /// Currently analyzed instruction. - current_instruction: SourceInstruction, /// Current analysis target, eventually needs to be added to a list of all targets. current_target: InitRelevantInstruction, } impl TargetFinder for CheckUninitVisitor { - fn find_all(&mut self, body: &MutableBody) -> Vec { + fn find_all(mut self, body: &MutableBody) -> Vec { self.locals = body.locals().to_vec(); for (bb_idx, bb) in body.blocks().iter().enumerate() { - self.current_instruction = SourceInstruction::Statement { idx: 0, bb: bb_idx }; + self.current_target = InitRelevantInstruction { + source: SourceInstruction::Statement { idx: 0, bb: bb_idx }, + before_instruction: vec![], + after_instruction: vec![], + }; self.visit_basic_block(bb); } - // Push the last current target into the list. - self.targets.push(self.current_target.clone()); - self.targets.clone() + self.targets } } @@ -53,7 +53,6 @@ impl CheckUninitVisitor { Self { locals: vec![], targets: vec![], - current_instruction: SourceInstruction::Statement { idx: 0, bb: 0 }, current_target: InitRelevantInstruction { source: SourceInstruction::Statement { idx: 0, bb: 0 }, before_instruction: vec![], @@ -63,15 +62,6 @@ impl CheckUninitVisitor { } fn push_target(&mut self, source_op: MemoryInitOp) { - // If we switched to the next instruction, push the old one onto the list of targets. - if self.current_target.source != self.current_instruction { - self.targets.push(self.current_target.clone()); - self.current_target = InitRelevantInstruction { - source: self.current_instruction, - after_instruction: vec![], - before_instruction: vec![], - }; - } self.current_target.push_operation(source_op); } } @@ -153,16 +143,27 @@ impl MirVisitor for CheckUninitVisitor { | StatementKind::Nop => self.super_statement(stmt, location), } // Switch to the next statement. - if let SourceInstruction::Statement { idx, bb } = self.current_instruction { - self.current_instruction = 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 let SourceInstruction::Statement { bb, .. } = self.current_instruction { - self.current_instruction = SourceInstruction::Terminator { bb }; + 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!() } @@ -332,6 +333,8 @@ impl MirVisitor for CheckUninitVisitor { | 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) { From f3553cfb6e69f3a82b816d09a7147c19875f0087 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Thu, 22 Aug 2024 08:55:38 -0400 Subject: [PATCH 12/12] Add tests where an instruction gets instrumented more than once --- .../uninit/multiple-instrumentations.expected | 20 +++++++++ .../uninit/multiple-instrumentations.rs | 42 +++++++++++++++++++ 2 files changed, 62 insertions(+) create mode 100644 tests/expected/uninit/multiple-instrumentations.expected create mode 100644 tests/expected/uninit/multiple-instrumentations.rs 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) +}