Skip to content

Commit 0847fc0

Browse files
committed
location insensitive: handle placeholders explicitly instead of a by-product of liveness
Also, number and comment the rules, because the expansions are very verbose and mistakes are easy to make here. 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)
1 parent 9106e7a commit 0847fc0

File tree

1 file changed

+31
-2
lines changed

1 file changed

+31
-2
lines changed

polonius-engine/src/output/location_insensitive.rs

Lines changed: 31 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,8 @@ pub(super) fn compute<T: FactTypes>(
3131
let placeholder_loan = &ctx.placeholder_loan;
3232
let known_contains = &ctx.known_contains;
3333

34+
// Rule 1: the subsets are the non-transitive `subset_base` static input.
35+
//
3436
// subset(Origin1, Origin2) :-
3537
// subset_base(Origin1, Origin2, _).
3638
let subset = Relation::from_iter(
@@ -52,6 +54,8 @@ pub(super) fn compute<T: FactTypes>(
5254

5355
// load initial facts.
5456

57+
// Rule 2: the issuing origins are the ones initially containing loans.
58+
//
5559
// origin_contains_loan_on_entry(Origin, Loan) :-
5660
// loan_issued_at(Origin, Loan, _).
5761
origin_contains_loan_on_entry.extend(
@@ -60,6 +64,8 @@ pub(super) fn compute<T: FactTypes>(
6064
.map(|&(origin, loan, _point)| (origin, loan)),
6165
);
6266

67+
// Rule 3: the placeholder origins also contain their placeholder loan.
68+
//
6369
// origin_contains_loan_on_entry(Origin, Loan) :-
6470
// placeholder_loan(Origin, Loan).
6571
origin_contains_loan_on_entry.extend(
@@ -70,6 +76,8 @@ pub(super) fn compute<T: FactTypes>(
7076

7177
// .. and then start iterating rules!
7278
while iteration.changed() {
79+
// Rule 4: propagate the loans from the origins to their subsets.
80+
//
7381
// origin_contains_loan_on_entry(Origin2, Loan) :-
7482
// origin_contains_loan_on_entry(Origin1, Loan),
7583
// subset(Origin1, Origin2).
@@ -82,9 +90,15 @@ pub(super) fn compute<T: FactTypes>(
8290
|&_origin1, &loan, &origin2| (origin2, loan),
8391
);
8492

93+
// Rule 5: compute potential errors, i.e. loans that are contained in an origin at any point in the CFG, and
94+
// which are invalidated at a point where that origin is live.
95+
//
8596
// loan_live_at(Loan, Point) :-
8697
// origin_contains_loan_on_entry(Origin, Loan),
87-
// origin_live_on_entry(Origin, Point)
98+
// (origin_live_on_entry(Origin, Point); placeholder_origin(Origin)). // -> A
99+
//
100+
// Since there is one alternative predicate, A, this will result in two expansions
101+
// of this rule: one for each alternative for predicate A.
88102
//
89103
// potential_errors(Loan, Point) :-
90104
// loan_invalidated_at(Loan, Point),
@@ -93,15 +107,30 @@ pub(super) fn compute<T: FactTypes>(
93107
// Note: we don't need to materialize `loan_live_at` here
94108
// so we can inline it in the `potential_errors` relation.
95109
//
110+
// 1) Rule 5, expansion 1 of 2
111+
// - predicate A: `origin_live_on_entry(Origin, Point)`
96112
potential_errors.from_leapjoin(
97113
&origin_contains_loan_on_entry,
98114
(
99-
origin_live_on_entry.extend_with(|&(origin, _loan)| origin),
115+
origin_live_on_entry.extend_with(|&(origin, _loan)| origin), // -> A
116+
loan_invalidated_at.extend_with(|&(_origin, loan)| loan),
117+
),
118+
|&(_origin, loan), &point| (loan, point),
119+
);
120+
// 2) Rule 5, expansion 2 of 2
121+
// - predicate A: `placeholder_origin(Origin)`
122+
potential_errors.from_leapjoin(
123+
&origin_contains_loan_on_entry,
124+
(
125+
placeholder_origin.filter_with(|&(origin, _loan)| (origin, ())), // -> A
100126
loan_invalidated_at.extend_with(|&(_origin, loan)| loan),
101127
),
102128
|&(_origin, loan), &point| (loan, point),
103129
);
104130

131+
// Rule 6: compute potential subset errors, i.e. the placeholder loans which ultimately
132+
// flowed into another placeholder origin unexpectedly.
133+
//
105134
// potential_subset_errors(Origin1, Origin2) :-
106135
// placeholder(Origin1, Loan1),
107136
// placeholder(Origin2, _),

0 commit comments

Comments
 (0)