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

  • ErrHandlerArgs 🔒
    Data given to the error handler
  • LocationState 🔒
    Data for a single location.
  • Node 🔒
    A node in the borrow tree. Each node is uniquely identified by a tag via the nodes map of Tree.
  • NodeAppArgs 🔒
    Data given to the transition function
  • Tree
    Tree structure with both parents and children since we want to be able to traverse the tree efficiently in both directions.
  • TreeVisitor 🔒
    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 and nodes)

Enums