Skip to content

Commit

Permalink
Merge pull request #127 from lqd/traveler_there_are_no_paths
Browse files Browse the repository at this point in the history
Clean up terminology: step 2 — more renaming, and using actual words
  • Loading branch information
nikomatsakis authored Oct 8, 2019
2 parents 1f31a28 + e55aebe commit 0a65ede
Show file tree
Hide file tree
Showing 12 changed files with 634 additions and 542 deletions.
58 changes: 29 additions & 29 deletions polonius-engine/src/facts.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,64 +4,64 @@ use std::hash::Hash;
/// The "facts" which are the basis of the NLL borrow analysis.
#[derive(Clone, Debug)]
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
/// `borrow_region(origin, loan, point)` -- the `origin` may refer to data
/// from `loan` starting at `point` (this is usually the
/// point *after* a borrow rvalue)
pub borrow_region: Vec<(T::Origin, T::Loan, T::Point)>,

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

/// `cfg_edge(P, Q)` for each edge `P -> Q` in the control flow
/// `cfg_edge(point1, point2)` for each edge `point1 -> point2` in the control flow
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`
/// `killed(loan, point)` when some prefix of the path borrowed at `loan` is assigned at `point`
pub killed: Vec<(T::Loan, T::Point)>,

/// `outlives(O1, P2, P)` when we require `O1@P: O2@P`
/// `outlives(origin1, origin2, point)` when we require `origin1@point: origin2@point`
pub outlives: Vec<(T::Origin, T::Origin, T::Point)>,

/// `invalidates(P, L)` when the loan `L` is invalidated at point `P`
/// `invalidates(point, loan)` when the `loan` is invalidated at `point`
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`
/// `var_used(var, point)` when the variable `var` is used for anything but a drop at `point`
pub var_used: Vec<(T::Variable, T::Point)>,

/// `var_defined(V, P)` when the variable `V` is overwritten by the point `P`
/// `var_defined(var, point)` when the variable `var` is overwritten at `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`
/// `var_used(var, point)` when the variable `var` is used in a drop at `point`
pub var_drop_used: Vec<(T::Variable, T::Point)>,

/// `var_uses_region(V, O)` when the type of `V` includes the origin `O`
/// `var_uses_region(var, origin)` when the type of `var` includes the `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
/// `var_drops_region(var, origin)` when the type of `var` includes the `origin` and uses
/// it when dropping
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)`
/// `child(path1, path2)` when the path `path1` is the direct or transitive child
/// of `path2`, 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<(T::MovePath, T::MovePath)>,
pub child: Vec<(T::Path, T::Path)>,

/// `path_belongs_to_var(M, V)` the root path `M` starting in variable `V`.
pub path_belongs_to_var: Vec<(T::MovePath, T::Variable)>,
/// `path_belongs_to_var(path, var)` the root path `path` starting in variable `var`.
pub path_belongs_to_var: Vec<(T::Path, 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<(T::MovePath, T::Point)>,
/// `initialized_at(path, point)` when the `path` was initialized at point
/// `point`. This fact is only emitted for a prefix `path`, and not for the
/// implicit initialization of all of `path`'s children. E.g. a statement like
/// `x.y = 3` at `point` would give the fact `initialized_at(x.y, point)` (but
/// neither `initialized_at(x.y.z, point)` nor `initialized_at(x, point)`).
pub initialized_at: Vec<(T::Path, T::Point)>,

/// `moved_out_at(M, P)` when the move path `M` was moved at point `P`. The
/// `moved_out_at(path, point)` when the `path` was moved at `point`. The
/// same logic is applied as for `initialized_at` above.
pub moved_out_at: Vec<(T::MovePath, T::Point)>,
pub moved_out_at: Vec<(T::Path, 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<(T::MovePath, T::Point)>,
/// `path_accessed_at(path, point)` when the `path` was accessed at point
/// `point`. The same logic as for `initialized_at` and `moved_out_at` applies.
pub path_accessed_at: Vec<(T::Path, T::Point)>,
}

impl<T: FactTypes> Default for AllFacts<T> {
Expand Down Expand Up @@ -98,5 +98,5 @@ pub trait FactTypes: Copy + Clone + Debug {
type Loan: Atom;
type Point: Atom;
type Variable: Atom;
type MovePath: Atom;
type Path: Atom;
}
Loading

0 comments on commit 0a65ede

Please sign in to comment.