From cb0461b1763b37085c292ae340529adcb8b1d15d Mon Sep 17 00:00:00 2001 From: Dylan MacKenzie Date: Thu, 12 Aug 2021 14:04:09 -0700 Subject: [PATCH 1/3] Remove re-indexed version of `origin_live_on_entry` from naive variant Now we only have the `Relation` version, so we could combine Rules 7 and 8 and leapjoin instead of doing two separate joins. --- polonius-engine/src/output/naive.rs | 39 ++++++----------------------- 1 file changed, 7 insertions(+), 32 deletions(-) diff --git a/polonius-engine/src/output/naive.rs b/polonius-engine/src/output/naive.rs index aa42048673..f9290ea4ef 100644 --- a/polonius-engine/src/output/naive.rs +++ b/polonius-engine/src/output/naive.rs @@ -27,7 +27,7 @@ pub(super) fn compute( let (errors, subset_errors) = { // Static inputs - let origin_live_on_entry_rel = &ctx.origin_live_on_entry; + let origin_live_on_entry = &ctx.origin_live_on_entry; let cfg_edge = &ctx.cfg_edge; let loan_killed_at = &ctx.loan_killed_at; let known_placeholder_subset = &ctx.known_placeholder_subset; @@ -57,33 +57,6 @@ pub(super) fn compute( let origin_contains_loan_on_entry_op = iteration.variable_indistinct("origin_contains_loan_on_entry_op"); - // Unfortunately, we need `origin_live_on_entry` in both variable and relation forms: - // We need: - // - `origin_live_on_entry` as a Relation for the leapjoins in rules 3 & 6 - // - `origin_live_on_entry` as a Variable for the join in rule 7 - // - // The leapjoins use `origin_live_on_entry` as `(Origin, Point)` tuples, while the join uses - // it as a `((O, P), ())` tuple to filter the `((Origin, Point), Loan)` tuples from - // `origin_contains_loan_on_entry_op`. - // - // The regular join in rule 7 could be turned into a `filter_with` leaper but that would - // result in a leapjoin with no `extend_*` leapers: a leapjoin that is not well-formed. - // Doing the filtering via an `extend_with` leaper would be extremely inefficient. - // - // Until there's an API in datafrog to handle this use-case better, we do a slightly less - // inefficient thing of copying the whole static input into a Variable to use a regular - // join, even though the liveness information can be quite heavy (around 1M tuples - // on `clap`). - // This is the Naive variant so this is not a big problem, but needs an - // explanation. - let origin_live_on_entry_var = - iteration.variable::<((T::Origin, T::Point), ())>("origin_live_on_entry"); - origin_live_on_entry_var.extend( - origin_live_on_entry_rel - .iter() - .map(|&(origin, point)| ((origin, point), ())), - ); - // output relations: illegal accesses errors, and illegal subset relations errors let errors = iteration.variable("errors"); let subset_errors = iteration.variable::<(T::Origin, T::Origin, T::Point)>("subset_errors"); @@ -155,8 +128,8 @@ pub(super) fn compute( &subset, ( cfg_edge.extend_with(|&(_origin1, _origin2, point1)| point1), - origin_live_on_entry_rel.extend_with(|&(origin1, _origin2, _point1)| origin1), - origin_live_on_entry_rel.extend_with(|&(_origin1, origin2, _point1)| origin2), + origin_live_on_entry.extend_with(|&(origin1, _origin2, _point1)| origin1), + origin_live_on_entry.extend_with(|&(_origin1, origin2, _point1)| origin2), ), |&(origin1, origin2, _point1), &point2| (origin1, origin2, point2), ); @@ -186,7 +159,7 @@ pub(super) fn compute( ( loan_killed_at.filter_anti(|&(_origin, loan, point1)| (loan, point1)), cfg_edge.extend_with(|&(_origin, _loan, point1)| point1), - origin_live_on_entry_rel.extend_with(|&(origin, _loan, _point1)| origin), + origin_live_on_entry.extend_with(|&(origin, _loan, _point1)| origin), ), |&(origin, loan, _point1), &point2| (origin, loan, point2), ); @@ -197,9 +170,11 @@ pub(super) fn compute( // loan_live_at(Loan, Point) :- // origin_contains_loan_on_entry(Origin, Loan, Point), // origin_live_on_entry(Origin, Point). + // + // FIXME: Should be merged with Rule 8 so we can leapjoin. loan_live_at.from_join( &origin_contains_loan_on_entry_op, - &origin_live_on_entry_var, + origin_live_on_entry, |&(_origin, point), &loan, _| ((loan, point), ()), ); From 440d0e8d1ec94d1ca137d2f3bc2c31937f248c46 Mon Sep 17 00:00:00 2001 From: Dylan MacKenzie Date: Thu, 12 Aug 2021 14:07:49 -0700 Subject: [PATCH 2/3] Remove `origin_live_on_entry_var` re-index from opt variant --- polonius-engine/src/output/datafrog_opt.rs | 36 ++++++++-------------- 1 file changed, 13 insertions(+), 23 deletions(-) diff --git a/polonius-engine/src/output/datafrog_opt.rs b/polonius-engine/src/output/datafrog_opt.rs index da9c343ccd..028cb031a3 100644 --- a/polonius-engine/src/output/datafrog_opt.rs +++ b/polonius-engine/src/output/datafrog_opt.rs @@ -25,7 +25,7 @@ pub(super) fn compute( let (errors, subset_errors) = { // Static inputs - let origin_live_on_entry_rel = &ctx.origin_live_on_entry; + let origin_live_on_entry = &ctx.origin_live_on_entry; let cfg_edge_rel = &ctx.cfg_edge; let loan_killed_at = &ctx.loan_killed_at; let known_placeholder_subset = &ctx.known_placeholder_subset; @@ -38,11 +38,6 @@ pub(super) fn compute( let loan_invalidated_at = iteration.variable::<((T::Loan, T::Point), ())>("loan_invalidated_at"); - // we need `origin_live_on_entry` in both variable and relation forms, - // (respectively, for join and antijoin). - let origin_live_on_entry_var = - iteration.variable::<((T::Origin, T::Point), ())>("origin_live_on_entry"); - // `loan_issued_at` input but organized for join let loan_issued_at_op = iteration.variable::<((T::Origin, T::Point), T::Loan)>("loan_issued_at_op"); @@ -149,11 +144,6 @@ pub(super) fn compute( .iter() .map(|&(loan, point)| ((loan, point), ())), ); - origin_live_on_entry_var.extend( - origin_live_on_entry_rel - .iter() - .map(|&(origin, point)| ((origin, point), ())), - ); // subset(origin1, origin2, point) :- // subset_base(origin1, origin2, point). @@ -205,8 +195,8 @@ pub(super) fn compute( &subset_o1p, ( cfg_edge_rel.extend_with(|&((_, point1), _)| point1), - origin_live_on_entry_rel.extend_with(|&((origin1, _), _)| origin1), - origin_live_on_entry_rel.extend_anti(|&((_, _), origin2)| origin2), + origin_live_on_entry.extend_with(|&((origin1, _), _)| origin1), + origin_live_on_entry.extend_anti(|&((_, _), origin2)| origin2), ), |&((origin1, point1), origin2), &point2| ((origin2, point1, point2), origin1), ); @@ -221,7 +211,7 @@ pub(super) fn compute( ( loan_killed_at.filter_anti(|&((_, point1), loan)| (loan, point1)), cfg_edge_rel.extend_with(|&((_, point1), _)| point1), - origin_live_on_entry_rel.extend_anti(|&((origin, _), _)| origin), + origin_live_on_entry.extend_anti(|&((origin, _), _)| origin), ), |&((origin, point1), loan), &point2| ((origin, point1, point2), loan), ); @@ -259,7 +249,7 @@ pub(super) fn compute( // "intermediate" `origin2` is dead at `point2`. dying_can_reach_1.from_antijoin( &dying_can_reach_o2q, - &origin_live_on_entry_rel, + &origin_live_on_entry, |&(origin2, point2), &(origin1, point1)| ((origin2, point1), (origin1, point2)), ); dying_can_reach_o2q.from_join( @@ -275,7 +265,7 @@ pub(super) fn compute( // origin_live_on_entry(origin2, point2). dying_can_reach_live.from_join( &dying_can_reach_o2q, - &origin_live_on_entry_var, + origin_live_on_entry, |&(origin2, point2), &(origin1, point1), _| ((origin1, point1, point2), origin2), ); @@ -291,8 +281,8 @@ pub(super) fn compute( &subset_o1p, ( cfg_edge_rel.extend_with(|&((_, point1), _)| point1), - origin_live_on_entry_rel.extend_with(|&((origin1, _), _)| origin1), - origin_live_on_entry_rel.extend_with(|&((_, _), origin2)| origin2), + origin_live_on_entry.extend_with(|&((origin1, _), _)| origin1), + origin_live_on_entry.extend_with(|&((_, _), origin2)| origin2), ), |&((origin1, _point1), origin2), &point2| ((origin1, point2), origin2), ); @@ -331,7 +321,7 @@ pub(super) fn compute( ( loan_killed_at.filter_anti(|&((_, point1), loan)| (loan, point1)), cfg_edge_rel.extend_with(|&((_, point1), _)| point1), - origin_live_on_entry_rel.extend_with(|&((origin, _), _)| origin), + origin_live_on_entry.extend_with(|&((origin, _), _)| origin), ), |&((origin, _), loan), &point2| ((origin, point2), loan), ); @@ -341,7 +331,7 @@ pub(super) fn compute( // !origin_live_on_entry(origin, point). dead_borrow_region_can_reach_root.from_antijoin( &loan_issued_at_op, - &origin_live_on_entry_rel, + &origin_live_on_entry, |&(origin, point), &loan| ((origin, point), loan), ); @@ -361,7 +351,7 @@ pub(super) fn compute( ); dead_borrow_region_can_reach_dead.from_antijoin( &dead_borrow_region_can_reach_dead_1, - &origin_live_on_entry_rel, + &origin_live_on_entry, |&(origin2, point), &loan| ((origin2, point), loan), ); @@ -370,7 +360,7 @@ pub(super) fn compute( // origin_live_on_entry(origin, point). loan_live_at.from_join( &origin_contains_loan_on_entry_op, - &origin_live_on_entry_var, + origin_live_on_entry, |&(_origin, point), &loan, _| ((loan, point), ()), ); @@ -385,7 +375,7 @@ pub(super) fn compute( // joined together. loan_live_at.from_join( &dead_borrow_region_can_reach_dead_1, - &origin_live_on_entry_var, + origin_live_on_entry, |&(_origin2, point), &loan, _| ((loan, point), ()), ); From ddad94cef1e07d1bdb714fa9787785195ab4af66 Mon Sep 17 00:00:00 2001 From: Dylan MacKenzie Date: Thu, 12 Aug 2021 14:07:49 -0700 Subject: [PATCH 3/3] Remove `loan_invalidated_at` re-index from opt variant --- polonius-engine/src/output/datafrog_opt.rs | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/polonius-engine/src/output/datafrog_opt.rs b/polonius-engine/src/output/datafrog_opt.rs index 028cb031a3..83a38fb69c 100644 --- a/polonius-engine/src/output/datafrog_opt.rs +++ b/polonius-engine/src/output/datafrog_opt.rs @@ -30,14 +30,11 @@ pub(super) fn compute( let loan_killed_at = &ctx.loan_killed_at; let known_placeholder_subset = &ctx.known_placeholder_subset; let placeholder_origin = &ctx.placeholder_origin; + let loan_invalidated_at = &ctx.loan_invalidated_at; // Create a new iteration context, ... let mut iteration = Iteration::new(); - // `loan_invalidated_at` facts, stored ready for joins - let loan_invalidated_at = - iteration.variable::<((T::Loan, T::Point), ())>("loan_invalidated_at"); - // `loan_issued_at` input but organized for join let loan_issued_at_op = iteration.variable::<((T::Origin, T::Point), T::Loan)>("loan_issued_at_op"); @@ -139,11 +136,6 @@ pub(super) fn compute( .iter() .map(|&(origin, loan, point)| ((origin, point), loan)), ); - loan_invalidated_at.extend( - ctx.loan_invalidated_at - .iter() - .map(|&(loan, point)| ((loan, point), ())), - ); // subset(origin1, origin2, point) :- // subset_base(origin1, origin2, point). @@ -383,8 +375,8 @@ pub(super) fn compute( // loan_invalidated_at(loan, point), // loan_live_at(loan, point). errors.from_join( - &loan_invalidated_at, &loan_live_at, + loan_invalidated_at, |&(loan, point), _, _| (loan, point), );