Add weakens before write

viperproject · Oct 20, 2023 · 58fe3c5 · 58fe3c5
1 parent 58d03fb
commit 58fe3c5
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 5 deletions.
diff --git 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
@@ -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) {