Skip to content

Commit 7a3dca6

Browse files
committed
Polonius: emit placeholder and known_subset facts, as inputs to the subset error computation
1 parent 4dd6292 commit 7a3dca6

File tree

2 files changed

+32
-0
lines changed

2 files changed

+32
-0
lines changed

src/librustc_mir/borrow_check/nll/facts.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,7 @@ impl AllFactsExt for AllFacts {
6666
wr.write_facts_to_path(self.[
6767
borrow_region,
6868
universal_region,
69+
placeholder,
6970
cfg_edge,
7071
killed,
7172
outlives,
@@ -80,6 +81,7 @@ impl AllFactsExt for AllFacts {
8081
initialized_at,
8182
moved_out_at,
8283
path_accessed_at,
84+
known_subset,
8385
])
8486
}
8587
Ok(())

src/librustc_mir/borrow_check/nll/mod.rs

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -209,6 +209,36 @@ pub(in crate::borrow_check) fn compute_regions<'cx, 'tcx>(
209209
.universal_region
210210
.extend(universal_regions.universal_regions());
211211
populate_polonius_move_facts(all_facts, move_data, location_table, &body);
212+
213+
// Emit universal regions facts, and their relations, for Polonius.
214+
//
215+
// 1: universal regions are modeled in Polonius as a pair:
216+
// - the universal region vid itself.
217+
// - a "placeholder loan" associated to this universal region. Since they don't exist in
218+
// the `borrow_set`, their `BorrowIndex` are synthesized as the universal region index
219+
// added to the existing number of loans, as if they succeeded them in the set.
220+
//
221+
let borrow_count = borrow_set.borrows.len();
222+
debug!(
223+
"compute_regions: polonius placeholders, num_universals={}, borrow_count={}",
224+
universal_regions.len(),
225+
borrow_count
226+
);
227+
228+
for universal_region in universal_regions.universal_regions() {
229+
let universal_region_idx = universal_region.index();
230+
let placeholder_loan_idx = borrow_count + universal_region_idx;
231+
all_facts.placeholder.push((universal_region, placeholder_loan_idx.into()));
232+
}
233+
234+
// 2: the universal region relations `outlives` constraints are emitted as
235+
// `known_subset` facts.
236+
for (fr1, fr2) in universal_region_relations.known_outlives() {
237+
if fr1 != fr2 {
238+
debug!("compute_regions: emitting polonius `known_subset` fr1={:?}, fr2={:?}", fr1, fr2);
239+
all_facts.known_subset.push((*fr1, *fr2));
240+
}
241+
}
212242
}
213243

214244
// Create the region inference context, taking ownership of the

0 commit comments

Comments
 (0)