bjoernager/rust
bjoernager/rust
1
Fork 0
Code Activity

Avoid extra copy by using retain_mut and moving the deletion into the closure

Browse source
This commit is contained in:
Johannes Hostert 2024-08-22 16:15:57 +02:00
parent 8b10bda1e4
commit 3a423fc6b7
No known key found for this signature in database
GPG key ID: 0BA6032B5A38D049
1 changed files with 24 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs
View file

@ -754,15 +754,9 @@ impl Tree {
// list of remaining children back in.
let mut children_of_node =
mem::take(&mut self.nodes.get_mut(*tag).unwrap().children);
// Remove all useless children, and save them for later.
// The closure needs `&self` and the loop below needs `&mut self`, so we need to `collect`
// in to a temporary list.
let to_remove: Vec<_> =
children_of_node.drain_filter(|x| self.is_useless(*x, live)).collect();
// Put back the now-filtered vector.
self.nodes.get_mut(*tag).unwrap().children = children_of_node;
// Now, all that is left is unregistering the children saved in `to_remove`.
for idx in to_remove {
// Remove all useless children.
children_of_node.retain_mut(|idx| {
if self.is_useless(*idx, live) {
// Note: In the rest of this comment, "this node" refers to `idx`.
// This node has no more children (if there were any, they have already been removed).
// It is also unreachable as determined by the GC, so we can remove it everywhere.
@ -771,12 +765,21 @@ impl Tree {
// (which are `self.nodes` and every range of `self.rperms`)
// before we can safely apply `UniKeyMap::remove` to truly remove
// this tag from the `tag_mapping`.
let node = self.nodes.remove(idx).unwrap();
let node = self.nodes.remove(*idx).unwrap();
for (_perms_range, perms) in self.rperms.iter_mut_all() {
perms.remove(idx);
perms.remove(*idx);
}
self.tag_mapping.remove(&node.tag);
// now delete it
false
} else {
// do nothing, but retain
true
}
});
// Put back the now-filtered vector.
self.nodes.get_mut(*tag).unwrap().children = children_of_node;
// We are done, the parent can continue.
stack.pop();
continue;