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 datafrog
::{Iteration, Relation, RelationLeaper}
;
12 use std
::time
::Instant
;
14 use crate::facts
::FactTypes
;
15 use crate::output
::{Context, Output}
;
17 pub(super) fn compute
<T
: FactTypes
>(
19 result
: &mut Output
<T
>,
20 ) -> Relation
<(T
::Loan
, T
::Point
)> {
21 let timer
= Instant
::now();
25 let region_live_at_rel
= &ctx
.region_live_at
;
26 let cfg_edge_rel
= &ctx
.cfg_edge
;
27 let killed_rel
= &ctx
.killed
;
29 // Create a new iteration context, ...
30 let mut iteration
= Iteration
::new();
32 // `invalidates` facts, stored ready for joins
33 let invalidates
= iteration
.variable
::<((T
::Loan
, T
::Point
), ())>("invalidates");
35 // we need `region_live_at` in both variable and relation forms,
36 // (respectively, for join and antijoin).
37 let region_live_at_var
=
38 iteration
.variable
::<((T
::Origin
, T
::Point
), ())>("region_live_at");
40 // `borrow_region` input but organized for join
41 let borrow_region_op
=
42 iteration
.variable
::<((T
::Origin
, T
::Point
), T
::Loan
)>("borrow_region_op");
44 // .decl subset(origin1, origin2, point)
46 // Indicates that `origin1: origin2` at `point`.
47 let subset_o1p
= iteration
.variable
::<((T
::Origin
, T
::Point
), T
::Origin
)>("subset_o1p");
49 // .decl requires(origin, loan, point)
51 // At `point`, things with `origin` may depend on data from `loan`.
52 let requires_op
= iteration
.variable
::<((T
::Origin
, T
::Point
), T
::Loan
)>("requires_op");
54 // .decl borrow_live_at(loan, point)
56 // True if the restrictions of the `loan` need to be enforced at `point`.
57 let borrow_live_at
= iteration
.variable
::<((T
::Loan
, T
::Point
), ())>("borrow_live_at");
59 // .decl live_to_dying_regions(origin1, origin2, point1, point2)
61 // The origins `origin1` and `origin2` are "live to dead"
62 // on the edge `point1 -> point2` if:
64 // - In `point1`, `origin1` <= `origin2`
65 // - In `point2`, `origin1` is live but `origin2` is dead.
67 // In that case, `point2` would like to add all the
68 // live things reachable from `origin2` to `origin1`.
70 let live_to_dying_regions_o2pq
= iteration
71 .variable
::<((T
::Origin
, T
::Point
, T
::Point
), T
::Origin
)>("live_to_dying_regions_o2pq");
73 // .decl dying_region_requires((origin, point1, point2), loan)
75 // The `origin` requires `loan`, but the `origin` goes dead
76 // along the edge `point1 -> point2`.
77 let dying_region_requires
= iteration
78 .variable
::<((T
::Origin
, T
::Point
, T
::Point
), T
::Loan
)>("dying_region_requires");
80 // .decl dying_can_reach_origins(origin, point1, point2)
82 // Contains dead origins where we are interested
83 // in computing the transitive closure of things they
86 // FIXME: this relation was named before renaming the `regions` atoms to `origins`, and
87 // will need to be renamed to change "_origins" to "_ascendants", "_roots", etc.
88 let dying_can_reach_origins
=
89 iteration
.variable
::<((T
::Origin
, T
::Point
), T
::Point
)>("dying_can_reach_origins");
91 // .decl dying_can_reach(origin1, origin2, point1, point2)
93 // Indicates that `origin1`, which is dead
94 // in `point2`, can reach `origin2` in `point1`.
96 // This is effectively the transitive subset
97 // relation, but we try to limit it to origins
98 // that are dying on the edge `point1 -> point2`.
99 let dying_can_reach_o2q
=
100 iteration
.variable
::<((T
::Origin
, T
::Point
), (T
::Origin
, T
::Point
))>("dying_can_reach");
101 let dying_can_reach_1
= iteration
.variable_indistinct("dying_can_reach_1");
103 // .decl dying_can_reach_live(origin1, origin2, point1, point2)
105 // Indicates that, along the edge `point1 -> point2`, the dead (in `point2`)
106 // `origin1` can reach the live (in `point2`) `origin2` via a subset
107 // relation. This is a subset of the full `dying_can_reach`
108 // relation where we filter down to those cases where `origin2` is
110 let dying_can_reach_live
= iteration
111 .variable
::<((T
::Origin
, T
::Point
, T
::Point
), T
::Origin
)>("dying_can_reach_live");
113 // .decl dead_borrow_region_can_reach_root((origin, point), loan)
115 // Indicates a "borrow region" `origin` at `point` which is not live on
117 let dead_borrow_region_can_reach_root
= iteration
118 .variable
::<((T
::Origin
, T
::Point
), T
::Loan
)>("dead_borrow_region_can_reach_root");
120 // .decl dead_borrow_region_can_reach_dead((origin2, point), loan)
121 let dead_borrow_region_can_reach_dead
= iteration
122 .variable
::<((T
::Origin
, T
::Point
), T
::Loan
)>("dead_borrow_region_can_reach_dead");
123 let dead_borrow_region_can_reach_dead_1
=
124 iteration
.variable_indistinct("dead_borrow_region_can_reach_dead_1");
126 // .decl errors(loan, point)
127 let errors
= iteration
.variable("errors");
129 // Make "variable" versions of the relations, needed for joins.
130 borrow_region_op
.extend(
133 .map(|&(origin
, loan
, point
)| ((origin
, point
), loan
)),
138 .map(|&(loan
, point
)| ((loan
, point
), ())),
140 region_live_at_var
.extend(
143 .map(|&(origin
, point
)| ((origin
, point
), ())),
146 // subset(origin1, origin2, point) :- outlives(origin1, origin2, point).
150 .map(|&(origin1
, origin2
, point
)| ((origin1
, point
), origin2
)),
153 // requires(origin, loan, point) :- borrow_region(origin, loan, point).
157 .map(|&(origin
, loan
, point
)| ((origin
, point
), loan
)),
160 // .. and then start iterating rules!
161 while iteration
.changed() {
162 // Cleanup step: remove symmetries
163 // - remove origins which are `subset`s of themselves
165 // FIXME: investigate whether is there a better way to do that without complicating
166 // the rules too much, because it would also require temporary variables and
167 // impact performance. Until then, the big reduction in tuples improves performance
168 // a lot, even if we're potentially adding a small number of tuples
169 // per round just to remove them in the next round.
174 .retain(|&((origin1
, _
), origin2
)| origin1
!= origin2
);
176 // live_to_dying_regions(origin1, origin2, point1, point2) :-
177 // subset(origin1, origin2, point1),
178 // cfg_edge(point1, point2),
179 // region_live_at(origin1, point2),
180 // !region_live_at(origin2, point2).
181 live_to_dying_regions_o2pq
.from_leapjoin(
184 cfg_edge_rel
.extend_with(|&((_
, point1
), _
)| point1
),
185 region_live_at_rel
.extend_with(|&((origin1
, _
), _
)| origin1
),
186 region_live_at_rel
.extend_anti(|&((_
, _
), origin2
)| origin2
),
188 |&((origin1
, point1
), origin2
), &point2
| ((origin2
, point1
, point2
), origin1
),
191 // dying_region_requires((origin, point1, point2), loan) :-
192 // requires(origin, loan, point1),
193 // !killed(loan, point1),
194 // cfg_edge(point1, point2),
195 // !region_live_at(origin, point2).
196 dying_region_requires
.from_leapjoin(
199 killed_rel
.filter_anti(|&((_
, point1
), loan
)| (loan
, point1
)),
200 cfg_edge_rel
.extend_with(|&((_
, point1
), _
)| point1
),
201 region_live_at_rel
.extend_anti(|&((origin
, _
), _
)| origin
),
203 |&((origin
, point1
), loan
), &point2
| ((origin
, point1
, point2
), loan
),
206 // dying_can_reach_origins(origin2, point1, point2) :-
207 // live_to_dying_regions(_, origin2, point1, point2).
208 dying_can_reach_origins
.from_map(
209 &live_to_dying_regions_o2pq
,
210 |&((origin2
, point1
, point2
), _origin1
)| ((origin2
, point1
), point2
),
213 // dying_can_reach_origins(origin, point1, point2) :-
214 // dying_region_requires(origin, point1, point2, _loan).
215 dying_can_reach_origins
.from_map(
216 &dying_region_requires
,
217 |&((origin
, point1
, point2
), _loan
)| ((origin
, point1
), point2
),
220 // dying_can_reach(origin1, origin2, point1, point2) :-
221 // dying_can_reach_origins(origin1, point1, point2),
222 // subset(origin1, origin2, point1).
223 dying_can_reach_o2q
.from_join(
224 &dying_can_reach_origins
,
226 |&(origin1
, point1
), &point2
, &origin2
| ((origin2
, point2
), (origin1
, point1
)),
229 // dying_can_reach(origin1, origin3, point1, point2) :-
230 // dying_can_reach(origin1, origin2, point1, point2),
231 // !region_live_at(origin2, point2),
232 // subset(origin2, origin3, point1).
234 // This is the "transitive closure" rule, but
235 // note that we only apply it with the
236 // "intermediate" `origin2` is dead at `point2`.
237 dying_can_reach_1
.from_antijoin(
238 &dying_can_reach_o2q
,
240 |&(origin2
, point2
), &(origin1
, point1
)| ((origin2
, point1
), (origin1
, point2
)),
242 dying_can_reach_o2q
.from_join(
245 |&(_origin2
, point1
), &(origin1
, point2
), &origin3
| {
246 ((origin3
, point2
), (origin1
, point1
))
250 // dying_can_reach_live(origin1, origin2, point1, point2) :-
251 // dying_can_reach(origin1, origin2, point1, point2),
252 // region_live_at(origin2, point2).
253 dying_can_reach_live
.from_join(
254 &dying_can_reach_o2q
,
256 |&(origin2
, point2
), &(origin1
, point1
), _
| ((origin1
, point1
, point2
), origin2
),
259 // subset(origin1, origin2, point2) :-
260 // subset(origin1, origin2, point1),
261 // cfg_edge(point1, point2),
262 // region_live_at(origin1, point2),
263 // region_live_at(origin2, point2).
265 // Carry `origin1 <= origin2` from `point1` into `point2` if both `origin1` and
266 // `origin2` are live in `point2`.
267 subset_o1p
.from_leapjoin(
270 cfg_edge_rel
.extend_with(|&((_
, point1
), _
)| point1
),
271 region_live_at_rel
.extend_with(|&((origin1
, _
), _
)| origin1
),
272 region_live_at_rel
.extend_with(|&((_
, _
), origin2
)| origin2
),
274 |&((origin1
, _point1
), origin2
), &point2
| ((origin1
, point2
), origin2
),
277 // subset(origin1, origin3, point2) :-
278 // live_to_dying_regions(origin1, origin2, point1, point2),
279 // dying_can_reach_live(origin2, origin3, point1, point2).
280 subset_o1p
.from_join(
281 &live_to_dying_regions_o2pq
,
282 &dying_can_reach_live
,
283 |&(_origin2
, _point1
, point2
), &origin1
, &origin3
| ((origin1
, point2
), origin3
),
286 // requires(origin2, loan, point2) :-
287 // dying_region_requires(origin1, loan, point1, point2),
288 // dying_can_reach_live(origin1, origin2, point1, point2).
290 // Communicate a `origin1 requires loan` relation across
291 // an edge `point1 -> point2` where `origin1` is dead in `point2`; in
292 // that case, for each origin `origin2` live in `point2`
293 // where `origin1 <= origin2` in `point1`, we add `origin2 requires loan`
295 requires_op
.from_join(
296 &dying_region_requires
,
297 &dying_can_reach_live
,
298 |&(_origin1
, _point1
, point2
), &loan
, &origin2
| ((origin2
, point2
), loan
),
301 // requires(origin, loan, point2) :-
302 // requires(origin, loan, point1),
303 // !killed(loan, point1),
304 // cfg_edge(point1, point2),
305 // region_live_at(origin, point2).
306 requires_op
.from_leapjoin(
309 killed_rel
.filter_anti(|&((_
, point1
), loan
)| (loan
, point1
)),
310 cfg_edge_rel
.extend_with(|&((_
, point1
), _
)| point1
),
311 region_live_at_rel
.extend_with(|&((origin
, _
), _
)| origin
),
313 |&((origin
, _
), loan
), &point2
| ((origin
, point2
), loan
),
316 // dead_borrow_region_can_reach_root((origin, point), loan) :-
317 // borrow_region(origin, loan, point),
318 // !region_live_at(origin, point).
319 dead_borrow_region_can_reach_root
.from_antijoin(
322 |&(origin
, point
), &loan
| ((origin
, point
), loan
),
325 // dead_borrow_region_can_reach_dead((origin, point), loan) :-
326 // dead_borrow_region_can_reach_root((origin, point), loan).
327 dead_borrow_region_can_reach_dead
328 .from_map(&dead_borrow_region_can_reach_root
, |&tuple
| tuple
);
330 // dead_borrow_region_can_reach_dead((origin2, point), loan) :-
331 // dead_borrow_region_can_reach_dead(origin1, loan, point),
332 // subset(origin1, origin2, point),
333 // !region_live_at(origin2, point).
334 dead_borrow_region_can_reach_dead_1
.from_join(
335 &dead_borrow_region_can_reach_dead
,
337 |&(_origin1
, point
), &loan
, &origin2
| ((origin2
, point
), loan
),
339 dead_borrow_region_can_reach_dead
.from_antijoin(
340 &dead_borrow_region_can_reach_dead_1
,
342 |&(origin2
, point
), &loan
| ((origin2
, point
), loan
),
345 // borrow_live_at(loan, point) :-
346 // requires(origin, loan, point),
347 // region_live_at(origin, point).
348 borrow_live_at
.from_join(
351 |&(_origin
, point
), &loan
, _
| ((loan
, point
), ()),
354 // borrow_live_at(loan, point) :-
355 // dead_borrow_region_can_reach_dead(origin1, loan, point),
356 // subset(origin1, origin2, point),
357 // region_live_at(origin2, point).
359 // NB: the datafrog code below uses
360 // `dead_borrow_region_can_reach_dead_1`, which is equal
361 // to `dead_borrow_region_can_reach_dead` and `subset`
363 borrow_live_at
.from_join(
364 &dead_borrow_region_can_reach_dead_1
,
366 |&(_origin2
, point
), &loan
, _
| ((loan
, point
), ()),
369 // errors(loan, point) :-
370 // invalidates(loan, point),
371 // borrow_live_at(loan, point).
372 errors
.from_join(&invalidates
, &borrow_live_at
, |&(loan
, point
), _
, _
| {
377 if result
.dump_enabled
{
378 let subset_o1p
= subset_o1p
.complete();
382 .filter(|&((origin1
, _
), origin2
)| origin1
== origin2
)
385 "unwanted subset symmetries"
387 for &((origin1
, location
), origin2
) in subset_o1p
.iter() {
397 let requires_op
= requires_op
.complete();
398 for &((origin
, location
), loan
) in requires_op
.iter() {
408 let borrow_live_at
= borrow_live_at
.complete();
409 for &((loan
, location
), _
) in borrow_live_at
.iter() {
422 "errors is complete: {} tuples, {:?}",