From c75dc8df5fc42c9612d6f559800e493be554505c Mon Sep 17 00:00:00 2001 From: lqd Date: Tue, 4 Aug 2020 14:18:10 +0200 Subject: [PATCH 01/15] compute location-insensitive potential subset errors - make the location-insensitive variant compute potential subset errors using placeholder loans - record those potential errors in the context for the Opt variant to make use of in the context of the Hybrid analysis --- .../src/output/location_insensitive.rs | 47 +++++++++++++++++-- polonius-engine/src/output/mod.rs | 32 ++++++++++--- 2 files changed, 67 insertions(+), 12 deletions(-) diff --git a/polonius-engine/src/output/location_insensitive.rs b/polonius-engine/src/output/location_insensitive.rs index 8a975f8575..5f6ed3ae59 100644 --- a/polonius-engine/src/output/location_insensitive.rs +++ b/polonius-engine/src/output/location_insensitive.rs @@ -17,13 +17,19 @@ use crate::output::{Context, Output}; pub(super) fn compute( ctx: &Context<'_, T>, result: &mut Output, -) -> Relation<(T::Loan, T::Point)> { +) -> ( + Relation<(T::Loan, T::Point)>, + Relation<(T::Origin, T::Origin)>, +) { let timer = Instant::now(); - let potential_errors = { + let (potential_errors, potential_subset_errors) = { // Static inputs let origin_live_on_entry = &ctx.origin_live_on_entry; let loan_invalidated_at = &ctx.loan_invalidated_at; + let placeholder_origin = &ctx.placeholder_origin; + let placeholder_loan = &ctx.placeholder_loan; + let known_contains = &ctx.known_contains; // Create a new iteration context, ... let mut iteration = Iteration::new(); @@ -34,6 +40,8 @@ pub(super) fn compute( iteration.variable::<(T::Origin, T::Loan)>("origin_contains_loan_on_entry"); let potential_errors = iteration.variable::<(T::Loan, T::Point)>("potential_errors"); + let potential_subset_errors = + iteration.variable::<(T::Origin, T::Origin)>("potential_subset_errors"); // load initial facts. @@ -53,6 +61,14 @@ pub(super) fn compute( .map(|&(origin, loan, _point)| (origin, loan)), ); + // origin_contains_loan_on_entry(Origin, Loan) :- + // placeholder_loan(Origin, Loan). + origin_contains_loan_on_entry.extend( + placeholder_loan + .iter() + .map(|&(loan, origin)| (origin, loan)), + ); + // .. and then start iterating rules! while iteration.changed() { // origin_contains_loan_on_entry(origin2, loan) :- @@ -86,6 +102,23 @@ pub(super) fn compute( ), |&(_origin, loan), &point| (loan, point), ); + + // potential_subset_errors(Origin1, Origin2) :- + // placeholder(Origin1, Loan1), + // placeholder(Origin2, _), + // origin_contains_loan_on_entry(Origin2, Loan1), + // !known_contains(Origin2, Loan1). + potential_subset_errors.from_leapjoin( + &origin_contains_loan_on_entry, + ( + known_contains.filter_anti(|&(origin2, loan1)| (origin2, loan1)), + placeholder_origin.filter_with(|&(origin2, _loan1)| (origin2, ())), + placeholder_loan.extend_with(|&(_origin2, loan1)| loan1), + // remove symmetries: + datafrog::ValueFilter::from(|&(origin2, _loan1), &origin1| origin2 != origin1), + ), + |&(origin2, _loan1), &origin1| (origin1, origin2), + ); } if result.dump_enabled { @@ -108,14 +141,18 @@ pub(super) fn compute( } } - potential_errors.complete() + ( + potential_errors.complete(), + potential_subset_errors.complete(), + ) }; info!( - "potential_errors is complete: {} tuples, {:?}", + "location_insensitive is complete: {} `potential_errors` tuples, {} `potential_subset_errors` tuples, {:?}", potential_errors.len(), + potential_subset_errors.len(), timer.elapsed() ); - potential_errors + (potential_errors, potential_subset_errors) } diff --git a/polonius-engine/src/output/mod.rs b/polonius-engine/src/output/mod.rs index 610bf7d1d7..19e4bcf379 100644 --- a/polonius-engine/src/output/mod.rs +++ b/polonius-engine/src/output/mod.rs @@ -138,6 +138,7 @@ struct Context<'ctx, T: FactTypes> { // Partial results possibly used by other variants as input potential_errors: Option>, + potential_subset_errors: Option>, } impl Output { @@ -267,10 +268,28 @@ impl Output { placeholder_origin, placeholder_loan, potential_errors: None, + potential_subset_errors: None, }; let errors = match algorithm { - Algorithm::LocationInsensitive => location_insensitive::compute(&ctx, &mut result), + Algorithm::LocationInsensitive => { + let (potential_errors, potential_subset_errors) = + location_insensitive::compute(&ctx, &mut result); + + // Note: the error location is meaningless for a location-insensitive + // subset error analysis. This is acceptable here as this variant is not one + // which should be used directly besides for debugging, the `Hybrid` variant will + // take advantage of its result. + for &(origin1, origin2) in potential_subset_errors.iter() { + result + .subset_errors + .entry(0.into()) + .or_default() + .insert((origin1, origin2)); + } + + potential_errors + } Algorithm::Naive => { let (errors, subset_errors) = naive::compute(&ctx, &mut result); @@ -287,21 +306,20 @@ impl Output { } Algorithm::DatafrogOpt => datafrog_opt::compute(&ctx, &mut result), Algorithm::Hybrid => { - // WIP: the `LocationInsensitive` variant doesn't compute any illegal subset - // relation errors. So using it as a quick pre-filter for illegal accesses - // errors will also end up skipping checking for subset errors. - // Execute the fast `LocationInsensitive` computation as a pre-pass: // if it finds no possible errors, we don't need to do the more complex // computations as they won't find errors either, and we can return early. - let potential_errors = location_insensitive::compute(&ctx, &mut result); - if potential_errors.is_empty() { + let (potential_errors, potential_subset_errors) = + location_insensitive::compute(&ctx, &mut result); + + if potential_errors.is_empty() && potential_subset_errors.is_empty() { potential_errors } else { // Record these potential errors as they can be used to limit the next // variant's work to only these loans. ctx.potential_errors = Some(potential_errors.iter().map(|&(loan, _)| loan).collect()); + ctx.potential_subset_errors = Some(potential_subset_errors); datafrog_opt::compute(&ctx, &mut result) } From e5e0e933f10e75cdf386468abb8c1456420baea7 Mon Sep 17 00:00:00 2001 From: lqd Date: Tue, 4 Aug 2020 14:21:38 +0200 Subject: [PATCH 02/15] `subset` is actually a static input and can be a Relation --- .../src/output/location_insensitive.rs | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/polonius-engine/src/output/location_insensitive.rs b/polonius-engine/src/output/location_insensitive.rs index 5f6ed3ae59..18918aff12 100644 --- a/polonius-engine/src/output/location_insensitive.rs +++ b/polonius-engine/src/output/location_insensitive.rs @@ -31,11 +31,18 @@ pub(super) fn compute( let placeholder_loan = &ctx.placeholder_loan; let known_contains = &ctx.known_contains; + // subset(Origin1, Origin2) :- + // subset_base(Origin1, Origin2, _). + let subset = Relation::from_iter( + ctx.subset_base + .iter() + .map(|&(origin1, origin2, _point)| (origin1, origin2)), + ); + // Create a new iteration context, ... let mut iteration = Iteration::new(); // .. some variables, .. - let subset = iteration.variable::<(T::Origin, T::Origin)>("subset"); let origin_contains_loan_on_entry = iteration.variable::<(T::Origin, T::Loan)>("origin_contains_loan_on_entry"); @@ -45,14 +52,6 @@ pub(super) fn compute( // load initial facts. - // subset(origin1, origin2) :- - // subset_base(origin1, origin2, _point). - subset.extend( - ctx.subset_base - .iter() - .map(|&(origin1, origin2, _point)| (origin1, origin2)), - ); - // origin_contains_loan_on_entry(origin, loan) :- // loan_issued_at(origin, loan, _point). origin_contains_loan_on_entry.extend( @@ -122,7 +121,6 @@ pub(super) fn compute( } if result.dump_enabled { - let subset = subset.complete(); for &(origin1, origin2) in subset.iter() { result .subset_anywhere From bf125c3e780c163910c10b8f757ee6bef129c502 Mon Sep 17 00:00:00 2001 From: lqd Date: Tue, 4 Aug 2020 14:24:19 +0200 Subject: [PATCH 03/15] comment craftsmanship --- .../src/output/location_insensitive.rs | 22 +++++++++---------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/polonius-engine/src/output/location_insensitive.rs b/polonius-engine/src/output/location_insensitive.rs index 18918aff12..8556fb2484 100644 --- a/polonius-engine/src/output/location_insensitive.rs +++ b/polonius-engine/src/output/location_insensitive.rs @@ -52,8 +52,8 @@ pub(super) fn compute( // load initial facts. - // origin_contains_loan_on_entry(origin, loan) :- - // loan_issued_at(origin, loan, _point). + // origin_contains_loan_on_entry(Origin, Loan) :- + // loan_issued_at(Origin, Loan, _). origin_contains_loan_on_entry.extend( ctx.loan_issued_at .iter() @@ -70,9 +70,9 @@ pub(super) fn compute( // .. and then start iterating rules! while iteration.changed() { - // origin_contains_loan_on_entry(origin2, loan) :- - // origin_contains_loan_on_entry(origin1, loan), - // subset(origin1, origin2). + // origin_contains_loan_on_entry(Origin2, Loan) :- + // origin_contains_loan_on_entry(Origin1, Loan), + // subset(Origin1, Origin2). // // Note: Since `subset` is effectively a static input, this join can be ported to // a leapjoin. Doing so, however, was 7% slower on `clap`. @@ -82,13 +82,13 @@ pub(super) fn compute( |&_origin1, &loan, &origin2| (origin2, loan), ); - // loan_live_at(loan, point) :- - // origin_contains_loan_on_entry(origin, loan), - // origin_live_on_entry(origin, point) + // loan_live_at(Loan, Point) :- + // origin_contains_loan_on_entry(Origin, Loan), + // origin_live_on_entry(Origin, Point) // - // potential_errors(loan, point) :- - // loan_invalidated_at(loan, point), - // loan_live_at(loan, point). + // potential_errors(Loan, Point) :- + // loan_invalidated_at(Loan, Point), + // loan_live_at(Loan, Point). // // Note: we don't need to materialize `loan_live_at` here // so we can inline it in the `potential_errors` relation. From 3e83792513df4238d86c41ffda359cf040015e9b Mon Sep 17 00:00:00 2001 From: lqd Date: Tue, 4 Aug 2020 15:48:54 +0200 Subject: [PATCH 04/15] augment tests to check for location-insensitive subset errors --- src/test.rs | 126 +++++++++++++++++++++++++++++++++++++---------- src/test_util.rs | 35 ++++++++++++- 2 files changed, 134 insertions(+), 27 deletions(-) diff --git a/src/test.rs b/src/test.rs index cc2224ae08..b336c3a548 100644 --- a/src/test.rs +++ b/src/test.rs @@ -5,7 +5,7 @@ use crate::facts::{AllFacts, Loan, Origin, Point}; use crate::intern; use crate::program::parse_from_program; use crate::tab_delim; -use crate::test_util::{assert_equal, check_program}; +use crate::test_util::{assert_equal, location_insensitive_checker_for, naive_checker_for}; use polonius_engine::Algorithm; use rustc_hash::FxHashMap; use std::error::Error; @@ -42,6 +42,34 @@ fn test_facts(all_facts: &AllFacts, algorithms: &[Algorithm]) { } } + // Check that the "naive subset errors" are a subset of the "insensitive ones". + for (naive_point, naive_origins) in &naive.subset_errors { + // Potential location-insensitive errors don't have a meaningful location, and use 0 + // as a default when debugging. + match insensitive.subset_errors.get(&0.into()) { + Some(insensitive_origins) => { + for &(origin1, origin2) in naive_origins { + if !insensitive_origins.contains(&(origin1, origin2)) { + panic!( + "naive analysis had subset error for `{:?}` <: `{:?}` at `{:?}` \ + but insensitive analysis did not \ + (origins = {:#?})", + origin1, origin2, naive_point, insensitive_origins, + ); + } + } + } + + None => { + panic!( + "naive analysis had subset errors at `{:?}` but insensitive analysis did not \ + (origins = {:#?})", + naive_point, naive_origins, + ); + } + } + } + // The optimized checks should behave exactly the same as the naive check. for &optimized_algorithm in algorithms { println!("Algorithm {:?}", optimized_algorithm); @@ -542,7 +570,7 @@ fn illegal_subset_error() { } "; - let mut checker = check_program(program, Algorithm::Naive, true); + let mut checker = naive_checker_for(program); assert_eq!(checker.facts.universal_region.len(), 2); assert_eq!(checker.facts.placeholder.len(), 2); @@ -553,6 +581,10 @@ fn illegal_subset_error() { // ...so there should be an error here about the missing `'b: 'a` subset assert_eq!(checker.subset_errors_count(), 1); assert!(checker.subset_error_exists("'b", "'a", "\"Mid(B0[0])\"")); + + // and in the location-insensitive results as well + assert!(location_insensitive_checker_for(program) + .location_insensitive_subset_error_exists("'b", "'a",)); } /// This is the same test as the `illegal_subset_error` one, but specifies the `'b: 'a` subset @@ -570,13 +602,17 @@ fn known_placeholder_origin_subset() { } "; - let checker = check_program(program, Algorithm::Naive, true); + let checker = naive_checker_for(program); assert_eq!(checker.facts.universal_region.len(), 2); assert_eq!(checker.facts.placeholder.len(), 2); assert_eq!(checker.facts.known_subset.len(), 1); assert_eq!(checker.subset_errors_count(), 0); + assert_eq!( + location_insensitive_checker_for(program).subset_errors_count(), + 0 + ); } /// This test ensures `known_subset`s are handled transitively: a known subset `'a: 'c` should be @@ -594,7 +630,7 @@ fn transitive_known_subset() { } "; - let checker = check_program(program, Algorithm::Naive, true); + let checker = naive_checker_for(program); assert_eq!(checker.facts.universal_region.len(), 3); assert_eq!(checker.facts.placeholder.len(), 3); @@ -604,6 +640,10 @@ fn transitive_known_subset() { assert_eq!(checker.output.known_contains.len(), 3); assert_eq!(checker.subset_errors_count(), 0); + assert_eq!( + location_insensitive_checker_for(program).subset_errors_count(), + 0 + ); } /// Even if `'a: 'b` is known, `'a`'s placeholder loan can flow into `'b''s supersets, @@ -619,22 +659,32 @@ fn transitive_illegal_subset_error() { loan_issued_at('x, L0), outlives('a: 'x), outlives('x: 'b); - // creates an unknown transitive `'a: 'c` subset + + // creates unknown transitive subsets: + // - `'b: 'c` + // - and therefore `'a: 'c` loan_issued_at('y, L1), outlives('b: 'y), outlives('y: 'c); } "; - let mut checker = check_program(program, Algorithm::Naive, true); + let mut checker = naive_checker_for(program); assert_eq!(checker.facts.universal_region.len(), 3); assert_eq!(checker.facts.placeholder.len(), 3); assert_eq!(checker.facts.known_subset.len(), 1); - // there should be an error here about the missing `'a: 'c` subset - assert_eq!(checker.subset_errors_count(), 1); + // There should be 2 errors here about the missing `'b: 'c` and `'a: 'c` subsets. + assert_eq!(checker.subset_errors_count(), 2); + assert!(checker.subset_error_exists("'b", "'c", "\"Mid(B0[1])\"")); assert!(checker.subset_error_exists("'a", "'c", "\"Mid(B0[1])\"")); + + // And similarly in the location-insensitive analysis. + let mut checker = location_insensitive_checker_for(program); + assert_eq!(checker.subset_errors_count(), 2); + assert!(checker.location_insensitive_subset_error_exists("'b", "'c")); + assert!(checker.location_insensitive_subset_error_exists("'a", "'c")); } #[test] @@ -651,9 +701,13 @@ fn successes_in_subset_relations_dataset() { let tables = &mut intern::InternerTables::new(); let facts = tab_delim::load_tab_delimited_facts(tables, &facts_dir).expect("facts"); - let result = Output::compute(&facts, Algorithm::Naive, true); - assert!(result.errors.is_empty()); - assert!(result.subset_errors.is_empty()); + let naive = Output::compute(&facts, Algorithm::Naive, true); + assert!(naive.errors.is_empty()); + assert!(naive.subset_errors.is_empty()); + + let insensitive = Output::compute(&facts, Algorithm::LocationInsensitive, true); + assert!(insensitive.errors.is_empty()); + assert!(insensitive.subset_errors.is_empty()); } } @@ -668,25 +722,40 @@ fn errors_in_subset_relations_dataset() { let facts = tab_delim::load_tab_delimited_facts(tables, &facts_dir).expect("facts"); // this function has no illegal access errors, but one subset error, over 3 points - let result = Output::compute(&facts, Algorithm::Naive, true); - assert!(result.errors.is_empty()); - assert_eq!(result.subset_errors.len(), 3); - - let points = ["\"Mid(bb0[0])\"", "\"Start(bb0[1])\"", "\"Mid(bb0[1])\""]; - for point in &points { - let point = tables.points.intern(point); - let subset_error = result.subset_errors.get(&point).unwrap(); + let naive = Output::compute(&facts, Algorithm::Naive, true); + assert!(naive.errors.is_empty()); + assert_eq!(naive.subset_errors.len(), 3); + let expected_subset_error = { // in this dataset, `'a` is interned as `'1` let origin_a = Origin::from(1); // `'b` is interned as `'2` let origin_b = Origin::from(2); - // and there should be a `'b: 'a` known subset to make the function valid, so - // that is the subset error we should find - assert!(subset_error.contains(&(origin_b, origin_a))); + // and `'b` should flow into `'a` + (origin_b, origin_a) + }; + + let points = ["\"Mid(bb0[0])\"", "\"Start(bb0[1])\"", "\"Mid(bb0[1])\""]; + for point in &points { + let point = tables.points.intern(point); + let subset_error = naive.subset_errors.get(&point).unwrap(); + + // There should be a `'b: 'a` known subset to make the function valid, so + // that is the subset error we should find. + assert!(subset_error.contains(&expected_subset_error)); } + + // Similarly, this single subset error should also be found by the + // location-insensitive analysis. + let insensitive = Output::compute(&facts, Algorithm::LocationInsensitive, true); + assert!(insensitive.errors.is_empty()); + assert_eq!(insensitive.subset_errors.len(), 1); + + let insensitive_subset_errors = insensitive.subset_errors.values().next().unwrap(); + assert_eq!(insensitive_subset_errors.len(), 1); + assert!(insensitive_subset_errors.contains(&expected_subset_error)); } // There's only a single successful test in the dataset for now, but the structure of this test @@ -705,10 +774,15 @@ fn successes_in_move_errors_dataset() { let tables = &mut intern::InternerTables::new(); let facts = tab_delim::load_tab_delimited_facts(tables, &facts_dir).expect("facts"); - let result = Output::compute(&facts, Algorithm::Naive, true); - assert!(result.errors.is_empty()); - assert!(result.subset_errors.is_empty()); - assert!(result.move_errors.is_empty()); + let naive = Output::compute(&facts, Algorithm::Naive, true); + assert!(naive.errors.is_empty()); + assert!(naive.subset_errors.is_empty()); + assert!(naive.move_errors.is_empty()); + + let insensitive = Output::compute(&facts, Algorithm::LocationInsensitive, true); + assert!(insensitive.errors.is_empty()); + assert!(insensitive.subset_errors.is_empty()); + assert!(insensitive.move_errors.is_empty()); } } diff --git a/src/test_util.rs b/src/test_util.rs index b0a9088696..39b39b4f25 100644 --- a/src/test_util.rs +++ b/src/test_util.rs @@ -75,6 +75,14 @@ pub(crate) fn check_program( } } +pub(crate) fn naive_checker_for(program: &str) -> FactChecker { + check_program(program, Algorithm::Naive, true) +} + +pub(crate) fn location_insensitive_checker_for(program: &str) -> FactChecker { + check_program(program, Algorithm::LocationInsensitive, true) +} + impl FactChecker { /// Asserts that there is a `subset_error` `origin1: origin2` at the specified `point`. pub fn subset_error_exists(&mut self, origin1: &str, origin2: &str, point: &str) -> bool { @@ -90,7 +98,32 @@ impl FactChecker { subset_errors.contains(&(origin1, origin2)) } + /// Asserts that there is a `subset_error` `origin1: origin2`. + /// The location of the subset error is ignored. + pub fn location_insensitive_subset_error_exists( + &mut self, + origin1: &str, + origin2: &str, + ) -> bool { + // Location-insensitive subset errors are wrapped at a single meaningless point + assert_eq!(self.output.subset_errors.len(), 1); + + let subset_errors = self + .output + .subset_errors + .values() + .next() + .expect("No subset errors found"); + + let origin1 = self.tables.origins.intern(origin1); + let origin2 = self.tables.origins.intern(origin2); + subset_errors.contains(&(origin1, origin2)) + } + + /// The number of undeclared relationships causing subset errors. + /// Note that this is different from checking `output.subset_errors.len()` as subset errors are + /// grouped by the location where they are detected. pub fn subset_errors_count(&self) -> usize { - self.output.subset_errors.len() + self.output.subset_errors.values().map(|origins| origins.len()).sum() } } From d9feffd260743ae0d0d3c89f34a7bbbeeaef326d Mon Sep 17 00:00:00 2001 From: lqd Date: Tue, 4 Aug 2020 18:42:55 +0200 Subject: [PATCH 05/15] unify a log output --- polonius-engine/src/output/location_insensitive.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/polonius-engine/src/output/location_insensitive.rs b/polonius-engine/src/output/location_insensitive.rs index 8556fb2484..83ce27757d 100644 --- a/polonius-engine/src/output/location_insensitive.rs +++ b/polonius-engine/src/output/location_insensitive.rs @@ -146,7 +146,7 @@ pub(super) fn compute( }; info!( - "location_insensitive is complete: {} `potential_errors` tuples, {} `potential_subset_errors` tuples, {:?}", + "analysis done: {} `potential_errors` tuples, {} `potential_subset_errors` tuples, {:?}", potential_errors.len(), potential_subset_errors.len(), timer.elapsed() From 0e44c05b49e4848da2c027e9d91ff6c55a8e7d81 Mon Sep 17 00:00:00 2001 From: lqd Date: Tue, 4 Aug 2020 19:27:58 +0200 Subject: [PATCH 06/15] make the Opt variant compute subset errors --- polonius-engine/src/output/datafrog_opt.rs | 71 +++++++++++++++-- polonius-engine/src/output/mod.rs | 92 +++++++++++++++------- 2 files changed, 129 insertions(+), 34 deletions(-) diff --git a/polonius-engine/src/output/datafrog_opt.rs b/polonius-engine/src/output/datafrog_opt.rs index 564696c304..9cb29e021e 100644 --- a/polonius-engine/src/output/datafrog_opt.rs +++ b/polonius-engine/src/output/datafrog_opt.rs @@ -17,14 +17,19 @@ use crate::output::{Context, Output}; pub(super) fn compute( ctx: &Context<'_, T>, result: &mut Output, -) -> Relation<(T::Loan, T::Point)> { +) -> ( + Relation<(T::Loan, T::Point)>, + Relation<(T::Origin, T::Origin, T::Point)>, +) { let timer = Instant::now(); - let errors = { + let (errors, subset_errors) = { // Static inputs let origin_live_on_entry_rel = &ctx.origin_live_on_entry; let cfg_edge_rel = &ctx.cfg_edge; let loan_killed_at = &ctx.loan_killed_at; + let known_subset = &ctx.known_subset; + let placeholder_origin = &ctx.placeholder_origin; // Create a new iteration context, ... let mut iteration = Iteration::new(); @@ -127,6 +132,11 @@ pub(super) fn compute( // .decl errors(loan, point) let errors = iteration.variable("errors"); + let subset_errors = iteration.variable::<(T::Origin, T::Origin, T::Point)>("subset_errors"); + + let subset_placeholder = + iteration.variable::<(T::Origin, T::Origin, T::Point)>("subset_placeholder"); + let subset_placeholder_o2p = iteration.variable_indistinct("subset_placeholder_o2p"); // Make "variable" versions of the relations, needed for joins. loan_issued_at_op.extend( @@ -177,6 +187,15 @@ pub(super) fn compute( .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) + }); + // live_to_dying_regions(origin1, origin2, point1, point2) :- // subset(origin1, origin2, point1), // cfg_edge(point1, point2), @@ -378,6 +397,47 @@ pub(super) fn compute( &loan_live_at, |&(loan, point), _, _| (loan, point), ); + + // subset_placeholder(Origin1, Origin2, Point) :- + // subset(Origin1, Origin2, Point), + // 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 + }), + ), + |&((origin1, point), origin2), _| (origin1, origin2, point), + ); + + // subset_placeholder(Origin1, Origin3, Point) :- + // subset_placeholder(Origin1, Origin2, Point), + // subset(Origin2, Origin3, Point). + subset_placeholder.from_join( + &subset_placeholder_o2p, + &subset_o1p, + |&(_origin2, point), &origin1, &origin3| (origin1, origin3, point), + ); + + // subset_error(Origin1, Origin2, Point) :- + // subset_placeholder(Origin1, Origin2, Point), + // placeholder_origin(Origin2), + // !known_subset(Origin1, Origin2). + subset_errors.from_leapjoin( + &subset_placeholder, + ( + placeholder_origin.extend_with(|&(_origin1, origin2, _point)| origin2), + known_subset.filter_anti(|&(origin1, origin2, _point)| (origin1, origin2)), + // remove symmetries: + datafrog::ValueFilter::from(|&(origin1, origin2, _point), _| { + origin1 != origin2 + }), + ), + |&(origin1, origin2, point), _| (origin1, origin2, point), + ); } if result.dump_enabled { @@ -417,14 +477,15 @@ pub(super) fn compute( } } - errors.complete() + (errors.complete(), subset_errors.complete()) }; info!( - "errors is complete: {} tuples, {:?}", + "analysis done: {} `errors` tuples, {} `subset_errors` tuples, {:?}", errors.len(), + subset_errors.len(), timer.elapsed() ); - errors + (errors, subset_errors) } diff --git a/polonius-engine/src/output/mod.rs b/polonius-engine/src/output/mod.rs index 19e4bcf379..1484464590 100644 --- a/polonius-engine/src/output/mod.rs +++ b/polonius-engine/src/output/mod.rs @@ -132,6 +132,11 @@ struct Context<'ctx, T: FactTypes> { placeholder_origin: Relation<(T::Origin, ())>, placeholder_loan: Relation<(T::Loan, T::Origin)>, + // The `known_subset` relation in the facts does not necessarily contain all the transitive + // subsets. The transitive closure is always needed, so this version here is fully closed + // over. + known_subset: Relation<(T::Origin, T::Origin)>, + // while this static input is unused by `LocationInsensitive`, it's depended on by initialization // and liveness, so already computed by the time we get to borrowcking. cfg_edge: Relation<(T::Point, T::Point)>, @@ -241,6 +246,9 @@ impl Output { let known_contains = Output::::compute_known_contains(&known_subset, &all_facts.placeholder); + // Fully close over the `known_subset` relation. + let known_subset = Output::::compute_known_subset(&known_subset); + let placeholder_origin: Relation<_> = Relation::from_iter( all_facts .universal_region @@ -265,45 +273,32 @@ impl Output { loan_issued_at: &all_facts.loan_issued_at, loan_killed_at, known_contains, + known_subset, placeholder_origin, placeholder_loan, potential_errors: None, potential_subset_errors: None, }; - let errors = match algorithm { + let (errors, subset_errors) = match algorithm { Algorithm::LocationInsensitive => { let (potential_errors, potential_subset_errors) = location_insensitive::compute(&ctx, &mut result); // Note: the error location is meaningless for a location-insensitive // subset error analysis. This is acceptable here as this variant is not one - // which should be used directly besides for debugging, the `Hybrid` variant will + // which should be used directly besides debugging, the `Hybrid` variant will // take advantage of its result. - for &(origin1, origin2) in potential_subset_errors.iter() { - result - .subset_errors - .entry(0.into()) - .or_default() - .insert((origin1, origin2)); - } - - potential_errors - } - Algorithm::Naive => { - let (errors, subset_errors) = naive::compute(&ctx, &mut result); - - // Record illegal subset errors - for &(origin1, origin2, location) in subset_errors.iter() { - result - .subset_errors - .entry(location) - .or_default() - .insert((origin1, origin2)); - } - - errors + let potential_subset_errors: Relation<(T::Origin, T::Origin, T::Point)> = + Relation::from_iter( + potential_subset_errors + .into_iter() + .map(|&(origin1, origin2)| (origin1, origin2, 0.into())), + ); + + (potential_errors, potential_subset_errors) } + Algorithm::Naive => naive::compute(&ctx, &mut result), Algorithm::DatafrogOpt => datafrog_opt::compute(&ctx, &mut result), Algorithm::Hybrid => { // Execute the fast `LocationInsensitive` computation as a pre-pass: @@ -313,7 +308,9 @@ impl Output { location_insensitive::compute(&ctx, &mut result); if potential_errors.is_empty() && potential_subset_errors.is_empty() { - potential_errors + // There are no loan errors, nor subset errors, we can early return + // empty errors lists and avoid doing the heavy analysis. + (potential_errors, Vec::new().into()) } else { // Record these potential errors as they can be used to limit the next // variant's work to only these loans. @@ -326,8 +323,8 @@ impl Output { } Algorithm::Compare => { // Ensure the `Naive` and `DatafrogOpt` errors are the same - let (naive_errors, _) = naive::compute(&ctx, &mut result); - let opt_errors = datafrog_opt::compute(&ctx, &mut result); + let (naive_errors, naive_subset_errors) = naive::compute(&ctx, &mut result); + let (opt_errors, _) = datafrog_opt::compute(&ctx, &mut result); // TODO: compare illegal subset relations errors as well here ? @@ -357,7 +354,7 @@ impl Output { debug!("Naive and optimized algorithms reported the same errors."); } - naive_errors + (naive_errors, naive_subset_errors) } }; @@ -366,6 +363,15 @@ impl Output { result.errors.entry(location).or_default().push(loan); } + // Record illegal subset errors + for &(origin1, origin2, location) in subset_errors.iter() { + result + .subset_errors + .entry(location) + .or_default() + .insert((origin1, origin2)); + } + // Record more debugging info when asked to do so if dump_enabled { for &(origin, location) in ctx.origin_live_on_entry.iter() { @@ -415,6 +421,34 @@ impl Output { known_contains.complete() } + /// Computes the transitive closure of the `known_subset` relation. + fn compute_known_subset( + known_subset: &Relation<(T::Origin, T::Origin)>, + ) -> Relation<(T::Origin, T::Origin)> { + use datafrog::{Iteration, RelationLeaper}; + let mut iteration = Iteration::new(); + + let known_subset_base = known_subset; + let known_subset = iteration.variable("known_subset"); + + // known_subset(Origin1, Origin2) :- + // known_subset_base(Origin1, Origin2). + known_subset.extend(known_subset_base.iter()); + + while iteration.changed() { + // known_subset(Origin1, Origin3) :- + // known_subset(Origin1, Origin2), + // known_subset_base(Origin2, Origin3). + known_subset.from_leapjoin( + &known_subset, + known_subset_base.extend_with(|&(_origin1, origin2)| origin2), + |&(origin1, _origin2), &origin3| (origin1, origin3), + ); + } + + known_subset.complete() + } + fn new(dump_enabled: bool) -> Self { Output { errors: FxHashMap::default(), From 4676a398aa54a5d5f561f78064acfb4a6b012c69 Mon Sep 17 00:00:00 2001 From: lqd Date: Tue, 4 Aug 2020 19:31:15 +0200 Subject: [PATCH 07/15] augment tests to check the subset errors computed by the opt variant all 3 types of errors should always be the same between the naive and opt variants --- src/test.rs | 47 ++++++++++++++++++++++++++++++++++++++++------- src/test_util.rs | 20 +++++++++++++++++++- 2 files changed, 59 insertions(+), 8 deletions(-) diff --git a/src/test.rs b/src/test.rs index b336c3a548..efbc4af293 100644 --- a/src/test.rs +++ b/src/test.rs @@ -5,7 +5,10 @@ use crate::facts::{AllFacts, Loan, Origin, Point}; use crate::intern; use crate::program::parse_from_program; use crate::tab_delim; -use crate::test_util::{assert_equal, location_insensitive_checker_for, naive_checker_for}; +use crate::test_util::{ + assert_checkers_match, assert_equal, assert_outputs_match, location_insensitive_checker_for, + naive_checker_for, opt_checker_for, +}; use polonius_engine::Algorithm; use rustc_hash::FxHashMap; use std::error::Error; @@ -77,11 +80,15 @@ fn test_facts(all_facts: &AllFacts, algorithms: &[Algorithm]) { // 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); } // 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); } fn test_fn(dir_name: &str, fn_name: &str, algorithm: Algorithm) -> Result<(), Box> { @@ -316,25 +323,30 @@ fn smoke_test_errors() { let facts = tab_delim::load_tab_delimited_facts(tables, &facts_dir).expect("facts"); let location_insensitive = Output::compute(&facts, Algorithm::LocationInsensitive, true); + let naive = Output::compute(&facts, Algorithm::Naive, true); + let opt = Output::compute(&facts, Algorithm::DatafrogOpt, true); + + // We have to find errors with every analysis assert!( !location_insensitive.errors.is_empty(), "LocationInsensitive didn't find errors for '{}'", test_fn ); - - let naive = Output::compute(&facts, Algorithm::Naive, true); assert!( !naive.errors.is_empty(), "Naive didn't find errors for '{}'", test_fn ); - - let opt = Output::compute(&facts, Algorithm::DatafrogOpt, true); assert!( !opt.errors.is_empty(), "DatafrogOpt didn't find errors for '{}'", test_fn ); + + // But not subset errors... + assert!(location_insensitive.subset_errors.is_empty()); + assert!(naive.subset_errors.is_empty()); + assert!(opt.subset_errors.is_empty()); } } @@ -584,7 +596,10 @@ fn illegal_subset_error() { // and in the location-insensitive results as well assert!(location_insensitive_checker_for(program) - .location_insensitive_subset_error_exists("'b", "'a",)); + .location_insensitive_subset_error_exists("'b", "'a")); + + // and finally the optimized-variant results should be the same as the naive ones + assert_checkers_match(&checker, &opt_checker_for(program)); } /// This is the same test as the `illegal_subset_error` one, but specifies the `'b: 'a` subset @@ -613,6 +628,7 @@ fn known_placeholder_origin_subset() { location_insensitive_checker_for(program).subset_errors_count(), 0 ); + assert_checkers_match(&checker, &opt_checker_for(program)); } /// This test ensures `known_subset`s are handled transitively: a known subset `'a: 'c` should be @@ -644,6 +660,7 @@ fn transitive_known_subset() { location_insensitive_checker_for(program).subset_errors_count(), 0 ); + assert_checkers_match(&checker, &opt_checker_for(program)); } /// Even if `'a: 'b` is known, `'a`'s placeholder loan can flow into `'b''s supersets, @@ -680,7 +697,10 @@ fn transitive_illegal_subset_error() { assert!(checker.subset_error_exists("'b", "'c", "\"Mid(B0[1])\"")); assert!(checker.subset_error_exists("'a", "'c", "\"Mid(B0[1])\"")); - // And similarly in the location-insensitive analysis. + // The optimized analysis results should be the same as the naive one's. + assert_checkers_match(&checker, &opt_checker_for(program)); + + // And the location-insensitive analysis should have the same errors, without a location. let mut checker = location_insensitive_checker_for(program); assert_eq!(checker.subset_errors_count(), 2); assert!(checker.location_insensitive_subset_error_exists("'b", "'c")); @@ -708,6 +728,10 @@ fn successes_in_subset_relations_dataset() { let insensitive = Output::compute(&facts, Algorithm::LocationInsensitive, true); assert!(insensitive.errors.is_empty()); assert!(insensitive.subset_errors.is_empty()); + + let opt = Output::compute(&facts, Algorithm::DatafrogOpt, true); + assert!(opt.errors.is_empty()); + assert!(opt.subset_errors.is_empty()); } } @@ -756,6 +780,10 @@ fn errors_in_subset_relations_dataset() { let insensitive_subset_errors = insensitive.subset_errors.values().next().unwrap(); assert_eq!(insensitive_subset_errors.len(), 1); assert!(insensitive_subset_errors.contains(&expected_subset_error)); + + // And the optimized analysis results should be the same as the naive one's. + let opt = Output::compute(&facts, Algorithm::Naive, true); + assert_outputs_match(&naive, &opt); } // There's only a single successful test in the dataset for now, but the structure of this test @@ -783,6 +811,11 @@ fn successes_in_move_errors_dataset() { assert!(insensitive.errors.is_empty()); assert!(insensitive.subset_errors.is_empty()); assert!(insensitive.move_errors.is_empty()); + + let opt = Output::compute(&facts, Algorithm::DatafrogOpt, true); + assert!(opt.errors.is_empty()); + assert!(opt.subset_errors.is_empty()); + assert!(opt.move_errors.is_empty()); } } diff --git a/src/test_util.rs b/src/test_util.rs index 39b39b4f25..f0f9c11e66 100644 --- a/src/test_util.rs +++ b/src/test_util.rs @@ -83,6 +83,20 @@ pub(crate) fn location_insensitive_checker_for(program: &str) -> FactChecker { check_program(program, Algorithm::LocationInsensitive, true) } +pub(crate) fn opt_checker_for(program: &str) -> FactChecker { + check_program(program, Algorithm::DatafrogOpt, true) +} + +pub(crate) fn assert_checkers_match(checker_a: &FactChecker, checker_b: &FactChecker) { + assert_outputs_match(&checker_a.output, &checker_b.output); +} + +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); +} + impl FactChecker { /// Asserts that there is a `subset_error` `origin1: origin2` at the specified `point`. pub fn subset_error_exists(&mut self, origin1: &str, origin2: &str, point: &str) -> bool { @@ -124,6 +138,10 @@ impl FactChecker { /// Note that this is different from checking `output.subset_errors.len()` as subset errors are /// grouped by the location where they are detected. pub fn subset_errors_count(&self) -> usize { - self.output.subset_errors.values().map(|origins| origins.len()).sum() + self.output + .subset_errors + .values() + .map(|origins| origins.len()) + .sum() } } From 2cbdf890711f2cfdfd56316d3735aea17734fe86 Mon Sep 17 00:00:00 2001 From: lqd Date: Tue, 4 Aug 2020 23:23:15 +0200 Subject: [PATCH 08/15] naive variant: alternate way of computing subset errors --- polonius-engine/src/output/mod.rs | 2 - polonius-engine/src/output/naive.rs | 75 ++++++++++++++++++----------- 2 files changed, 47 insertions(+), 30 deletions(-) diff --git a/polonius-engine/src/output/mod.rs b/polonius-engine/src/output/mod.rs index 1484464590..a587d1c5f7 100644 --- a/polonius-engine/src/output/mod.rs +++ b/polonius-engine/src/output/mod.rs @@ -126,7 +126,6 @@ struct Context<'ctx, T: FactTypes> { loan_issued_at: &'ctx Vec<(T::Origin, T::Loan, T::Point)>, // static inputs used by variants other than `LocationInsensitive` - cfg_node: &'ctx BTreeSet, loan_killed_at: Relation<(T::Loan, T::Point)>, known_contains: Relation<(T::Origin, T::Loan)>, placeholder_origin: Relation<(T::Origin, ())>, @@ -268,7 +267,6 @@ impl Output { origin_live_on_entry, loan_invalidated_at, cfg_edge, - cfg_node: &cfg_node, subset_base: &all_facts.subset_base, loan_issued_at: &all_facts.loan_issued_at, loan_killed_at, diff --git a/polonius-engine/src/output/naive.rs b/polonius-engine/src/output/naive.rs index 31156ee71a..ffa43a0769 100644 --- a/polonius-engine/src/output/naive.rs +++ b/polonius-engine/src/output/naive.rs @@ -29,11 +29,9 @@ pub(super) fn compute( // Static inputs let origin_live_on_entry_rel = &ctx.origin_live_on_entry; let cfg_edge_rel = &ctx.cfg_edge; - let cfg_node = ctx.cfg_node; let loan_killed_at = &ctx.loan_killed_at; - let known_contains = &ctx.known_contains; + let known_subset = &ctx.known_subset; let placeholder_origin = &ctx.placeholder_origin; - let placeholder_loan = &ctx.placeholder_loan; // Create a new iteration context, ... let mut iteration = Iteration::new(); @@ -65,6 +63,10 @@ pub(super) fn compute( let errors = iteration.variable("errors"); let subset_errors = iteration.variable::<(T::Origin, T::Origin, T::Point)>("subset_errors"); + let subset_placeholder = + iteration.variable::<(T::Origin, T::Origin, T::Point)>("subset_placeholder"); + let subset_placeholder_o2p = iteration.variable_indistinct("subset_placeholder_o2p"); + // load initial facts. subset.extend(ctx.subset_base.iter()); origin_contains_loan_on_entry.extend(ctx.loan_issued_at.iter()); @@ -79,20 +81,6 @@ pub(super) fn compute( .map(|&(origin, point)| ((origin, point), ())), ); - // Placeholder loans are contained by their placeholder origin at all points of the CFG. - // - // contains(Origin, Loan, Node) :- - // cfg_node(Node), - // placeholder(Origin, Loan). - let mut placeholder_loans = Vec::with_capacity(placeholder_loan.len() * cfg_node.len()); - for &(loan, origin) in placeholder_loan.iter() { - for &node in cfg_node.iter() { - placeholder_loans.push((origin, loan, node)); - } - } - - origin_contains_loan_on_entry.extend(placeholder_loans); - // .. and then start iterating rules! while iteration.changed() { // Cleanup step: remove symmetries @@ -109,6 +97,15 @@ pub(super) fn compute( .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) + }); + // remap fields to re-index by keys. subset_o1p.from_map(&subset, |&(origin1, origin2, point)| { ((origin1, point), origin2) @@ -196,23 +193,45 @@ pub(super) fn compute( |&(loan, point), _, _| (loan, point), ); + // subset_placeholder(Origin1, Origin2, Point) :- + // subset(Origin1, Origin2, Point), + // 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 + }), + ), + |&((origin1, point), origin2), _| (origin1, origin2, point), + ); + + // subset_placeholder(Origin1, Origin3, Point) :- + // subset_placeholder(Origin1, Origin2, Point), + // subset(Origin2, Origin3, Point). + subset_placeholder.from_join( + &subset_placeholder_o2p, + &subset_o1p, + |&(_origin2, point), &origin1, &origin3| (origin1, origin3, point), + ); + // subset_errors(Origin1, Origin2, Point) :- - // origin_contains_loan_on_entry(Origin2, Loan1, Point), - // placeholder(Origin2, _), - // placeholder(Origin1, Loan1), - // !known_contains(Origin2, Loan1). + // subset_placeholder(Origin1, Origin2, Point), + // placeholder_origin(Origin2), + // !known_subset(Origin1, Origin2). subset_errors.from_leapjoin( - &origin_contains_loan_on_entry, + &subset_placeholder, ( - placeholder_origin.filter_with(|&(origin2, _loan1, _point)| (origin2, ())), - placeholder_loan.extend_with(|&(_origin2, loan1, _point)| loan1), - known_contains.filter_anti(|&(origin2, loan1, _point)| (origin2, loan1)), + placeholder_origin.extend_with(|&(_origin1, origin2, _point)| origin2), + known_subset.filter_anti(|&(origin1, origin2, _point)| (origin1, origin2)), // remove symmetries: - datafrog::ValueFilter::from(|&(origin2, _loan1, _point), &origin1| { - origin2 != origin1 + datafrog::ValueFilter::from(|&(origin1, origin2, _point), _| { + origin1 != origin2 }), ), - |&(origin2, _loan1, point), &origin1| (origin1, origin2, point), + |&(origin1, origin2, point), _| (origin1, origin2, point), ); } From f4dbce89848999bfd52df906b9929511e0340ffe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Rakic?= Date: Mon, 21 Dec 2020 11:55:36 +0100 Subject: [PATCH 09/15] style: rename a variable and move code around --- polonius-engine/src/output/naive.rs | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/polonius-engine/src/output/naive.rs b/polonius-engine/src/output/naive.rs index ffa43a0769..cabaebf180 100644 --- a/polonius-engine/src/output/naive.rs +++ b/polonius-engine/src/output/naive.rs @@ -28,7 +28,7 @@ pub(super) fn compute( let (errors, subset_errors) = { // Static inputs let origin_live_on_entry_rel = &ctx.origin_live_on_entry; - let cfg_edge_rel = &ctx.cfg_edge; + let cfg_edge = &ctx.cfg_edge; let loan_killed_at = &ctx.loan_killed_at; let known_subset = &ctx.known_subset; let placeholder_origin = &ctx.placeholder_origin; @@ -59,14 +59,15 @@ pub(super) fn compute( let origin_live_on_entry_var = iteration.variable::<((T::Origin, T::Point), ())>("origin_live_on_entry"); - // 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"); - + // variable and index to compute the subsets of placeholders let subset_placeholder = iteration.variable::<(T::Origin, T::Origin, T::Point)>("subset_placeholder"); let subset_placeholder_o2p = iteration.variable_indistinct("subset_placeholder_o2p"); + // 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"); + // load initial facts. subset.extend(ctx.subset_base.iter()); origin_contains_loan_on_entry.extend(ctx.loan_issued_at.iter()); @@ -102,9 +103,6 @@ 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) - }); // remap fields to re-index by keys. subset_o1p.from_map(&subset, |&(origin1, origin2, point)| { @@ -114,6 +112,10 @@ pub(super) fn compute( ((origin2, point), origin1) }); + subset_placeholder_o2p.from_map(&subset_placeholder, |&(origin1, origin2, point)| { + ((origin2, point), origin1) + }); + origin_contains_loan_on_entry_op .from_map(&origin_contains_loan_on_entry, |&(origin, loan, point)| { ((origin, point), loan) @@ -140,7 +142,7 @@ pub(super) fn compute( subset.from_leapjoin( &subset, ( - cfg_edge_rel.extend_with(|&(_origin1, _origin2, point1)| point1), + 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), ), @@ -169,7 +171,7 @@ pub(super) fn compute( &origin_contains_loan_on_entry, ( loan_killed_at.filter_anti(|&(_origin, loan, point1)| (loan, point1)), - cfg_edge_rel.extend_with(|&(_origin, _loan, point1)| point1), + cfg_edge.extend_with(|&(_origin, _loan, point1)| point1), origin_live_on_entry_rel.extend_with(|&(origin, _loan, _point1)| origin), ), |&(origin, loan, _point1), &point2| (origin, loan, point2), From a998edd684dc6df1e92f29b07e7b9408b82fe1ea Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Rakic?= Date: Mon, 21 Dec 2020 16:09:03 +0100 Subject: [PATCH 10/15] naive: number and document the rules This will help readability, and documentation, when we extract the rules to the book. Also describes more precisely why we need a duplicate liveness relation. --- polonius-engine/src/output/naive.rs | 127 +++++++++++++++++++--------- 1 file changed, 85 insertions(+), 42 deletions(-) diff --git a/polonius-engine/src/output/naive.rs b/polonius-engine/src/output/naive.rs index cabaebf180..8acb2479df 100644 --- a/polonius-engine/src/output/naive.rs +++ b/polonius-engine/src/output/naive.rs @@ -45,6 +45,11 @@ pub(super) fn compute( // `loan_invalidated_at` facts, stored ready for joins let loan_invalidated_at = iteration.variable::<((T::Loan, T::Point), ())>("loan_invalidated_at"); + loan_invalidated_at.extend( + ctx.loan_invalidated_at + .iter() + .map(|&(loan, point)| ((loan, point), ())), + ); // different indices for `subset`. let subset_o1p = iteration.variable_indistinct("subset_o1p"); @@ -54,10 +59,32 @@ pub(super) fn compute( let origin_contains_loan_on_entry_op = iteration.variable_indistinct("origin_contains_loan_on_entry_op"); - // we need `origin_live_on_entry` in both variable and relation forms. - // (respectively, for the regular join and the leapjoin). + // 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), ())), + ); // variable and index to compute the subsets of placeholders let subset_placeholder = @@ -68,19 +95,19 @@ pub(super) fn compute( let errors = iteration.variable("errors"); let subset_errors = iteration.variable::<(T::Origin, T::Origin, T::Point)>("subset_errors"); - // load initial facts. + // load initial facts: + + // Rule 1: the initial subsets are the non-transitive `subset_base` static input. + // + // subset(Origin1, Origin2, Point) :- + // subset_base(Origin1, Origin2, Point). subset.extend(ctx.subset_base.iter()); + + // Rule 4: 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.extend(ctx.loan_issued_at.iter()); - 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), ())), - ); // .. and then start iterating rules! while iteration.changed() { @@ -104,7 +131,7 @@ pub(super) fn compute( .elements .retain(|&(origin1, origin2, _)| origin1 != origin2); - // remap fields to re-index by keys. + // 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) }); @@ -121,24 +148,26 @@ pub(super) fn compute( ((origin, point), loan) }); - // subset(origin1, origin2, point) :- - // subset_base(origin1, origin2, point). - // Already loaded; `subset_base` is static. + // Rule 1: done above, as part of the static input facts setup. - // subset(origin1, origin3, point) :- - // subset(origin1, origin2, point), - // subset(origin2, origin3, point). + // Rule 2: compute the subset transitive closure, at a given point. + // + // subset(Origin1, Origin3, Point) :- + // subset(Origin1, Origin2, Point), + // subset(Origin2, Origin3, Point). subset.from_join( &subset_o2p, &subset_o1p, |&(_origin2, point), &origin1, &origin3| (origin1, origin3, point), ); - // subset(origin1, origin2, point2) :- - // subset(origin1, origin2, point1), - // cfg_edge(point1, point2), - // origin_live_on_entry(origin1, point2), - // origin_live_on_entry(origin2, point2). + // Rule 3: propagate subsets along the CFG, according to liveness. + // + // subset(Origin1, Origin2, Point2) :- + // subset(Origin1, Origin2, Point1), + // cfg_edge(Point1, Point2), + // origin_live_on_entry(Origin1, Point2), + // origin_live_on_entry(Origin2, Point2). subset.from_leapjoin( &subset, ( @@ -149,24 +178,26 @@ pub(super) fn compute( |&(origin1, origin2, _point1), &point2| (origin1, origin2, point2), ); - // origin_contains_loan_on_entry(origin, loan, point) :- - // loan_issued_at(origin, loan, point). - // Already loaded; `loan_issued_at` is static. + // Rule 4: done above as part of the static input facts setup. - // origin_contains_loan_on_entry(origin2, loan, point) :- - // origin_contains_loan_on_entry(origin1, loan, point), - // subset(origin1, origin2, point). + // Rule 5: propagate loans within origins, at a given point, according to subsets. + // + // origin_contains_loan_on_entry(Origin2, Loan, Point) :- + // origin_contains_loan_on_entry(Origin1, Loan, Point), + // subset(Origin1, Origin2, Point). origin_contains_loan_on_entry.from_join( &origin_contains_loan_on_entry_op, &subset_o1p, |&(_origin1, point), &loan, &origin2| (origin2, loan, point), ); - // 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). + // Rule 6: propagate loans along the CFG, according to liveness. + // + // 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_contains_loan_on_entry.from_leapjoin( &origin_contains_loan_on_entry, ( @@ -177,24 +208,31 @@ pub(super) fn compute( |&(origin, loan, _point1), &point2| (origin, loan, point2), ); - // loan_live_at(loan, point) :- - // origin_contains_loan_on_entry(origin, loan, point), - // origin_live_on_entry(origin, point). + // 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. + // + // loan_live_at(Loan, Point) :- + // origin_contains_loan_on_entry(Origin, Loan, Point), + // origin_live_on_entry(Origin, Point). loan_live_at.from_join( &origin_contains_loan_on_entry_op, &origin_live_on_entry_var, |&(_origin, point), &loan, _| ((loan, point), ()), ); - // errors(loan, point) :- - // loan_invalidated_at(loan, point), - // loan_live_at(loan, point). + // Rule 8: 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). errors.from_join( &loan_invalidated_at, &loan_live_at, |&(loan, point), _, _| (loan, point), ); + // Rule 9: compute the subsets of the placeholder origins, at a given point. + // // subset_placeholder(Origin1, Origin2, Point) :- // subset(Origin1, Origin2, Point), // placeholder_origin(Origin1). @@ -210,6 +248,8 @@ pub(super) fn compute( |&((origin1, point), origin2), _| (origin1, origin2, point), ); + // Rule 10: compute the subset transitive closure of placeholder origins. + // // subset_placeholder(Origin1, Origin3, Point) :- // subset_placeholder(Origin1, Origin2, Point), // subset(Origin2, Origin3, Point). @@ -219,6 +259,9 @@ pub(super) fn compute( |&(_origin2, point), &origin1, &origin3| (origin1, origin3, point), ); + // Rule 11: 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), From d67fa2a1b7e7e34cc8fd7805b4e42a5544ab0c40 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Rakic?= Date: Mon, 21 Dec 2020 16:52:01 +0100 Subject: [PATCH 11/15] naive: the `loan_invalidated_at` relation does not need to be a variable --- polonius-engine/src/output/naive.rs | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/polonius-engine/src/output/naive.rs b/polonius-engine/src/output/naive.rs index 8acb2479df..65bea3777a 100644 --- a/polonius-engine/src/output/naive.rs +++ b/polonius-engine/src/output/naive.rs @@ -43,9 +43,7 @@ pub(super) fn compute( let loan_live_at = iteration.variable::<((T::Loan, T::Point), ())>("loan_live_at"); // `loan_invalidated_at` facts, stored ready for joins - let loan_invalidated_at = - iteration.variable::<((T::Loan, T::Point), ())>("loan_invalidated_at"); - loan_invalidated_at.extend( + let loan_invalidated_at = Relation::from_iter( ctx.loan_invalidated_at .iter() .map(|&(loan, point)| ((loan, point), ())), @@ -112,7 +110,7 @@ pub(super) fn compute( // .. and then start iterating rules! while iteration.changed() { // Cleanup step: remove symmetries - // - remove regions which are `subset`s of themselves + // - 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 @@ -222,12 +220,16 @@ pub(super) fn compute( // Rule 8: compute illegal access errors, i.e. an invalidation of a live loan. // + // Here again, this join acts as a pure filter and could be a more efficient leapjoin. + // However, similarly to the `origin_live_on_entry` example described above, the + // leapjoin with a single `filter_with` leaper would currently not be well-formed. + // // errors(Loan, Point) :- // 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), ); From a4731788f888094411753ff82dbb66ef9115286b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Rakic?= Date: Mon, 21 Dec 2020 17:59:20 +0100 Subject: [PATCH 12/15] naive: simplify subset errors computation Since we're already computing the full subset TC, adding a check for placeholder origins at the same time is simpler, and as a bonus, barely noticeable performance-wise (therefore, faster than tracking the placeholder subsets). --- polonius-engine/src/output/naive.rs | 58 ++++++----------------------- 1 file changed, 11 insertions(+), 47 deletions(-) diff --git a/polonius-engine/src/output/naive.rs b/polonius-engine/src/output/naive.rs index 65bea3777a..7bc345fc58 100644 --- a/polonius-engine/src/output/naive.rs +++ b/polonius-engine/src/output/naive.rs @@ -84,11 +84,6 @@ pub(super) fn compute( .map(|&(origin, point)| ((origin, point), ())), ); - // variable and index to compute the subsets of placeholders - let subset_placeholder = - iteration.variable::<(T::Origin, T::Origin, T::Point)>("subset_placeholder"); - let subset_placeholder_o2p = iteration.variable_indistinct("subset_placeholder_o2p"); - // 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"); @@ -123,12 +118,6 @@ pub(super) fn compute( .elements .retain(|&(origin1, origin2, _)| origin1 != origin2); - subset_placeholder - .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,10 +126,6 @@ pub(super) fn compute( ((origin2, point), origin1) }); - subset_placeholder_o2p.from_map(&subset_placeholder, |&(origin1, origin2, point)| { - ((origin2, point), origin1) - }); - origin_contains_loan_on_entry_op .from_map(&origin_contains_loan_on_entry, |&(origin, loan, point)| { ((origin, point), loan) @@ -223,6 +208,9 @@ pub(super) fn compute( // Here again, this join acts as a pure filter and could be a more efficient leapjoin. // However, similarly to the `origin_live_on_entry` example described above, the // leapjoin with a single `filter_with` leaper would currently not be well-formed. + // We don't explictly need to materialize `loan_live_at` either, and that doesn't + // change the well-formedness situation, so we still materialize it (since that also + // helps in testing). // // errors(Loan, Point) :- // loan_invalidated_at(Loan, Point), @@ -233,44 +221,20 @@ pub(super) fn compute( |&(loan, point), _, _| (loan, point), ); - // Rule 9: compute the subsets of the placeholder origins, at a given point. - // - // subset_placeholder(Origin1, Origin2, Point) :- - // subset(Origin1, Origin2, Point), - // 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 - }), - ), - |&((origin1, point), origin2), _| (origin1, origin2, point), - ); - - // Rule 10: compute the subset transitive closure of placeholder origins. - // - // subset_placeholder(Origin1, Origin3, Point) :- - // subset_placeholder(Origin1, Origin2, Point), - // subset(Origin2, Origin3, Point). - subset_placeholder.from_join( - &subset_placeholder_o2p, - &subset_o1p, - |&(_origin2, point), &origin1, &origin3| (origin1, origin3, point), - ); - - // Rule 11: compute illegal subset relations errors, i.e. the undeclared subsets + // Rule 9: compute illegal subset relations errors, i.e. the undeclared subsets // between two placeholder origins. + // 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_errors(Origin1, Origin2, Point) :- - // subset_placeholder(Origin1, Origin2, Point), + // subset_error(Origin1, Origin2, Point) :- + // subset(Origin1, Origin2, Point), + // placeholder_origin(Origin1), // placeholder_origin(Origin2), // !known_subset(Origin1, Origin2). subset_errors.from_leapjoin( - &subset_placeholder, + &subset, ( + placeholder_origin.extend_with(|&(origin1, _origin2, _point)| origin1), placeholder_origin.extend_with(|&(_origin1, origin2, _point)| origin2), known_subset.filter_anti(|&(origin1, origin2, _point)| (origin1, origin2)), // remove symmetries: From 965e7a430f3a52b6cd1a935465670d9971951b0d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Rakic?= Date: Mon, 21 Dec 2020 18:19:46 +0100 Subject: [PATCH 13/15] refactor: rename `known_subset` relation to `known_placeholder_subset` According to our finalized rules hackmd --- polonius-engine/src/facts.rs | 4 +- polonius-engine/src/output/datafrog_opt.rs | 7 ++- polonius-engine/src/output/mod.rs | 66 +++++++++++----------- polonius-engine/src/output/naive.rs | 7 ++- src/program.rs | 8 +-- src/tab_delim.rs | 2 +- src/test.rs | 10 ++-- 7 files changed, 53 insertions(+), 51 deletions(-) diff --git a/polonius-engine/src/facts.rs b/polonius-engine/src/facts.rs index 9e3b0770df..442ba186cc 100644 --- a/polonius-engine/src/facts.rs +++ b/polonius-engine/src/facts.rs @@ -82,7 +82,7 @@ pub struct AllFacts { /// - and one for the `'a: 'c` implied bound from the `x` parameter, /// (note that the transitive relation `'b: 'c` is not necessarily included /// explicitly, but rather inferred by polonius). - pub known_subset: Vec<(T::Origin, T::Origin)>, + pub known_placeholder_subset: Vec<(T::Origin, T::Origin)>, /// `placeholder(origin, loan)` describes a placeholder `origin`, with its associated /// placeholder `loan`. @@ -108,7 +108,7 @@ impl Default for AllFacts { path_assigned_at_base: Vec::default(), path_moved_at_base: Vec::default(), path_accessed_at_base: Vec::default(), - known_subset: Vec::default(), + known_placeholder_subset: Vec::default(), placeholder: Vec::default(), } } diff --git a/polonius-engine/src/output/datafrog_opt.rs b/polonius-engine/src/output/datafrog_opt.rs index 9cb29e021e..2be2836e0f 100644 --- a/polonius-engine/src/output/datafrog_opt.rs +++ b/polonius-engine/src/output/datafrog_opt.rs @@ -28,7 +28,7 @@ pub(super) fn compute( let origin_live_on_entry_rel = &ctx.origin_live_on_entry; let cfg_edge_rel = &ctx.cfg_edge; let loan_killed_at = &ctx.loan_killed_at; - let known_subset = &ctx.known_subset; + let known_placeholder_subset = &ctx.known_placeholder_subset; let placeholder_origin = &ctx.placeholder_origin; // Create a new iteration context, ... @@ -425,12 +425,13 @@ pub(super) fn compute( // subset_error(Origin1, Origin2, Point) :- // subset_placeholder(Origin1, Origin2, Point), // placeholder_origin(Origin2), - // !known_subset(Origin1, Origin2). + // !known_placeholder_subset(Origin1, Origin2). subset_errors.from_leapjoin( &subset_placeholder, ( placeholder_origin.extend_with(|&(_origin1, origin2, _point)| origin2), - known_subset.filter_anti(|&(origin1, origin2, _point)| (origin1, origin2)), + known_placeholder_subset + .filter_anti(|&(origin1, origin2, _point)| (origin1, origin2)), // remove symmetries: datafrog::ValueFilter::from(|&(origin1, origin2, _point), _| { origin1 != origin2 diff --git a/polonius-engine/src/output/mod.rs b/polonius-engine/src/output/mod.rs index a587d1c5f7..21b173fc39 100644 --- a/polonius-engine/src/output/mod.rs +++ b/polonius-engine/src/output/mod.rs @@ -131,13 +131,13 @@ struct Context<'ctx, T: FactTypes> { placeholder_origin: Relation<(T::Origin, ())>, placeholder_loan: Relation<(T::Loan, T::Origin)>, - // The `known_subset` relation in the facts does not necessarily contain all the transitive - // subsets. The transitive closure is always needed, so this version here is fully closed - // over. - known_subset: Relation<(T::Origin, T::Origin)>, + // The `known_placeholder_subset` relation in the facts does not necessarily contain all the + // transitive subsets. The transitive closure is always needed, so this version here is fully + // closed over. + known_placeholder_subset: Relation<(T::Origin, T::Origin)>, - // while this static input is unused by `LocationInsensitive`, it's depended on by initialization - // and liveness, so already computed by the time we get to borrowcking. + // while this static input is unused by `LocationInsensitive`, it's depended on by + // initialization and liveness, so already computed by the time we get to borrowcking. cfg_edge: Relation<(T::Point, T::Point)>, // Partial results possibly used by other variants as input @@ -236,17 +236,18 @@ impl Output { let loan_killed_at = all_facts.loan_killed_at.clone().into(); - // `known_subset` is a list of all the `'a: 'b` subset relations the user gave: + // `known_placeholder_subset` is a list of all the `'a: 'b` subset relations the user gave: // it's not required to be transitive. `known_contains` is its transitive closure: a list // of all the known placeholder loans that each of these placeholder origins contains. - // Given the `known_subset`s `'a: 'b` and `'b: 'c`: in the `known_contains` relation, `'a` - // will also contain `'c`'s placeholder loan. - let known_subset = all_facts.known_subset.clone().into(); + // Given the `known_placeholder_subset`s `'a: 'b` and `'b: 'c`: in the `known_contains` + // relation, `'a` will also contain `'c`'s placeholder loan. + let known_placeholder_subset = all_facts.known_placeholder_subset.clone().into(); let known_contains = - Output::::compute_known_contains(&known_subset, &all_facts.placeholder); + Output::::compute_known_contains(&known_placeholder_subset, &all_facts.placeholder); - // Fully close over the `known_subset` relation. - let known_subset = Output::::compute_known_subset(&known_subset); + // Fully close over the `known_placeholder_subset` relation. + let known_placeholder_subset = + Output::::compute_known_placeholder_subset(&known_placeholder_subset); let placeholder_origin: Relation<_> = Relation::from_iter( all_facts @@ -271,7 +272,7 @@ impl Output { loan_issued_at: &all_facts.loan_issued_at, loan_killed_at, known_contains, - known_subset, + known_placeholder_subset, placeholder_origin, placeholder_loan, potential_errors: None, @@ -392,10 +393,10 @@ impl Output { result } - /// Computes the transitive closure of the `known_subset` relation, so that we have + /// Computes the transitive closure of the `known_placeholder_subset` relation, so that we have /// the full list of placeholder loans contained by the placeholder origins. fn compute_known_contains( - known_subset: &Relation<(T::Origin, T::Origin)>, + known_placeholder_subset: &Relation<(T::Origin, T::Origin)>, placeholder: &[(T::Origin, T::Loan)], ) -> Relation<(T::Origin, T::Loan)> { let mut iteration = datafrog::Iteration::new(); @@ -408,10 +409,10 @@ impl Output { while iteration.changed() { // known_contains(Origin2, Loan1) :- // known_contains(Origin1, Loan1), - // known_subset(Origin1, Origin2). + // known_placeholder_subset(Origin1, Origin2). known_contains.from_join( &known_contains, - known_subset, + known_placeholder_subset, |&_origin1, &loan1, &origin2| (origin2, loan1), ); } @@ -419,32 +420,31 @@ impl Output { known_contains.complete() } - /// Computes the transitive closure of the `known_subset` relation. - fn compute_known_subset( - known_subset: &Relation<(T::Origin, T::Origin)>, + /// Computes the transitive closure of the `known_placeholder_subset` relation. + fn compute_known_placeholder_subset( + known_placeholder_subset_base: &Relation<(T::Origin, T::Origin)>, ) -> Relation<(T::Origin, T::Origin)> { use datafrog::{Iteration, RelationLeaper}; let mut iteration = Iteration::new(); - let known_subset_base = known_subset; - let known_subset = iteration.variable("known_subset"); + let known_placeholder_subset = iteration.variable("known_placeholder_subset"); - // known_subset(Origin1, Origin2) :- - // known_subset_base(Origin1, Origin2). - known_subset.extend(known_subset_base.iter()); + // known_placeholder_subset(Origin1, Origin2) :- + // known_placeholder_subset_base(Origin1, Origin2). + known_placeholder_subset.extend(known_placeholder_subset_base.iter()); while iteration.changed() { - // known_subset(Origin1, Origin3) :- - // known_subset(Origin1, Origin2), - // known_subset_base(Origin2, Origin3). - known_subset.from_leapjoin( - &known_subset, - known_subset_base.extend_with(|&(_origin1, origin2)| origin2), + // known_placeholder_subset(Origin1, Origin3) :- + // known_placeholder_subset(Origin1, Origin2), + // known_placeholder_subset_base(Origin2, Origin3). + known_placeholder_subset.from_leapjoin( + &known_placeholder_subset, + known_placeholder_subset_base.extend_with(|&(_origin1, origin2)| origin2), |&(origin1, _origin2), &origin3| (origin1, origin3), ); } - known_subset.complete() + known_placeholder_subset.complete() } fn new(dump_enabled: bool) -> Self { diff --git a/polonius-engine/src/output/naive.rs b/polonius-engine/src/output/naive.rs index 7bc345fc58..aa42048673 100644 --- a/polonius-engine/src/output/naive.rs +++ b/polonius-engine/src/output/naive.rs @@ -30,7 +30,7 @@ pub(super) fn compute( let origin_live_on_entry_rel = &ctx.origin_live_on_entry; let cfg_edge = &ctx.cfg_edge; let loan_killed_at = &ctx.loan_killed_at; - let known_subset = &ctx.known_subset; + let known_placeholder_subset = &ctx.known_placeholder_subset; let placeholder_origin = &ctx.placeholder_origin; // Create a new iteration context, ... @@ -230,13 +230,14 @@ pub(super) fn compute( // subset(Origin1, Origin2, Point), // placeholder_origin(Origin1), // placeholder_origin(Origin2), - // !known_subset(Origin1, Origin2). + // !known_placeholder_subset(Origin1, Origin2). subset_errors.from_leapjoin( &subset, ( placeholder_origin.extend_with(|&(origin1, _origin2, _point)| origin1), placeholder_origin.extend_with(|&(_origin1, origin2, _point)| origin2), - known_subset.filter_anti(|&(origin1, origin2, _point)| (origin1, origin2)), + known_placeholder_subset + .filter_anti(|&(origin1, origin2, _point)| (origin1, origin2)), // remove symmetries: datafrog::ValueFilter::from(|&(origin1, origin2, _point), _| { origin1 != origin2 diff --git a/src/program.rs b/src/program.rs index 53e8b5a704..8e0de05978 100644 --- a/src/program.rs +++ b/src/program.rs @@ -19,7 +19,7 @@ struct Facts { loan_killed_at: BTreeSet<(Loan, Point)>, subset_base: BTreeSet<(Origin, Origin, Point)>, loan_invalidated_at: BTreeSet<(Point, Loan)>, - known_subset: BTreeSet<(Origin, Origin)>, + known_placeholder_subset: BTreeSet<(Origin, Origin)>, placeholder: BTreeSet<(Origin, Loan)>, var_defined_at: BTreeSet<(Variable, Point)>, var_used_at: BTreeSet<(Variable, Point)>, @@ -52,7 +52,7 @@ impl From for AllFacts { path_assigned_at_base: facts.path_assigned_at_base.into_iter().collect(), path_moved_at_base: facts.path_moved_at_base.into_iter().collect(), path_accessed_at_base: facts.path_accessed_at_base.into_iter().collect(), - known_subset: facts.known_subset.into_iter().collect(), + known_placeholder_subset: facts.known_placeholder_subset.into_iter().collect(), placeholder: facts.placeholder.into_iter().collect(), } } @@ -113,8 +113,8 @@ pub(crate) fn parse_from_program( }), ); - // facts: known_subset(Origin, Origin) - facts.known_subset.extend( + // facts: known_placeholder_subset(Origin, Origin) + facts.known_placeholder_subset.extend( input .known_subsets .iter() diff --git a/src/tab_delim.rs b/src/tab_delim.rs index 91bb0e2ebc..be8f3e9718 100644 --- a/src/tab_delim.rs +++ b/src/tab_delim.rs @@ -49,7 +49,7 @@ pub(crate) fn load_tab_delimited_facts( path_assigned_at_base, path_moved_at_base, path_accessed_at_base, - known_subset, + known_placeholder_subset, placeholder, } } diff --git a/src/test.rs b/src/test.rs index efbc4af293..30d94bdf34 100644 --- a/src/test.rs +++ b/src/test.rs @@ -588,7 +588,7 @@ fn illegal_subset_error() { assert_eq!(checker.facts.placeholder.len(), 2); // no known subsets are defined in the program... - assert_eq!(checker.facts.known_subset.len(), 0); + assert_eq!(checker.facts.known_placeholder_subset.len(), 0); // ...so there should be an error here about the missing `'b: 'a` subset assert_eq!(checker.subset_errors_count(), 1); @@ -621,7 +621,7 @@ fn known_placeholder_origin_subset() { assert_eq!(checker.facts.universal_region.len(), 2); assert_eq!(checker.facts.placeholder.len(), 2); - assert_eq!(checker.facts.known_subset.len(), 1); + assert_eq!(checker.facts.known_placeholder_subset.len(), 1); assert_eq!(checker.subset_errors_count(), 0); assert_eq!( @@ -651,8 +651,8 @@ fn transitive_known_subset() { assert_eq!(checker.facts.universal_region.len(), 3); assert_eq!(checker.facts.placeholder.len(), 3); - // the 2 `known_subset`s here mean 3 `known_contains`, transitively - assert_eq!(checker.facts.known_subset.len(), 2); + // the 2 `known_placeholder_subset`s here mean 3 `known_contains`, transitively + assert_eq!(checker.facts.known_placeholder_subset.len(), 2); assert_eq!(checker.output.known_contains.len(), 3); assert_eq!(checker.subset_errors_count(), 0); @@ -690,7 +690,7 @@ fn transitive_illegal_subset_error() { assert_eq!(checker.facts.universal_region.len(), 3); assert_eq!(checker.facts.placeholder.len(), 3); - assert_eq!(checker.facts.known_subset.len(), 1); + assert_eq!(checker.facts.known_placeholder_subset.len(), 1); // There should be 2 errors here about the missing `'b: 'c` and `'a: 'c` subsets. assert_eq!(checker.subset_errors_count(), 2); From b1a339e77f8ec110e430b989b67b8cdc85666031 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Rakic?= Date: Mon, 21 Dec 2020 18:20:16 +0100 Subject: [PATCH 14/15] tests: rename `known_subset.facts` input file to `known_placeholder_subset.facts` --- .../{known_subset.facts => known_placeholder_subset.facts} | 0 .../main/{known_subset.facts => known_placeholder_subset.facts} | 0 .../{known_subset.facts => known_placeholder_subset.facts} | 0 .../{known_subset.facts => known_placeholder_subset.facts} | 0 .../{known_subset.facts => known_placeholder_subset.facts} | 0 .../foo/{known_subset.facts => known_placeholder_subset.facts} | 0 .../main/{known_subset.facts => known_placeholder_subset.facts} | 0 .../{known_subset.facts => known_placeholder_subset.facts} | 0 .../{known_subset.facts => known_placeholder_subset.facts} | 0 .../random/{known_subset.facts => known_placeholder_subset.facts} | 0 .../{known_subset.facts => known_placeholder_subset.facts} | 0 .../{known_subset.facts => known_placeholder_subset.facts} | 0 .../{known_subset.facts => known_placeholder_subset.facts} | 0 .../{known_subset.facts => known_placeholder_subset.facts} | 0 .../{known_subset.facts => known_placeholder_subset.facts} | 0 .../{known_subset.facts => known_placeholder_subset.facts} | 0 .../{known_subset.facts => known_placeholder_subset.facts} | 0 .../foo1/{known_subset.facts => known_placeholder_subset.facts} | 0 .../foo2/{known_subset.facts => known_placeholder_subset.facts} | 0 .../foo3/{known_subset.facts => known_placeholder_subset.facts} | 0 .../main/{known_subset.facts => known_placeholder_subset.facts} | 0 .../{known_subset.facts => known_placeholder_subset.facts} | 0 22 files changed, 0 insertions(+), 0 deletions(-) rename inputs/clap-rs/app-parser-{{impl}}-add_defaults/{known_subset.facts => known_placeholder_subset.facts} (100%) rename inputs/issue-47680/nll-facts/main/{known_subset.facts => known_placeholder_subset.facts} (100%) rename inputs/issue-47680/nll-facts/{{impl}}-maybe_next/{known_subset.facts => known_placeholder_subset.facts} (100%) rename inputs/smoke-test/nll-facts/basic_move_error/{known_subset.facts => known_placeholder_subset.facts} (100%) rename inputs/smoke-test/nll-facts/conditional_init/{known_subset.facts => known_placeholder_subset.facts} (100%) rename inputs/smoke-test/nll-facts/foo/{known_subset.facts => known_placeholder_subset.facts} (100%) rename inputs/smoke-test/nll-facts/main/{known_subset.facts => known_placeholder_subset.facts} (100%) rename inputs/smoke-test/nll-facts/move_reinitialize_ok/{known_subset.facts => known_placeholder_subset.facts} (100%) rename inputs/smoke-test/nll-facts/position_dependent_outlives/{known_subset.facts => known_placeholder_subset.facts} (100%) rename inputs/smoke-test/nll-facts/random/{known_subset.facts => known_placeholder_subset.facts} (100%) rename inputs/smoke-test/nll-facts/return_ref_to_local/{known_subset.facts => known_placeholder_subset.facts} (100%) rename inputs/smoke-test/nll-facts/use_while_mut/{known_subset.facts => known_placeholder_subset.facts} (100%) rename inputs/smoke-test/nll-facts/use_while_mut_fr/{known_subset.facts => known_placeholder_subset.facts} (100%) rename inputs/smoke-test/nll-facts/well_formed_function_inputs/{known_subset.facts => known_placeholder_subset.facts} (100%) rename inputs/subset-relations/nll-facts/implied_bounds_subset/{known_subset.facts => known_placeholder_subset.facts} (100%) rename inputs/subset-relations/nll-facts/missing_subset/{known_subset.facts => known_placeholder_subset.facts} (100%) rename inputs/subset-relations/nll-facts/valid_subset/{known_subset.facts => known_placeholder_subset.facts} (100%) rename inputs/vec-push-ref/nll-facts/foo1/{known_subset.facts => known_placeholder_subset.facts} (100%) rename inputs/vec-push-ref/nll-facts/foo2/{known_subset.facts => known_placeholder_subset.facts} (100%) rename inputs/vec-push-ref/nll-facts/foo3/{known_subset.facts => known_placeholder_subset.facts} (100%) rename inputs/vec-push-ref/nll-facts/main/{known_subset.facts => known_placeholder_subset.facts} (100%) rename inputs/vec-push-ref/nll-facts/something/{known_subset.facts => known_placeholder_subset.facts} (100%) diff --git a/inputs/clap-rs/app-parser-{{impl}}-add_defaults/known_subset.facts b/inputs/clap-rs/app-parser-{{impl}}-add_defaults/known_placeholder_subset.facts similarity index 100% rename from inputs/clap-rs/app-parser-{{impl}}-add_defaults/known_subset.facts rename to inputs/clap-rs/app-parser-{{impl}}-add_defaults/known_placeholder_subset.facts diff --git a/inputs/issue-47680/nll-facts/main/known_subset.facts b/inputs/issue-47680/nll-facts/main/known_placeholder_subset.facts similarity index 100% rename from inputs/issue-47680/nll-facts/main/known_subset.facts rename to inputs/issue-47680/nll-facts/main/known_placeholder_subset.facts diff --git a/inputs/issue-47680/nll-facts/{{impl}}-maybe_next/known_subset.facts b/inputs/issue-47680/nll-facts/{{impl}}-maybe_next/known_placeholder_subset.facts similarity index 100% rename from inputs/issue-47680/nll-facts/{{impl}}-maybe_next/known_subset.facts rename to inputs/issue-47680/nll-facts/{{impl}}-maybe_next/known_placeholder_subset.facts diff --git a/inputs/smoke-test/nll-facts/basic_move_error/known_subset.facts b/inputs/smoke-test/nll-facts/basic_move_error/known_placeholder_subset.facts similarity index 100% rename from inputs/smoke-test/nll-facts/basic_move_error/known_subset.facts rename to inputs/smoke-test/nll-facts/basic_move_error/known_placeholder_subset.facts diff --git a/inputs/smoke-test/nll-facts/conditional_init/known_subset.facts b/inputs/smoke-test/nll-facts/conditional_init/known_placeholder_subset.facts similarity index 100% rename from inputs/smoke-test/nll-facts/conditional_init/known_subset.facts rename to inputs/smoke-test/nll-facts/conditional_init/known_placeholder_subset.facts diff --git a/inputs/smoke-test/nll-facts/foo/known_subset.facts b/inputs/smoke-test/nll-facts/foo/known_placeholder_subset.facts similarity index 100% rename from inputs/smoke-test/nll-facts/foo/known_subset.facts rename to inputs/smoke-test/nll-facts/foo/known_placeholder_subset.facts diff --git a/inputs/smoke-test/nll-facts/main/known_subset.facts b/inputs/smoke-test/nll-facts/main/known_placeholder_subset.facts similarity index 100% rename from inputs/smoke-test/nll-facts/main/known_subset.facts rename to inputs/smoke-test/nll-facts/main/known_placeholder_subset.facts diff --git a/inputs/smoke-test/nll-facts/move_reinitialize_ok/known_subset.facts b/inputs/smoke-test/nll-facts/move_reinitialize_ok/known_placeholder_subset.facts similarity index 100% rename from inputs/smoke-test/nll-facts/move_reinitialize_ok/known_subset.facts rename to inputs/smoke-test/nll-facts/move_reinitialize_ok/known_placeholder_subset.facts diff --git a/inputs/smoke-test/nll-facts/position_dependent_outlives/known_subset.facts b/inputs/smoke-test/nll-facts/position_dependent_outlives/known_placeholder_subset.facts similarity index 100% rename from inputs/smoke-test/nll-facts/position_dependent_outlives/known_subset.facts rename to inputs/smoke-test/nll-facts/position_dependent_outlives/known_placeholder_subset.facts diff --git a/inputs/smoke-test/nll-facts/random/known_subset.facts b/inputs/smoke-test/nll-facts/random/known_placeholder_subset.facts similarity index 100% rename from inputs/smoke-test/nll-facts/random/known_subset.facts rename to inputs/smoke-test/nll-facts/random/known_placeholder_subset.facts diff --git a/inputs/smoke-test/nll-facts/return_ref_to_local/known_subset.facts b/inputs/smoke-test/nll-facts/return_ref_to_local/known_placeholder_subset.facts similarity index 100% rename from inputs/smoke-test/nll-facts/return_ref_to_local/known_subset.facts rename to inputs/smoke-test/nll-facts/return_ref_to_local/known_placeholder_subset.facts diff --git a/inputs/smoke-test/nll-facts/use_while_mut/known_subset.facts b/inputs/smoke-test/nll-facts/use_while_mut/known_placeholder_subset.facts similarity index 100% rename from inputs/smoke-test/nll-facts/use_while_mut/known_subset.facts rename to inputs/smoke-test/nll-facts/use_while_mut/known_placeholder_subset.facts diff --git a/inputs/smoke-test/nll-facts/use_while_mut_fr/known_subset.facts b/inputs/smoke-test/nll-facts/use_while_mut_fr/known_placeholder_subset.facts similarity index 100% rename from inputs/smoke-test/nll-facts/use_while_mut_fr/known_subset.facts rename to inputs/smoke-test/nll-facts/use_while_mut_fr/known_placeholder_subset.facts diff --git a/inputs/smoke-test/nll-facts/well_formed_function_inputs/known_subset.facts b/inputs/smoke-test/nll-facts/well_formed_function_inputs/known_placeholder_subset.facts similarity index 100% rename from inputs/smoke-test/nll-facts/well_formed_function_inputs/known_subset.facts rename to inputs/smoke-test/nll-facts/well_formed_function_inputs/known_placeholder_subset.facts diff --git a/inputs/subset-relations/nll-facts/implied_bounds_subset/known_subset.facts b/inputs/subset-relations/nll-facts/implied_bounds_subset/known_placeholder_subset.facts similarity index 100% rename from inputs/subset-relations/nll-facts/implied_bounds_subset/known_subset.facts rename to inputs/subset-relations/nll-facts/implied_bounds_subset/known_placeholder_subset.facts diff --git a/inputs/subset-relations/nll-facts/missing_subset/known_subset.facts b/inputs/subset-relations/nll-facts/missing_subset/known_placeholder_subset.facts similarity index 100% rename from inputs/subset-relations/nll-facts/missing_subset/known_subset.facts rename to inputs/subset-relations/nll-facts/missing_subset/known_placeholder_subset.facts diff --git a/inputs/subset-relations/nll-facts/valid_subset/known_subset.facts b/inputs/subset-relations/nll-facts/valid_subset/known_placeholder_subset.facts similarity index 100% rename from inputs/subset-relations/nll-facts/valid_subset/known_subset.facts rename to inputs/subset-relations/nll-facts/valid_subset/known_placeholder_subset.facts diff --git a/inputs/vec-push-ref/nll-facts/foo1/known_subset.facts b/inputs/vec-push-ref/nll-facts/foo1/known_placeholder_subset.facts similarity index 100% rename from inputs/vec-push-ref/nll-facts/foo1/known_subset.facts rename to inputs/vec-push-ref/nll-facts/foo1/known_placeholder_subset.facts diff --git a/inputs/vec-push-ref/nll-facts/foo2/known_subset.facts b/inputs/vec-push-ref/nll-facts/foo2/known_placeholder_subset.facts similarity index 100% rename from inputs/vec-push-ref/nll-facts/foo2/known_subset.facts rename to inputs/vec-push-ref/nll-facts/foo2/known_placeholder_subset.facts diff --git a/inputs/vec-push-ref/nll-facts/foo3/known_subset.facts b/inputs/vec-push-ref/nll-facts/foo3/known_placeholder_subset.facts similarity index 100% rename from inputs/vec-push-ref/nll-facts/foo3/known_subset.facts rename to inputs/vec-push-ref/nll-facts/foo3/known_placeholder_subset.facts diff --git a/inputs/vec-push-ref/nll-facts/main/known_subset.facts b/inputs/vec-push-ref/nll-facts/main/known_placeholder_subset.facts similarity index 100% rename from inputs/vec-push-ref/nll-facts/main/known_subset.facts rename to inputs/vec-push-ref/nll-facts/main/known_placeholder_subset.facts diff --git a/inputs/vec-push-ref/nll-facts/something/known_subset.facts b/inputs/vec-push-ref/nll-facts/something/known_placeholder_subset.facts similarity index 100% rename from inputs/vec-push-ref/nll-facts/something/known_subset.facts rename to inputs/vec-push-ref/nll-facts/something/known_placeholder_subset.facts From 594c7df887d7f1e480880b1ebac7402f3c196b95 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Rakic?= Date: Fri, 30 Jul 2021 18:08:58 +0200 Subject: [PATCH 15/15] document the invariant in the `subset_placeholder` TC --- polonius-engine/src/output/datafrog_opt.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/polonius-engine/src/output/datafrog_opt.rs b/polonius-engine/src/output/datafrog_opt.rs index 2be2836e0f..da9c343ccd 100644 --- a/polonius-engine/src/output/datafrog_opt.rs +++ b/polonius-engine/src/output/datafrog_opt.rs @@ -413,6 +413,9 @@ 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. + // // subset_placeholder(Origin1, Origin3, Point) :- // subset_placeholder(Origin1, Origin2, Point), // subset(Origin2, Origin3, Point).