Skip to content

Commit

Permalink
Better explanations and extra functionality in MutableBody
Browse files Browse the repository at this point in the history
  • Loading branch information
@artemagvanian
artemagvanian committed Jul 24, 2024
1 parent 1b1a9b6 commit ade0550
Show file tree
Hide file tree
Showing 4 changed files with 119 additions and 72 deletions.
151 changes: 99 additions & 52 deletions kani-compiler/src/kani_middle/transform/body.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -88,16 +88,20 @@ impl MutableBody {

pub fn new_str_operand(&mut self, msg: &str, span: Span) -> Operand {
let literal = MirConst::from_str(msg);
Operand::Constant(ConstOperand { span, user_ty: None, const_: literal })
self.new_const_operand(literal, span)
}

pub fn new_const_operand(&mut self, val: u128, uint_ty: UintTy, span: Span) -> Operand {
pub fn new_uint_operand(&mut self, val: u128, uint_ty: UintTy, span: Span) -> Operand {
let literal = MirConst::try_from_uint(val, uint_ty).unwrap();
self.new_const_operand(literal, span)
}

fn new_const_operand(&mut self, literal: MirConst, span: Span) -> Operand {
Operand::Constant(ConstOperand { span, user_ty: None, const_: literal })
}

/// Create a raw pointer of `*mut type` and return a new local where that value is stored.
pub fn new_cast_ptr(
pub fn new_ptr_cast(
&mut self,
from: Operand,
pointee_ty: Ty,
Expand Down Expand Up @@ -128,7 +132,7 @@ impl MutableBody {

/// Add a new assignment.
///
/// Return local where the result is saved.
/// Return the local where the result is saved.
pub fn new_assignment(
&mut self,
rvalue: Rvalue,
Expand All @@ -146,9 +150,10 @@ impl MutableBody {
/// Add a new assert to the basic block indicated by the given index.
///
/// The new assertion will have the same span as the source instruction, and the basic block
/// will be split. The source instruction will be adjusted to point to the first instruction in
/// the new basic block.
pub fn add_check(
/// will be split. If `InsertPosition` is `InsertPosition::Before`, `source` will point to the
/// same instruction as before. If `InsertPosition` is `InsertPosition::After`, `source` will
/// point to the new terminator.
pub fn new_check(
&mut self,
tcx: TyCtxt,
check_type: &CheckType,
Expand Down Expand Up @@ -183,7 +188,7 @@ impl MutableBody {
unwind: UnwindAction::Terminate,
};
let terminator = Terminator { kind, span };
self.split_bb(source, position, terminator);
self.insert_terminator(source, position, terminator);
}
CheckType::Panic | CheckType::NoCore => {
tcx.sess
Expand All @@ -199,10 +204,11 @@ impl MutableBody {

/// Add a new call to the basic block indicated by the given index.
///
/// The new call will have the same span as the source instruction, and the basic block
/// will be split. The source instruction will be adjusted to point to the first instruction in
/// the new basic block.
pub fn add_call(
/// The new call will have the same span as the source instruction, and the basic block will be
/// split. If `InsertPosition` is `InsertPosition::Before`, `source` will point to the same
/// instruction as before. If `InsertPosition` is `InsertPosition::After`, `source` will point
/// to the new terminator.
pub fn new_call(
&mut self,
callee: &Instance,
source: &mut SourceInstruction,
Expand All @@ -222,13 +228,14 @@ impl MutableBody {
unwind: UnwindAction::Terminate,
};
let terminator = Terminator { kind, span };
self.split_bb(source, position, terminator);
self.insert_terminator(source, position, terminator);
}

/// Split a basic block and use the new terminator in the basic block that was split.
///
/// The source is updated to point to the same instruction which is now in the new basic block.
pub fn split_bb(
/// Split a basic block and use the new terminator in the basic block that was split. If
/// `InsertPosition` is `InsertPosition::Before`, `source` will point to the same instruction as
/// before. If `InsertPosition` is `InsertPosition::After`, `source` will point to the new
/// terminator.
fn split_bb(
&mut self,
source: &mut SourceInstruction,
position: InsertPosition,
Expand All @@ -245,6 +252,7 @@ impl MutableBody {
}

/// Split a basic block right before the source location.
/// `source` will point to the same instruction as before after the function is done.
fn split_bb_before(&mut self, source: &mut SourceInstruction, new_term: Terminator) {
let new_bb_idx = self.blocks.len();
let (idx, bb) = match source {
Expand All @@ -268,46 +276,77 @@ impl MutableBody {
}

/// Split a basic block right after the source location.
/// `source` will point to the new terminator after the function is done.
fn split_bb_after(&mut self, source: &mut SourceInstruction, mut new_term: Terminator) {
let new_bb_idx = self.blocks.len();
match source {
// Split the current block after the statement located at `source`
// and move the remaining statements into the new one.
SourceInstruction::Statement { idx, bb } => {
let (orig_idx, orig_bb) = (*idx, *bb);
*idx = 0;
*bb = new_bb_idx;
let old_term = mem::replace(&mut self.blocks[orig_bb].terminator, new_term);
let bb_stmts = &mut self.blocks[orig_bb].statements;
let remaining = bb_stmts.split_off(orig_idx + 1);
let new_bb = BasicBlock { statements: remaining, terminator: old_term };
self.blocks.push(new_bb);
// 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.
SourceInstruction::Terminator { bb } => {
let current_terminator = &mut self.blocks.get_mut(*bb).unwrap().terminator;
// Kani can only instrument function calls like this.
match (&mut current_terminator.kind, &mut new_term.kind) {
(
TerminatorKind::Call { target: Some(target_bb), .. },
TerminatorKind::Call { target: Some(new_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 current poisition.
*bb = new_bb_idx;
self.blocks.push(BasicBlock { statements: vec![], terminator: new_term });
}
_ => unimplemented!("Kani can only split blocks after calls."),
};
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;
// Update the source to point at the terminator.
*bb = new_bb_idx;
self.blocks.push(BasicBlock { statements: vec![], terminator: new_term });
}
};
}

/// Insert statement before or after the source instruction and update the source as needed.
/// Insert basic block before or after the source instruction and update `source` accordingly. If
/// `InsertPosition` is `InsertPosition::Before`, `source` will point to the same instruction as
/// before. If `InsertPosition` is `InsertPosition::After`, `source` will point to the
/// terminator of the newly inserted basic block.
pub fn insert_bb(
&mut self,
mut bb: BasicBlock,
source: &mut SourceInstruction,
position: InsertPosition,
) {
// Splitting adds 1 block, so the added block index is len + 1;
let split_bb_idx = self.blocks().len();
let inserted_bb_idx = self.blocks().len() + 1;
// Update the terminator of the basic block to point at the remaining part of the split
// basic block.
let target = get_mut_target_ref(&mut bb.terminator);
*target = split_bb_idx;
let new_term = Terminator {
kind: TerminatorKind::Goto { target: inserted_bb_idx },
span: source.span(&self.blocks),
};
self.split_bb(source, position, new_term);
self.blocks.push(bb);
}

pub fn insert_terminator(
&mut self,
source: &mut SourceInstruction,
position: InsertPosition,
terminator: Terminator,
) {
self.split_bb(source, position, terminator);
}

/// Insert statement before or after the source instruction and update the source as needed. If
/// `InsertPosition` is `InsertPosition::Before`, `source` will point to the same instruction as
/// before. If `InsertPosition` is `InsertPosition::After`, `source` will point to the
/// newly inserted statement.
pub fn insert_stmt(
&mut self,
new_stmt: Statement,
Expand Down Expand Up @@ -338,22 +377,18 @@ impl MutableBody {
SourceInstruction::Terminator { bb } => {
// Create a new basic block, as we need to append a statement after the terminator.
let current_terminator = &mut self.blocks.get_mut(*bb).unwrap().terminator;
// Kani can only instrument function calls in this way.
match &mut current_terminator.kind {
TerminatorKind::Call { target: Some(target_bb), .. } => {
*source = SourceInstruction::Statement { idx: 0, bb: new_bb_idx };
let new_bb = BasicBlock {
statements: vec![new_stmt],
terminator: Terminator {
kind: TerminatorKind::Goto { target: *target_bb },
span,
},
};
*target_bb = new_bb_idx;
self.blocks.push(new_bb);
}
_ => unimplemented!("Kani can only insert statements after calls."),
// Update target of the terminator.
let target_bb = get_mut_target_ref(current_terminator);
*source = SourceInstruction::Statement { idx: 0, bb: new_bb_idx };
let new_bb = BasicBlock {
statements: vec![new_stmt],
terminator: Terminator {
kind: TerminatorKind::Goto { target: *target_bb },
span,
},
};
*target_bb = new_bb_idx;
self.blocks.push(new_bb);
}
}
}
Expand Down Expand Up @@ -574,3 +609,15 @@ pub trait MutMirVisitor {
}
}
}

fn get_mut_target_ref(terminator: &mut Terminator) -> &mut BasicBlockIdx {
match &mut terminator.kind {
TerminatorKind::Assert { target, .. }
| TerminatorKind::Drop { target, .. }
| TerminatorKind::Goto { target }
| TerminatorKind::Call { target: Some(target), .. } => target,
_ => unimplemented!(
"Kani can only insert instructions after terminators that have a `target` field."
),
}
}
14 changes: 7 additions & 7 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 @@ -230,7 +230,7 @@ impl UninitPass {
*pointee_info.ty(),
);
collect_skipped(&operation, body, skip_first);
body.add_call(
body.new_call(
&is_ptr_initialized_instance,
source,
operation.position(),
Expand All @@ -257,7 +257,7 @@ impl UninitPass {
let layout_operand =
mk_layout_operand(body, source, operation.position(), &element_layout);
collect_skipped(&operation, body, skip_first);
body.add_call(
body.new_call(
&is_ptr_initialized_instance,
source,
operation.position(),
Expand All @@ -276,7 +276,7 @@ impl UninitPass {
// Make sure all non-padding bytes are initialized.
collect_skipped(&operation, body, skip_first);
let ptr_operand_ty = ptr_operand.ty(body.locals()).unwrap();
body.add_check(
body.new_check(
tcx,
&self.check_type,
source,
Expand Down Expand Up @@ -345,7 +345,7 @@ impl UninitPass {
*pointee_info.ty(),
);
collect_skipped(&operation, body, skip_first);
body.add_call(
body.new_call(
&set_ptr_initialized_instance,
source,
operation.position(),
Expand All @@ -372,7 +372,7 @@ impl UninitPass {
let layout_operand =
mk_layout_operand(body, source, operation.position(), &element_layout);
collect_skipped(&operation, body, skip_first);
body.add_call(
body.new_call(
&set_ptr_initialized_instance,
source,
operation.position(),
Expand Down Expand Up @@ -409,7 +409,7 @@ impl UninitPass {
user_ty: None,
}));
let result = body.new_assignment(rvalue, source, position);
body.add_check(tcx, &self.check_type, source, position, result, reason);
body.new_check(tcx, &self.check_type, source, position, result, reason);
}
}

Expand Down Expand Up @@ -531,7 +531,7 @@ fn inject_memory_init_setup(
)
.unwrap();

new_body.add_call(
new_body.new_call(
&memory_initialization_init,
&mut source,
InsertPosition::Before,
Expand Down
16 changes: 8 additions & 8 deletions kani-compiler/src/kani_middle/transform/check_values.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,7 @@ impl ValidValuePass {
let result = build_limits(body, &range, rvalue_ptr.clone(), &mut source);
let msg =
format!("Undefined Behavior: Invalid value of type `{target_ty}`",);
body.add_check(
body.new_check(
tcx,
&self.check_type,
&mut source,
Expand All @@ -106,7 +106,7 @@ impl ValidValuePass {
let result = build_limits(body, &range, rvalue.clone(), &mut source);
let msg =
format!("Undefined Behavior: Invalid value of type `{pointee_ty}`",);
body.add_check(
body.new_check(
tcx,
&self.check_type,
&mut source,
Expand Down Expand Up @@ -140,7 +140,7 @@ impl ValidValuePass {
user_ty: None,
}));
let result = body.new_assignment(rvalue, source, InsertPosition::Before);
body.add_check(tcx, &self.check_type, source, InsertPosition::Before, result, reason);
body.new_check(tcx, &self.check_type, source, InsertPosition::Before, result, reason);
}
}

Expand Down Expand Up @@ -771,18 +771,18 @@ pub fn build_limits(
let span = source.span(body.blocks());
debug!(?req, ?rvalue_ptr, ?span, "build_limits");
let primitive_ty = uint_ty(req.size.bytes());
let start_const = body.new_const_operand(req.valid_range.start, primitive_ty, span);
let end_const = body.new_const_operand(req.valid_range.end, primitive_ty, span);
let start_const = body.new_uint_operand(req.valid_range.start, primitive_ty, span);
let end_const = body.new_uint_operand(req.valid_range.end, primitive_ty, span);
let orig_ptr = if req.offset != 0 {
let start_ptr = move_local(body.new_assignment(rvalue_ptr, source, InsertPosition::Before));
let byte_ptr = move_local(body.new_cast_ptr(
let byte_ptr = move_local(body.new_ptr_cast(
start_ptr,
Ty::unsigned_ty(UintTy::U8),
Mutability::Not,
source,
InsertPosition::Before,
));
let offset_const = body.new_const_operand(req.offset as _, UintTy::Usize, span);
let offset_const = body.new_uint_operand(req.offset as _, UintTy::Usize, span);
let offset = move_local(body.new_assignment(
Rvalue::Use(offset_const),
source,
Expand All @@ -798,7 +798,7 @@ pub fn build_limits(
} else {
move_local(body.new_assignment(rvalue_ptr, source, InsertPosition::Before))
};
let value_ptr = body.new_cast_ptr(
let value_ptr = body.new_ptr_cast(
orig_ptr,
Ty::unsigned_ty(primitive_ty),
Mutability::Not,
Expand Down
Loading

0 comments on commit ade0550

Please sign in to comment.