From 130cfd56e75822ec8dd7f3e9da2d2bbf30f952a0 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 5 Aug 2024 11:57:15 -0700 Subject: [PATCH 01/13] Avoid corner-cases by grouping instrumentation into basic blocks --- .../src/kani_middle/transform/body.rs | 16 +- .../kani_middle/transform/check_uninit/mod.rs | 295 ++++++++++++------ .../check_uninit/relevant_instruction.rs | 65 +++- .../kani_middle/transform/kani_intrinsics.rs | 120 ++++--- 4 files changed, 331 insertions(+), 165 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 3d110c4e9656..4a64ea7615f8 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -309,16 +309,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 }); @@ -501,6 +501,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/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs index 5c7194f879d1..5299f8f2679f 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, ConstOperand, Mutability, + Operand, Place, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, UnwindAction, }, ty::{FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Ty, TyConst, TyKind, UintTy}, CrateDef, @@ -94,17 +94,32 @@ impl<'a> UninitInstrumenter<'a> { // the source instruction. let mut skip_first = HashSet::new(); + // 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. + let mut autogenerated_bbs = 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 !autogenerated_bbs.contains(&bb_idx) { + 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, + &mut autogenerated_bbs, + ); + } + } + bb_idx += 1; } (orig_len != body.blocks().len(), body) } @@ -116,13 +131,28 @@ impl<'a> UninitInstrumenter<'a> { body: &mut MutableBody, instruction: InitRelevantInstruction, skip_first: &mut HashSet, + autogenerated_bbs: &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( + tcx, + body, + &mut source, + operation, + skip_first, + autogenerated_bbs, + ); } for operation in instruction.after_instruction { - self.build_check_for_operation(tcx, body, &mut source, operation, skip_first); + self.build_check_for_operation( + tcx, + body, + &mut source, + operation, + skip_first, + autogenerated_bbs, + ); } } @@ -134,18 +164,22 @@ impl<'a> UninitInstrumenter<'a> { source: &mut SourceInstruction, operation: MemoryInitOp, skip_first: &mut HashSet, + autogenerated_bbs: &mut HashSet, ) { if let MemoryInitOp::Unsupported { reason } | MemoryInitOp::TriviallyUnsafe { reason } = &operation { - collect_skipped(&operation, body, skip_first); + // If the operation is unsupported or trivially accesses uninitialized memory, encode + // the check as `assert!(false)`. + collect_skipped(operation.position(), source, body, skip_first); self.inject_assert_false(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,34 +188,47 @@ 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); + collect_skipped(operation.position(), source, body, skip_first); self.inject_assert_false(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) - } + | MemoryInitOp::CheckRef { .. } => self.build_get_and_check( + tcx, + body, + source, + operation, + pointee_info, + skip_first, + autogenerated_bbs, + ), MemoryInitOp::SetSliceChunk { .. } | MemoryInitOp::Set { .. } - | MemoryInitOp::SetRef { .. } => { - self.build_set(tcx, body, source, operation, pointee_ty_info, skip_first) - } + | MemoryInitOp::SetRef { .. } => self.build_set( + tcx, + body, + source, + operation, + pointee_info, + skip_first, + autogenerated_bbs, + ), MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => { unreachable!() } - } + }; } /// Inject a load from memory initialization state and an assertion that all non-padding bytes @@ -194,15 +241,21 @@ impl<'a> UninitInstrumenter<'a> { operation: MemoryInitOp, pointee_info: PointeeInfo, skip_first: &mut HashSet, + autogenerated_bbs: &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); + // 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; + + let ptr_operand = operation.mk_operand(body, &mut statements, source); 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 { @@ -224,14 +277,20 @@ impl<'a> UninitInstrumenter<'a> { 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 = 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. @@ -250,27 +309,38 @@ impl<'a> UninitInstrumenter<'a> { 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 = 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, 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); 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, skip_first); + body.insert_bb(BasicBlock { statements, terminator }, source, operation.position()); + 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, skip_first); let operand_ty = match &operation { MemoryInitOp::Check { operand } | MemoryInitOp::CheckSliceChunk { operand, .. } @@ -299,17 +369,23 @@ impl<'a> UninitInstrumenter<'a> { operation: MemoryInitOp, pointee_info: PointeeInfo, skip_first: &mut HashSet, + autogenerated_bbs: &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); + // 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; + + let ptr_operand = operation.mk_operand(body, &mut statements, source); let value = operation.expect_value(); 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 { @@ -347,14 +423,20 @@ impl<'a> UninitInstrumenter<'a> { 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 = 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. @@ -373,28 +455,38 @@ impl<'a> UninitInstrumenter<'a> { 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 = 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, skip_first); + body.insert_bb(BasicBlock { statements, terminator }, source, operation.position()); + autogenerated_bbs.insert(body.blocks().len() - 1); } fn inject_assert_false( @@ -430,36 +522,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/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..b4b7568f6f94 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) => { @@ -206,18 +216,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 +258,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 +308,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 e3993f96f3e5977b8403c72c835258937b683817 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 5 Aug 2024 15:05:13 -0700 Subject: [PATCH 02/13] Make sure we short-circuit correctly when encountering ZSTs in the predicates --- .../src/kani_middle/transform/kani_intrinsics.rs | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index b4b7568f6f94..2b9d6d22f040 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -205,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( From 43a884f36e59927af3b3c303dfc62226eba09e6f Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 5 Aug 2024 15:08:29 -0700 Subject: [PATCH 03/13] Mitigate the case when delayed UB analysis returns false positives due to over-instrumentation --- .../kani_middle/points_to/points_to_graph.rs | 78 +++++++++++++------ .../delayed_ub/instrumentation_visitor.rs | 68 +++++++++++----- .../transform/check_uninit/delayed_ub/mod.rs | 4 +- 3 files changed, 104 insertions(+), 46 deletions(-) diff --git a/kani-compiler/src/kani_middle/points_to/points_to_graph.rs b/kani-compiler/src/kani_middle/points_to/points_to_graph.rs index d2e80f24c737..61804d0ff71a 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_graph.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_graph.rs @@ -63,6 +63,27 @@ impl<'tcx> MemLoc<'tcx> { } } +/// Data structure to keep track of both successors and ancestors of the node. +#[derive(Clone, Debug, Default, PartialEq, Eq)] +struct NodeData<'tcx> { + successors: HashSet>, + ancestors: HashSet>, +} + +impl<'tcx> NodeData<'tcx> { + /// Merge two instances of NodeData together, return true if the original one was updated and + /// false otherwise. + fn merge(&mut self, other: Self) -> bool { + let successors_before = self.successors.len(); + let ancestors_before = self.ancestors.len(); + self.successors.extend(other.successors); + self.ancestors.extend(other.ancestors); + let successors_after = self.successors.len(); + let ancestors_after = self.ancestors.len(); + successors_before != successors_after || ancestors_before != ancestors_after + } +} + /// Graph data structure that stores the current results of the point-to analysis. The graph is /// directed, so having an edge between two places means that one is pointing to the other. /// @@ -82,24 +103,39 @@ impl<'tcx> MemLoc<'tcx> { #[derive(Clone, Debug, PartialEq, Eq)] pub struct PointsToGraph<'tcx> { /// A hash map of node --> {nodes} edges. - edges: HashMap, HashSet>>, + nodes: HashMap, NodeData<'tcx>>, } impl<'tcx> PointsToGraph<'tcx> { pub fn empty() -> Self { - Self { edges: HashMap::new() } + Self { nodes: HashMap::new() } } /// Collect all nodes which have incoming edges from `nodes`. pub fn successors(&self, nodes: &HashSet>) -> HashSet> { - nodes.iter().flat_map(|node| self.edges.get(node).cloned().unwrap_or_default()).collect() + nodes + .iter() + .flat_map(|node| self.nodes.get(node).cloned().unwrap_or_default().successors) + .collect() } - /// For each node in `from`, add an edge to each node in `to`. + /// Collect all nodes which have outgoing edges to `nodes`. + pub fn ancestors(&self, nodes: &HashSet>) -> HashSet> { + nodes + .iter() + .flat_map(|node| self.nodes.get(node).cloned().unwrap_or_default().ancestors) + .collect() + } + + /// For each node in `from`, add an edge to each node in `to` (and the reverse for ancestors). pub fn extend(&mut self, from: &HashSet>, to: &HashSet>) { for node in from.iter() { - let node_pointees = self.edges.entry(*node).or_default(); - node_pointees.extend(to.iter()); + let node_pointees = self.nodes.entry(*node).or_default(); + node_pointees.successors.extend(to.iter()); + } + for node in to.iter() { + let node_pointees = self.nodes.entry(*node).or_default(); + node_pointees.ancestors.extend(from.iter()); } } @@ -150,16 +186,16 @@ impl<'tcx> PointsToGraph<'tcx> { /// Dump the graph into a file using the graphviz format for later visualization. pub fn dump(&self, file_path: &str) { let mut nodes: Vec = - self.edges.keys().map(|from| format!("\t\"{:?}\"", from)).collect(); + self.nodes.keys().map(|from| format!("\t\"{:?}\"", from)).collect(); nodes.sort(); let nodes_str = nodes.join("\n"); let mut edges: Vec = self - .edges + .nodes .iter() .flat_map(|(from, to)| { let from = format!("\"{:?}\"", from); - to.iter().map(move |to| { + to.successors.iter().map(move |to| { let to = format!("\"{:?}\"", to); format!("\t{} -> {}", from.clone(), to) }) @@ -178,24 +214,18 @@ impl<'tcx> PointsToGraph<'tcx> { // Working queue. let mut queue = VecDeque::from_iter(targets); // Add all statics, as they can be accessed at any point. - let statics = self.edges.keys().filter(|node| matches!(node, MemLoc::Static(_))); + let statics = self.nodes.keys().filter(|node| matches!(node, MemLoc::Static(_))); queue.extend(statics); // Add all entries. while let Some(next_target) = queue.pop_front() { - result.edges.entry(next_target).or_insert_with(|| { - let outgoing_edges = - self.edges.get(&next_target).cloned().unwrap_or(HashSet::new()); - queue.extend(outgoing_edges.iter()); + result.nodes.entry(next_target).or_insert_with(|| { + let outgoing_edges = self.nodes.get(&next_target).cloned().unwrap_or_default(); + queue.extend(outgoing_edges.successors.iter()); outgoing_edges.clone() }); } result } - - /// Retrieve all places to which a given place is pointing to. - pub fn pointees_of(&self, target: &MemLoc<'tcx>) -> HashSet> { - self.edges.get(&target).unwrap_or(&HashSet::new()).clone() - } } /// Since we are performing the analysis using a dataflow, we need to implement a proper monotonous @@ -206,12 +236,10 @@ impl<'tcx> JoinSemiLattice for PointsToGraph<'tcx> { fn join(&mut self, other: &Self) -> bool { let mut updated = false; // Check every node in the other graph. - for (from, to) in other.edges.iter() { - let existing_to = self.edges.entry(*from).or_default(); - let initial_size = existing_to.len(); - existing_to.extend(to); - let new_size = existing_to.len(); - updated |= initial_size != new_size; + for (node, data) in other.nodes.iter() { + let existing_node = self.nodes.entry(*node).or_default(); + let changed = existing_node.merge(data.clone()); + updated |= changed; } updated } 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..d044134b0e46 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 @@ -112,25 +112,57 @@ impl<'a, 'tcx> MirVisitor for InstrumentationVisitor<'a, 'tcx> { } 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 - .resolve_place_stable(place.clone(), self.current_instance, self.tcx) - .intersection(&self.analysis_targets) - .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()) }); + // In order to check whether we should set-instrument the place, we need to figure out if + // the place has a common ancestor of the same level with the target. + // + // This is needed because instrumenting the place only if it points to the target could give + // false positives in presence of some aliasing relations. + // + // Here is a simple example, imagine the following aliasing graph: + // + // `place_a <-- place_b --> place_c` + // + // If `place_a` is a legitimate instrumentation target, we would get-instrument an + // instruction that reads from `(*place_b)`, but that could mean that `place_c` is checked, + // too. Hence, if we don't set-instrument `place_c` we will get a false-positive. + let needs_set = { + let mut has_common_ancestor = false; + let mut self_ancestors = + self.points_to.resolve_place_stable(place.clone(), self.current_instance, self.tcx); + let mut target_ancestors = self.analysis_targets.clone(); + + while !self_ancestors.is_empty() || !target_ancestors.is_empty() { + if self_ancestors.intersection(&target_ancestors).next().is_some() { + has_common_ancestor = true; + break; + } + self_ancestors = self.points_to.ancestors(&self_ancestors); + target_ancestors = self.points_to.ancestors(&target_ancestors); } + + has_common_ancestor + }; + + // In order to check whether we should get-instrument the place, finding the intersection + // with analysis targets is enough. + let needs_get = { + self.points_to + .resolve_place_stable(place.clone(), self.current_instance, self.tcx) + .intersection(&self.analysis_targets) + .next() + .is_some() + }; + + // If we are mutating the place, initialize it. + if ptx.is_mutating() && needs_set { + self.push_target(MemoryInitOp::SetRef { + operand: Operand::Copy(place.clone()), + value: true, + position: InsertPosition::After, + }); + } else if !ptx.is_mutating() && needs_get { + // 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/delayed_ub/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs index 6b488569813f..14ed0345e88d 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 @@ -101,9 +101,7 @@ impl GlobalPass for DelayedUbPass { } // Since analysis targets are *pointers*, need to get its successors for instrumentation. - for target in targets.iter() { - analysis_targets.extend(global_points_to_graph.pointees_of(target)); - } + analysis_targets.extend(global_points_to_graph.successors(&targets)); // If we are generating MIR, generate the points-to graph as well. if tcx.sess.opts.output_types.contains_key(&OutputType::Mir) { From 9a54aa633fb8d62c039810aa4e6155cca7fa24b3 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 5 Aug 2024 15:27:46 -0700 Subject: [PATCH 04/13] Better comment explaining delayed UB instrumentation --- .../delayed_ub/instrumentation_visitor.rs | 43 ++++++++++++------- 1 file changed, 27 insertions(+), 16 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 d044134b0e46..4c0622d6ac1a 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 @@ -112,19 +112,40 @@ impl<'a, 'tcx> MirVisitor for InstrumentationVisitor<'a, 'tcx> { } fn visit_place(&mut self, place: &Place, ptx: PlaceContext, location: Location) { + // In order to check whether we should get-instrument the place, see if it resolves to the + // analysis target. + let needs_get = { + self.points_to + .resolve_place_stable(place.clone(), self.current_instance, self.tcx) + .intersection(&self.analysis_targets) + .next() + .is_some() + }; + // In order to check whether we should set-instrument the place, we need to figure out if // the place has a common ancestor of the same level with the target. // - // This is needed because instrumenting the place only if it points to the target could give + // This is needed because instrumenting the place only if it resolves to the target could give // false positives in presence of some aliasing relations. // - // Here is a simple example, imagine the following aliasing graph: + // Here is a simple example: + // ``` + // fn foo(val_1: u32, val_2: u32, flag: bool) { + // let reference = if flag { + // &val_1 + // } else { + // &val_2 + // }; + // let _ = *reference; + // } + // ``` + // It yields the following aliasing graph: // - // `place_a <-- place_b --> place_c` + // `val_1 <-- reference --> val_2` // - // If `place_a` is a legitimate instrumentation target, we would get-instrument an - // instruction that reads from `(*place_b)`, but that could mean that `place_c` is checked, - // too. Hence, if we don't set-instrument `place_c` we will get a false-positive. + // If `val_1` is a legitimate instrumentation target, we would get-instrument an instruction + // that reads from `*reference`, but that could mean that `val_2` is checked, too. Hence, + // if we don't set-instrument `val_2` we will get a false-positive. let needs_set = { let mut has_common_ancestor = false; let mut self_ancestors = @@ -143,16 +164,6 @@ impl<'a, 'tcx> MirVisitor for InstrumentationVisitor<'a, 'tcx> { has_common_ancestor }; - // In order to check whether we should get-instrument the place, finding the intersection - // with analysis targets is enough. - let needs_get = { - self.points_to - .resolve_place_stable(place.clone(), self.current_instance, self.tcx) - .intersection(&self.analysis_targets) - .next() - .is_some() - }; - // If we are mutating the place, initialize it. if ptx.is_mutating() && needs_set { self.push_target(MemoryInitOp::SetRef { From 92f967f5b80387516defd2805d94eaf4c43c2bdc Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Tue, 6 Aug 2024 08:40:01 -0700 Subject: [PATCH 05/13] Create a single interface for UninitInstrumenter --- .../transform/check_uninit/delayed_ub/mod.rs | 23 +- .../kani_middle/transform/check_uninit/mod.rs | 197 ++++++++---------- .../transform/check_uninit/ptr_uninit/mod.rs | 16 +- 3 files changed, 104 insertions(+), 132 deletions(-) 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 14ed0345e88d..c31f72c9b5c3 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; @@ -110,12 +109,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, @@ -123,12 +118,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 5299f8f2679f..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,7 +13,7 @@ use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use stable_mir::{ mir::{ - mono::Instance, AggregateKind, BasicBlock, BasicBlockIdx, ConstOperand, Mutability, + 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}, @@ -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,39 +121,15 @@ 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(); - - // 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. - let mut autogenerated_bbs = 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() { // Skip instrumentation of autogenerated blocks. - if !autogenerated_bbs.contains(&bb_idx) { + if !self.autogenerated_bbs.contains(&bb_idx) { if let Some(candidate) = - target_finder.find_next(&body, bb_idx, skip_first.contains(&bb_idx)) + target_finder.find_next(&body, bb_idx, self.skip_first.contains(&bb_idx)) { - self.build_check_for_instruction( - tcx, - &mut body, - candidate, - &mut skip_first, - &mut autogenerated_bbs, - ); + self.build_check_for_instruction(&mut body, candidate); } } bb_idx += 1; @@ -127,52 +140,32 @@ 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, - autogenerated_bbs: &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, - autogenerated_bbs, - ); + 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, - autogenerated_bbs, - ); + 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, - autogenerated_bbs: &mut HashSet, ) { if let MemoryInitOp::Unsupported { reason } | MemoryInitOp::TriviallyUnsafe { reason } = &operation { // If the operation is unsupported or trivially accesses uninitialized memory, encode // the check as `assert!(false)`. - collect_skipped(operation.position(), source, 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; }; @@ -195,8 +188,8 @@ impl<'a> UninitInstrumenter<'a> { let reason = format!( "Kani currently doesn't support checking memory initialization for pointers to `{pointee_ty}.", ); - collect_skipped(operation.position(), source, 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; } } @@ -205,26 +198,12 @@ impl<'a> UninitInstrumenter<'a> { match &operation { MemoryInitOp::CheckSliceChunk { .. } | MemoryInitOp::Check { .. } - | MemoryInitOp::CheckRef { .. } => self.build_get_and_check( - tcx, - body, - source, - operation, - pointee_info, - skip_first, - autogenerated_bbs, - ), + | MemoryInitOp::CheckRef { .. } => { + self.build_get_and_check(body, source, operation, pointee_info) + } MemoryInitOp::SetSliceChunk { .. } | MemoryInitOp::Set { .. } - | MemoryInitOp::SetRef { .. } => self.build_set( - tcx, - body, - source, - operation, - pointee_info, - skip_first, - autogenerated_bbs, - ), + | MemoryInitOp::SetRef { .. } => self.build_set(body, source, operation, pointee_info), MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => { unreachable!() } @@ -235,13 +214,10 @@ impl<'a> UninitInstrumenter<'a> { /// 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, - autogenerated_bbs: &mut HashSet, ) { let ret_place = Place { local: body.new_local(Ty::bool_ty(), source.span(body.blocks()), Mutability::Not), @@ -250,10 +226,8 @@ impl<'a> UninitInstrumenter<'a> { // 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; - let ptr_operand = operation.mk_operand(body, &mut statements, source); - match pointee_info.layout() { + let terminator = match pointee_info.layout() { PointeeLayout::Sized { 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 @@ -273,11 +247,11 @@ 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(), ); - terminator = Terminator { + Terminator { kind: TerminatorKind::Call { func: Operand::Copy(Place::from(body.new_local( is_ptr_initialized_instance.ty(), @@ -290,7 +264,7 @@ impl<'a> UninitInstrumenter<'a> { 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. @@ -304,13 +278,13 @@ 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, &mut statements, source, &element_layout); - terminator = Terminator { + Terminator { kind: TerminatorKind::Call { func: Operand::Copy(Place::from(body.new_local( is_ptr_initialized_instance.ty(), @@ -323,24 +297,24 @@ impl<'a> UninitInstrumenter<'a> { unwind: UnwindAction::Terminate, }, span: source.span(body.blocks()), - }; + } } PointeeLayout::TraitObject => { - collect_skipped(operation.position(), source, 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; } }; // Construct the basic block and insert it into the body. - collect_skipped(operation.position(), source, body, skip_first); + collect_skipped(operation.position(), source, body, &mut self.skip_first); body.insert_bb(BasicBlock { statements, terminator }, source, operation.position()); - autogenerated_bbs.insert(body.blocks().len() - 1); + 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, skip_first); + collect_skipped(operation.position(), source, body, &mut self.skip_first); let operand_ty = match &operation { MemoryInitOp::Check { operand } | MemoryInitOp::CheckSliceChunk { operand, .. } @@ -348,7 +322,7 @@ impl<'a> UninitInstrumenter<'a> { _ => unreachable!(), }; body.insert_check( - tcx, + self.tcx, &self.check_type, source, operation.position(), @@ -363,27 +337,22 @@ 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, - autogenerated_bbs: &mut HashSet, ) { let ret_place = Place { local: body.new_local(Ty::new_tuple(&[]), source.span(body.blocks()), Mutability::Not), projection: vec![], }; + // 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; - let ptr_operand = operation.mk_operand(body, &mut statements, source); let value = operation.expect_value(); - - match pointee_info.layout() { + let terminator = match pointee_info.layout() { PointeeLayout::Sized { 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 @@ -419,11 +388,11 @@ 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(), ); - terminator = Terminator { + Terminator { kind: TerminatorKind::Call { func: Operand::Copy(Place::from(body.new_local( set_ptr_initialized_instance.ty(), @@ -436,7 +405,7 @@ impl<'a> UninitInstrumenter<'a> { 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. @@ -450,13 +419,13 @@ 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, &mut statements, source, &element_layout); - terminator = Terminator { + Terminator { kind: TerminatorKind::Call { func: Operand::Copy(Place::from(body.new_local( set_ptr_initialized_instance.ty(), @@ -477,16 +446,16 @@ impl<'a> UninitInstrumenter<'a> { 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, skip_first); + collect_skipped(operation.position(), source, body, &mut self.skip_first); body.insert_bb(BasicBlock { statements, terminator }, source, operation.position()); - autogenerated_bbs.insert(body.blocks().len() - 1); + self.autogenerated_bbs.insert(body.blocks().len() - 1); } fn inject_assert_false( 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) } } From f3d97d07d887ba36b8b7a74bfc43f28155eda1bd Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Tue, 6 Aug 2024 10:35:40 -0700 Subject: [PATCH 06/13] Add a harness for `Box::from_raw` --- tests/std-checks/std/Cargo.toml | 13 ++++++++++ tests/std-checks/std/boxed.expected | 1 + tests/std-checks/std/src/boxed.rs | 40 +++++++++++++++++++++++++++++ tests/std-checks/std/src/lib.rs | 8 ++++++ 4 files changed, 62 insertions(+) create mode 100644 tests/std-checks/std/Cargo.toml create mode 100644 tests/std-checks/std/boxed.expected create mode 100644 tests/std-checks/std/src/boxed.rs create mode 100644 tests/std-checks/std/src/lib.rs diff --git a/tests/std-checks/std/Cargo.toml b/tests/std-checks/std/Cargo.toml new file mode 100644 index 000000000000..29a9a12663e9 --- /dev/null +++ b/tests/std-checks/std/Cargo.toml @@ -0,0 +1,13 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "verify-std" +version = "0.1.0" +edition = "2021" +description = "This crate contains contracts and harnesses for std library" + +[package.metadata.kani] +unstable = { function-contracts = true, mem-predicates = true, ptr-to-ref-cast-checks = true, uninit-checks = true } + +[package.metadata.kani.flags] +output-format = "terse" diff --git a/tests/std-checks/std/boxed.expected b/tests/std-checks/std/boxed.expected new file mode 100644 index 000000000000..4426ff6c02cd --- /dev/null +++ b/tests/std-checks/std/boxed.expected @@ -0,0 +1 @@ +Complete - 2 successfully verified harnesses, 0 failures, 2 total. diff --git a/tests/std-checks/std/src/boxed.rs b/tests/std-checks/std/src/boxed.rs new file mode 100644 index 000000000000..a587f29a93d3 --- /dev/null +++ b/tests/std-checks/std/src/boxed.rs @@ -0,0 +1,40 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +extern crate kani; + +/// Create wrapper functions to standard library functions that contains their contract. +pub mod contracts { + use kani::{mem::*, requires}; + + /// The actual pre-condition is more complicated: + /// + /// "For non-zero-sized values, ... a value: *mut T that has been allocated with the Global + /// allocator with Layout::for_value(&*value) may be converted into a box using + /// Box::::from_raw(value)." + /// + /// "For zero-sized values, the Box pointer still has to be valid for reads and writes and + /// sufficiently aligned." + #[requires(can_dereference(raw))] + pub unsafe fn from_raw(raw: *mut T) -> Box { + std::boxed::Box::from_raw(raw) + } +} + +#[cfg(kani)] +mod verify { + use super::*; + + #[kani::proof_for_contract(contracts::from_raw)] + pub fn check_from_raw_u32() { + let ptr = unsafe { std::alloc::alloc(std::alloc::Layout::new::()) as *mut u32 }; + unsafe { ptr.write(kani::any()) }; + let _ = unsafe { contracts::from_raw(ptr) }; + } + + #[kani::proof_for_contract(contracts::from_raw)] + pub fn check_from_raw_unit() { + let ptr = kani::any::() as *mut (); + let _ = unsafe { contracts::from_raw(ptr) }; + } +} diff --git a/tests/std-checks/std/src/lib.rs b/tests/std-checks/std/src/lib.rs new file mode 100644 index 000000000000..af285a9729cb --- /dev/null +++ b/tests/std-checks/std/src/lib.rs @@ -0,0 +1,8 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Top file that includes all sub-modules mimicking std structure. + +extern crate kani; + +mod boxed; From baa01592c3b5fcb44f7e86a1596443cd2f2d3085 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Tue, 6 Aug 2024 11:00:02 -0700 Subject: [PATCH 07/13] Add a test to catch spurious failures due to points-to analysis overapproximation --- .../delayed_ub/instrumentation_visitor.rs | 2 ++ .../uninit/delayed-ub-overapprox.expected | 1 + .../expected/uninit/delayed-ub-overapprox.rs | 32 +++++++++++++++++++ 3 files changed, 35 insertions(+) create mode 100644 tests/expected/uninit/delayed-ub-overapprox.expected create mode 100644 tests/expected/uninit/delayed-ub-overapprox.rs 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 4c0622d6ac1a..d3800027e002 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 @@ -146,6 +146,8 @@ impl<'a, 'tcx> MirVisitor for InstrumentationVisitor<'a, 'tcx> { // If `val_1` is a legitimate instrumentation target, we would get-instrument an instruction // that reads from `*reference`, but that could mean that `val_2` is checked, too. Hence, // if we don't set-instrument `val_2` we will get a false-positive. + // + // See `tests/expected/uninit/delayed-ub-overapprox.rs` for a more specific example. let needs_set = { let mut has_common_ancestor = false; let mut self_ancestors = diff --git a/tests/expected/uninit/delayed-ub-overapprox.expected b/tests/expected/uninit/delayed-ub-overapprox.expected new file mode 100644 index 000000000000..01a90d50b557 --- /dev/null +++ b/tests/expected/uninit/delayed-ub-overapprox.expected @@ -0,0 +1 @@ +Complete - 1 successfully verified harnesses, 0 failures, 1 total. diff --git a/tests/expected/uninit/delayed-ub-overapprox.rs b/tests/expected/uninit/delayed-ub-overapprox.rs new file mode 100644 index 000000000000..68585443fd38 --- /dev/null +++ b/tests/expected/uninit/delayed-ub-overapprox.rs @@ -0,0 +1,32 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks + +//! Make sure that no false positives are generated when points-to analysis overapproximates +//! aliasing. + +#[kani::proof] +fn check_delayed_ub_overapprox() { + unsafe { + let mut value: u128 = 0; + let value_ref = &mut value; + // Perform a call to the helper before mutable pointer cast. This way, a check inserted into + // the helper will pass. + helper(value_ref); + // Cast between two pointers of different padding, which will mark `value` as a possible + // delayed UB analysis target. + let ptr = value_ref as *mut _ as *mut (u8, u32, u64); + *ptr = (4, 4, 4); // Note that since we never read from `value` after overwriting it, no delayed UB occurs. + // Create another `value` and call helper. Note that since helper could potentially + // dereference a delayed-UB pointer, an initialization check will be added to the helper. + // Hence, delayed UB analysis needs to mark the value as properly initialized in shadow + // memory to avoid the spurious failure. + let mut value2: u128 = 0; + helper(&value2); + } +} + +/// A helper that could trigger delayed UB. +fn helper(reference: &u128) -> bool { + *reference == 42 +} From 1e5f822374303a4a21d2be820da1182720459ad4 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Tue, 6 Aug 2024 11:28:18 -0700 Subject: [PATCH 08/13] Code formatting --- tests/std-checks/std/src/boxed.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/std-checks/std/src/boxed.rs b/tests/std-checks/std/src/boxed.rs index a587f29a93d3..112b076ae4a3 100644 --- a/tests/std-checks/std/src/boxed.rs +++ b/tests/std-checks/std/src/boxed.rs @@ -7,8 +7,8 @@ extern crate kani; pub mod contracts { use kani::{mem::*, requires}; - /// The actual pre-condition is more complicated: - /// + /// The actual pre-condition is more complicated: + /// /// "For non-zero-sized values, ... a value: *mut T that has been allocated with the Global /// allocator with Layout::for_value(&*value) may be converted into a box using /// Box::::from_raw(value)." From aecfc72e9271c4594e27da9d1a2651bb261412d9 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 7 Aug 2024 08:52:33 -0700 Subject: [PATCH 09/13] Add tests for `Atomic::from_raw` --- tests/std-checks/std/atomic.expected | 1 + tests/std-checks/std/src/lib.rs | 1 + tests/std-checks/std/src/sync/atomic.rs | 77 +++++++++++++++++++++++++ tests/std-checks/std/src/sync/mod.rs | 4 ++ 4 files changed, 83 insertions(+) create mode 100644 tests/std-checks/std/atomic.expected create mode 100644 tests/std-checks/std/src/sync/atomic.rs create mode 100644 tests/std-checks/std/src/sync/mod.rs diff --git a/tests/std-checks/std/atomic.expected b/tests/std-checks/std/atomic.expected new file mode 100644 index 000000000000..158e99910c43 --- /dev/null +++ b/tests/std-checks/std/atomic.expected @@ -0,0 +1 @@ +Complete - 5 successfully verified harnesses, 0 failures, 5 total. diff --git a/tests/std-checks/std/src/lib.rs b/tests/std-checks/std/src/lib.rs index af285a9729cb..d78cf75a14ed 100644 --- a/tests/std-checks/std/src/lib.rs +++ b/tests/std-checks/std/src/lib.rs @@ -6,3 +6,4 @@ extern crate kani; mod boxed; +mod sync; diff --git a/tests/std-checks/std/src/sync/atomic.rs b/tests/std-checks/std/src/sync/atomic.rs new file mode 100644 index 000000000000..85c9a3380775 --- /dev/null +++ b/tests/std-checks/std/src/sync/atomic.rs @@ -0,0 +1,77 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +extern crate kani; + +use std::sync::atomic::{AtomicU16, AtomicU32, AtomicU64, AtomicU8, AtomicUsize}; + +/// Create wrapper functions to standard library functions that contains their contract. +pub mod contracts { + use super::*; + use kani::{mem::*, requires}; + + #[requires(can_dereference(ptr))] + pub unsafe fn from_ptr_u8<'a>(ptr: *mut u8) -> &'a AtomicU8 { + AtomicU8::from_ptr(ptr) + } + + #[requires(can_dereference(ptr))] + pub unsafe fn from_ptr_u16<'a>(ptr: *mut u16) -> &'a AtomicU16 { + AtomicU16::from_ptr(ptr) + } + + #[requires(can_dereference(ptr))] + pub unsafe fn from_ptr_u32<'a>(ptr: *mut u32) -> &'a AtomicU32 { + AtomicU32::from_ptr(ptr) + } + + #[requires(can_dereference(ptr))] + pub unsafe fn from_ptr_u64<'a>(ptr: *mut u64) -> &'a AtomicU64 { + AtomicU64::from_ptr(ptr) + } + + #[requires(can_dereference(ptr))] + pub unsafe fn from_ptr_usize<'a>(ptr: *mut usize) -> &'a AtomicUsize { + AtomicUsize::from_ptr(ptr) + } +} + +#[cfg(kani)] +mod verify { + use super::*; + + #[kani::proof_for_contract(contracts::from_ptr_u8)] + pub fn check_from_ptr_u8() { + let ptr = unsafe { std::alloc::alloc(std::alloc::Layout::new::()) as *mut u8 }; + unsafe { ptr.write(kani::any()) }; + let _ = unsafe { contracts::from_ptr_u8(ptr) }; + } + + #[kani::proof_for_contract(contracts::from_ptr_u16)] + pub fn check_from_ptr_u16() { + let ptr = unsafe { std::alloc::alloc(std::alloc::Layout::new::()) as *mut u16 }; + unsafe { ptr.write(kani::any()) }; + let _ = unsafe { contracts::from_ptr_u16(ptr) }; + } + + #[kani::proof_for_contract(contracts::from_ptr_u32)] + pub fn check_from_ptr_u32() { + let ptr = unsafe { std::alloc::alloc(std::alloc::Layout::new::()) as *mut u32 }; + unsafe { ptr.write(kani::any()) }; + let _ = unsafe { contracts::from_ptr_u32(ptr) }; + } + + #[kani::proof_for_contract(contracts::from_ptr_u64)] + pub fn check_from_ptr_u64() { + let ptr = unsafe { std::alloc::alloc(std::alloc::Layout::new::()) as *mut u64 }; + unsafe { ptr.write(kani::any()) }; + let _ = unsafe { contracts::from_ptr_u64(ptr) }; + } + + #[kani::proof_for_contract(contracts::from_ptr_usize)] + pub fn check_from_ptr_usize() { + let ptr = unsafe { std::alloc::alloc(std::alloc::Layout::new::()) as *mut usize }; + unsafe { ptr.write(kani::any()) }; + let _ = unsafe { contracts::from_ptr_usize(ptr) }; + } +} diff --git a/tests/std-checks/std/src/sync/mod.rs b/tests/std-checks/std/src/sync/mod.rs new file mode 100644 index 000000000000..14b3b086e487 --- /dev/null +++ b/tests/std-checks/std/src/sync/mod.rs @@ -0,0 +1,4 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +mod atomic; From 9aa9f1598bfc03f0dda0aa5d8db9be18347c2973 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 12 Aug 2024 14:42:24 -0700 Subject: [PATCH 10/13] Remove old flag --- tests/std-checks/std/Cargo.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/std-checks/std/Cargo.toml b/tests/std-checks/std/Cargo.toml index 29a9a12663e9..6c2b4e0073cb 100644 --- a/tests/std-checks/std/Cargo.toml +++ b/tests/std-checks/std/Cargo.toml @@ -7,7 +7,7 @@ edition = "2021" description = "This crate contains contracts and harnesses for std library" [package.metadata.kani] -unstable = { function-contracts = true, mem-predicates = true, ptr-to-ref-cast-checks = true, uninit-checks = true } +unstable = { function-contracts = true, mem-predicates = true, uninit-checks = true } [package.metadata.kani.flags] output-format = "terse" From 55daf4b1a5e83e5a5bd7c2d91b7f5b615a725c81 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 14 Aug 2024 08:52:22 -0700 Subject: [PATCH 11/13] Revert "Create a single interface for UninitInstrumenter" This reverts commit 92f967f5b80387516defd2805d94eaf4c43c2bdc. --- .../transform/check_uninit/delayed_ub/mod.rs | 23 +- .../kani_middle/transform/check_uninit/mod.rs | 197 ++++++++++-------- .../transform/check_uninit/ptr_uninit/mod.rs | 16 +- 3 files changed, 132 insertions(+), 104 deletions(-) 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 c31f72c9b5c3..14ed0345e88d 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,8 +11,9 @@ use crate::kani_middle::{ points_to::{run_points_to_analysis, MemLoc, PointsToGraph}, reachability::CallGraph, transform::{ - body::CheckType, check_uninit::UninitInstrumenter, BodyTransformation, GlobalPass, - TransformationResult, + body::{CheckType, MutableBody}, + check_uninit::UninitInstrumenter, + BodyTransformation, GlobalPass, TransformationResult, }, }; use crate::kani_queries::QueryDb; @@ -109,8 +110,12 @@ 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 = transformer.body(tcx, instance); + let body = MutableBody::from(transformer.body(tcx, instance)); // Instrument for delayed UB. let target_finder = InstrumentationVisitor::new( &global_points_to_graph, @@ -118,18 +123,12 @@ impl GlobalPass for DelayedUbPass { instance, tcx, ); - let (instrumentation_added, body) = UninitInstrumenter::run( - body, - tcx, - instance, - self.check_type.clone(), - &mut self.mem_init_fn_cache, - target_finder, - ); + let (instrumentation_added, body) = + instrumenter.instrument(tcx, body, instance, 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); + *transformation_result = TransformationResult::Modified(body.into()); }); } } diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs index cca33b902ed9..5299f8f2679f 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -13,7 +13,7 @@ use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use stable_mir::{ mir::{ - mono::Instance, AggregateKind, BasicBlock, BasicBlockIdx, Body, ConstOperand, Mutability, + mono::Instance, AggregateKind, BasicBlock, BasicBlockIdx, ConstOperand, Mutability, Operand, Place, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, UnwindAction, }, ty::{FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Ty, TyConst, TyKind, UintTy}, @@ -31,7 +31,7 @@ mod relevant_instruction; mod ty_layout; /// Trait that the instrumentation target providers must implement to work with the instrumenter. -pub trait TargetFinder { +trait TargetFinder { fn find_next( &mut self, body: &MutableBody, @@ -53,64 +53,27 @@ const SKIPPED_DIAGNOSTIC_ITEMS: &[&str] = &[ ]; /// Instruments the code with checks for uninitialized memory, agnostic to the source of targets. -pub struct UninitInstrumenter<'a, 'tcx> { - check_type: CheckType, +#[derive(Debug)] +pub struct UninitInstrumenter<'a> { + pub check_type: CheckType, /// 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, + pub mem_init_fn_cache: &'a mut HashMap<&'static str, FnDef>, } -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()) - } - +impl<'a> UninitInstrumenter<'a> { /// 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 self - .tcx - .get_diagnostic_name(rustc_internal::internal(self.tcx, instance.def.def_id())) + if tcx + .get_diagnostic_name(rustc_internal::internal(tcx, instance.def.def_id())) .map(|diagnostic_name| { SKIPPED_DIAGNOSTIC_ITEMS.contains(&diagnostic_name.to_ident_string().as_str()) }) @@ -121,15 +84,39 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { 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(); + + // 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. + let mut autogenerated_bbs = 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() { // Skip instrumentation of autogenerated blocks. - if !self.autogenerated_bbs.contains(&bb_idx) { + if !autogenerated_bbs.contains(&bb_idx) { if let Some(candidate) = - target_finder.find_next(&body, bb_idx, self.skip_first.contains(&bb_idx)) + target_finder.find_next(&body, bb_idx, skip_first.contains(&bb_idx)) { - self.build_check_for_instruction(&mut body, candidate); + self.build_check_for_instruction( + tcx, + &mut body, + candidate, + &mut skip_first, + &mut autogenerated_bbs, + ); } } bb_idx += 1; @@ -140,32 +127,52 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { /// 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, + autogenerated_bbs: &mut HashSet, ) { let mut source = instruction.source; for operation in instruction.before_instruction { - self.build_check_for_operation(body, &mut source, operation); + self.build_check_for_operation( + tcx, + body, + &mut source, + operation, + skip_first, + autogenerated_bbs, + ); } for operation in instruction.after_instruction { - self.build_check_for_operation(body, &mut source, operation); + self.build_check_for_operation( + tcx, + body, + &mut source, + operation, + skip_first, + autogenerated_bbs, + ); } } /// 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, + autogenerated_bbs: &mut HashSet, ) { if let MemoryInitOp::Unsupported { reason } | MemoryInitOp::TriviallyUnsafe { reason } = &operation { // 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); + collect_skipped(operation.position(), source, body, skip_first); + self.inject_assert_false(tcx, body, source, operation.position(), reason); return; }; @@ -188,8 +195,8 @@ 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); + collect_skipped(operation.position(), source, body, skip_first); + self.inject_assert_false(tcx, body, source, operation.position(), &reason); return; } } @@ -198,12 +205,26 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { match &operation { MemoryInitOp::CheckSliceChunk { .. } | MemoryInitOp::Check { .. } - | MemoryInitOp::CheckRef { .. } => { - self.build_get_and_check(body, source, operation, pointee_info) - } + | MemoryInitOp::CheckRef { .. } => self.build_get_and_check( + tcx, + body, + source, + operation, + pointee_info, + skip_first, + autogenerated_bbs, + ), MemoryInitOp::SetSliceChunk { .. } | MemoryInitOp::Set { .. } - | MemoryInitOp::SetRef { .. } => self.build_set(body, source, operation, pointee_info), + | MemoryInitOp::SetRef { .. } => self.build_set( + tcx, + body, + source, + operation, + pointee_info, + skip_first, + autogenerated_bbs, + ), MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => { unreachable!() } @@ -214,10 +235,13 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { /// 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, + autogenerated_bbs: &mut HashSet, ) { let ret_place = Place { local: body.new_local(Ty::bool_ty(), source.span(body.blocks()), Mutability::Not), @@ -226,8 +250,10 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { // 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; + let ptr_operand = operation.mk_operand(body, &mut statements, source); - let terminator = match pointee_info.layout() { + match pointee_info.layout() { PointeeLayout::Sized { 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 @@ -247,11 +273,11 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { _ => unreachable!(), }; let is_ptr_initialized_instance = resolve_mem_init_fn( - get_mem_init_fn_def(self.tcx, diagnostic, &mut self.mem_init_fn_cache), + get_mem_init_fn_def(tcx, diagnostic, &mut self.mem_init_fn_cache), layout.len(), *pointee_info.ty(), ); - Terminator { + terminator = Terminator { kind: TerminatorKind::Call { func: Operand::Copy(Place::from(body.new_local( is_ptr_initialized_instance.ty(), @@ -264,7 +290,7 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { 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. @@ -278,13 +304,13 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { _ => unreachable!(), }; let is_ptr_initialized_instance = resolve_mem_init_fn( - get_mem_init_fn_def(self.tcx, diagnostic, &mut self.mem_init_fn_cache), + get_mem_init_fn_def(tcx, diagnostic, &mut self.mem_init_fn_cache), element_layout.len(), slicee_ty, ); let layout_operand = mk_layout_operand(body, &mut statements, source, &element_layout); - Terminator { + terminator = Terminator { kind: TerminatorKind::Call { func: Operand::Copy(Place::from(body.new_local( is_ptr_initialized_instance.ty(), @@ -297,24 +323,24 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { unwind: UnwindAction::Terminate, }, span: source.span(body.blocks()), - } + }; } PointeeLayout::TraitObject => { - collect_skipped(operation.position(), source, body, &mut self.skip_first); + collect_skipped(operation.position(), source, body, 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); + self.inject_assert_false(tcx, body, source, operation.position(), reason); return; } }; // Construct the basic block and insert it into the body. - collect_skipped(operation.position(), source, body, &mut self.skip_first); + collect_skipped(operation.position(), source, body, skip_first); body.insert_bb(BasicBlock { statements, terminator }, source, operation.position()); - self.autogenerated_bbs.insert(body.blocks().len() - 1); + 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); + collect_skipped(operation.position(), source, body, skip_first); let operand_ty = match &operation { MemoryInitOp::Check { operand } | MemoryInitOp::CheckSliceChunk { operand, .. } @@ -322,7 +348,7 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { _ => unreachable!(), }; body.insert_check( - self.tcx, + tcx, &self.check_type, source, operation.position(), @@ -337,22 +363,27 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { /// 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, + autogenerated_bbs: &mut HashSet, ) { let ret_place = Place { local: body.new_local(Ty::new_tuple(&[]), source.span(body.blocks()), Mutability::Not), projection: vec![], }; - // 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; + let ptr_operand = operation.mk_operand(body, &mut statements, source); let value = operation.expect_value(); - let terminator = match pointee_info.layout() { + + match pointee_info.layout() { PointeeLayout::Sized { 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 @@ -388,11 +419,11 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { _ => unreachable!(), }; let set_ptr_initialized_instance = resolve_mem_init_fn( - get_mem_init_fn_def(self.tcx, diagnostic, &mut self.mem_init_fn_cache), + get_mem_init_fn_def(tcx, diagnostic, &mut self.mem_init_fn_cache), layout.len(), *pointee_info.ty(), ); - Terminator { + terminator = Terminator { kind: TerminatorKind::Call { func: Operand::Copy(Place::from(body.new_local( set_ptr_initialized_instance.ty(), @@ -405,7 +436,7 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { 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. @@ -419,13 +450,13 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { _ => unreachable!(), }; let set_ptr_initialized_instance = resolve_mem_init_fn( - get_mem_init_fn_def(self.tcx, diagnostic, &mut self.mem_init_fn_cache), + get_mem_init_fn_def(tcx, diagnostic, &mut self.mem_init_fn_cache), element_layout.len(), slicee_ty, ); let layout_operand = mk_layout_operand(body, &mut statements, source, &element_layout); - Terminator { + terminator = Terminator { kind: TerminatorKind::Call { func: Operand::Copy(Place::from(body.new_local( set_ptr_initialized_instance.ty(), @@ -446,16 +477,16 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> { 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); + collect_skipped(operation.position(), source, body, skip_first); body.insert_bb(BasicBlock { statements, terminator }, source, operation.position()); - self.autogenerated_bbs.insert(body.blocks().len() - 1); + autogenerated_bbs.insert(body.blocks().len() - 1); } fn inject_assert_false( 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 37f1d94ed744..af2753ea7175 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,16 +62,14 @@ impl TransformPass for UninitPass { } // Call a helper that performs the actual instrumentation. - let (instrumentation_added, body) = UninitInstrumenter::run( - new_body.into(), - tcx, - instance, - self.check_type.clone(), - &mut self.mem_init_fn_cache, - CheckUninitVisitor::new(), - ); + 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()); - (changed || instrumentation_added, body) + (changed || instrumentation_added, body.into()) } } From 5626f6b524b83777ad5d67ca1e10b40dddc618fb Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 14 Aug 2024 08:52:37 -0700 Subject: [PATCH 12/13] Revert "Make sure we short-circuit correctly when encountering ZSTs in the predicates" This reverts commit e3993f96f3e5977b8403c72c835258937b683817. --- .../src/kani_middle/transform/kani_intrinsics.rs | 15 --------------- 1 file changed, 15 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..b4b7568f6f94 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -205,21 +205,6 @@ 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( From 3bfb417c4d4813fab5b91b11d0a280e024353104 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 14 Aug 2024 08:52:45 -0700 Subject: [PATCH 13/13] Revert "Avoid corner-cases by grouping instrumentation into basic blocks" This reverts commit 130cfd56e75822ec8dd7f3e9da2d2bbf30f952a0. --- .../src/kani_middle/transform/body.rs | 16 +- .../kani_middle/transform/check_uninit/mod.rs | 295 ++++++------------ .../check_uninit/relevant_instruction.rs | 65 +--- .../kani_middle/transform/kani_intrinsics.rs | 120 +++---- 4 files changed, 165 insertions(+), 331 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index e050084eaf44..fa4e5eb1ad97 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 - // provided by the caller. + // Make the terminator at `source` point at the new block, + // the terminator of which is a simple Goto instruction. 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); - // 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); + // 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; // Update the source to point at the terminator. *bb = new_bb_idx; self.blocks.push(BasicBlock { statements: vec![], terminator: new_term }); @@ -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/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs index 5299f8f2679f..5c7194f879d1 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, BasicBlock, BasicBlockIdx, ConstOperand, Mutability, - Operand, Place, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, UnwindAction, + mono::Instance, AggregateKind, BasicBlockIdx, ConstOperand, Mutability, Operand, Place, + Rvalue, }, ty::{FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Ty, TyConst, TyKind, UintTy}, CrateDef, @@ -94,32 +94,17 @@ impl<'a> UninitInstrumenter<'a> { // the source instruction. let mut skip_first = HashSet::new(); - // 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. - let mut autogenerated_bbs = 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() { - // Skip instrumentation of autogenerated blocks. - if !autogenerated_bbs.contains(&bb_idx) { - 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, - &mut autogenerated_bbs, - ); - } - } - bb_idx += 1; + 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; + }; } (orig_len != body.blocks().len(), body) } @@ -131,28 +116,13 @@ impl<'a> UninitInstrumenter<'a> { body: &mut MutableBody, instruction: InitRelevantInstruction, skip_first: &mut HashSet, - autogenerated_bbs: &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, - autogenerated_bbs, - ); + self.build_check_for_operation(tcx, body, &mut source, operation, skip_first); } for operation in instruction.after_instruction { - self.build_check_for_operation( - tcx, - body, - &mut source, - operation, - skip_first, - autogenerated_bbs, - ); + self.build_check_for_operation(tcx, body, &mut source, operation, skip_first); } } @@ -164,22 +134,18 @@ impl<'a> UninitInstrumenter<'a> { source: &mut SourceInstruction, operation: MemoryInitOp, skip_first: &mut HashSet, - autogenerated_bbs: &mut HashSet, ) { if let MemoryInitOp::Unsupported { reason } | MemoryInitOp::TriviallyUnsafe { reason } = &operation { - // If the operation is unsupported or trivially accesses uninitialized memory, encode - // the check as `assert!(false)`. - collect_skipped(operation.position(), source, body, skip_first); + collect_skipped(&operation, body, skip_first); self.inject_assert_false(tcx, body, source, operation.position(), reason); return; }; - 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_info = { + let ptr_operand = operation.mk_operand(body, source); + let ptr_operand_ty = ptr_operand.ty(body.locals()).unwrap(); let pointee_ty = match ptr_operand_ty.kind() { TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) => pointee_ty, _ => { @@ -188,47 +154,34 @@ 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.position(), source, body, skip_first); + collect_skipped(&operation, body, skip_first); self.inject_assert_false(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_info, - skip_first, - autogenerated_bbs, - ), + | MemoryInitOp::CheckRef { .. } => { + self.build_get_and_check(tcx, body, source, operation, pointee_ty_info, skip_first) + } MemoryInitOp::SetSliceChunk { .. } | MemoryInitOp::Set { .. } - | MemoryInitOp::SetRef { .. } => self.build_set( - tcx, - body, - source, - operation, - pointee_info, - skip_first, - autogenerated_bbs, - ), + | MemoryInitOp::SetRef { .. } => { + self.build_set(tcx, body, source, operation, pointee_ty_info, skip_first) + } MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => { unreachable!() } - }; + } } /// Inject a load from memory initialization state and an assertion that all non-padding bytes @@ -241,21 +194,15 @@ impl<'a> UninitInstrumenter<'a> { operation: MemoryInitOp, pointee_info: PointeeInfo, skip_first: &mut HashSet, - autogenerated_bbs: &mut HashSet, ) { let ret_place = Place { local: body.new_local(Ty::bool_ty(), source.span(body.blocks()), Mutability::Not), projection: vec![], }; - // 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; - - let ptr_operand = operation.mk_operand(body, &mut statements, source); + let ptr_operand = operation.mk_operand(body, source); match pointee_info.layout() { PointeeLayout::Sized { layout } => { - let layout_operand = mk_layout_operand(body, &mut statements, source, &layout); + let layout_operand = mk_layout_operand(body, source, operation.position(), &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 { @@ -277,20 +224,14 @@ impl<'a> UninitInstrumenter<'a> { layout.len(), *pointee_info.ty(), ); - terminator = 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()), - }; + collect_skipped(&operation, body, skip_first); + body.insert_call( + &is_ptr_initialized_instance, + source, + operation.position(), + args, + ret_place.clone(), + ); } PointeeLayout::Slice { element_layout } => { // Since `str`` is a separate type, need to differentiate between [T] and str. @@ -309,38 +250,27 @@ impl<'a> UninitInstrumenter<'a> { slicee_ty, ); let layout_operand = - mk_layout_operand(body, &mut statements, source, &element_layout); - terminator = 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()), - }; + 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(), + ); } PointeeLayout::TraitObject => { - collect_skipped(operation.position(), source, body, skip_first); + collect_skipped(&operation, body, skip_first); let reason = "Kani does not support reasoning about memory initialization of pointers to trait objects."; self.inject_assert_false(tcx, body, source, operation.position(), reason); return; } }; - // Construct the basic block and insert it into the body. - collect_skipped(operation.position(), source, body, skip_first); - body.insert_bb(BasicBlock { statements, terminator }, source, operation.position()); - 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, skip_first); + // Make sure all non-padding bytes are initialized. + collect_skipped(&operation, body, skip_first); + // Find the real operand type for a good error message. let operand_ty = match &operation { MemoryInitOp::Check { operand } | MemoryInitOp::CheckSliceChunk { operand, .. } @@ -369,23 +299,17 @@ impl<'a> UninitInstrumenter<'a> { operation: MemoryInitOp, pointee_info: PointeeInfo, skip_first: &mut HashSet, - autogenerated_bbs: &mut HashSet, ) { let ret_place = Place { local: body.new_local(Ty::new_tuple(&[]), source.span(body.blocks()), Mutability::Not), projection: vec![], }; - // 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; - - let ptr_operand = operation.mk_operand(body, &mut statements, source); + let ptr_operand = operation.mk_operand(body, source); let value = operation.expect_value(); match pointee_info.layout() { PointeeLayout::Sized { layout } => { - let layout_operand = mk_layout_operand(body, &mut statements, source, &layout); + let layout_operand = mk_layout_operand(body, source, operation.position(), &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 { @@ -423,20 +347,14 @@ impl<'a> UninitInstrumenter<'a> { layout.len(), *pointee_info.ty(), ); - terminator = 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()), - }; + collect_skipped(&operation, body, skip_first); + body.insert_call( + &set_ptr_initialized_instance, + source, + operation.position(), + args, + ret_place, + ); } PointeeLayout::Slice { element_layout } => { // Since `str`` is a separate type, need to differentiate between [T] and str. @@ -455,38 +373,28 @@ impl<'a> UninitInstrumenter<'a> { slicee_ty, ); let layout_operand = - mk_layout_operand(body, &mut statements, source, &element_layout); - terminator = 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()), - }; + 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, + ); } 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, skip_first); - body.insert_bb(BasicBlock { statements, terminator }, source, operation.position()); - autogenerated_bbs.insert(body.blocks().len() - 1); } fn inject_assert_false( @@ -522,43 +430,36 @@ 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 { - 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![] }) + 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![], + }) } /// 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()) - { +fn collect_skipped(operation: &MemoryInitOp, body: &MutableBody, skip_first: &mut HashSet) { + if operation.position() == InsertPosition::Before { let new_bb_idx = body.blocks().len(); skip_first.insert(new_bb_idx); } diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs b/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs index dbee561df516..3bc5b534a23b 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,10 +5,7 @@ //! character of instrumentation needed. use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; -use stable_mir::{ - mir::{Mutability, Operand, Place, Rvalue, Statement, StatementKind}, - ty::Ty, -}; +use stable_mir::mir::{Mutability, Operand, Place, Rvalue}; use strum_macros::AsRefStr; /// Memory initialization operations: set or get memory initialization state for a given pointer. @@ -42,57 +39,27 @@ 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, - statements: &mut Vec, - source: &mut SourceInstruction, - ) -> Operand { + pub fn mk_operand(&self, body: &mut MutableBody, 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, .. } => { - 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() + 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![], + }) } 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 b4b7568f6f94..cc748c39a7f5 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::{ - BasicBlock, BinOp, Body, ConstOperand, Mutability, Operand, Place, Rvalue, Statement, - StatementKind, Terminator, TerminatorKind, UnwindAction, RETURN_LOCAL, + BinOp, Body, ConstOperand, Operand, Place, Rvalue, Statement, StatementKind, TerminatorKind, + RETURN_LOCAL, }; use stable_mir::target::MachineInfo; use stable_mir::ty::{FnDef, MirConst, RigidTy, Ty, TyKind, UintTy}; @@ -164,40 +164,30 @@ 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 source = SourceInstruction::Terminator { bb: 0 }; + 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); - // Short-circut if uninitialized memory checks are not enabled. if !self.arguments.ub_check.contains(&ExtraChecks::Uninit) { - // 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, - ); + // Short-circut if uninitialized memory checks are not enabled. 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) => { @@ -216,28 +206,18 @@ impl IntrinsicGeneratorPass { layout.len(), *pointee_info.ty(), ); - 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, + let layout_operand = mk_layout_operand( + &mut new_body, + &mut terminator, + InsertPosition::Before, + &layout, + ); + new_body.insert_call( + &is_ptr_initialized_instance, + &mut terminator, InsertPosition::Before, + vec![Operand::Copy(Place::from(1)), layout_operand], + Place::from(ret_var), ); } PointeeLayout::Slice { element_layout } => { @@ -258,45 +238,35 @@ impl IntrinsicGeneratorPass { ); let layout_operand = mk_layout_operand( &mut new_body, - &mut statements, - &mut source, + &mut terminator, + InsertPosition::Before, &element_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, + new_body.insert_call( + &is_ptr_initialized_instance, + &mut terminator, 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: source.span(new_body.blocks()), + span, user_ty: None, })); - let result = - new_body.insert_assignment(rvalue, &mut source, InsertPosition::Before); + let result = new_body.insert_assignment( + rvalue, + &mut terminator, + InsertPosition::Before, + ); let reason: &str = "Kani does not support reasoning about memory initialization of pointers to trait objects."; new_body.insert_check( tcx, &self.check_type, - &mut source, + &mut terminator, InsertPosition::Before, result, &reason, @@ -308,18 +278,18 @@ impl IntrinsicGeneratorPass { // We failed to retrieve the type layout. let rvalue = Rvalue::Use(Operand::Constant(ConstOperand { const_: MirConst::from_bool(false), - span: source.span(new_body.blocks()), + span, user_ty: None, })); let result = - new_body.insert_assignment(rvalue, &mut source, InsertPosition::Before); + new_body.insert_assignment(rvalue, &mut terminator, 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 source, + &mut terminator, InsertPosition::Before, result, &reason,