diff --git a/polonius-engine/src/facts.rs b/polonius-engine/src/facts.rs index eb90b3f2846..c9c67e64297 100644 --- a/polonius-engine/src/facts.rs +++ b/polonius-engine/src/facts.rs @@ -3,70 +3,68 @@ use std::hash::Hash; /// The "facts" which are the basis of the NLL borrow analysis. #[derive(Clone, Debug)] -pub struct AllFacts { +pub struct AllFacts { /// `borrow_region(O, L, P)` -- the origin `O` may refer to data /// from loan `L` starting at the point `P` (this is usually the /// point *after* a borrow rvalue) - pub borrow_region: Vec<(Origin, Loan, Point)>, + pub borrow_region: Vec<(T::Origin, T::Loan, T::Point)>, /// `universal_region(O)` -- this is a "free region" within fn body - pub universal_region: Vec, + pub universal_region: Vec, /// `cfg_edge(P, Q)` for each edge `P -> Q` in the control flow - pub cfg_edge: Vec<(Point, Point)>, + pub cfg_edge: Vec<(T::Point, T::Point)>, /// `killed(L, P)` when some prefix of the path borrowed at `L` is assigned at point `P` - pub killed: Vec<(Loan, Point)>, + pub killed: Vec<(T::Loan, T::Point)>, /// `outlives(O1, P2, P)` when we require `O1@P: O2@P` - pub outlives: Vec<(Origin, Origin, Point)>, + pub outlives: Vec<(T::Origin, T::Origin, T::Point)>, /// `invalidates(P, L)` when the loan `L` is invalidated at point `P` - pub invalidates: Vec<(Point, Loan)>, + pub invalidates: Vec<(T::Point, T::Loan)>, /// `var_used(V, P)` when the variable `V` is used for anything but a drop at point `P` - pub var_used: Vec<(Variable, Point)>, + pub var_used: Vec<(T::Variable, T::Point)>, /// `var_defined(V, P)` when the variable `V` is overwritten by the point `P` - pub var_defined: Vec<(Variable, Point)>, + pub var_defined: Vec<(T::Variable, T::Point)>, /// `var_used(V, P)` when the variable `V` is used in a drop at point `P` - pub var_drop_used: Vec<(Variable, Point)>, + pub var_drop_used: Vec<(T::Variable, T::Point)>, /// `var_uses_region(V, O)` when the type of `V` includes the origin `O` - pub var_uses_region: Vec<(Variable, Origin)>, + pub var_uses_region: Vec<(T::Variable, T::Origin)>, /// `var_drops_region(V, O)` when the type of `V` includes the origin `O` and uses /// it when dropping - pub var_drops_region: Vec<(Variable, Origin)>, + pub var_drops_region: Vec<(T::Variable, T::Origin)>, /// `child(M1, M2)` when the move path `M1` is the direct or transitive child /// of `M2`, e.g. `child(x.y, x)`, `child(x.y.z, x.y)`, `child(x.y.z, x)` /// would all be true if there was a path like `x.y.z`. - pub child: Vec<(MovePath, MovePath)>, + pub child: Vec<(T::MovePath, T::MovePath)>, /// `path_belongs_to_var(M, V)` the root path `M` starting in variable `V`. - pub path_belongs_to_var: Vec<(MovePath, Variable)>, + pub path_belongs_to_var: Vec<(T::MovePath, T::Variable)>, /// `initialized_at(M, P)` when the move path `M` was initialized at point /// `P`. This fact is only emitted for a prefix `M`, and not for the /// implicit initialization of all of `M`'s children. E.g. a statement like /// `x.y = 3` at point `P` would give the fact `initialized_at(x.y, P)` (but /// neither `initialized_at(x.y.z, P)` nor `initialized_at(x, P)`). - pub initialized_at: Vec<(MovePath, Point)>, + pub initialized_at: Vec<(T::MovePath, T::Point)>, /// `moved_out_at(M, P)` when the move path `M` was moved at point `P`. The /// same logic is applied as for `initialized_at` above. - pub moved_out_at: Vec<(MovePath, Point)>, + pub moved_out_at: Vec<(T::MovePath, T::Point)>, /// `path_accessed_at(M, P)` when the move path `M` was accessed at point /// `P`. The same logic as for `initialized_at` and `moved_out_at` applies. - pub path_accessed_at: Vec<(MovePath, Point)>, + pub path_accessed_at: Vec<(T::MovePath, T::Point)>, } -impl Default - for AllFacts -{ +impl Default for AllFacts { fn default() -> Self { AllFacts { borrow_region: Vec::default(), @@ -94,3 +92,11 @@ pub trait Atom: { fn index(self) -> usize; } + +pub trait FactTypes: Copy + Clone + Debug { + type Origin: Atom; + type Loan: Atom; + type Point: Atom; + type Variable: Atom; + type MovePath: Atom; +} diff --git a/polonius-engine/src/lib.rs b/polonius-engine/src/lib.rs index 19586f51950..0926be8f593 100644 --- a/polonius-engine/src/lib.rs +++ b/polonius-engine/src/lib.rs @@ -11,5 +11,6 @@ mod output; // Reexports of facts pub use facts::AllFacts; pub use facts::Atom; +pub use facts::FactTypes; pub use output::Algorithm; pub use output::Output; diff --git a/polonius-engine/src/output/datafrog_opt.rs b/polonius-engine/src/output/datafrog_opt.rs index 378597dc969..a15f2828a3c 100644 --- a/polonius-engine/src/output/datafrog_opt.rs +++ b/polonius-engine/src/output/datafrog_opt.rs @@ -16,12 +16,9 @@ use crate::output::liveness; use crate::output::Output; use datafrog::{Iteration, Relation, RelationLeaper}; -use facts::{AllFacts, Atom}; +use facts::{AllFacts, FactTypes}; -pub(super) fn compute( - dump_enabled: bool, - all_facts: AllFacts, -) -> Output { +pub(super) fn compute(dump_enabled: bool, all_facts: AllFacts) -> Output { let mut result = Output::new(dump_enabled); let var_maybe_initialized_on_exit = initialization::init_var_maybe_initialized_on_exit( @@ -55,33 +52,35 @@ pub(super) fn compute = all_facts.killed.into(); + let killed_rel: Relation<(T::Loan, T::Point)> = all_facts.killed.into(); // `invalidates` facts, stored ready for joins - let invalidates = iteration.variable::<((Loan, Point), ())>("invalidates"); + 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<(Origin, Point)> = region_live_at.into(); - let region_live_at_var = iteration.variable::<((Origin, Point), ())>("region_live_at"); + 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"); // `borrow_region` input but organized for join - let borrow_region_rp = iteration.variable::<((Origin, Point), Loan)>("borrow_region_rp"); + let borrow_region_rp = + iteration.variable::<((T::Origin, T::Point), T::Loan)>("borrow_region_rp"); // .decl subset(R1, R2, P) // // Indicates that `R1: R2` at the point `P`. - let subset_r1p = iteration.variable::<((Origin, Point), Origin)>("subset_r1p"); + let subset_r1p = iteration.variable::<((T::Origin, T::Point), T::Origin)>("subset_r1p"); // .decl requires(R, B, P) // // At the point, things with origin R may depend on data from // borrow B - let requires_rp = iteration.variable::<((Origin, Point), Loan)>("requires_rp"); + let requires_rp = iteration.variable::<((T::Origin, T::Point), T::Loan)>("requires_rp"); // .decl borrow_live_at(B, P) -- true if the restrictions of the borrow B // need to be enforced at the point P - let borrow_live_at = iteration.variable::<((Loan, Point), ())>("borrow_live_at"); + let borrow_live_at = iteration.variable::<((T::Loan, T::Point), ())>("borrow_live_at"); // .decl live_to_dying_regions(R1, R2, P, Q) // @@ -94,15 +93,15 @@ pub(super) fn compute("live_to_dying_regions_r2pq"); + let live_to_dying_regions_r2pq = iteration + .variable::<((T::Origin, T::Point, T::Point), T::Origin)>("live_to_dying_regions_r2pq"); // .decl dying_region_requires((R, P, Q), B) // // The origin `R` requires the borrow `B`, but the // origin `R` goes dead along the edge `P -> Q` - let dying_region_requires = - iteration.variable::<((Origin, Point, Point), Loan)>("dying_region_requires"); + let dying_region_requires = iteration + .variable::<((T::Origin, T::Point, T::Point), T::Loan)>("dying_region_requires"); // .decl dying_can_reach_origins(R, P, Q) // @@ -110,7 +109,7 @@ pub(super) fn compute("dying_can_reach_origins"); + iteration.variable::<((T::Origin, T::Point), T::Point)>("dying_can_reach_origins"); // .decl dying_can_reach(R1, R2, P, Q) // @@ -121,7 +120,7 @@ pub(super) fn compute Q. let dying_can_reach_r2q = - iteration.variable::<((Origin, Point), (Origin, Point))>("dying_can_reach"); + iteration.variable::<((T::Origin, T::Point), (T::Origin, T::Point))>("dying_can_reach"); let dying_can_reach_1 = iteration.variable_indistinct("dying_can_reach_1"); // .decl dying_can_reach_live(R1, R2, P, Q) @@ -131,19 +130,19 @@ pub(super) fn compute("dying_can_reach_live"); + let dying_can_reach_live = iteration + .variable::<((T::Origin, T::Point, T::Point), T::Origin)>("dying_can_reach_live"); // .decl dead_borrow_region_can_reach_root((R, P), B) // // Indicates a "borrow region" R at P which is not live on // entry to P. - let dead_borrow_region_can_reach_root = - iteration.variable::<((Origin, Point), Loan)>("dead_borrow_region_can_reach_root"); + let dead_borrow_region_can_reach_root = iteration + .variable::<((T::Origin, T::Point), T::Loan)>("dead_borrow_region_can_reach_root"); // .decl dead_borrow_region_can_reach_dead((R2, P), B) - let dead_borrow_region_can_reach_dead = - iteration.variable::<((Origin, Point), Loan)>("dead_borrow_region_can_reach_dead"); + let dead_borrow_region_can_reach_dead = iteration + .variable::<((T::Origin, T::Point), T::Loan)>("dead_borrow_region_can_reach_dead"); let dead_borrow_region_can_reach_dead_1 = iteration.variable_indistinct("dead_borrow_region_can_reach_dead_1"); diff --git a/polonius-engine/src/output/hybrid.rs b/polonius-engine/src/output/hybrid.rs index 39274ecbe18..91ef4fede1b 100644 --- a/polonius-engine/src/output/hybrid.rs +++ b/polonius-engine/src/output/hybrid.rs @@ -14,12 +14,9 @@ use crate::output::datafrog_opt; use crate::output::location_insensitive; use crate::output::Output; -use facts::{AllFacts, Atom}; +use facts::{AllFacts, FactTypes}; -pub(super) fn compute( - dump_enabled: bool, - all_facts: AllFacts, -) -> Output { +pub(super) fn compute(dump_enabled: bool, all_facts: AllFacts) -> Output { let lins_output = location_insensitive::compute(dump_enabled, &all_facts); if lins_output.errors.is_empty() { lins_output diff --git a/polonius-engine/src/output/initialization.rs b/polonius-engine/src/output/initialization.rs index 463ce804b8a..3f12f5765cf 100644 --- a/polonius-engine/src/output/initialization.rs +++ b/polonius-engine/src/output/initialization.rs @@ -1,50 +1,43 @@ use std::time::Instant; use crate::output::Output; -use facts::Atom; +use facts::FactTypes; use datafrog::{Iteration, Relation, RelationLeaper}; -pub(super) fn init_var_maybe_initialized_on_exit( - child: Vec<(MovePath, MovePath)>, - path_belongs_to_var: Vec<(MovePath, Variable)>, - initialized_at: Vec<(MovePath, Point)>, - moved_out_at: Vec<(MovePath, Point)>, - path_accessed_at: Vec<(MovePath, Point)>, - cfg_edge: &[(Point, Point)], - output: &mut Output, -) -> Vec<(Variable, Point)> -where - Origin: Atom, - Loan: Atom, - Point: Atom, - Variable: Atom, - MovePath: Atom, -{ +pub(super) fn init_var_maybe_initialized_on_exit( + child: Vec<(T::MovePath, T::MovePath)>, + path_belongs_to_var: Vec<(T::MovePath, T::Variable)>, + initialized_at: Vec<(T::MovePath, T::Point)>, + moved_out_at: Vec<(T::MovePath, T::Point)>, + path_accessed_at: Vec<(T::MovePath, T::Point)>, + cfg_edge: &[(T::Point, T::Point)], + output: &mut Output, +) -> Vec<(T::Variable, T::Point)> { debug!("compute_initialization()"); let computation_start = Instant::now(); let mut iteration = Iteration::new(); // Relations - //let parent: Relation<(MovePath, MovePath)> = child.iter().map(|&(c, p)| (p, c)).collect(); - let child: Relation<(MovePath, MovePath)> = child.into(); - let path_belongs_to_var: Relation<(MovePath, Variable)> = path_belongs_to_var.into(); - let initialized_at: Relation<(MovePath, Point)> = initialized_at.into(); - let moved_out_at: Relation<(MovePath, Point)> = moved_out_at.into(); - let cfg_edge: Relation<(Point, Point)> = cfg_edge.iter().cloned().collect(); - let _path_accessed_at: Relation<(MovePath, Point)> = path_accessed_at.into(); + //let parent: Relation<(T::MovePath, T::MovePath)> = child.iter().map(|&(c, p)| (p, c)).collect(); + let child: Relation<(T::MovePath, T::MovePath)> = child.into(); + let path_belongs_to_var: Relation<(T::MovePath, T::Variable)> = path_belongs_to_var.into(); + let initialized_at: Relation<(T::MovePath, T::Point)> = initialized_at.into(); + let moved_out_at: Relation<(T::MovePath, 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::MovePath, T::Point)> = path_accessed_at.into(); // Variables // var_maybe_initialized_on_exit(V, P): Upon leaving `P`, at least one part of the // variable `V` might be initialized for some path through the CFG. let var_maybe_initialized_on_exit = - iteration.variable::<(Variable, Point)>("var_maybe_initialized_on_exit"); + iteration.variable::<(T::Variable, T::Point)>("var_maybe_initialized_on_exit"); // path_maybe_initialized_on_exit(M, P): Upon leaving `P`, the move path `M` // might be *partially* initialized for some path through the CFG. let path_maybe_initialized_on_exit = - iteration.variable::<(MovePath, Point)>("path_maybe_initialized_on_exit"); + iteration.variable::<(T::MovePath, T::Point)>("path_maybe_initialized_on_exit"); // Initial propagation of static relations diff --git a/polonius-engine/src/output/liveness.rs b/polonius-engine/src/output/liveness.rs index 098665062d2..3a3ba8b0c35 100644 --- a/polonius-engine/src/output/liveness.rs +++ b/polonius-engine/src/output/liveness.rs @@ -14,54 +14,48 @@ use std::collections::BTreeSet; use std::time::Instant; use crate::output::Output; -use facts::Atom; +use facts::FactTypes; use datafrog::{Iteration, Relation, RelationLeaper}; -pub(super) fn compute_live_regions( - var_used: Vec<(Variable, Point)>, - var_drop_used: Vec<(Variable, Point)>, - var_defined: Vec<(Variable, Point)>, - var_uses_region: Vec<(Variable, Origin)>, - var_drops_region: Vec<(Variable, Origin)>, - cfg_edge: &[(Point, Point)], - var_maybe_initialized_on_exit: Vec<(Variable, Point)>, - output: &mut Output, -) -> Vec<(Origin, Point)> -where - Origin: Atom, - Loan: Atom, - Point: Atom, - Variable: Atom, - MovePath: Atom, -{ +pub(super) fn compute_live_regions( + var_used: Vec<(T::Variable, T::Point)>, + var_drop_used: Vec<(T::Variable, T::Point)>, + var_defined: Vec<(T::Variable, T::Point)>, + var_uses_region: Vec<(T::Variable, T::Origin)>, + var_drops_region: Vec<(T::Variable, T::Origin)>, + cfg_edge: &[(T::Point, T::Point)], + var_maybe_initialized_on_exit: Vec<(T::Variable, T::Point)>, + output: &mut Output, +) -> Vec<(T::Origin, T::Point)> { debug!("compute_liveness()"); let computation_start = Instant::now(); let mut iteration = Iteration::new(); // Relations - let var_defined_rel: Relation<(Variable, Point)> = var_defined.into(); - let cfg_edge_rel: Relation<(Point, Point)> = cfg_edge.iter().map(|(p, q)| (*p, *q)).collect(); - let cfg_edge_reverse_rel: Relation<(Point, Point)> = + let var_defined_rel: Relation<(T::Variable, T::Point)> = var_defined.into(); + let cfg_edge_rel: Relation<(T::Point, T::Point)> = + cfg_edge.iter().map(|(p, q)| (*p, *q)).collect(); + let cfg_edge_reverse_rel: Relation<(T::Point, T::Point)> = cfg_edge.iter().map(|(p, q)| (*q, *p)).collect(); - let var_uses_region_rel: Relation<(Variable, Origin)> = var_uses_region.into(); - let var_drops_region_rel: Relation<(Variable, Origin)> = var_drops_region.into(); - let var_maybe_initialized_on_exit_rel: Relation<(Variable, Point)> = + let var_uses_region_rel: Relation<(T::Variable, T::Origin)> = var_uses_region.into(); + let var_drops_region_rel: Relation<(T::Variable, T::Origin)> = var_drops_region.into(); + let var_maybe_initialized_on_exit_rel: Relation<(T::Variable, T::Point)> = var_maybe_initialized_on_exit.into(); - let var_drop_used_rel: Relation<((Variable, Point), ())> = var_drop_used + let var_drop_used_rel: Relation<((T::Variable, T::Point), ())> = var_drop_used .into_iter() .map(|(v, p)| ((v, p), ())) .collect(); - // Variables + // T::Variables // `var_live`: variable V is live upon entry in point P - let var_live_var = iteration.variable::<(Variable, Point)>("var_live_at"); + let var_live_var = iteration.variable::<(T::Variable, T::Point)>("var_live_at"); // `var_drop_live`: variable V is drop-live (will be used for a drop) upon entry in point P - let var_drop_live_var = iteration.variable::<(Variable, Point)>("var_drop_live_at"); + let var_drop_live_var = iteration.variable::<(T::Variable, T::Point)>("var_drop_live_at"); // This is what we are actually calculating: - let region_live_at_var = iteration.variable::<((Origin, Point), ())>("region_live_at"); + let region_live_at_var = iteration.variable::<((T::Origin, T::Point), ())>("region_live_at"); // This propagates the relation `var_live(V, P) :- var_used(V, P)`: var_live_var.insert(var_used.into()); @@ -163,14 +157,14 @@ where .collect() } -pub(super) fn make_universal_region_live( - region_live_at: &mut Vec<(Origin, Point)>, - cfg_edge: &[(Point, Point)], - universal_region: Vec, +pub(super) fn make_universal_region_live( + region_live_at: &mut Vec<(T::Origin, T::Point)>, + cfg_edge: &[(T::Point, T::Point)], + universal_region: Vec, ) { debug!("make_universal_regions_live()"); - let all_points: BTreeSet = cfg_edge + let all_points: BTreeSet = cfg_edge .iter() .map(|&(p, _)| p) .chain(cfg_edge.iter().map(|&(_, q)| q)) @@ -184,23 +178,17 @@ pub(super) fn make_universal_region_live( } } -pub(super) fn init_region_live_at< - Origin: Atom, - Loan: Atom, - Point: Atom, - Variable: Atom, - MovePath: Atom, ->( - var_used: Vec<(Variable, Point)>, - var_drop_used: Vec<(Variable, Point)>, - var_defined: Vec<(Variable, Point)>, - var_uses_region: Vec<(Variable, Origin)>, - var_drops_region: Vec<(Variable, Origin)>, - var_maybe_initialized_on_exit: Vec<(Variable, Point)>, - cfg_edge: &[(Point, Point)], - universal_region: Vec, - output: &mut Output, -) -> Vec<(Origin, Point)> { +pub(super) fn init_region_live_at( + var_used: Vec<(T::Variable, T::Point)>, + var_drop_used: Vec<(T::Variable, T::Point)>, + var_defined: Vec<(T::Variable, T::Point)>, + var_uses_region: Vec<(T::Variable, T::Origin)>, + var_drops_region: Vec<(T::Variable, T::Origin)>, + var_maybe_initialized_on_exit: Vec<(T::Variable, T::Point)>, + cfg_edge: &[(T::Point, T::Point)], + universal_region: Vec, + output: &mut Output, +) -> Vec<(T::Origin, T::Point)> { debug!("init_region_live_at()"); let mut region_live_at = compute_live_regions( var_used, @@ -213,7 +201,7 @@ pub(super) fn init_region_live_at< output, ); - make_universal_region_live(&mut region_live_at, cfg_edge, universal_region); + make_universal_region_live::(&mut region_live_at, cfg_edge, universal_region); region_live_at } diff --git a/polonius-engine/src/output/location_insensitive.rs b/polonius-engine/src/output/location_insensitive.rs index 4805aa47742..de55ec5c321 100644 --- a/polonius-engine/src/output/location_insensitive.rs +++ b/polonius-engine/src/output/location_insensitive.rs @@ -16,12 +16,9 @@ use crate::output::liveness; use crate::output::Output; use datafrog::{Iteration, Relation, RelationLeaper}; -use facts::{AllFacts, Atom}; +use facts::{AllFacts, FactTypes}; -pub(super) fn compute( - dump_enabled: bool, - all_facts: &AllFacts, -) -> Output { +pub(super) fn compute(dump_enabled: bool, all_facts: &AllFacts) -> Output { let mut result = Output::new(dump_enabled); let var_maybe_initialized_on_exit = initialization::init_var_maybe_initialized_on_exit( all_facts.child.clone(), @@ -51,14 +48,14 @@ pub(super) fn compute = region_live_at.into(); + let region_live_at: Relation<(T::Origin, T::Point)> = region_live_at.into(); let invalidates = Relation::from_iter(all_facts.invalidates.iter().map(|&(b, p)| (p, b))); // .. some variables, .. - let subset = iteration.variable::<(Origin, Origin)>("subset"); - let requires = iteration.variable::<(Origin, Loan)>("requires"); + let subset = iteration.variable::<(T::Origin, T::Origin)>("subset"); + let requires = iteration.variable::<(T::Origin, T::Loan)>("requires"); - let potential_errors = iteration.variable::<(Loan, Point)>("potential_errors"); + let potential_errors = iteration.variable::<(T::Loan, T::Point)>("potential_errors"); // load initial facts. diff --git a/polonius-engine/src/output/mod.rs b/polonius-engine/src/output/mod.rs index 82712160a44..88e8955eab7 100644 --- a/polonius-engine/src/output/mod.rs +++ b/polonius-engine/src/output/mod.rs @@ -18,7 +18,7 @@ mod initialization; mod liveness; mod location_insensitive; mod naive; -use facts::{AllFacts, Atom}; +use facts::{AllFacts, Atom, FactTypes}; #[derive(Debug, Clone, Copy)] pub enum Algorithm { @@ -62,30 +62,23 @@ impl ::std::str::FromStr for Algorithm { } #[derive(Clone, Debug)] -pub struct Output -where - Origin: Atom, - Loan: Atom, - Point: Atom, - Variable: Atom, - MovePath: Atom, -{ - pub errors: FxHashMap>, +pub struct Output { + pub errors: FxHashMap>, pub dump_enabled: bool, // these are just for debugging - pub borrow_live_at: FxHashMap>, - pub restricts: FxHashMap>>, - pub restricts_anywhere: FxHashMap>, - pub region_live_at: FxHashMap>, - pub invalidates: FxHashMap>, - pub subset: FxHashMap>>, - pub subset_anywhere: FxHashMap>, - pub var_live_at: FxHashMap>, - pub var_drop_live_at: FxHashMap>, - pub path_maybe_initialized_at: FxHashMap>, - pub var_maybe_initialized_on_exit: FxHashMap>, + pub borrow_live_at: FxHashMap>, + pub restricts: FxHashMap>>, + pub restricts_anywhere: FxHashMap>, + pub region_live_at: FxHashMap>, + pub invalidates: FxHashMap>, + pub subset: FxHashMap>>, + pub subset_anywhere: FxHashMap>, + pub var_live_at: FxHashMap>, + pub var_drop_live_at: FxHashMap>, + pub path_maybe_initialized_at: FxHashMap>, + pub var_maybe_initialized_on_exit: FxHashMap>, } /// Compares errors reported by Naive implementation with the errors @@ -124,19 +117,8 @@ fn compare_errors( differ } -impl Output -where - Origin: Atom, - Loan: Atom, - Point: Atom, - Variable: Atom, - MovePath: Atom, -{ - pub fn compute( - all_facts: &AllFacts, - algorithm: Algorithm, - dump_enabled: bool, - ) -> Self { +impl Output { + pub fn compute(all_facts: &AllFacts, algorithm: Algorithm, dump_enabled: bool) -> Self { match algorithm { Algorithm::Naive => naive::compute(dump_enabled, all_facts.clone()), Algorithm::DatafrogOpt => datafrog_opt::compute(dump_enabled, all_facts.clone()), @@ -179,21 +161,24 @@ where } } - pub fn errors_at(&self, location: Point) -> &[Loan] { + pub fn errors_at(&self, location: T::Point) -> &[T::Loan] { match self.errors.get(&location) { Some(v) => v, None => &[], } } - pub fn borrows_in_scope_at(&self, location: Point) -> &[Loan] { + pub fn borrows_in_scope_at(&self, location: T::Point) -> &[T::Loan] { match self.borrow_live_at.get(&location) { Some(p) => p, None => &[], } } - pub fn restricts_at(&self, location: Point) -> Cow<'_, BTreeMap>> { + pub fn restricts_at( + &self, + location: T::Point, + ) -> Cow<'_, BTreeMap>> { assert!(self.dump_enabled); match self.restricts.get(&location) { Some(map) => Cow::Borrowed(map), @@ -201,7 +186,7 @@ where } } - pub fn regions_live_at(&self, location: Point) -> &[Origin] { + pub fn regions_live_at(&self, location: T::Point) -> &[T::Origin] { assert!(self.dump_enabled); match self.region_live_at.get(&location) { Some(v) => v, @@ -209,7 +194,10 @@ where } } - pub fn subsets_at(&self, location: Point) -> Cow<'_, BTreeMap>> { + pub fn subsets_at( + &self, + location: T::Point, + ) -> Cow<'_, BTreeMap>> { assert!(self.dump_enabled); match self.subset.get(&location) { Some(v) => Cow::Borrowed(v), diff --git a/polonius-engine/src/output/naive.rs b/polonius-engine/src/output/naive.rs index acacd7fab37..4da6047ab30 100644 --- a/polonius-engine/src/output/naive.rs +++ b/polonius-engine/src/output/naive.rs @@ -16,14 +16,11 @@ use std::time::Instant; use crate::output::initialization; use crate::output::liveness; use crate::output::Output; -use facts::{AllFacts, Atom}; +use facts::{AllFacts, FactTypes}; use datafrog::{Iteration, Relation, RelationLeaper}; -pub(super) fn compute( - dump_enabled: bool, - all_facts: AllFacts, -) -> Output { +pub(super) fn compute(dump_enabled: bool, all_facts: AllFacts) -> Output { let mut result = Output::new(dump_enabled); let var_maybe_initialized_on_exit = initialization::init_var_maybe_initialized_on_exit( @@ -55,17 +52,17 @@ pub(super) fn compute = all_facts.cfg_edge.into(); - let killed_rel: Relation<(Loan, Point)> = all_facts.killed.into(); - let region_live_at_rel: Relation<(Origin, Point)> = region_live_at.into(); + let cfg_edge_rel: Relation<(T::Point, T::Point)> = all_facts.cfg_edge.into(); + let killed_rel: Relation<(T::Loan, T::Point)> = all_facts.killed.into(); + let region_live_at_rel: Relation<(T::Origin, T::Point)> = region_live_at.into(); // .. some variables, .. - let subset = iteration.variable::<(Origin, Origin, Point)>("subset"); - let requires = iteration.variable::<(Origin, Loan, Point)>("requires"); - let borrow_live_at = iteration.variable::<((Loan, Point), ())>("borrow_live_at"); + let subset = iteration.variable::<(T::Origin, T::Origin, T::Point)>("subset"); + let requires = iteration.variable::<(T::Origin, T::Loan, T::Point)>("requires"); + let borrow_live_at = iteration.variable::<((T::Loan, T::Point), ())>("borrow_live_at"); // `invalidates` facts, stored ready for joins - let invalidates = iteration.variable::<((Loan, Point), ())>("invalidates"); + let invalidates = iteration.variable::<((T::Loan, T::Point), ())>("invalidates"); // different indices for `subset`. let subset_r1p = iteration.variable_indistinct("subset_r1p"); @@ -76,7 +73,8 @@ pub(super) fn compute("region_live_at"); + let region_live_at_var = + iteration.variable::<((T::Origin, T::Point), ())>("region_live_at"); // output let errors = iteration.variable("errors"); diff --git a/src/dump.rs b/src/dump.rs index 2c9d0a56e68..d6b14fa73d0 100644 --- a/src/dump.rs +++ b/src/dump.rs @@ -13,7 +13,7 @@ use std::hash::Hash; use std::io::{self, Write}; use std::path::PathBuf; -pub(crate) type Output = PoloniusEngineOutput; +pub(crate) type Output = PoloniusEngineOutput; pub(crate) fn dump_output( output: &Output, diff --git a/src/facts.rs b/src/facts.rs index a04d9c2cf99..11e7a39bdb7 100644 --- a/src/facts.rs +++ b/src/facts.rs @@ -1,6 +1,9 @@ -use polonius_engine; +use polonius_engine::{self, FactTypes}; -pub(crate) type AllFacts = polonius_engine::AllFacts; +#[derive(Copy, Clone, Debug)] +pub(crate) struct LocalFacts; + +pub(crate) type AllFacts = polonius_engine::AllFacts; macro_rules! index_type { ($t:ident) => { @@ -36,3 +39,11 @@ index_type!(Loan); index_type!(Point); index_type!(Variable); index_type!(MovePath); + +impl FactTypes for LocalFacts { + type Origin = Origin; + type Loan = Loan; + type Point = Point; + type Variable = Variable; + type MovePath = MovePath; +}