improve consistency within fact gen

- fix names
- fix ordering of arguments
This commit is contained in:
Rémy Rakic 2024-12-11 15:23:32 +00:00
parent 7ad1f5bec5
commit 8562497d0a
4 changed files with 44 additions and 46 deletions

View file

@ -11,12 +11,12 @@ use crate::universal_regions::UniversalRegions;
/// Emit polonius facts for variable defs, uses, drops, and path accesses.
pub(crate) fn emit_access_facts<'tcx>(
facts: &mut AllFacts,
tcx: TyCtxt<'tcx>,
facts: &mut AllFacts,
body: &Body<'tcx>,
location_table: &LocationTable,
move_data: &MoveData<'tcx>,
universal_regions: &UniversalRegions<'tcx>,
location_table: &LocationTable,
) {
let mut extractor = AccessFactsExtractor { facts, move_data, location_table };
extractor.visit_body(body);

View file

@ -21,22 +21,22 @@ use crate::{
/// Emit `loan_invalidated_at` facts.
pub(super) fn emit_loan_invalidations<'tcx>(
tcx: TyCtxt<'tcx>,
all_facts: &mut AllFacts,
location_table: &LocationTable,
facts: &mut AllFacts,
body: &Body<'tcx>,
location_table: &LocationTable,
borrow_set: &BorrowSet<'tcx>,
) {
let dominators = body.basic_blocks.dominators();
let mut visitor =
LoanInvalidationsGenerator { all_facts, borrow_set, tcx, location_table, body, dominators };
LoanInvalidationsGenerator { facts, borrow_set, tcx, location_table, body, dominators };
visitor.visit_body(body);
}
struct LoanInvalidationsGenerator<'a, 'tcx> {
tcx: TyCtxt<'tcx>,
all_facts: &'a mut AllFacts,
location_table: &'a LocationTable,
facts: &'a mut AllFacts,
body: &'a Body<'tcx>,
location_table: &'a LocationTable,
dominators: &'a Dominators<BasicBlock>,
borrow_set: &'a BorrowSet<'tcx>,
}
@ -151,7 +151,7 @@ impl<'a, 'tcx> Visitor<'tcx> for LoanInvalidationsGenerator<'a, 'tcx> {
let resume = self.location_table.start_index(resume.start_location());
for (i, data) in borrow_set.iter_enumerated() {
if borrow_of_local_data(data.borrowed_place) {
self.all_facts.loan_invalidated_at.push((resume, i));
self.facts.loan_invalidated_at.push((resume, i));
}
}
@ -165,7 +165,7 @@ impl<'a, 'tcx> Visitor<'tcx> for LoanInvalidationsGenerator<'a, 'tcx> {
let start = self.location_table.start_index(location);
for (i, data) in borrow_set.iter_enumerated() {
if borrow_of_local_data(data.borrowed_place) {
self.all_facts.loan_invalidated_at.push((start, i));
self.facts.loan_invalidated_at.push((start, i));
}
}
}
@ -409,7 +409,7 @@ impl<'a, 'tcx> LoanInvalidationsGenerator<'a, 'tcx> {
/// Generates a new `loan_invalidated_at(L, B)` fact.
fn emit_loan_invalidated_at(&mut self, b: BorrowIndex, l: Location) {
let lidx = self.location_table.start_index(l);
self.all_facts.loan_invalidated_at.push((lidx, b));
self.facts.loan_invalidated_at.push((lidx, b));
}
fn check_activations(&mut self, location: Location) {

View file

@ -14,12 +14,12 @@ use crate::places_conflict;
/// Emit `loan_killed_at` and `cfg_edge` facts at the same time.
pub(super) fn emit_loan_kills<'tcx>(
tcx: TyCtxt<'tcx>,
all_facts: &mut AllFacts,
location_table: &LocationTable,
facts: &mut AllFacts,
body: &Body<'tcx>,
location_table: &LocationTable,
borrow_set: &BorrowSet<'tcx>,
) {
let mut visitor = LoanKillsGenerator { borrow_set, tcx, location_table, all_facts, body };
let mut visitor = LoanKillsGenerator { borrow_set, tcx, location_table, facts, body };
for (bb, data) in body.basic_blocks.iter_enumerated() {
visitor.visit_basic_block_data(bb, data);
}
@ -27,7 +27,7 @@ pub(super) fn emit_loan_kills<'tcx>(
struct LoanKillsGenerator<'a, 'tcx> {
tcx: TyCtxt<'tcx>,
all_facts: &'a mut AllFacts,
facts: &'a mut AllFacts,
location_table: &'a LocationTable,
borrow_set: &'a BorrowSet<'tcx>,
body: &'a Body<'tcx>,
@ -36,12 +36,12 @@ struct LoanKillsGenerator<'a, 'tcx> {
impl<'a, 'tcx> Visitor<'tcx> for LoanKillsGenerator<'a, 'tcx> {
fn visit_statement(&mut self, statement: &Statement<'tcx>, location: Location) {
// Also record CFG facts here.
self.all_facts.cfg_edge.push((
self.facts.cfg_edge.push((
self.location_table.start_index(location),
self.location_table.mid_index(location),
));
self.all_facts.cfg_edge.push((
self.facts.cfg_edge.push((
self.location_table.mid_index(location),
self.location_table.start_index(location.successor_within_block()),
));
@ -63,15 +63,15 @@ impl<'a, 'tcx> Visitor<'tcx> for LoanKillsGenerator<'a, 'tcx> {
fn visit_terminator(&mut self, terminator: &Terminator<'tcx>, location: Location) {
// Also record CFG facts here.
self.all_facts.cfg_edge.push((
self.facts.cfg_edge.push((
self.location_table.start_index(location),
self.location_table.mid_index(location),
));
let successor_blocks = terminator.successors();
self.all_facts.cfg_edge.reserve(successor_blocks.size_hint().0);
self.facts.cfg_edge.reserve(successor_blocks.size_hint().0);
for successor_block in successor_blocks {
self.all_facts.cfg_edge.push((
self.facts.cfg_edge.push((
self.location_table.mid_index(location),
self.location_table.start_index(successor_block.start_location()),
));
@ -128,7 +128,7 @@ impl<'tcx> LoanKillsGenerator<'_, 'tcx> {
if places_conflict {
let location_index = self.location_table.mid_index(location);
self.all_facts.loan_killed_at.push((borrow_index, location_index));
self.facts.loan_killed_at.push((borrow_index, location_index));
}
}
}
@ -140,9 +140,9 @@ impl<'tcx> LoanKillsGenerator<'_, 'tcx> {
fn record_killed_borrows_for_local(&mut self, local: Local, location: Location) {
if let Some(borrow_indices) = self.borrow_set.local_map.get(&local) {
let location_index = self.location_table.mid_index(location);
self.all_facts.loan_killed_at.reserve(borrow_indices.len());
self.facts.loan_killed_at.reserve(borrow_indices.len());
for &borrow_index in borrow_indices {
self.all_facts.loan_killed_at.push((borrow_index, location_index));
self.facts.loan_killed_at.push((borrow_index, location_index));
}
}
}

View file

@ -43,40 +43,38 @@ pub(crate) fn emit_facts<'tcx>(
universal_region_relations: &UniversalRegionRelations<'tcx>,
constraints: &MirTypeckRegionConstraints<'tcx>,
) {
let Some(all_facts) = all_facts else {
let Some(facts) = all_facts else {
// We don't do anything if there are no facts to fill.
return;
};
let _prof_timer = tcx.prof.generic_activity("polonius_fact_generation");
emit_move_facts(all_facts, move_data, location_table, body);
emit_universal_region_facts(all_facts, borrow_set, universal_region_relations);
loan_kills::emit_loan_kills(tcx, all_facts, location_table, body, borrow_set);
loan_invalidations::emit_loan_invalidations(tcx, all_facts, location_table, body, borrow_set);
emit_move_facts(facts, body, location_table, move_data);
emit_universal_region_facts(facts, borrow_set, universal_region_relations);
loan_kills::emit_loan_kills(tcx, facts, body, location_table, borrow_set);
loan_invalidations::emit_loan_invalidations(tcx, facts, body, location_table, borrow_set);
accesses::emit_access_facts(
all_facts,
tcx,
facts,
body,
location_table,
move_data,
&universal_region_relations.universal_regions,
location_table,
);
emit_outlives_facts(all_facts, location_table, constraints);
emit_outlives_facts(facts, location_table, constraints);
}
/// Emit facts needed for move/init analysis: moves and assignments.
fn emit_move_facts(
all_facts: &mut AllFacts,
move_data: &MoveData<'_>,
location_table: &LocationTable,
facts: &mut AllFacts,
body: &Body<'_>,
location_table: &LocationTable,
move_data: &MoveData<'_>,
) {
all_facts
.path_is_var
.extend(move_data.rev_lookup.iter_locals_enumerated().map(|(l, r)| (r, l)));
facts.path_is_var.extend(move_data.rev_lookup.iter_locals_enumerated().map(|(l, r)| (r, l)));
for (child, move_path) in move_data.move_paths.iter_enumerated() {
if let Some(parent) = move_path.parent {
all_facts.child_path.push((child, parent));
facts.child_path.push((child, parent));
}
}
@ -102,14 +100,14 @@ fn emit_move_facts(
// The initialization happened in (or rather, when arriving at)
// the successors, but not in the unwind block.
let first_statement = Location { block: successor, statement_index: 0 };
all_facts
facts
.path_assigned_at_base
.push((init.path, location_table.start_index(first_statement)));
}
} else {
// In all other cases, the initialization just happens at the
// midpoint, like any other effect.
all_facts
facts
.path_assigned_at_base
.push((init.path, location_table.mid_index(location)));
}
@ -117,7 +115,7 @@ fn emit_move_facts(
// Arguments are initialized on function entry
InitLocation::Argument(local) => {
assert!(body.local_kind(local) == LocalKind::Arg);
all_facts.path_assigned_at_base.push((init.path, fn_entry_start));
facts.path_assigned_at_base.push((init.path, fn_entry_start));
}
}
}
@ -126,20 +124,20 @@ fn emit_move_facts(
if body.local_kind(local) != LocalKind::Arg {
// Non-arguments start out deinitialised; we simulate this with an
// initial move:
all_facts.path_moved_at_base.push((path, fn_entry_start));
facts.path_moved_at_base.push((path, fn_entry_start));
}
}
// moved_out_at
// deinitialisation is assumed to always happen!
all_facts
facts
.path_moved_at_base
.extend(move_data.moves.iter().map(|mo| (mo.path, location_table.mid_index(mo.source))));
}
/// Emit universal regions facts, and their relations.
fn emit_universal_region_facts(
all_facts: &mut AllFacts,
facts: &mut AllFacts,
borrow_set: &BorrowSet<'_>,
universal_region_relations: &UniversalRegionRelations<'_>,
) {
@ -150,7 +148,7 @@ fn emit_universal_region_facts(
// added to the existing number of loans, as if they succeeded them in the set.
//
let universal_regions = &universal_region_relations.universal_regions;
all_facts
facts
.universal_region
.extend(universal_regions.universal_regions_iter().map(PoloniusRegionVid::from));
let borrow_count = borrow_set.len();
@ -163,7 +161,7 @@ fn emit_universal_region_facts(
for universal_region in universal_regions.universal_regions_iter() {
let universal_region_idx = universal_region.index();
let placeholder_loan_idx = borrow_count + universal_region_idx;
all_facts.placeholder.push((universal_region.into(), placeholder_loan_idx.into()));
facts.placeholder.push((universal_region.into(), placeholder_loan_idx.into()));
}
// 2: the universal region relations `outlives` constraints are emitted as
@ -175,7 +173,7 @@ fn emit_universal_region_facts(
fr1={:?}, fr2={:?}",
fr1, fr2
);
all_facts.known_placeholder_subset.push((fr1.into(), fr2.into()));
facts.known_placeholder_subset.push((fr1.into(), fr2.into()));
}
}
}