Skip to content

Commit

Permalink
replace fact type parameters with FactTypes
Browse files Browse the repository at this point in the history
  • Loading branch information
@csmoe
csmoe committed Sep 24, 2019
1 parent 1b00de0 commit bd7c225
Show file tree
Hide file tree
Showing 9 changed files with 123 additions and 157 deletions.
38 changes: 19 additions & 19 deletions polonius-engine/src/output/datafrog_opt.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,12 +16,12 @@ 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<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, MovePath: Atom>(
pub(super) fn compute<T: FactTypes>(
dump_enabled: bool,
all_facts: AllFacts<Origin, Loan, Point, Variable, MovePath>,
) -> Output<Origin, Loan, Point, Variable, MovePath> {
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(
Expand Down Expand Up @@ -55,33 +55,33 @@ pub(super) fn compute<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, Mov
// static inputs
let cfg_edge_rel = Relation::from_iter(all_facts.cfg_edge.iter().map(|&(p, q)| (p, q)));

let killed_rel: Relation<(Loan, Point)> = 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)
//
Expand All @@ -95,22 +95,22 @@ pub(super) fn compute<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, Mov
// live things reachable from `R2` to `R1`.
//
let live_to_dying_regions_r2pq =
iteration.variable::<((Origin, Point, Point), Origin)>("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");
iteration.variable::<((T::Origin, T::Point, T::Point), T::Loan)>("dying_region_requires");

// .decl dying_can_reach_origins(R, P, Q)
//
// Contains dead regions where we are interested
// in computing the transitive closure of things they
// can reach.
let dying_can_reach_origins =
iteration.variable::<((Origin, Point), Point)>("dying_can_reach_origins");
iteration.variable::<((T::Origin, T::Point), T::Point)>("dying_can_reach_origins");

// .decl dying_can_reach(R1, R2, P, Q)
//
Expand All @@ -121,7 +121,7 @@ pub(super) fn compute<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, Mov
// relation, but we try to limit it to regions
// that are dying on the edge P -> 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)
Expand All @@ -132,18 +132,18 @@ pub(super) fn compute<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, Mov
// relation where we filter down to those cases where R2 is
// live in Q.
let dying_can_reach_live =
iteration.variable::<((Origin, Point, Point), Origin)>("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");
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");
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");

Expand Down
8 changes: 4 additions & 4 deletions polonius-engine/src/output/hybrid.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,12 +14,12 @@
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<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, MovePath: Atom>(
pub(super) fn compute<T: FactTypes>(
dump_enabled: bool,
all_facts: AllFacts<Origin, Loan, Point, Variable, MovePath>,
) -> Output<Origin, Loan, Point, Variable, MovePath> {
all_facts: AllFacts<T>,
) -> Output<T> {
let lins_output = location_insensitive::compute(dump_enabled, &all_facts);
if lins_output.errors.is_empty() {
lins_output
Expand Down
45 changes: 19 additions & 26 deletions polonius-engine/src/output/initialization.rs
View file
Original file line number Diff line number Diff line change
@@ -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<Origin, Loan, Point, Variable, MovePath>(
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<Origin, Loan, Point, Variable, MovePath>,
) -> Vec<(Variable, Point)>
where
Origin: Atom,
Loan: Atom,
Point: Atom,
Variable: Atom,
MovePath: Atom,
{
pub(super) fn init_var_maybe_initialized_on_exit<T: FactTypes>(
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<T>,
) -> 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

Expand Down
89 changes: 38 additions & 51 deletions polonius-engine/src/output/liveness.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,54 +14,47 @@ 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<Origin, Loan, Point, Variable, MovePath>(
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<Origin, Loan, Point, Variable, MovePath>,
) -> Vec<(Origin, Point)>
where
Origin: Atom,
Loan: Atom,
Point: Atom,
Variable: Atom,
MovePath: Atom,
{
pub(super) fn compute_live_regions<T: FactTypes>(
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<T>,
) -> 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());
Expand Down Expand Up @@ -163,14 +156,14 @@ where
.collect()
}

pub(super) fn make_universal_region_live<Origin: Atom, Point: Atom>(
region_live_at: &mut Vec<(Origin, Point)>,
cfg_edge: &[(Point, Point)],
universal_region: Vec<Origin>,
pub(super) fn make_universal_region_live<T: FactTypes>(
region_live_at: &mut Vec<(T::Origin, T::Point)>,
cfg_edge: &[(T::Point, T::Point)],
universal_region: Vec<T::Origin>,
) {
debug!("make_universal_regions_live()");

let all_points: BTreeSet<Point> = cfg_edge
let all_points: BTreeSet<T::Point> = cfg_edge
.iter()
.map(|&(p, _)| p)
.chain(cfg_edge.iter().map(|&(_, q)| q))
Expand All @@ -184,23 +177,17 @@ pub(super) fn make_universal_region_live<Origin: Atom, Point: Atom>(
}
}

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<Origin>,
output: &mut Output<Origin, Loan, Point, Variable, MovePath>,
) -> Vec<(Origin, Point)> {
pub(super) fn init_region_live_at<T: FactTypes>(
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<T::Origin>,
output: &mut Output<T>,
) -> Vec<(T::Origin, T::Point)> {
debug!("init_region_live_at()");
let mut region_live_at = compute_live_regions(
var_used,
Expand Down
16 changes: 8 additions & 8 deletions polonius-engine/src/output/location_insensitive.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,12 +16,12 @@ 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<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, MovePath: Atom>(
pub(super) fn compute<T: FactTypes>(
dump_enabled: bool,
all_facts: &AllFacts<Origin, Loan, Point, Variable, MovePath>,
) -> Output<Origin, Loan, Point, Variable, MovePath> {
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.clone(),
Expand Down Expand Up @@ -51,14 +51,14 @@ pub(super) fn compute<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, Mov
let mut iteration = Iteration::new();

// static inputs
let region_live_at: Relation<(Origin, Point)> = 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.

Expand Down
Loading

0 comments on commit bd7c225

Please sign in to comment.