Add weakens before write

viperproject · Oct 20, 2023 · 8e4030c · 8e4030c
1 parent 4467796
commit 8e4030c
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 3 deletions.
diff --git a/mir-state-analysis/src/free_pcs/impl/triple.rs b/mir-state-analysis/src/free_pcs/impl/triple.rs
@@ -79,13 +79,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
@@ -55,8 +55,11 @@ 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 kind = cp.insert(place, cap).unwrap();
         assert!(kind >= cap);
+        if kind != cap {
+            self.repackings.push(RepackOp::Weaken(place, kind, cap));
+        }
     }
 
     pub(crate) fn ensures_unalloc(&mut self, local: Local) {