Compute subset errors everywhere

polonius-engine/src/facts.rs

@@ -82,7 +82,7 @@ pub struct AllFacts<T: FactTypes> {
     /// - 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<T: FactTypes> Default for AllFacts<T> {
             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(),
         }
     }

polonius-engine/src/output/datafrog_opt.rs

@@ -17,14 +17,19 @@ use crate::output::{Context, Output};
 pub(super) fn compute<T: FactTypes>(
     ctx: &Context<'_, T>,
     result: &mut Output<T>,
-) -> 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<T: FactTypes>(
 
         // .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<T: FactTypes>(
                 .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<T: FactTypes>(
                 &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<T: FactTypes>(
             }
         }
 
-        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)
 }

polonius-engine/src/output/location_insensitive.rs

@@ -17,47 +17,62 @@ use crate::output::{Context, Output};
 pub(super) fn compute<T: FactTypes>(
     ctx: &Context<'_, T>,
     result: &mut Output<T>,
-) -> 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<T: FactTypes>(
                 |&_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<T: FactTypes>(
                 ),
                 |&(_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<T: FactTypes>(
             }
         }
 
-        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)
 }