Explicit capability changes: action deltas, freezes, two-phase activation, joins as reached meets

src/action.rs

@@ -14,11 +14,11 @@ use crate::{
         unblock_graph::BorrowPcgUnblockAction,
         validity_conditions::ValidityConditions,
     },
-    owned_pcg::{RegainedCapability, RepackOp},
-    pcg::capabilities::CapabilityKind,
+    owned_pcg::RepackOp,
+    pcg::{CapabilityKind, place_capabilities::PlaceCapabilitiesInterface},
     rustc_interface::middle::mir,
     utils::{
-        DebugRepr, HasBorrowCheckerCtxt, PcgNodeComponent, Place, PlaceLike,
+        DebugRepr, HasBorrowCheckerCtxt, PcgNodeComponent, Place,
         display::{DisplayOutput, DisplayWithCtxt, OutputMode},
     },
 };
@@ -116,10 +116,6 @@ impl<'tcx> From<Vec<OwnedPcgAction<'tcx>>> for PcgActions<'tcx> {
 }
 
 impl<'tcx> PcgActions<'tcx> {
-    pub(crate) fn extend(&mut self, actions: PcgActions<'tcx>) {
-        self.actions.extend(actions.actions);
-    }
-
     /// The subset of actions applied to the Borrow PCG.
     #[must_use]
     pub fn borrow_pcg_actions(&self) -> BorrowPcgActions<'tcx> {
@@ -157,7 +153,7 @@ impl<'tcx> PcgActions<'tcx> {
             .iter()
             .filter_map(|action| match action {
                 PcgAction::Borrow(BorrowPcgAction {
-                    kind: BorrowPcgActionKind::RemoveEdge(edge),
+                    kind: BorrowPcgActionKind::RemoveEdge { edge, .. },
                     ..
                 }) => Some(BorrowPcgUnblockAction::new(edge.clone())),
                 _ => None,
@@ -166,54 +162,167 @@ impl<'tcx> PcgActions<'tcx> {
     }
 }
 
-/// A pair of a PCG action and a debug context (indicating the source of the
-/// action and possibly its effects).
+/// The capability changes of an action: each place gets the capability, or
+/// loses its capability (`None`).
+#[derive(Clone, Debug, PartialEq, Eq, Serialize)]
+#[cfg_attr(feature = "type-export", derive(ts_rs::TS))]
+#[cfg_attr(feature = "type-export", ts(export, concrete(P = String)))]
+pub struct CapabilityChanges<P>(Vec<(P, Option<CapabilityKind>)>);
+
+impl<P> Default for CapabilityChanges<P> {
+    fn default() -> Self {
+        Self(vec![])
+    }
+}
+
+impl<P> From<Vec<(P, Option<CapabilityKind>)>> for CapabilityChanges<P> {
+    fn from(changes: Vec<(P, Option<CapabilityKind>)>) -> Self {
+        Self(changes)
+    }
+}
+
+impl<P: Copy + Eq + std::hash::Hash> CapabilityChanges<P> {
+    /// Sets the change of `place`, replacing an earlier change of it.
+    pub(crate) fn set(&mut self, place: P, capability: Option<CapabilityKind>) {
+        if let Some(change) = self.0.iter_mut().find(|(p, _)| *p == place) {
+            change.1 = capability;
+        } else {
+            self.0.push((place, capability));
+        }
+    }
+
+    pub(crate) fn extend(&mut self, other: &Self) {
+        for (place, capability) in other.iter() {
+            self.set(place, capability);
+        }
+    }
+
+    pub fn iter(&self) -> impl Iterator<Item = (P, Option<CapabilityKind>)> + '_ {
+        self.0.iter().copied()
+    }
+
+    #[must_use]
+    pub fn is_empty(&self) -> bool {
+        self.0.is_empty()
+    }
+
+    pub(crate) fn apply<'tcx, Ctxt: Copy>(
+        &self,
+        capabilities: &mut impl PlaceCapabilitiesInterface<'tcx, CapabilityKind, P>,
+        ctxt: Ctxt,
+    ) -> bool {
+        let mut changed = false;
+        for (place, capability) in self.iter() {
+            changed |= match capability {
+                Some(capability) => capabilities.insert(place, capability, ctxt),
+                None => capabilities.remove(place, ctxt).is_some(),
+            };
+        }
+        changed
+    }
+}
+
+impl<Ctxt: Copy, P: DisplayWithCtxt<Ctxt>> DisplayWithCtxt<Ctxt> for CapabilityChanges<P> {
+    fn display_output(&self, ctxt: Ctxt, mode: OutputMode) -> DisplayOutput {
+        DisplayOutput::join(
+            self.0.iter().map(|(place, capability)| {
+                DisplayOutput::Seq(vec![
+                    place.display_output(ctxt, mode),
+                    ": ".into(),
+                    match capability {
+                        Some(capability) => capability.display_output(ctxt, mode),
+                        None => "None".into(),
+                    },
+                ])
+            }),
+            &", ".into(),
+        )
+    }
+}
+
+/// A PCG action, the capability changes it makes, and a debug context
+/// (indicating the source of the action and possibly its effects).
 #[derive(Clone, Debug, PartialEq, Eq, Serialize)]
 #[cfg_attr(feature = "type-export", derive(ts_rs::TS))]
 #[cfg_attr(feature = "type-export", ts(export))]
-pub struct ActionKindWithDebugInfo<T, DebugInfo = Option<DisplayOutput>> {
+pub struct ActionKindWithDebugInfo<T, P, DebugInfo = Option<DisplayOutput>> {
     pub(crate) kind: T,
+    /// The capability changes of the action. Every capability change of an
+    /// action is listed here.
+    pub(crate) capabilities: CapabilityChanges<P>,
     pub(crate) debug_info: DebugInfo,
 }
 
-impl<T> ActionKindWithDebugInfo<T> {
+impl<T, P> ActionKindWithDebugInfo<T, P> {
     pub fn kind(&self) -> &T {
         &self.kind
     }
 
+    pub fn capabilities(&self) -> &CapabilityChanges<P> {
+        &self.capabilities
+    }
+
     pub(crate) fn new(kind: T, debug_info: Option<DisplayOutput>) -> Self {
-        Self { kind, debug_info }
+        Self {
+            kind,
+            capabilities: CapabilityChanges::default(),
+            debug_info,
+        }
+    }
+
+    pub(crate) fn with_capabilities(mut self, capabilities: CapabilityChanges<P>) -> Self {
+        self.capabilities = capabilities;
+        self
     }
 
     pub(crate) fn debug_line<Ctxt>(&self, ctxt: Ctxt) -> Cow<'static, str>
     where
-        T: DisplayWithCtxt<Ctxt>,
+        Self: DisplayWithCtxt<Ctxt>,
     {
-        self.kind.display_output(ctxt, OutputMode::Test).into_text()
+        self.display_output(ctxt, OutputMode::Test).into_text()
     }
 }
 
-impl<Ctxt, T: DebugRepr<Ctxt>> DebugRepr<Ctxt> for ActionKindWithDebugInfo<T> {
-    type Repr = ActionKindWithDebugInfo<T::Repr, Option<String>>;
+impl<Ctxt: Copy, T: DebugRepr<Ctxt>, P: DisplayWithCtxt<Ctxt>> DebugRepr<Ctxt>
+    for ActionKindWithDebugInfo<T, P>
+{
+    type Repr = ActionKindWithDebugInfo<T::Repr, String, Option<String>>;
     fn debug_repr(&self, ctxt: Ctxt) -> Self::Repr {
         ActionKindWithDebugInfo {
             kind: self.kind.debug_repr(ctxt),
+            capabilities: CapabilityChanges(
+                self.capabilities
+                    .0
+                    .iter()
+                    .map(|(place, capability)| {
+                        (
+                            place
+                                .display_output(ctxt, OutputMode::Normal)
+                                .into_text()
+                                .to_string(),
+                            *capability,
+                        )
+                    })
+                    .collect(),
+            ),
             debug_info: self.debug_info.as_ref().map(|ctxt| ctxt.debug_repr(())),
         }
     }
 }
 
-impl<Ctxt, T: DisplayWithCtxt<Ctxt>> DisplayWithCtxt<Ctxt> for ActionKindWithDebugInfo<T> {
-    fn display_output(&self, ctxt: Ctxt, mode: OutputMode) -> DisplayOutput {
-        self.kind.display_output(ctxt, mode)
-    }
-}
-
 /// An action applied to the Owned PCG during the PCG analysis
 /// for which consumers (e.g. Prusti) may wish to perform
 /// their own effect (e.g. folding a predicate).
 pub type OwnedPcgAction<'tcx, P = Place<'tcx>> =
-    ActionKindWithDebugInfo<RepackOp<'tcx, mir::Local, P>>;
+    ActionKindWithDebugInfo<RepackOp<'tcx, mir::Local, P>, P>;
+
+impl<Ctxt, P: std::fmt::Debug + DisplayWithCtxt<Ctxt>> DisplayWithCtxt<Ctxt>
+    for OwnedPcgAction<'_, P>
+{
+    fn display_output(&self, ctxt: Ctxt, mode: OutputMode) -> DisplayOutput {
+        self.kind.display_output(ctxt, mode)
+    }
+}
 
 /// An action applied to the Borrow PCG during the PCG analysis
 /// for which consumers (e.g. Prusti) may wish to perform
@@ -223,7 +332,7 @@ pub type BorrowPcgAction<
     EdgeKind = BorrowPcgEdgeKind<'tcx>,
     P = Place<'tcx>,
     VC = ValidityConditions,
-> = ActionKindWithDebugInfo<BorrowPcgActionKind<'tcx, EdgeKind, P, VC>>;
+> = ActionKindWithDebugInfo<BorrowPcgActionKind<'tcx, EdgeKind, P, VC>, P>;
 
 mod private {
     use serde_derive::Serialize;
@@ -255,6 +364,12 @@ impl<'tcx, EdgeKind, P, VC> From<OwnedPcgAction<'tcx, P>> for PcgAction<'tcx, Ed
     }
 }
 
+impl<'tcx, EdgeKind, VC> From<RepackOp<'tcx>> for PcgAction<'tcx, EdgeKind, Place<'tcx>, VC> {
+    fn from(repack: RepackOp<'tcx>) -> Self {
+        OwnedPcgAction::new(repack, None).into()
+    }
+}
+
 /// An action applied to the PCG during the PCG analysis.
 pub type PcgAction<
     'tcx,
@@ -264,8 +379,8 @@ pub type PcgAction<
 > = private::GenericPcgAction<BorrowPcgAction<'tcx, EdgeKind, P, VC>, OwnedPcgAction<'tcx, P>>;
 
 pub(crate) type PcgActionDebugRepr = private::GenericPcgAction<
-    ActionKindWithDebugInfo<BorrowPcgActionKindDebugRepr, Option<String>>,
-    ActionKindWithDebugInfo<RepackOp<'static, String, String, String>, Option<String>>,
+    ActionKindWithDebugInfo<BorrowPcgActionKindDebugRepr, String, Option<String>>,
+    ActionKindWithDebugInfo<RepackOp<'static, String, String, String>, String, Option<String>>,
 >;
 
 impl<'a, 'tcx: 'a, Ctxt: HasBorrowCheckerCtxt<'a, 'tcx>> DebugRepr<Ctxt> for PcgAction<'tcx> {
@@ -279,34 +394,11 @@ impl<'a, 'tcx: 'a, Ctxt: HasBorrowCheckerCtxt<'a, 'tcx>> DebugRepr<Ctxt> for Pcg
     }
 }
 
-impl<'tcx, P: PcgNodeComponent, VC> PcgAction<'tcx, BorrowPcgEdgeKind<'tcx, P>, P, VC> {
-    pub(crate) fn restore_capability<Ctxt>(
-        place: P,
-        capability: CapabilityKind,
-        debug_context: impl Into<DisplayOutput>,
-        ctxt: Ctxt,
-    ) -> Self
-    where
-        P: PlaceLike<'tcx, Ctxt>,
-    {
-        let debug_context: DisplayOutput = debug_context.into();
-        if place.is_owned(ctxt) {
-            PcgAction::<'tcx, BorrowPcgEdgeKind<'tcx, P>, P, VC>::Owned(OwnedPcgAction {
-                kind: RepackOp::RegainLoanedCapability(RegainedCapability::new(place, capability)),
-                debug_info: Some(debug_context),
-            })
-        } else {
-            BorrowPcgAction::restore_capability(place, capability, debug_context).into()
-        }
-    }
-}
-
 impl<'tcx, EdgeKind, P: PcgNodeComponent, VC> PcgAction<'tcx, EdgeKind, P, VC> {
     pub(crate) fn debug_line<Ctxt>(&self, ctxt: Ctxt) -> Cow<'static, str>
     where
-        BorrowPcgActionKind<'tcx, EdgeKind, P, VC>: DisplayWithCtxt<Ctxt>,
+        BorrowPcgAction<'tcx, EdgeKind, P, VC>: DisplayWithCtxt<Ctxt>,
         OwnedPcgAction<'tcx, P>: DisplayWithCtxt<Ctxt>,
-        P: DisplayWithCtxt<Ctxt>,
     {
         match self {
             PcgAction::Borrow(action) => action.debug_line(ctxt),

src/borrow_checker/mod.rs

@@ -137,33 +137,17 @@ impl<'tcx, T: RustBorrowCheckerInterface<'tcx> + DisplayCtxtFor<RegionVid>>
         location: Location,
         ctxt: CompilerCtxt<'_, 'tcx>,
     ) -> bool {
-        let mut conflict = false;
-        each_borrow_involving_path(
-            &mut (),
-            ctxt,
-            blocked_place,
-            self.borrow_set(),
-            |borrow_index| self.borrow_in_scope_at(borrow_index, location),
-            |_this, borrow_index, _borrow| {
-                tracing::debug!(
-                    "Checking if {} contains {:?} at {:?}",
-                    blocking_place.display_string(ctxt),
-                    borrow_index,
-                    location
-                );
-                if blocking_place
-                    .regions(ctxt)
-                    .iter()
-                    .any(|region| self.origin_contains_loan_at(*region, borrow_index, location))
-                {
-                    conflict = true;
-                    ControlFlow::Break(())
-                } else {
-                    ControlFlow::Continue(())
-                }
-            },
-        );
-        conflict
+        holds_loan_of(self, blocking_place, blocked_place, false, location, ctxt)
+    }
+
+    fn blocks_entirely(
+        &self,
+        blocking_place: Place<'tcx>,
+        blocked_place: Place<'tcx>,
+        location: Location,
+        ctxt: CompilerCtxt<'_, 'tcx>,
+    ) -> bool {
+        holds_loan_of(self, blocking_place, blocked_place, true, location, ctxt)
     }
 
     fn as_dyn(&self) -> &dyn BorrowCheckerInterface<'tcx> {
@@ -187,6 +171,47 @@ impl<'tcx, T: RustBorrowCheckerInterface<'tcx> + DisplayCtxtFor<RegionVid>>
     }
 }
 
+/// Whether a region of `blocking_place` contains, at `location`, a loan in
+/// scope that conflicts with `blocked_place`; if `entirely`, a loan of
+/// `blocked_place` itself or of a place it is part of.
+fn holds_loan_of<'tcx>(
+    bc: &impl RustBorrowCheckerInterface<'tcx>,
+    blocking_place: Place<'tcx>,
+    blocked_place: Place<'tcx>,
+    entirely: bool,
+    location: Location,
+    ctxt: CompilerCtxt<'_, 'tcx>,
+) -> bool {
+    let mut conflict = false;
+    each_borrow_involving_path(
+        &mut (),
+        ctxt,
+        blocked_place,
+        bc.borrow_set(),
+        |borrow_index| bc.borrow_in_scope_at(borrow_index, location),
+        |_this, borrow_index, borrow| {
+            tracing::debug!(
+                "Checking if {} contains {:?} at {:?}",
+                blocking_place.display_string(ctxt),
+                borrow_index,
+                location
+            );
+            if (!entirely || borrow.get_borrowed_place().is_prefix_of(blocked_place))
+                && blocking_place
+                    .regions(ctxt)
+                    .iter()
+                    .any(|region| bc.origin_contains_loan_at(*region, borrow_index, location))
+            {
+                conflict = true;
+                ControlFlow::Break(())
+            } else {
+                ControlFlow::Continue(())
+            }
+        },
+    );
+    conflict
+}
+
 pub trait BorrowCheckerInterface<'tcx>: DisplayCtxtFor<RegionVid> {
     /* Main Interface Start */
 
@@ -211,6 +236,17 @@ pub trait BorrowCheckerInterface<'tcx>: DisplayCtxtFor<RegionVid> {
         ctxt: CompilerCtxt<'_, 'tcx>,
     ) -> bool;
 
+    /// Like [`Self::blocks`], but only for a loan of `blocked_place` itself or
+    /// of a place it is part of: all of `blocked_place` is lent, not just one
+    /// of its parts.
+    fn blocks_entirely(
+        &self,
+        blocking_place: Place<'tcx>,
+        blocked_place: Place<'tcx>,
+        location: Location,
+        ctxt: CompilerCtxt<'_, 'tcx>,
+    ) -> bool;
+
     /// Returns true iff `sup` is required to outlive `sub` at `location`.
     fn outlives(&self, sup: PcgRegion<'tcx>, sub: PcgRegion<'tcx>, location: Location) -> bool;