Comment by vollbrecht
3 days ago
Hmm i just tested out the claim that the following rust code would be rejected ( Example 4 in the paper).
And it seams to not be the case on the stable compiler version?
fn write(x: &mut i32) {*x = 10}
fn main() {
let x = &mut 0;
let y = x as *mut i32;
//write(x); // this should use the mention implicit twophase borrow
*x = 10; // this should not and therefore be rejected by the compiler
unsafe {*y = 15 };
}
Stacked borrows is miri's runtime model. Run it under miri and you will see the error reported for the `*x = 10;` version but not the `write(x);` version - "Undefined Behavior: attempting a write access using [...] but that tag does not exist in the borrow stack for this location".
rustc itself has no reason to reject either version, because y is a *mut and thus has no borrow/lifetime relation to the &mut that x is, from a compile-time/typesystem perspective.
Ah that make sense. Thanks for clarifying.
The paper mentions that the authors implemented tree borrows in Miri. Is this change likely to be adopted by Miri as the default model going forward?
The paper is describing the behavior under the proposed Tree Borrows model, not the current borrow checker implementation which uses a more limited analysis that doesn't detect this particular conflict between the raw pointer and mutable reference.