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

Clean up terminology: step 1 — rename Region to Origin #125

Merged
merged 15 commits into from
Sep 18, 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
74 changes: 38 additions & 36 deletions polonius-engine/src/facts.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,68 +3,70 @@ use std::hash::Hash;

/// The "facts" which are the basis of the NLL borrow analysis.
#[derive(Clone, Debug)]
pub struct AllFacts<R: Atom, L: Atom, P: Atom, V: Atom, M: Atom> {
/// `borrow_region(R, B, P)` -- the region R may refer to data
/// from borrow B starting at the point P (this is usually the
pub struct AllFacts<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, MovePath: Atom> {
/// `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<(R, L, P)>,
pub borrow_region: Vec<(Origin, Loan, Point)>,

/// `universal_region(R)` -- this is a "free region" within fn body
pub universal_region: Vec<R>,
/// `universal_region(O)` -- this is a "free region" within fn body
pub universal_region: Vec<Origin>,

/// `cfg_edge(P,Q)` for each edge P -> Q in the control flow
pub cfg_edge: Vec<(P, P)>,
/// `cfg_edge(P, Q)` for each edge `P -> Q` in the control flow
pub cfg_edge: Vec<(Point, Point)>,

/// `killed(B,P)` when some prefix of the path borrowed at B is assigned at point P
pub killed: Vec<(L, P)>,
/// `killed(L, P)` when some prefix of the path borrowed at `L` is assigned at point `P`
pub killed: Vec<(Loan, Point)>,

/// `outlives(R1, R2, P)` when we require `R1@P: R2@P`
pub outlives: Vec<(R, R, P)>,
/// `outlives(O1, P2, P)` when we require `O1@P: O2@P`
pub outlives: Vec<(Origin, Origin, Point)>,

/// `invalidates(P, L)` when the loan L is invalidated at point P
pub invalidates: Vec<(P, L)>,
/// `invalidates(P, L)` when the loan `L` is invalidated at point `P`
pub invalidates: Vec<(Point, Loan)>,

/// `var_used(V, P) when the variable V is used for anything but a drop at point P`
pub var_used: Vec<(V, P)>,
/// `var_used(V, P)` when the variable `V` is used for anything but a drop at point `P`
pub var_used: Vec<(Variable, Point)>,

/// `var_defined(V, P) when the variable V is overwritten by the point P`
pub var_defined: Vec<(V, P)>,
/// `var_defined(V, P)` when the variable `V` is overwritten by the point `P`
pub var_defined: Vec<(Variable, Point)>,

/// `var_used(V, P) when the variable V is used in a drop at point P`
pub var_drop_used: Vec<(V, P)>,
/// `var_used(V, P)` when the variable `V` is used in a drop at point `P`
pub var_drop_used: Vec<(Variable, Point)>,

/// `var_uses_region(V, R) when the type of V includes the region R`
pub var_uses_region: Vec<(V, R)>,
/// `var_uses_region(V, O)` when the type of `V` includes the origin `O`
pub var_uses_region: Vec<(Variable, Origin)>,

/// `var_drops_region(V, R) when the type of V includes the region R and uses
/// it when dropping`
pub var_drops_region: Vec<(V, R)>,
/// `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)>,

/// `child(M1, M2) when the move path `M1` is the direct or transitive child
/// `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<(M, M)>,
pub child: Vec<(MovePath, MovePath)>,

/// `path_belongs_to_var(M, V) the root path `M` starting in variable `V`.
pub path_belongs_to_var: Vec<(M, V)>,
/// `path_belongs_to_var(M, V)` the root path `M` starting in variable `V`.
pub path_belongs_to_var: Vec<(MovePath, Variable)>,

/// `initialized_at(M, P) when the move path `M` was initialized at point
/// `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<(M, P)>,
pub initialized_at: Vec<(MovePath, Point)>,

/// `moved_out_at(M, P) when the move path `M` was moved at point `P`. The
/// `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<(M, P)>,
pub moved_out_at: Vec<(MovePath, Point)>,

/// `path_accessed_at(M, P) when the move path `M` was accessed at 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<(M, P)>,
pub path_accessed_at: Vec<(MovePath, Point)>,
}

impl<R: Atom, L: Atom, P: Atom, V: Atom, M: Atom> Default for AllFacts<R, L, P, V, M> {
impl<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, MovePath: Atom> Default
for AllFacts<Origin, Loan, Point, Variable, MovePath>
{
fn default() -> Self {
AllFacts {
borrow_region: Vec::default(),
Expand Down
54 changes: 27 additions & 27 deletions polonius-engine/src/output/datafrog_opt.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,10 +18,10 @@ use crate::output::Output;
use datafrog::{Iteration, Relation, RelationLeaper};
use facts::{AllFacts, Atom};

pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom, Variable: Atom, MovePath: Atom>(
pub(super) fn compute<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, MovePath: Atom>(
dump_enabled: bool,
all_facts: AllFacts<Region, Loan, Point, Variable, MovePath>,
) -> Output<Region, Loan, Point, Variable, MovePath> {
all_facts: AllFacts<Origin, Loan, Point, Variable, MovePath>,
) -> Output<Origin, Loan, Point, Variable, MovePath> {
let mut result = Output::new(dump_enabled);

let var_maybe_initialized_on_exit = initialization::init_var_maybe_initialized_on_exit(
Expand Down Expand Up @@ -62,22 +62,22 @@ pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom, Variable: Atom, Mov

// we need `region_live_at` in both variable and relation forms.
// (respectively, for join and antijoin).
let region_live_at_rel: Relation<(Region, Point)> = region_live_at.into();
let region_live_at_var = iteration.variable::<((Region, Point), ())>("region_live_at");
let region_live_at_rel: Relation<(Origin, Point)> = region_live_at.into();
let region_live_at_var = iteration.variable::<((Origin, Point), ())>("region_live_at");

// `borrow_region` input but organized for join
let borrow_region_rp = iteration.variable::<((Region, Point), Loan)>("borrow_region_rp");
let borrow_region_rp = iteration.variable::<((Origin, Point), Loan)>("borrow_region_rp");

// .decl subset(R1, R2, P)
//
// Indicates that `R1: R2` at the point `P`.
let subset_r1p = iteration.variable::<((Region, Point), Region)>("subset_r1p");
let subset_r1p = iteration.variable::<((Origin, Point), Origin)>("subset_r1p");

// .decl requires(R, B, P)
//
// At the point, things with region R may depend on data from
// At the point, things with origin R may depend on data from
// borrow B
let requires_rp = iteration.variable::<((Region, Point), Loan)>("requires_rp");
let requires_rp = iteration.variable::<((Origin, Point), 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
Expand All @@ -95,55 +95,55 @@ pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom, Variable: Atom, Mov
// live things reachable from `R2` to `R1`.
//
let live_to_dying_regions_r2pq =
iteration.variable::<((Region, Point, Point), Region)>("live_to_dying_regions_r2pq");
iteration.variable::<((Origin, Point, Point), Origin)>("live_to_dying_regions_r2pq");

// .decl dying_region_requires((R, P, Q), B)
//
// The region `R` requires the borrow `B`, but the
// region `R` goes dead along the edge `P -> Q`
// The origin `R` requires the borrow `B`, but the
// origin `R` goes dead along the edge `P -> Q`
let dying_region_requires =
iteration.variable::<((Region, Point, Point), Loan)>("dying_region_requires");
iteration.variable::<((Origin, Point, Point), 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::<((Region, Point), Point)>("dying_can_reach_origins");
iteration.variable::<((Origin, Point), Point)>("dying_can_reach_origins");

// .decl dying_can_reach(R1, R2, P, Q)
//
// Indicates that the region `R1`, which is dead
// in `Q`, can reach the region `R2` in P.
// Indicates that the origin `R1`, which is dead
// in `Q`, can reach the origin `R2` in P.
//
// This is effectively the transitive subset
// relation, but we try to limit it to regions
// that are dying on the edge P -> Q.
let dying_can_reach_r2q =
iteration.variable::<((Region, Point), (Region, Point))>("dying_can_reach");
iteration.variable::<((Origin, Point), (Origin, 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)
//
// Indicates that, along the edge `P -> Q`, the dead (in Q)
// region R1 can reach the live (in Q) region R2 via a subset
// origin R1 can reach the live (in Q) origin R2 via a subset
// 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::<((Region, Point, Point), Region)>("dying_can_reach_live");
iteration.variable::<((Origin, Point, Point), 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::<((Region, Point), Loan)>("dead_borrow_region_can_reach_root");
iteration.variable::<((Origin, Point), 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::<((Region, Point), Loan)>("dead_borrow_region_can_reach_dead");
iteration.variable::<((Origin, Point), 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 Expand Up @@ -234,7 +234,7 @@ pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom, Variable: Atom, Mov
//
// This is the "transitive closure" rule, but
// note that we only apply it with the
// "intermediate" region R2 is dead at Q.
// "intermediate" origin R2 is dead at Q.
dying_can_reach_1.from_antijoin(
&dying_can_reach_r2q,
&region_live_at_rel,
Expand Down Expand Up @@ -288,7 +288,7 @@ pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom, Variable: Atom, Mov
//
// Communicate a `R1 requires B` relation across
// an edge `P -> Q` where `R1` is dead in Q; in
// that case, for each region `R2` live in `Q`
// that case, for each origin `R2` live in `Q`
// where `R1 <= R2` in P, we add `R2 requires B`
// to `Q`.
requires_rp.from_join(
Expand Down Expand Up @@ -366,12 +366,12 @@ pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom, Variable: Atom, Mov
}

if dump_enabled {
for (region, location) in &region_live_at_rel.elements {
for (origin, location) in &region_live_at_rel.elements {
result
.region_live_at
.entry(*location)
.or_insert(vec![])
.push(*region);
.push(*origin);
}

let subset_r1p = subset_r1p.complete();
Expand All @@ -390,12 +390,12 @@ pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom, Variable: Atom, Mov
}

let requires_rp = requires_rp.complete();
for ((region, location), borrow) in &requires_rp.elements {
for ((origin, location), borrow) in &requires_rp.elements {
result
.restricts
.entry(*location)
.or_insert(BTreeMap::new())
.entry(*region)
.entry(*origin)
.or_insert(BTreeSet::new())
.insert(*borrow);
}
Expand Down
6 changes: 3 additions & 3 deletions polonius-engine/src/output/hybrid.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,10 +16,10 @@ use crate::output::location_insensitive;
use crate::output::Output;
use facts::{AllFacts, Atom};

pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom, Variable: Atom, MovePath: Atom>(
pub(super) fn compute<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, MovePath: Atom>(
dump_enabled: bool,
all_facts: AllFacts<Region, Loan, Point, Variable, MovePath>,
) -> Output<Region, Loan, Point, Variable, MovePath> {
all_facts: AllFacts<Origin, Loan, Point, Variable, MovePath>,
) -> Output<Origin, Loan, Point, Variable, MovePath> {
let lins_output = location_insensitive::compute(dump_enabled, &all_facts);
if lins_output.errors.is_empty() {
lins_output
Expand Down
6 changes: 3 additions & 3 deletions polonius-engine/src/output/initialization.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,17 +5,17 @@ use facts::Atom;

use datafrog::{Iteration, Relation, RelationLeaper};

pub(super) fn init_var_maybe_initialized_on_exit<Region, Loan, Point, Variable, MovePath>(
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<Region, Loan, Point, Variable, MovePath>,
output: &mut Output<Origin, Loan, Point, Variable, MovePath>,
) -> Vec<(Variable, Point)>
where
Region: Atom,
Origin: Atom,
Loan: Atom,
Point: Atom,
Variable: Atom,
Expand Down
38 changes: 19 additions & 19 deletions polonius-engine/src/output/liveness.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
// option. This file may not be copied, modified, or distributed
// except according to those terms.

//! An implementation of the region liveness calculation logic
//! An implementation of the origin liveness calculation logic

use std::collections::BTreeSet;
use std::time::Instant;
Expand All @@ -18,18 +18,18 @@ use facts::Atom;

use datafrog::{Iteration, Relation, RelationLeaper};

pub(super) fn compute_live_regions<Region, Loan, Point, Variable, MovePath>(
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, Region)>,
var_drops_region: Vec<(Variable, Region)>,
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<Region, Loan, Point, Variable, MovePath>,
) -> Vec<(Region, Point)>
output: &mut Output<Origin, Loan, Point, Variable, MovePath>,
) -> Vec<(Origin, Point)>
where
Region: Atom,
Origin: Atom,
Loan: Atom,
Point: Atom,
Variable: Atom,
Expand All @@ -44,8 +44,8 @@ where
let cfg_edge_rel: Relation<(Point, Point)> = cfg_edge.iter().map(|(p, q)| (*p, *q)).collect();
let cfg_edge_reverse_rel: Relation<(Point, Point)> =
cfg_edge.iter().map(|(p, q)| (*q, *p)).collect();
let var_uses_region_rel: Relation<(Variable, Region)> = var_uses_region.into();
let var_drops_region_rel: Relation<(Variable, Region)> = var_drops_region.into();
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)> =
var_maybe_initialized_on_exit.into();
let var_drop_used_rel: Relation<((Variable, Point), ())> = var_drop_used
Expand All @@ -61,7 +61,7 @@ where
let var_drop_live_var = iteration.variable::<(Variable, Point)>("var_drop_live_at");

// This is what we are actually calculating:
let region_live_at_var = iteration.variable::<((Region, Point), ())>("region_live_at");
let region_live_at_var = iteration.variable::<((Origin, 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,10 +163,10 @@ where
.collect()
}

pub(super) fn make_universal_region_live<Region: Atom, Point: Atom>(
region_live_at: &mut Vec<(Region, Point)>,
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<Region>,
universal_region: Vec<Origin>,
) {
debug!("make_universal_regions_live()");

Expand All @@ -185,7 +185,7 @@ pub(super) fn make_universal_region_live<Region: Atom, Point: Atom>(
}

pub(super) fn init_region_live_at<
Region: Atom,
Origin: Atom,
Loan: Atom,
Point: Atom,
Variable: Atom,
Expand All @@ -194,13 +194,13 @@ pub(super) fn init_region_live_at<
var_used: Vec<(Variable, Point)>,
var_drop_used: Vec<(Variable, Point)>,
var_defined: Vec<(Variable, Point)>,
var_uses_region: Vec<(Variable, Region)>,
var_drops_region: Vec<(Variable, Region)>,
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<Region>,
output: &mut Output<Region, Loan, Point, Variable, MovePath>,
) -> Vec<(Region, Point)> {
universal_region: Vec<Origin>,
output: &mut Output<Origin, Loan, Point, Variable, MovePath>,
) -> Vec<(Origin, Point)> {
debug!("init_region_live_at()");
let mut region_live_at = compute_live_regions(
var_used,
Expand Down
Loading