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/mod.rs

@@ -232,3 +232,80 @@ fn find_fn_def(tcx: TyCtxt, diagnostic: &str) -> Option<FnDef> {
     };
     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<T> {
+    /// 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<P, F, E>(&mut self, p: P, f: F) -> Result<&mut T, E>
+    where
+        F: FnOnce() -> Result<T, E>,
+        P: Fn(&T) -> bool;
+}
+
+impl<T> Cache<T> for Vec<T>
+where
+    T: PartialEq,
+{
+    fn try_get_or_insert<P, F, E>(&mut self, p: P, f: F) -> Result<&mut T, E>
+    where
+        F: FnOnce() -> Result<T, E>,
+        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<NamedFnDef>,
+}
+
+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)
+    }
+}

kani-compiler/src/kani_middle/reachability.rs

@@ -579,6 +579,7 @@ impl CallGraph {
 
     /// Print the graph in DOT format to a file.
     /// See <https://graphviz.org/doc/info/lang.html> 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<W: Write>(&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<W: Write>(&self, writer: &mut W, target: &str) -> std::io::Result<()> {
         let mut queue: Vec<Node> =
             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 {

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,24 +242,40 @@ 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<Operand>,
+        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<Operand>,
         destination: Place,
     ) {
         let new_bb = self.blocks.len();
         let span = source.span(&self.blocks);
-        let callee_op =
-            Operand::Copy(Place::from(self.new_local(callee.ty(), span, Mutability::Not)));
+        let callee_op = Operand::Copy(Place::from(callee));
         let kind = TerminatorKind::Call {
             func: callee_op,
             args,

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<T> = std::result::Result<T, super::MirError>;
+
+
+/// Caches function instances for later lookups.
+#[derive(Default, Debug)]
+pub struct Cache {
+    /// The cache
+    cache: Vec<NamedFnDef>,
+}
+
+fn try_get_or_insert<T, P, F>(vec: &mut Vec<T>, p: P, f: F) -> Result<&mut T>
+where
+    F: FnOnce() -> Result<T>,
+    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)
+    }
+}