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 diff --git a/polonius-engine/src/facts.rs b/polonius-engine/src/facts.rs index 9e3b0770dff..442ba186cc6 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 564696c3041..da9c343ccd9 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_placeholder_subset = &ctx.known_placeholder_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,51 @@ 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), + ); + + // 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). + 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_placeholder_subset(Origin1, Origin2). + subset_errors.from_leapjoin( + &subset_placeholder, + ( + placeholder_origin.extend_with(|&(_origin1, origin2, _point)| origin2), + known_placeholder_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 +481,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/location_insensitive.rs b/polonius-engine/src/output/location_insensitive.rs index 8a975f8575a..83ce27757de 100644 --- a/polonius-engine/src/output/location_insensitive.rs +++ b/polonius-engine/src/output/location_insensitive.rs @@ -17,47 +17,62 @@ 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; + + // 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"); 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. - // subset(origin1, origin2) :- - // subset_base(origin1, origin2, _point). - subset.extend( - ctx.subset_base + // origin_contains_loan_on_entry(Origin, Loan) :- + // loan_issued_at(Origin, Loan, _). + origin_contains_loan_on_entry.extend( + ctx.loan_issued_at .iter() - .map(|&(origin1, origin2, _point)| (origin1, origin2)), + .map(|&(origin, loan, _point)| (origin, loan)), ); - // origin_contains_loan_on_entry(origin, loan) :- - // loan_issued_at(origin, loan, _point). + // origin_contains_loan_on_entry(Origin, Loan) :- + // placeholder_loan(Origin, Loan). origin_contains_loan_on_entry.extend( - ctx.loan_issued_at + placeholder_loan .iter() - .map(|&(origin, loan, _point)| (origin, loan)), + .map(|&(loan, origin)| (origin, loan)), ); // .. 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`. @@ -67,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. @@ -86,10 +101,26 @@ 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 { - let subset = subset.complete(); for &(origin1, origin2) in subset.iter() { result .subset_anywhere @@ -108,14 +139,18 @@ pub(super) fn compute( } } - potential_errors.complete() + ( + potential_errors.complete(), + potential_subset_errors.complete(), + ) }; info!( - "potential_errors is complete: {} tuples, {:?}", + "analysis done: {} `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 610bf7d1d75..21b173fc390 100644 --- a/polonius-engine/src/output/mod.rs +++ b/polonius-engine/src/output/mod.rs @@ -126,18 +126,23 @@ 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, ())>, placeholder_loan: Relation<(T::Loan, 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. + // 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. cfg_edge: Relation<(T::Point, T::Point)>, // Partial results possibly used by other variants as input potential_errors: Option>, + potential_subset_errors: Option>, } impl Output { @@ -231,14 +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_placeholder_subset` relation. + let known_placeholder_subset = + Output::::compute_known_placeholder_subset(&known_placeholder_subset); let placeholder_origin: Relation<_> = Relation::from_iter( all_facts @@ -259,57 +268,62 @@ 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, known_contains, + known_placeholder_subset, placeholder_origin, placeholder_loan, potential_errors: None, + potential_subset_errors: None, }; - let errors = match algorithm { - Algorithm::LocationInsensitive => location_insensitive::compute(&ctx, &mut result), - 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 (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 debugging, the `Hybrid` variant will + // take advantage of its result. + 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 => { - // 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() { - potential_errors + let (potential_errors, potential_subset_errors) = + location_insensitive::compute(&ctx, &mut result); + + if potential_errors.is_empty() && potential_subset_errors.is_empty() { + // 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. 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) } } 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 ? @@ -339,7 +353,7 @@ impl Output { debug!("Naive and optimized algorithms reported the same errors."); } - naive_errors + (naive_errors, naive_subset_errors) } }; @@ -348,6 +362,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() { @@ -370,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(); @@ -386,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), ); } @@ -397,6 +420,33 @@ impl Output { known_contains.complete() } + /// 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_placeholder_subset = iteration.variable("known_placeholder_subset"); + + // known_placeholder_subset(Origin1, Origin2) :- + // known_placeholder_subset_base(Origin1, Origin2). + known_placeholder_subset.extend(known_placeholder_subset_base.iter()); + + while iteration.changed() { + // 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_placeholder_subset.complete() + } + fn new(dump_enabled: bool) -> Self { Output { errors: FxHashMap::default(), diff --git a/polonius-engine/src/output/naive.rs b/polonius-engine/src/output/naive.rs index 31156ee71a4..aa42048673d 100644 --- a/polonius-engine/src/output/naive.rs +++ b/polonius-engine/src/output/naive.rs @@ -28,12 +28,10 @@ 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_node = ctx.cfg_node; + let cfg_edge = &ctx.cfg_edge; let loan_killed_at = &ctx.loan_killed_at; - let known_contains = &ctx.known_contains; + let known_placeholder_subset = &ctx.known_placeholder_subset; let placeholder_origin = &ctx.placeholder_origin; - let placeholder_loan = &ctx.placeholder_loan; // Create a new iteration context, ... let mut iteration = Iteration::new(); @@ -45,8 +43,11 @@ 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"); + let loan_invalidated_at = Relation::from_iter( + ctx.loan_invalidated_at + .iter() + .map(|&(loan, point)| ((loan, point), ())), + ); // different indices for `subset`. let subset_o1p = iteration.variable_indistinct("subset_o1p"); @@ -56,47 +57,55 @@ 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"); - - // 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()); - 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), ())), ); - // Placeholder loans are contained by their placeholder origin at all points of the CFG. + // 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: + + // Rule 1: the initial subsets are the non-transitive `subset_base` static input. // - // 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)); - } - } + // subset(Origin1, Origin2, Point) :- + // subset_base(Origin1, Origin2, Point). + subset.extend(ctx.subset_base.iter()); - origin_contains_loan_on_entry.extend(placeholder_loans); + // 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()); // .. 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 @@ -109,7 +118,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) }); @@ -122,97 +131,119 @@ 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, ( - 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), ), |&(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, ( 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), ); - // 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. + // + // 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), + // loan_live_at(Loan, Point). errors.from_join( - &loan_invalidated_at, &loan_live_at, + &loan_invalidated_at, |&(loan, point), _, _| (loan, point), ); - // subset_errors(Origin1, Origin2, Point) :- - // origin_contains_loan_on_entry(Origin2, Loan1, Point), - // placeholder(Origin2, _), - // placeholder(Origin1, Loan1), - // !known_contains(Origin2, Loan1). + // 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_error(Origin1, Origin2, Point) :- + // subset(Origin1, Origin2, Point), + // placeholder_origin(Origin1), + // placeholder_origin(Origin2), + // !known_placeholder_subset(Origin1, Origin2). subset_errors.from_leapjoin( - &origin_contains_loan_on_entry, + &subset, ( - 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)| origin1), + placeholder_origin.extend_with(|&(_origin1, origin2, _point)| origin2), + known_placeholder_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), ); } diff --git a/src/program.rs b/src/program.rs index 53e8b5a704e..8e0de05978f 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 91bb0e2ebc3..be8f3e9718f 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 cc2224ae086..30d94bdf34e 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, check_program}; +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; @@ -42,6 +45,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); @@ -49,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> { @@ -288,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()); } } @@ -542,17 +582,24 @@ 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); // 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); 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")); + + // 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 @@ -570,13 +617,18 @@ 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.facts.known_placeholder_subset.len(), 1); assert_eq!(checker.subset_errors_count(), 0); + assert_eq!( + 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 @@ -594,16 +646,21 @@ 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); - // 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); + assert_eq!( + 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, @@ -619,22 +676,35 @@ 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); + assert_eq!(checker.facts.known_placeholder_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])\"")); + + // 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")); + assert!(checker.location_insensitive_subset_error_exists("'a", "'c")); } #[test] @@ -651,9 +721,17 @@ 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()); + + let opt = Output::compute(&facts, Algorithm::DatafrogOpt, true); + assert!(opt.errors.is_empty()); + assert!(opt.subset_errors.is_empty()); } } @@ -668,25 +746,44 @@ 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)); + + // 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 @@ -705,10 +802,20 @@ 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()); + + 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 b0a90886967..f0f9c11e660 100644 --- a/src/test_util.rs +++ b/src/test_util.rs @@ -75,6 +75,28 @@ 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) +} + +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 { @@ -90,7 +112,36 @@ 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() } }