Skip to content

Commit 7e2d22d

Browse files
lqdlqd
committed
naive: number and document the rules
This will help readability, and documentation, when we extract the rules to the book. Also describes more precisely why we need a duplicate liveness relation.
1 parent ee15395 commit 7e2d22d

File tree

1 file changed

+85
-42
lines changed

1 file changed

+85
-42
lines changed

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

Lines changed: 85 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,11 @@ pub(super) fn compute<T: FactTypes>(
4545
// `loan_invalidated_at` facts, stored ready for joins
4646
let loan_invalidated_at =
4747
iteration.variable::<((T::Loan, T::Point), ())>("loan_invalidated_at");
48+
loan_invalidated_at.extend(
49+
ctx.loan_invalidated_at
50+
.iter()
51+
.map(|&(loan, point)| ((loan, point), ())),
52+
);
4853

4954
// different indices for `subset`.
5055
let subset_o1p = iteration.variable_indistinct("subset_o1p");
@@ -54,10 +59,32 @@ pub(super) fn compute<T: FactTypes>(
5459
let origin_contains_loan_on_entry_op =
5560
iteration.variable_indistinct("origin_contains_loan_on_entry_op");
5661

57-
// we need `origin_live_on_entry` in both variable and relation forms.
58-
// (respectively, for the regular join and the leapjoin).
62+
// Unfortunately, we need `origin_live_on_entry` in both variable and relation forms:
63+
// We need:
64+
// - `origin_live_on_entry` as a Relation for the leapjoins in rules 3 & 6
65+
// - `origin_live_on_entry` as a Variable for the join in rule 7
66+
//
67+
// The leapjoins use `origin_live_on_entry` as `(Origin, Point)` tuples, while the join uses
68+
// it as a `((O, P), ())` tuple to filter the `((Origin, Point), Loan)` tuples from
69+
// `origin_contains_loan_on_entry_op`.
70+
//
71+
// The regular join in rule 7 could be turned into a `filter_with` leaper but that would
72+
// result in a leapjoin with no `extend_*` leapers: a leapjoin that is not well-formed.
73+
// Doing the filtering via an `extend_with` leaper would be extremely inefficient.
74+
//
75+
// Until there's an API in datafrog to handle this use-case better, we do a slightly less
76+
// inefficient thing of copying the whole static input into a Variable to use a regular
77+
// join, even though the liveness information can be quite heavy (around 1M tuples
78+
// on `clap`).
79+
// This is the Naive variant so this is not a big problem, but needs an
80+
// explanation.
5981
let origin_live_on_entry_var =
6082
iteration.variable::<((T::Origin, T::Point), ())>("origin_live_on_entry");
83+
origin_live_on_entry_var.extend(
84+
origin_live_on_entry_rel
85+
.iter()
86+
.map(|&(origin, point)| ((origin, point), ())),
87+
);
6188

6289
// variable and index to compute the subsets of placeholders
6390
let subset_placeholder =
@@ -68,19 +95,19 @@ pub(super) fn compute<T: FactTypes>(
6895
let errors = iteration.variable("errors");
6996
let subset_errors = iteration.variable::<(T::Origin, T::Origin, T::Point)>("subset_errors");
7097

71-
// load initial facts.
98+
// load initial facts:
99+
100+
// Rule 1: the initial subsets are the non-transitive `subset_base` static input.
101+
//
102+
// subset(Origin1, Origin2, Point) :-
103+
// subset_base(Origin1, Origin2, Point).
72104
subset.extend(ctx.subset_base.iter());
105+
106+
// Rule 4: the issuing origins are the ones initially containing loans.
107+
//
108+
// origin_contains_loan_on_entry(Origin, Loan, Point) :-
109+
// loan_issued_at(Origin, Loan, Point).
73110
origin_contains_loan_on_entry.extend(ctx.loan_issued_at.iter());
74-
loan_invalidated_at.extend(
75-
ctx.loan_invalidated_at
76-
.iter()
77-
.map(|&(loan, point)| ((loan, point), ())),
78-
);
79-
origin_live_on_entry_var.extend(
80-
origin_live_on_entry_rel
81-
.iter()
82-
.map(|&(origin, point)| ((origin, point), ())),
83-
);
84111

85112
// .. and then start iterating rules!
86113
while iteration.changed() {
@@ -104,7 +131,7 @@ pub(super) fn compute<T: FactTypes>(
104131
.elements
105132
.retain(|&(origin1, origin2, _)| origin1 != origin2);
106133

107-
// remap fields to re-index by keys.
134+
// Remap fields to re-index by keys, to prepare the data needed by the rules below.
108135
subset_o1p.from_map(&subset, |&(origin1, origin2, point)| {
109136
((origin1, point), origin2)
110137
});
@@ -121,24 +148,26 @@ pub(super) fn compute<T: FactTypes>(
121148
((origin, point), loan)
122149
});
123150

124-
// subset(origin1, origin2, point) :-
125-
// subset_base(origin1, origin2, point).
126-
// Already loaded; `subset_base` is static.
151+
// Rule 1: done above, as part of the static input facts setup.
127152

128-
// subset(origin1, origin3, point) :-
129-
// subset(origin1, origin2, point),
130-
// subset(origin2, origin3, point).
153+
// Rule 2: compute the subset transitive closure, at a given point.
154+
//
155+
// subset(Origin1, Origin3, Point) :-
156+
// subset(Origin1, Origin2, Point),
157+
// subset(Origin2, Origin3, Point).
131158
subset.from_join(
132159
&subset_o2p,
133160
&subset_o1p,
134161
|&(_origin2, point), &origin1, &origin3| (origin1, origin3, point),
135162
);
136163

137-
// subset(origin1, origin2, point2) :-
138-
// subset(origin1, origin2, point1),
139-
// cfg_edge(point1, point2),
140-
// origin_live_on_entry(origin1, point2),
141-
// origin_live_on_entry(origin2, point2).
164+
// Rule 3: propagate subsets along the CFG, according to liveness.
165+
//
166+
// subset(Origin1, Origin2, Point2) :-
167+
// subset(Origin1, Origin2, Point1),
168+
// cfg_edge(Point1, Point2),
169+
// origin_live_on_entry(Origin1, Point2),
170+
// origin_live_on_entry(Origin2, Point2).
142171
subset.from_leapjoin(
143172
&subset,
144173
(
@@ -149,24 +178,26 @@ pub(super) fn compute<T: FactTypes>(
149178
|&(origin1, origin2, _point1), &point2| (origin1, origin2, point2),
150179
);
151180

152-
// origin_contains_loan_on_entry(origin, loan, point) :-
153-
// loan_issued_at(origin, loan, point).
154-
// Already loaded; `loan_issued_at` is static.
181+
// Rule 4: done above as part of the static input facts setup.
155182

156-
// origin_contains_loan_on_entry(origin2, loan, point) :-
157-
// origin_contains_loan_on_entry(origin1, loan, point),
158-
// subset(origin1, origin2, point).
183+
// Rule 5: propagate loans within origins, at a given point, according to subsets.
184+
//
185+
// origin_contains_loan_on_entry(Origin2, Loan, Point) :-
186+
// origin_contains_loan_on_entry(Origin1, Loan, Point),
187+
// subset(Origin1, Origin2, Point).
159188
origin_contains_loan_on_entry.from_join(
160189
&origin_contains_loan_on_entry_op,
161190
&subset_o1p,
162191
|&(_origin1, point), &loan, &origin2| (origin2, loan, point),
163192
);
164193

165-
// origin_contains_loan_on_entry(origin, loan, point2) :-
166-
// origin_contains_loan_on_entry(origin, loan, point1),
167-
// !loan_killed_at(loan, point1),
168-
// cfg_edge(point1, point2),
169-
// origin_live_on_entry(origin, point2).
194+
// Rule 6: propagate loans along the CFG, according to liveness.
195+
//
196+
// origin_contains_loan_on_entry(Origin, Loan, Point2) :-
197+
// origin_contains_loan_on_entry(Origin, Loan, Point1),
198+
// !loan_killed_at(Loan, Point1),
199+
// cfg_edge(Point1, Point2),
200+
// origin_live_on_entry(Origin, Point2).
170201
origin_contains_loan_on_entry.from_leapjoin(
171202
&origin_contains_loan_on_entry,
172203
(
@@ -177,24 +208,31 @@ pub(super) fn compute<T: FactTypes>(
177208
|&(origin, loan, _point1), &point2| (origin, loan, point2),
178209
);
179210

180-
// loan_live_at(loan, point) :-
181-
// origin_contains_loan_on_entry(origin, loan, point),
182-
// origin_live_on_entry(origin, point).
211+
// Rule 7: compute whether a loan is live at a given point, i.e. whether it is
212+
// contained in a live origin at this point.
213+
//
214+
// loan_live_at(Loan, Point) :-
215+
// origin_contains_loan_on_entry(Origin, Loan, Point),
216+
// origin_live_on_entry(Origin, Point).
183217
loan_live_at.from_join(
184218
&origin_contains_loan_on_entry_op,
185219
&origin_live_on_entry_var,
186220
|&(_origin, point), &loan, _| ((loan, point), ()),
187221
);
188222

189-
// errors(loan, point) :-
190-
// loan_invalidated_at(loan, point),
191-
// loan_live_at(loan, point).
223+
// Rule 8: compute illegal access errors, i.e. an invalidation of a live loan.
224+
//
225+
// errors(Loan, Point) :-
226+
// loan_invalidated_at(Loan, Point),
227+
// loan_live_at(Loan, Point).
192228
errors.from_join(
193229
&loan_invalidated_at,
194230
&loan_live_at,
195231
|&(loan, point), _, _| (loan, point),
196232
);
197233

234+
// Rule 9: compute the subsets of the placeholder origins, at a given point.
235+
//
198236
// subset_placeholder(Origin1, Origin2, Point) :-
199237
// subset(Origin1, Origin2, Point),
200238
// placeholder_origin(Origin1).
@@ -210,6 +248,8 @@ pub(super) fn compute<T: FactTypes>(
210248
|&((origin1, point), origin2), _| (origin1, origin2, point),
211249
);
212250

251+
// Rule 10: compute the subset transitive closure of placeholder origins.
252+
//
213253
// subset_placeholder(Origin1, Origin3, Point) :-
214254
// subset_placeholder(Origin1, Origin2, Point),
215255
// subset(Origin2, Origin3, Point).
@@ -219,6 +259,9 @@ pub(super) fn compute<T: FactTypes>(
219259
|&(_origin2, point), &origin1, &origin3| (origin1, origin3, point),
220260
);
221261

262+
// Rule 11: compute illegal subset relations errors, i.e. the undeclared subsets
263+
// between two placeholder origins.
264+
//
222265
// subset_errors(Origin1, Origin2, Point) :-
223266
// subset_placeholder(Origin1, Origin2, Point),
224267
// placeholder_origin(Origin2),

0 commit comments

Comments
 (0)