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.
4//
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.
10
11use datafrog::{Iteration, Relation, RelationLeaper};
12use std::time::Instant;
13
14use crate::facts::FactTypes;
15use crate::output::{Context, Output};
16
17pub(super) fn compute<T: FactTypes>(
18 ctx: &Context<'_, T>,
19 result: &mut Output<T>,
20) -> (
21 Relation<(T::Loan, T::Point)>,
22 Relation<(T::Origin, T::Origin, T::Point)>,
23) {
24 let timer = Instant::now();
25
26 let (errors, subset_errors) = {
27 // Static inputs
28 let origin_live_on_entry_rel = &ctx.origin_live_on_entry;
29 let cfg_edge_rel = &ctx.cfg_edge;
30 let loan_killed_at = &ctx.loan_killed_at;
31 let known_placeholder_subset = &ctx.known_placeholder_subset;
32 let placeholder_origin = &ctx.placeholder_origin;
33
34 // Create a new iteration context, ...
35 let mut iteration = Iteration::new();
36
37 // `loan_invalidated_at` facts, stored ready for joins
38 let loan_invalidated_at =
39 iteration.variable::<((T::Loan, T::Point), ())>("loan_invalidated_at");
40
41 // we need `origin_live_on_entry` in both variable and relation forms,
42 // (respectively, for join and antijoin).
43 let origin_live_on_entry_var =
44 iteration.variable::<((T::Origin, T::Point), ())>("origin_live_on_entry");
45
46 // `loan_issued_at` input but organized for join
47 let loan_issued_at_op =
48 iteration.variable::<((T::Origin, T::Point), T::Loan)>("loan_issued_at_op");
49
50 // .decl subset(origin1, origin2, point)
51 //
52 // Indicates that `origin1: origin2` at `point`.
53 let subset_o1p = iteration.variable::<((T::Origin, T::Point), T::Origin)>("subset_o1p");
54
55 // .decl origin_contains_loan_on_entry(origin, loan, point)
56 //
57 // At `point`, things with `origin` may depend on data from `loan`.
58 let origin_contains_loan_on_entry_op = iteration
59 .variable::<((T::Origin, T::Point), T::Loan)>("origin_contains_loan_on_entry_op");
60
61 // .decl loan_live_at(loan, point)
62 //
63 // True if the restrictions of the `loan` need to be enforced at `point`.
64 let loan_live_at = iteration.variable::<((T::Loan, T::Point), ())>("loan_live_at");
65
66 // .decl live_to_dying_regions(origin1, origin2, point1, point2)
67 //
68 // The origins `origin1` and `origin2` are "live to dead"
69 // on the edge `point1 -> point2` if:
70 //
71 // - In `point1`, `origin1` <= `origin2`
72 // - In `point2`, `origin1` is live but `origin2` is dead.
73 //
74 // In that case, `point2` would like to add all the
75 // live things reachable from `origin2` to `origin1`.
76 //
77 let live_to_dying_regions_o2pq = iteration
78 .variable::<((T::Origin, T::Point, T::Point), T::Origin)>("live_to_dying_regions_o2pq");
79
80 // .decl dying_region_requires((origin, point1, point2), loan)
81 //
82 // The `origin` requires `loan`, but the `origin` goes dead
83 // along the edge `point1 -> point2`.
84 let dying_region_requires = iteration
85 .variable::<((T::Origin, T::Point, T::Point), T::Loan)>("dying_region_requires");
86
87 // .decl dying_can_reach_origins(origin, point1, point2)
88 //
89 // Contains dead origins where we are interested
90 // in computing the transitive closure of things they
91 // can reach.
92 //
93 // FIXME: this relation was named before renaming the `regions` atoms to `origins`, and
94 // will need to be renamed to change "_origins" to "_ascendants", "_roots", etc.
95 let dying_can_reach_origins =
96 iteration.variable::<((T::Origin, T::Point), T::Point)>("dying_can_reach_origins");
97
98 // .decl dying_can_reach(origin1, origin2, point1, point2)
99 //
100 // Indicates that `origin1`, which is dead
101 // in `point2`, can reach `origin2` in `point1`.
102 //
103 // This is effectively the transitive subset
104 // relation, but we try to limit it to origins
105 // that are dying on the edge `point1 -> point2`.
106 let dying_can_reach_o2q =
107 iteration.variable::<((T::Origin, T::Point), (T::Origin, T::Point))>("dying_can_reach");
108 let dying_can_reach_1 = iteration.variable_indistinct("dying_can_reach_1");
109
110 // .decl dying_can_reach_live(origin1, origin2, point1, point2)
111 //
112 // Indicates that, along the edge `point1 -> point2`, the dead (in `point2`)
113 // `origin1` can reach the live (in `point2`) `origin2` via a subset
114 // relation. This is a subset of the full `dying_can_reach`
115 // relation where we filter down to those cases where `origin2` is
116 // live in `point2`.
117 let dying_can_reach_live = iteration
118 .variable::<((T::Origin, T::Point, T::Point), T::Origin)>("dying_can_reach_live");
119
120 // .decl dead_borrow_region_can_reach_root((origin, point), loan)
121 //
122 // Indicates a "borrow region" `origin` at `point` which is not live on
123 // entry to `point`.
124 let dead_borrow_region_can_reach_root = iteration
125 .variable::<((T::Origin, T::Point), T::Loan)>("dead_borrow_region_can_reach_root");
126
127 // .decl dead_borrow_region_can_reach_dead((origin2, point), loan)
128 let dead_borrow_region_can_reach_dead = iteration
129 .variable::<((T::Origin, T::Point), T::Loan)>("dead_borrow_region_can_reach_dead");
130 let dead_borrow_region_can_reach_dead_1 =
131 iteration.variable_indistinct("dead_borrow_region_can_reach_dead_1");
132
133 // .decl errors(loan, point)
134 let errors = iteration.variable("errors");
135 let subset_errors = iteration.variable::<(T::Origin, T::Origin, T::Point)>("subset_errors");
136
137 let subset_placeholder =
138 iteration.variable::<(T::Origin, T::Origin, T::Point)>("subset_placeholder");
139 let subset_placeholder_o2p = iteration.variable_indistinct("subset_placeholder_o2p");
140
141 // Make "variable" versions of the relations, needed for joins.
142 loan_issued_at_op.extend(
143 ctx.loan_issued_at
144 .iter()
145 .map(|&(origin, loan, point)| ((origin, point), loan)),
146 );
147 loan_invalidated_at.extend(
148 ctx.loan_invalidated_at
149 .iter()
150 .map(|&(loan, point)| ((loan, point), ())),
151 );
152 origin_live_on_entry_var.extend(
153 origin_live_on_entry_rel
154 .iter()
155 .map(|&(origin, point)| ((origin, point), ())),
156 );
157
158 // subset(origin1, origin2, point) :-
159 // subset_base(origin1, origin2, point).
160 subset_o1p.extend(
161 ctx.subset_base
162 .iter()
163 .map(|&(origin1, origin2, point)| ((origin1, point), origin2)),
164 );
165
166 // origin_contains_loan_on_entry(origin, loan, point) :-
167 // loan_issued_at(origin, loan, point).
168 origin_contains_loan_on_entry_op.extend(
169 ctx.loan_issued_at
170 .iter()
171 .map(|&(origin, loan, point)| ((origin, point), loan)),
172 );
173
174 // .. and then start iterating rules!
175 while iteration.changed() {
176 // Cleanup step: remove symmetries
177 // - remove origins which are `subset`s of themselves
178 //
179 // FIXME: investigate whether is there a better way to do that without complicating
180 // the rules too much, because it would also require temporary variables and
181 // impact performance. Until then, the big reduction in tuples improves performance
182 // a lot, even if we're potentially adding a small number of tuples
183 // per round just to remove them in the next round.
184 subset_o1p
185 .recent
186 .borrow_mut()
187 .elements
188 .retain(|&((origin1, _), origin2)| origin1 != origin2);
189
190 subset_placeholder
191 .recent
192 .borrow_mut()
193 .elements
194 .retain(|&(origin1, origin2, _)| origin1 != origin2);
195 subset_placeholder_o2p.from_map(&subset_placeholder, |&(origin1, origin2, point)| {
196 ((origin2, point), origin1)
197 });
198
199 // live_to_dying_regions(origin1, origin2, point1, point2) :-
200 // subset(origin1, origin2, point1),
201 // cfg_edge(point1, point2),
202 // origin_live_on_entry(origin1, point2),
203 // !origin_live_on_entry(origin2, point2).
204 live_to_dying_regions_o2pq.from_leapjoin(
205 &subset_o1p,
206 (
207 cfg_edge_rel.extend_with(|&((_, point1), _)| point1),
208 origin_live_on_entry_rel.extend_with(|&((origin1, _), _)| origin1),
209 origin_live_on_entry_rel.extend_anti(|&((_, _), origin2)| origin2),
210 ),
211 |&((origin1, point1), origin2), &point2| ((origin2, point1, point2), origin1),
212 );
213
214 // dying_region_requires((origin, point1, point2), loan) :-
215 // origin_contains_loan_on_entry(origin, loan, point1),
216 // !loan_killed_at(loan, point1),
217 // cfg_edge(point1, point2),
218 // !origin_live_on_entry(origin, point2).
219 dying_region_requires.from_leapjoin(
220 &origin_contains_loan_on_entry_op,
221 (
222 loan_killed_at.filter_anti(|&((_, point1), loan)| (loan, point1)),
223 cfg_edge_rel.extend_with(|&((_, point1), _)| point1),
224 origin_live_on_entry_rel.extend_anti(|&((origin, _), _)| origin),
225 ),
226 |&((origin, point1), loan), &point2| ((origin, point1, point2), loan),
227 );
228
229 // dying_can_reach_origins(origin2, point1, point2) :-
230 // live_to_dying_regions(_, origin2, point1, point2).
231 dying_can_reach_origins.from_map(
232 &live_to_dying_regions_o2pq,
233 |&((origin2, point1, point2), _origin1)| ((origin2, point1), point2),
234 );
235
236 // dying_can_reach_origins(origin, point1, point2) :-
237 // dying_region_requires(origin, point1, point2, _loan).
238 dying_can_reach_origins.from_map(
239 &dying_region_requires,
240 |&((origin, point1, point2), _loan)| ((origin, point1), point2),
241 );
242
243 // dying_can_reach(origin1, origin2, point1, point2) :-
244 // dying_can_reach_origins(origin1, point1, point2),
245 // subset(origin1, origin2, point1).
246 dying_can_reach_o2q.from_join(
247 &dying_can_reach_origins,
248 &subset_o1p,
249 |&(origin1, point1), &point2, &origin2| ((origin2, point2), (origin1, point1)),
250 );
251
252 // dying_can_reach(origin1, origin3, point1, point2) :-
253 // dying_can_reach(origin1, origin2, point1, point2),
254 // !origin_live_on_entry(origin2, point2),
255 // subset(origin2, origin3, point1).
256 //
257 // This is the "transitive closure" rule, but
258 // note that we only apply it with the
259 // "intermediate" `origin2` is dead at `point2`.
260 dying_can_reach_1.from_antijoin(
261 &dying_can_reach_o2q,
262 &origin_live_on_entry_rel,
263 |&(origin2, point2), &(origin1, point1)| ((origin2, point1), (origin1, point2)),
264 );
265 dying_can_reach_o2q.from_join(
266 &dying_can_reach_1,
267 &subset_o1p,
268 |&(_origin2, point1), &(origin1, point2), &origin3| {
269 ((origin3, point2), (origin1, point1))
270 },
271 );
272
273 // dying_can_reach_live(origin1, origin2, point1, point2) :-
274 // dying_can_reach(origin1, origin2, point1, point2),
275 // origin_live_on_entry(origin2, point2).
276 dying_can_reach_live.from_join(
277 &dying_can_reach_o2q,
278 &origin_live_on_entry_var,
279 |&(origin2, point2), &(origin1, point1), _| ((origin1, point1, point2), origin2),
280 );
281
282 // subset(origin1, origin2, point2) :-
283 // subset(origin1, origin2, point1),
284 // cfg_edge(point1, point2),
285 // origin_live_on_entry(origin1, point2),
286 // origin_live_on_entry(origin2, point2).
287 //
288 // Carry `origin1 <= origin2` from `point1` into `point2` if both `origin1` and
289 // `origin2` are live in `point2`.
290 subset_o1p.from_leapjoin(
291 &subset_o1p,
292 (
293 cfg_edge_rel.extend_with(|&((_, point1), _)| point1),
294 origin_live_on_entry_rel.extend_with(|&((origin1, _), _)| origin1),
295 origin_live_on_entry_rel.extend_with(|&((_, _), origin2)| origin2),
296 ),
297 |&((origin1, _point1), origin2), &point2| ((origin1, point2), origin2),
298 );
299
300 // subset(origin1, origin3, point2) :-
301 // live_to_dying_regions(origin1, origin2, point1, point2),
302 // dying_can_reach_live(origin2, origin3, point1, point2).
303 subset_o1p.from_join(
304 &live_to_dying_regions_o2pq,
305 &dying_can_reach_live,
306 |&(_origin2, _point1, point2), &origin1, &origin3| ((origin1, point2), origin3),
307 );
308
309 // origin_contains_loan_on_entry(origin2, loan, point2) :-
310 // dying_region_requires(origin1, loan, point1, point2),
311 // dying_can_reach_live(origin1, origin2, point1, point2).
312 //
313 // Communicate a `origin1 contains loan` relation across
314 // an edge `point1 -> point2` where `origin1` is dead in `point2`; in
315 // that case, for each origin `origin2` live in `point2`
316 // where `origin1 <= origin2` in `point1`, we add `origin2 contains loan`
317 // to `point2`.
318 origin_contains_loan_on_entry_op.from_join(
319 &dying_region_requires,
320 &dying_can_reach_live,
321 |&(_origin1, _point1, point2), &loan, &origin2| ((origin2, point2), loan),
322 );
323
324 // origin_contains_loan_on_entry(origin, loan, point2) :-
325 // origin_contains_loan_on_entry(origin, loan, point1),
326 // !loan_killed_at(loan, point1),
327 // cfg_edge(point1, point2),
328 // origin_live_on_entry(origin, point2).
329 origin_contains_loan_on_entry_op.from_leapjoin(
330 &origin_contains_loan_on_entry_op,
331 (
332 loan_killed_at.filter_anti(|&((_, point1), loan)| (loan, point1)),
333 cfg_edge_rel.extend_with(|&((_, point1), _)| point1),
334 origin_live_on_entry_rel.extend_with(|&((origin, _), _)| origin),
335 ),
336 |&((origin, _), loan), &point2| ((origin, point2), loan),
337 );
338
339 // dead_borrow_region_can_reach_root((origin, point), loan) :-
340 // loan_issued_at(origin, loan, point),
341 // !origin_live_on_entry(origin, point).
342 dead_borrow_region_can_reach_root.from_antijoin(
343 &loan_issued_at_op,
344 &origin_live_on_entry_rel,
345 |&(origin, point), &loan| ((origin, point), loan),
346 );
347
348 // dead_borrow_region_can_reach_dead((origin, point), loan) :-
349 // dead_borrow_region_can_reach_root((origin, point), loan).
350 dead_borrow_region_can_reach_dead
351 .from_map(&dead_borrow_region_can_reach_root, |&tuple| tuple);
352
353 // dead_borrow_region_can_reach_dead((origin2, point), loan) :-
354 // dead_borrow_region_can_reach_dead(origin1, loan, point),
355 // subset(origin1, origin2, point),
356 // !origin_live_on_entry(origin2, point).
357 dead_borrow_region_can_reach_dead_1.from_join(
358 &dead_borrow_region_can_reach_dead,
359 &subset_o1p,
360 |&(_origin1, point), &loan, &origin2| ((origin2, point), loan),
361 );
362 dead_borrow_region_can_reach_dead.from_antijoin(
363 &dead_borrow_region_can_reach_dead_1,
364 &origin_live_on_entry_rel,
365 |&(origin2, point), &loan| ((origin2, point), loan),
366 );
367
368 // loan_live_at(loan, point) :-
369 // origin_contains_loan_on_entry(origin, loan, point),
370 // origin_live_on_entry(origin, point).
371 loan_live_at.from_join(
372 &origin_contains_loan_on_entry_op,
373 &origin_live_on_entry_var,
374 |&(_origin, point), &loan, _| ((loan, point), ()),
375 );
376
377 // loan_live_at(loan, point) :-
378 // dead_borrow_region_can_reach_dead(origin1, loan, point),
379 // subset(origin1, origin2, point),
380 // origin_live_on_entry(origin2, point).
381 //
382 // NB: the datafrog code below uses
383 // `dead_borrow_region_can_reach_dead_1`, which is equal
384 // to `dead_borrow_region_can_reach_dead` and `subset`
385 // joined together.
386 loan_live_at.from_join(
387 &dead_borrow_region_can_reach_dead_1,
388 &origin_live_on_entry_var,
389 |&(_origin2, point), &loan, _| ((loan, point), ()),
390 );
391
392 // errors(loan, point) :-
393 // loan_invalidated_at(loan, point),
394 // loan_live_at(loan, point).
395 errors.from_join(
396 &loan_invalidated_at,
397 &loan_live_at,
398 |&(loan, point), _, _| (loan, point),
399 );
400
401 // subset_placeholder(Origin1, Origin2, Point) :-
402 // subset(Origin1, Origin2, Point),
403 // placeholder_origin(Origin1).
404 subset_placeholder.from_leapjoin(
405 &subset_o1p,
406 (
407 placeholder_origin.extend_with(|&((origin1, _point), _origin2)| origin1),
408 // remove symmetries:
409 datafrog::ValueFilter::from(|&((origin1, _point), origin2), _| {
410 origin1 != origin2
411 }),
412 ),
413 |&((origin1, point), origin2), _| (origin1, origin2, point),
414 );
415
416 // We compute the transitive closure of the placeholder origins, so we
417 // maintain the invariant from the rule above that `Origin1` is a placeholder origin.
418 //
419 // subset_placeholder(Origin1, Origin3, Point) :-
420 // subset_placeholder(Origin1, Origin2, Point),
421 // subset(Origin2, Origin3, Point).
422 subset_placeholder.from_join(
423 &subset_placeholder_o2p,
424 &subset_o1p,
425 |&(_origin2, point), &origin1, &origin3| (origin1, origin3, point),
426 );
427
428 // subset_error(Origin1, Origin2, Point) :-
429 // subset_placeholder(Origin1, Origin2, Point),
430 // placeholder_origin(Origin2),
431 // !known_placeholder_subset(Origin1, Origin2).
432 subset_errors.from_leapjoin(
433 &subset_placeholder,
434 (
435 placeholder_origin.extend_with(|&(_origin1, origin2, _point)| origin2),
436 known_placeholder_subset
437 .filter_anti(|&(origin1, origin2, _point)| (origin1, origin2)),
438 // remove symmetries:
439 datafrog::ValueFilter::from(|&(origin1, origin2, _point), _| {
440 origin1 != origin2
441 }),
442 ),
443 |&(origin1, origin2, point), _| (origin1, origin2, point),
444 );
445 }
446
447 if result.dump_enabled {
448 let subset_o1p = subset_o1p.complete();
449 assert!(
450 subset_o1p
451 .iter()
452 .filter(|&((origin1, _), origin2)| origin1 == origin2)
453 .count()
454 == 0,
455 "unwanted subset symmetries"
456 );
457 for &((origin1, location), origin2) in subset_o1p.iter() {
458 result
459 .subset
460 .entry(location)
461 .or_default()
462 .entry(origin1)
463 .or_default()
464 .insert(origin2);
465 }
466
467 let origin_contains_loan_on_entry_op = origin_contains_loan_on_entry_op.complete();
468 for &((origin, location), loan) in origin_contains_loan_on_entry_op.iter() {
469 result
470 .origin_contains_loan_at
471 .entry(location)
472 .or_default()
473 .entry(origin)
474 .or_default()
475 .insert(loan);
476 }
477
478 let loan_live_at = loan_live_at.complete();
479 for &((loan, location), _) in loan_live_at.iter() {
480 result.loan_live_at.entry(location).or_default().push(loan);
481 }
482 }
483
484 (errors.complete(), subset_errors.complete())
485 };
486
487 info!(
488 "analysis done: {} `errors` tuples, {} `subset_errors` tuples, {:?}",
489 errors.len(),
490 subset_errors.len(),
491 timer.elapsed()
492 );
493
494 (errors, subset_errors)
495}
496