refactor: rename known_subset relation to known_placeholder_subset

According to our finalized rules hackmd

Author: lqd

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

@@ -28,7 +28,7 @@ pub(super) fn compute<T: FactTypes>(
         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<T: FactTypes>(
             // 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

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<T: FactTypes> Output<T> {
 
         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::<T>::compute_known_contains(&known_subset, &all_facts.placeholder);
+            Output::<T>::compute_known_contains(&known_placeholder_subset, &all_facts.placeholder);
 
-        // Fully close over the `known_subset` relation.
-        let known_subset = Output::<T>::compute_known_subset(&known_subset);
+        // Fully close over the `known_placeholder_subset` relation.
+        let known_placeholder_subset =
+            Output::<T>::compute_known_placeholder_subset(&known_placeholder_subset);
 
         let placeholder_origin: Relation<_> = Relation::from_iter(
             all_facts
@@ -271,7 +272,7 @@ impl<T: FactTypes> Output<T> {
             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<T: FactTypes> Output<T> {
         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,43 +409,42 @@ impl<T: FactTypes> Output<T> {
         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),
             );
         }
 
         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 {

polonius-engine/src/output/naive.rs

@@ -30,7 +30,7 @@ pub(super) fn compute<T: FactTypes>(
         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<T: FactTypes>(
             //   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

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<Facts> 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()

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,
         }
     }

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);