From 7284e48ade4308d5b5a862a07471359c687cd044 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Rakic?= Date: Tue, 22 Dec 2020 23:34:36 +0100 Subject: [PATCH 1/5] tests: re-enable comparisons of the `loan_live_at` relation Also, add a descriptive message if the `assert_equal` helper fails its assertions. --- src/test.rs | 40 +++++++++++++++++++++++++++++----------- src/test_util.rs | 18 +++++++++++------- 2 files changed, 40 insertions(+), 18 deletions(-) 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 { From 539492d9da55e18fbd20987f886085a5f3676f2a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Rakic?= Date: Tue, 22 Dec 2020 23:42:35 +0100 Subject: [PATCH 2/5] location insensitive: handle placeholders explicitly instead of a by-product of liveness MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Also, number and comment the rules, because the expansions are very verbose and mistakes are easy to make here. We simplified the rules by modeling the fact that placeholder origins are live at all points by ... materializing this as actual tuples in the `origin_live_on_entry` relation, even though liveness analysis does not computes that. This was also done because soufflé provides an easy `;` alternative operator, while datafrog requires us to do the alternative expansions manually. (Also we were lazy) --- .../src/output/location_insensitive.rs | 33 +++++++++++++++++-- 1 file changed, 31 insertions(+), 2 deletions(-) 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, _), From f103a75a638e076bfb8f8734c1a5fca8edb8e0a4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Rakic?= Date: Tue, 22 Dec 2020 23:44:24 +0100 Subject: [PATCH 3/5] naive: handle placeholders explicitly in the rules MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We simplified the rules by modeling the fact that placeholder origins are live at all points by ... materializing this as actual tuples in the `origin_live_on_entry` relation, even though liveness analysis does not computes that. This was also done because soufflé provides an easy `;` alternative operator, while datafrog requires us to do the alternative expansions manually. (Also we were lazy) --- polonius-engine/src/output/naive.rs | 92 ++++++++++++++++++++++++++--- 1 file changed, 83 insertions(+), 9 deletions(-) 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), From e6dd2fb7707892848f4242bf37c6d6f94168e12f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Rakic?= Date: Tue, 22 Dec 2020 23:53:03 +0100 Subject: [PATCH 4/5] opt: handle placeholders explicitly in the rules MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Also, number and comment some rules. We simplified the rules by modeling the fact that placeholder origins are live at all points by ... materializing this as actual tuples in the `origin_live_on_entry` relation, even though liveness analysis does not computes that. This was also done because soufflé provides an easy `;` alternative operator, while datafrog requires us to do the alternative expansions manually. (Also we were lazy). Where possible `filter_with` leapers were added, and where WF-ness would not be possible, `extend_with` leapers were used. This should be similar here: the `placeholder_origin` relation being a single value relation, there is only a single unit tuple to extend a key with. --- polonius-engine/src/output/datafrog_opt.rs | 205 +++++++++++++++++++-- 1 file changed, 188 insertions(+), 17 deletions(-) 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). From c44775144e8825570281504702cacc152f5e5908 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Rakic?= Date: Tue, 22 Dec 2020 23:57:50 +0100 Subject: [PATCH 5/5] liveness: stop materializing facts that placeholders are live at all points --- polonius-engine/src/output/liveness.rs | 20 ++------------------ polonius-engine/src/output/mod.rs | 16 +--------------- 2 files changed, 3 insertions(+), 33 deletions(-) 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/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.