Merge pull request #134 from lqd/its_all_contextual

Proposal: split `AllFacts` into contexts dedicated to each component of the pipeline

polonius-engine/src/output/datafrog_opt.rs

@@ -8,62 +8,32 @@
 // option. This file may not be copied, modified, or distributed
 // except according to those terms.
 
-use std::time::Instant;
-
-use crate::output::initialization;
-use crate::output::liveness;
-use crate::output::Output;
-
 use datafrog::{Iteration, Relation, RelationLeaper};
-use facts::{AllFacts, FactTypes};
-
-pub(super) fn compute<T: FactTypes>(dump_enabled: bool, all_facts: AllFacts<T>) -> Output<T> {
-    let mut result = Output::new(dump_enabled);
-
-    let var_maybe_initialized_on_exit = initialization::init_var_maybe_initialized_on_exit(
-        all_facts.child,
-        all_facts.path_belongs_to_var,
-        all_facts.initialized_at,
-        all_facts.moved_out_at,
-        all_facts.path_accessed_at,
-        &all_facts.cfg_edge,
-        &mut result,
-    );
+use std::time::Instant;
 
-    let region_live_at = liveness::init_region_live_at(
-        all_facts.var_used,
-        all_facts.var_drop_used,
-        all_facts.var_defined,
-        all_facts.var_uses_region,
-        all_facts.var_drops_region,
-        var_maybe_initialized_on_exit,
-        &all_facts.cfg_edge,
-        all_facts.universal_region,
-        &mut result,
-    );
+use crate::facts::FactTypes;
+use crate::output::{Context, Output};
 
+pub(super) fn compute<T: FactTypes>(
+    ctx: &Context<T>,
+    result: &mut Output<T>,
+) -> Relation<(T::Loan, T::Point)> {
     let timer = Instant::now();
 
     let errors = {
+        // Static inputs
+        let region_live_at_rel = &ctx.region_live_at;
+        let cfg_edge_rel = &ctx.cfg_edge;
+        let killed_rel = &ctx.killed;
+
         // Create a new iteration context, ...
         let mut iteration = Iteration::new();
 
-        // static inputs
-        let cfg_edge_rel = Relation::from_iter(
-            all_facts
-                .cfg_edge
-                .iter()
-                .map(|&(point1, point2)| (point1, point2)),
-        );
-
-        let killed_rel: Relation<(T::Loan, T::Point)> = all_facts.killed.into();
-
         // `invalidates` facts, stored ready for joins
         let invalidates = iteration.variable::<((T::Loan, T::Point), ())>("invalidates");
 
         // we need `region_live_at` in both variable and relation forms,
         // (respectively, for join and antijoin).
-        let region_live_at_rel: Relation<(T::Origin, T::Point)> = region_live_at.into();
         let region_live_at_var =
             iteration.variable::<((T::Origin, T::Point), ())>("region_live_at");
 
@@ -158,16 +128,14 @@ pub(super) fn compute<T: FactTypes>(dump_enabled: bool, all_facts: AllFacts<T>)
 
         // Make "variable" versions of the relations, needed for joins.
         borrow_region_op.extend(
-            all_facts
-                .borrow_region
+            ctx.borrow_region
                 .iter()
                 .map(|&(origin, loan, point)| ((origin, point), loan)),
         );
         invalidates.extend(
-            all_facts
-                .invalidates
+            ctx.invalidates
                 .iter()
-                .map(|&(point, loan)| ((loan, point), ())),
+                .map(|&(loan, point)| ((loan, point), ())),
         );
         region_live_at_var.extend(
             region_live_at_rel
@@ -177,16 +145,14 @@ pub(super) fn compute<T: FactTypes>(dump_enabled: bool, all_facts: AllFacts<T>)
 
         // subset(origin1, origin2, point) :- outlives(origin1, origin2, point).
         subset_o1p.extend(
-            all_facts
-                .outlives
+            ctx.outlives
                 .iter()
                 .map(|&(origin1, origin2, point)| ((origin1, point), origin2)),
         );
 
         // requires(origin, loan, point) :- borrow_region(origin, loan, point).
         requires_op.extend(
-            all_facts
-                .borrow_region
+            ctx.borrow_region
                 .iter()
                 .map(|&(origin, loan, point)| ((origin, point), loan)),
         );
@@ -408,15 +374,7 @@ pub(super) fn compute<T: FactTypes>(dump_enabled: bool, all_facts: AllFacts<T>)
             });
         }
 
-        if dump_enabled {
-            for &(origin, location) in region_live_at_rel.iter() {
-                result
-                    .region_live_at
-                    .entry(location)
-                    .or_default()
-                    .push(origin);
-            }
-
+        if result.dump_enabled {
             let subset_o1p = subset_o1p.complete();
             assert!(
                 subset_o1p
@@ -460,17 +418,11 @@ pub(super) fn compute<T: FactTypes>(dump_enabled: bool, all_facts: AllFacts<T>)
         errors.complete()
     };
 
-    if dump_enabled {
-        info!(
-            "errors is complete: {} tuples, {:?}",
-            errors.len(),
-            timer.elapsed()
-        );
-    }
-
-    for &(loan, location) in errors.iter() {
-        result.errors.entry(location).or_default().push(loan);
-    }
+    info!(
+        "errors is complete: {} tuples, {:?}",
+        errors.len(),
+        timer.elapsed()
+    );
 
-    result
+    errors
 }

polonius-engine/src/output/initialization.rs

@@ -1,30 +1,25 @@
 use std::time::Instant;
 
-use crate::output::Output;
-use facts::FactTypes;
+use crate::facts::FactTypes;
+use crate::output::{InitializationContext, Output};
 
 use datafrog::{Iteration, Relation, RelationLeaper};
 
 pub(super) fn init_var_maybe_initialized_on_exit<T: FactTypes>(
-    child: Vec<(T::Path, T::Path)>,
-    path_belongs_to_var: Vec<(T::Path, T::Variable)>,
-    initialized_at: Vec<(T::Path, T::Point)>,
-    moved_out_at: Vec<(T::Path, T::Point)>,
-    path_accessed_at: Vec<(T::Path, T::Point)>,
-    cfg_edge: &[(T::Point, T::Point)],
+    ctx: InitializationContext<T>,
+    cfg_edge: &Relation<(T::Point, T::Point)>,
     output: &mut Output<T>,
-) -> Vec<(T::Variable, T::Point)> {
-    let computation_start = Instant::now();
+) -> Relation<(T::Variable, T::Point)> {
+    let timer = Instant::now();
     let mut iteration = Iteration::new();
 
     // Relations
     //let parent: Relation<(Path, Path)> = child.iter().map(|&(child_path, parent_path)| (parent_path, child_path)).collect();
-    let child: Relation<(T::Path, T::Path)> = child.into();
-    let path_belongs_to_var: Relation<(T::Path, T::Variable)> = path_belongs_to_var.into();
-    let initialized_at: Relation<(T::Path, T::Point)> = initialized_at.into();
-    let moved_out_at: Relation<(T::Path, T::Point)> = moved_out_at.into();
-    let cfg_edge: Relation<(T::Point, T::Point)> = cfg_edge.iter().cloned().collect();
-    let _path_accessed_at: Relation<(T::Path, T::Point)> = path_accessed_at.into();
+    let child: Relation<(T::Path, T::Path)> = ctx.child.into();
+    let path_belongs_to_var: Relation<(T::Path, T::Variable)> = ctx.path_belongs_to_var.into();
+    let initialized_at: Relation<(T::Path, T::Point)> = ctx.initialized_at.into();
+    let moved_out_at: Relation<(T::Path, T::Point)> = ctx.moved_out_at.into();
+    let _path_accessed_at: Relation<(T::Path, T::Point)> = ctx.path_accessed_at.into();
 
     // Variables
 
@@ -60,10 +55,10 @@ pub(super) fn init_var_maybe_initialized_on_exit<T: FactTypes>(
         // path_maybe_initialized_on_exit(Mother, point) :-
         //     path_maybe_initialized_on_exit(Daughter, point),
         //     child(Daughter, Mother).
-        path_maybe_initialized_on_exit.from_leapjoin(
+        path_maybe_initialized_on_exit.from_join(
             &path_maybe_initialized_on_exit,
-            child.extend_with(|&(daughter, _point)| daughter),
-            |&(_daughter, point), &mother| (mother, point),
+            &child,
+            |&_daughter, &point, &mother| (mother, point),
         );
 
         // TODO: the following lines contain things left to implement for move
@@ -93,12 +88,12 @@ pub(super) fn init_var_maybe_initialized_on_exit<T: FactTypes>(
         // END TODO
 
         // var_maybe_initialized_on_exit(var, point) :-
-        //     path_belongs_to_var(path, var),
-        //     path_maybe_initialized_at(path, point).
-        var_maybe_initialized_on_exit.from_leapjoin(
+        //     path_maybe_initialized_on_exit(path, point),
+        //     path_belongs_to_var(path, var).
+        var_maybe_initialized_on_exit.from_join(
             &path_maybe_initialized_on_exit,
-            path_belongs_to_var.extend_with(|&(path, _point)| path),
-            |&(_path, point), &var| (var, point),
+            &path_belongs_to_var,
+            |&_path, &point, &var| (var, point),
         );
     }
 
@@ -107,7 +102,7 @@ pub(super) fn init_var_maybe_initialized_on_exit<T: FactTypes>(
     info!(
         "init_var_maybe_initialized_on_exit() completed: {} tuples, {:?}",
         var_maybe_initialized_on_exit.len(),
-        computation_start.elapsed()
+        timer.elapsed()
     );
 
     if output.dump_enabled {
@@ -130,7 +125,4 @@ pub(super) fn init_var_maybe_initialized_on_exit<T: FactTypes>(
     }
 
     var_maybe_initialized_on_exit
-        .iter()
-        .map(|&(var, point)| (var, point))
-        .collect()
 }