diff --git a/src/lib.rs b/src/lib.rs index 366da876e..3c84a164d 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -89,6 +89,9 @@ pub struct Weaken<'tcx, Place = crate::utils::Place<'tcx>, ToCap = Option is resolved. + pub(crate) for_storage_dead: bool, #[serde(skip)] _marker: PhantomData<&'tcx ()>, } @@ -102,6 +105,7 @@ impl<'a, 'tcx: 'a, Ctxt: HasCompilerCtxt<'a, 'tcx>, ToCap: Copy + serde::Seriali place: self.place.display_string(ctxt), from: self.from, to: self.to, + for_storage_dead: self.for_storage_dead, _marker: PhantomData, } } @@ -113,6 +117,19 @@ impl Weaken<'_, Place, ToCap> { place, from, to, + for_storage_dead: false, + _marker: PhantomData, + } + } + + /// Create a Weaken that is due to a `StorageDead`. + /// Temporary workaround until is resolved. + pub(crate) fn new_for_storage_dead(place: Place, from: CapabilityKind, to: ToCap) -> Self { + Self { + place, + from, + to, + for_storage_dead: true, _marker: PhantomData, } } @@ -134,6 +151,12 @@ impl Weaken<'_, Place, ToCap> { { self.to } + + /// Returns true if this Weaken was emitted due to a `StorageDead`. + /// Temporary workaround until is resolved. + pub fn is_for_storage_dead(&self) -> bool { + self.for_storage_dead + } } impl<'a, 'tcx: 'a, Ctxt: HasBorrowCheckerCtxt<'a, 'tcx>> DisplayWithCtxt for Weaken<'tcx> { diff --git a/src/owned_pcg/impl/join_semi_lattice.rs b/src/owned_pcg/impl/join_semi_lattice.rs index c8aed5811..6417fbcd0 100644 --- a/src/owned_pcg/impl/join_semi_lattice.rs +++ b/src/owned_pcg/impl/join_semi_lattice.rs @@ -65,7 +65,9 @@ impl<'a, 'pcg, 'tcx> JoinOwnedData<'a, 'pcg, 'tcx, &'pcg mut OwnedPcgLocal<'tcx> let mut repacks = vec![]; for (place, k) in self.capabilities.owned_capabilities(expansions.local, ctxt) { if k.expect_concrete() > CapabilityKind::Write { - repacks.push(RepackOp::weaken( + // Temporary: mark as for_storage_dead until + // https://github.com/prusti/pcg/issues/137 is resolved. + repacks.push(RepackOp::weaken_for_storage_dead( place, k.expect_concrete(), CapabilityKind::Write, diff --git a/src/owned_pcg/results/repacks.rs b/src/owned_pcg/results/repacks.rs index 6f8bf0293..efc551458 100644 --- a/src/owned_pcg/results/repacks.rs +++ b/src/owned_pcg/results/repacks.rs @@ -338,8 +338,14 @@ impl> DisplayWithCtxt } impl<'tcx> RepackOp<'tcx> { - pub(crate) fn weaken(place: Place<'tcx>, from: CapabilityKind, to: CapabilityKind) -> Self { - Self::Weaken(Weaken::new(place, from, to)) + /// Temporary: create a Weaken for `StorageDead`. + /// Required until is resolved. + pub(crate) fn weaken_for_storage_dead( + place: Place<'tcx>, + from: CapabilityKind, + to: CapabilityKind, + ) -> Self { + Self::Weaken(Weaken::new_for_storage_dead(place, from, to)) } pub(crate) fn expand<'a>( from: Place<'tcx>, diff --git a/src/pcg/visitor/obtain.rs b/src/pcg/visitor/obtain.rs index d4d392c22..88401357d 100644 --- a/src/pcg/visitor/obtain.rs +++ b/src/pcg/visitor/obtain.rs @@ -713,8 +713,10 @@ impl<'state, 'a: 'state, 'tcx: 'a, Ctxt: DataflowCtxt<'a, 'tcx>> .pcg .place_capability_equals(place, CapabilityKind::Exclusive) { + // Temporary: mark as for_storage_dead until + // https://github.com/prusti/pcg/issues/137 is resolved. self.record_and_apply_action(PcgAction::Owned(OwnedPcgAction::new( - RepackOp::Weaken(Weaken::new( + RepackOp::Weaken(Weaken::new_for_storage_dead( place, CapabilityKind::Exclusive, CapabilityKind::Write, diff --git a/test-files/211_cond_drop_join.rs b/test-files/211_cond_drop_join.rs index 4680ed91c..5289f67e8 100644 --- a/test-files/211_cond_drop_join.rs +++ b/test-files/211_cond_drop_join.rs @@ -9,7 +9,7 @@ fn ex1_replace_fst_cond(mut p: Pair, s: String) -> Pair { drop(p.fst); } // PCG: bb4 -> bb5: unpack p with capability E - // PCG: bb4 -> bb5: Weaken(Weaken { place: _1.0, from: E, to: W, _marker: PhantomData<&()> }) + // PCG: bb4 -> bb5: Weaken(Weaken { place: _1.0, from: E, to: W, for_storage_dead: false, _marker: PhantomData<&()> }) p.fst = s; p } diff --git a/test-files/218_storagedead_weaken.rs b/test-files/218_storagedead_weaken.rs index 52e853aff..3d0ce4683 100644 --- a/test-files/218_storagedead_weaken.rs +++ b/test-files/218_storagedead_weaken.rs @@ -2,6 +2,6 @@ fn bar() -> *mut i32 { let mut x = 5; &raw mut x // Before the storagedead, there should be a weaken from E to W - // PCG: bb0[4] pre_main: Weaken(Weaken { place: _1, from: E, to: W, _marker: PhantomData<&()> }) + // PCG: bb0[4] pre_main: Weaken(Weaken { place: _1, from: E, to: W, for_storage_dead: true, _marker: PhantomData<&()> }) // PCG: bb0[4] pre_main: Label place x (StorageDead) } diff --git a/visualization/src/generated/types.ts b/visualization/src/generated/types.ts index 202a7a174..98a267a9b 100644 --- a/visualization/src/generated/types.ts +++ b/visualization/src/generated/types.ts @@ -185,4 +185,9 @@ export type ValidityConditionsDebugRepr = { branch_choices: BranchChoicesDebugRe * be weakened to the second given capability. We guarantee that `_.1 > _.2`. * If `_.2` is `None`, the capability is removed. */ -export type Weaken = { place: Place; from: CapabilityKind; to: ToCap }; \ No newline at end of file +export type Weaken = { place: Place; from: CapabilityKind; to: ToCap; +/** + * Temporary flag indicating this Weaken was emitted due to a `StorageDead`. + * Required until is resolved. + */ +for_storage_dead: boolean }; \ No newline at end of file