From cbdb555010ece7e70f744db214610bcf7d775765 Mon Sep 17 00:00:00 2001 From: Dylan MacKenzie Date: Thu, 12 Aug 2021 13:14:48 -0700 Subject: [PATCH 1/2] Eagerly filter reflexive subset relations in naive variant ...instead of removing them at the start of each iteration. --- polonius-engine/src/output/naive.rs | 27 ++++++--------------------- 1 file changed, 6 insertions(+), 21 deletions(-) diff --git a/polonius-engine/src/output/naive.rs b/polonius-engine/src/output/naive.rs index aa42048673..8539c4c1a7 100644 --- a/polonius-engine/src/output/naive.rs +++ b/polonius-engine/src/output/naive.rs @@ -104,20 +104,6 @@ pub(super) fn compute( // .. 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) @@ -137,11 +123,14 @@ pub(super) fn compute( // // 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. @@ -238,10 +227,6 @@ pub(super) fn compute( 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), ); From a6dbde6b11ab2df44a8aa4652c9247d111a3d0a3 Mon Sep 17 00:00:00 2001 From: Dylan MacKenzie Date: Thu, 12 Aug 2021 13:45:00 -0700 Subject: [PATCH 2/2] Eagerly filter reflexive subset relations in opt variant --- polonius-engine/src/output/datafrog_opt.rs | 49 ++++++---------------- 1 file changed, 13 insertions(+), 36 deletions(-) diff --git a/polonius-engine/src/output/datafrog_opt.rs b/polonius-engine/src/output/datafrog_opt.rs index da9c343ccd..54f80852be 100644 --- a/polonius-engine/src/output/datafrog_opt.rs +++ b/polonius-engine/src/output/datafrog_opt.rs @@ -173,25 +173,6 @@ pub(super) fn compute( // .. 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) }); @@ -299,11 +280,14 @@ pub(super) fn compute( // 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)) + }, ); // origin_contains_loan_on_entry(origin2, loan, point2) :- @@ -403,13 +387,7 @@ pub(super) fn compute( // 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), ); @@ -418,11 +396,14 @@ pub(super) fn compute( // // 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) :- @@ -435,10 +416,6 @@ pub(super) fn compute( 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), );