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.

Sign up for GitHub

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 2 — more renaming, and using actual words #127

Merged
merged 1 commit into from
Oct 8, 2019
Merged

Clean up terminology: step 2 — more renaming, and using actual words #127

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
58 changes: 29 additions & 29 deletions polonius-engine/src/facts.rs
View file
Open in desktop
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