From ffaa0bd642fd7002e9c8a1bcab4547cbb418b861 Mon Sep 17 00:00:00 2001 From: Jacob Salzberg Date: Fri, 30 Aug 2024 17:30:05 -0400 Subject: [PATCH] Stacked Borrows in Kani (#3406) This PR adds stacked borrows to Kani, strengthening its model of pointers to detect violations of Rust's aliasing model. It does this by automatically instrumenting code with hooks at every stack and heap allocation, ensuring that a live mutable pointer is never aliased. This instrumentation is subject to several limitations: 1. Currently, function calls are not permitted. To implement them, the "protector" mechanism of the stacked borrows calculus has to be implemented first. 2. Only one byte is monitored; it is picked nondeterministic-ally at the beginning of the instrumented code. Function contracts may need to keep track of relations between multiple references and raw pointers in their pre & post conditions, and are therefore not yet tracked. 3. The address of locals is taken before they are initialized; because of this, optimizations to the "local storage" part of the stack frame may break this analysis. In our cases so far, no such optimizations are performed. It also means that initialization must be checked separately using the Uninit pass 4. Arrays are not yet modelled 5. Malloc is not yet modelled 7. Pointer manipulation is not yet modelled 8. Two phase borrows are not yet modelled. Two phase borrows: The rust compiler will desugar the following: ```rust fn p(mut x: Vec) { x.push(x.len()) } ``` to ```rust fn p(mut x: Vec) { let y: &mut Vec = &mut x; let z: usize = Vec::len(x); Vec::push(y, z) } ``` Marking the borrow into y as "two phase." This may be enabled in the future via a hack (ref: https://www.ralfj.de/blog/2023/06/02/tree-borrows.html) and so the aliasing model may in the future change to accommodate these differently. 10. There are numerous unhandled syntactic constructs. - Assignments that Copy/Move - Terminators - Fields - Arrays/Slices/Indices These constructs _must_ be handled in the future to say that we have ported stacked borrows to Kani. Currently, print statements are made; these constructs are expected to do pointer manipulation, but to no effect. In the future, we will want to instrument all of these. We need 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: Jacob Salzberg --- kani-compiler/src/args.rs | 2 + kani-compiler/src/kani_middle/mod.rs | 77 ++++ kani-compiler/src/kani_middle/reachability.rs | 12 + .../src/kani_middle/transform/body.rs | 86 +++- .../check_aliasing/function_cache.rs | 54 +++ .../check_aliasing/instrumentation.rs | 425 ++++++++++++++++++ .../transform/check_aliasing/mod.rs | 132 ++++++ .../transform/check_aliasing/visitor.rs | 253 +++++++++++ .../src/kani_middle/transform/mod.rs | 4 + kani-driver/src/call_single_file.rs | 6 + kani_metadata/src/unstable.rs | 2 + library/kani/src/aliasing.rs | 361 +++++++++++++++ library/kani/src/lib.rs | 3 + tests/expected/aliasing/box.rs.fixme | 20 + tests/expected/aliasing/control_flow.expected | 1 + tests/expected/aliasing/control_flow.rs | 43 ++ .../aliasing/duplicate_write.expected | 2 + tests/expected/aliasing/duplicate_write.rs | 31 ++ .../duplicate_write_compressed.expected | 2 + .../aliasing/duplicate_write_compressed.rs | 20 + 20 files changed, 1512 insertions(+), 24 deletions(-) create mode 100644 kani-compiler/src/kani_middle/transform/check_aliasing/function_cache.rs create mode 100644 kani-compiler/src/kani_middle/transform/check_aliasing/instrumentation.rs create mode 100644 kani-compiler/src/kani_middle/transform/check_aliasing/mod.rs create mode 100644 kani-compiler/src/kani_middle/transform/check_aliasing/visitor.rs create mode 100644 library/kani/src/aliasing.rs create mode 100644 tests/expected/aliasing/box.rs.fixme create mode 100644 tests/expected/aliasing/control_flow.expected create mode 100644 tests/expected/aliasing/control_flow.rs create mode 100644 tests/expected/aliasing/duplicate_write.expected create mode 100644 tests/expected/aliasing/duplicate_write.rs create mode 100644 tests/expected/aliasing/duplicate_write_compressed.expected create mode 100644 tests/expected/aliasing/duplicate_write_compressed.rs 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; + } +}