diff --git a/polonius-engine/src/output/datafrog_opt.rs b/polonius-engine/src/output/datafrog_opt.rs index da9c343ccd..83a38fb69c 100644 --- a/polonius-engine/src/output/datafrog_opt.rs +++ b/polonius-engine/src/output/datafrog_opt.rs @@ -25,24 +25,16 @@ 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; 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"); - - // 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"); @@ -144,16 +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), ())), - ); - 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 +187,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 +203,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 +241,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 +257,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 +273,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 +313,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 +323,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 +343,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 +352,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 +367,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), ()), ); @@ -393,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), ); 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), ()), );