Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 17 additions & 0 deletions .github/workflows/test.yml
Original file line number Diff line number Diff line change
Expand Up @@ -164,6 +164,23 @@ jobs:
working-directory: flowistry/crates/flowistry
run: cargo test

check_generated_types:
runs-on: ${{ vars.RUNNER || 'ubuntu-latest' }}
container: ${{ fromJSON(vars.CONTAINER || 'null') }}
steps:
- uses: actions/checkout@v4
- name: Save current generated types
run: cp visualization/src/generated/types.ts /tmp/types.ts.before
- name: Generate TypeScript types
run: cargo run --manifest-path type-export/Cargo.toml --bin generate_types
- name: Check generated types are up-to-date
run: |
if ! diff /tmp/types.ts.before visualization/src/generated/types.ts; then
echo "ERROR: Generated TypeScript types are out of date."
echo "Run 'cargo run --manifest-path type-export/Cargo.toml --bin generate_types' to update."
exit 1
fi

build_visualization:
runs-on: ubuntu-latest
steps:
Expand Down
24 changes: 12 additions & 12 deletions src/borrow_pcg/graph/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -164,6 +164,18 @@ impl<'tcx, EdgeKind, VC> BorrowsGraph<'tcx, EdgeKind, VC> {
})
.collect()
}

pub(crate) fn edges_blocking<'slf, Ctxt: Copy + DebugCtxt, P: PcgNodeComponent>(
&'slf self,
node: BlockedNode<'tcx, P>,
ctxt: Ctxt,
) -> impl Iterator<Item = BorrowPcgEdgeRef<'tcx, 'slf, EdgeKind, VC>>
where
EdgeKind: EdgeData<'tcx, Ctxt, P> + std::hash::Hash + Eq,
{
self.edges()
.filter(move |edge| edge.kind.blocks_node(node, ctxt))
}
}

impl<'tcx, P: PcgNodeComponent, VC> BorrowsGraph<'tcx, BorrowPcgEdgeKind<'tcx, P>, VC> {
Expand Down Expand Up @@ -233,18 +245,6 @@ impl<'tcx, P: PcgNodeComponent, VC> BorrowsGraph<'tcx, BorrowPcgEdgeKind<'tcx, P
.all(|place| nodes.contains(&place.to_pcg_node(ctxt))))
}

pub(crate) fn edges_blocking<'slf, Ctxt: Copy + DebugCtxt>(
&'slf self,
node: BlockedNode<'tcx, P>,
ctxt: Ctxt,
) -> impl Iterator<Item = BorrowPcgEdgeRef<'tcx, 'slf, BorrowPcgEdgeKind<'tcx, P>, VC>>
where
BorrowPcgEdgeKind<'tcx, P>: EdgeData<'tcx, Ctxt, P>,
{
self.edges()
.filter(move |edge| edge.kind.blocks_node(node, ctxt))
}

pub fn edges_blocked_by<'graph, Ctxt: Copy + DebugCtxt>(
&'graph self,
node: LocalNode<'tcx, P>,
Expand Down
13 changes: 13 additions & 0 deletions src/borrow_pcg/state/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -349,6 +349,19 @@ pub(crate) trait BorrowsStateLike<'tcx, EdgeKind = BorrowPcgEdgeKind<'tcx>, VC =
};
Ok(result)
}

fn edges_blocking<'slf, Ctxt: Copy + DebugCtxt>(
&'slf self,
node: BlockedNode<'tcx>,
ctxt: Ctxt,
) -> impl Iterator<Item = BorrowPcgEdgeRef<'tcx, 'slf, EdgeKind, VC>>
where
EdgeKind: EdgeData<'tcx, Ctxt, Place<'tcx>> + std::hash::Hash + Eq + 'slf,
VC: 'slf,
'tcx: 'slf,
{
self.graph().edges_blocking(node, ctxt)
}
}

impl<'pcg, 'tcx: 'pcg> BorrowsStateLike<'tcx> for BorrowStateMutRef<'pcg, 'tcx> {
Expand Down
6 changes: 5 additions & 1 deletion src/pcg/domain/pcg.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ use std::borrow::Cow;
use crate::{
DebugLines, Weaken,
borrow_pcg::{
edge::kind::BorrowPcgEdgeKind,
edge::{borrow::BorrowEdge, kind::BorrowPcgEdgeKind},
graph::{BorrowsGraph, join::JoinBorrowsArgs},
state::{BorrowStateMutRef, BorrowStateRef, BorrowsState, BorrowsStateLike},
},
Expand Down Expand Up @@ -327,6 +327,10 @@ impl<'a, 'tcx: 'a> Pcg<'a, 'tcx> {
&self.owned
}

pub(crate) fn borrow_created_at(&self, location: mir::Location) -> Option<&BorrowEdge<'tcx>> {
self.borrow.graph().borrow_created_at(location)
}

#[must_use]
pub fn borrow_pcg(&self) -> &BorrowsState<'a, 'tcx> {
&self.borrow
Expand Down
22 changes: 11 additions & 11 deletions src/pcg/visitor/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,9 +15,10 @@ use crate::{
obtain::{PlaceCollapser, PlaceObtainer, expand::PlaceExpander},
place_capabilities::{PlaceCapabilitiesInterface, PlaceCapabilitiesReader},
triple::TripleWalker,
visitor::upgrade::AdjustCapabilityReason,
},
rustc_interface::middle::mir::{self, Location, Operand, Rvalue, Statement, Terminator},
utils::{PlaceLike, data_structures::HashSet, display::DisplayWithCompilerCtxt},
utils::{data_structures::HashSet, display::DisplayWithCompilerCtxt},
};

use crate::utils::{
Expand Down Expand Up @@ -418,21 +419,20 @@ impl<'a, 'tcx: 'a, Ctxt: DataflowCtxt<'a, 'tcx>> PcgVisitor<'_, 'a, 'tcx, Ctxt>
&mut self,
created_location: Location,
) -> Result<(), PcgError<'tcx>> {
let Some(borrow) = self.pcg.borrow.graph().borrow_created_at(created_location) else {
let Some(borrow) = self.pcg.borrow_created_at(created_location) else {
return Ok(());
};
tracing::debug!(
"activate twophase borrow: {}",
tracing::info!(
"{:?} activate twophase borrow: {}",
self.location(),
borrow.display_string(self.ctxt.bc_ctxt())
);
let blocked_place = borrow.blocked_place.place();
if !blocked_place.is_owned(self.ctxt) {
self.place_obtainer()
.remove_read_permission_upwards_and_label_rps(
blocked_place,
"Activate twophase borrow",
)?;
}
self.place_obtainer()
.remove_read_permission_upwards_and_label_rps(
blocked_place,
AdjustCapabilityReason::TwoPhaseBorrowActivation,
)?;
Ok(())
}
}
Expand Down
6 changes: 5 additions & 1 deletion src/pcg/visitor/obtain.rs
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ use crate::{
BlockType, PlaceCapabilitiesInterface, PlaceCapabilitiesReader,
SymbolicPlaceCapabilities,
},
visitor::upgrade::AdjustCapabilityReason,
},
pcg_validity_assert,
rustc_interface::middle::mir,
Expand Down Expand Up @@ -420,7 +421,10 @@ impl<'state, 'a: 'state, 'tcx: 'a, Ctxt: DataflowCtxt<'a, 'tcx>>
)?;
self.remove_read_permission_downwards(place)?;
if let Some(parent) = place.parent_place() {
self.remove_read_permission_upwards_and_label_rps(parent, "Upgrade read to exclusive")?;
self.remove_read_permission_upwards_and_label_rps(
parent,
AdjustCapabilityReason::UpgradeReadToExclusive,
)?;
}
Ok(())
}
Expand Down
58 changes: 43 additions & 15 deletions src/pcg/visitor/upgrade.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ use crate::{
pcg::{
CapabilityKind, PcgNode, PcgRefLike,
obtain::{HasSnapshotLocation, PlaceObtainer},
place_capabilities::{BlockType, PlaceCapabilitiesReader},
place_capabilities::BlockType,
},
utils::{
DataflowCtxt, DebugCtxt, Place, PlaceLike, data_structures::HashSet,
Expand All @@ -27,10 +27,10 @@ use crate::{
impl<'state, 'a: 'state, 'tcx: 'a, Ctxt: DataflowCtxt<'a, 'tcx> + DebugCtxt>
PlaceObtainer<'state, 'a, 'tcx, Ctxt>
{
fn weaken_place_from_read_upwards(
fn weaken_capability_from_read(
&mut self,
place: Place<'tcx>,
debug_ctxt: &str,
reason: AdjustCapabilityReason,
) -> Result<(), PcgError<'tcx>> {
if place.is_mut_ref(self.ctxt) {
// We've reached an indirection (e.g from **s to *s), we
Expand All @@ -43,8 +43,8 @@ impl<'state, 'a: 'state, 'tcx: 'a, Ctxt: DataflowCtxt<'a, 'tcx> + DebugCtxt>
CapabilityKind::Read,
BlockType::DerefMutRefForExclusive.blocked_place_maximum_retained_capability(),
format!(
"{}: remove read permission upwards from base place {} (downgrade R to W for mut ref)",
debug_ctxt,
"{:?}: remove read permission upwards from base place {} (downgrade R to W for mut ref)",
reason,
place.display_string(self.ctxt.bc_ctxt()),
)
)
Expand All @@ -57,8 +57,8 @@ impl<'state, 'a: 'state, 'tcx: 'a, Ctxt: DataflowCtxt<'a, 'tcx> + DebugCtxt>
CapabilityKind::Read,
None,
format!(
"{}: remove read permission upwards from base place {}",
debug_ctxt,
"{:?}: remove read permission upwards from base place {}",
reason,
place.display_string(self.ctxt.bc_ctxt()),
),
)
Expand All @@ -75,13 +75,16 @@ impl<'state, 'a: 'state, 'tcx: 'a, Ctxt: DataflowCtxt<'a, 'tcx> + DebugCtxt>
pub(crate) fn remove_read_permission_upwards_and_label_rps(
&mut self,
place: Place<'tcx>,
debug_ctxt: &str,
reason: AdjustCapabilityReason,
) -> Result<(), PcgError<'tcx>> {
let place_regions = place.regions(self.ctxt);
let mut prev = None;
let mut current = place;
while self.pcg.capabilities.get(current, self.ctxt) == Some(CapabilityKind::Read.into()) {
self.weaken_place_from_read_upwards(current, debug_ctxt)?;
while self
.pcg
.place_capability_equals(current, CapabilityKind::Read)
{
self.weaken_capability_from_read(current, reason)?;
let leaf_nodes = self.pcg.borrow.leaf_nodes(self.ctxt.bc_ctxt());
for place in self.pcg.borrow.graph.places(self.ctxt.bc_ctxt()) {
if prev != Some(place)
Expand All @@ -97,8 +100,8 @@ impl<'state, 'a: 'state, 'tcx: 'a, Ctxt: DataflowCtxt<'a, 'tcx> + DebugCtxt>
place,
CapabilityKind::Exclusive,
format!(
"{}: remove_read_permission_upwards_and_label_rps: restore exclusive cap for leaf place {}",
debug_ctxt,
"{:?}: remove_read_permission_upwards_and_label_rps: restore exclusive cap for leaf place {}",
reason,
place.display_string(self.ctxt.bc_ctxt())
),
)
Expand All @@ -123,7 +126,6 @@ impl<'state, 'a: 'state, 'tcx: 'a, Ctxt: DataflowCtxt<'a, 'tcx> + DebugCtxt>
let edges_blocking_current_rp = self
.pcg
.borrow
.graph
.edges_blocking(current_rp.into(), self.ctxt.bc_ctxt())
.collect::<Vec<_>>();
if !edges_blocking_current_rp.is_empty() {
Expand Down Expand Up @@ -154,8 +156,8 @@ impl<'state, 'a: 'state, 'tcx: 'a, Ctxt: DataflowCtxt<'a, 'tcx> + DebugCtxt>
LabelNodePredicate::equals_lifetime_projection(current_rp.into()),
Some(self.prev_snapshot_location().into()),
format!(
"{}: remove_read_permission_upwards_and_label_rps: label current lifetime projection {} with previous snapshot location {:?}",
debug_ctxt,
"{:?}: remove_read_permission_upwards_and_label_rps: label current lifetime projection {} with previous snapshot location {:?}",
reason,
current_rp.display_string(self.ctxt.bc_ctxt()),
self.prev_snapshot_location()
),
Expand Down Expand Up @@ -220,3 +222,29 @@ impl<'state, 'a: 'state, 'tcx: 'a, Ctxt: DataflowCtxt<'a, 'tcx> + DebugCtxt>
Ok(())
}
}

/// The reason for performing in-place updates on the PCG capabilities.
#[derive(Debug, Clone, Copy, Eq, PartialEq, Hash)]
pub(crate) enum AdjustCapabilityReason {
/// Just prior to activating a two-phase borrow, the capability of the
/// blocked place is R. The PCG evaluates the two-phase borrow by removing
/// this capability and adjusting the capabilities of the parents of the
/// blocked place as well as their related places. In particular, if the
/// blocked place's parent place also has capability R, it should be removed
/// as well.
TwoPhaseBorrowActivation,

/// Currently, there are situations in the analysis that require obtaining
/// capability E to a place with capability R. In particular, consider the following code:
/// ```rust
/// let mut pair = (String::new(), String::new());
/// let fst = &pair.0;
/// let snd = pair.1;
/// ```
/// For the assignment to `fst`, the PCG will weaken `pair` to capability
/// `R`, and then unpack it. Therefore, `pair.1` will have capability `R`.
/// The assignment to `snd` requires obtaining capability `E` to `pair.1`,
/// To handle this case, we would remove capability from `pair` and upgrade
/// `pair.1` to `E`.
UpgradeReadToExclusive,
}
6 changes: 5 additions & 1 deletion src/utils/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -228,7 +228,11 @@ impl PcgSettings {
tracing::info!("Using user path for {var_name}: {:?}", user_path);
match user_path.canonicalize() {
Ok(path) => tracing::info!("Absolute path: {:?}", path),
Err(e) => tracing::error!("User path cannot be canonicalized: {e}"),
Err(e) => tracing::error!(
"User path {} cannot be canonicalized from current directory {}: {e}",
user_path.display(),
std::env::current_dir().unwrap().display()
),
}
user_path
} else {
Expand Down
18 changes: 18 additions & 0 deletions test-files/219_twophase.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
struct Tmp {}

impl Tmp {
fn read(&self) -> Self {
Tmp {}
}

fn write (&mut self, x: Self) {

}
}

fn foo() {
let mut x = Tmp {};
x.write(x.read());
// PCG: bb1[1] pre_operands: Weaken x from R to None
// `x`'s capability should be removed when the two-phase borrow is activated
}
29 changes: 26 additions & 3 deletions type-export/Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Loading
Loading