1 // Copyright 2017 The Rust Project Developers. See the COPYRIGHT
2 // file at the top-level directory of this distribution and at
3 // http://rust-lang.org/COPYRIGHT.
5 // Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
6 // http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
7 // <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
8 // option. This file may not be copied, modified, or distributed
9 // except according to those terms.
11 use std
::collections
::{BTreeMap, BTreeSet}
;
12 use std
::time
::Instant
;
14 use crate::output
::Output
;
16 use datafrog
::{Iteration, Relation}
;
17 use facts
::{AllFacts, Atom}
;
19 pub(super) fn compute
<Region
: Atom
, Loan
: Atom
, Point
: Atom
>(
21 mut all_facts
: AllFacts
<Region
, Loan
, Point
>,
22 ) -> Output
<Region
, Loan
, Point
> {
23 // Declare that each universal region is live at every point.
24 let all_points
: BTreeSet
<Point
> = all_facts
28 .chain(all_facts
.cfg_edge
.iter().map(|&(_
, q
)| q
))
31 for &r
in &all_facts
.universal_region
{
32 for &p
in &all_points
{
33 all_facts
.region_live_at
.push((r
, p
));
37 let timer
= Instant
::now();
39 let mut result
= Output
::new(dump_enabled
);
42 // Create a new iteration context, ...
43 let mut iteration
= Iteration
::new();
46 let cfg_edge
= iteration
.variable
::<(Point
, Point
)>("cfg_edge");
47 let killed
= all_facts
.killed
.into();
49 // `invalidates` facts, stored ready for joins
50 let invalidates
= iteration
.variable
::<((Loan
, Point
), ())>("invalidates");
52 // we need `region_live_at` in both variable and relation forms.
53 // (respectively, for join and antijoin).
54 let region_live_at_rel
=
55 Relation
::from(all_facts
.region_live_at
.iter().map(|&(r
, p
)| (r
, p
)));
56 let region_live_at_var
= iteration
.variable
::<((Region
, Point
), ())>("region_live_at");
58 // variables, indices for the computation rules, and temporaries for the multi-way joins
59 let subset
= iteration
.variable
::<(Region
, Region
, Point
)>("subset");
60 let subset_1
= iteration
.variable_indistinct("subset_1");
61 let subset_2
= iteration
.variable_indistinct("subset_2");
62 let subset_r1p
= iteration
.variable_indistinct("subset_r1p");
63 let subset_p
= iteration
.variable_indistinct("subset_p");
65 let requires
= iteration
.variable
::<(Region
, Loan
, Point
)>("requires");
66 let requires_1
= iteration
.variable_indistinct("requires_1");
67 let requires_2
= iteration
.variable_indistinct("requires_2");
68 let requires_bp
= iteration
.variable_indistinct("requires_bp");
69 let requires_rp
= iteration
.variable_indistinct("requires_rp");
71 let borrow_live_at
= iteration
.variable
::<((Loan
, Point
), ())>("borrow_live_at");
73 let live_to_dead_regions
=
74 iteration
.variable
::<(Region
, Region
, Point
, Point
)>("live_to_dead_regions");
75 let live_to_dead_regions_1
= iteration
.variable_indistinct("live_to_dead_regions_1");
76 let live_to_dead_regions_2
= iteration
.variable_indistinct("live_to_dead_regions_2");
77 let live_to_dead_regions_r2pq
= iteration
.variable_indistinct("live_to_dead_regions_r2pq");
79 let dead_region_requires
=
80 iteration
.variable
::<((Region
, Point
, Point
), Loan
)>("dead_region_requires");
81 let dead_region_requires_1
= iteration
.variable_indistinct("dead_region_requires_1");
82 let dead_region_requires_2
= iteration
.variable_indistinct("dead_region_requires_2");
84 let dead_can_reach_origins
=
85 iteration
.variable
::<((Region
, Point
), Point
)>("dead_can_reach_origins");
86 let dead_can_reach
= iteration
.variable
::<(Region
, Region
, Point
, Point
)>("dead_can_reach");
87 let dead_can_reach_1
= iteration
.variable_indistinct("dead_can_reach_1");
88 let dead_can_reach_r2q
= iteration
.variable_indistinct("dead_can_reach_r2q");
89 // nmatsakis: I tried to merge `dead_can_reach_r2q` and
90 // `dead_can_reach`, but the result was ever so slightly slower, at least on clap.
92 let dead_can_reach_live
=
93 iteration
.variable
::<((Region
, Point
, Point
), Region
)>("dead_can_reach_live");
94 let dead_can_reach_live_r1pq
= iteration
.variable_indistinct("dead_can_reach_live_r1pq");
97 let errors
= iteration
.variable("errors");
99 // load initial facts.
100 cfg_edge
.insert(all_facts
.cfg_edge
.into());
101 invalidates
.insert(Relation
::from(
102 all_facts
.invalidates
.iter().map(|&(p
, b
)| ((b
, p
), ())),
104 region_live_at_var
.insert(Relation
::from(
105 all_facts
.region_live_at
.iter().map(|&(r
, p
)| ((r
, p
), ())),
107 subset
.insert(all_facts
.outlives
.into());
108 requires
.insert(all_facts
.borrow_region
.into());
110 // .. and then start iterating rules!
111 while iteration
.changed() {
112 // remap fields to re-index by the different keys
113 subset_r1p
.from_map(&subset
, |&(r1
, r2
, p
)| ((r1
, p
), r2
));
114 subset_p
.from_map(&subset
, |&(r1
, r2
, p
)| (p
, (r1
, r2
)));
116 requires_bp
.from_map(&requires
, |&(r
, b
, p
)| ((b
, p
), r
));
117 requires_rp
.from_map(&requires
, |&(r
, b
, p
)| ((r
, p
), b
));
119 live_to_dead_regions_r2pq
120 .from_map(&live_to_dead_regions
, |&(r1
, r2
, p
, q
)| ((r2
, p
, q
), r1
));
122 dead_can_reach_r2q
.from_map(&dead_can_reach
, |&(r1
, r2
, p
, q
)| ((r2
, q
), (r1
, p
)));
123 dead_can_reach_live_r1pq
124 .from_map(&dead_can_reach_live
, |&((r1
, p
, q
), r2
)| ((r1
, p
, q
), r2
));
126 // it's now time ... to datafrog:
128 // .decl subset(R1, R2, P)
130 // At the point P, R1 <= R2.
132 // subset(R1, R2, P) :- outlives(R1, R2, P).
133 // -> already loaded; outlives is a static input.
135 // .decl requires(R, B, P) -- at the point, things with region R
136 // may depend on data from borrow B
138 // requires(R, B, P) :- borrow_region(R, B, P).
139 // -> already loaded; borrow_region is a static input.
141 // .decl live_to_dead_regions(R1, R2, P, Q)
143 // The regions `R1` and `R2` are "live to dead"
144 // on the edge `P -> Q` if:
146 // - In P, `R1` <= `R2`
147 // - In Q, `R1` is live but `R2` is dead.
149 // In that case, `Q` would like to add all the
150 // live things reachable from `R2` to `R1`.
152 // live_to_dead_regions(R1, R2, P, Q) :-
153 // subset(R1, R2, P),
155 // region_live_at(R1, Q),
156 // !region_live_at(R2, Q).
157 live_to_dead_regions_1
158 .from_join(&subset_p
, &cfg_edge
, |&p
, &(r1
, r2
), &q
| ((r1
, q
), (r2
, p
)));
159 live_to_dead_regions_2
.from_join(
160 &live_to_dead_regions_1
,
162 |&(r1
, q
), &(r2
, p
), &()| ((r2
, q
), (r1
, p
)),
164 live_to_dead_regions
.from_antijoin(
165 &live_to_dead_regions_2
,
167 |&(r2
, q
), &(r1
, p
)| (r1
, r2
, p
, q
),
170 // .decl dead_region_requires((R, P, Q), B)
172 // The region `R` requires the borrow `B`, but the
173 // region `R` goes dead along the edge `P -> Q`
175 // dead_region_requires((R, P, Q), B) :-
176 // requires(R, B, P),
179 // !region_live_at(R, Q).
180 dead_region_requires_1
.from_antijoin(&requires_bp
, &killed
, |&(b
, p
), &r
| (p
, (b
, r
)));
181 dead_region_requires_2
.from_join(
182 &dead_region_requires_1
,
184 |&p
, &(b
, r
), &q
| ((r
, q
), (b
, p
)),
186 dead_region_requires
.from_antijoin(
187 &dead_region_requires_2
,
189 |&(r
, q
), &(b
, p
)| ((r
, p
, q
), b
),
192 // .decl dead_can_reach_origins(R, P, Q)
194 // Contains dead regions where we are interested
195 // in computing the transitive closure of things they
197 dead_can_reach_origins
.from_map(&live_to_dead_regions
, |&(_r1
, r2
, p
, q
)| ((r2
, p
), q
));
198 dead_can_reach_origins
.from_map(&dead_region_requires
, |&((r
, p
, q
), _b
)| ((r
, p
), q
));
200 // .decl dead_can_reach(R1, R2, P, Q)
202 // Indicates that the region `R1`, which is dead
203 // in `Q`, can reach the region `R2` in P.
205 // This is effectively the transitive subset
206 // relation, but we try to limit it to regions
207 // that are dying on the edge P -> Q.
209 // dead_can_reach(R1, R2, P, Q) :-
210 // dead_can_reach_origins(R1, P, Q),
211 // subset(R1, R2, P).
212 dead_can_reach
.from_join(&dead_can_reach_origins
, &subset_r1p
, |&(r1
, p
), &q
, &r2
| {
216 // dead_can_reach(R1, R3, P, Q) :-
217 // dead_can_reach(R1, R2, P, Q),
218 // !region_live_at(R2, Q),
219 // subset(R2, R3, P).
221 // This is the "transitive closure" rule, but
222 // note that we only apply it with the
223 // "intermediate" region R2 is dead at Q.
224 dead_can_reach_1
.from_antijoin(
227 |&(r2
, q
), &(r1
, p
)| ((r2
, p
), (r1
, q
)),
229 dead_can_reach
.from_join(
232 |&(_r2
, p
), &(r1
, q
), &r3
| (r1
, r3
, p
, q
),
235 // .decl dead_can_reach_live(R1, R2, P, Q)
237 // Indicates that, along the edge `P -> Q`, the
238 // dead (in Q) region R1 can reach the live (in Q)
239 // region R2 via a subset relation. This is a
240 // subset of the full `dead_can_reach` relation
241 // where we filter down to those cases where R2 is
243 dead_can_reach_live
.from_join(
246 |&(r2
, q
), &(r1
, p
), &()| ((r1
, p
, q
), r2
),
249 // subset(R1, R2, Q) :-
250 // subset(R1, R2, P),
252 // region_live_at(R1, Q),
253 // region_live_at(R2, Q).
255 // Carry `R1 <= R2` from P into Q if both `R1` and
256 // `R2` are live in Q.
257 subset_1
.from_join(&subset_p
, &cfg_edge
, |&_p
, &(r1
, r2
), &q
| ((r1
, q
), r2
));
258 subset_2
.from_join(&subset_1
, ®ion_live_at_var
, |&(r1
, q
), &r2
, &()| {
261 subset
.from_join(&subset_2
, ®ion_live_at_var
, |&(r2
, q
), &r1
, &()| {
265 // subset(R1, R3, Q) :-
266 // live_to_dead_regions(R1, R2, P, Q),
267 // dead_can_reach_live(R2, R3, P, Q).
269 &live_to_dead_regions_r2pq
,
270 &dead_can_reach_live_r1pq
,
271 |&(_r2
, _p
, q
), &r1
, &r3
| (r1
, r3
, q
),
274 // requires(R2, B, Q) :-
275 // dead_region_requires(R1, B, P, Q),
276 // dead_can_reach_live(R1, R2, P, Q).
278 // Communicate a `R1 requires B` relation across
279 // an edge `P -> Q` where `R1` is dead in Q; in
280 // that case, for each region `R2` live in `Q`
281 // where `R1 <= R2` in P, we add `R2 requires B`
284 &dead_region_requires
,
285 &dead_can_reach_live_r1pq
,
286 |&(_r1
, _p
, q
), &b
, &r2
| (r2
, b
, q
),
289 // requires(R, B, Q) :-
290 // requires(R, B, P),
293 // region_live_at(R, Q).
294 requires_1
.from_antijoin(&requires_bp
, &killed
, |&(b
, p
), &r
| (p
, (r
, b
)));
295 requires_2
.from_join(&requires_1
, &cfg_edge
, |&_p
, &(r
, b
), &q
| ((r
, q
), b
));
296 requires
.from_join(&requires_2
, ®ion_live_at_var
, |&(r
, q
), &b
, &()| {
300 // .decl borrow_live_at(B, P) -- true if the restrictions of the borrow B
301 // need to be enforced at the point P
303 // borrow_live_at(B, P) :- requires(R, B, P), region_live_at(R, P)
304 borrow_live_at
.from_join(&requires_rp
, ®ion_live_at_var
, |&(_r
, p
), &b
, &()| {
308 // .decl errors(B, P) :- invalidates(B, P), borrow_live_at(B, P).
309 errors
.from_join(&invalidates
, &borrow_live_at
, |&(b
, p
), &(), &()| (b
, p
));
313 for (region
, location
) in ®ion_live_at_rel
.elements
{
321 let subset
= subset
.complete();
322 for (r1
, r2
, location
) in &subset
.elements
{
326 .or_insert(BTreeMap
::new())
328 .or_insert(BTreeSet
::new())
332 let requires
= requires
.complete();
333 for (region
, borrow
, location
) in &requires
.elements
{
337 .or_insert(BTreeMap
::new())
339 .or_insert(BTreeSet
::new())
343 let borrow_live_at
= borrow_live_at
.complete();
344 for ((borrow
, location
), ()) in &borrow_live_at
.elements
{
348 .or_insert(Vec
::new())
358 "errors is complete: {} tuples, {:?}",
364 for (borrow
, location
) in &errors
.elements
{
368 .or_insert(Vec
::new())