Skip to content

Commit a473178

Browse files
committed
naive: simplify subset errors computation
Since we're already computing the full subset TC, adding a check for placeholder origins at the same time is simpler, and as a bonus, barely noticeable performance-wise (therefore, faster than tracking the placeholder subsets).
1 parent d67fa2a commit a473178

File tree

1 file changed

+11
-47
lines changed

1 file changed

+11
-47
lines changed

polonius-engine/src/output/naive.rs

Lines changed: 11 additions & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -84,11 +84,6 @@ pub(super) fn compute<T: FactTypes>(
8484
.map(|&(origin, point)| ((origin, point), ())),
8585
);
8686

87-
// variable and index to compute the subsets of placeholders
88-
let subset_placeholder =
89-
iteration.variable::<(T::Origin, T::Origin, T::Point)>("subset_placeholder");
90-
let subset_placeholder_o2p = iteration.variable_indistinct("subset_placeholder_o2p");
91-
9287
// output relations: illegal accesses errors, and illegal subset relations errors
9388
let errors = iteration.variable("errors");
9489
let subset_errors = iteration.variable::<(T::Origin, T::Origin, T::Point)>("subset_errors");
@@ -123,12 +118,6 @@ pub(super) fn compute<T: FactTypes>(
123118
.elements
124119
.retain(|&(origin1, origin2, _)| origin1 != origin2);
125120

126-
subset_placeholder
127-
.recent
128-
.borrow_mut()
129-
.elements
130-
.retain(|&(origin1, origin2, _)| origin1 != origin2);
131-
132121
// Remap fields to re-index by keys, to prepare the data needed by the rules below.
133122
subset_o1p.from_map(&subset, |&(origin1, origin2, point)| {
134123
((origin1, point), origin2)
@@ -137,10 +126,6 @@ pub(super) fn compute<T: FactTypes>(
137126
((origin2, point), origin1)
138127
});
139128

140-
subset_placeholder_o2p.from_map(&subset_placeholder, |&(origin1, origin2, point)| {
141-
((origin2, point), origin1)
142-
});
143-
144129
origin_contains_loan_on_entry_op
145130
.from_map(&origin_contains_loan_on_entry, |&(origin, loan, point)| {
146131
((origin, point), loan)
@@ -223,6 +208,9 @@ pub(super) fn compute<T: FactTypes>(
223208
// Here again, this join acts as a pure filter and could be a more efficient leapjoin.
224209
// However, similarly to the `origin_live_on_entry` example described above, the
225210
// leapjoin with a single `filter_with` leaper would currently not be well-formed.
211+
// We don't explictly need to materialize `loan_live_at` either, and that doesn't
212+
// change the well-formedness situation, so we still materialize it (since that also
213+
// helps in testing).
226214
//
227215
// errors(Loan, Point) :-
228216
// loan_invalidated_at(Loan, Point),
@@ -233,44 +221,20 @@ pub(super) fn compute<T: FactTypes>(
233221
|&(loan, point), _, _| (loan, point),
234222
);
235223

236-
// Rule 9: compute the subsets of the placeholder origins, at a given point.
237-
//
238-
// subset_placeholder(Origin1, Origin2, Point) :-
239-
// subset(Origin1, Origin2, Point),
240-
// placeholder_origin(Origin1).
241-
subset_placeholder.from_leapjoin(
242-
&subset_o1p,
243-
(
244-
placeholder_origin.extend_with(|&((origin1, _point), _origin2)| origin1),
245-
// remove symmetries:
246-
datafrog::ValueFilter::from(|&((origin1, _point), origin2), _| {
247-
origin1 != origin2
248-
}),
249-
),
250-
|&((origin1, point), origin2), _| (origin1, origin2, point),
251-
);
252-
253-
// Rule 10: compute the subset transitive closure of placeholder origins.
254-
//
255-
// subset_placeholder(Origin1, Origin3, Point) :-
256-
// subset_placeholder(Origin1, Origin2, Point),
257-
// subset(Origin2, Origin3, Point).
258-
subset_placeholder.from_join(
259-
&subset_placeholder_o2p,
260-
&subset_o1p,
261-
|&(_origin2, point), &origin1, &origin3| (origin1, origin3, point),
262-
);
263-
264-
// Rule 11: compute illegal subset relations errors, i.e. the undeclared subsets
224+
// Rule 9: compute illegal subset relations errors, i.e. the undeclared subsets
265225
// between two placeholder origins.
226+
// Here as well, WF-ness prevents this join from being a filter-only leapjoin. It
227+
// doesn't matter much, as `placeholder_origin` is single-value relation.
266228
//
267-
// subset_errors(Origin1, Origin2, Point) :-
268-
// subset_placeholder(Origin1, Origin2, Point),
229+
// subset_error(Origin1, Origin2, Point) :-
230+
// subset(Origin1, Origin2, Point),
231+
// placeholder_origin(Origin1),
269232
// placeholder_origin(Origin2),
270233
// !known_subset(Origin1, Origin2).
271234
subset_errors.from_leapjoin(
272-
&subset_placeholder,
235+
&subset,
273236
(
237+
placeholder_origin.extend_with(|&(origin1, _origin2, _point)| origin1),
274238
placeholder_origin.extend_with(|&(_origin1, origin2, _point)| origin2),
275239
known_subset.filter_anti(|&(origin1, origin2, _point)| (origin1, origin2)),
276240
// remove symmetries:

0 commit comments

Comments
 (0)