]> git.proxmox.com Git - rustc.git/blob - vendor/polonius-engine/src/output/datafrog_opt.rs
New upstream version 1.41.1+dfsg1
[rustc.git] / vendor / polonius-engine / src / output / datafrog_opt.rs
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
11 use datafrog::{Iteration, Relation, RelationLeaper};
12 use std::time::Instant;
13
14 use crate::facts::FactTypes;
15 use crate::output::{Context, Output};
16
17 pub(super) fn compute<T: FactTypes>(
18 ctx: &Context<T>,
19 result: &mut Output<T>,
20 ) -> Relation<(T::Loan, T::Point)> {
21 let timer = Instant::now();
22
23 let errors = {
24 // Static inputs
25 let region_live_at_rel = &ctx.region_live_at;
26 let cfg_edge_rel = &ctx.cfg_edge;
27 let killed_rel = &ctx.killed;
28
29 // Create a new iteration context, ...
30 let mut iteration = Iteration::new();
31
32 // `invalidates` facts, stored ready for joins
33 let invalidates = iteration.variable::<((T::Loan, T::Point), ())>("invalidates");
34
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");
39
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");
43
44 // .decl subset(origin1, origin2, point)
45 //
46 // Indicates that `origin1: origin2` at `point`.
47 let subset_o1p = iteration.variable::<((T::Origin, T::Point), T::Origin)>("subset_o1p");
48
49 // .decl requires(origin, loan, point)
50 //
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");
53
54 // .decl borrow_live_at(loan, point)
55 //
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");
58
59 // .decl live_to_dying_regions(origin1, origin2, point1, point2)
60 //
61 // The origins `origin1` and `origin2` are "live to dead"
62 // on the edge `point1 -> point2` if:
63 //
64 // - In `point1`, `origin1` <= `origin2`
65 // - In `point2`, `origin1` is live but `origin2` is dead.
66 //
67 // In that case, `point2` would like to add all the
68 // live things reachable from `origin2` to `origin1`.
69 //
70 let live_to_dying_regions_o2pq = iteration
71 .variable::<((T::Origin, T::Point, T::Point), T::Origin)>("live_to_dying_regions_o2pq");
72
73 // .decl dying_region_requires((origin, point1, point2), loan)
74 //
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");
79
80 // .decl dying_can_reach_origins(origin, point1, point2)
81 //
82 // Contains dead origins where we are interested
83 // in computing the transitive closure of things they
84 // can reach.
85 //
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");
90
91 // .decl dying_can_reach(origin1, origin2, point1, point2)
92 //
93 // Indicates that `origin1`, which is dead
94 // in `point2`, can reach `origin2` in `point1`.
95 //
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");
102
103 // .decl dying_can_reach_live(origin1, origin2, point1, point2)
104 //
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
109 // live in `point2`.
110 let dying_can_reach_live = iteration
111 .variable::<((T::Origin, T::Point, T::Point), T::Origin)>("dying_can_reach_live");
112
113 // .decl dead_borrow_region_can_reach_root((origin, point), loan)
114 //
115 // Indicates a "borrow region" `origin` at `point` which is not live on
116 // entry to `point`.
117 let dead_borrow_region_can_reach_root = iteration
118 .variable::<((T::Origin, T::Point), T::Loan)>("dead_borrow_region_can_reach_root");
119
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");
125
126 // .decl errors(loan, point)
127 let errors = iteration.variable("errors");
128
129 // Make "variable" versions of the relations, needed for joins.
130 borrow_region_op.extend(
131 ctx.borrow_region
132 .iter()
133 .map(|&(origin, loan, point)| ((origin, point), loan)),
134 );
135 invalidates.extend(
136 ctx.invalidates
137 .iter()
138 .map(|&(loan, point)| ((loan, point), ())),
139 );
140 region_live_at_var.extend(
141 region_live_at_rel
142 .iter()
143 .map(|&(origin, point)| ((origin, point), ())),
144 );
145
146 // subset(origin1, origin2, point) :- outlives(origin1, origin2, point).
147 subset_o1p.extend(
148 ctx.outlives
149 .iter()
150 .map(|&(origin1, origin2, point)| ((origin1, point), origin2)),
151 );
152
153 // requires(origin, loan, point) :- borrow_region(origin, loan, point).
154 requires_op.extend(
155 ctx.borrow_region
156 .iter()
157 .map(|&(origin, loan, point)| ((origin, point), loan)),
158 );
159
160 // .. and then start iterating rules!
161 while iteration.changed() {
162 // Cleanup step: remove symmetries
163 // - remove origins which are `subset`s of themselves
164 //
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.
170 subset_o1p
171 .recent
172 .borrow_mut()
173 .elements
174 .retain(|&((origin1, _), origin2)| origin1 != origin2);
175
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(
182 &subset_o1p,
183 (
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),
187 ),
188 |&((origin1, point1), origin2), &point2| ((origin2, point1, point2), origin1),
189 );
190
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(
197 &requires_op,
198 (
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),
202 ),
203 |&((origin, point1), loan), &point2| ((origin, point1, point2), loan),
204 );
205
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),
211 );
212
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),
218 );
219
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,
225 &subset_o1p,
226 |&(origin1, point1), &point2, &origin2| ((origin2, point2), (origin1, point1)),
227 );
228
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).
233 //
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,
239 &region_live_at_rel,
240 |&(origin2, point2), &(origin1, point1)| ((origin2, point1), (origin1, point2)),
241 );
242 dying_can_reach_o2q.from_join(
243 &dying_can_reach_1,
244 &subset_o1p,
245 |&(_origin2, point1), &(origin1, point2), &origin3| {
246 ((origin3, point2), (origin1, point1))
247 },
248 );
249
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,
255 &region_live_at_var,
256 |&(origin2, point2), &(origin1, point1), _| ((origin1, point1, point2), origin2),
257 );
258
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).
264 //
265 // Carry `origin1 <= origin2` from `point1` into `point2` if both `origin1` and
266 // `origin2` are live in `point2`.
267 subset_o1p.from_leapjoin(
268 &subset_o1p,
269 (
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),
273 ),
274 |&((origin1, _point1), origin2), &point2| ((origin1, point2), origin2),
275 );
276
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),
284 );
285
286 // requires(origin2, loan, point2) :-
287 // dying_region_requires(origin1, loan, point1, point2),
288 // dying_can_reach_live(origin1, origin2, point1, point2).
289 //
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`
294 // to `point2`.
295 requires_op.from_join(
296 &dying_region_requires,
297 &dying_can_reach_live,
298 |&(_origin1, _point1, point2), &loan, &origin2| ((origin2, point2), loan),
299 );
300
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(
307 &requires_op,
308 (
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),
312 ),
313 |&((origin, _), loan), &point2| ((origin, point2), loan),
314 );
315
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(
320 &borrow_region_op,
321 &region_live_at_rel,
322 |&(origin, point), &loan| ((origin, point), loan),
323 );
324
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);
329
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,
336 &subset_o1p,
337 |&(_origin1, point), &loan, &origin2| ((origin2, point), loan),
338 );
339 dead_borrow_region_can_reach_dead.from_antijoin(
340 &dead_borrow_region_can_reach_dead_1,
341 &region_live_at_rel,
342 |&(origin2, point), &loan| ((origin2, point), loan),
343 );
344
345 // borrow_live_at(loan, point) :-
346 // requires(origin, loan, point),
347 // region_live_at(origin, point).
348 borrow_live_at.from_join(
349 &requires_op,
350 &region_live_at_var,
351 |&(_origin, point), &loan, _| ((loan, point), ()),
352 );
353
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).
358 //
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`
362 // joined together.
363 borrow_live_at.from_join(
364 &dead_borrow_region_can_reach_dead_1,
365 &region_live_at_var,
366 |&(_origin2, point), &loan, _| ((loan, point), ()),
367 );
368
369 // errors(loan, point) :-
370 // invalidates(loan, point),
371 // borrow_live_at(loan, point).
372 errors.from_join(&invalidates, &borrow_live_at, |&(loan, point), _, _| {
373 (loan, point)
374 });
375 }
376
377 if result.dump_enabled {
378 let subset_o1p = subset_o1p.complete();
379 assert!(
380 subset_o1p
381 .iter()
382 .filter(|&((origin1, _), origin2)| origin1 == origin2)
383 .count()
384 == 0,
385 "unwanted subset symmetries"
386 );
387 for &((origin1, location), origin2) in subset_o1p.iter() {
388 result
389 .subset
390 .entry(location)
391 .or_default()
392 .entry(origin1)
393 .or_default()
394 .insert(origin2);
395 }
396
397 let requires_op = requires_op.complete();
398 for &((origin, location), loan) in requires_op.iter() {
399 result
400 .restricts
401 .entry(location)
402 .or_default()
403 .entry(origin)
404 .or_default()
405 .insert(loan);
406 }
407
408 let borrow_live_at = borrow_live_at.complete();
409 for &((loan, location), _) in borrow_live_at.iter() {
410 result
411 .borrow_live_at
412 .entry(location)
413 .or_default()
414 .push(loan);
415 }
416 }
417
418 errors.complete()
419 };
420
421 info!(
422 "errors is complete: {} tuples, {:?}",
423 errors.len(),
424 timer.elapsed()
425 );
426
427 errors
428 }