Skip to content

Commit

Permalink
Disallow expanding through Projection at edges
Browse files Browse the repository at this point in the history
  • Loading branch information
JonasAlaif committed Nov 13, 2023
1 parent 54651c9 commit b9ba878
Show file tree
Hide file tree
Showing 4 changed files with 32 additions and 14 deletions.
18 changes: 14 additions & 4 deletions mir-state-analysis/src/free_pcs/check/checker.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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;
Expand All @@ -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);
Expand All @@ -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;
Expand All @@ -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,
);
}
Expand All @@ -115,6 +116,7 @@ impl<'tcx> RepackOp<'tcx> {
self,
state: &mut CapabilitySummary<'tcx>,
is_cleanup: bool,
can_downcast: bool,
rp: PlaceRepacker<'_, 'tcx>,
) {
match self {
Expand Down Expand Up @@ -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),
Expand Down
16 changes: 10 additions & 6 deletions mir-state-analysis/src/free_pcs/impl/join_semi_lattice.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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);
}
}
}
Expand Down
9 changes: 7 additions & 2 deletions mir-state-analysis/src/free_pcs/impl/local.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand All @@ -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);
}
Expand Down Expand Up @@ -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 {
Expand Down
3 changes: 1 addition & 2 deletions mir-state-analysis/src/free_pcs/impl/update.rs
Original file line number Diff line number Diff line change
Expand Up @@ -76,8 +76,7 @@ impl<'tcx> Fpcs<'_, 'tcx> {
fn ensures_alloc(&mut self, place: impl Into<Place<'tcx>>, 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<Place<'tcx>>) {
self.ensures_alloc(place, CapabilityKind::Exclusive)
Expand Down

0 comments on commit b9ba878

Please sign in to comment.