@@ -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