Skip to content

Commit c9ecc9b

Browse files
authored
Merge pull request #130 from csmoe/factypes
replace fact type parameters with FactTypes
2 parents b688fb5 + 4cf4dbe commit c9ecc9b

File tree

11 files changed

+170
-192
lines changed

11 files changed

+170
-192
lines changed

polonius-engine/src/facts.rs

Lines changed: 26 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -3,70 +3,68 @@ use std::hash::Hash;
33

44
/// The "facts" which are the basis of the NLL borrow analysis.
55
#[derive(Clone, Debug)]
6-
pub struct AllFacts<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, MovePath: Atom> {
6+
pub struct AllFacts<T: FactTypes> {
77
/// `borrow_region(O, L, P)` -- the origin `O` may refer to data
88
/// from loan `L` starting at the point `P` (this is usually the
99
/// point *after* a borrow rvalue)
10-
pub borrow_region: Vec<(Origin, Loan, Point)>,
10+
pub borrow_region: Vec<(T::Origin, T::Loan, T::Point)>,
1111

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

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

1818
/// `killed(L, P)` when some prefix of the path borrowed at `L` is assigned at point `P`
19-
pub killed: Vec<(Loan, Point)>,
19+
pub killed: Vec<(T::Loan, T::Point)>,
2020

2121
/// `outlives(O1, P2, P)` when we require `O1@P: O2@P`
22-
pub outlives: Vec<(Origin, Origin, Point)>,
22+
pub outlives: Vec<(T::Origin, T::Origin, T::Point)>,
2323

2424
/// `invalidates(P, L)` when the loan `L` is invalidated at point `P`
25-
pub invalidates: Vec<(Point, Loan)>,
25+
pub invalidates: Vec<(T::Point, T::Loan)>,
2626

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

3030
/// `var_defined(V, P)` when the variable `V` is overwritten by the point `P`
31-
pub var_defined: Vec<(Variable, Point)>,
31+
pub var_defined: Vec<(T::Variable, T::Point)>,
3232

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

3636
/// `var_uses_region(V, O)` when the type of `V` includes the origin `O`
37-
pub var_uses_region: Vec<(Variable, Origin)>,
37+
pub var_uses_region: Vec<(T::Variable, T::Origin)>,
3838

3939
/// `var_drops_region(V, O)` when the type of `V` includes the origin `O` and uses
4040
/// it when dropping
41-
pub var_drops_region: Vec<(Variable, Origin)>,
41+
pub var_drops_region: Vec<(T::Variable, T::Origin)>,
4242

4343
/// `child(M1, M2)` when the move path `M1` is the direct or transitive child
4444
/// of `M2`, e.g. `child(x.y, x)`, `child(x.y.z, x.y)`, `child(x.y.z, x)`
4545
/// would all be true if there was a path like `x.y.z`.
46-
pub child: Vec<(MovePath, MovePath)>,
46+
pub child: Vec<(T::MovePath, T::MovePath)>,
4747

4848
/// `path_belongs_to_var(M, V)` the root path `M` starting in variable `V`.
49-
pub path_belongs_to_var: Vec<(MovePath, Variable)>,
49+
pub path_belongs_to_var: Vec<(T::MovePath, T::Variable)>,
5050

5151
/// `initialized_at(M, P)` when the move path `M` was initialized at point
5252
/// `P`. This fact is only emitted for a prefix `M`, and not for the
5353
/// implicit initialization of all of `M`'s children. E.g. a statement like
5454
/// `x.y = 3` at point `P` would give the fact `initialized_at(x.y, P)` (but
5555
/// neither `initialized_at(x.y.z, P)` nor `initialized_at(x, P)`).
56-
pub initialized_at: Vec<(MovePath, Point)>,
56+
pub initialized_at: Vec<(T::MovePath, T::Point)>,
5757

5858
/// `moved_out_at(M, P)` when the move path `M` was moved at point `P`. The
5959
/// same logic is applied as for `initialized_at` above.
60-
pub moved_out_at: Vec<(MovePath, Point)>,
60+
pub moved_out_at: Vec<(T::MovePath, T::Point)>,
6161

6262
/// `path_accessed_at(M, P)` when the move path `M` was accessed at point
6363
/// `P`. The same logic as for `initialized_at` and `moved_out_at` applies.
64-
pub path_accessed_at: Vec<(MovePath, Point)>,
64+
pub path_accessed_at: Vec<(T::MovePath, T::Point)>,
6565
}
6666

67-
impl<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, MovePath: Atom> Default
68-
for AllFacts<Origin, Loan, Point, Variable, MovePath>
69-
{
67+
impl<T: FactTypes> Default for AllFacts<T> {
7068
fn default() -> Self {
7169
AllFacts {
7270
borrow_region: Vec::default(),
@@ -94,3 +92,11 @@ pub trait Atom:
9492
{
9593
fn index(self) -> usize;
9694
}
95+
96+
pub trait FactTypes: Copy + Clone + Debug {
97+
type Origin: Atom;
98+
type Loan: Atom;
99+
type Point: Atom;
100+
type Variable: Atom;
101+
type MovePath: Atom;
102+
}

polonius-engine/src/lib.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,5 +11,6 @@ mod output;
1111
// Reexports of facts
1212
pub use facts::AllFacts;
1313
pub use facts::Atom;
14+
pub use facts::FactTypes;
1415
pub use output::Algorithm;
1516
pub use output::Output;

polonius-engine/src/output/datafrog_opt.rs

Lines changed: 24 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -16,12 +16,9 @@ use crate::output::liveness;
1616
use crate::output::Output;
1717

1818
use datafrog::{Iteration, Relation, RelationLeaper};
19-
use facts::{AllFacts, Atom};
19+
use facts::{AllFacts, FactTypes};
2020

21-
pub(super) fn compute<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, MovePath: Atom>(
22-
dump_enabled: bool,
23-
all_facts: AllFacts<Origin, Loan, Point, Variable, MovePath>,
24-
) -> Output<Origin, Loan, Point, Variable, MovePath> {
21+
pub(super) fn compute<T: FactTypes>(dump_enabled: bool, all_facts: AllFacts<T>) -> Output<T> {
2522
let mut result = Output::new(dump_enabled);
2623

2724
let var_maybe_initialized_on_exit = initialization::init_var_maybe_initialized_on_exit(
@@ -55,33 +52,35 @@ pub(super) fn compute<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, Mov
5552
// static inputs
5653
let cfg_edge_rel = Relation::from_iter(all_facts.cfg_edge.iter().map(|&(p, q)| (p, q)));
5754

58-
let killed_rel: Relation<(Loan, Point)> = all_facts.killed.into();
55+
let killed_rel: Relation<(T::Loan, T::Point)> = all_facts.killed.into();
5956

6057
// `invalidates` facts, stored ready for joins
61-
let invalidates = iteration.variable::<((Loan, Point), ())>("invalidates");
58+
let invalidates = iteration.variable::<((T::Loan, T::Point), ())>("invalidates");
6259

6360
// we need `region_live_at` in both variable and relation forms.
6461
// (respectively, for join and antijoin).
65-
let region_live_at_rel: Relation<(Origin, Point)> = region_live_at.into();
66-
let region_live_at_var = iteration.variable::<((Origin, Point), ())>("region_live_at");
62+
let region_live_at_rel: Relation<(T::Origin, T::Point)> = region_live_at.into();
63+
let region_live_at_var =
64+
iteration.variable::<((T::Origin, T::Point), ())>("region_live_at");
6765

6866
// `borrow_region` input but organized for join
69-
let borrow_region_rp = iteration.variable::<((Origin, Point), Loan)>("borrow_region_rp");
67+
let borrow_region_rp =
68+
iteration.variable::<((T::Origin, T::Point), T::Loan)>("borrow_region_rp");
7069

7170
// .decl subset(R1, R2, P)
7271
//
7372
// Indicates that `R1: R2` at the point `P`.
74-
let subset_r1p = iteration.variable::<((Origin, Point), Origin)>("subset_r1p");
73+
let subset_r1p = iteration.variable::<((T::Origin, T::Point), T::Origin)>("subset_r1p");
7574

7675
// .decl requires(R, B, P)
7776
//
7877
// At the point, things with origin R may depend on data from
7978
// borrow B
80-
let requires_rp = iteration.variable::<((Origin, Point), Loan)>("requires_rp");
79+
let requires_rp = iteration.variable::<((T::Origin, T::Point), T::Loan)>("requires_rp");
8180

8281
// .decl borrow_live_at(B, P) -- true if the restrictions of the borrow B
8382
// need to be enforced at the point P
84-
let borrow_live_at = iteration.variable::<((Loan, Point), ())>("borrow_live_at");
83+
let borrow_live_at = iteration.variable::<((T::Loan, T::Point), ())>("borrow_live_at");
8584

8685
// .decl live_to_dying_regions(R1, R2, P, Q)
8786
//
@@ -94,23 +93,23 @@ pub(super) fn compute<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, Mov
9493
// In that case, `Q` would like to add all the
9594
// live things reachable from `R2` to `R1`.
9695
//
97-
let live_to_dying_regions_r2pq =
98-
iteration.variable::<((Origin, Point, Point), Origin)>("live_to_dying_regions_r2pq");
96+
let live_to_dying_regions_r2pq = iteration
97+
.variable::<((T::Origin, T::Point, T::Point), T::Origin)>("live_to_dying_regions_r2pq");
9998

10099
// .decl dying_region_requires((R, P, Q), B)
101100
//
102101
// The origin `R` requires the borrow `B`, but the
103102
// origin `R` goes dead along the edge `P -> Q`
104-
let dying_region_requires =
105-
iteration.variable::<((Origin, Point, Point), Loan)>("dying_region_requires");
103+
let dying_region_requires = iteration
104+
.variable::<((T::Origin, T::Point, T::Point), T::Loan)>("dying_region_requires");
106105

107106
// .decl dying_can_reach_origins(R, P, Q)
108107
//
109108
// Contains dead regions where we are interested
110109
// in computing the transitive closure of things they
111110
// can reach.
112111
let dying_can_reach_origins =
113-
iteration.variable::<((Origin, Point), Point)>("dying_can_reach_origins");
112+
iteration.variable::<((T::Origin, T::Point), T::Point)>("dying_can_reach_origins");
114113

115114
// .decl dying_can_reach(R1, R2, P, Q)
116115
//
@@ -121,7 +120,7 @@ pub(super) fn compute<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, Mov
121120
// relation, but we try to limit it to regions
122121
// that are dying on the edge P -> Q.
123122
let dying_can_reach_r2q =
124-
iteration.variable::<((Origin, Point), (Origin, Point))>("dying_can_reach");
123+
iteration.variable::<((T::Origin, T::Point), (T::Origin, T::Point))>("dying_can_reach");
125124
let dying_can_reach_1 = iteration.variable_indistinct("dying_can_reach_1");
126125

127126
// .decl dying_can_reach_live(R1, R2, P, Q)
@@ -131,19 +130,19 @@ pub(super) fn compute<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, Mov
131130
// relation. This is a subset of the full `dying_can_reach`
132131
// relation where we filter down to those cases where R2 is
133132
// live in Q.
134-
let dying_can_reach_live =
135-
iteration.variable::<((Origin, Point, Point), Origin)>("dying_can_reach_live");
133+
let dying_can_reach_live = iteration
134+
.variable::<((T::Origin, T::Point, T::Point), T::Origin)>("dying_can_reach_live");
136135

137136
// .decl dead_borrow_region_can_reach_root((R, P), B)
138137
//
139138
// Indicates a "borrow region" R at P which is not live on
140139
// entry to P.
141-
let dead_borrow_region_can_reach_root =
142-
iteration.variable::<((Origin, Point), Loan)>("dead_borrow_region_can_reach_root");
140+
let dead_borrow_region_can_reach_root = iteration
141+
.variable::<((T::Origin, T::Point), T::Loan)>("dead_borrow_region_can_reach_root");
143142

144143
// .decl dead_borrow_region_can_reach_dead((R2, P), B)
145-
let dead_borrow_region_can_reach_dead =
146-
iteration.variable::<((Origin, Point), Loan)>("dead_borrow_region_can_reach_dead");
144+
let dead_borrow_region_can_reach_dead = iteration
145+
.variable::<((T::Origin, T::Point), T::Loan)>("dead_borrow_region_can_reach_dead");
147146
let dead_borrow_region_can_reach_dead_1 =
148147
iteration.variable_indistinct("dead_borrow_region_can_reach_dead_1");
149148

polonius-engine/src/output/hybrid.rs

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -14,12 +14,9 @@
1414
use crate::output::datafrog_opt;
1515
use crate::output::location_insensitive;
1616
use crate::output::Output;
17-
use facts::{AllFacts, Atom};
17+
use facts::{AllFacts, FactTypes};
1818

19-
pub(super) fn compute<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, MovePath: Atom>(
20-
dump_enabled: bool,
21-
all_facts: AllFacts<Origin, Loan, Point, Variable, MovePath>,
22-
) -> Output<Origin, Loan, Point, Variable, MovePath> {
19+
pub(super) fn compute<T: FactTypes>(dump_enabled: bool, all_facts: AllFacts<T>) -> Output<T> {
2320
let lins_output = location_insensitive::compute(dump_enabled, &all_facts);
2421
if lins_output.errors.is_empty() {
2522
lins_output

polonius-engine/src/output/initialization.rs

Lines changed: 19 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -1,50 +1,43 @@
11
use std::time::Instant;
22

33
use crate::output::Output;
4-
use facts::Atom;
4+
use facts::FactTypes;
55

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

8-
pub(super) fn init_var_maybe_initialized_on_exit<Origin, Loan, Point, Variable, MovePath>(
9-
child: Vec<(MovePath, MovePath)>,
10-
path_belongs_to_var: Vec<(MovePath, Variable)>,
11-
initialized_at: Vec<(MovePath, Point)>,
12-
moved_out_at: Vec<(MovePath, Point)>,
13-
path_accessed_at: Vec<(MovePath, Point)>,
14-
cfg_edge: &[(Point, Point)],
15-
output: &mut Output<Origin, Loan, Point, Variable, MovePath>,
16-
) -> Vec<(Variable, Point)>
17-
where
18-
Origin: Atom,
19-
Loan: Atom,
20-
Point: Atom,
21-
Variable: Atom,
22-
MovePath: Atom,
23-
{
8+
pub(super) fn init_var_maybe_initialized_on_exit<T: FactTypes>(
9+
child: Vec<(T::MovePath, T::MovePath)>,
10+
path_belongs_to_var: Vec<(T::MovePath, T::Variable)>,
11+
initialized_at: Vec<(T::MovePath, T::Point)>,
12+
moved_out_at: Vec<(T::MovePath, T::Point)>,
13+
path_accessed_at: Vec<(T::MovePath, T::Point)>,
14+
cfg_edge: &[(T::Point, T::Point)],
15+
output: &mut Output<T>,
16+
) -> Vec<(T::Variable, T::Point)> {
2417
debug!("compute_initialization()");
2518
let computation_start = Instant::now();
2619
let mut iteration = Iteration::new();
2720

2821
// Relations
29-
//let parent: Relation<(MovePath, MovePath)> = child.iter().map(|&(c, p)| (p, c)).collect();
30-
let child: Relation<(MovePath, MovePath)> = child.into();
31-
let path_belongs_to_var: Relation<(MovePath, Variable)> = path_belongs_to_var.into();
32-
let initialized_at: Relation<(MovePath, Point)> = initialized_at.into();
33-
let moved_out_at: Relation<(MovePath, Point)> = moved_out_at.into();
34-
let cfg_edge: Relation<(Point, Point)> = cfg_edge.iter().cloned().collect();
35-
let _path_accessed_at: Relation<(MovePath, Point)> = path_accessed_at.into();
22+
//let parent: Relation<(T::MovePath, T::MovePath)> = child.iter().map(|&(c, p)| (p, c)).collect();
23+
let child: Relation<(T::MovePath, T::MovePath)> = child.into();
24+
let path_belongs_to_var: Relation<(T::MovePath, T::Variable)> = path_belongs_to_var.into();
25+
let initialized_at: Relation<(T::MovePath, T::Point)> = initialized_at.into();
26+
let moved_out_at: Relation<(T::MovePath, T::Point)> = moved_out_at.into();
27+
let cfg_edge: Relation<(T::Point, T::Point)> = cfg_edge.iter().cloned().collect();
28+
let _path_accessed_at: Relation<(T::MovePath, T::Point)> = path_accessed_at.into();
3629

3730
// Variables
3831

3932
// var_maybe_initialized_on_exit(V, P): Upon leaving `P`, at least one part of the
4033
// variable `V` might be initialized for some path through the CFG.
4134
let var_maybe_initialized_on_exit =
42-
iteration.variable::<(Variable, Point)>("var_maybe_initialized_on_exit");
35+
iteration.variable::<(T::Variable, T::Point)>("var_maybe_initialized_on_exit");
4336

4437
// path_maybe_initialized_on_exit(M, P): Upon leaving `P`, the move path `M`
4538
// might be *partially* initialized for some path through the CFG.
4639
let path_maybe_initialized_on_exit =
47-
iteration.variable::<(MovePath, Point)>("path_maybe_initialized_on_exit");
40+
iteration.variable::<(T::MovePath, T::Point)>("path_maybe_initialized_on_exit");
4841

4942
// Initial propagation of static relations
5043

0 commit comments

Comments
 (0)