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<usize>) { x.push(x.len()) } 
```
to
```rust
fn p(mut x: Vec<usize>) {
  let y: &mut Vec<i32> = &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 <salzber@amazon.com>

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)
+ }
+}