From b9ba8789dedc8ee1c9499e92dcac7b250a7b6016 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= Date: Mon, 13 Nov 2023 19:17:16 +0100 Subject: [PATCH] Disallow expanding through `Projection` at edges --- .../src/free_pcs/check/checker.rs | 18 ++++++++++++++---- .../src/free_pcs/impl/join_semi_lattice.rs | 16 ++++++++++------ mir-state-analysis/src/free_pcs/impl/local.rs | 9 +++++++-- mir-state-analysis/src/free_pcs/impl/update.rs | 3 +-- 4 files changed, 32 insertions(+), 14 deletions(-) diff --git a/mir-state-analysis/src/free_pcs/check/checker.rs b/mir-state-analysis/src/free_pcs/check/checker.rs index 63fc3c7bae2..77a9ffedea6 100644 --- a/mir-state-analysis/src/free_pcs/check/checker.rs +++ b/mir-state-analysis/src/free_pcs/check/checker.rs @@ -41,7 +41,7 @@ pub(crate) fn check(mut cursor: FreePcsAnalysis<'_, '_>) { assert_eq!(fpcs_after.location, loc); // Repacks for &op in &fpcs_after.repacks_middle { - op.update_free(&mut fpcs.summary, false, rp); + op.update_free(&mut fpcs.summary, data.is_cleanup, true, rp); } // Consistency fpcs.summary.consistency_check(rp); @@ -53,7 +53,7 @@ pub(crate) fn check(mut cursor: FreePcsAnalysis<'_, '_>) { // Repacks for op in fpcs_after.repacks { - op.update_free(&mut fpcs.summary, false, rp); + op.update_free(&mut fpcs.summary, data.is_cleanup, true, rp); } // Statement post fpcs.apply_pre_effect = false; @@ -70,7 +70,7 @@ pub(crate) fn check(mut cursor: FreePcsAnalysis<'_, '_>) { assert_eq!(fpcs_after.location, loc); // Repacks for op in fpcs_after.repacks_middle { - op.update_free(&mut fpcs.summary, false, rp); + op.update_free(&mut fpcs.summary, data.is_cleanup, true, rp); } // Consistency fpcs.summary.consistency_check(rp); @@ -82,7 +82,7 @@ pub(crate) fn check(mut cursor: FreePcsAnalysis<'_, '_>) { // Repacks for op in fpcs_after.repacks { - op.update_free(&mut fpcs.summary, false, rp); + op.update_free(&mut fpcs.summary, data.is_cleanup, true, rp); } // Statement post fpcs.apply_pre_effect = false; @@ -101,6 +101,7 @@ pub(crate) fn check(mut cursor: FreePcsAnalysis<'_, '_>) { op.update_free( &mut from.summary, body.basic_blocks[succ.location.block].is_cleanup, + false, rp, ); } @@ -115,6 +116,7 @@ impl<'tcx> RepackOp<'tcx> { self, state: &mut CapabilitySummary<'tcx>, is_cleanup: bool, + can_downcast: bool, rp: PlaceRepacker<'_, 'tcx>, ) { match self { @@ -144,6 +146,14 @@ impl<'tcx> RepackOp<'tcx> { RepackOp::Expand(place, guide, kind) => { assert_eq!(kind, CapabilityKind::Exclusive, "{self:?}"); assert!(place.is_prefix_exact(guide), "{self:?}"); + assert!( + can_downcast + || !matches!( + guide.projection.last().unwrap(), + ProjectionElem::Downcast(..) + ), + "{self:?}" + ); let curr_state = state[place.local].get_allocated_mut(); assert_eq!( curr_state.remove(&place), diff --git a/mir-state-analysis/src/free_pcs/impl/join_semi_lattice.rs b/mir-state-analysis/src/free_pcs/impl/join_semi_lattice.rs index e2880d86002..24536ef2a79 100644 --- a/mir-state-analysis/src/free_pcs/impl/join_semi_lattice.rs +++ b/mir-state-analysis/src/free_pcs/impl/join_semi_lattice.rs @@ -125,16 +125,20 @@ impl<'tcx> RepackingJoinSemiLattice<'tcx> for CapabilityProjections<'tcx> { if !self.contains_key(&p) { continue; } - let p = if kind != CapabilityKind::Exclusive { - changed = true; - self.collapse(related.get_from(), related.to, repacker); + let collapse_to = if kind != CapabilityKind::Exclusive { related.to } else { - p + related.to.joinable_to(p) }; + if collapse_to != p { + changed = true; + let mut from = related.get_from(); + from.retain(|&from| collapse_to.is_prefix(from)); + self.collapse(from, collapse_to, repacker); + } if k > kind { changed = true; - self.insert(p, kind); + self.update_cap(collapse_to, kind); } } None @@ -151,7 +155,7 @@ impl<'tcx> RepackingJoinSemiLattice<'tcx> for CapabilityProjections<'tcx> { // Downgrade the permission if needed if self[&place] > kind { changed = true; - self.insert(place, kind); + self.update_cap(place, kind); } } } diff --git a/mir-state-analysis/src/free_pcs/impl/local.rs b/mir-state-analysis/src/free_pcs/impl/local.rs index fda663d4cd7..b154e6b34a5 100644 --- a/mir-state-analysis/src/free_pcs/impl/local.rs +++ b/mir-state-analysis/src/free_pcs/impl/local.rs @@ -82,6 +82,11 @@ impl<'tcx> CapabilityProjections<'tcx> { self.iter().next().unwrap().0.local } + pub(crate) fn update_cap(&mut self, place: Place<'tcx>, cap: CapabilityKind) { + let old = self.insert(place, cap); + assert!(old.is_some()); + } + /// Returns all related projections of the given place that are contained in this map. /// A `Ordering::Less` means that the given `place` is a prefix of the iterator place. /// For example: find_all_related(x.f.g) = [(Less, x.f.g.h), (Greater, x.f)] @@ -104,7 +109,7 @@ impl<'tcx> CapabilityProjections<'tcx> { // Some(cap_no_read) // }; if let Some(expected) = expected { - assert_eq!(ord, expected); + assert_eq!(ord, expected, "({self:?}) {from:?} {to:?}"); } else { expected = Some(ord); } @@ -179,7 +184,7 @@ impl<'tcx> CapabilityProjections<'tcx> { .map(|&p| (p, self.remove(&p).unwrap())) .collect(); let collapsed = to.collapse(&mut from, repacker); - assert!(from.is_empty()); + assert!(from.is_empty(), "{from:?} ({collapsed:?}) {to:?}"); let mut exclusive_at = Vec::new(); if !to.projects_shared_ref(repacker) { for (to, _, kind) in &collapsed { diff --git a/mir-state-analysis/src/free_pcs/impl/update.rs b/mir-state-analysis/src/free_pcs/impl/update.rs index 23bcd14981e..1e59d315ecb 100644 --- a/mir-state-analysis/src/free_pcs/impl/update.rs +++ b/mir-state-analysis/src/free_pcs/impl/update.rs @@ -76,8 +76,7 @@ impl<'tcx> Fpcs<'_, 'tcx> { fn ensures_alloc(&mut self, place: impl Into>, cap: CapabilityKind) { let place = place.into(); let cp: &mut CapabilityProjections = self.summary[place.local].get_allocated_mut(); - let old = cp.insert(place, cap); - assert!(old.is_some()); + cp.update_cap(place, cap); } pub(crate) fn ensures_exclusive(&mut self, place: impl Into>) { self.ensures_alloc(place, CapabilityKind::Exclusive)