From 58fe3c5603c739ea9dedb62df62615802ca51eec Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= <jonas.fiala@inf.ethz.ch>
Date: Fri, 20 Oct 2023 16:11:19 +0200
Subject: [PATCH] Add weakens before write

---
 mir-state-analysis/src/free_pcs/impl/triple.rs | 5 +++--
 mir-state-analysis/src/free_pcs/impl/update.rs | 9 ++++++---
 2 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/mir-state-analysis/src/free_pcs/impl/triple.rs b/mir-state-analysis/src/free_pcs/impl/triple.rs
index 6c400653237..07e0eda5866 100644
--- a/mir-state-analysis/src/free_pcs/impl/triple.rs
+++ b/mir-state-analysis/src/free_pcs/impl/triple.rs
@@ -83,13 +83,14 @@ impl<'tcx> Visitor<'tcx> for Fpcs<'_, 'tcx> {
                 let always_live = self.repacker.always_live_locals();
                 for local in 0..self.repacker.local_count() {
                     let local = Local::from_usize(local);
-                    if always_live.contains(local) {
+                    if local == RETURN_PLACE {
+                        self.requires_exclusive(RETURN_PLACE);
+                    } else if always_live.contains(local) {
                         self.requires_write(local);
                     } else {
                         self.requires_unalloc(local);
                     }
                 }
-                self.requires_exclusive(RETURN_PLACE);
             }
             &Drop { place, .. } => {
                 self.requires_write(place);
diff --git a/mir-state-analysis/src/free_pcs/impl/update.rs b/mir-state-analysis/src/free_pcs/impl/update.rs
index ef7b1a55533..f4862dd4363 100644
--- a/mir-state-analysis/src/free_pcs/impl/update.rs
+++ b/mir-state-analysis/src/free_pcs/impl/update.rs
@@ -61,9 +61,12 @@ impl<'tcx> Fpcs<'_, 'tcx> {
         let cp: &mut CapabilityProjections = self.summary[place.local].get_allocated_mut();
         let ops = cp.repack(place, self.repacker);
         self.repackings.extend(ops);
-        let kind = (*cp)[&place];
-        let bound = self.bound(place);
-        assert!(kind.minimum(bound).unwrap() >= cap, "{place:?}, have: {kind:?}, bound: {bound:?}, want: {cap:?}");
+        let kind = cp.insert(place, cap).unwrap();
+        let bounded = self.bound(place).minimum(kind).unwrap();
+        assert!(bounded >= cap);
+        if bounded != cap && matches!(cap, CapabilityKind::Write) {
+            self.repackings.push(RepackOp::Weaken(place, kind, cap));
+        }
     }
 
     pub(crate) fn ensures_unalloc(&mut self, local: Local) {