6 ms·
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 compile
by vollbrecht 1y 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 };
}
- Arnavion 1y agoStacked 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.
- vollbrecht 1y agoAh that make sense. Thanks for clarifying.
- haberman 1y agoThe 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?
- ethan_smith 1y agoThe 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.