Module places_conflict

The borrowck rules for proving disjointness are applied from the “root” of the borrow forwards, iterating over “similar” projections in lockstep until we can prove overlap one way or another. Essentially, we treat Overlap as a monoid and report a conflict if the product ends up not being Disjoint.

On each step, if we didn’t run out of borrow or place, we know that our elements have the same type, and that they only overlap if they are the identical.

For example, if we are comparing these:

BORROW:  (*x1[2].y).z.a
ACCESS:  (*x1[i].y).w.b

Then our steps are:

      x1         |   x1          -- places are the same
      x1[2]      |   x1[i]       -- equal or disjoint (disjoint if indexes differ)
      x1[2].y    |   x1[i].y     -- equal or disjoint
     *x1[2].y    |  *x1[i].y     -- equal or disjoint
    (*x1[2].y).z | (*x1[i].y).w  -- we are disjoint and don't need to check more!

Because zip does potentially bad things to the iterator inside, this loop also handles the case where the access might be a prefix of the borrow, e.g.

BORROW:  (*x1[2].y).z.a
ACCESS:  x1[i].y

Then our steps are:

      x1         |   x1          -- places are the same
      x1[2]      |   x1[i]       -- equal or disjoint (disjoint if indexes differ)
      x1[2].y    |   x1[i].y     -- equal or disjoint

– here we run out of access - the borrow can access a part of it. If this is a full deep access, then we know the borrow conflicts with it. However, if the access is shallow, then we can proceed:

      x1[2].y    | (*x1[i].y)    -- a deref! the access can't get past this, so we
                                    are disjoint

Our invariant is, that at each step of the iteration:

• If we didn’t run out of access to match, our borrow and access are comparable and either equal or disjoint.
• If we did run out of access, the borrow can access a part of it.

Enums

• PlaceConflictBias
  When checking if a place conflicts with another place, this enum is used to influence decisions where a place might be equal or disjoint with another place, such as if a[i] == a[j]. PlaceConflictBias::Overlap would bias toward assuming that i might equal j and that these places overlap. PlaceConflictBias::NoOverlap assumes that for the purposes of the predicate being run in the calling context, the conservative choice is to assume the compared indices are disjoint (and therefore, do not overlap).

Functions

• borrow_conflicts_with_place 🔒
  Checks whether the borrow_place conflicts with the access_place given a borrow kind and access depth. The bias parameter is used to determine how the unknowable (comparing runtime array indices, for example) should be interpreted - this depends on what the caller wants in order to make the conservative choice and preserve soundness.
• place_components_conflict 🔒
• place_projection_conflict 🔒
• places_conflict
  Helper function for checking if places conflict with a mutable borrow and deep access depth. This is used to check for places conflicting outside of the borrow checking code (such as in dataflow).