Stacked Borrows in Kani

[jsalzbergedu]

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
6. Pointer manipulation is not yet modelled
7. Two phase borrows are not yet modelled.

Two phase borrows:
The rust compiler will desugar the following:

fn p(mut x: Vec<usize>) { x.push(x.len()) } 

to

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.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[jsalzbergedu]

This instrumentation also does not target optimal performance; there is no plan to use CBMC's shadow memory despite the fact that u8 are used to model pointer tags. Instead, Kani's shadow memory is used.

[artemagvanian]

Thanks! Having Stacked Borrows instrumentation in Kani is very cool!

It seems like the code uses a version of body mutation that is quite similar to MutableBody that we already have. I think integrating with current instrumentation (and improving it) is better than creating a different version of it. Moreover, I am not sure the instrumentation introduced in this PR actually works for any non-trivial CFG and there are no tests to convince me of the opposite.

I also added several small comments here and there.

[celinval]

Ok. I think I'm almost done reviewing the library changes. Thanks for your patience!

I think it will be very helpful if you add more tests with things like structure fields, arrays, more elaborated tests as well. Even if they don't pass today, it will be helpful to know how these cases are mitigated. It will also be helpful if you can add tests where the alias analysis finds no error and one that it finds multiple errors.