Skip to content

Commit

Permalink
Merge branch 'main' into uninit-unions
Browse files Browse the repository at this point in the history
  • Loading branch information
@artemagvanian
artemagvanian committed Aug 22, 2024
2 parents 2f9acc5 + 0ed9a62 commit acf6d91
Show file tree
Hide file tree
Showing 8 changed files with 430 additions and 439 deletions.
6 changes: 1 addition & 5 deletions kani-compiler/src/kani_middle/transform/body.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -484,7 +484,7 @@ impl CheckType {
}

/// We store the index of an instruction to avoid borrow checker issues and unnecessary copies.
#[derive(Copy, Clone, Debug)]
#[derive(Copy, Clone, Debug, PartialEq, Eq)]
pub enum SourceInstruction {
Statement { idx: usize, bb: BasicBlockIdx },
Terminator { bb: BasicBlockIdx },
Expand All @@ -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<Instance> {
Expand Down
88 changes: 47 additions & 41 deletions kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,20 +18,15 @@ use rustc_middle::ty::TyCtxt;
use stable_mir::mir::{
mono::Instance,
visit::{Location, PlaceContext},
BasicBlockIdx, MirVisitor, Operand, Place, Rvalue, Statement, Terminator,
MirVisitor, Operand, Place, Rvalue, Statement, Terminator,
};
use std::collections::HashSet;

pub struct InstrumentationVisitor<'a, 'tcx> {
/// Whether we should skip the next instruction, since it might've been instrumented already.
/// When we instrument an instruction, we partition the basic block, and the instruction that
/// may trigger UB becomes the first instruction of the basic block, which we need to skip
/// later.
skip_next: bool,
/// The instruction being visited at a given point.
current: SourceInstruction,
/// The target instruction that should be verified.
pub target: Option<InitRelevantInstruction>,
/// All target instructions in the body.
targets: Vec<InitRelevantInstruction>,
/// Current analysis target, eventually needs to be added to a list of all targets.
current_target: InitRelevantInstruction,
/// Aliasing analysis data.
points_to: &'a PointsToGraph<'tcx>,
/// The list of places we should be looking for, ignoring others
Expand All @@ -41,17 +36,16 @@ pub struct InstrumentationVisitor<'a, 'tcx> {
}

impl<'a, 'tcx> TargetFinder for InstrumentationVisitor<'a, 'tcx> {
fn find_next(
&mut self,
body: &MutableBody,
bb: BasicBlockIdx,
skip_first: bool,
) -> Option<InitRelevantInstruction> {
self.skip_next = skip_first;
self.current = SourceInstruction::Statement { idx: 0, bb };
self.target = None;
self.visit_basic_block(&body.blocks()[bb]);
self.target.clone()
fn find_all(mut self, body: &MutableBody) -> Vec<InitRelevantInstruction> {
for (bb_idx, bb) in body.blocks().iter().enumerate() {
self.current_target = InitRelevantInstruction {
source: SourceInstruction::Statement { idx: 0, bb: bb_idx },
before_instruction: vec![],
after_instruction: vec![],
};
self.visit_basic_block(bb);
}
self.targets
}
}

Expand All @@ -63,43 +57,55 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> {
tcx: TyCtxt<'tcx>,
) -> Self {
Self {
skip_next: false,
current: SourceInstruction::Statement { idx: 0, bb: 0 },
target: None,
targets: vec![],
current_target: InitRelevantInstruction {
source: SourceInstruction::Statement { idx: 0, bb: 0 },
before_instruction: vec![],
after_instruction: vec![],
},
points_to,
analysis_targets,
current_instance,
tcx,
}
}

fn push_target(&mut self, source_op: MemoryInitOp) {
let target = self.target.get_or_insert_with(|| InitRelevantInstruction {
source: self.current,
after_instruction: vec![],
before_instruction: vec![],
});
target.push_operation(source_op);
self.current_target.push_operation(source_op);
}
}

impl<'a, 'tcx> MirVisitor for InstrumentationVisitor<'a, 'tcx> {
fn visit_statement(&mut self, stmt: &Statement, location: Location) {
if self.skip_next {
self.skip_next = false;
} else if self.target.is_none() {
// Check all inner places.
self.super_statement(stmt, location);
}
self.super_statement(stmt, location);
// Switch to the next statement.
let SourceInstruction::Statement { idx, bb } = self.current else { unreachable!() };
self.current = SourceInstruction::Statement { idx: idx + 1, bb };
if let SourceInstruction::Statement { idx, bb } = self.current_target.source {
self.targets.push(self.current_target.clone());
self.current_target = InitRelevantInstruction {
source: SourceInstruction::Statement { idx: idx + 1, bb },
after_instruction: vec![],
before_instruction: vec![],
};
} else {
unreachable!()
}
}

fn visit_terminator(&mut self, term: &Terminator, location: Location) {
if !(self.skip_next || self.target.is_some()) {
self.current = SourceInstruction::Terminator { bb: self.current.bb() };
self.super_terminator(term, location);
if let SourceInstruction::Statement { bb, .. } = self.current_target.source {
// We don't have to push the previous target, since it already happened in the statement
// handling code.
self.current_target = InitRelevantInstruction {
source: SourceInstruction::Terminator { bb },
after_instruction: vec![],
before_instruction: vec![],
};
} else {
unreachable!()
}
self.super_terminator(term, location);
// Push the current target from the terminator onto the list.
self.targets.push(self.current_target.clone());
}

fn visit_rvalue(&mut self, rvalue: &Rvalue, location: Location) {
Expand Down
91 changes: 13 additions & 78 deletions kani-compiler/src/kani_middle/transform/check_uninit/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,13 +13,13 @@ use rustc_middle::ty::TyCtxt;
use rustc_smir::rustc_internal;
use stable_mir::{
mir::{
mono::Instance, AggregateKind, BasicBlock, BasicBlockIdx, Body, ConstOperand, Mutability,
Operand, Place, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, UnwindAction,
mono::Instance, AggregateKind, BasicBlock, Body, ConstOperand, Mutability, Operand, Place,
Rvalue, Statement, StatementKind, Terminator, TerminatorKind, UnwindAction,
},
ty::{FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Ty, TyConst, TyKind, UintTy},
CrateDef,
};
use std::collections::{HashMap, HashSet};
use std::collections::HashMap;

pub use delayed_ub::DelayedUbPass;
pub use ptr_uninit::UninitPass;
Expand All @@ -32,12 +32,7 @@ mod ty_layout;

/// Trait that the instrumentation target providers must implement to work with the instrumenter.
pub trait TargetFinder {
fn find_next(
&mut self,
body: &MutableBody,
bb: BasicBlockIdx,
skip_first: bool,
) -> Option<InitRelevantInstruction>;
fn find_all(self, body: &MutableBody) -> Vec<InitRelevantInstruction>;
}

// Function bodies of those functions will not be instrumented as not to cause infinite recursion.
Expand All @@ -58,22 +53,6 @@ pub struct UninitInstrumenter<'a, 'tcx> {
/// Used to cache FnDef lookups of injected memory initialization functions.
mem_init_fn_cache: &'a mut HashMap<&'static str, FnDef>,
tcx: TyCtxt<'tcx>,
/// Set of basic block indices for which analyzing first statement should be skipped.
///
/// This is necessary because some checks are inserted before the source instruction, which, in
/// turn, gets moved to the next basic block. Hence, we would not need to look at the
/// instruction again as a part of new basic block. However, if the check is inserted after the
/// source instruction, we still need to look at the first statement of the new basic block, so
/// we need to keep track of which basic blocks were created as a part of injecting checks after
/// the source instruction.
skip_first: HashSet<BasicBlockIdx>,
/// 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<BasicBlockIdx>,
}

impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> {
Expand All @@ -86,13 +65,7 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> {
mem_init_fn_cache: &'a mut HashMap<&'static str, FnDef>,
target_finder: impl TargetFinder,
) -> (bool, Body) {
let mut instrumenter = Self {
check_type,
mem_init_fn_cache,
tcx,
skip_first: HashSet::new(),
autogenerated_bbs: HashSet::new(),
};
let mut instrumenter = Self { check_type, mem_init_fn_cache, tcx };
let body = MutableBody::from(body);
let (changed, new_body) = instrumenter.instrument(body, instance, target_finder);
(changed, new_body.into())
Expand All @@ -104,7 +77,7 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> {
&mut self,
mut body: MutableBody,
instance: Instance,
mut target_finder: impl TargetFinder,
target_finder: impl TargetFinder,
) -> (bool, MutableBody) {
// Need to break infinite recursion when memory initialization checks are inserted, so the
// internal functions responsible for memory initialization are skipped.
Expand All @@ -120,19 +93,9 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> {
}

let orig_len = body.blocks().len();

// Do not cache body.blocks().len() since it will change as we add new checks.
let mut bb_idx = 0;
while bb_idx < body.blocks().len() {
// Skip instrumentation of autogenerated blocks.
if !self.autogenerated_bbs.contains(&bb_idx) {
if let Some(candidate) =
target_finder.find_next(&body, bb_idx, self.skip_first.contains(&bb_idx))
{
self.build_check_for_instruction(&mut body, candidate);
}
}
bb_idx += 1;
for instruction in target_finder.find_all(&body).into_iter().rev() {
let source = instruction.source;
self.build_check_for_instruction(&mut body, instruction, source);
}
(orig_len != body.blocks().len(), body)
}
Expand All @@ -142,8 +105,8 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> {
&mut self,
body: &mut MutableBody,
instruction: InitRelevantInstruction,
mut source: SourceInstruction,
) {
let mut source = instruction.source;
for operation in instruction.before_instruction {
self.build_check_for_operation(body, &mut source, operation);
}
Expand All @@ -164,7 +127,6 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> {
{
// If the operation is unsupported or trivially accesses uninitialized memory, encode
// the check as `assert!(false)`.
collect_skipped(operation.position(), source, body, &mut self.skip_first);
self.inject_assert_false(self.tcx, body, source, operation.position(), reason);
return;
};
Expand All @@ -188,7 +150,6 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> {
let reason = format!(
"Kani currently doesn't support checking memory initialization for pointers to `{pointee_ty}.",
);
collect_skipped(operation.position(), source, body, &mut self.skip_first);
self.inject_assert_false(self.tcx, body, source, operation.position(), &reason);
return;
}
Expand Down Expand Up @@ -307,7 +268,6 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> {
}
}
PointeeLayout::TraitObject => {
collect_skipped(operation.position(), source, body, &mut self.skip_first);
let reason = "Kani does not support reasoning about memory initialization of pointers to trait objects.";
self.inject_assert_false(self.tcx, body, source, operation.position(), reason);
return;
Expand All @@ -316,21 +276,17 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> {
// Here we are reading from a pointer to a union.
// TODO: we perhaps need to check that the union at least contains an intersection
// of all layouts initialized.
collect_skipped(operation.position(), source, body, &mut self.skip_first);
let reason = "Interaction between raw pointers and unions is not yet supported.";
self.inject_assert_false(self.tcx, body, source, operation.position(), reason);
return;
}
};

// Construct the basic block and insert it into the body.
collect_skipped(operation.position(), source, body, &mut self.skip_first);
body.insert_bb(BasicBlock { statements, terminator }, source, operation.position());
self.autogenerated_bbs.insert(body.blocks().len() - 1);

// Since the check involves a terminator, we cannot add it to the previously constructed
// basic block. Instead, we insert the check after the basic block.
collect_skipped(operation.position(), source, body, &mut self.skip_first);
let operand_ty = match &operation {
MemoryInitOp::Check { operand }
| MemoryInitOp::CheckSliceChunk { operand, .. }
Expand Down Expand Up @@ -479,7 +435,6 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> {
let union_field = match operation.union_field() {
Some(field) => field,
None => {
collect_skipped(operation.position(), source, body, &mut self.skip_first);
let reason =
"Interaction between raw pointers and unions is not yet supported.";
self.inject_assert_false(
Expand Down Expand Up @@ -526,9 +481,7 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> {
}
};
// Construct the basic block and insert it into the body.
collect_skipped(operation.position(), source, body, &mut self.skip_first);
body.insert_bb(BasicBlock { statements, terminator }, source, operation.position());
self.autogenerated_bbs.insert(body.blocks().len() - 1);
}

/// Copy memory initialization state from one pointer to the other.
Expand All @@ -549,13 +502,13 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> {
layout_size,
*pointee_info.ty(),
);
collect_skipped(operation.position(), source, body, &mut self.skip_first);
let position = operation.position();
let (from, to) = operation.expect_copy_operands();
let count = operation.expect_count();
body.insert_call(
&copy_init_state_instance,
source,
operation.position(),
position,
vec![from, to, count],
ret_place.clone(),
);
Expand All @@ -580,7 +533,7 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> {
layout_size,
*pointee_info.ty(),
);
let (from, to) = operation.mk_assign_union_operands(body, &mut statements, source);
let (from, to) = operation.expect_assign_union_operands(body, &mut statements, source);
let terminator = Terminator {
kind: TerminatorKind::Call {
func: Operand::Copy(Place::from(body.new_local(
Expand All @@ -597,9 +550,7 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> {
};

// Construct the basic block and insert it into the body.
collect_skipped(operation.position(), source, body, &mut self.skip_first);
body.insert_bb(BasicBlock { statements, terminator }, source, operation.position());
self.autogenerated_bbs.insert(body.blocks().len() - 1);
}

fn inject_assert_false(
Expand Down Expand Up @@ -661,22 +612,6 @@ pub fn mk_layout_operand(
Operand::Move(Place { local: result, projection: vec![] })
}

/// If injecting a new call to the function before the current statement, need to skip the original
/// statement when analyzing it as a part of the new basic block.
fn collect_skipped(
position: InsertPosition,
source: &SourceInstruction,
body: &MutableBody,
skip_first: &mut HashSet<usize>,
) {
if position == InsertPosition::Before
|| (position == InsertPosition::After && source.is_terminator())
{
let new_bb_idx = body.blocks().len();
skip_first.insert(new_bb_idx);
}
}

/// Retrieve a function definition by diagnostic string, caching the result.
pub fn get_mem_init_fn_def(
tcx: TyCtxt,
Expand Down
Loading

0 comments on commit acf6d91

Please sign in to comment.