Skip to content

Filter reflexive subset relations eagerly #177

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from
Draft

Filter reflexive subset relations eagerly #177

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
cbdb555
Eagerly filter reflexive subset relations in naive variant
ecstatic-morse Aug 12, 2021
a6dbde6
Eagerly filter reflexive subset relations in opt variant
ecstatic-morse Aug 12, 2021
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
49 changes: 13 additions & 36 deletions polonius-engine/src/output/datafrog_opt.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -173,25 +173,6 @@ pub(super) fn compute<T: FactTypes>(

// .. and then start iterating rules!
while iteration.changed() {
// Cleanup step: remove symmetries
// - remove origins which are `subset`s of themselves
//
// FIXME: investigate whether is there a better way to do that without complicating
// the rules too much, because it would also require temporary variables and
// impact performance. Until then, the big reduction in tuples improves performance
// a lot, even if we're potentially adding a small number of tuples
// per round just to remove them in the next round.
subset_o1p
.recent
.borrow_mut()
.elements
.retain(|&((origin1, _), origin2)| origin1 != origin2);

subset_placeholder
.recent
.borrow_mut()
.elements
.retain(|&(origin1, origin2, _)| origin1 != origin2);
subset_placeholder_o2p.from_map(&subset_placeholder, |&(origin1, origin2, point)| {
((origin2, point), origin1)
});
Expand Down Expand Up @@ -299,11 +280,14 @@ pub(super) fn compute<T: FactTypes>(

// subset(origin1, origin3, point2) :-
// live_to_dying_regions(origin1, origin2, point1, point2),
// dying_can_reach_live(origin2, origin3, point1, point2).
subset_o1p.from_join(
// dying_can_reach_live(origin2, origin3, point1, point2),
// origin1 != origin3.
subset_o1p.from_join_filtered(
&live_to_dying_regions_o2pq,
&dying_can_reach_live,
|&(_origin2, _point1, point2), &origin1, &origin3| ((origin1, point2), origin3),
|&(_origin2, _point1, point2), &origin1, &origin3| {
(origin1 != origin3).then(|| ((origin1, point2), origin3))
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Personally not a big fan of bool::then, but I don't mind if you and the others like it.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I quite like it. If you and/or Niko find it too obtuse, we can change it of course.

},
);

// origin_contains_loan_on_entry(origin2, loan, point2) :-
Expand Down Expand Up @@ -403,13 +387,7 @@ pub(super) fn compute<T: FactTypes>(
// placeholder_origin(Origin1).
subset_placeholder.from_leapjoin(
&subset_o1p,
(
placeholder_origin.extend_with(|&((origin1, _point), _origin2)| origin1),
// remove symmetries:
datafrog::ValueFilter::from(|&((origin1, _point), origin2), _| {
origin1 != origin2
}),
),
placeholder_origin.extend_with(|&((origin1, _point), _origin2)| origin1),
|&((origin1, point), origin2), _| (origin1, origin2, point),
);

Expand All @@ -418,11 +396,14 @@ pub(super) fn compute<T: FactTypes>(
//
// subset_placeholder(Origin1, Origin3, Point) :-
// subset_placeholder(Origin1, Origin2, Point),
// subset(Origin2, Origin3, Point).
subset_placeholder.from_join(
// subset(Origin2, Origin3, Point),
// Origin1 != Origin3.
subset_placeholder.from_join_filtered(
&subset_placeholder_o2p,
&subset_o1p,
|&(_origin2, point), &origin1, &origin3| (origin1, origin3, point),
|&(_origin2, point), &origin1, &origin3| {
(origin1 != origin3).then(|| (origin1, origin3, point))
},
);

// subset_error(Origin1, Origin2, Point) :-
Expand All @@ -435,10 +416,6 @@ pub(super) fn compute<T: FactTypes>(
placeholder_origin.extend_with(|&(_origin1, origin2, _point)| origin2),
known_placeholder_subset
.filter_anti(|&(origin1, origin2, _point)| (origin1, origin2)),
// remove symmetries:
datafrog::ValueFilter::from(|&(origin1, origin2, _point), _| {
origin1 != origin2
}),
),
|&(origin1, origin2, point), _| (origin1, origin2, point),
);
Expand Down
27 changes: 6 additions & 21 deletions polonius-engine/src/output/naive.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -104,20 +104,6 @@ pub(super) fn compute<T: FactTypes>(

// .. and then start iterating rules!
while iteration.changed() {
// Cleanup step: remove symmetries
// - remove origins which are `subset`s of themselves
//
// FIXME: investigate whether is there a better way to do that without complicating
// the rules too much, because it would also require temporary variables and
// impact performance. Until then, the big reduction in tuples improves performance
// a lot, even if we're potentially adding a small number of tuples
// per round just to remove them in the next round.
subset
.recent
.borrow_mut()
.elements
.retain(|&(origin1, origin2, _)| origin1 != origin2);

// Remap fields to re-index by keys, to prepare the data needed by the rules below.
subset_o1p.from_map(&subset, |&(origin1, origin2, point)| {
((origin1, point), origin2)
Expand All @@ -137,11 +123,14 @@ pub(super) fn compute<T: FactTypes>(
//
// subset(Origin1, Origin3, Point) :-
// subset(Origin1, Origin2, Point),
// subset(Origin2, Origin3, Point).
subset.from_join(
// subset(Origin2, Origin3, Point),
// Origin1 != Origin3.
subset.from_join_filtered(
&subset_o2p,
&subset_o1p,
|&(_origin2, point), &origin1, &origin3| (origin1, origin3, point),
|&(_origin2, point), &origin1, &origin3| {
(origin1 != origin3).then(|| (origin1, origin3, point))
},
);

// Rule 3: propagate subsets along the CFG, according to liveness.
Expand Down Expand Up @@ -238,10 +227,6 @@ pub(super) fn compute<T: FactTypes>(
placeholder_origin.extend_with(|&(_origin1, origin2, _point)| origin2),
known_placeholder_subset
.filter_anti(|&(origin1, origin2, _point)| (origin1, origin2)),
// remove symmetries:
datafrog::ValueFilter::from(|&(origin1, origin2, _point), _| {
origin1 != origin2
}),
),
|&(origin1, origin2, point), _| (origin1, origin2, point),
);
Expand Down