diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs index 3fa74b0e5aba..ea80c2cf8926 100644 --- a/kani-compiler/src/args.rs +++ b/kani-compiler/src/args.rs @@ -82,6 +82,8 @@ pub enum ExtraChecks { /// Check that produced values are valid except for uninitialized values. /// See https://github.com/model-checking/kani/issues/920. Validity, + /// Check for violations of pointer aliasing model + Aliasing, /// Check for using uninitialized memory. Uninit, } diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index a5d077d9c16e..00eeb98baebe 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -232,3 +232,80 @@ fn find_fn_def(tcx: TyCtxt, diagnostic: &str) -> Option { }; Some(def) } + +/// NamedFnDef encapsulates the diagnostic along with the fn def. +#[derive(Clone, Debug, Eq, PartialEq)] +pub struct NamedFnDef { + /// The diagnostic with which the function definition + /// is found + diagnostic: String, + /// The "value", the resolved function instance itself + def: FnDef, +} + +impl NamedFnDef { + /// Create a new cacheable instance with the given signature and + /// def + pub fn new(diagnostic: String, def: FnDef) -> NamedFnDef { + NamedFnDef { diagnostic, def } + } +} + +trait Cache { + /// Generate a mutable reference to the cache's first item, + /// or if none exists try generating a new one with `f` + /// and return it. When `f` fails, return an error + /// `vec`'s first item that + /// passes the predicate `p`, or if none exists try generating + /// a new one with `f` and return it. + /// When `f` fails, return an error. + fn try_get_or_insert(&mut self, p: P, f: F) -> Result<&mut T, E> + where + F: FnOnce() -> Result, + P: Fn(&T) -> bool; +} + +impl Cache for Vec +where + T: PartialEq, +{ + fn try_get_or_insert(&mut self, p: P, f: F) -> Result<&mut T, E> + where + F: FnOnce() -> Result, + P: Fn(&T) -> bool, + { + if let Some(i) = self.iter().position(p) { + Ok(&mut self[i]) + } else { + self.push(f()?); + Ok(self.last_mut().unwrap()) + } + } +} + +/// Caches function instances for later lookups. +#[derive(Default, Debug)] +pub struct FnDefCache { + /// The cache + cache: Vec, +} + +impl FnDefCache { + pub fn register( + &mut self, + ctx: &TyCtxt, + diagnostic: String, + ) -> Result<&FnDef, stable_mir::Error> { + let test_diagnostic = diagnostic.clone(); + self.cache + .try_get_or_insert( + |item: &NamedFnDef| item.diagnostic == test_diagnostic, + || { + let fndef = find_fn_def(*ctx, diagnostic.as_str()) + .ok_or(stable_mir::Error::new(format!("Not found: {}", &diagnostic)))?; + Ok(NamedFnDef::new(diagnostic, fndef)) + }, + ) + .map(|entry| &entry.def) + } +} diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index d2c9d50515c4..ca60b4684e08 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -579,6 +579,7 @@ impl CallGraph { /// Print the graph in DOT format to a file. /// See for more information. + #[allow(unused)] fn dump_dot(&self, tcx: TyCtxt) -> std::io::Result<()> { if let Ok(target) = std::env::var("KANI_REACH_DEBUG") { debug!(?target, "dump_dot"); @@ -601,6 +602,7 @@ impl CallGraph { } /// Write all notes to the given writer. + #[allow(unused)] fn dump_all(&self, writer: &mut W) -> std::io::Result<()> { tracing::info!(nodes=?self.nodes.len(), edges=?self.edges.len(), "dump_all"); for node in &self.nodes { @@ -614,6 +616,7 @@ impl CallGraph { } /// Write all notes that may have led to the discovery of the given target. + #[allow(unused)] fn dump_reason(&self, writer: &mut W, target: &str) -> std::io::Result<()> { let mut queue: Vec = self.nodes.iter().filter(|item| item.to_string().contains(target)).cloned().collect(); @@ -645,6 +648,15 @@ impl CallGraph { } Ok(()) } + + /// Get all items adjacent to the current item in the + /// call graph. + pub fn successors(&self, node: MonoItem) -> Vec<&MonoItem> { + match self.edges.get(&Node(node)) { + None => vec![], + Some(list) => list.iter().map(|collected| &collected.0.item).collect(), + } + } } impl Display for Node { diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 24fe5d8b2b2e..4ca4f4b4671b 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -165,7 +165,46 @@ impl MutableBody { self.insert_stmt(stmt, source, position); } - /// Add a new assert to the basic block indicated by the given index. + /// Add a new assert to the basic block by the source instruction, using + /// "local" as the checking function. + /// + /// The new assertion 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 insert_check_with_local( + &mut self, + local: Local, + source: &mut SourceInstruction, + position: InsertPosition, + value: Local, + msg: &str, + ) { + assert_eq!( + self.locals[value].ty, + Ty::bool_ty(), + "Expected boolean value as the assert input" + ); + assert!(self.locals[local].ty.kind().is_fn(), "Expected a function type as assert"); + let new_bb = self.blocks.len(); + let span = source.span(&self.blocks); + let assert_op = Operand::Copy(Place::from(local)); + let msg_op = self.new_str_operand(msg, span); + let kind = TerminatorKind::Call { + func: assert_op, + args: vec![Operand::Move(Place::from(value)), msg_op], + destination: Place { + local: self.new_local(Ty::new_tuple(&[]), span, Mutability::Not), + projection: vec![], + }, + target: Some(new_bb), + unwind: UnwindAction::Terminate, + }; + let terminator = Terminator { kind, span }; + self.insert_terminator(source, position, terminator); + } + + /// Add a new assert to the basic block indicated by "source". /// /// The new assertion 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 @@ -185,28 +224,11 @@ impl MutableBody { Ty::bool_ty(), "Expected boolean value as the assert input" ); - let new_bb = self.blocks.len(); let span = source.span(&self.blocks); match check_type { CheckType::Assert(assert_fn) => { - let assert_op = Operand::Copy(Place::from(self.new_local( - assert_fn.ty(), - span, - Mutability::Not, - ))); - let msg_op = self.new_str_operand(msg, span); - let kind = TerminatorKind::Call { - func: assert_op, - args: vec![Operand::Move(Place::from(value)), msg_op], - destination: Place { - local: self.new_local(Ty::new_tuple(&[]), span, Mutability::Not), - projection: vec![], - }, - target: Some(new_bb), - unwind: UnwindAction::Terminate, - }; - let terminator = Terminator { kind, span }; - self.insert_terminator(source, position, terminator); + let local = self.new_local(assert_fn.ty(), span, Mutability::Not); + self.insert_check_with_local(local, source, position, value, msg); } CheckType::Panic | CheckType::NoCore => { tcx.sess @@ -220,15 +242,32 @@ impl MutableBody { } } + /// Add a new call to the basic block indicated by the given index. + /// This has the same semantics as insert_call_to_local, the only + /// difference being that a new local is created for the given function + /// instance. + pub fn insert_call( + &mut self, + callee: &Instance, + source: &mut SourceInstruction, + position: InsertPosition, + args: Vec, + destination: Place, + ) { + let span = source.span(&self.blocks); + let local = self.new_local(callee.ty(), span, Mutability::Not); + self.insert_call_to_local(local, source, position, args, destination); + } + /// 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. 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 insert_call( + pub fn insert_call_to_local( &mut self, - callee: &Instance, + callee: Local, source: &mut SourceInstruction, position: InsertPosition, args: Vec, @@ -236,8 +275,7 @@ impl MutableBody { ) { 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 callee_op = Operand::Copy(Place::from(callee)); let kind = TerminatorKind::Call { func: callee_op, args, diff --git a/kani-compiler/src/kani_middle/transform/check_aliasing/function_cache.rs b/kani-compiler/src/kani_middle/transform/check_aliasing/function_cache.rs new file mode 100644 index 000000000000..1e5cd45aea5f --- /dev/null +++ b/kani-compiler/src/kani_middle/transform/check_aliasing/function_cache.rs @@ -0,0 +1,54 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! This module contains a cache of resolved generic functions + +use crate::kani_middle::find_fn_def; +use rustc_middle::ty::TyCtxt; + +type Result = std::result::Result; + + +/// Caches function instances for later lookups. +#[derive(Default, Debug)] +pub struct Cache { + /// The cache + cache: Vec, +} + +fn try_get_or_insert(vec: &mut Vec, p: P, f: F) -> Result<&mut T> +where + F: FnOnce() -> Result, + P: Fn(&T) -> bool, + T: PartialEq, +{ + if let Some(i) = vec.iter().position(p) { + Ok(&mut vec[i]) + } else { + vec.push(f()?); + Ok(vec.last_mut().unwrap()) + } +} + +impl Cache { + /// Register the signature the to the cache + /// in the given compilation context, ctx + pub fn register( + &mut self, + ctx: &TyCtxt, + signature: Signature, + ) -> Result<&> { + let test_sig = signature.clone(); + let Cache { cache } = self; + try_get_or_insert( + cache, + |item| item.signature == test_sig, + || { + let fndef = find_fn_def(*ctx, &signature.diagnostic) + .ok_or(MirError::new(format!("Not found: {}", &signature.diagnostic)))?; + let instance = MirInstance::resolve(fndef, &GenericArgs(signature.args.clone()))?; + Ok(NamedFnDef::new(signature, instance)) + }, + ) + .map(|entry| &entry.instance) + } +} diff --git a/kani-compiler/src/kani_middle/transform/check_aliasing/instrumentation.rs b/kani-compiler/src/kani_middle/transform/check_aliasing/instrumentation.rs new file mode 100644 index 000000000000..c1d412c3db54 --- /dev/null +++ b/kani-compiler/src/kani_middle/transform/check_aliasing/instrumentation.rs @@ -0,0 +1,425 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! This module contains methods handling the data needed +//! for the instrumentation of a single function body with updates from the +//! stacked borrows calculus. These data ensure that each of the original +//! locals is instrumented, that each of the original instructions +//! are instrumented, and that no code that is added by the instrumentation +//! pass itself is instrumented or analyzed. + +use super::Cache; +use crate::kani_middle::transform::body::InsertPosition; +use rustc_middle::ty::TyCtxt; +use stable_mir::mir::mono::Instance; +use stable_mir::mir::{ + BasicBlock, Body, ConstOperand, Local, MirVisitor, Mutability, Operand, Place, Rvalue, + Statement, StatementKind, Terminator, TerminatorKind, UnwindAction, +}; +use stable_mir::ty::{GenericArgKind, GenericArgs, MirConst, Span, Ty}; +use std::collections::HashMap; +use tracing::debug; + +use super::super::body::{MutableBody, SourceInstruction}; +use super::{Action, CollectActions, MirError}; + +type Result = std::result::Result; + +pub struct InstrumentationData<'tcx, 'cache> { + /// Compilation context, used to fetch resolved generic functions + tcx: TyCtxt<'tcx>, + /// Cache of resolved generic functions, + /// potentially populated by previous passes + cache: &'cache mut Cache, + /// Map associating each local with a local storing + /// its address on the stack, which is used to associate + /// the metadata. + meta_stack: HashMap, + /// The count of the number of locals in the original + /// body + local_count: usize, + /// A local storing the unit value + unit: Local, + /// A local storing whether the stack is still in a valid + /// state + valid: Local, + /// A map associating resolved generic functions with + /// locals in the body that can be used to call them + fn_pointers: HashMap, + /// The span of the body + span: Span, + /// The body being instrumented + body: MutableBody, + /// The code actions for the instruction + actions: Option)>>, +} + +impl<'tcx, 'cache> InstrumentationData<'tcx, 'cache> { + /// Using a (potentially) pre-populated cache of resolved generic + /// functions, and the StableMir body "body", initialize the instrumentation + /// pass data. + pub fn new(tcx: TyCtxt<'tcx>, cache: &'cache mut Cache, body: Body) -> Self { + let mut visitor = CollectActions::new(body.locals()); + visitor.visit_body(&body); + let actions = Some(visitor.finalize()); + let span = body.span; + let mut body = MutableBody::from(body); + let meta_stack = HashMap::new(); + let local_count = body.locals().len(); + let fn_pointers = HashMap::new(); + let unit = body.new_local(Ty::new_tuple(&[]), span, Mutability::Not); + let valid = body.new_local( + Ty::from_rigid_kind(stable_mir::ty::RigidTy::Bool), + span, + Mutability::Mut, + ); + InstrumentationData { + tcx, + cache, + meta_stack, + local_count, + unit, + valid, + fn_pointers, + span, + body, + actions, + } + } + + /// Register the function described by the diagnostic + /// and generic arguments in "Signature". + fn register_fn(&mut self, diagnostic: &str, args: &[GenericArgKind]) -> Result { + let def = self.cache.register(&self.tcx, diagnostic.to_owned())?; + let instance = Instance::resolve(*def, &GenericArgs(args.to_vec()))?; + let func_local = self + .fn_pointers + .entry(instance) + .or_insert_with(|| self.body.new_local(instance.ty(), self.span, Mutability::Not)); + Ok(*func_local) + } + + /// Call at source and insert position, using the arguments + /// in args and returning into "dest". + /// This differs from Mutable Body's call in that the + /// function name is cached. + pub fn call( + &mut self, + diagnostic: &str, + tys: &[GenericArgKind], + args: Vec, + dest: Local, + source: &SourceInstruction, + ) -> Result { + let fn_local = self.register_fn(diagnostic, tys)?; + let func = Operand::Copy(Place::from(fn_local)); + let args = args.into_iter().map(|local| Operand::Copy(Place::from(local))).collect(); + let destination = Place::from(dest); + let target = Some(0); // doesn't matter, updated later + let unwind = UnwindAction::Terminate; + let kind = TerminatorKind::Call { func, args, destination, target, unwind }; + let span = source.span(self.body.blocks()); + Ok(Terminator { kind, span }) + } + + /// Instrument the call generated by "call" for these parameters. + pub fn instrument_call( + &mut self, + callee: &str, + tys: &[GenericArgKind], + args: Vec, + dest: Local, + source: &mut SourceInstruction, + ) -> Result<()> { + let terminator = self.call(callee, tys, args, dest, source)?; + let bb = BasicBlock { statements: vec![], terminator }; + self.body.insert_bb(bb, source, InsertPosition::Before); + Ok(()) + } + + /// Instrument an assignment to a local + pub fn assign_pointer( + &mut self, + lvalue: Local, + rvalue: Local, + source: &SourceInstruction, + ) -> Statement { + let span = source.span(&self.body.blocks()); + let rvalue = Rvalue::AddressOf(Mutability::Not, Place::from(rvalue)); + Statement { kind: StatementKind::Assign(Place::from(lvalue), rvalue), span } + } + + pub fn first_instruction(&self) -> SourceInstruction { + if self.body.blocks()[0].statements.is_empty() { + SourceInstruction::Terminator { bb: 0 } + } else { + SourceInstruction::Statement { idx: 0, bb: 0 } + } + } + + /// For some local, say let x: T; + /// instrument it with the functions that initialize the stack: + /// let ptr_x: *const T = &raw const x; + /// initialize_local(ptr_x); + pub fn instrument_local(&mut self, local: Local) -> Result<()> { + let ty = self.body.locals()[local].ty; + let local_ptr = *self.meta_stack.get(&local).unwrap(); + let statement = self.assign_pointer(local_ptr, local, &self.first_instruction()); + let statements = vec![statement]; + let terminator = self.call( + "KaniInitializeLocal", + &[GenericArgKind::Type(ty)], + vec![local_ptr], + self.unit, + &self.first_instruction(), + )?; + let bb = BasicBlock { statements, terminator }; + self.body.insert_bb(bb, &mut self.first_instruction(), InsertPosition::Before); + Ok(()) + } + + /// Instrument a stack reference of the fo + /// lvalue = &rvalue + /// with an update to the stacked borrows state, + /// at the code index source. + pub fn instrument_new_stack_reference( + &mut self, + source: &mut SourceInstruction, + lvalue: Local, + rvalue: Local, + ) -> Result<()> { + // Initialize the constants + let ty = self.body.locals()[rvalue].ty; + let lvalue_ref = self.meta_stack.get(&lvalue).unwrap(); + let rvalue_ref = self.meta_stack.get(&rvalue).unwrap(); + self.instrument_call( + "KaniNewMutRefFromValue", + &[GenericArgKind::Type(ty)], + vec![*lvalue_ref, *rvalue_ref], + self.unit, + source, + )?; + Ok(()) + } + + /// Return the source instruction one below "source," + /// or the instruction at 0 if there are none below + fn predecessor(&self, source: &SourceInstruction) -> SourceInstruction { + match source { + // One below 0, 0 is 0, 0 + SourceInstruction::Statement { idx: 0, bb: 0 } => { + SourceInstruction::Statement { idx: 0, bb: 0 } + } + // One below the first statement of a block is the + // previous terminator + SourceInstruction::Statement { idx: 0, bb } => { + SourceInstruction::Terminator { bb: *bb - 1 } + } + // Otherwise one below the statement of a block is the + // previous statement + SourceInstruction::Statement { idx, bb } => { + SourceInstruction::Statement { idx: idx - 1, bb: *bb } + } + // One below the terminator of the first block with no statements + // is 0, 0 + SourceInstruction::Terminator { bb: 0 } + if self.body.blocks()[0].statements.is_empty() => + { + SourceInstruction::Statement { idx: 0, bb: 0 } + } + // Otherwise one below the terminator of a block is the previous + // terminator if there are no statements in the block, + SourceInstruction::Terminator { bb } + if self.body.blocks()[*bb].statements.is_empty() => + { + SourceInstruction::Terminator { bb: *bb - 1 } + } + // Or the last statement of the current block. + SourceInstruction::Terminator { bb } => SourceInstruction::Statement { + idx: self.body.blocks()[*bb].statements.len() - 1, + bb: *bb, + }, + } + } + + /// Instrument with stack violated / not violated + pub fn instrument_stack_check( + &mut self, + source: &mut SourceInstruction, + check_source: &SourceInstruction, + ) -> Result<()> { + let less = self.predecessor(check_source); + let msg = format!( + "Stacked borrows state invalidated at {:?}", + less.span(self.body.blocks()).get_lines() + ); + self.instrument_call("KaniStackValid", &[], vec![], self.valid, source)?; + let assert = self.register_fn("KaniAssert", &[])?; + self.body.insert_check_with_local(assert, source, InsertPosition::Before, self.valid, &msg); + Ok(()) + } + + /// Instrument a validity assertion on the stacked borrows state + /// at idx for (place: &mut T). + pub fn instrument_stack_update_ref( + &mut self, + source: &mut SourceInstruction, + place: Local, + ty: Ty, + ) -> Result<()> { + // Initialize the constants + let place_ref = self.meta_stack.get(&place).unwrap(); + self.instrument_call( + "KaniStackCheckRef", + &[GenericArgKind::Type(ty)], + vec![*place_ref], + self.unit, + source, + )?; + Ok(()) + } + + /// Instrument a validity assertion on the stacked borrows state + /// at idx for (place: *const T). + pub fn instrument_stack_update_ptr( + &mut self, + source: &mut SourceInstruction, + place: Local, + ty: Ty, + ) -> Result<()> { + // Initialize the constants + let place_ref = self.meta_stack.get(&place).unwrap(); + self.instrument_call( + "KaniStackCheckPtr", + &[GenericArgKind::Type(ty)], + vec![*place_ref], + self.unit, + source, + )?; + Ok(()) + } + + /// Instrument code of the form + /// created = &mut *(raw: const *T). + pub fn instrument_new_mut_ref_from_raw( + &mut self, + source: &mut SourceInstruction, + created: Local, + raw: Local, + ty: Ty, + ) -> Result<()> { + // Initialize the constants + let created_ref = self.meta_stack.get(&created).unwrap(); + let reference_ref = self.meta_stack.get(&raw).unwrap(); + self.instrument_call( + "KaniNewMutRefFromRaw", + &[GenericArgKind::Type(ty)], + vec![*created_ref, *reference_ref], + self.unit, + source, + )?; + Ok(()) + } + + /// Instrument code of the form + /// created = (ref: &mut T) as *mut T + pub fn instrument_new_mut_raw_from_ref( + &mut self, + source: &mut SourceInstruction, + created: Local, + reference: Local, + ty: Ty, + ) -> Result<()> { + // Initialize the constants + let created_ref = self.meta_stack.get(&created).unwrap(); + let reference_ref = self.meta_stack.get(&reference).unwrap(); + self.instrument_call( + "KaniNewMutRawFromRef", + &[GenericArgKind::Type(ty)], + vec![*created_ref, *reference_ref], + self.unit, + source, + )?; + Ok(()) + } + + /// Instrument each of the locals collected into values with + /// initialization data. + pub fn instrument_locals(&mut self) -> Result<()> { + for local in ((self.body.arg_count() + 1)..self.local_count).rev() { + self.instrument_local(local)? + } + Ok(()) + } + + /// Instrument the action given in "action" with the appropriate + /// update to the stacked borrows state. + fn instrument_action( + &mut self, + source: &mut SourceInstruction, + check_source: &SourceInstruction, + action: Action, + ) -> Result<()> { + match action { + Action::StackCheck => self.instrument_stack_check(source, check_source), + Action::NewStackReference { lvalue, rvalue } => { + eprintln!("instrumenting stack ref"); + self.instrument_new_stack_reference(source, lvalue, rvalue) + } + Action::StackUpdateReference { place, ty } => { + self.instrument_stack_update_ref(source, place, ty) + } + Action::NewMutRefFromRaw { lvalue, rvalue, ty } => { + self.instrument_new_mut_ref_from_raw(source, lvalue, rvalue, ty) + } + Action::StackUpdatePointer { place, ty } => { + self.instrument_stack_update_ptr(source, place, ty) + } + Action::NewMutRawFromRef { lvalue, rvalue, ty } => { + self.instrument_new_mut_raw_from_ref(source, lvalue, rvalue, ty) + } + } + } + + /// Instrument all of the instructions and terminators in the function body + /// with appropriate updates to the stacked borrows state + /// and with validity assertions on the stacked borrows state. + pub fn instrument_instructions(&mut self) -> Result<()> { + let to_instrument = self.actions.take().unwrap(); + for (mut source, actions) in to_instrument.into_iter().rev() { + let check_source = source; + for action in actions.into_iter() { + self.instrument_action(&mut source, &check_source, action)?; + } + } + Ok(()) + } + + /// Initialize the "valid" local, used to check whether + /// the stack has been invalidated + pub fn instrument_initialize_stack_check(&mut self) { + let mut source = self.first_instruction(); + let span = self.first_instruction().span(self.body.blocks()); + let lvalue = Place::from(self.valid); + let user_ty = None; + let const_ = MirConst::from_bool(true); + let operand = Operand::Constant(ConstOperand { span, user_ty, const_ }); + let rvalue = Rvalue::Use(operand); + let statement = Statement { kind: StatementKind::Assign(lvalue, rvalue), span }; + self.body.insert_stmt(statement, &mut source, InsertPosition::Before); + } + + /// Run the passes and retrieve the mutable body + pub fn finalize(mut self) -> Result { + for local in ((self.body.arg_count() + 1)..self.local_count).rev() { + let ty = self.body.locals()[local].ty; + let ptr_ty = Ty::new_ptr(ty, Mutability::Not); + let local_ptr = self.body.new_local(ptr_ty, self.span, Mutability::Not); + self.meta_stack.insert(local, local_ptr); + } + debug!("instrumenting instructions"); + self.instrument_instructions()?; + self.instrument_locals()?; + self.instrument_initialize_stack_check(); + Ok(self.body) + } +} diff --git a/kani-compiler/src/kani_middle/transform/check_aliasing/mod.rs b/kani-compiler/src/kani_middle/transform/check_aliasing/mod.rs new file mode 100644 index 000000000000..25e92a0799ce --- /dev/null +++ b/kani-compiler/src/kani_middle/transform/check_aliasing/mod.rs @@ -0,0 +1,132 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! Implement a pass that instruments code with assertions +//! that will fail when the aliasing model is violated. + +use stable_mir::mir::mono::{Instance, MonoItem}; +use stable_mir::CrateDef; +// Reimport components of mir that conflict with +// parts of the sub-pass's API. +pub use stable_mir::Error as MirError; + +mod visitor; +use visitor::*; +mod instrumentation; +use instrumentation::*; + +use crate::args::ExtraChecks; +use crate::kani_middle::transform::{TransformPass, TransformationResult, TransformationType}; +use crate::kani_middle::FnDefCache as Cache; +use crate::kani_queries::QueryDb; +use rustc_middle::ty::TyCtxt; +use stable_mir::mir::Body; +use std::collections::{HashSet, VecDeque}; +use std::fmt::Debug; +use tracing::trace; + +use super::GlobalPass; + +/// Instrument the code with checks for aliasing model +/// violations. +/// Cache functions in-between applications of the pass. +/// This is performed by taking the incoming body, +/// using a visitor to find instructions relevant to +/// the instrumentation, then iterating over these +/// instructions backwards, inserting code prior to their +/// execution. +#[derive(Debug)] +struct AliasingPass<'cache> { + cache: &'cache mut Cache, +} + +/// Returns whether ExtraChecks::Aliasing is included +/// in the command line arguments +fn db_includes_aliasing(query_db: &QueryDb) -> bool { + query_db.args().ub_check.contains(&ExtraChecks::Aliasing) +} + +impl<'cache> TransformPass for AliasingPass<'cache> { + fn transformation_type() -> TransformationType + where + Self: Sized, + { + TransformationType::Instrumentation + } + + fn is_enabled(&self, query_db: &QueryDb) -> bool + where + Self: Sized, + { + db_includes_aliasing(query_db) + } + + fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { + trace!(function=?instance.name(), "transform: aliasing pass"); + let instrumentation_data = InstrumentationData::new(tcx, &mut self.cache, body); + let out = instrumentation_data.finalize().unwrap().into(); + (true, out) + } +} + +/// The global aliasing pass keeps a cache of resolved generic functions, +/// and ensures that only the functions that are called +/// from the proof harness itself are instrumented. +/// To avoid instrumenting functions that were not present in the source, +/// but added in the instrumented code, this first collects the functions +/// present in the source, then instruments them. +#[derive(Debug, Default)] +pub struct GlobalAliasingPass { + cache: Cache, +} + +impl GlobalAliasingPass { + pub fn new() -> Self { + Default::default() + } +} + +impl GlobalPass for GlobalAliasingPass { + fn is_enabled(&self, query_db: &QueryDb) -> bool + where + Self: Sized, + { + db_includes_aliasing(query_db) + } + + fn transform( + &mut self, + tcx: TyCtxt, + call_graph: &crate::kani_middle::reachability::CallGraph, + _starting_items: &[stable_mir::mir::mono::MonoItem], + instances: Vec, + transformer: &mut super::BodyTransformation, + ) { + let mut found = HashSet::new(); + let mut queue = VecDeque::new(); + // Collect + for instance in &instances { + if instance + .def + .all_attrs() + .into_iter() + .any(|attr| attr.as_str().contains("kanitool::proof")) + && found.insert(instance) + { + queue.push_back(instance) + } + } + while let Some(instance) = queue.pop_front() { + let mut pass = AliasingPass { cache: &mut self.cache }; + let (_, body) = pass.transform(tcx, transformer.body(tcx, *instance), *instance); + transformer.cache.insert(*instance, TransformationResult::Modified(body)); + for node in call_graph.successors(MonoItem::Fn(*instance).clone()) { + if let MonoItem::Fn(adjacent) = node { + if found.insert(adjacent) { + queue.push_back(adjacent); + } + } + } + } + } +} diff --git a/kani-compiler/src/kani_middle/transform/check_aliasing/visitor.rs b/kani-compiler/src/kani_middle/transform/check_aliasing/visitor.rs new file mode 100644 index 000000000000..5ace61e85723 --- /dev/null +++ b/kani-compiler/src/kani_middle/transform/check_aliasing/visitor.rs @@ -0,0 +1,253 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! This module contains stacked borrows "actions," +//! or updates to the stacked borrows state, as well as +//! methods that collect the actions that need to be applied from the +//! statements of the code. + +use stable_mir::mir::visit::Location; +use stable_mir::mir::{ + BorrowKind, Local, LocalDecl, MirVisitor, Mutability, Operand, Place, ProjectionElem, Rvalue, + Statement, StatementKind, Terminator, +}; +use stable_mir::ty::{RigidTy, Ty, TyKind}; + +use crate::kani_middle::transform::body::SourceInstruction; + +/// Update action to the stacked borrows state +#[derive(Debug)] +pub enum Action { + StackCheck, + NewStackReference { lvalue: Local, rvalue: usize }, + StackUpdateReference { place: usize, ty: Ty }, + NewMutRefFromRaw { lvalue: usize, rvalue: usize, ty: Ty }, + StackUpdatePointer { place: usize, ty: Ty }, + NewMutRawFromRef { lvalue: usize, rvalue: usize, ty: Ty }, +} + +/// The actions of a statement +pub struct CollectActions<'locals> { + /// The source instruction currently being visited + source: SourceInstruction, + /// The current actions collected + collected: Vec, + /// The code actions to insert behind the given + /// instruction + actions: Vec<(SourceInstruction, Vec)>, + /// The locals, required to ensure that the references + /// and pointers are picked appropriately. + locals: &'locals [LocalDecl], +} + +impl<'locals> CollectActions<'locals> { + /// Initialize the struct using the given locals + pub fn new(locals: &'locals [LocalDecl]) -> Self { + CollectActions { + source: SourceInstruction::Statement { idx: 0, bb: 0 }, + collected: Vec::new(), + actions: Vec::new(), + locals, + } + } + + pub fn finalize(self) -> Vec<(SourceInstruction, Vec)> { + self.actions + } + + /// Collect the actions for assigning the lvalue + /// to the dereferenced rvalue + fn visit_assign_reference_dereference(&mut self, lvalue: Local, rvalue: Local) { + match self.locals[rvalue].ty.kind() { + TyKind::RigidTy(RigidTy::Ref(_, ty, _)) | TyKind::RigidTy(RigidTy::RawPtr(ty, _)) => { + self.collected.push(Action::NewMutRefFromRaw { lvalue, rvalue, ty }); + } + _ => {} + } + } + + /// Collect the actions for assigning the reference in + /// "place" to the local at "to". + fn visit_assign_reference(&mut self, to: Local, from: Place) { + match from.projection[..] { + [] => { + // Direct reference to stack local + // x = &y; + let lvalue = to; + let rvalue = from.local; + self.collected.push(Action::NewStackReference { lvalue, rvalue }); + } + [ProjectionElem::Deref] => { + // Reborrow + // x : &mut T = &*(y : *mut T OR &mut T) + let lvalue = to; // Copy to avoid borrow + let rvalue = from.local; // Copy to avoid borrow + self.visit_assign_reference_dereference(lvalue, rvalue); + } + _ => { + eprintln!("not yet handled: assignment to reference {:?}", from) + } + } + } + + /// Collect the actions for assigning the data at + /// from to the local at to. + fn visit_assign_pointer(&mut self, to: Local, from: Place) { + match from.projection[..] { + [] => { + // x = &raw y + panic!("Addr of not yet handled"); + } + [ProjectionElem::Deref] => { + // x = &raw mut *(y: &mut T OR *mut T) + let rvalue = from.local; // Copy to avoid borrow + let lvalue = to; + match self.locals[rvalue].ty.kind() { + TyKind::RigidTy(RigidTy::Ref(_, ty, _)) => { + self.collected.push(Action::NewMutRawFromRef { lvalue, rvalue, ty }); + } + _ => { + panic!( + "Dereference of rvalue case not yet handled for raw pointers {:?}", + from + ); + } + } + } + _ => {} + } + } + + /// Collect the actions for a Place, + /// incurring a stack check in the case of a + /// dereference of a pointer or reference + fn visit_place(&mut self, place: &Place) { + match &place.projection[..] { + [] => { + // Direct usage -- no update needed + return; + } + [ProjectionElem::Deref] => { + // Dereference -- instrument stack check + } + _ => { + // Field access -- not yet handled. + return; + } + }; + if self.locals[place.local].ty.kind().is_ref() { + let ty = place.ty(self.locals).unwrap(); + self.collected.push(Action::StackUpdateReference { place: place.local, ty }); + self.collected.push(Action::StackCheck); + } + if self.locals[place.local].ty.kind().is_raw_ptr() { + let ty = place.ty(self.locals).unwrap(); + self.collected.push(Action::StackUpdatePointer { place: place.local, ty }); + self.collected.push(Action::StackCheck); + } + } + + /// Collect the actions for the places of an Rvalue + fn visit_rvalue_places(&mut self, rvalue: &Rvalue) { + match rvalue { + Rvalue::AddressOf(_, place) => { + self.visit_place(place); + } + Rvalue::Ref(_, _, place) => { + self.visit_place(place); + } + // The rest are not yet handled + _ => { + eprintln!("Not yet handled: {:?}", rvalue); + } + } + } + + /// Collect the actions for the places of a statement + fn visit_statement_places(&mut self, stmt: &Statement) { + match &stmt.kind { + StatementKind::Assign(place, rvalue) => { + self.visit_rvalue_places(rvalue); + self.visit_place(place); + } + _ => { + eprintln!("Not yet handled: {:?}", stmt); + } + } + } + + /// Collect the actions for the places of the statement, + /// then find assignments of pointer values to lvalues + /// and collect updates to the stacked borrows state + /// accordingly. + /// This is performed in a different order than Mir Visitor's + /// visit statement, and so we call it from the visitor. + fn visit_statement_internal(&mut self, stmt: &Statement) { + self.visit_statement_places(stmt); + match &stmt.kind { + StatementKind::Assign(to, rvalue) => { + match rvalue { + Rvalue::Ref(_, BorrowKind::Mut { .. }, from) => { + self.visit_assign_reference(to.local, from.clone()); + } + Rvalue::AddressOf(Mutability::Mut, from) => { + self.visit_assign_pointer(to.local, from.clone()); + } + Rvalue::Use(Operand::Constant(_)) => { + // Do nothing for the constants case + } + Rvalue::Use(Operand::Copy(_)) => { + eprintln!("Copy not yet handled"); + // Do nothing for the constants case + } + Rvalue::Use(Operand::Move(_)) => { + eprintln!("Move not yet handled"); + // Do nothing for the constants case + } + Rvalue::BinaryOp(_, _, _) => { + eprintln!("Binary op not yet handled"); + } + Rvalue::CheckedBinaryOp(_, _, _) => { + eprintln!("Checked binary op not yet handled"); + } + _ => { + panic!("Rvalue kind: {:?} not yet handled", rvalue); + } + } + } + _ => { + eprintln!("Not yet handled, {:?}", stmt); + } + } + } +} + +impl<'locals> MirVisitor for CollectActions<'locals> { + /// Visit the statement stmt. + /// Associate the actions collected so far with the + /// current source index, then collect the actions + /// of the statement and increase the source index + fn visit_statement(&mut self, stmt: &Statement, _location: Location) { + let collected = std::mem::take(&mut self.collected); + self.actions.push((self.source, collected)); + self.visit_statement_internal(stmt); + self.source = match self.source { + SourceInstruction::Statement { idx, bb } => { + SourceInstruction::Statement { idx: idx + 1, bb } + } + _ => { + unreachable!("Statements follow the first instruction or a terminator.") + } + }; + } + + /// Visit the terminator. + /// Associate the actions collected so far with the + /// current source index, then increase the source index + /// to the next basic block + fn visit_terminator(&mut self, _term: &Terminator, _location: Location) { + let collected = std::mem::take(&mut self.collected); + let bb = self.source.bb(); + self.actions.push((SourceInstruction::Terminator { bb }, collected)); + self.source = SourceInstruction::Statement { idx: 0, bb: bb + 1 }; + } +} diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index 2d963cd1d6eb..ef9023649775 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -25,6 +25,7 @@ use crate::kani_middle::transform::contracts::{AnyModifiesPass, FunctionWithCont use crate::kani_middle::transform::kani_intrinsics::IntrinsicGeneratorPass; use crate::kani_middle::transform::stubs::{ExternFnStubPass, FnStubPass}; use crate::kani_queries::QueryDb; +use check_aliasing::GlobalAliasingPass; use dump_mir_pass::DumpMirPass; use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::{Instance, MonoItem}; @@ -35,6 +36,7 @@ use std::fmt::Debug; pub use internal_mir::RustcInternalMir; pub(crate) mod body; +mod check_aliasing; mod check_uninit; mod check_values; mod contracts; @@ -87,6 +89,7 @@ impl BodyTransformation { mem_init_fn_cache: HashMap::new(), }, ); + // Check aliasing transformer.add_pass( queries, IntrinsicGeneratorPass { @@ -196,6 +199,7 @@ impl GlobalPasses { pub fn new(queries: &QueryDb, tcx: TyCtxt) -> Self { let mut global_passes = GlobalPasses { global_passes: vec![] }; global_passes.add_global_pass(queries, DelayedUbPass::new(CheckType::new_assert(tcx))); + global_passes.add_global_pass(queries, GlobalAliasingPass::new()); global_passes.add_global_pass(queries, DumpMirPass::new(tcx)); global_passes } diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 868d1adce636..9cfa594c54a9 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -142,6 +142,12 @@ impl KaniSession { flags.push("--ub-check=uninit".into()); } + if self.args.common_args.unstable_features.contains(UnstableFeature::Aliasing) { + // Automatically enable shadow memory, since the version of uninitialized memory checks + // without non-determinism depends on it. + flags.push("--ub-check=aliasing".into()); + } + flags.extend(self.args.common_args.unstable_features.as_arguments().map(str::to_string)); // This argument will select the Kani flavour of the compiler. It will be removed before diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index 11df998c820f..a532f017a392 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -92,6 +92,8 @@ pub enum UnstableFeature { GhostState, /// Automatically check that uninitialized memory is not used. UninitChecks, + /// Check the pointer aliasing model + Aliasing, /// Enable an unstable option or subcommand. UnstableOptions, } diff --git a/library/kani/src/aliasing.rs b/library/kani/src/aliasing.rs new file mode 100644 index 000000000000..ef634e817a24 --- /dev/null +++ b/library/kani/src/aliasing.rs @@ -0,0 +1,361 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +#![allow(unused)] // All functions hidden; some may be queried by diagnostic +//! The stacked borrows state. +//! +//! The stacked borrows state associates every pointer value +//! (IE reference or raw pointer) with a unique tag and permission +//! in shadow memory. +//! +//! The tags correspond to the time of the creation of the pointer +//! value, and the permissions correspond to the mutability +//! of the pointer value and its status as a raw pointer or reference. +//! +//! It also associates each byte of the program's memory +//! with a stack of tags, tracking the borrows of the memory +//! containing that byte in temporal order. Every time a +//! pointer value is used, the stack is popped down to that pointer value's +//! tag, effectively marking the borrows that occur after that variable +//! as dead. If the borrows associated with the tags popped are later used, +//! the search for them at that byte fails and the stacked borrows state +//! is considered violated. +//! +//! For example: +//! ```rust +//! // Stack allocate 10 and store it at x. +//! // Stack at addr_of!(x) through addr_of!(x) + 4: +//! // [(TAG_0, Permission::UNIQUE)] +//! let mut x: i32 = 10; +//! // Make the pointer object `&mut x`. Associate `&mut x` +//! // with the tag and permission `(1, Permission::UNIQUE)` +//! // by associating `addr_of!(y)` with `(1, Permission::UNIQUE)` +//! // in shadow memory. Push the tag to the borrow stacks of +//! // `addr_of!(x)` through `addr_of!(x) + 4` yielding +//! // the stacks [(TAG_0, Permission::UNIQUE), (TAG_1, Permission::UNIQUE)] +//! let y = &mut x; +//! // Associate `addr_of!(z)` and push the stacks as +//! // above with the tag (2, Permission::SHAREDRW), +//! // corresponding to a raw pointer, yielding the stacks +//! // [(TAG_0, Permission::UNIQUE), (TAG_1, Permission::UNIQUE), +//! // (TAG_2, Permission::SHAREDRW)]. +//! let z = y as *mut i32; +//! // Pop elements from the pointee object stack until it matches +//! // the tag associated with the pointer value, yielding +//! // [(TAG_0, Permission::UNIQUE), (TAG_1, Permission::UNIQUE)] +//! *y = 10; +//! // Run stack lookup on the tag associated with the pointer +//! // object created at `y as *mut i32`, ie, (TAG_2, Permission::SHAREDRW) +//! // resulting in an error. +//! unsafe { *(&mut *z) = 10; } +//! ``` +//! When demonic nondeterminism is used (currently it is always used), +//! a nondeterminism oracle is queried to select a single byte of the program's +//! memory. This way, if a single byte is ever invalid, the nondeterminism +//! oracle will select it, and allow an error to be thrown. +//! This can be used with the restriction that assertions over +//! relations between the stacks (such as, for example, equality between +//! the top two tags of two different stacks) are never needed. + +use crate::mem::{pointer_object, pointer_offset}; +use crate::shadow::ShadowMem; + +/// Bounds on the space usage of the analysis +mod limits { + pub(super) const STACK_DEPTH: usize = 15; +} + +/// Types used in the analysis +mod types { + /// Pointer tag. + /// Up to 256 pointers are tracked; and so they are + /// given a symbolic name by the PointerTag type. + pub(super) type PointerTag = u8; + + /// Access bit. + /// Encoded as associated constants + /// instead of as an enum to ensure + /// that the representation uses + /// 8 bits. Using an enum instead can cause + /// factor of 2 blowups. + pub(super) type AccessBit = bool; + pub(super) struct Access; + impl Access { + pub(super) const READ: AccessBit = false; + pub(super) const WRITE: AccessBit = true; + } + + /// Type of permission. + /// To ensure that 8 bit, instead of larger, + /// repreesentations are used in cbmc, this + /// is encoded using associated constants. + pub(super) type PermissionByte = u8; + pub(super) struct Permission; + impl Permission { + /// Unique ownership of a memory location + pub(super) const UNIQUE: u8 = 0; + /// Raw pointer read/write permission + pub(super) const SHAREDRW: u8 = 1; + /// Raw pointer read permission + pub(super) const SHAREDRO: u8 = 2; + /// Disabled -- no accesses allowed + pub(super) const DISABLED: u8 = 3; + } + + impl Permission { + /// Returns whether the access bit is granted by the permission + /// byte + pub(super) fn grants(access: AccessBit, perm: PermissionByte) -> bool { + perm != Permission::DISABLED + && (access != Access::WRITE || perm != Permission::SHAREDRO) + } + } + + /// Tracks whether the monitor is on or off. + /// Encoded as associated constants instead + /// of as an enum to ensure that the representation + /// uses 1 bit. + pub(super) type MonitorBit = bool; + pub(super) struct MonitorState; + impl MonitorState { + pub(super) const ON: MonitorBit = false; + pub(super) const OFF: MonitorBit = true; + } +} + +// The global state of the analysis. +mod global { + use super::limits::*; + use super::types::*; + use super::ShadowMem; + + pub(super) const INITIAL_TAG: PointerTag = 0; + + /// Associate every pointer object with a tag + pub(super) static mut TAGS: ShadowMem = ShadowMem::new(INITIAL_TAG); + + /// Associate every pointer object with a permission + pub(super) static mut PERMS: ShadowMem = ShadowMem::new(Permission::SHAREDRO); + + /// Next pointer id: the next pointer id in sequence + pub(super) static mut NEXT_TAG: PointerTag = INITIAL_TAG; + + /// Set to true whenever the stack has been + /// invalidated by a failed lookup. + pub(super) static mut STACK_VALID: bool = true; + + /// Object + offset being monitored + pub(super) static mut MONITORED: *const u8 = std::ptr::null(); + /// The tags of the pointer objects borrowing the byte + pub(super) static mut STACK_TAGS: [PointerTag; STACK_DEPTH] = [INITIAL_TAG; STACK_DEPTH]; + /// The permissions of the pointer objects borrowing the byte + pub(super) static mut STACK_PERMS: [PermissionByte; STACK_DEPTH] = + [Permission::UNIQUE; STACK_DEPTH]; + /// The "top" of the stack + pub(super) static mut STACK_TOP: usize = 0; +} + +#[rustc_diagnostic_item = "KaniStackValid"] +fn stack_valid() -> bool { + unsafe { global::STACK_VALID } +} + +/// Manipulation of the monitor of the stacked +/// borrows state +pub(super) mod monitor_transitions { + use super::global::*; + use super::limits::*; + use super::types::*; + use crate::mem::{pointer_object, pointer_offset}; + + fn demonic_nondet() -> bool { + crate::any() + } + + #[allow(unused)] + pub(super) const STACK_DEPTH: usize = 15; + + /// Initialize local when track local is true, picking a monitor, + /// and setting its object and offset to within pointer. + pub(super) unsafe fn track_local(tag: PointerTag, pointer: *const U) + where + U: Sized, + { + // Decide whether to initialize the stacks + // for location:location+size_of(U). + unsafe { + if demonic_nondet() { + let offset: usize = kani::any(); + crate::assume(offset < std::mem::size_of::()); + STACK_TOP = 1; + MONITORED = pointer.byte_add(offset) as *const u8; + STACK_TAGS[0] = tag; + STACK_PERMS[0] = Permission::UNIQUE; + } + } + } + + /// Push a tag with a permission perm at pointer + pub(super) unsafe fn push(tag: PointerTag, perm: PermissionByte, pointer: *const U) + where + U: Sized, + { + // Decide whether to initialize the stacks + // for location:location+size_of(U). + // Offset has already been picked earlier. + unsafe { + crate::assert(STACK_TOP < STACK_DEPTH, "Max # of nested borrows (15) exceeded"); + let size = std::mem::size_of_val_raw(pointer); + if pointer_object(MONITORED) == pointer_object(pointer) + && pointer_offset(MONITORED) <= size + { + STACK_TAGS[STACK_TOP] = tag; + STACK_PERMS[STACK_TOP] = perm; + STACK_TOP += 1; + } + } + } + + /// Run a stack check on the monitored byte for the given + /// tag and the given access permission. + pub(super) fn stack_check(tag: PointerTag, access: AccessBit) { + unsafe { + let mut found = false; + let mut j = 0; + let mut new_top = 0; + crate::assert(STACK_TOP < STACK_DEPTH, "Max # of nested borrows (15) exceeded"); + while j < STACK_DEPTH { + if j < STACK_TOP { + let id = STACK_TAGS[j]; + let kind = STACK_PERMS[j]; + if Permission::grants(access, kind) && id == tag { + new_top = j + 1; + found = true; + } + } + j += 1; + } + STACK_TOP = new_top; + STACK_VALID = STACK_VALID && found; + } + } +} + +/// Push the permissions at the given location +unsafe fn push(tag: types::PointerTag, perm: types::PermissionByte, address: *const U) { + self::monitor_transitions::push(tag, perm, address) +} + +/// Initialize the local stored at reference if initialized is set to false, +/// and track it using a monitor when using demonic nondeterminism. +/// +/// Every function call in the source program stack-allocates +/// the local variables that it uses; references to these +/// variables are only valid after these variables are initialized (first written). +/// Therefore this function can be used by supplying an initialized flag +/// set to true after the first write, a track flag set to the value +/// of a query to a demonic nondeterminism oracle (when this feature is used) +/// and a reference to the stack location. +#[rustc_diagnostic_item = "KaniInitializeLocal"] +fn initialize_local(pointer: *const U) { + unsafe { + let tag = global::NEXT_TAG; + global::TAGS.set(pointer, tag); + global::PERMS.set(pointer, types::Permission::UNIQUE); + global::NEXT_TAG += 1; + monitor_transitions::track_local(tag, pointer); + } +} + +/// Stack check the object pointed by pointer_value. +/// +/// This is done by checking `crate::mem::pointer_object` and +/// `crate::mem::pointer_offset`, which for arrays: +/// ```rust +/// let mut x: [i32; 100] = [0; 100]; +/// let x_ptr: *const [i32; 100] = std::ptr::addr_of!(x); +/// let y = &mut x[10]; +/// let y_ptr = y as *mut i32; +/// crate::assert(crate::mem::pointer_object(x_ptr) == +/// crate::mem::pointer_object(y_ptr), "pointers ="); +/// ``` +/// and for fields: +/// ```rust +/// struct TwoElements { +/// x: i32, +/// y: i32, +/// } +/// let mut x: TwoElements = TwoElements { x: 0, y: 0 }; +/// let x_ptr: *const TwoElements = std::ptr::addr_of!(x); +/// let y = &mut x.x; +/// let y_ptr = y as *mut i32; +/// crate::assert(crate::mem::pointer_object(x_ptr) == +/// crate::mem::pointer_object(y_ptr), "pointers ="); +/// ``` +/// will succeed, given that offsets within the same allocation +/// are considered parts of the same pointer object by cbmc. +#[rustc_diagnostic_item = "KaniStackCheckPtr"] +unsafe fn stack_check_ptr(pointer_value: *const *mut U) { + unsafe { + let pointer = *pointer_value; + let size = unsafe { std::mem::size_of_val_raw::(pointer) }; + if pointer_object(pointer) == pointer_object(global::MONITORED) + && pointer_offset(global::MONITORED) < size + { + let tag = global::TAGS.get(pointer_value); + let perm = global::PERMS.get(pointer_value); + if types::Permission::grants(types::Access::READ, perm) { + self::monitor_transitions::stack_check(tag, types::Access::READ); + } else if types::Permission::grants(types::Access::WRITE, perm) { + self::monitor_transitions::stack_check(tag, types::Access::WRITE); + } + } + } +} + +#[rustc_diagnostic_item = "KaniStackCheckRef"] +unsafe fn stack_check_ref(pointer_value: *const &mut U) { + stack_check_ptr(pointer_value as *const *mut U); +} + +/// Update the stacked borrows state for the case created: &mut T = &mut (referent:T) +/// by associating the location of the created value, stored at pointer_to_created, +/// with a new tag, and pushing the new tag to the created reference, stored at +/// pointer_to_val. +#[rustc_diagnostic_item = "KaniNewMutRefFromValue"] +fn new_mut_ref_from_value(pointer_to_created: *const &mut T, pointer_to_val: *const T) { + unsafe { + // Then associate the lvalue and push it + global::TAGS.set(pointer_to_created, global::NEXT_TAG); + global::PERMS.set(pointer_to_created, types::Permission::SHAREDRW); + push(global::NEXT_TAG, types::Permission::SHAREDRW, pointer_to_val); + global::NEXT_TAG += 1; + } +} + +/// Update the stacked borrows state for the case created = (reference: &mut T) as *mut T, +/// associating the location of the created value, stored at pointer_to_created, with a new +/// tag, running a stack check on the tag associated with the reference, accessed by +/// pointer_to_ref, and pushing the tag to the original location. +#[rustc_diagnostic_item = "KaniNewMutRawFromRef"] +fn new_mut_raw_from_ref(pointer_to_created: *const *mut T, pointer_to_ref: *const &mut T) { + unsafe { + // Then associate the lvalue and push it + global::TAGS.set(pointer_to_created, global::NEXT_TAG); + push(global::NEXT_TAG, types::Permission::SHAREDRW, *pointer_to_ref); + global::NEXT_TAG += 1; + } +} + +/// Update the stacked borrows state for the case created = (reference: &mut T) as *mut T, +/// associating the location of the created value, stored at pointer_to_created, with a new +/// tag, running a stack check on the tag associated with the reference, accessed by +/// pointer_to_ref, and pushing the tag to the original location. +#[rustc_diagnostic_item = "KaniNewMutRefFromRaw"] +fn new_mut_ref_from_raw(pointer_to_created: *const &mut T, pointer_to_ref: *const *mut T) { + unsafe { + // Then associate the lvalue and push it + global::TAGS.set(pointer_to_created, global::NEXT_TAG); + push(global::NEXT_TAG, types::Permission::SHAREDRW, *pointer_to_ref); + global::NEXT_TAG += 1; + } +} diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 59a89622a52d..d1ea796617e7 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -19,10 +19,13 @@ #![feature(ptr_metadata)] #![feature(f16)] #![feature(f128)] +// required for using size_of_val_raw +#![feature(layout_for_ptr)] // Allow us to use `kani::` to access crate features. extern crate self as kani; +mod aliasing; pub mod arbitrary; #[cfg(feature = "concrete_playback")] mod concrete_playback; diff --git a/tests/expected/aliasing/box.rs.fixme b/tests/expected/aliasing/box.rs.fixme new file mode 100644 index 000000000000..2e1e72171bde --- /dev/null +++ b/tests/expected/aliasing/box.rs.fixme @@ -0,0 +1,20 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zaliasing +// In the following code, the aliasing pattern +// is disallowed by stacked borrows. +// That is, since raw_1 borrows raw_2, +// write raw_2, followed by read raw_1, followed +// by write raw_2, causes an error: +// the scope of the borrow ends when raw_1 is written. + +#[kani::proof] +fn write_out_of_order_to_box() { + let x = Box::new(10); + let ref_x = Box::into_raw(x); + let raw_1 = ref_x as *mut i32; + let raw_2 = ref_x as *mut i32; + let _write = unsafe { *raw_2 = 100 }; + let _read = unsafe { *raw_1 }; + let _write = unsafe { *raw_2 = 110 }; +} diff --git a/tests/expected/aliasing/control_flow.expected b/tests/expected/aliasing/control_flow.expected new file mode 100644 index 000000000000..0f13dc515e6f --- /dev/null +++ b/tests/expected/aliasing/control_flow.expected @@ -0,0 +1 @@ +Failed Checks: Stacked borrows state invalidated at LineInfo { start_line: 37, start_col: 17, end_line: 37, end_col: 36 } diff --git a/tests/expected/aliasing/control_flow.rs b/tests/expected/aliasing/control_flow.rs new file mode 100644 index 000000000000..f9bc99340b3d --- /dev/null +++ b/tests/expected/aliasing/control_flow.rs @@ -0,0 +1,43 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zghost-state -Zaliasing + +// In the following code, +// ref_from_raw_1 and ref_from_raw_2 +// borrow from the memory location of local. +// In the second iteration of the loop, +// the write to ref_from_raw_2 should end the scope +// of ref_from_raw_1's borrow. +// When ref_from_raw_1 then is written, an aliasing +// error should be thrown. + +// This example is used as a litmus test to check +// that multiple basic blocks with non-linear +// control flow are instrumented properly + +#[allow(unused)] +#[kani::proof] +fn violation_within_control_flow() { + let mut local: i32 = 10; + let mut referent_1: i32 = 0; + let mut referent_2: i32 = 0; + let mut ref_from_raw_1: &mut i32 = &mut referent_1; + let mut ref_from_raw_2: &mut i32 = &mut referent_2; + let raw_pointer: *mut i32 = &mut local as *mut i32; + let mut state = false; + let mut iters = 0; + unsafe { + while iters < 2 { + if state { + ref_from_raw_1 = &mut *raw_pointer; + *ref_from_raw_1 = 0; + } else { + ref_from_raw_2 = &mut *raw_pointer; + *ref_from_raw_2 = 1; + *ref_from_raw_1 = 2; + } + state = true; + iters += 1; + } + } +} diff --git a/tests/expected/aliasing/duplicate_write.expected b/tests/expected/aliasing/duplicate_write.expected new file mode 100644 index 000000000000..63aeba869f3f --- /dev/null +++ b/tests/expected/aliasing/duplicate_write.expected @@ -0,0 +1,2 @@ + +Failed Checks: Stacked borrows state invalidated at LineInfo { start_line: 29, start_col: 9, end_line: 29, end_col: 28 } diff --git a/tests/expected/aliasing/duplicate_write.rs b/tests/expected/aliasing/duplicate_write.rs new file mode 100644 index 000000000000..e85be58ba1d2 --- /dev/null +++ b/tests/expected/aliasing/duplicate_write.rs @@ -0,0 +1,31 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zghost-state -Zaliasing + +// In the following code, +// ref_from_raw_1 and ref_from_raw_2 both +// borrow the memory location of local. +// After ref_from_raw_2 is written, ref_from_raw_1's +// borrow ends. +// The subsequent write to ref_from_raw_1 will cause an aliasing +// error. + +#[kani::proof] +fn use_after_borrow_ends() { + let mut local: i32; + let temp_ref: &mut i32; + let raw_pointer: *mut i32; + let ref_from_raw_1: &mut i32; + let ref_from_raw_2: &mut i32; + + local = 0; + temp_ref = &mut local; + raw_pointer = temp_ref as *mut i32; + unsafe { + ref_from_raw_1 = &mut *raw_pointer; + *ref_from_raw_1 = 0; + ref_from_raw_2 = &mut *raw_pointer; + *ref_from_raw_2 = 1; + *ref_from_raw_1 = 2; + } +} diff --git a/tests/expected/aliasing/duplicate_write_compressed.expected b/tests/expected/aliasing/duplicate_write_compressed.expected new file mode 100644 index 000000000000..acbb8d1e361d --- /dev/null +++ b/tests/expected/aliasing/duplicate_write_compressed.expected @@ -0,0 +1,2 @@ + +Failed Checks: Stacked borrows state invalidated at LineInfo { start_line: 18, start_col: 9, end_line: 18, end_col: 28 } diff --git a/tests/expected/aliasing/duplicate_write_compressed.rs b/tests/expected/aliasing/duplicate_write_compressed.rs new file mode 100644 index 000000000000..298accae8dcc --- /dev/null +++ b/tests/expected/aliasing/duplicate_write_compressed.rs @@ -0,0 +1,20 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zghost-state -Zaliasing + +// The following code is equivalent to duplicate_write, +// the only difference being that operations may be chained +// in one line. + +#[kani::proof] +fn main() { + let mut local: i32 = 0; + let raw_pointer = &mut local as *mut i32; + unsafe { + let ref_from_raw_1 = &mut *raw_pointer; + *ref_from_raw_1 = 0; + let ref_from_raw_2 = &mut *raw_pointer; + *ref_from_raw_2 = 1; + *ref_from_raw_1 = 2; + } +}