Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

replace fact type parameters with FactTypes #130

Merged
merged 4 commits into from
Oct 3, 2019
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
46 changes: 26 additions & 20 deletions polonius-engine/src/facts.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, MovePath: Atom> {
pub struct AllFacts<T: FactTypes> {
/// `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<Origin>,
pub universal_region: Vec<T::Origin>,

/// `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<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, MovePath: Atom> Default
for AllFacts<Origin, Loan, Point, Variable, MovePath>
{
impl<T: FactTypes> Default for AllFacts<T> {
fn default() -> Self {
AllFacts {
borrow_region: Vec::default(),
Expand Down Expand Up @@ -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;
}
1 change: 1 addition & 0 deletions polonius-engine/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
49 changes: 24 additions & 25 deletions polonius-engine/src/output/datafrog_opt.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, MovePath: Atom>(
dump_enabled: bool,
all_facts: AllFacts<Origin, Loan, Point, Variable, MovePath>,
) -> Output<Origin, Loan, Point, Variable, MovePath> {
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(
Expand Down Expand Up @@ -55,33 +52,35 @@ 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 @@ -94,23 +93,23 @@ pub(super) fn compute<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, Mov
// In that case, `Q` would like to add all the
// live things reachable from `R2` to `R1`.
//
let live_to_dying_regions_r2pq =
iteration.variable::<((Origin, Point, Point), Origin)>("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)
//
// 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 +120,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 @@ -131,19 +130,19 @@ pub(super) fn compute<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, Mov
// relation. This is a subset of the full `dying_can_reach`
// 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");
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");

Expand Down
7 changes: 2 additions & 5 deletions polonius-engine/src/output/hybrid.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, MovePath: Atom>(
dump_enabled: bool,
all_facts: AllFacts<Origin, Loan, Point, Variable, MovePath>,
) -> Output<Origin, Loan, Point, Variable, MovePath> {
pub(super) fn compute<T: FactTypes>(dump_enabled: bool, 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
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
Loading