From e171b678fb0508569fc9bf4f0a7576430f7c415f Mon Sep 17 00:00:00 2001 From: Zack Grannan Date: Tue, 3 Mar 2026 10:52:11 -0800 Subject: [PATCH 1/5] Add metadata to weaken op --- src/lib.rs | 23 +++++++++++++++++++++++ src/owned_pcg/impl/join_semi_lattice.rs | 4 +++- src/owned_pcg/results/repacks.rs | 9 +++++++++ src/pcg/engine.rs | 23 ----------------------- src/pcg/visitor/obtain.rs | 4 +++- 5 files changed, 38 insertions(+), 25 deletions(-) diff --git a/src/lib.rs b/src/lib.rs index 366da876e..f3969833f 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -89,6 +89,9 @@ pub struct Weaken<'tcx, Place = crate::utils::Place<'tcx>, ToCap = Option, } @@ -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 https://github.com/prusti/pcg/issues/137 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 https://github.com/prusti/pcg/issues/137 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..3add7538e 100644 --- a/src/owned_pcg/results/repacks.rs +++ b/src/owned_pcg/results/repacks.rs @@ -341,6 +341,15 @@ 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 https://github.com/prusti/pcg/issues/137 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>, guide: Option, diff --git a/src/pcg/engine.rs b/src/pcg/engine.rs index 0a89b4145..7bc25cff7 100644 --- a/src/pcg/engine.rs +++ b/src/pcg/engine.rs @@ -81,29 +81,6 @@ impl<'tcx> BodyWithBorrowckFacts<'tcx> { fn erase_regions(tcx: ty::TyCtxt<'tcx>, body: Body<'tcx>) -> Body<'tcx> { tcx.erase_regions(body) } - - #[must_use] - pub fn monomorphize( - self, - tcx: ty::TyCtxt<'tcx>, - substs: GenericArgsRef<'tcx>, - param_env: MonomorphizeEnv<'tcx>, - ) -> Self { - let body = Self::erase_regions(tcx, self.body.clone()); - let monomorphized_body = tcx.instantiate_and_normalize_erasing_regions( - substs, - param_env, - ty::EarlyBinder::bind(body), - ); - Self { - body: monomorphized_body, - promoted: self.promoted, - borrow_set: self.borrow_set, - region_inference_context: self.region_inference_context, - input_facts: self.input_facts, - location_table: self.location_table, - } - } } impl<'tcx> From> for BodyWithBorrowckFacts<'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, From 3c2ea6edb2de19ea40729fc3e99e0ca67fa464c9 Mon Sep 17 00:00:00 2001 From: Zack Grannan Date: Tue, 3 Mar 2026 12:41:32 -0800 Subject: [PATCH 2/5] bump From 5df0ec24c83d9d3434b6fee182196815aee9856e Mon Sep 17 00:00:00 2001 From: Zack Grannan Date: Tue, 3 Mar 2026 12:55:54 -0800 Subject: [PATCH 3/5] Update to appease linter --- src/lib.rs | 12 ++++++------ src/owned_pcg/results/repacks.rs | 7 ++----- src/pcg/engine.rs | 15 --------------- 3 files changed, 8 insertions(+), 26 deletions(-) diff --git a/src/lib.rs b/src/lib.rs index f3969833f..3c84a164d 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -89,8 +89,8 @@ pub struct Weaken<'tcx, Place = crate::utils::Place<'tcx>, ToCap = Option is resolved. pub(crate) for_storage_dead: bool, #[serde(skip)] _marker: PhantomData<&'tcx ()>, @@ -122,8 +122,8 @@ impl Weaken<'_, Place, ToCap> { } } - /// Create a Weaken that is due to a StorageDead. - /// Temporary workaround until https://github.com/prusti/pcg/issues/137 is resolved. + /// 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, @@ -152,8 +152,8 @@ impl Weaken<'_, Place, ToCap> { self.to } - /// Returns true if this Weaken was emitted due to a StorageDead. - /// Temporary workaround until https://github.com/prusti/pcg/issues/137 is resolved. + /// 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 } diff --git a/src/owned_pcg/results/repacks.rs b/src/owned_pcg/results/repacks.rs index 3add7538e..efc551458 100644 --- a/src/owned_pcg/results/repacks.rs +++ b/src/owned_pcg/results/repacks.rs @@ -338,11 +338,8 @@ 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 https://github.com/prusti/pcg/issues/137 is resolved. + /// Temporary: create a Weaken for `StorageDead`. + /// Required until is resolved. pub(crate) fn weaken_for_storage_dead( place: Place<'tcx>, from: CapabilityKind, diff --git a/src/pcg/engine.rs b/src/pcg/engine.rs index 7bc25cff7..1a56cf11b 100644 --- a/src/pcg/engine.rs +++ b/src/pcg/engine.rs @@ -28,7 +28,6 @@ use crate::{ self, BasicBlock, Body, Location, Promoted, START_BLOCK, Statement, Terminator, TerminatorEdges, }, - ty::{self, GenericArgsRef}, }, mir_dataflow::{Forward, move_paths::MoveData}, }, @@ -69,20 +68,6 @@ impl<'tcx> BodyAndBorrows<'tcx> for BodyWithBorrowckFacts<'tcx> { } } -type MonomorphizeEnv<'tcx> = ty::TypingEnv<'tcx>; - -impl<'tcx> BodyWithBorrowckFacts<'tcx> { - #[rustversion::since(2025-12-01)] - fn erase_regions(tcx: ty::TyCtxt<'tcx>, body: Body<'tcx>) -> Body<'tcx> { - tcx.erase_and_anonymize_regions(body) - } - - #[rustversion::before(2025-12-01)] - fn erase_regions(tcx: ty::TyCtxt<'tcx>, body: Body<'tcx>) -> Body<'tcx> { - tcx.erase_regions(body) - } -} - impl<'tcx> From> for BodyWithBorrowckFacts<'tcx> { fn from(value: borrowck::BodyWithBorrowckFacts<'tcx>) -> Self { Self { From 8e44130934af02d567d32ebc5c6eea8d6e734e19 Mon Sep 17 00:00:00 2001 From: Zack Grannan Date: Tue, 3 Mar 2026 13:25:10 -0800 Subject: [PATCH 4/5] fix tests --- src/pcg/engine.rs | 18 ++++++++++++++++++ test-files/211_cond_drop_join.rs | 2 +- test-files/218_storagedead_weaken.rs | 2 +- visualization/src/generated/types.ts | 7 ++++++- 4 files changed, 26 insertions(+), 3 deletions(-) diff --git a/src/pcg/engine.rs b/src/pcg/engine.rs index 1a56cf11b..daefd2a4a 100644 --- a/src/pcg/engine.rs +++ b/src/pcg/engine.rs @@ -28,6 +28,7 @@ use crate::{ self, BasicBlock, Body, Location, Promoted, START_BLOCK, Statement, Terminator, TerminatorEdges, }, + ty, }, mir_dataflow::{Forward, move_paths::MoveData}, }, @@ -68,6 +69,23 @@ impl<'tcx> BodyAndBorrows<'tcx> for BodyWithBorrowckFacts<'tcx> { } } +#[allow(dead_code)] +type MonomorphizeEnv<'tcx> = ty::TypingEnv<'tcx>; + +impl<'tcx> BodyWithBorrowckFacts<'tcx> { + #[allow(dead_code)] + #[rustversion::since(2025-12-01)] + fn erase_regions(tcx: ty::TyCtxt<'tcx>, body: Body<'tcx>) -> Body<'tcx> { + tcx.erase_and_anonymize_regions(body) + } + + #[allow(dead_code)] + #[rustversion::before(2025-12-01)] + fn erase_regions(tcx: ty::TyCtxt<'tcx>, body: Body<'tcx>) -> Body<'tcx> { + tcx.erase_regions(body) + } +} + impl<'tcx> From> for BodyWithBorrowckFacts<'tcx> { fn from(value: borrowck::BodyWithBorrowckFacts<'tcx>) -> Self { Self { 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 From 02cb52516d41dde70d6ac5f0287ca377f3db7c5a Mon Sep 17 00:00:00 2001 From: Zack Grannan Date: Tue, 3 Mar 2026 13:26:06 -0800 Subject: [PATCH 5/5] revert --- src/pcg/engine.rs | 28 ++++++++++++++++++++++++---- 1 file changed, 24 insertions(+), 4 deletions(-) diff --git a/src/pcg/engine.rs b/src/pcg/engine.rs index daefd2a4a..0a89b4145 100644 --- a/src/pcg/engine.rs +++ b/src/pcg/engine.rs @@ -28,7 +28,7 @@ use crate::{ self, BasicBlock, Body, Location, Promoted, START_BLOCK, Statement, Terminator, TerminatorEdges, }, - ty, + ty::{self, GenericArgsRef}, }, mir_dataflow::{Forward, move_paths::MoveData}, }, @@ -69,21 +69,41 @@ impl<'tcx> BodyAndBorrows<'tcx> for BodyWithBorrowckFacts<'tcx> { } } -#[allow(dead_code)] type MonomorphizeEnv<'tcx> = ty::TypingEnv<'tcx>; impl<'tcx> BodyWithBorrowckFacts<'tcx> { - #[allow(dead_code)] #[rustversion::since(2025-12-01)] fn erase_regions(tcx: ty::TyCtxt<'tcx>, body: Body<'tcx>) -> Body<'tcx> { tcx.erase_and_anonymize_regions(body) } - #[allow(dead_code)] #[rustversion::before(2025-12-01)] fn erase_regions(tcx: ty::TyCtxt<'tcx>, body: Body<'tcx>) -> Body<'tcx> { tcx.erase_regions(body) } + + #[must_use] + pub fn monomorphize( + self, + tcx: ty::TyCtxt<'tcx>, + substs: GenericArgsRef<'tcx>, + param_env: MonomorphizeEnv<'tcx>, + ) -> Self { + let body = Self::erase_regions(tcx, self.body.clone()); + let monomorphized_body = tcx.instantiate_and_normalize_erasing_regions( + substs, + param_env, + ty::EarlyBinder::bind(body), + ); + Self { + body: monomorphized_body, + promoted: self.promoted, + borrow_set: self.borrow_set, + region_inference_context: self.region_inference_context, + input_facts: self.input_facts, + location_table: self.location_table, + } + } } impl<'tcx> From> for BodyWithBorrowckFacts<'tcx> {