Add metadata to weaken op

src/lib.rs

@@ -89,6 +89,9 @@ pub struct Weaken<'tcx, Place = crate::utils::Place<'tcx>, ToCap = Option<Capabi
     pub(crate) place: Place,
     pub(crate) from: CapabilityKind,
     pub(crate) to: ToCap,
+    /// Temporary flag indicating this Weaken was emitted due to a `StorageDead`.
+    /// Required until <https://github.com/prusti/pcg/issues/137> 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<Place, ToCap> 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<Place, ToCap> 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<Ctxt> for Weaken<'tcx> {

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,

src/owned_pcg/results/repacks.rs

@@ -338,8 +338,14 @@ impl<Ctxt, P: std::fmt::Debug + DisplayWithCtxt<Ctxt>> DisplayWithCtxt<Ctxt>
 }
 
 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>,

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,

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
 }

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)
 }

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, ToCap> = { place: Place; from: CapabilityKind; to: ToCap };
+export type Weaken<Place, ToCap> = { place: Place; from: CapabilityKind; to: ToCap; 
+/**
+ * Temporary flag indicating this Weaken was emitted due to a `StorageDead`.
+ * Required until <https://github.com/prusti/pcg/issues/137> is resolved.
+ */
+for_storage_dead: boolean };