diff --git a/src/librustc_mir/borrow_check/nll/facts.rs b/src/librustc_mir/borrow_check/nll/facts.rs index eabb11acab91..a16c36d749f0 100644 --- a/src/librustc_mir/borrow_check/nll/facts.rs +++ b/src/librustc_mir/borrow_check/nll/facts.rs @@ -66,6 +66,7 @@ impl AllFactsExt for AllFacts { wr.write_facts_to_path(self.[ borrow_region, universal_region, + placeholder, cfg_edge, killed, outlives, @@ -80,6 +81,7 @@ impl AllFactsExt for AllFacts { initialized_at, moved_out_at, path_accessed_at, + known_subset, ]) } Ok(()) diff --git a/src/librustc_mir/borrow_check/nll/mod.rs b/src/librustc_mir/borrow_check/nll/mod.rs index 337f612f7cea..ffd9c011717d 100644 --- a/src/librustc_mir/borrow_check/nll/mod.rs +++ b/src/librustc_mir/borrow_check/nll/mod.rs @@ -209,6 +209,36 @@ pub(in crate::borrow_check) fn compute_regions<'cx, 'tcx>( .universal_region .extend(universal_regions.universal_regions()); populate_polonius_move_facts(all_facts, move_data, location_table, &body); + + // Emit universal regions facts, and their relations, for Polonius. + // + // 1: universal regions are modeled in Polonius as a pair: + // - the universal region vid itself. + // - a "placeholder loan" associated to this universal region. Since they don't exist in + // the `borrow_set`, their `BorrowIndex` are synthesized as the universal region index + // added to the existing number of loans, as if they succeeded them in the set. + // + let borrow_count = borrow_set.borrows.len(); + debug!( + "compute_regions: polonius placeholders, num_universals={}, borrow_count={}", + universal_regions.len(), + borrow_count + ); + + for universal_region in universal_regions.universal_regions() { + let universal_region_idx = universal_region.index(); + let placeholder_loan_idx = borrow_count + universal_region_idx; + all_facts.placeholder.push((universal_region, placeholder_loan_idx.into())); + } + + // 2: the universal region relations `outlives` constraints are emitted as + // `known_subset` facts. + for (fr1, fr2) in universal_region_relations.known_outlives() { + if fr1 != fr2 { + debug!("compute_regions: emitting polonius `known_subset` fr1={:?}, fr2={:?}", fr1, fr2); + all_facts.known_subset.push((*fr1, *fr2)); + } + } } // Create the region inference context, taking ownership of the