Skip to content

Commit

Permalink
Ignore path liveness when collecting actual/expected permissions in b…
Browse files Browse the repository at this point in the history
…oundary analysis.
  • Loading branch information
gavinleroy committed Dec 28, 2024
1 parent 2f02d23 commit 8855299
Show file tree
Hide file tree
Showing 24 changed files with 286 additions and 302 deletions.
13 changes: 8 additions & 5 deletions crates/aquascope/src/analysis/boundaries/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -223,7 +223,8 @@ pub struct PermissionsBoundary {
#[serde(skip)]
byte_location: BytePos,
pub expected: Permissions,
pub actual: PermissionsData,
pub actual: Permissions,
pub data: PermissionsData,
#[serde(skip_serializing_if = "Option::is_none")]
pub expecting_flow: Option<FlowBoundary>,
}
Expand All @@ -232,7 +233,7 @@ impl PermissionsBoundary {
pub fn is_violation(&self) -> bool {
macro_rules! is_missing {
($this:ident, $perm:ident) => {
($this.expected.$perm && !$this.actual.permissions.$perm)
($this.expected.$perm && !$this.actual.$perm)
};
}

Expand Down Expand Up @@ -735,11 +736,11 @@ fn path_to_perm_boundary<'tcx>(
&path_locations,
)?;

log::debug!("Chosen place at location {place:#?} {loc:#?} other options: {path_locations:#?}");

let point = ctxt.location_to_point(loc);
let path = ctxt.place_to_path(&place);

log::debug!("Chosen place at location {place:#?} {loc:#?} ({point:?},{path:?})\nOther options: {path_locations:#?}");

Some((point, path))
};

Expand All @@ -755,8 +756,9 @@ fn path_to_perm_boundary<'tcx>(
})
})
.map(|(point, path)| {
let actual = ctxt.permissions_data_at_point(path, point);
let data = ctxt.permissions_data_at_point(path, point);
let expected = path_boundary.expected;
let actual = data.permissions_ignore_liveness();

let expecting_flow =
get_flow_permission(analysis, path_boundary.flow_context, hir_id);
Expand All @@ -781,6 +783,7 @@ fn path_to_perm_boundary<'tcx>(
byte_location,
expected: expected.into(),
actual,
data,
expecting_flow,
}
});
Expand Down
39 changes: 2 additions & 37 deletions crates/aquascope/src/analysis/permissions/context.rs
Original file line number Diff line number Diff line change
Expand Up @@ -300,11 +300,6 @@ impl<'tcx> PermissionsCtxt<'tcx> {
loan_read_refined: None,
loan_write_refined: None,
loan_drop_refined: None,
permissions: Permissions {
read: true,
write: true,
drop: true,
},
}
}

Expand Down Expand Up @@ -349,6 +344,8 @@ impl<'tcx> PermissionsCtxt<'tcx> {
path: Path,
point: Point,
) -> PermissionsData {
log::trace!("permissions_data_at_point: {:?} at {:?}", path, point);

let empty_hash_move = &HashMap::default();
let empty_hash_loan = &HashMap::default();
let empty_set = &HashSet::default();
Expand Down Expand Up @@ -384,36 +381,6 @@ impl<'tcx> PermissionsCtxt<'tcx> {
let loan_drop_refined: Option<LoanKey> =
loan_drop_refined.get(path).map(Into::<LoanKey>::into);

let mem_uninit = path_moved.is_some() || path_uninitialized;

// An English description of the previous Datalog rules:
//
// A path is readable IFF:
// - it is not moved.
// - there doesn't exist a read-refining loan at this point.
//
// A path is writeable IFF:
// - the path's declared type allows for mutability.
// - the path is readable (you can't write if you can't read)
// this implies that the path isn't moved.
// - there doesn't exist a write-refining loan at this point.
//
// A path is droppable(without copy) IFF:
// - the path's declared type is droppable.
// - it isn't moved.
// - no drop-refining loan exists at this point.
let permissions = if !is_live {
Permissions::bottom()
} else {
let read = !mem_uninit && loan_read_refined.is_none();

let write = type_writeable && read && loan_write_refined.is_none();

let drop = type_droppable && read && loan_drop_refined.is_none();

Permissions { read, write, drop }
};

PermissionsData {
type_droppable,
type_writeable,
Expand All @@ -424,7 +391,6 @@ impl<'tcx> PermissionsCtxt<'tcx> {
loan_read_refined,
loan_write_refined,
loan_drop_refined,
permissions,
}
}

Expand All @@ -450,7 +416,6 @@ impl<'tcx> PermissionsCtxt<'tcx> {
loan_read_refined: None,
loan_write_refined: None,
loan_drop_refined: None,
permissions: Permissions::bottom(),
})
})
.collect::<HashMap<_, _>>()
Expand Down
37 changes: 35 additions & 2 deletions crates/aquascope/src/analysis/permissions/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -113,9 +113,42 @@ pub struct PermissionsData {
#[serde(skip_serializing_if = "Option::is_none")]
/// Is a live loan removing `drop` permissions?
pub loan_drop_refined: Option<LoanKey>,
}

impl PermissionsData {
/// If the place is not live, then the permissions are always the bottom type.
/// Otherwise, see `permissions_ignore_liveness`. (You may want to ignore liveness
/// when you know a variable is being used, and should therefore be live.)
pub fn permissions(&self) -> Permissions {
if !self.is_live {
Permissions::bottom()
} else {
self.permissions_ignore_liveness()
}
}

/// Computed permissions given the above information.
pub permissions: Permissions,
/// A path is readable IFF:
/// - it is not moved.
/// - there doesn't exist a read-refining loan at this point.
///
/// A path is writeable IFF:
/// - the path's declared type allows for mutability.
/// - the path is readable (you can't write if you can't read)
/// this implies that the path isn't moved.
/// - there doesn't exist a write-refining loan at this point.
///
/// A path is droppable(without copy) IFF:
/// - the path's declared type is droppable.
/// - it isn't moved.
/// - no drop-refining loan exists at this point.
pub fn permissions_ignore_liveness(&self) -> Permissions {
let mem_uninit = self.path_moved.is_some() || self.path_uninitialized;
let read = !mem_uninit && self.loan_read_refined.is_none();
let write =
self.type_writeable && read && self.loan_write_refined.is_none();
let drop = self.type_droppable && read && self.loan_drop_refined.is_none();
Permissions { read, write, drop }
}
}

/// A permissions refiner. [`Loan`]s and moves can refine permissions.
Expand Down
17 changes: 8 additions & 9 deletions crates/aquascope/src/analysis/permissions/utils.rs
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,8 @@ pub(crate) fn dump_mir_debug(ctxt: &PermissionsCtxt) {
},
)
.unwrap();

log::debug!("{:?}", ctxt.polonius_output);
}

// --------------------------------------------------
Expand Down Expand Up @@ -67,7 +69,7 @@ impl JoinSemiLattice for PermissionsDomain<'_> {
for (place, perms) in other.0.iter() {
match self.0.entry(*place) {
Entry::Occupied(mut entry) => {
changed |= entry.get_mut().permissions.join(&perms.permissions);
changed |= entry.get_mut().permissions().join(&perms.permissions());
}
Entry::Vacant(entry) => {
entry.insert(*perms);
Expand Down Expand Up @@ -119,7 +121,7 @@ impl<C> DebugWithContext<C> for PermissionsDomain<'_> {
r#"<table border="0" cellborder="1" cellspacing="0" cellpadding="2">"#
)?;
for (place, perms) in self.iter() {
let perms = perms.permissions;
let perms = perms.permissions();
write!(
f,
r#"<tr><td align="left">{place:?}</td><td align="left">{perms:?}</td></tr>"#
Expand All @@ -137,11 +139,11 @@ impl<C> DebugWithContext<C> for PermissionsDomain<'_> {
f: &mut std::fmt::Formatter<'_>,
) -> std::fmt::Result {
let no_perm_changes = self.0.iter().all(|(place, permsd)| {
let perms = permsd.permissions;
let perms = permsd.permissions();
old
.0
.get(place)
.map_or(true, |permd| permd.permissions == perms)
.map_or(true, |permd| permd.permissions() == perms)
});

if old == self || no_perm_changes {
Expand All @@ -153,10 +155,10 @@ impl<C> DebugWithContext<C> for PermissionsDomain<'_> {
r#"<table border="0" cellborder="1" cellspacing="0" cellpadding="2" sides="rb">"#
)?;
for (place, perms) in self.0.iter() {
let perms = perms.permissions;
let perms = perms.permissions();
match old.0.get(place) {
Some(old_perms) => {
let old_perms = old_perms.permissions;
let old_perms = old_perms.permissions();
if perms != old_perms {
write!(
f,
Expand Down Expand Up @@ -214,8 +216,6 @@ impl<'tcx> Analysis<'tcx> for PAnalysis<'_, 'tcx> {
.domain_places()
.into_iter()
.map(|place| {
let path = self.ctxt.place_to_path(&place);
let mp = self.ctxt.max_permissions(path);
// NOTE: I'm currently just ignoring the permissions data
// for this utility just so we can see the permissions changes.
(place, PermissionsData {
Expand All @@ -228,7 +228,6 @@ impl<'tcx> Analysis<'tcx> for PAnalysis<'_, 'tcx> {
loan_read_refined: None,
loan_write_refined: None,
loan_drop_refined: None,
permissions: mp,
})
})
.collect::<HashMap<_, _>>()
Expand Down
2 changes: 1 addition & 1 deletion crates/aquascope/src/analysis/stepper/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -266,7 +266,7 @@ impl Difference for PermissionsData {
loan_drop_refined: self.loan_drop_refined.diff(rhs.loan_drop_refined),
path_moved: self.path_moved.diff(rhs.path_moved),
path_uninitialized: self.path_uninitialized.diff(rhs.path_uninitialized),
permissions: self.permissions.diff(rhs.permissions),
permissions: self.permissions().diff(rhs.permissions()),
}
}
}
Expand Down
5 changes: 3 additions & 2 deletions crates/aquascope/src/test_utils.rs
Original file line number Diff line number Diff line change
Expand Up @@ -272,8 +272,9 @@ pub fn test_refinements_in_file(path: &Path) {

let path = ctxt.place_to_path(&place);
let point = ctxt.location_to_point(loc);
let computed_perms =
ctxt.permissions_data_at_point(path, point).permissions;
let computed_perms = ctxt
.permissions_data_at_point(path, point)
.permissions_ignore_liveness();

assert!(
(*expected_perms == computed_perms),
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -10,15 +10,15 @@ description: bar@coerced_0.test
write: true
drop: false
actual:
read: true
write: true
drop: true
data:
type_droppable: true
type_writeable: true
type_copyable: false
is_live: true
path_uninitialized: false
permissions:
read: true
write: true
drop: true
- location:
line: 3
column: 29
Expand All @@ -27,15 +27,15 @@ description: bar@coerced_0.test
write: true
drop: false
actual:
read: true
write: true
drop: false
data:
type_droppable: false
type_writeable: true
type_copyable: false
is_live: true
path_uninitialized: false
permissions:
read: true
write: true
drop: false
- location:
line: 4
column: 9
Expand All @@ -44,15 +44,15 @@ description: bar@coerced_0.test
write: true
drop: false
actual:
read: true
write: true
drop: false
data:
type_droppable: false
type_writeable: true
type_copyable: false
is_live: true
path_uninitialized: false
permissions:
read: true
write: true
drop: false
- location:
line: 5
column: 3
Expand All @@ -61,13 +61,12 @@ description: bar@coerced_0.test
write: true
drop: false
actual:
read: true
write: true
drop: false
data:
type_droppable: false
type_writeable: true
type_copyable: false
is_live: true
path_uninitialized: false
permissions:
read: true
write: true
drop: false

Original file line number Diff line number Diff line change
Expand Up @@ -10,13 +10,12 @@ description: foo@mut_assign.test
write: true
drop: false
actual:
read: true
write: true
drop: false
data:
type_droppable: false
type_writeable: true
type_copyable: false
is_live: true
path_uninitialized: false
permissions:
read: true
write: true
drop: false

Loading

0 comments on commit 8855299

Please sign in to comment.