Skip to content

Commit

Permalink
Towards Proving Memory Initialization (#3264)
Browse files Browse the repository at this point in the history 
This PR enables automatic memory initialization proofs for raw pointers
in Kani. This is done without any extra instrumentation from the user.

Currently, due to high memory consumption and only partial support of
pointee types for which memory initialization proofs work, this feature
is gated behind `-Z uninit-checks` flag. Note that because it uses
shadow memory under the hood, programs using this feature need to pass
`-Z ghost-state` flag as well.

This PR is a part of working towards #3300.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Celina G. Val <[email protected]>
  • Loading branch information
@artemagvanian @celinval
artemagvanian and celinval authored Jul 2, 2024
1 parent 2fb97d2 commit d926482
Show file tree
Hide file tree
Showing 41 changed files with 2,500 additions and 53 deletions.
2 changes: 2 additions & 0 deletions kani-compiler/src/args.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -88,4 +88,6 @@ pub enum ExtraChecks {
/// Check pointer validity when casting pointers to references.
/// See https://github.com/model-checking/kani/issues/2975.
PtrToRefCast,
/// Check for using uninitialized memory.
Uninit,
}
22 changes: 22 additions & 0 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -118,6 +118,27 @@ impl<'tcx> GotocCtx<'tcx> {
.typ
.clone();

let shadow_memory_assign = self
.tcx
.all_diagnostic_items(())
.name_to_id
.get(&rustc_span::symbol::Symbol::intern("KaniMemInitShadowMem"))
.map(|attr_id| {
self.tcx
.symbol_name(rustc_middle::ty::Instance::mono(self.tcx, *attr_id))
.name
.to_string()
})
.and_then(|shadow_memory_table| self.symbol_table.lookup(&shadow_memory_table).cloned())
.map(|shadow_memory_symbol| {
vec![Lambda::as_contract_for(
&goto_annotated_fn_typ,
None,
shadow_memory_symbol.to_expr(),
)]
})
.unwrap_or_default();

let assigns = modified_places
.into_iter()
.map(|local| {
Expand All @@ -127,6 +148,7 @@ impl<'tcx> GotocCtx<'tcx> {
self.codegen_place_stable(&local.into(), loc).unwrap().goto_expr.dereference(),
)
})
.chain(shadow_memory_assign)
.collect();

FunctionContract::new(assigns)
Expand Down
178 changes: 158 additions & 20 deletions kani-compiler/src/kani_middle/transform/body.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,13 @@ pub struct MutableBody {
span: Span,
}

/// Denotes whether instrumentation should be inserted before or after the statement.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum InsertPosition {
Before,
After,
}

impl MutableBody {
/// Get the basic blocks of this builder.
pub fn blocks(&self) -> &[BasicBlock] {
Expand Down Expand Up @@ -95,12 +102,13 @@ impl MutableBody {
from: Operand,
pointee_ty: Ty,
mutability: Mutability,
before: &mut SourceInstruction,
source: &mut SourceInstruction,
position: InsertPosition,
) -> Local {
assert!(from.ty(self.locals()).unwrap().kind().is_raw_ptr());
let target_ty = Ty::new_ptr(pointee_ty, mutability);
let rvalue = Rvalue::Cast(CastKind::PtrToPtr, from, target_ty);
self.new_assignment(rvalue, before)
self.new_assignment(rvalue, source, position)
}

/// Add a new assignment for the given binary operation.
Expand All @@ -111,21 +119,27 @@ impl MutableBody {
bin_op: BinOp,
lhs: Operand,
rhs: Operand,
before: &mut SourceInstruction,
source: &mut SourceInstruction,
position: InsertPosition,
) -> Local {
let rvalue = Rvalue::BinaryOp(bin_op, lhs, rhs);
self.new_assignment(rvalue, before)
self.new_assignment(rvalue, source, position)
}

/// Add a new assignment.
///
/// Return local where the result is saved.
pub fn new_assignment(&mut self, rvalue: Rvalue, before: &mut SourceInstruction) -> Local {
let span = before.span(&self.blocks);
pub fn new_assignment(
&mut self,
rvalue: Rvalue,
source: &mut SourceInstruction,
position: InsertPosition,
) -> Local {
let span = source.span(&self.blocks);
let ret_ty = rvalue.ty(&self.locals).unwrap();
let result = self.new_local(ret_ty, span, Mutability::Not);
let stmt = Statement { kind: StatementKind::Assign(Place::from(result), rvalue), span };
self.insert_stmt(stmt, before);
self.insert_stmt(stmt, source, position);
result
}

Expand All @@ -139,6 +153,7 @@ impl MutableBody {
tcx: TyCtxt,
check_type: &CheckType,
source: &mut SourceInstruction,
position: InsertPosition,
value: Local,
msg: &str,
) {
Expand Down Expand Up @@ -168,7 +183,7 @@ impl MutableBody {
unwind: UnwindAction::Terminate,
};
let terminator = Terminator { kind, span };
self.split_bb(source, terminator);
self.split_bb(source, position, terminator);
}
CheckType::Panic | CheckType::NoCore => {
tcx.sess
Expand All @@ -182,11 +197,55 @@ impl MutableBody {
}
}

/// Split a basic block right before the source location and use the new terminator
/// in the basic block that was split.
/// 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(
&mut self,
callee: &Instance,
source: &mut SourceInstruction,
position: InsertPosition,
args: Vec<Operand>,
destination: Place,
) {
let new_bb = self.blocks.len();
let span = source.span(&self.blocks);
let callee_op =
Operand::Copy(Place::from(self.new_local(callee.ty(), span, Mutability::Not)));
let kind = TerminatorKind::Call {
func: callee_op,
args,
destination,
target: Some(new_bb),
unwind: UnwindAction::Terminate,
};
let terminator = Terminator { kind, span };
self.split_bb(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(&mut self, source: &mut SourceInstruction, new_term: Terminator) {
pub fn split_bb(
&mut self,
source: &mut SourceInstruction,
position: InsertPosition,
new_term: Terminator,
) {
match position {
InsertPosition::Before => {
self.split_bb_before(source, new_term);
}
InsertPosition::After => {
self.split_bb_after(source, new_term);
}
}
}

/// Split a basic block right before the source location.
fn split_bb_before(&mut self, source: &mut SourceInstruction, new_term: Terminator) {
let new_bb_idx = self.blocks.len();
let (idx, bb) = match source {
SourceInstruction::Statement { idx, bb } => {
Expand All @@ -196,9 +255,9 @@ impl MutableBody {
(orig_idx, orig_bb)
}
SourceInstruction::Terminator { bb } => {
let orig_bb = *bb;
let (orig_idx, orig_bb) = (self.blocks[*bb].statements.len(), *bb);
*bb = new_bb_idx;
(self.blocks[orig_bb].statements.len(), orig_bb)
(orig_idx, orig_bb)
}
};
let old_term = mem::replace(&mut self.blocks[bb].terminator, new_term);
Expand All @@ -208,16 +267,95 @@ impl MutableBody {
self.blocks.push(new_bb);
}

/// Insert statement before the source instruction and update the source as needed.
pub fn insert_stmt(&mut self, new_stmt: Statement, before: &mut SourceInstruction) {
match before {
/// Split a basic block right after the source location.
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 } => {
self.blocks[*bb].statements.insert(*idx, new_stmt);
*idx += 1;
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);
}
// Make the terminator at `source` point at the new block,
// the terminator of which is a simple Goto instruction.
SourceInstruction::Terminator { bb } => {
// Append statements at the end of the basic block.
self.blocks[*bb].statements.push(new_stmt);
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."),
};
}
};
}

/// Insert statement before or after the source instruction and update the source as needed.
pub fn insert_stmt(
&mut self,
new_stmt: Statement,
source: &mut SourceInstruction,
position: InsertPosition,
) {
match position {
InsertPosition::Before => {
match source {
SourceInstruction::Statement { idx, bb } => {
self.blocks[*bb].statements.insert(*idx, new_stmt);
*idx += 1;
}
SourceInstruction::Terminator { bb } => {
// Append statements at the end of the basic block.
self.blocks[*bb].statements.push(new_stmt);
}
}
}
InsertPosition::After => {
let new_bb_idx = self.blocks.len();
let span = source.span(&self.blocks);
match source {
SourceInstruction::Statement { idx, bb } => {
self.blocks[*bb].statements.insert(*idx + 1, new_stmt);
*idx += 1;
}
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."),
};
}
}
}
}
}
Expand Down
Loading

0 comments on commit d926482

Please sign in to comment.