mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Auto merge of #3532 - RalfJung:tb-protectors, r=RalfJung

Browse Source 
Tree Borrows: first apply transition, then check protector with new 'initialized'
This commit is contained in:
bors 2024-05-02 09:17:18 +00:00
commit ca3defe245
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs
View File

@ -106,6 +106,8 @@ fn perform_access(
let old_perm = self.permission;
let transition = Permission::perform_access(access_kind, rel_pos, old_perm, protected)
.ok_or(TransitionError::ChildAccessForbidden(old_perm))?;
self.initialized |= !rel_pos.is_foreign();
self.permission = transition.applied(old_perm).unwrap();
// Why do only initialized locations cause protector errors?
// Consider two mutable references `x`, `y` into disjoint parts of
// the same allocation. A priori, these may actually both be used to
@ -123,8 +125,6 @@ fn perform_access(
if protected && self.initialized && transition.produces_disabled() {
return Err(TransitionError::ProtectedDisabled(old_perm));
}
self.permission = transition.applied(old_perm).unwrap();
self.initialized |= !rel_pos.is_foreign();
Ok(transition)
}