Stacked Borrows in Kani

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,
 }

kani-compiler/src/kani_middle/transform/check_aliasing/actions.rs

@@ -0,0 +1,237 @@
+// 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::{
+    BorrowKind, Local, LocalDecl, Mutability, Operand, Place, ProjectionElem, Rvalue, Statement,
+    StatementKind,
+};
+use stable_mir::ty::{RigidTy, Ty, TyKind};
+
+/// 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> {
+    actions: Vec<Action>,
+    /// 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 { actions: Vec::new(), locals }
+    }
+
+    /// Finalize the code actions to be taken
+    pub fn finalize(self) -> Vec<Action> {
+        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, _)) => {
+                // reborrow
+                self.actions.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.clone();
+                self.actions.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);
+            }
+            _ => { /* not yet handled */ }
+        }
+    }
+
+    /// 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.actions.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;
+            }
+        };
+        match self.locals[place.local].ty.kind() {
+            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);
+            }
+            _ => {}
+        }
+    }
+
+    /// 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
+            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(_) => {}
+        }
+    }
+
+    /// 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);
+            }
+            StatementKind::FakeRead(_, _) => {}
+            StatementKind::SetDiscriminant { .. } => {}
+            StatementKind::Deinit(_) => {}
+            StatementKind::StorageLive(_) => {}
+            StatementKind::StorageDead(_) => {}
+            StatementKind::Retag(_, _) => {}
+            StatementKind::PlaceMention(_) => {}
+            StatementKind::AscribeUserType { .. } => {}
+            StatementKind::Coverage(_) => {}
+            StatementKind::Intrinsic(_) => {}
+            StatementKind::ConstEvalCounter => {}
+            StatementKind::Nop => {}
+        }
+    }
+
+    /// 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
+    pub fn visit_statement(&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);
+                    }
+                }
+            }
+            // The following are not yet handled, however, no info is printed
+            // to avoid blowups:
+            StatementKind::Retag(_, _) => {}
+            StatementKind::FakeRead(_, _) => {}
+            StatementKind::SetDiscriminant { .. } => {}
+            StatementKind::Deinit(_) => {}
+            StatementKind::StorageLive(_) => {}
+            StatementKind::StorageDead(_) => {}
+            StatementKind::PlaceMention(_) => {}
+            StatementKind::AscribeUserType { .. } => {}
+            StatementKind::Coverage(_) => {}
+            StatementKind::Intrinsic(_) => {}
+            StatementKind::ConstEvalCounter => {}
+            StatementKind::Nop => {}
+        }
+    }
+}

kani-compiler/src/kani_middle/transform/check_aliasing/function_cache.rs

@@ -0,0 +1,90 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! This module contains a cache of resolved generic functions
+
+use super::{MirError, MirInstance};
+use crate::kani_middle::find_fn_def;
+use rustc_middle::ty::TyCtxt;
+use stable_mir::ty::{GenericArgKind as GenericArg, GenericArgs};
+
+/// FunctionSignature encapsulates the data
+/// for rust functions with generic arguments
+/// to ensure that it can be cached.
+#[derive(Clone, Debug, Eq, PartialEq)]
+pub struct Signature {
+    /// The diagnostic string associated with the function
+    diagnostic: String,
+    /// The generic arguments applied
+    args: Vec<GenericArg>,
+}
+
+impl Signature {
+    /// Create a new signature from the name and args
+    pub fn new(name: &str, args: &[GenericArg]) -> Signature {
+        Signature { diagnostic: name.to_string(), args: args.to_vec() }
+    }
+}
+
+/// FunctionInstance encapsulates the
+/// data for a resolved rust function with
+/// generic arguments to ensure that it can be cached.
+#[derive(Clone, Debug, Eq, PartialEq)]
+pub struct Instance {
+    /// The "key" with which the function instance
+    /// is created, and with which the function instance
+    /// can be looked up
+    signature: Signature,
+    /// The "value", the resolved function instance itself
+    instance: MirInstance,
+}
+
+impl Instance {
+    /// Create a new cacheable instance with the given signature and
+    /// instance
+    pub fn new(signature: Signature, instance: MirInstance) -> Instance {
+        Instance { signature, instance }
+    }
+}
+
+/// Caches function instances for later lookups.
+#[derive(Default, Debug)]
+pub struct Cache {
+    /// The cache
+    cache: Vec<Instance>,
+}
+
+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> {
+        let Cache { cache } = self;
+        for i in 0..cache.len() {
+            if sig == cache[i].signature {
+                return Ok(&cache[i].instance);
+            }
+        }
+        let fndef = find_fn_def(*ctx, &sig.diagnostic)
+            .ok_or(MirError::new(format!("Not found: {}", &sig.diagnostic)))?;
+        let instance = MirInstance::resolve(fndef, &GenericArgs(sig.args.clone()))?;
+        cache.push(Instance::new(sig, instance));
+        Ok(&cache[cache.len() - 1].instance)
+    }
+
+    /// Register the kani assertion function
+    pub fn register_assert(&mut self, ctx: &TyCtxt) -> Result<&MirInstance, MirError> {
+        let diagnostic = "KaniAssert".to_string();
+        let args = vec![];
+        let sig = Signature { diagnostic, args };
+        let Cache { cache } = self;
+        for i in 0..cache.len() {
+            if sig == cache[i].signature {
+                return Ok(&cache[i].instance);
+            }
+        }
+        let fndef = find_fn_def(*ctx, &sig.diagnostic)
+            .ok_or(MirError::new(format!("Not found: {}", &sig.diagnostic)))?;
+        let instance = super::MirInstance::resolve(fndef, &GenericArgs(sig.args.clone()))?;
+        cache.push(Instance::new(sig, instance));
+        Ok(&cache[cache.len() - 1].instance)
+    }
+}