Skip to content

Commit 61534f9

Browse files
lqdlqd
committed
naive: handle placeholders explicitly in the 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)
1 parent 0847fc0 commit 61534f9

File tree

1 file changed

+83
-9
lines changed

1 file changed

+83
-9
lines changed

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

Lines changed: 83 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -146,17 +146,61 @@ pub(super) fn compute<T: FactTypes>(
146146

147147
// Rule 3: propagate subsets along the CFG, according to liveness.
148148
//
149+
// Since there are two alternative predicates, A and B, this will result in four
150+
// expansions of this rule: two alternatives for predicate A, and two alternatives for
151+
// predicate B.
152+
//
149153
// subset(Origin1, Origin2, Point2) :-
150154
// subset(Origin1, Origin2, Point1),
151155
// cfg_edge(Point1, Point2),
152-
// origin_live_on_entry(Origin1, Point2),
153-
// origin_live_on_entry(Origin2, Point2).
156+
// (origin_live_on_entry(Origin1, Point2); placeholder_origin(Origin1)), // -> A
157+
// (origin_live_on_entry(Origin2, Point2); placeholder_origin(Origin2)). // -> B
158+
//
159+
// 1) Rule 3, expansion 1 of 4
160+
// - predicate A: `origin_live_on_entry(Origin1, Point2)`
161+
// - predicate B: `origin_live_on_entry(Origin2, Point2)`
162+
subset.from_leapjoin(
163+
&subset,
164+
(
165+
cfg_edge.extend_with(|&(_origin1, _origin2, point1)| point1),
166+
origin_live_on_entry_rel.extend_with(|&(origin1, _origin2, _point1)| origin1), // -> A
167+
origin_live_on_entry_rel.extend_with(|&(_origin1, origin2, _point1)| origin2), // -> B
168+
),
169+
|&(origin1, origin2, _point1), &point2| (origin1, origin2, point2),
170+
);
171+
// 2) Rule 3, expansion 2 of 4
172+
// - predicate A: `origin_live_on_entry(Origin1, Point2)`
173+
// - predicate B: `placeholder_origin(Origin2)`
154174
subset.from_leapjoin(
155175
&subset,
156176
(
157177
cfg_edge.extend_with(|&(_origin1, _origin2, point1)| point1),
158-
origin_live_on_entry_rel.extend_with(|&(origin1, _origin2, _point1)| origin1),
159-
origin_live_on_entry_rel.extend_with(|&(_origin1, origin2, _point1)| origin2),
178+
origin_live_on_entry_rel.extend_with(|&(origin1, _origin2, _point1)| origin1), // -> A
179+
placeholder_origin.filter_with(|&(_origin1, origin2, _point1)| (origin2, ())), // -> B
180+
),
181+
|&(origin1, origin2, _point1), &point2| (origin1, origin2, point2),
182+
);
183+
// 3) Rule 3, expansion 3 of 4
184+
// - predicate A: `placeholder_origin(Origin1)`
185+
// - predicate B: `origin_live_on_entry(Origin2, Point2)`
186+
subset.from_leapjoin(
187+
&subset,
188+
(
189+
cfg_edge.extend_with(|&(_origin1, _origin2, point1)| point1),
190+
placeholder_origin.filter_with(|&(origin1, _origin2, _point1)| (origin1, ())), // -> A
191+
origin_live_on_entry_rel.extend_with(|&(_origin1, origin2, _point1)| origin2), // -> B
192+
),
193+
|&(origin1, origin2, _point1), &point2| (origin1, origin2, point2),
194+
);
195+
// 4) Rule 3, expansion 4 of 4
196+
// - predicate A: `placeholder_origin(Origin1)`
197+
// - predicate B: `placeholder_origin(Origin2)`
198+
subset.from_leapjoin(
199+
&subset,
200+
(
201+
cfg_edge.extend_with(|&(_origin1, _origin2, point1)| point1),
202+
placeholder_origin.filter_with(|&(origin1, _origin2, _point1)| (origin1, ())), // -> A
203+
placeholder_origin.filter_with(|&(_origin1, origin2, _point1)| (origin2, ())), // -> B
160204
),
161205
|&(origin1, origin2, _point1), &point2| (origin1, origin2, point2),
162206
);
@@ -176,32 +220,62 @@ pub(super) fn compute<T: FactTypes>(
176220

177221
// Rule 6: propagate loans along the CFG, according to liveness.
178222
//
223+
// Since there is one alternative predicate, A, this will result in two expansions
224+
// of this rule: one for each alternative for predicate A.
225+
//
179226
// origin_contains_loan_on_entry(Origin, Loan, Point2) :-
180227
// origin_contains_loan_on_entry(Origin, Loan, Point1),
181228
// !loan_killed_at(Loan, Point1),
182229
// cfg_edge(Point1, Point2),
183-
// origin_live_on_entry(Origin, Point2).
230+
// (origin_live_on_entry(Origin, Point2); placeholder_origin(Origin)). // -> A
231+
//
232+
// 1) Rule 6, expansion 1 of 2
233+
// - predicate A: `origin_live_on_entry(Origin, Point2)`
234+
origin_contains_loan_on_entry.from_leapjoin(
235+
&origin_contains_loan_on_entry,
236+
(
237+
loan_killed_at.filter_anti(|&(_origin, loan, point1)| (loan, point1)),
238+
cfg_edge.extend_with(|&(_origin, _loan, point1)| point1),
239+
origin_live_on_entry_rel.extend_with(|&(origin, _loan, _point1)| origin), // -> A
240+
),
241+
|&(origin, loan, _point1), &point2| (origin, loan, point2),
242+
);
243+
// 2) Rule 6, expansion 2 of 2
244+
// - predicate A: `placeholder_origin(Origin)`
184245
origin_contains_loan_on_entry.from_leapjoin(
185246
&origin_contains_loan_on_entry,
186247
(
187248
loan_killed_at.filter_anti(|&(_origin, loan, point1)| (loan, point1)),
188249
cfg_edge.extend_with(|&(_origin, _loan, point1)| point1),
189-
origin_live_on_entry_rel.extend_with(|&(origin, _loan, _point1)| origin),
250+
placeholder_origin.filter_with(|&(origin, _loan, _point1)| (origin, ())), // -> A
190251
),
191252
|&(origin, loan, _point1), &point2| (origin, loan, point2),
192253
);
193254

194255
// Rule 7: compute whether a loan is live at a given point, i.e. whether it is
195256
// contained in a live origin at this point.
196257
//
258+
// Since there is one alternative predicate, A, this will result in two expansions
259+
// of this rule: one for each alternative for predicate A.
260+
//
197261
// loan_live_at(Loan, Point) :-
198262
// origin_contains_loan_on_entry(Origin, Loan, Point),
199-
// origin_live_on_entry(Origin, Point).
263+
// (origin_live_on_entry(Origin, Point); placeholder_origin(Origin)). // -> A
264+
//
265+
// 1) Rule 7, expansion 1 of 2
266+
// - predicate A: `origin_live_on_entry(Origin, Point)`
200267
loan_live_at.from_join(
201268
&origin_contains_loan_on_entry_op,
202-
&origin_live_on_entry_var,
269+
&origin_live_on_entry_var, // -> A
203270
|&(_origin, point), &loan, _| ((loan, point), ()),
204271
);
272+
// 2) Rule 7, expansion 2 of 2
273+
// - predicate A: `placeholder_origin(Origin)`
274+
loan_live_at.from_leapjoin(
275+
&origin_contains_loan_on_entry_op,
276+
placeholder_origin.extend_with(|&((origin, _point), _loan)| origin), // -> A
277+
|&((_origin, point), loan), _| ((loan, point), ()),
278+
);
205279

206280
// Rule 8: compute illegal access errors, i.e. an invalidation of a live loan.
207281
//
@@ -226,7 +300,7 @@ pub(super) fn compute<T: FactTypes>(
226300
// Here as well, WF-ness prevents this join from being a filter-only leapjoin. It
227301
// doesn't matter much, as `placeholder_origin` is single-value relation.
228302
//
229-
// subset_error(Origin1, Origin2, Point) :-
303+
// subset_errors(Origin1, Origin2, Point) :-
230304
// subset(Origin1, Origin2, Point),
231305
// placeholder_origin(Origin1),
232306
// placeholder_origin(Origin2),

0 commit comments

Comments
 (0)