Skip to content

Commit e14c09f

Browse files
Add polonius_facts crate containing AllFacts
1 parent c228cde commit e14c09f

File tree

6 files changed

+7
-132
lines changed

6 files changed

+7
-132
lines changed

polonius-engine/Cargo.toml

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,5 +10,7 @@ keywords = ["compiler", "borrowck", "datalog"]
1010

1111
[dependencies]
1212
datafrog = "2.0.0"
13+
polonius-facts = { path = "../polonius-facts" }
14+
polonius-souffle = { path = "../polonius-souffle" }
1315
rustc-hash = "1.0.0"
1416
log = "0.4"

polonius-engine/src/facts.rs

Lines changed: 1 addition & 129 deletions
Original file line numberDiff line numberDiff line change
@@ -1,129 +1 @@
1-
use std::fmt::Debug;
2-
use std::hash::Hash;
3-
4-
/// The "facts" which are the basis of the NLL borrow analysis.
5-
#[derive(Clone, Debug)]
6-
pub struct AllFacts<T: FactTypes> {
7-
/// `loan_issued_at(origin, loan, point)` indicates that the `loan` was "issued"
8-
/// at the given `point`, creating a reference with the `origin`.
9-
/// Effectively, `origin` may refer to data from `loan` starting at `point` (this is usually
10-
/// the point *after* a borrow rvalue).
11-
pub loan_issued_at: Vec<(T::Origin, T::Loan, T::Point)>,
12-
13-
/// `universal_region(origin)` -- this is a "free region" within fn body
14-
pub universal_region: Vec<(T::Origin,)>,
15-
16-
/// `cfg_edge(point1, point2)` for each edge `point1 -> point2` in the control flow
17-
pub cfg_edge: Vec<(T::Point, T::Point)>,
18-
19-
/// `loan_killed_at(loan, point)` when some prefix of the path borrowed at `loan`
20-
/// is assigned at `point`.
21-
/// Indicates that the path borrowed by the `loan` has changed in some way that the loan no
22-
/// longer needs to be tracked. (In particular, mutations to the path that was borrowed
23-
/// no longer invalidate the loan)
24-
pub loan_killed_at: Vec<(T::Loan, T::Point)>,
25-
26-
/// `subset_base(origin1, origin2, point)` when we require `origin1@point: origin2@point`.
27-
/// Indicates that `origin1 <= origin2` -- i.e., the set of loans in `origin1` are a subset
28-
/// of those in `origin2`.
29-
pub subset_base: Vec<(T::Origin, T::Origin, T::Point)>,
30-
31-
/// `loan_invalidated_at(point, loan)` indicates that the `loan` is invalidated by some action
32-
/// taking place at `point`; if any origin that references this loan is live, this is an error.
33-
pub loan_invalidated_at: Vec<(T::Point, T::Loan)>,
34-
35-
/// `var_used_at(var, point)` when the variable `var` is used for anything
36-
/// but a drop at `point`
37-
pub var_used_at: Vec<(T::Variable, T::Point)>,
38-
39-
/// `var_defined_at(var, point)` when the variable `var` is overwritten at `point`
40-
pub var_defined_at: Vec<(T::Variable, T::Point)>,
41-
42-
/// `var_dropped_at(var, point)` when the variable `var` is used in a drop at `point`
43-
pub var_dropped_at: Vec<(T::Variable, T::Point)>,
44-
45-
/// `use_of_var_derefs_origin(variable, origin)`: References with the given
46-
/// `origin` may be dereferenced when the `variable` is used.
47-
///
48-
/// In rustc, we generate this whenever the type of the variable includes the
49-
/// given origin.
50-
pub use_of_var_derefs_origin: Vec<(T::Variable, T::Origin)>,
51-
52-
/// `drop_of_var_derefs_origin(var, origin)` when the type of `var` includes
53-
/// the `origin` and uses it when dropping
54-
pub drop_of_var_derefs_origin: Vec<(T::Variable, T::Origin)>,
55-
56-
/// `child_path(child, parent)` when the path `child` is the direct child of
57-
/// `parent`, e.g. `child_path(x.y, x)`, but not `child_path(x.y.z, x)`.
58-
pub child_path: Vec<(T::Path, T::Path)>,
59-
60-
/// `path_is_var(path, var)` the root path `path` starting in variable `var`.
61-
pub path_is_var: Vec<(T::Path, T::Variable)>,
62-
63-
/// `path_assigned_at_base(path, point)` when the `path` was initialized at point
64-
/// `point`. This fact is only emitted for a prefix `path`, and not for the
65-
/// implicit initialization of all of `path`'s children. E.g. a statement like
66-
/// `x.y = 3` at `point` would give the fact `path_assigned_at_base(x.y, point)` (but
67-
/// neither `path_assigned_at_base(x.y.z, point)` nor `path_assigned_at_base(x, point)`).
68-
pub path_assigned_at_base: Vec<(T::Path, T::Point)>,
69-
70-
/// `path_moved_at_base(path, point)` when the `path` was moved at `point`. The
71-
/// same logic is applied as for `path_assigned_at_base` above.
72-
pub path_moved_at_base: Vec<(T::Path, T::Point)>,
73-
74-
/// `path_accessed_at_base(path, point)` when the `path` was accessed at point
75-
/// `point`. The same logic as for `path_assigned_at_base` and `path_moved_at_base` applies.
76-
pub path_accessed_at_base: Vec<(T::Path, T::Point)>,
77-
78-
/// These reflect the `'a: 'b` relations that are either declared by the user on function
79-
/// declarations or which are inferred via implied bounds.
80-
/// For example: `fn foo<'a, 'b: 'a, 'c>(x: &'c &'a u32)` would have two entries:
81-
/// - one for the user-supplied subset `'b: 'a`
82-
/// - and one for the `'a: 'c` implied bound from the `x` parameter,
83-
/// (note that the transitive relation `'b: 'c` is not necessarily included
84-
/// explicitly, but rather inferred by polonius).
85-
pub known_placeholder_subset: Vec<(T::Origin, T::Origin)>,
86-
87-
/// `placeholder(origin, loan)` describes a placeholder `origin`, with its associated
88-
/// placeholder `loan`.
89-
pub placeholder: Vec<(T::Origin, T::Loan)>,
90-
}
91-
92-
impl<T: FactTypes> Default for AllFacts<T> {
93-
fn default() -> Self {
94-
AllFacts {
95-
loan_issued_at: Vec::default(),
96-
universal_region: Vec::default(),
97-
cfg_edge: Vec::default(),
98-
loan_killed_at: Vec::default(),
99-
subset_base: Vec::default(),
100-
loan_invalidated_at: Vec::default(),
101-
var_used_at: Vec::default(),
102-
var_defined_at: Vec::default(),
103-
var_dropped_at: Vec::default(),
104-
use_of_var_derefs_origin: Vec::default(),
105-
drop_of_var_derefs_origin: Vec::default(),
106-
child_path: Vec::default(),
107-
path_is_var: Vec::default(),
108-
path_assigned_at_base: Vec::default(),
109-
path_moved_at_base: Vec::default(),
110-
path_accessed_at_base: Vec::default(),
111-
known_placeholder_subset: Vec::default(),
112-
placeholder: Vec::default(),
113-
}
114-
}
115-
}
116-
117-
pub trait Atom:
118-
From<usize> + Into<usize> + Copy + Clone + Debug + Eq + Ord + Hash + 'static
119-
{
120-
fn index(self) -> usize;
121-
}
122-
123-
pub trait FactTypes: Copy + Clone + Debug {
124-
type Origin: Atom;
125-
type Loan: Atom;
126-
type Point: Atom;
127-
type Variable: Atom;
128-
type Path: Atom;
129-
}
1+
pub use polonius_facts::*;

polonius-engine/src/lib.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ extern crate datafrog;
44
#[macro_use]
55
extern crate log;
66
extern crate rustc_hash;
7+
extern crate polonius_facts;
78

89
mod facts;
910
mod output;

polonius-souffle/Cargo.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ build = "build.rs"
1515
[dependencies]
1616
cxx = "1.0.50"
1717
log = "0.4"
18-
polonius-engine = { path = "../polonius-engine" }
18+
polonius-facts = { path = "../polonius-facts" }
1919

2020
[build-dependencies]
2121
cc = "1.0.69"

polonius-souffle/src/facts.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ use std::convert::TryInto;
22
use std::pin::Pin;
33

44
use log::warn;
5-
use polonius_engine::{AllFacts, FactTypes};
5+
use polonius_facts::{AllFacts, FactTypes};
66

77
use crate::ffi::{self, InsertIntoRelation};
88

polonius-souffle/src/lib.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ use std::collections::HashMap;
77
use std::path::Path;
88

99
use cxx::let_cxx_string;
10-
use polonius_engine::{AllFacts, FactTypes};
10+
use polonius_facts::{AllFacts, FactTypes};
1111

1212
pub fn run_from_dir(prog: &str, facts_dir: &Path) {
1313
let_cxx_string!(facts = facts_dir.to_string_lossy().as_bytes());

0 commit comments

Comments
 (0)