Module miri::borrow_tracker::tree_borrows::tree
source · Expand description
In this file we handle the “Tree” part of Tree Borrows, i.e. all tree traversal functions, optimizations to trim branches, and keeping track of the relative position of the access to each node being updated. This of course also includes the definition of the tree structure.
Functions here manipulate permissions but are oblivious to them: as
the internals of Permission
are private, the update process is a black
box. All we need to know here are
- the fact that updates depend only on the old state, the status of protectors, and the relative position of the access;
- idempotency properties asserted in
perms.rs
(for optimizations)
Structs
- Data given to the error handler
- Data for a single location.
- Node 🔒A node in the borrow tree. Each node is uniquely identified by a tag via the
nodes
map ofTree
. - Data given to the transition function
- Tree structure with both parents and children since we want to be able to traverse the tree efficiently in both directions.
- Internal contents of
Tree
with the minimum of mutable access for the purposes of the tree traversal functions: the permissions (perms
) can be updated but not the tree structure (tag_mapping
andnodes
)
Enums
- Relative position of the access
- Whether to continue exploring the children recursively or not.