Skip to main content

lub_perms

Function lub_perms 

Source
pub fn lub_perms<'db>(
    env: &Env<'db>,
    perm1: RedPerm<'db>,
    perm2: RedPerm<'db>,
) -> RedPerm<'db>
Expand description

The least upper bound (LUB) of two permissions (perm1, perm2). The LUB perm3 is a permission such that perm1 <: perm3 and perm1 <: perm3 but also there is no other mutual upper bound perm4 where perm4 <: perm3. In other words, if perm1 and perm2 represent lower bounds in inference (i.e., for some inference variable ?X, perm1 <: ?X and perm2 <: ?X), then perm3 combines those two bounds on ?X into a single bound perm3 <: ?X that must also hold (because there is no possible value for ?X that wouldn’t satisfy it).

Computing the LUB is fairly trivial for us because we can just union the chains. This is not necessarily the most compact representation of the LUB but it is correct. We do some minimal simplification.

§Examples

  • lub_perms([our], [ref[x]]) = [ref[x]].
    • The union would be [our, ref[x]] but just [ref[x]] is equivalent and more compact.
      • Equivalent because (our | ref[x]) <: ref[x] and ref[x] <: (our | ref[x]))
  • lub_perms([ref[x.y]], [ref[x]]) = [ref[x]].
    • Another example where the union [ref[x], ref[x.y]] contains redundancies.
  • lub_perms([ref[x.y]], [ref[x.z]]) = [ref[x.y], ref[x.z]].
    • Union suffices.
  • lub_perms([ref[x.y]], [ref[x.z]]) = [ref[x.y], ref[x.z]].