|
| 1 | +//! Functions dedicated to fact generation for the `-Zpolonius=legacy` datalog implementation. |
| 2 | +//! |
| 3 | +//! Will be removed in the future, once the in-tree `-Zpolonius=next` implementation reaches feature |
| 4 | +//! parity. |
| 5 | +
|
| 6 | +use rustc_middle::mir::{Body, LocalKind, Location, START_BLOCK}; |
| 7 | +use rustc_middle::ty::TyCtxt; |
| 8 | +use rustc_mir_dataflow::move_paths::{InitKind, InitLocation, MoveData}; |
| 9 | +use tracing::debug; |
| 10 | + |
| 11 | +use crate::borrow_set::BorrowSet; |
| 12 | +use crate::facts::{AllFacts, PoloniusRegionVid}; |
| 13 | +use crate::location::LocationTable; |
| 14 | +use crate::type_check::free_region_relations::UniversalRegionRelations; |
| 15 | + |
| 16 | +mod loan_invalidations; |
| 17 | +mod loan_kills; |
| 18 | + |
| 19 | +/// When requested, emit most of the facts needed by polonius: |
| 20 | +/// - moves and assignments |
| 21 | +/// - universal regions and their relations |
| 22 | +/// - CFG points and edges |
| 23 | +/// - loan kills |
| 24 | +/// - loan invalidations |
| 25 | +/// |
| 26 | +/// The rest of the facts are emitted during typeck and liveness. |
| 27 | +pub(crate) fn emit_facts<'tcx>( |
| 28 | + all_facts: &mut Option<AllFacts>, |
| 29 | + tcx: TyCtxt<'tcx>, |
| 30 | + location_table: &LocationTable, |
| 31 | + body: &Body<'tcx>, |
| 32 | + borrow_set: &BorrowSet<'tcx>, |
| 33 | + move_data: &MoveData<'_>, |
| 34 | + universal_region_relations: &UniversalRegionRelations<'_>, |
| 35 | +) { |
| 36 | + let Some(all_facts) = all_facts else { |
| 37 | + // We don't do anything if there are no facts to fill. |
| 38 | + return; |
| 39 | + }; |
| 40 | + let _prof_timer = tcx.prof.generic_activity("polonius_fact_generation"); |
| 41 | + emit_move_facts(all_facts, move_data, location_table, body); |
| 42 | + emit_universal_region_facts(all_facts, borrow_set, universal_region_relations); |
| 43 | + emit_cfg_and_loan_kills_facts(all_facts, tcx, location_table, body, borrow_set); |
| 44 | + emit_loan_invalidations_facts(all_facts, tcx, location_table, body, borrow_set); |
| 45 | +} |
| 46 | + |
| 47 | +/// Emit facts needed for move/init analysis: moves and assignments. |
| 48 | +fn emit_move_facts( |
| 49 | + all_facts: &mut AllFacts, |
| 50 | + move_data: &MoveData<'_>, |
| 51 | + location_table: &LocationTable, |
| 52 | + body: &Body<'_>, |
| 53 | +) { |
| 54 | + all_facts |
| 55 | + .path_is_var |
| 56 | + .extend(move_data.rev_lookup.iter_locals_enumerated().map(|(l, r)| (r, l))); |
| 57 | + |
| 58 | + for (child, move_path) in move_data.move_paths.iter_enumerated() { |
| 59 | + if let Some(parent) = move_path.parent { |
| 60 | + all_facts.child_path.push((child, parent)); |
| 61 | + } |
| 62 | + } |
| 63 | + |
| 64 | + let fn_entry_start = |
| 65 | + location_table.start_index(Location { block: START_BLOCK, statement_index: 0 }); |
| 66 | + |
| 67 | + // initialized_at |
| 68 | + for init in move_data.inits.iter() { |
| 69 | + match init.location { |
| 70 | + InitLocation::Statement(location) => { |
| 71 | + let block_data = &body[location.block]; |
| 72 | + let is_terminator = location.statement_index == block_data.statements.len(); |
| 73 | + |
| 74 | + if is_terminator && init.kind == InitKind::NonPanicPathOnly { |
| 75 | + // We are at the terminator of an init that has a panic path, |
| 76 | + // and where the init should not happen on panic |
| 77 | + |
| 78 | + for successor in block_data.terminator().successors() { |
| 79 | + if body[successor].is_cleanup { |
| 80 | + continue; |
| 81 | + } |
| 82 | + |
| 83 | + // The initialization happened in (or rather, when arriving at) |
| 84 | + // the successors, but not in the unwind block. |
| 85 | + let first_statement = Location { block: successor, statement_index: 0 }; |
| 86 | + all_facts |
| 87 | + .path_assigned_at_base |
| 88 | + .push((init.path, location_table.start_index(first_statement))); |
| 89 | + } |
| 90 | + } else { |
| 91 | + // In all other cases, the initialization just happens at the |
| 92 | + // midpoint, like any other effect. |
| 93 | + all_facts |
| 94 | + .path_assigned_at_base |
| 95 | + .push((init.path, location_table.mid_index(location))); |
| 96 | + } |
| 97 | + } |
| 98 | + // Arguments are initialized on function entry |
| 99 | + InitLocation::Argument(local) => { |
| 100 | + assert!(body.local_kind(local) == LocalKind::Arg); |
| 101 | + all_facts.path_assigned_at_base.push((init.path, fn_entry_start)); |
| 102 | + } |
| 103 | + } |
| 104 | + } |
| 105 | + |
| 106 | + for (local, path) in move_data.rev_lookup.iter_locals_enumerated() { |
| 107 | + if body.local_kind(local) != LocalKind::Arg { |
| 108 | + // Non-arguments start out deinitialised; we simulate this with an |
| 109 | + // initial move: |
| 110 | + all_facts.path_moved_at_base.push((path, fn_entry_start)); |
| 111 | + } |
| 112 | + } |
| 113 | + |
| 114 | + // moved_out_at |
| 115 | + // deinitialisation is assumed to always happen! |
| 116 | + all_facts |
| 117 | + .path_moved_at_base |
| 118 | + .extend(move_data.moves.iter().map(|mo| (mo.path, location_table.mid_index(mo.source)))); |
| 119 | +} |
| 120 | + |
| 121 | +/// Emit universal regions facts, and their relations. |
| 122 | +fn emit_universal_region_facts( |
| 123 | + all_facts: &mut AllFacts, |
| 124 | + borrow_set: &BorrowSet<'_>, |
| 125 | + universal_region_relations: &UniversalRegionRelations<'_>, |
| 126 | +) { |
| 127 | + // 1: universal regions are modeled in Polonius as a pair: |
| 128 | + // - the universal region vid itself. |
| 129 | + // - a "placeholder loan" associated to this universal region. Since they don't exist in |
| 130 | + // the `borrow_set`, their `BorrowIndex` are synthesized as the universal region index |
| 131 | + // added to the existing number of loans, as if they succeeded them in the set. |
| 132 | + // |
| 133 | + let universal_regions = &universal_region_relations.universal_regions; |
| 134 | + all_facts |
| 135 | + .universal_region |
| 136 | + .extend(universal_regions.universal_regions_iter().map(PoloniusRegionVid::from)); |
| 137 | + let borrow_count = borrow_set.len(); |
| 138 | + debug!( |
| 139 | + "emit_universal_region_facts: polonius placeholders, num_universals={}, borrow_count={}", |
| 140 | + universal_regions.len(), |
| 141 | + borrow_count |
| 142 | + ); |
| 143 | + |
| 144 | + for universal_region in universal_regions.universal_regions_iter() { |
| 145 | + let universal_region_idx = universal_region.index(); |
| 146 | + let placeholder_loan_idx = borrow_count + universal_region_idx; |
| 147 | + all_facts.placeholder.push((universal_region.into(), placeholder_loan_idx.into())); |
| 148 | + } |
| 149 | + |
| 150 | + // 2: the universal region relations `outlives` constraints are emitted as |
| 151 | + // `known_placeholder_subset` facts. |
| 152 | + for (fr1, fr2) in universal_region_relations.known_outlives() { |
| 153 | + if fr1 != fr2 { |
| 154 | + debug!( |
| 155 | + "emit_universal_region_facts: emitting polonius `known_placeholder_subset` \ |
| 156 | + fr1={:?}, fr2={:?}", |
| 157 | + fr1, fr2 |
| 158 | + ); |
| 159 | + all_facts.known_placeholder_subset.push((fr1.into(), fr2.into())); |
| 160 | + } |
| 161 | + } |
| 162 | +} |
| 163 | + |
| 164 | +/// Emit facts about loan invalidations. |
| 165 | +fn emit_loan_invalidations_facts<'tcx>( |
| 166 | + all_facts: &mut AllFacts, |
| 167 | + tcx: TyCtxt<'tcx>, |
| 168 | + location_table: &LocationTable, |
| 169 | + body: &Body<'tcx>, |
| 170 | + borrow_set: &BorrowSet<'tcx>, |
| 171 | +) { |
| 172 | + loan_invalidations::emit_loan_invalidations(tcx, all_facts, location_table, body, borrow_set); |
| 173 | +} |
| 174 | + |
| 175 | +/// Emit facts about CFG points and edges, as well as locations where loans are killed. |
| 176 | +fn emit_cfg_and_loan_kills_facts<'tcx>( |
| 177 | + all_facts: &mut AllFacts, |
| 178 | + tcx: TyCtxt<'tcx>, |
| 179 | + location_table: &LocationTable, |
| 180 | + body: &Body<'tcx>, |
| 181 | + borrow_set: &BorrowSet<'tcx>, |
| 182 | +) { |
| 183 | + loan_kills::emit_loan_kills(tcx, all_facts, location_table, body, borrow_set); |
| 184 | +} |
0 commit comments