diff --git a/kani-compiler/src/kani_middle/transform/check_aliasing/actions.rs b/kani-compiler/src/kani_middle/transform/check_aliasing/actions.rs index 3e735307b47d..dc629bd1e0b9 100644 --- a/kani-compiler/src/kani_middle/transform/check_aliasing/actions.rs +++ b/kani-compiler/src/kani_middle/transform/check_aliasing/actions.rs @@ -6,8 +6,8 @@ //! statements of the code. use stable_mir::mir::{ - BorrowKind, Local, LocalDecl, Mutability, Operand, ProjectionElem, Rvalue, - Statement, StatementKind, Place, + BorrowKind, Local, LocalDecl, Mutability, Operand, Place, ProjectionElem, Rvalue, Statement, + StatementKind, }; use stable_mir::ty::{RigidTy, Ty, TyKind}; @@ -47,11 +47,7 @@ impl<'locals> CollectActions<'locals> { match self.locals[rvalue].ty.kind() { TyKind::RigidTy(RigidTy::Ref(_, ty, _)) | TyKind::RigidTy(RigidTy::RawPtr(ty, _)) => { // reborrow - self.actions.push(Action::NewMutRefFromRaw { - lvalue, - rvalue, - ty, - }); + self.actions.push(Action::NewMutRefFromRaw { lvalue, rvalue, ty }); } _ => {} } @@ -67,7 +63,7 @@ impl<'locals> CollectActions<'locals> { let lvalue = to; let rvalue = from.local.clone(); self.actions.push(Action::NewStackReference { lvalue, rvalue }); - }, + } [ProjectionElem::Deref] => { // Reborrow // x : &mut T = &*(y : *mut T OR &mut T) @@ -93,14 +89,13 @@ impl<'locals> CollectActions<'locals> { let lvalue = to; match self.locals[rvalue].ty.kind() { TyKind::RigidTy(RigidTy::Ref(_, ty, _)) => { - self.actions.push(Action::NewMutRawFromRef { - lvalue, - rvalue, - ty, - }); + self.actions.push(Action::NewMutRawFromRef { lvalue, rvalue, ty }); } _ => { - panic!("Dereference of rvalue case not yet handled for raw pointers {:?}", from); + panic!( + "Dereference of rvalue case not yet handled for raw pointers {:?}", + from + ); } } } @@ -116,10 +111,10 @@ impl<'locals> CollectActions<'locals> { [] => { // Direct usage -- no update needed return; - }, + } [ProjectionElem::Deref] => { // Dereference -- instrument stack check - }, + } _ => { // Field access -- not yet handled. return; @@ -129,12 +124,12 @@ impl<'locals> CollectActions<'locals> { TyKind::RigidTy(RigidTy::Ref(_, ty, _)) => { self.actions.push(Action::StackUpdateReference { place: place.local, ty }); self.actions.push(Action::StackCheck); - }, + } TyKind::RigidTy(RigidTy::RawPtr(ty, _)) => { self.actions.push(Action::StackUpdatePointer { place: place.local, ty }); self.actions.push(Action::StackCheck); - }, - _ => {}, + } + _ => {} } } @@ -143,24 +138,24 @@ impl<'locals> CollectActions<'locals> { match rvalue { Rvalue::AddressOf(_, place) => { self.visit_place(place); - }, + } Rvalue::Ref(_, _, place) => { self.visit_place(place); } // The rest are not yet handled - Rvalue::Aggregate(_, _) => {}, - Rvalue::BinaryOp(_, _, _) => {}, - Rvalue::Cast(_, _, _) => {}, - Rvalue::CheckedBinaryOp(_, _, _) => {}, - Rvalue::CopyForDeref(_) => {}, - Rvalue::Discriminant(_) => {}, - Rvalue::Len(_) => {}, - Rvalue::Repeat(_, _) => {}, - Rvalue::ShallowInitBox(_, _) => {}, - Rvalue::ThreadLocalRef(_) => {}, - Rvalue::NullaryOp(_, _) => {}, - Rvalue::UnaryOp(_, _) => {}, - Rvalue::Use(_) => {}, + Rvalue::Aggregate(_, _) => {} + Rvalue::BinaryOp(_, _, _) => {} + Rvalue::Cast(_, _, _) => {} + Rvalue::CheckedBinaryOp(_, _, _) => {} + Rvalue::CopyForDeref(_) => {} + Rvalue::Discriminant(_) => {} + Rvalue::Len(_) => {} + Rvalue::Repeat(_, _) => {} + Rvalue::ShallowInitBox(_, _) => {} + Rvalue::ThreadLocalRef(_) => {} + Rvalue::NullaryOp(_, _) => {} + Rvalue::UnaryOp(_, _) => {} + Rvalue::Use(_) => {} } } @@ -171,18 +166,18 @@ impl<'locals> CollectActions<'locals> { self.visit_rvalue_places(rvalue); self.visit_place(place); } - StatementKind::FakeRead(_, _) => {}, - StatementKind::SetDiscriminant { .. } => {}, - StatementKind::Deinit(_) => {}, - StatementKind::StorageLive(_) => {}, - StatementKind::StorageDead(_) => {}, - StatementKind::Retag(_, _) => {}, - StatementKind::PlaceMention(_) => {}, - StatementKind::AscribeUserType { .. } => {}, - StatementKind::Coverage(_) => {}, - StatementKind::Intrinsic(_) => {}, - StatementKind::ConstEvalCounter => {}, - StatementKind::Nop => {}, + StatementKind::FakeRead(_, _) => {} + StatementKind::SetDiscriminant { .. } => {} + StatementKind::Deinit(_) => {} + StatementKind::StorageLive(_) => {} + StatementKind::StorageDead(_) => {} + StatementKind::Retag(_, _) => {} + StatementKind::PlaceMention(_) => {} + StatementKind::AscribeUserType { .. } => {} + StatementKind::Coverage(_) => {} + StatementKind::Intrinsic(_) => {} + StatementKind::ConstEvalCounter => {} + StatementKind::Nop => {} } } 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 index e9e589053c61..7bbbabf68fd1 100644 --- a/kani-compiler/src/kani_middle/transform/check_aliasing/function_cache.rs +++ b/kani-compiler/src/kani_middle/transform/check_aliasing/function_cache.rs @@ -2,10 +2,10 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! This module contains a cache of resolved generic functions -use super::{MirInstance, MirError}; +use super::{MirError, MirInstance}; +use crate::kani_middle::find_fn_def; use rustc_middle::ty::TyCtxt; use stable_mir::ty::{GenericArgKind as GenericArg, GenericArgs}; -use crate::kani_middle::find_fn_def; /// FunctionSignature encapsulates the data /// for rust functions with generic arguments @@ -56,8 +56,7 @@ pub struct Cache { impl Cache { /// Register the signature the to the cache /// in the given compilation context, ctx - pub fn register(&mut self, ctx: &TyCtxt, sig: Signature) -> - Result<&MirInstance, MirError> { + pub fn register(&mut self, ctx: &TyCtxt, sig: Signature) -> Result<&MirInstance, MirError> { let Cache { cache } = self; for i in 0..cache.len() { if sig == cache[i].signature { @@ -72,8 +71,7 @@ impl Cache { } /// Register the kani assertion function - pub fn register_assert(&mut self, ctx: &TyCtxt) -> - Result<&MirInstance, MirError> { + pub fn register_assert(&mut self, ctx: &TyCtxt) -> Result<&MirInstance, MirError> { let diagnostic = "KaniAssert".to_string(); let args = vec![]; let sig = Signature { diagnostic, args }; diff --git a/kani-compiler/src/kani_middle/transform/check_aliasing/instrumentation.rs b/kani-compiler/src/kani_middle/transform/check_aliasing/instrumentation.rs index 9ace574c9378..65b2a5dc6e04 100644 --- a/kani-compiler/src/kani_middle/transform/check_aliasing/instrumentation.rs +++ b/kani-compiler/src/kani_middle/transform/check_aliasing/instrumentation.rs @@ -7,14 +7,16 @@ //! are instrumented, and that no code that is added by the instrumentation //! pass itself is instrumented or analyzed. -use std::collections::HashMap; -use rustc_middle::ty::TyCtxt; -use stable_mir::mir::{Body, Local, Mutability, Operand, Place, Rvalue, Terminator, TerminatorKind, UnwindAction}; -use stable_mir::ty::{GenericArgKind, Ty, Span}; use crate::kani_middle::transform::body::{CheckType, InsertPosition}; +use rustc_middle::ty::TyCtxt; +use stable_mir::mir::{ + Body, Local, Mutability, Operand, Place, Rvalue, Terminator, TerminatorKind, UnwindAction, +}; +use stable_mir::ty::{GenericArgKind, Span, Ty}; +use std::collections::HashMap; -use super::{Action, Cache, CollectActions, MirError, MirInstance, Signature}; use super::super::body::{MutableBody, SourceInstruction}; +use super::{Action, Cache, CollectActions, MirError, MirInstance, Signature}; type Result = std::result::Result; @@ -62,7 +64,7 @@ impl<'tcx, 'cache> InstrumentationData<'tcx, 'cache> { 0 => { source = SourceInstruction::Terminator { bb: 0 }; span = body.blocks()[0].terminator.span; - }, + } _ => { source = SourceInstruction::Statement { idx: 0, bb: 0 }; span = body.blocks()[0].terminator.span; @@ -84,14 +86,30 @@ impl<'tcx, 'cache> InstrumentationData<'tcx, 'cache> { 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); + let valid = body.new_local( + Ty::from_rigid_kind(stable_mir::ty::RigidTy::Bool), + span, + Mutability::Mut, + ); let bb = body.blocks().len() - 1; let min_processed = match body.blocks()[bb].statements.len() { 0 => SourceInstruction::Terminator { bb }, - n => SourceInstruction::Statement { idx: n - 1, bb } + n => SourceInstruction::Statement { idx: n - 1, bb }, }; let ghost_index = SourceInstruction::Terminator { bb: 0 }; - InstrumentationData { tcx, cache, meta_stack, local_count, unit, valid, fn_pointers, span, min_processed, ghost_index, body } + InstrumentationData { + tcx, + cache, + meta_stack, + local_count, + unit, + valid, + fn_pointers, + span, + min_processed, + ghost_index, + body, + } } /// Register the function described by the diagnostic @@ -103,7 +121,8 @@ impl<'tcx, 'cache> InstrumentationData<'tcx, 'cache> { let body = &mut self.body; let span = self.span.clone(); let instance = cache.register(tcx, callee)?; - let func_local = fn_pointers.entry(*instance) + let func_local = fn_pointers + .entry(*instance) .or_insert_with(|| body.new_local(instance.ty(), span, Mutability::Not)); Ok(*func_local) } @@ -112,10 +131,7 @@ impl<'tcx, 'cache> InstrumentationData<'tcx, 'cache> { /// 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, - callee: Signature, - args: Vec, - dest: Local) -> Result<()> { + pub fn call(&mut self, callee: Signature, args: Vec, dest: Local) -> Result<()> { let func_local = self.register_fn(callee)?; let new_bb = self.body.blocks().len(); let span = self.body.blocks()[self.min_processed.bb()].terminator.span; @@ -142,7 +158,12 @@ impl<'tcx, 'cache> InstrumentationData<'tcx, 'cache> { pub fn assign_pointer(&mut self, lvalue: Local, rvalue: Local) { let source = &mut self.ghost_index; let position = InsertPosition::After; - self.body.assign_to(Place::from(lvalue), Rvalue::AddressOf(Mutability::Not, Place::from(rvalue)), source, position); + self.body.assign_to( + Place::from(lvalue), + Rvalue::AddressOf(Mutability::Not, Place::from(rvalue)), + source, + position, + ); } /// For some local, say let x: T; @@ -154,11 +175,17 @@ impl<'tcx, 'cache> InstrumentationData<'tcx, 'cache> { let ptr_ty = Ty::new_ptr(ty, Mutability::Not); let span = self.span.clone(); let body = &mut self.body; - let local_ptr = - self.meta_stack.entry(local).or_insert_with(|| body.new_local(ptr_ty, span, Mutability::Not)); + let local_ptr = self + .meta_stack + .entry(local) + .or_insert_with(|| body.new_local(ptr_ty, span, Mutability::Not)); let local_ptr = *local_ptr; self.assign_pointer(local_ptr, local); - self.call(Signature::new("KaniInitializeLocal", &[GenericArgKind::Type(ty)]), vec![local_ptr], self.unit)?; + self.call( + Signature::new("KaniInitializeLocal", &[GenericArgKind::Type(ty)]), + vec![local_ptr], + self.unit, + )?; Ok(()) } @@ -206,7 +233,7 @@ impl<'tcx, 'cache> InstrumentationData<'tcx, 'cache> { body.replace_terminator(&execute_terminator_block, original); self.ghost_index = execute_ghost_block; - }, + } SourceInstruction::Statement { idx, bb } => { // In this case it is simple, merely goto the ghost code // immdediately. @@ -225,16 +252,16 @@ impl<'tcx, 'cache> InstrumentationData<'tcx, 'cache> { /// lvalue = &rvalue /// with an update to the stacked borrows state, /// at the code index source. - pub fn instrument_new_stack_reference( - &mut self, - lvalue: Local, - rvalue: Local, - ) -> Result<()> { + pub fn instrument_new_stack_reference(&mut self, 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.call(Signature::new("KaniNewMutRefFromValue", &[GenericArgKind::Type(ty)]), vec![*lvalue_ref, *rvalue_ref], self.unit)?; + self.call( + Signature::new("KaniNewMutRefFromValue", &[GenericArgKind::Type(ty)]), + vec![*lvalue_ref, *rvalue_ref], + self.unit, + )?; Ok(()) } @@ -245,36 +272,47 @@ impl<'tcx, 'cache> InstrumentationData<'tcx, 'cache> { SourceInstruction::Terminator { bb } => self.body.blocks()[bb].terminator.span, }; self.call(Signature::new("KaniStackValid", &[]), vec![], self.valid)?; - let msg = format!("Stacked borrows aliasing model violated at {:?}:{:?}", span.get_filename(), span.get_lines()); + let msg = format!( + "Stacked borrows aliasing model violated at {:?}:{:?}", + span.get_filename(), + span.get_lines() + ); let check_fn = self.cache.register_assert(&self.tcx)?; let check_type = &CheckType::Assert(*check_fn); - self.body.insert_check(self.tcx, check_type, &mut self.ghost_index, InsertPosition::After, self.valid, &msg); + self.body.insert_check( + self.tcx, + check_type, + &mut self.ghost_index, + InsertPosition::After, + 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, - place: Local, - ty: Ty, - ) -> Result<()> { + pub fn instrument_stack_update_ref(&mut self, place: Local, ty: Ty) -> Result<()> { // Initialize the constants let place_ref = self.meta_stack.get(&place).unwrap(); - self.call(Signature::new("KaniStackCheckRef", &[GenericArgKind::Type(ty)]), vec![*place_ref], self.unit)?; + self.call( + Signature::new("KaniStackCheckRef", &[GenericArgKind::Type(ty)]), + vec![*place_ref], + self.unit, + )?; Ok(()) } /// Instrument a validity assertion on the stacked borrows state /// at idx for (place: *const T). - pub fn instrument_stack_update_ptr( - &mut self, - place: Local, - ty: Ty, - ) -> Result<()> { + pub fn instrument_stack_update_ptr(&mut self, place: Local, ty: Ty) -> Result<()> { // Initialize the constants let place_ref = self.meta_stack.get(&place).unwrap(); - self.call(Signature::new("KaniStackCheckPtr", &[GenericArgKind::Type(ty)]), vec![*place_ref], self.unit)?; + self.call( + Signature::new("KaniStackCheckPtr", &[GenericArgKind::Type(ty)]), + vec![*place_ref], + self.unit, + )?; Ok(()) } @@ -289,7 +327,11 @@ impl<'tcx, 'cache> InstrumentationData<'tcx, 'cache> { // Initialize the constants let created_ref = self.meta_stack.get(&created).unwrap(); let reference_ref = self.meta_stack.get(&raw).unwrap(); - self.call(Signature::new("KaniNewMutRefFromRaw", &[GenericArgKind::Type(ty)]), vec![*created_ref, *reference_ref], self.unit)?; + self.call( + Signature::new("KaniNewMutRefFromRaw", &[GenericArgKind::Type(ty)]), + vec![*created_ref, *reference_ref], + self.unit, + )?; Ok(()) } @@ -304,7 +346,11 @@ impl<'tcx, 'cache> InstrumentationData<'tcx, 'cache> { // Initialize the constants let created_ref = self.meta_stack.get(&created).unwrap(); let reference_ref = self.meta_stack.get(&reference).unwrap(); - self.call(Signature::new("KaniNewMutRawFromRef", &[GenericArgKind::Type(ty)]), vec![*created_ref, *reference_ref], self.unit)?; + self.call( + Signature::new("KaniNewMutRawFromRef", &[GenericArgKind::Type(ty)]), + vec![*created_ref, *reference_ref], + self.unit, + )?; Ok(()) } @@ -321,7 +367,7 @@ impl<'tcx, 'cache> InstrumentationData<'tcx, 'cache> { pub fn instruction_actions(&self) -> Vec { let mut visitor = CollectActions::new(self.body.locals()); match self.min_processed { - SourceInstruction::Terminator { .. } => { /* not yet handled */ }, + SourceInstruction::Terminator { .. } => { /* not yet handled */ } SourceInstruction::Statement { idx, bb } => { visitor.visit_statement(&self.body.blocks()[bb].statements[idx]); } @@ -334,11 +380,19 @@ impl<'tcx, 'cache> InstrumentationData<'tcx, 'cache> { fn instrument_action(&mut self, action: Action) -> Result<()> { match action { Action::StackCheck => self.instrument_stack_check(), - Action::NewStackReference { lvalue, rvalue } => self.instrument_new_stack_reference(lvalue, rvalue), - Action::StackUpdateReference { place, ty } => self.instrument_stack_update_ref(place, ty), - Action::NewMutRefFromRaw { lvalue, rvalue, ty } => self.instrument_new_mut_ref_from_raw(lvalue, rvalue, ty), + Action::NewStackReference { lvalue, rvalue } => { + self.instrument_new_stack_reference(lvalue, rvalue) + } + Action::StackUpdateReference { place, ty } => { + self.instrument_stack_update_ref(place, ty) + } + Action::NewMutRefFromRaw { lvalue, rvalue, ty } => { + self.instrument_new_mut_ref_from_raw(lvalue, rvalue, ty) + } Action::StackUpdatePointer { place, ty } => self.instrument_stack_update_ptr(place, ty), - Action::NewMutRawFromRef { lvalue, rvalue, ty } => self.instrument_new_mut_raw_from_ref(lvalue, rvalue, ty), + Action::NewMutRawFromRef { lvalue, rvalue, ty } => { + self.instrument_new_mut_raw_from_ref(lvalue, rvalue, ty) + } } } @@ -357,13 +411,29 @@ impl<'tcx, 'cache> InstrumentationData<'tcx, 'cache> { self.instrument_action(action)?; } self.min_processed = match self.min_processed { - SourceInstruction::Statement { idx: 0, bb: 0 } => { break; }, - SourceInstruction::Statement { idx: 0, bb } => SourceInstruction::Terminator { bb: bb - 1 }, - SourceInstruction::Statement { idx, bb } => SourceInstruction::Statement { idx: idx - 1, bb }, - SourceInstruction::Terminator { bb } if self.body.blocks()[bb].statements.len() > 0 => - SourceInstruction::Statement { idx: self.body.blocks()[bb].statements.len() - 1, bb }, - SourceInstruction::Terminator { bb } if bb > 0 => SourceInstruction::Terminator { bb: bb - 1 }, - SourceInstruction::Terminator { .. } => { break; } + SourceInstruction::Statement { idx: 0, bb: 0 } => { + break; + } + SourceInstruction::Statement { idx: 0, bb } => { + SourceInstruction::Terminator { bb: bb - 1 } + } + SourceInstruction::Statement { idx, bb } => { + SourceInstruction::Statement { idx: idx - 1, bb } + } + SourceInstruction::Terminator { bb } + if self.body.blocks()[bb].statements.len() > 0 => + { + SourceInstruction::Statement { + idx: self.body.blocks()[bb].statements.len() - 1, + bb, + } + } + SourceInstruction::Terminator { bb } if bb > 0 => { + SourceInstruction::Terminator { bb: bb - 1 } + } + SourceInstruction::Terminator { .. } => { + break; + } } } Ok(()) diff --git a/kani-compiler/src/kani_middle/transform/check_aliasing/mod.rs b/kani-compiler/src/kani_middle/transform/check_aliasing/mod.rs index 869417454f0c..0f30c1ff51f3 100644 --- a/kani-compiler/src/kani_middle/transform/check_aliasing/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_aliasing/mod.rs @@ -121,8 +121,14 @@ impl GlobalPass for GlobalAliasingPass { let mut found = HashSet::new(); // Collect for instance in &instances { - if instance.def.all_attrs().into_iter().fold(false, |is_proof, attr| is_proof || attr.as_str().contains("kanitool::proof")) { - let (items, _) = collect_reachable_items(tcx, transformer, &[MonoItem::Fn(*instance)]); + if instance + .def + .all_attrs() + .into_iter() + .fold(false, |is_proof, attr| is_proof || attr.as_str().contains("kanitool::proof")) + { + let (items, _) = + collect_reachable_items(tcx, transformer, &[MonoItem::Fn(*instance)]); for item in items { if let MonoItem::Fn(instance) = item { found.insert(instance); @@ -136,11 +142,8 @@ impl GlobalPass for GlobalAliasingPass { if found.contains(instance) { found.remove(instance); 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)); + let (_, body) = pass.transform(tcx, transformer.body(tcx, *instance), *instance); + transformer.cache.insert(*instance, TransformationResult::Modified(body)); } } } diff --git a/library/kani/src/aliasing.rs b/library/kani/src/aliasing.rs index 240d9d6d1447..3243f67634d2 100644 --- a/library/kani/src/aliasing.rs +++ b/library/kani/src/aliasing.rs @@ -75,7 +75,7 @@ static mut STACK_VALID: bool = true; #[rustc_diagnostic_item = "KaniStackValid"] fn stack_valid() -> bool { - unsafe {STACK_VALID} + unsafe { STACK_VALID } } /// Type of access. @@ -282,10 +282,7 @@ fn new_mut_ref_from_value(pointer_to_created: *const &mut T, pointer_to_val: /// 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, -) { +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 TAGS.set(pointer_to_created, NEXT_TAG); @@ -299,10 +296,7 @@ fn new_mut_raw_from_ref( /// 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, -) { +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 TAGS.set(pointer_to_created, NEXT_TAG);