diff --git a/polonius-engine/src/output/datafrog_opt.rs b/polonius-engine/src/output/datafrog_opt.rs index da9c343ccd..37ac43edd7 100644 --- a/polonius-engine/src/output/datafrog_opt.rs +++ b/polonius-engine/src/output/datafrog_opt.rs @@ -155,6 +155,8 @@ pub(super) fn compute( .map(|&(origin, point)| ((origin, point), ())), ); + // Rule 1: the initial subsets are the non-transitive `subset_base` static input. + // // subset(origin1, origin2, point) :- // subset_base(origin1, origin2, point). subset_o1p.extend( @@ -163,6 +165,8 @@ pub(super) fn compute( .map(|&(origin1, origin2, point)| ((origin1, point), origin2)), ); + // Rule 2: the issuing origins are the ones initially containing loans. + // // origin_contains_loan_on_entry(origin, loan, point) :- // loan_issued_at(origin, loan, point). origin_contains_loan_on_entry_op.extend( @@ -192,25 +196,47 @@ pub(super) fn compute( .borrow_mut() .elements .retain(|&(origin1, origin2, _)| origin1 != origin2); + subset_placeholder_o2p.from_map(&subset_placeholder, |&(origin1, origin2, point)| { ((origin2, point), origin1) }); + // Rule 3 + // // live_to_dying_regions(origin1, origin2, point1, point2) :- // subset(origin1, origin2, point1), // cfg_edge(point1, point2), - // origin_live_on_entry(origin1, point2), + // (origin_live_on_entry(origin1, point2); placeholder_origin(origin1)), // -> A // !origin_live_on_entry(origin2, point2). + // + // Since there is one alternative predicate, A, this will result in two expansions + // of this rule: one for each alternative for predicate A. + // + // 1) Rule 3, expansion 1 of 2 + // - predicate A: `origin_live_on_entry(origin1, point2)` live_to_dying_regions_o2pq.from_leapjoin( &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(|&((origin1, _), _)| origin1), // -> A + origin_live_on_entry_rel.extend_anti(|&((_, _), origin2)| origin2), + ), + |&((origin1, point1), origin2), &point2| ((origin2, point1, point2), origin1), + ); + // 2) Rule 3, expansion 2 of 2 + // - predicate A: `placeholder_origin(origin1)` + live_to_dying_regions_o2pq.from_leapjoin( + &subset_o1p, + ( + cfg_edge_rel.extend_with(|&((_, point1), _)| point1), + placeholder_origin.filter_with(|&((origin1, _), _)| (origin1, ())), // -> A origin_live_on_entry_rel.extend_anti(|&((_, _), origin2)| origin2), ), |&((origin1, point1), origin2), &point2| ((origin2, point1, point2), origin1), ); + // Rule 4 + // // dying_region_requires((origin, point1, point2), loan) :- // origin_contains_loan_on_entry(origin, loan, point1), // !loan_killed_at(loan, point1), @@ -226,6 +252,8 @@ pub(super) fn compute( |&((origin, point1), loan), &point2| ((origin, point1, point2), loan), ); + // Rule 5 + // // dying_can_reach_origins(origin2, point1, point2) :- // live_to_dying_regions(_, origin2, point1, point2). dying_can_reach_origins.from_map( @@ -233,6 +261,8 @@ pub(super) fn compute( |&((origin2, point1, point2), _origin1)| ((origin2, point1), point2), ); + // Rule 6 + // // dying_can_reach_origins(origin, point1, point2) :- // dying_region_requires(origin, point1, point2, _loan). dying_can_reach_origins.from_map( @@ -240,6 +270,8 @@ pub(super) fn compute( |&((origin, point1, point2), _loan)| ((origin, point1), point2), ); + // Rule 7 + // // dying_can_reach(origin1, origin2, point1, point2) :- // dying_can_reach_origins(origin1, point1, point2), // subset(origin1, origin2, point1). @@ -249,6 +281,8 @@ pub(super) fn compute( |&(origin1, point1), &point2, &origin2| ((origin2, point2), (origin1, point1)), ); + // Rule 8 + // // dying_can_reach(origin1, origin3, point1, point2) :- // dying_can_reach(origin1, origin2, point1, point2), // !origin_live_on_entry(origin2, point2), @@ -270,33 +304,96 @@ pub(super) fn compute( }, ); + // Rule 9 + // // dying_can_reach_live(origin1, origin2, point1, point2) :- // dying_can_reach(origin1, origin2, point1, point2), - // origin_live_on_entry(origin2, point2). + // (origin_live_on_entry(origin2, point2); placeholder_origin(origin2)). // -> A + // + // Since there is one alternative predicate, A, this will result in two expansions + // of this rule: one for each alternative for predicate A. + // + // 1) Rule 9, expansion 1 of 2 + // - predicate A: `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_var, // -> A |&(origin2, point2), &(origin1, point1), _| ((origin1, point1, point2), origin2), ); + // 2) Rule 9, expansion 2 of 2 + // - predicate A: `placeholder_origin(origin2)` + dying_can_reach_live.from_leapjoin( + &dying_can_reach_o2q, + placeholder_origin.extend_with(|&((origin2, _), (_, _))| origin2), // -> A + |&((origin2, point2), (origin1, point1)), _| ((origin1, point1, point2), origin2), + ); + // Rule 10 + // // subset(origin1, origin2, point2) :- // subset(origin1, origin2, point1), // cfg_edge(point1, point2), - // origin_live_on_entry(origin1, point2), - // origin_live_on_entry(origin2, point2). + // (origin_live_on_entry(origin1, point2); placeholder_origin(origin1)), // -> A + // (origin_live_on_entry(origin2, point2); placeholder_origin(origin2)). // -> B + // + // Since there are two alternative predicates, A and B, this will result in four + // expansions of this rule: two alternatives for predicate A, and two alternatives for + // predicate B. // // Carry `origin1 <= origin2` from `point1` into `point2` if both `origin1` and // `origin2` are live in `point2`. + // + // 1) Rule 10, expansion 1 of 4 + // - predicate A: `origin_live_on_entry(origin1, point2)` + // - predicate B: `origin_live_on_entry(origin2, point2)` + subset_o1p.from_leapjoin( + &subset_o1p, + ( + cfg_edge_rel.extend_with(|&((_, point1), _)| point1), + origin_live_on_entry_rel.extend_with(|&((origin1, _), _)| origin1), // -> A + origin_live_on_entry_rel.extend_with(|&((_, _), origin2)| origin2), // -> B + ), + |&((origin1, _point1), origin2), &point2| ((origin1, point2), origin2), + ); + // 2) Rule 10, expansion 2 of 4 + // - predicate A: `origin_live_on_entry(origin1, point2)` + // - predicate B: `placeholder_origin(origin2)` + subset_o1p.from_leapjoin( + &subset_o1p, + ( + cfg_edge_rel.extend_with(|&((_, point1), _)| point1), + origin_live_on_entry_rel.extend_with(|&((origin1, _), _)| origin1), // -> A + placeholder_origin.filter_with(|&((_, _), origin2)| (origin2, ())), // -> B + ), + |&((origin1, _point1), origin2), &point2| ((origin1, point2), origin2), + ); + // 3) Rule 10, expansion 3 of 4 + // - predicate A: `placeholder_origin(origin1)` + // - predicate B: `origin_live_on_entry(origin2, point2)` subset_o1p.from_leapjoin( &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), + placeholder_origin.filter_with(|&((origin1, _), _)| (origin1, ())), // -> A + origin_live_on_entry_rel.extend_with(|&((_, _), origin2)| origin2), // -> B + ), + |&((origin1, _point1), origin2), &point2| ((origin1, point2), origin2), + ); + // 4) Rule 10, expansion 4 of 4 + // - predicate A: `placeholder_origin(origin1)` + // - predicate B: `placeholder_origin(origin2)` + subset_o1p.from_leapjoin( + &subset_o1p, + ( + cfg_edge_rel.extend_with(|&((_, point1), _)| point1), + placeholder_origin.filter_with(|&((origin1, _), _)| (origin1, ())), // -> A + placeholder_origin.filter_with(|&((_, _), origin2)| (origin2, ())), // -> B ), |&((origin1, _point1), origin2), &point2| ((origin1, point2), origin2), ); + // Rule 11 + // // subset(origin1, origin3, point2) :- // live_to_dying_regions(origin1, origin2, point1, point2), // dying_can_reach_live(origin2, origin3, point1, point2). @@ -306,6 +403,8 @@ pub(super) fn compute( |&(_origin2, _point1, point2), &origin1, &origin3| ((origin1, point2), origin3), ); + // Rule 12 + // // origin_contains_loan_on_entry(origin2, loan, point2) :- // dying_region_requires(origin1, loan, point1, point2), // dying_can_reach_live(origin1, origin2, point1, point2). @@ -321,35 +420,70 @@ pub(super) fn compute( |&(_origin1, _point1, point2), &loan, &origin2| ((origin2, point2), loan), ); + // Rule 13 + // // origin_contains_loan_on_entry(origin, loan, point2) :- // origin_contains_loan_on_entry(origin, loan, point1), // !loan_killed_at(loan, point1), // cfg_edge(point1, point2), - // origin_live_on_entry(origin, point2). + // (origin_live_on_entry(origin, point2); placeholder_origin(origin)). // -> A + // + // Since there is one alternative predicate, A, this will result in two expansions + // of this rule: one for each alternative for predicate A. + // + // 1) Rule 13, expansion 1 of 2 + // - predicate A: `origin_live_on_entry(origin, point2)` + origin_contains_loan_on_entry_op.from_leapjoin( + &origin_contains_loan_on_entry_op, + ( + 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), // -> A + ), + |&((origin, _), loan), &point2| ((origin, point2), loan), + ); + // 2) Rule 13, expansion 2 of 2 + // - predicate A: `placeholder_origin(origin)` origin_contains_loan_on_entry_op.from_leapjoin( &origin_contains_loan_on_entry_op, ( 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), + placeholder_origin.filter_with(|&((origin, _), _)| (origin, ())), // -> A ), |&((origin, _), loan), &point2| ((origin, point2), loan), ); + // Rule 14 + // // dead_borrow_region_can_reach_root((origin, point), loan) :- // loan_issued_at(origin, loan, point), // !origin_live_on_entry(origin, point). + // + // Even though `loan_issued_at_op` is a Variable here for the antijoin API (and + // nowadays datafrog's Relations can be built with `Relation::from_antijoin`), this is + // a join over two static inputs. It should not produce facts each round, and could be + // moved out of the loop (and most likely should be inlined into rule 15). + // dead_borrow_region_can_reach_root.from_antijoin( &loan_issued_at_op, &origin_live_on_entry_rel, |&(origin, point), &loan| ((origin, point), loan), ); + // Rule 15 + // // dead_borrow_region_can_reach_dead((origin, point), loan) :- // dead_borrow_region_can_reach_root((origin, point), loan). + // + // Note: this is effectively mapping over a static input, and + // `dead_borrow_region_can_reach_root` could probably be inlined in this relation. + // dead_borrow_region_can_reach_dead .from_map(&dead_borrow_region_can_reach_root, |&tuple| tuple); + // Rule 16 + // // dead_borrow_region_can_reach_dead((origin2, point), loan) :- // dead_borrow_region_can_reach_dead(origin1, loan, point), // subset(origin1, origin2, point), @@ -365,30 +499,62 @@ pub(super) fn compute( |&(origin2, point), &loan| ((origin2, point), loan), ); + // Rule 17 + // // loan_live_at(loan, point) :- // origin_contains_loan_on_entry(origin, loan, point), - // origin_live_on_entry(origin, point). + // (origin_live_on_entry(origin, point); placeholder_origin(origin)). // -> A + // + // Since there is one alternative predicate, A, this will result in two expansions + // of this rule: one for each alternative for predicate A. + // + // 1) Rule 17, expansion 1 of 2 + // - predicate A: `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_var, // -> A |&(_origin, point), &loan, _| ((loan, point), ()), ); + // 2) Rule 17, expansion 2 of 2 + // - predicate A: `placeholder_origin(origin)` + loan_live_at.from_leapjoin( + &origin_contains_loan_on_entry_op, + placeholder_origin.extend_with(|&((origin, _point), _loan)| origin), // -> A + |&((_origin, point), loan), _| ((loan, point), ()), + ); + // Rule 18 + // // loan_live_at(loan, point) :- // dead_borrow_region_can_reach_dead(origin1, loan, point), // subset(origin1, origin2, point), - // origin_live_on_entry(origin2, point). + // (origin_live_on_entry(origin2, point); placeholder_origin(origin2)). // -> A + // + // Since there is one alternative predicate, A, this will result in two expansions + // of this rule: one for each alternative for predicate A. // // NB: the datafrog code below uses // `dead_borrow_region_can_reach_dead_1`, which is equal // to `dead_borrow_region_can_reach_dead` and `subset` // joined together. + // + // 1) Rule 18, expansion 1 of 2 + // - predicate A: `origin_live_on_entry(origin2, point)` loan_live_at.from_join( &dead_borrow_region_can_reach_dead_1, - &origin_live_on_entry_var, + &origin_live_on_entry_var, // -> A |&(_origin2, point), &loan, _| ((loan, point), ()), ); + // 2) Rule 18, expansion 2 of 2 + // - predicate A: `placeholder_origin(origin2)` + loan_live_at.from_leapjoin( + &dead_borrow_region_can_reach_dead_1, + placeholder_origin.extend_with(|&((origin2, _point), _loan)| origin2), // -> A + |&((_origin2, point), loan), _| ((loan, point), ()), + ); + // Rule 19: compute illegal access errors, i.e. an invalidation of a live loan. + // // errors(loan, point) :- // loan_invalidated_at(loan, point), // loan_live_at(loan, point). @@ -398,6 +564,8 @@ pub(super) fn compute( |&(loan, point), _, _| (loan, point), ); + // Rule 20: compute the subsets of the placeholder origins, at a given point. + // // subset_placeholder(Origin1, Origin2, Point) :- // subset(Origin1, Origin2, Point), // placeholder_origin(Origin1). @@ -413,8 +581,8 @@ pub(super) fn compute( |&((origin1, point), origin2), _| (origin1, origin2, point), ); - // We compute the transitive closure of the placeholder origins, so we - // maintain the invariant from the rule above that `Origin1` is a placeholder origin. + // Rule 21: compute the subset transitive closure of placeholder origins. + // We maintain the invariant from rule 20 that `Origin1` is a placeholder origin. // // subset_placeholder(Origin1, Origin3, Point) :- // subset_placeholder(Origin1, Origin2, Point), @@ -425,7 +593,10 @@ pub(super) fn compute( |&(_origin2, point), &origin1, &origin3| (origin1, origin3, point), ); - // subset_error(Origin1, Origin2, Point) :- + // Rule 22: compute illegal subset relations errors, i.e. the undeclared subsets + // between two placeholder origins. + // + // subset_errors(Origin1, Origin2, Point) :- // subset_placeholder(Origin1, Origin2, Point), // placeholder_origin(Origin2), // !known_placeholder_subset(Origin1, Origin2). diff --git a/polonius-engine/src/output/liveness.rs b/polonius-engine/src/output/liveness.rs index 1b4b4ce53f..46ca456033 100644 --- a/polonius-engine/src/output/liveness.rs +++ b/polonius-engine/src/output/liveness.rs @@ -10,7 +10,6 @@ //! An implementation of the origin liveness calculation logic -use std::collections::BTreeSet; use std::time::Instant; use crate::facts::FactTypes; @@ -23,7 +22,7 @@ pub(super) fn compute_live_origins( cfg_edge: &Relation<(T::Point, T::Point)>, var_maybe_partly_initialized_on_exit: Relation<(T::Variable, T::Point)>, output: &mut Output, -) -> Vec<(T::Origin, T::Point)> { +) -> Relation<(T::Origin, T::Point)> { let timer = Instant::now(); let mut iteration = Iteration::new(); @@ -151,20 +150,5 @@ pub(super) fn compute_live_origins( } } - origin_live_on_entry.elements -} - -pub(super) fn make_universal_regions_live( - origin_live_on_entry: &mut Vec<(T::Origin, T::Point)>, - cfg_node: &BTreeSet, - universal_regions: &[T::Origin], -) { - debug!("make_universal_regions_live()"); - - origin_live_on_entry.reserve(universal_regions.len() * cfg_node.len()); - for &origin in universal_regions.iter() { - for &point in cfg_node.iter() { - origin_live_on_entry.push((origin, point)); - } - } + origin_live_on_entry } diff --git a/polonius-engine/src/output/location_insensitive.rs b/polonius-engine/src/output/location_insensitive.rs index 83ce27757d..2e4912e53d 100644 --- a/polonius-engine/src/output/location_insensitive.rs +++ b/polonius-engine/src/output/location_insensitive.rs @@ -31,6 +31,8 @@ pub(super) fn compute( let placeholder_loan = &ctx.placeholder_loan; let known_contains = &ctx.known_contains; + // Rule 1: the subsets are the non-transitive `subset_base` static input. + // // subset(Origin1, Origin2) :- // subset_base(Origin1, Origin2, _). let subset = Relation::from_iter( @@ -52,6 +54,8 @@ pub(super) fn compute( // load initial facts. + // Rule 2: the issuing origins are the ones initially containing loans. + // // origin_contains_loan_on_entry(Origin, Loan) :- // loan_issued_at(Origin, Loan, _). origin_contains_loan_on_entry.extend( @@ -60,6 +64,8 @@ pub(super) fn compute( .map(|&(origin, loan, _point)| (origin, loan)), ); + // Rule 3: the placeholder origins also contain their placeholder loan. + // // origin_contains_loan_on_entry(Origin, Loan) :- // placeholder_loan(Origin, Loan). origin_contains_loan_on_entry.extend( @@ -70,6 +76,8 @@ pub(super) fn compute( // .. and then start iterating rules! while iteration.changed() { + // Rule 4: propagate the loans from the origins to their subsets. + // // origin_contains_loan_on_entry(Origin2, Loan) :- // origin_contains_loan_on_entry(Origin1, Loan), // subset(Origin1, Origin2). @@ -82,9 +90,15 @@ pub(super) fn compute( |&_origin1, &loan, &origin2| (origin2, loan), ); + // Rule 5: compute potential errors, i.e. loans that are contained in an origin at any point in the CFG, and + // which are invalidated at a point where that origin is live. + // // loan_live_at(Loan, Point) :- // origin_contains_loan_on_entry(Origin, Loan), - // origin_live_on_entry(Origin, Point) + // (origin_live_on_entry(Origin, Point); placeholder_origin(Origin)). // -> A + // + // Since there is one alternative predicate, A, this will result in two expansions + // of this rule: one for each alternative for predicate A. // // potential_errors(Loan, Point) :- // loan_invalidated_at(Loan, Point), @@ -93,15 +107,30 @@ pub(super) fn compute( // Note: we don't need to materialize `loan_live_at` here // so we can inline it in the `potential_errors` relation. // + // 1) Rule 5, expansion 1 of 2 + // - predicate A: `origin_live_on_entry(Origin, Point)` potential_errors.from_leapjoin( &origin_contains_loan_on_entry, ( - origin_live_on_entry.extend_with(|&(origin, _loan)| origin), + origin_live_on_entry.extend_with(|&(origin, _loan)| origin), // -> A + loan_invalidated_at.extend_with(|&(_origin, loan)| loan), + ), + |&(_origin, loan), &point| (loan, point), + ); + // 2) Rule 5, expansion 2 of 2 + // - predicate A: `placeholder_origin(Origin)` + potential_errors.from_leapjoin( + &origin_contains_loan_on_entry, + ( + placeholder_origin.filter_with(|&(origin, _loan)| (origin, ())), // -> A loan_invalidated_at.extend_with(|&(_origin, loan)| loan), ), |&(_origin, loan), &point| (loan, point), ); + // Rule 6: compute potential subset errors, i.e. the placeholder loans which ultimately + // flowed into another placeholder origin unexpectedly. + // // potential_subset_errors(Origin1, Origin2) :- // placeholder(Origin1, Loan1), // placeholder(Origin2, _), diff --git a/polonius-engine/src/output/mod.rs b/polonius-engine/src/output/mod.rs index 21b173fc39..3e7b8ad460 100644 --- a/polonius-engine/src/output/mod.rs +++ b/polonius-engine/src/output/mod.rs @@ -191,25 +191,13 @@ impl Output { drop_of_var_derefs_origin: all_facts.drop_of_var_derefs_origin.clone(), }; - let mut origin_live_on_entry = liveness::compute_live_origins( + let origin_live_on_entry = liveness::compute_live_origins( liveness_ctx, &cfg_edge, var_maybe_partly_initialized_on_exit, &mut result, ); - let cfg_node = cfg_edge - .iter() - .map(|&(point1, _)| point1) - .chain(cfg_edge.iter().map(|&(_, point2)| point2)) - .collect(); - - liveness::make_universal_regions_live::( - &mut origin_live_on_entry, - &cfg_node, - &all_facts.universal_region, - ); - // 3) Borrow checking // Prepare data as datafrog relations, ready to join. @@ -222,8 +210,6 @@ impl Output { // analysis. If these facts happened to be recorded in separate MIR walks, we might also // avoid generating those facts. - let origin_live_on_entry = origin_live_on_entry.into(); - // TODO: also flip the order of this relation's arguments in rustc // from `loan_invalidated_at(point, loan)` to `loan_invalidated_at(loan, point)`. // to avoid this allocation. diff --git a/polonius-engine/src/output/naive.rs b/polonius-engine/src/output/naive.rs index aa42048673..4ff57ac797 100644 --- a/polonius-engine/src/output/naive.rs +++ b/polonius-engine/src/output/naive.rs @@ -146,17 +146,61 @@ pub(super) fn compute( // Rule 3: propagate subsets along the CFG, according to liveness. // + // Since there are two alternative predicates, A and B, this will result in four + // expansions of this rule: two alternatives for predicate A, and two alternatives for + // predicate B. + // // subset(Origin1, Origin2, Point2) :- // subset(Origin1, Origin2, Point1), // cfg_edge(Point1, Point2), - // origin_live_on_entry(Origin1, Point2), - // origin_live_on_entry(Origin2, Point2). + // (origin_live_on_entry(Origin1, Point2); placeholder_origin(Origin1)), // -> A + // (origin_live_on_entry(Origin2, Point2); placeholder_origin(Origin2)). // -> B + // + // 1) Rule 3, expansion 1 of 4 + // - predicate A: `origin_live_on_entry(Origin1, Point2)` + // - predicate B: `origin_live_on_entry(Origin2, Point2)` + subset.from_leapjoin( + &subset, + ( + cfg_edge.extend_with(|&(_origin1, _origin2, point1)| point1), + origin_live_on_entry_rel.extend_with(|&(origin1, _origin2, _point1)| origin1), // -> A + origin_live_on_entry_rel.extend_with(|&(_origin1, origin2, _point1)| origin2), // -> B + ), + |&(origin1, origin2, _point1), &point2| (origin1, origin2, point2), + ); + // 2) Rule 3, expansion 2 of 4 + // - predicate A: `origin_live_on_entry(Origin1, Point2)` + // - predicate B: `placeholder_origin(Origin2)` subset.from_leapjoin( &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_rel.extend_with(|&(origin1, _origin2, _point1)| origin1), // -> A + placeholder_origin.filter_with(|&(_origin1, origin2, _point1)| (origin2, ())), // -> B + ), + |&(origin1, origin2, _point1), &point2| (origin1, origin2, point2), + ); + // 3) Rule 3, expansion 3 of 4 + // - predicate A: `placeholder_origin(Origin1)` + // - predicate B: `origin_live_on_entry(Origin2, Point2)` + subset.from_leapjoin( + &subset, + ( + cfg_edge.extend_with(|&(_origin1, _origin2, point1)| point1), + placeholder_origin.filter_with(|&(origin1, _origin2, _point1)| (origin1, ())), // -> A + origin_live_on_entry_rel.extend_with(|&(_origin1, origin2, _point1)| origin2), // -> B + ), + |&(origin1, origin2, _point1), &point2| (origin1, origin2, point2), + ); + // 4) Rule 3, expansion 4 of 4 + // - predicate A: `placeholder_origin(Origin1)` + // - predicate B: `placeholder_origin(Origin2)` + subset.from_leapjoin( + &subset, + ( + cfg_edge.extend_with(|&(_origin1, _origin2, point1)| point1), + placeholder_origin.filter_with(|&(origin1, _origin2, _point1)| (origin1, ())), // -> A + placeholder_origin.filter_with(|&(_origin1, origin2, _point1)| (origin2, ())), // -> B ), |&(origin1, origin2, _point1), &point2| (origin1, origin2, point2), ); @@ -176,17 +220,34 @@ pub(super) fn compute( // Rule 6: propagate loans along the CFG, according to liveness. // + // Since there is one alternative predicate, A, this will result in two expansions + // of this rule: one for each alternative for predicate A. + // // origin_contains_loan_on_entry(Origin, Loan, Point2) :- // origin_contains_loan_on_entry(Origin, Loan, Point1), // !loan_killed_at(Loan, Point1), // cfg_edge(Point1, Point2), - // origin_live_on_entry(Origin, Point2). + // (origin_live_on_entry(Origin, Point2); placeholder_origin(Origin)). // -> A + // + // 1) Rule 6, expansion 1 of 2 + // - predicate A: `origin_live_on_entry(Origin, Point2)` + origin_contains_loan_on_entry.from_leapjoin( + &origin_contains_loan_on_entry, + ( + 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), // -> A + ), + |&(origin, loan, _point1), &point2| (origin, loan, point2), + ); + // 2) Rule 6, expansion 2 of 2 + // - predicate A: `placeholder_origin(Origin)` origin_contains_loan_on_entry.from_leapjoin( &origin_contains_loan_on_entry, ( 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), + placeholder_origin.filter_with(|&(origin, _loan, _point1)| (origin, ())), // -> A ), |&(origin, loan, _point1), &point2| (origin, loan, point2), ); @@ -194,14 +255,27 @@ pub(super) fn compute( // Rule 7: compute whether a loan is live at a given point, i.e. whether it is // contained in a live origin at this point. // + // Since there is one alternative predicate, A, this will result in two expansions + // of this rule: one for each alternative for predicate A. + // // loan_live_at(Loan, Point) :- // origin_contains_loan_on_entry(Origin, Loan, Point), - // origin_live_on_entry(Origin, Point). + // (origin_live_on_entry(Origin, Point); placeholder_origin(Origin)). // -> A + // + // 1) Rule 7, expansion 1 of 2 + // - predicate A: `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_var, // -> A |&(_origin, point), &loan, _| ((loan, point), ()), ); + // 2) Rule 7, expansion 2 of 2 + // - predicate A: `placeholder_origin(Origin)` + loan_live_at.from_leapjoin( + &origin_contains_loan_on_entry_op, + placeholder_origin.extend_with(|&((origin, _point), _loan)| origin), // -> A + |&((_origin, point), loan), _| ((loan, point), ()), + ); // Rule 8: compute illegal access errors, i.e. an invalidation of a live loan. // @@ -226,7 +300,7 @@ pub(super) fn compute( // Here as well, WF-ness prevents this join from being a filter-only leapjoin. It // doesn't matter much, as `placeholder_origin` is single-value relation. // - // subset_error(Origin1, Origin2, Point) :- + // subset_errors(Origin1, Origin2, Point) :- // subset(Origin1, Origin2, Point), // placeholder_origin(Origin1), // placeholder_origin(Origin2), diff --git a/src/test.rs b/src/test.rs index 30d94bdf34..7af7d60b92 100644 --- a/src/test.rs +++ b/src/test.rs @@ -17,8 +17,7 @@ use std::path::Path; fn test_facts(all_facts: &AllFacts, algorithms: &[Algorithm]) { let naive = Output::compute(all_facts, Algorithm::Naive, true); - // Check that the "naive errors" are a subset of the "insensitive - // ones". + // Check that the "naive errors" are a subset of the "insensitive ones". let insensitive = Output::compute(all_facts, Algorithm::LocationInsensitive, false); for (naive_point, naive_loans) in &naive.errors { match insensitive.errors.get(&naive_point) { @@ -77,18 +76,37 @@ fn test_facts(all_facts: &AllFacts, algorithms: &[Algorithm]) { for &optimized_algorithm in algorithms { println!("Algorithm {:?}", optimized_algorithm); let opt = Output::compute(all_facts, optimized_algorithm, true); - // TMP: until we reach our correctness goals, deactivate some comparisons between variants - // assert_equal(&naive.loan_live_at, &opt.loan_live_at); - assert_equal(&naive.errors, &opt.errors); - assert_equal(&naive.subset_errors, &opt.subset_errors); - assert_equal(&naive.move_errors, &opt.move_errors); + assert_equal( + &naive.loan_live_at, + &opt.loan_live_at, + "naive vs opt loan_live_at", + ); + assert_equal(&naive.errors, &opt.errors, "naive vs opt errors"); + assert_equal( + &naive.subset_errors, + &opt.subset_errors, + "naive vs opt subset_errors", + ); + assert_equal( + &naive.move_errors, + &opt.move_errors, + "naive vs opt move_errors", + ); } // The hybrid algorithm gets the same errors as the naive version let opt = Output::compute(all_facts, Algorithm::Hybrid, true); - assert_equal(&naive.errors, &opt.errors); - assert_equal(&naive.subset_errors, &opt.subset_errors); - assert_equal(&naive.move_errors, &opt.move_errors); + assert_equal(&naive.errors, &opt.errors, "naive vs hybrid errors"); + assert_equal( + &naive.subset_errors, + &opt.subset_errors, + "naive vs hybrid subset_errors", + ); + assert_equal( + &naive.move_errors, + &opt.move_errors, + "naive vs hybrid move_errors", + ); } fn test_fn(dir_name: &str, fn_name: &str, algorithm: Algorithm) -> Result<(), Box> { @@ -155,7 +173,7 @@ fn test_insensitive_errors() -> Result<(), Box> { expected.insert(Point::from(24), vec![Loan::from(1)]); expected.insert(Point::from(50), vec![Loan::from(2)]); - assert_equal(&insensitive.errors, &expected); + assert_equal(&insensitive.errors, &expected, "insensitive errors"); Ok(()) } diff --git a/src/test_util.rs b/src/test_util.rs index f0f9c11e66..2aa6cac85e 100644 --- a/src/test_util.rs +++ b/src/test_util.rs @@ -8,13 +8,13 @@ use crate::intern::InternerTables; use crate::program::parse_from_program; /// Test that two values are equal, with a better error than `assert_eq` -pub fn assert_equal(expected_value: &A, actual_value: &A) +pub fn assert_equal(expected_value: &A, actual_value: &A, message: &str) where A: ?Sized + Debug + Eq, { // First check that they have the same debug text. This produces a better error. let expected_text = format!("{:#?}", expected_value); - assert_expected_debug(&expected_text, actual_value); + assert_expected_debug(&expected_text, actual_value, message); // Then check that they are `eq` too, for good measure. assert_eq!(expected_value, actual_value); @@ -22,7 +22,7 @@ where /// Test that the debug output of `actual_value` is as expected. Gives /// a nice diff if things fail. -pub fn assert_expected_debug(expected_text: &str, actual_value: &A) +pub fn assert_expected_debug(expected_text: &str, actual_value: &A, message: &str) where A: ?Sized + Debug, { @@ -47,7 +47,7 @@ where } } - panic!("debug comparison failed"); + panic!("debug comparison failed: {}", message); } /// Builder for fact checking assertions @@ -92,9 +92,13 @@ pub(crate) fn assert_checkers_match(checker_a: &FactChecker, checker_b: &FactChe } pub(crate) fn assert_outputs_match(output_a: &Output, output_b: &Output) { - assert_equal(&output_a.errors, &output_b.errors); - assert_equal(&output_a.subset_errors, &output_b.subset_errors); - assert_equal(&output_a.move_errors, &output_b.move_errors); + assert_equal(&output_a.errors, &output_b.errors, "errors"); + assert_equal( + &output_a.subset_errors, + &output_b.subset_errors, + "subset_errors", + ); + assert_equal(&output_a.move_errors, &output_b.move_errors, "move_errors"); } impl FactChecker {