Skip to content

Commit a05aea4

Browse files
authored
Merge pull request #125 from lqd/a_region_has_no_name
Clean up terminology: step 1 — rename `Region` to `Origin`
2 parents 575f6d1 + 7002550 commit a05aea4

16 files changed

+175
-176
lines changed

polonius-engine/src/facts.rs

Lines changed: 38 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -3,68 +3,70 @@ 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<R: Atom, L: Atom, P: Atom, V: Atom, M: Atom> {
7-
/// `borrow_region(R, B, P)` -- the region R may refer to data
8-
/// from borrow B starting at the point P (this is usually the
6+
pub struct AllFacts<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, MovePath: Atom> {
7+
/// `borrow_region(O, L, P)` -- the origin `O` may refer to data
8+
/// from loan `L` starting at the point `P` (this is usually the
99
/// point *after* a borrow rvalue)
10-
pub borrow_region: Vec<(R, L, P)>,
10+
pub borrow_region: Vec<(Origin, Loan, Point)>,
1111

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

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

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

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

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

27-
/// `var_used(V, P) when the variable V is used for anything but a drop at point P`
28-
pub var_used: Vec<(V, P)>,
27+
/// `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)>,
2929

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

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

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

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

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

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

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

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

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

67-
impl<R: Atom, L: Atom, P: Atom, V: Atom, M: Atom> Default for AllFacts<R, L, P, V, M> {
67+
impl<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, MovePath: Atom> Default
68+
for AllFacts<Origin, Loan, Point, Variable, MovePath>
69+
{
6870
fn default() -> Self {
6971
AllFacts {
7072
borrow_region: Vec::default(),

polonius-engine/src/output/datafrog_opt.rs

Lines changed: 27 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -18,10 +18,10 @@ use crate::output::Output;
1818
use datafrog::{Iteration, Relation, RelationLeaper};
1919
use facts::{AllFacts, Atom};
2020

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

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

6363
// we need `region_live_at` in both variable and relation forms.
6464
// (respectively, for join and antijoin).
65-
let region_live_at_rel: Relation<(Region, Point)> = region_live_at.into();
66-
let region_live_at_var = iteration.variable::<((Region, Point), ())>("region_live_at");
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");
6767

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

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

7676
// .decl requires(R, B, P)
7777
//
78-
// At the point, things with region R may depend on data from
78+
// At the point, things with origin R may depend on data from
7979
// borrow B
80-
let requires_rp = iteration.variable::<((Region, Point), Loan)>("requires_rp");
80+
let requires_rp = iteration.variable::<((Origin, Point), Loan)>("requires_rp");
8181

8282
// .decl borrow_live_at(B, P) -- true if the restrictions of the borrow B
8383
// need to be enforced at the point P
@@ -95,55 +95,55 @@ pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom, Variable: Atom, Mov
9595
// live things reachable from `R2` to `R1`.
9696
//
9797
let live_to_dying_regions_r2pq =
98-
iteration.variable::<((Region, Point, Point), Region)>("live_to_dying_regions_r2pq");
98+
iteration.variable::<((Origin, Point, Point), Origin)>("live_to_dying_regions_r2pq");
9999

100100
// .decl dying_region_requires((R, P, Q), B)
101101
//
102-
// The region `R` requires the borrow `B`, but the
103-
// region `R` goes dead along the edge `P -> Q`
102+
// The origin `R` requires the borrow `B`, but the
103+
// origin `R` goes dead along the edge `P -> Q`
104104
let dying_region_requires =
105-
iteration.variable::<((Region, Point, Point), Loan)>("dying_region_requires");
105+
iteration.variable::<((Origin, Point, Point), Loan)>("dying_region_requires");
106106

107107
// .decl dying_can_reach_origins(R, P, Q)
108108
//
109109
// Contains dead regions where we are interested
110110
// in computing the transitive closure of things they
111111
// can reach.
112112
let dying_can_reach_origins =
113-
iteration.variable::<((Region, Point), Point)>("dying_can_reach_origins");
113+
iteration.variable::<((Origin, Point), Point)>("dying_can_reach_origins");
114114

115115
// .decl dying_can_reach(R1, R2, P, Q)
116116
//
117-
// Indicates that the region `R1`, which is dead
118-
// in `Q`, can reach the region `R2` in P.
117+
// Indicates that the origin `R1`, which is dead
118+
// in `Q`, can reach the origin `R2` in P.
119119
//
120120
// This is effectively the transitive subset
121121
// relation, but we try to limit it to regions
122122
// that are dying on the edge P -> Q.
123123
let dying_can_reach_r2q =
124-
iteration.variable::<((Region, Point), (Region, Point))>("dying_can_reach");
124+
iteration.variable::<((Origin, Point), (Origin, Point))>("dying_can_reach");
125125
let dying_can_reach_1 = iteration.variable_indistinct("dying_can_reach_1");
126126

127127
// .decl dying_can_reach_live(R1, R2, P, Q)
128128
//
129129
// Indicates that, along the edge `P -> Q`, the dead (in Q)
130-
// region R1 can reach the live (in Q) region R2 via a subset
130+
// origin R1 can reach the live (in Q) origin R2 via a subset
131131
// relation. This is a subset of the full `dying_can_reach`
132132
// relation where we filter down to those cases where R2 is
133133
// live in Q.
134134
let dying_can_reach_live =
135-
iteration.variable::<((Region, Point, Point), Region)>("dying_can_reach_live");
135+
iteration.variable::<((Origin, Point, Point), Origin)>("dying_can_reach_live");
136136

137137
// .decl dead_borrow_region_can_reach_root((R, P), B)
138138
//
139139
// Indicates a "borrow region" R at P which is not live on
140140
// entry to P.
141141
let dead_borrow_region_can_reach_root =
142-
iteration.variable::<((Region, Point), Loan)>("dead_borrow_region_can_reach_root");
142+
iteration.variable::<((Origin, Point), Loan)>("dead_borrow_region_can_reach_root");
143143

144144
// .decl dead_borrow_region_can_reach_dead((R2, P), B)
145145
let dead_borrow_region_can_reach_dead =
146-
iteration.variable::<((Region, Point), Loan)>("dead_borrow_region_can_reach_dead");
146+
iteration.variable::<((Origin, Point), Loan)>("dead_borrow_region_can_reach_dead");
147147
let dead_borrow_region_can_reach_dead_1 =
148148
iteration.variable_indistinct("dead_borrow_region_can_reach_dead_1");
149149

@@ -234,7 +234,7 @@ pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom, Variable: Atom, Mov
234234
//
235235
// This is the "transitive closure" rule, but
236236
// note that we only apply it with the
237-
// "intermediate" region R2 is dead at Q.
237+
// "intermediate" origin R2 is dead at Q.
238238
dying_can_reach_1.from_antijoin(
239239
&dying_can_reach_r2q,
240240
&region_live_at_rel,
@@ -288,7 +288,7 @@ pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom, Variable: Atom, Mov
288288
//
289289
// Communicate a `R1 requires B` relation across
290290
// an edge `P -> Q` where `R1` is dead in Q; in
291-
// that case, for each region `R2` live in `Q`
291+
// that case, for each origin `R2` live in `Q`
292292
// where `R1 <= R2` in P, we add `R2 requires B`
293293
// to `Q`.
294294
requires_rp.from_join(
@@ -366,12 +366,12 @@ pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom, Variable: Atom, Mov
366366
}
367367

368368
if dump_enabled {
369-
for (region, location) in &region_live_at_rel.elements {
369+
for (origin, location) in &region_live_at_rel.elements {
370370
result
371371
.region_live_at
372372
.entry(*location)
373373
.or_insert(vec![])
374-
.push(*region);
374+
.push(*origin);
375375
}
376376

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

392392
let requires_rp = requires_rp.complete();
393-
for ((region, location), borrow) in &requires_rp.elements {
393+
for ((origin, location), borrow) in &requires_rp.elements {
394394
result
395395
.restricts
396396
.entry(*location)
397397
.or_insert(BTreeMap::new())
398-
.entry(*region)
398+
.entry(*origin)
399399
.or_insert(BTreeSet::new())
400400
.insert(*borrow);
401401
}

polonius-engine/src/output/hybrid.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,10 +16,10 @@ use crate::output::location_insensitive;
1616
use crate::output::Output;
1717
use facts::{AllFacts, Atom};
1818

19-
pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom, Variable: Atom, MovePath: Atom>(
19+
pub(super) fn compute<Origin: Atom, Loan: Atom, Point: Atom, Variable: Atom, MovePath: Atom>(
2020
dump_enabled: bool,
21-
all_facts: AllFacts<Region, Loan, Point, Variable, MovePath>,
22-
) -> Output<Region, Loan, Point, Variable, MovePath> {
21+
all_facts: AllFacts<Origin, Loan, Point, Variable, MovePath>,
22+
) -> Output<Origin, Loan, Point, Variable, MovePath> {
2323
let lins_output = location_insensitive::compute(dump_enabled, &all_facts);
2424
if lins_output.errors.is_empty() {
2525
lins_output

polonius-engine/src/output/initialization.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,17 +5,17 @@ use facts::Atom;
55

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

8-
pub(super) fn init_var_maybe_initialized_on_exit<Region, Loan, Point, Variable, MovePath>(
8+
pub(super) fn init_var_maybe_initialized_on_exit<Origin, Loan, Point, Variable, MovePath>(
99
child: Vec<(MovePath, MovePath)>,
1010
path_belongs_to_var: Vec<(MovePath, Variable)>,
1111
initialized_at: Vec<(MovePath, Point)>,
1212
moved_out_at: Vec<(MovePath, Point)>,
1313
path_accessed_at: Vec<(MovePath, Point)>,
1414
cfg_edge: &[(Point, Point)],
15-
output: &mut Output<Region, Loan, Point, Variable, MovePath>,
15+
output: &mut Output<Origin, Loan, Point, Variable, MovePath>,
1616
) -> Vec<(Variable, Point)>
1717
where
18-
Region: Atom,
18+
Origin: Atom,
1919
Loan: Atom,
2020
Point: Atom,
2121
Variable: Atom,

polonius-engine/src/output/liveness.rs

Lines changed: 19 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88
// option. This file may not be copied, modified, or distributed
99
// except according to those terms.
1010

11-
//! An implementation of the region liveness calculation logic
11+
//! An implementation of the origin liveness calculation logic
1212
1313
use std::collections::BTreeSet;
1414
use std::time::Instant;
@@ -18,18 +18,18 @@ use facts::Atom;
1818

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

21-
pub(super) fn compute_live_regions<Region, Loan, Point, Variable, MovePath>(
21+
pub(super) fn compute_live_regions<Origin, Loan, Point, Variable, MovePath>(
2222
var_used: Vec<(Variable, Point)>,
2323
var_drop_used: Vec<(Variable, Point)>,
2424
var_defined: Vec<(Variable, Point)>,
25-
var_uses_region: Vec<(Variable, Region)>,
26-
var_drops_region: Vec<(Variable, Region)>,
25+
var_uses_region: Vec<(Variable, Origin)>,
26+
var_drops_region: Vec<(Variable, Origin)>,
2727
cfg_edge: &[(Point, Point)],
2828
var_maybe_initialized_on_exit: Vec<(Variable, Point)>,
29-
output: &mut Output<Region, Loan, Point, Variable, MovePath>,
30-
) -> Vec<(Region, Point)>
29+
output: &mut Output<Origin, Loan, Point, Variable, MovePath>,
30+
) -> Vec<(Origin, Point)>
3131
where
32-
Region: Atom,
32+
Origin: Atom,
3333
Loan: Atom,
3434
Point: Atom,
3535
Variable: Atom,
@@ -44,8 +44,8 @@ where
4444
let cfg_edge_rel: Relation<(Point, Point)> = cfg_edge.iter().map(|(p, q)| (*p, *q)).collect();
4545
let cfg_edge_reverse_rel: Relation<(Point, Point)> =
4646
cfg_edge.iter().map(|(p, q)| (*q, *p)).collect();
47-
let var_uses_region_rel: Relation<(Variable, Region)> = var_uses_region.into();
48-
let var_drops_region_rel: Relation<(Variable, Region)> = var_drops_region.into();
47+
let var_uses_region_rel: Relation<(Variable, Origin)> = var_uses_region.into();
48+
let var_drops_region_rel: Relation<(Variable, Origin)> = var_drops_region.into();
4949
let var_maybe_initialized_on_exit_rel: Relation<(Variable, Point)> =
5050
var_maybe_initialized_on_exit.into();
5151
let var_drop_used_rel: Relation<((Variable, Point), ())> = var_drop_used
@@ -61,7 +61,7 @@ where
6161
let var_drop_live_var = iteration.variable::<(Variable, Point)>("var_drop_live_at");
6262

6363
// This is what we are actually calculating:
64-
let region_live_at_var = iteration.variable::<((Region, Point), ())>("region_live_at");
64+
let region_live_at_var = iteration.variable::<((Origin, Point), ())>("region_live_at");
6565

6666
// This propagates the relation `var_live(V, P) :- var_used(V, P)`:
6767
var_live_var.insert(var_used.into());
@@ -163,10 +163,10 @@ where
163163
.collect()
164164
}
165165

166-
pub(super) fn make_universal_region_live<Region: Atom, Point: Atom>(
167-
region_live_at: &mut Vec<(Region, Point)>,
166+
pub(super) fn make_universal_region_live<Origin: Atom, Point: Atom>(
167+
region_live_at: &mut Vec<(Origin, Point)>,
168168
cfg_edge: &[(Point, Point)],
169-
universal_region: Vec<Region>,
169+
universal_region: Vec<Origin>,
170170
) {
171171
debug!("make_universal_regions_live()");
172172

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

187187
pub(super) fn init_region_live_at<
188-
Region: Atom,
188+
Origin: Atom,
189189
Loan: Atom,
190190
Point: Atom,
191191
Variable: Atom,
@@ -194,13 +194,13 @@ pub(super) fn init_region_live_at<
194194
var_used: Vec<(Variable, Point)>,
195195
var_drop_used: Vec<(Variable, Point)>,
196196
var_defined: Vec<(Variable, Point)>,
197-
var_uses_region: Vec<(Variable, Region)>,
198-
var_drops_region: Vec<(Variable, Region)>,
197+
var_uses_region: Vec<(Variable, Origin)>,
198+
var_drops_region: Vec<(Variable, Origin)>,
199199
var_maybe_initialized_on_exit: Vec<(Variable, Point)>,
200200
cfg_edge: &[(Point, Point)],
201-
universal_region: Vec<Region>,
202-
output: &mut Output<Region, Loan, Point, Variable, MovePath>,
203-
) -> Vec<(Region, Point)> {
201+
universal_region: Vec<Origin>,
202+
output: &mut Output<Origin, Loan, Point, Variable, MovePath>,
203+
) -> Vec<(Origin, Point)> {
204204
debug!("init_region_live_at()");
205205
let mut region_live_at = compute_live_regions(
206206
var_used,

0 commit comments

Comments
 (0)