Skip to content

Commit e6dd2fb

Browse files
lqdlqd
committed
opt: handle placeholders explicitly in the rules
Also, number and comment some rules. We simplified the rules by modeling the fact that placeholder origins are live at all points by ... materializing this as actual tuples in the `origin_live_on_entry` relation, even though liveness analysis does not computes that. This was also done because soufflé provides an easy `;` alternative operator, while datafrog requires us to do the alternative expansions manually. (Also we were lazy). Where possible `filter_with` leapers were added, and where WF-ness would not be possible, `extend_with` leapers were used. This should be similar here: the `placeholder_origin` relation being a single value relation, there is only a single unit tuple to extend a key with.
1 parent f103a75 commit e6dd2fb

File tree

1 file changed

+188
-17
lines changed

1 file changed

+188
-17
lines changed

‎polonius-engine/src/output/datafrog_opt.rs‎

Lines changed: 188 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -155,6 +155,8 @@ pub(super) fn compute<T: FactTypes>(
155155
.map(|&(origin, point)| ((origin, point), ())),
156156
);
157157

158+
// Rule 1: the initial subsets are the non-transitive `subset_base` static input.
159+
//
158160
// subset(origin1, origin2, point) :-
159161
// subset_base(origin1, origin2, point).
160162
subset_o1p.extend(
@@ -163,6 +165,8 @@ pub(super) fn compute<T: FactTypes>(
163165
.map(|&(origin1, origin2, point)| ((origin1, point), origin2)),
164166
);
165167

168+
// Rule 2: the issuing origins are the ones initially containing loans.
169+
//
166170
// origin_contains_loan_on_entry(origin, loan, point) :-
167171
// loan_issued_at(origin, loan, point).
168172
origin_contains_loan_on_entry_op.extend(
@@ -192,25 +196,47 @@ pub(super) fn compute<T: FactTypes>(
192196
.borrow_mut()
193197
.elements
194198
.retain(|&(origin1, origin2, _)| origin1 != origin2);
199+
195200
subset_placeholder_o2p.from_map(&subset_placeholder, |&(origin1, origin2, point)| {
196201
((origin2, point), origin1)
197202
});
198203

204+
// Rule 3
205+
//
199206
// live_to_dying_regions(origin1, origin2, point1, point2) :-
200207
// subset(origin1, origin2, point1),
201208
// cfg_edge(point1, point2),
202-
// origin_live_on_entry(origin1, point2),
209+
// (origin_live_on_entry(origin1, point2); placeholder_origin(origin1)), // -> A
203210
// !origin_live_on_entry(origin2, point2).
211+
//
212+
// Since there is one alternative predicate, A, this will result in two expansions
213+
// of this rule: one for each alternative for predicate A.
214+
//
215+
// 1) Rule 3, expansion 1 of 2
216+
// - predicate A: `origin_live_on_entry(origin1, point2)`
204217
live_to_dying_regions_o2pq.from_leapjoin(
205218
&subset_o1p,
206219
(
207220
cfg_edge_rel.extend_with(|&((_, point1), _)| point1),
208-
origin_live_on_entry_rel.extend_with(|&((origin1, _), _)| origin1),
221+
origin_live_on_entry_rel.extend_with(|&((origin1, _), _)| origin1), // -> A
222+
origin_live_on_entry_rel.extend_anti(|&((_, _), origin2)| origin2),
223+
),
224+
|&((origin1, point1), origin2), &point2| ((origin2, point1, point2), origin1),
225+
);
226+
// 2) Rule 3, expansion 2 of 2
227+
// - predicate A: `placeholder_origin(origin1)`
228+
live_to_dying_regions_o2pq.from_leapjoin(
229+
&subset_o1p,
230+
(
231+
cfg_edge_rel.extend_with(|&((_, point1), _)| point1),
232+
placeholder_origin.filter_with(|&((origin1, _), _)| (origin1, ())), // -> A
209233
origin_live_on_entry_rel.extend_anti(|&((_, _), origin2)| origin2),
210234
),
211235
|&((origin1, point1), origin2), &point2| ((origin2, point1, point2), origin1),
212236
);
213237

238+
// Rule 4
239+
//
214240
// dying_region_requires((origin, point1, point2), loan) :-
215241
// origin_contains_loan_on_entry(origin, loan, point1),
216242
// !loan_killed_at(loan, point1),
@@ -226,20 +252,26 @@ pub(super) fn compute<T: FactTypes>(
226252
|&((origin, point1), loan), &point2| ((origin, point1, point2), loan),
227253
);
228254

255+
// Rule 5
256+
//
229257
// dying_can_reach_origins(origin2, point1, point2) :-
230258
// live_to_dying_regions(_, origin2, point1, point2).
231259
dying_can_reach_origins.from_map(
232260
&live_to_dying_regions_o2pq,
233261
|&((origin2, point1, point2), _origin1)| ((origin2, point1), point2),
234262
);
235263

264+
// Rule 6
265+
//
236266
// dying_can_reach_origins(origin, point1, point2) :-
237267
// dying_region_requires(origin, point1, point2, _loan).
238268
dying_can_reach_origins.from_map(
239269
&dying_region_requires,
240270
|&((origin, point1, point2), _loan)| ((origin, point1), point2),
241271
);
242272

273+
// Rule 7
274+
//
243275
// dying_can_reach(origin1, origin2, point1, point2) :-
244276
// dying_can_reach_origins(origin1, point1, point2),
245277
// subset(origin1, origin2, point1).
@@ -249,6 +281,8 @@ pub(super) fn compute<T: FactTypes>(
249281
|&(origin1, point1), &point2, &origin2| ((origin2, point2), (origin1, point1)),
250282
);
251283

284+
// Rule 8
285+
//
252286
// dying_can_reach(origin1, origin3, point1, point2) :-
253287
// dying_can_reach(origin1, origin2, point1, point2),
254288
// !origin_live_on_entry(origin2, point2),
@@ -270,33 +304,96 @@ pub(super) fn compute<T: FactTypes>(
270304
},
271305
);
272306

307+
// Rule 9
308+
//
273309
// dying_can_reach_live(origin1, origin2, point1, point2) :-
274310
// dying_can_reach(origin1, origin2, point1, point2),
275-
// origin_live_on_entry(origin2, point2).
311+
// (origin_live_on_entry(origin2, point2); placeholder_origin(origin2)). // -> A
312+
//
313+
// Since there is one alternative predicate, A, this will result in two expansions
314+
// of this rule: one for each alternative for predicate A.
315+
//
316+
// 1) Rule 9, expansion 1 of 2
317+
// - predicate A: `origin_live_on_entry(origin2, point2)`
276318
dying_can_reach_live.from_join(
277319
&dying_can_reach_o2q,
278-
&origin_live_on_entry_var,
320+
&origin_live_on_entry_var, // -> A
279321
|&(origin2, point2), &(origin1, point1), _| ((origin1, point1, point2), origin2),
280322
);
323+
// 2) Rule 9, expansion 2 of 2
324+
// - predicate A: `placeholder_origin(origin2)`
325+
dying_can_reach_live.from_leapjoin(
326+
&dying_can_reach_o2q,
327+
placeholder_origin.extend_with(|&((origin2, _), (_, _))| origin2), // -> A
328+
|&((origin2, point2), (origin1, point1)), _| ((origin1, point1, point2), origin2),
329+
);
281330

331+
// Rule 10
332+
//
282333
// subset(origin1, origin2, point2) :-
283334
// subset(origin1, origin2, point1),
284335
// cfg_edge(point1, point2),
285-
// origin_live_on_entry(origin1, point2),
286-
// origin_live_on_entry(origin2, point2).
336+
// (origin_live_on_entry(origin1, point2); placeholder_origin(origin1)), // -> A
337+
// (origin_live_on_entry(origin2, point2); placeholder_origin(origin2)). // -> B
338+
//
339+
// Since there are two alternative predicates, A and B, this will result in four
340+
// expansions of this rule: two alternatives for predicate A, and two alternatives for
341+
// predicate B.
287342
//
288343
// Carry `origin1 <= origin2` from `point1` into `point2` if both `origin1` and
289344
// `origin2` are live in `point2`.
345+
//
346+
// 1) Rule 10, expansion 1 of 4
347+
// - predicate A: `origin_live_on_entry(origin1, point2)`
348+
// - predicate B: `origin_live_on_entry(origin2, point2)`
349+
subset_o1p.from_leapjoin(
350+
&subset_o1p,
351+
(
352+
cfg_edge_rel.extend_with(|&((_, point1), _)| point1),
353+
origin_live_on_entry_rel.extend_with(|&((origin1, _), _)| origin1), // -> A
354+
origin_live_on_entry_rel.extend_with(|&((_, _), origin2)| origin2), // -> B
355+
),
356+
|&((origin1, _point1), origin2), &point2| ((origin1, point2), origin2),
357+
);
358+
// 2) Rule 10, expansion 2 of 4
359+
// - predicate A: `origin_live_on_entry(origin1, point2)`
360+
// - predicate B: `placeholder_origin(origin2)`
361+
subset_o1p.from_leapjoin(
362+
&subset_o1p,
363+
(
364+
cfg_edge_rel.extend_with(|&((_, point1), _)| point1),
365+
origin_live_on_entry_rel.extend_with(|&((origin1, _), _)| origin1), // -> A
366+
placeholder_origin.filter_with(|&((_, _), origin2)| (origin2, ())), // -> B
367+
),
368+
|&((origin1, _point1), origin2), &point2| ((origin1, point2), origin2),
369+
);
370+
// 3) Rule 10, expansion 3 of 4
371+
// - predicate A: `placeholder_origin(origin1)`
372+
// - predicate B: `origin_live_on_entry(origin2, point2)`
290373
subset_o1p.from_leapjoin(
291374
&subset_o1p,
292375
(
293376
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),
377+
placeholder_origin.filter_with(|&((origin1, _), _)| (origin1, ())), // -> A
378+
origin_live_on_entry_rel.extend_with(|&((_, _), origin2)| origin2), // -> B
379+
),
380+
|&((origin1, _point1), origin2), &point2| ((origin1, point2), origin2),
381+
);
382+
// 4) Rule 10, expansion 4 of 4
383+
// - predicate A: `placeholder_origin(origin1)`
384+
// - predicate B: `placeholder_origin(origin2)`
385+
subset_o1p.from_leapjoin(
386+
&subset_o1p,
387+
(
388+
cfg_edge_rel.extend_with(|&((_, point1), _)| point1),
389+
placeholder_origin.filter_with(|&((origin1, _), _)| (origin1, ())), // -> A
390+
placeholder_origin.filter_with(|&((_, _), origin2)| (origin2, ())), // -> B
296391
),
297392
|&((origin1, _point1), origin2), &point2| ((origin1, point2), origin2),
298393
);
299394

395+
// Rule 11
396+
//
300397
// subset(origin1, origin3, point2) :-
301398
// live_to_dying_regions(origin1, origin2, point1, point2),
302399
// dying_can_reach_live(origin2, origin3, point1, point2).
@@ -306,6 +403,8 @@ pub(super) fn compute<T: FactTypes>(
306403
|&(_origin2, _point1, point2), &origin1, &origin3| ((origin1, point2), origin3),
307404
);
308405

406+
// Rule 12
407+
//
309408
// origin_contains_loan_on_entry(origin2, loan, point2) :-
310409
// dying_region_requires(origin1, loan, point1, point2),
311410
// dying_can_reach_live(origin1, origin2, point1, point2).
@@ -321,35 +420,70 @@ pub(super) fn compute<T: FactTypes>(
321420
|&(_origin1, _point1, point2), &loan, &origin2| ((origin2, point2), loan),
322421
);
323422

423+
// Rule 13
424+
//
324425
// origin_contains_loan_on_entry(origin, loan, point2) :-
325426
// origin_contains_loan_on_entry(origin, loan, point1),
326427
// !loan_killed_at(loan, point1),
327428
// cfg_edge(point1, point2),
328-
// origin_live_on_entry(origin, point2).
429+
// (origin_live_on_entry(origin, point2); placeholder_origin(origin)). // -> A
430+
//
431+
// Since there is one alternative predicate, A, this will result in two expansions
432+
// of this rule: one for each alternative for predicate A.
433+
//
434+
// 1) Rule 13, expansion 1 of 2
435+
// - predicate A: `origin_live_on_entry(origin, point2)`
436+
origin_contains_loan_on_entry_op.from_leapjoin(
437+
&origin_contains_loan_on_entry_op,
438+
(
439+
loan_killed_at.filter_anti(|&((_, point1), loan)| (loan, point1)),
440+
cfg_edge_rel.extend_with(|&((_, point1), _)| point1),
441+
origin_live_on_entry_rel.extend_with(|&((origin, _), _)| origin), // -> A
442+
),
443+
|&((origin, _), loan), &point2| ((origin, point2), loan),
444+
);
445+
// 2) Rule 13, expansion 2 of 2
446+
// - predicate A: `placeholder_origin(origin)`
329447
origin_contains_loan_on_entry_op.from_leapjoin(
330448
&origin_contains_loan_on_entry_op,
331449
(
332450
loan_killed_at.filter_anti(|&((_, point1), loan)| (loan, point1)),
333451
cfg_edge_rel.extend_with(|&((_, point1), _)| point1),
334-
origin_live_on_entry_rel.extend_with(|&((origin, _), _)| origin),
452+
placeholder_origin.filter_with(|&((origin, _), _)| (origin, ())), // -> A
335453
),
336454
|&((origin, _), loan), &point2| ((origin, point2), loan),
337455
);
338456

457+
// Rule 14
458+
//
339459
// dead_borrow_region_can_reach_root((origin, point), loan) :-
340460
// loan_issued_at(origin, loan, point),
341461
// !origin_live_on_entry(origin, point).
462+
//
463+
// Even though `loan_issued_at_op` is a Variable here for the antijoin API (and
464+
// nowadays datafrog's Relations can be built with `Relation::from_antijoin`), this is
465+
// a join over two static inputs. It should not produce facts each round, and could be
466+
// moved out of the loop (and most likely should be inlined into rule 15).
467+
//
342468
dead_borrow_region_can_reach_root.from_antijoin(
343469
&loan_issued_at_op,
344470
&origin_live_on_entry_rel,
345471
|&(origin, point), &loan| ((origin, point), loan),
346472
);
347473

474+
// Rule 15
475+
//
348476
// dead_borrow_region_can_reach_dead((origin, point), loan) :-
349477
// dead_borrow_region_can_reach_root((origin, point), loan).
478+
//
479+
// Note: this is effectively mapping over a static input, and
480+
// `dead_borrow_region_can_reach_root` could probably be inlined in this relation.
481+
//
350482
dead_borrow_region_can_reach_dead
351483
.from_map(&dead_borrow_region_can_reach_root, |&tuple| tuple);
352484

485+
// Rule 16
486+
//
353487
// dead_borrow_region_can_reach_dead((origin2, point), loan) :-
354488
// dead_borrow_region_can_reach_dead(origin1, loan, point),
355489
// subset(origin1, origin2, point),
@@ -365,30 +499,62 @@ pub(super) fn compute<T: FactTypes>(
365499
|&(origin2, point), &loan| ((origin2, point), loan),
366500
);
367501

502+
// Rule 17
503+
//
368504
// loan_live_at(loan, point) :-
369505
// origin_contains_loan_on_entry(origin, loan, point),
370-
// origin_live_on_entry(origin, point).
506+
// (origin_live_on_entry(origin, point); placeholder_origin(origin)). // -> A
507+
//
508+
// Since there is one alternative predicate, A, this will result in two expansions
509+
// of this rule: one for each alternative for predicate A.
510+
//
511+
// 1) Rule 17, expansion 1 of 2
512+
// - predicate A: `origin_live_on_entry(origin, point)`
371513
loan_live_at.from_join(
372514
&origin_contains_loan_on_entry_op,
373-
&origin_live_on_entry_var,
515+
&origin_live_on_entry_var, // -> A
374516
|&(_origin, point), &loan, _| ((loan, point), ()),
375517
);
518+
// 2) Rule 17, expansion 2 of 2
519+
// - predicate A: `placeholder_origin(origin)`
520+
loan_live_at.from_leapjoin(
521+
&origin_contains_loan_on_entry_op,
522+
placeholder_origin.extend_with(|&((origin, _point), _loan)| origin), // -> A
523+
|&((_origin, point), loan), _| ((loan, point), ()),
524+
);
376525

526+
// Rule 18
527+
//
377528
// loan_live_at(loan, point) :-
378529
// dead_borrow_region_can_reach_dead(origin1, loan, point),
379530
// subset(origin1, origin2, point),
380-
// origin_live_on_entry(origin2, point).
531+
// (origin_live_on_entry(origin2, point); placeholder_origin(origin2)). // -> A
532+
//
533+
// Since there is one alternative predicate, A, this will result in two expansions
534+
// of this rule: one for each alternative for predicate A.
381535
//
382536
// NB: the datafrog code below uses
383537
// `dead_borrow_region_can_reach_dead_1`, which is equal
384538
// to `dead_borrow_region_can_reach_dead` and `subset`
385539
// joined together.
540+
//
541+
// 1) Rule 18, expansion 1 of 2
542+
// - predicate A: `origin_live_on_entry(origin2, point)`
386543
loan_live_at.from_join(
387544
&dead_borrow_region_can_reach_dead_1,
388-
&origin_live_on_entry_var,
545+
&origin_live_on_entry_var, // -> A
389546
|&(_origin2, point), &loan, _| ((loan, point), ()),
390547
);
548+
// 2) Rule 18, expansion 2 of 2
549+
// - predicate A: `placeholder_origin(origin2)`
550+
loan_live_at.from_leapjoin(
551+
&dead_borrow_region_can_reach_dead_1,
552+
placeholder_origin.extend_with(|&((origin2, _point), _loan)| origin2), // -> A
553+
|&((_origin2, point), loan), _| ((loan, point), ()),
554+
);
391555

556+
// Rule 19: compute illegal access errors, i.e. an invalidation of a live loan.
557+
//
392558
// errors(loan, point) :-
393559
// loan_invalidated_at(loan, point),
394560
// loan_live_at(loan, point).
@@ -398,6 +564,8 @@ pub(super) fn compute<T: FactTypes>(
398564
|&(loan, point), _, _| (loan, point),
399565
);
400566

567+
// Rule 20: compute the subsets of the placeholder origins, at a given point.
568+
//
401569
// subset_placeholder(Origin1, Origin2, Point) :-
402570
// subset(Origin1, Origin2, Point),
403571
// placeholder_origin(Origin1).
@@ -413,8 +581,8 @@ pub(super) fn compute<T: FactTypes>(
413581
|&((origin1, point), origin2), _| (origin1, origin2, point),
414582
);
415583

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.
584+
// Rule 21: compute the subset transitive closure of placeholder origins.
585+
// We maintain the invariant from rule 20 that `Origin1` is a placeholder origin.
418586
//
419587
// subset_placeholder(Origin1, Origin3, Point) :-
420588
// subset_placeholder(Origin1, Origin2, Point),
@@ -425,7 +593,10 @@ pub(super) fn compute<T: FactTypes>(
425593
|&(_origin2, point), &origin1, &origin3| (origin1, origin3, point),
426594
);
427595

428-
// subset_error(Origin1, Origin2, Point) :-
596+
// Rule 22: compute illegal subset relations errors, i.e. the undeclared subsets
597+
// between two placeholder origins.
598+
//
599+
// subset_errors(Origin1, Origin2, Point) :-
429600
// subset_placeholder(Origin1, Origin2, Point),
430601
// placeholder_origin(Origin2),
431602
// !known_placeholder_subset(Origin1, Origin2).

0 commit comments

Comments
 (0)