Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Don't re-index relations just to add an empty tuple #178

Draft
wants to merge 3 commits into
base: master
Choose a base branch
from
Draft

Don't re-index relations just to add an empty tuple #178

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
cb0461b
Remove re-indexed version of `origin_live_on_entry` from naive variant
ecstatic-morse Aug 12, 2021
440d0e8
Remove `origin_live_on_entry_var` re-index from opt variant
ecstatic-morse Aug 12, 2021
ddad94c
Remove `loan_invalidated_at` re-index from opt variant
ecstatic-morse Aug 12, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
48 changes: 15 additions & 33 deletions polonius-engine/src/output/datafrog_opt.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,24 +25,16 @@ pub(super) fn compute<T: FactTypes>(

let (errors, subset_errors) = {
// Static inputs
let origin_live_on_entry_rel = &ctx.origin_live_on_entry;
let origin_live_on_entry = &ctx.origin_live_on_entry;
let cfg_edge_rel = &ctx.cfg_edge;
let loan_killed_at = &ctx.loan_killed_at;
let known_placeholder_subset = &ctx.known_placeholder_subset;
let placeholder_origin = &ctx.placeholder_origin;
let loan_invalidated_at = &ctx.loan_invalidated_at;

// Create a new iteration context, ...
let mut iteration = Iteration::new();

// `loan_invalidated_at` facts, stored ready for joins
let loan_invalidated_at =
iteration.variable::<((T::Loan, T::Point), ())>("loan_invalidated_at");

// we need `origin_live_on_entry` in both variable and relation forms,
// (respectively, for join and antijoin).
let origin_live_on_entry_var =
iteration.variable::<((T::Origin, T::Point), ())>("origin_live_on_entry");

// `loan_issued_at` input but organized for join
let loan_issued_at_op =
iteration.variable::<((T::Origin, T::Point), T::Loan)>("loan_issued_at_op");
Expand Down Expand Up @@ -144,16 +136,6 @@ pub(super) fn compute<T: FactTypes>(
.iter()
.map(|&(origin, loan, point)| ((origin, point), loan)),
);
loan_invalidated_at.extend(
ctx.loan_invalidated_at
.iter()
.map(|&(loan, point)| ((loan, point), ())),
);
origin_live_on_entry_var.extend(
origin_live_on_entry_rel
.iter()
.map(|&(origin, point)| ((origin, point), ())),
);

// subset(origin1, origin2, point) :-
// subset_base(origin1, origin2, point).
Expand Down Expand Up @@ -205,8 +187,8 @@ pub(super) fn compute<T: FactTypes>(
&subset_o1p,
(
cfg_edge_rel.extend_with(|&((_, point1), _)| point1),
origin_live_on_entry_rel.extend_with(|&((origin1, _), _)| origin1),
origin_live_on_entry_rel.extend_anti(|&((_, _), origin2)| origin2),
origin_live_on_entry.extend_with(|&((origin1, _), _)| origin1),
origin_live_on_entry.extend_anti(|&((_, _), origin2)| origin2),
),
|&((origin1, point1), origin2), &point2| ((origin2, point1, point2), origin1),
);
Expand All @@ -221,7 +203,7 @@ pub(super) fn compute<T: FactTypes>(
(
loan_killed_at.filter_anti(|&((_, point1), loan)| (loan, point1)),
cfg_edge_rel.extend_with(|&((_, point1), _)| point1),
origin_live_on_entry_rel.extend_anti(|&((origin, _), _)| origin),
origin_live_on_entry.extend_anti(|&((origin, _), _)| origin),
),
|&((origin, point1), loan), &point2| ((origin, point1, point2), loan),
);
Expand Down Expand Up @@ -259,7 +241,7 @@ pub(super) fn compute<T: FactTypes>(
// "intermediate" `origin2` is dead at `point2`.
dying_can_reach_1.from_antijoin(
&dying_can_reach_o2q,
&origin_live_on_entry_rel,
&origin_live_on_entry,
|&(origin2, point2), &(origin1, point1)| ((origin2, point1), (origin1, point2)),
);
dying_can_reach_o2q.from_join(
Expand All @@ -275,7 +257,7 @@ pub(super) fn compute<T: FactTypes>(
// origin_live_on_entry(origin2, point2).
dying_can_reach_live.from_join(
&dying_can_reach_o2q,
&origin_live_on_entry_var,
origin_live_on_entry,
|&(origin2, point2), &(origin1, point1), _| ((origin1, point1, point2), origin2),
);

Expand All @@ -291,8 +273,8 @@ pub(super) fn compute<T: FactTypes>(
&subset_o1p,
(
cfg_edge_rel.extend_with(|&((_, point1), _)| point1),
origin_live_on_entry_rel.extend_with(|&((origin1, _), _)| origin1),
origin_live_on_entry_rel.extend_with(|&((_, _), origin2)| origin2),
origin_live_on_entry.extend_with(|&((origin1, _), _)| origin1),
origin_live_on_entry.extend_with(|&((_, _), origin2)| origin2),
),
|&((origin1, _point1), origin2), &point2| ((origin1, point2), origin2),
);
Expand Down Expand Up @@ -331,7 +313,7 @@ pub(super) fn compute<T: FactTypes>(
(
loan_killed_at.filter_anti(|&((_, point1), loan)| (loan, point1)),
cfg_edge_rel.extend_with(|&((_, point1), _)| point1),
origin_live_on_entry_rel.extend_with(|&((origin, _), _)| origin),
origin_live_on_entry.extend_with(|&((origin, _), _)| origin),
),
|&((origin, _), loan), &point2| ((origin, point2), loan),
);
Expand All @@ -341,7 +323,7 @@ pub(super) fn compute<T: FactTypes>(
// !origin_live_on_entry(origin, point).
dead_borrow_region_can_reach_root.from_antijoin(
&loan_issued_at_op,
&origin_live_on_entry_rel,
&origin_live_on_entry,
|&(origin, point), &loan| ((origin, point), loan),
);

Expand All @@ -361,7 +343,7 @@ pub(super) fn compute<T: FactTypes>(
);
dead_borrow_region_can_reach_dead.from_antijoin(
&dead_borrow_region_can_reach_dead_1,
&origin_live_on_entry_rel,
&origin_live_on_entry,
|&(origin2, point), &loan| ((origin2, point), loan),
);

Expand All @@ -370,7 +352,7 @@ pub(super) fn compute<T: FactTypes>(
// origin_live_on_entry(origin, point).
loan_live_at.from_join(
&origin_contains_loan_on_entry_op,
&origin_live_on_entry_var,
origin_live_on_entry,
|&(_origin, point), &loan, _| ((loan, point), ()),
);

Expand All @@ -385,16 +367,16 @@ pub(super) fn compute<T: FactTypes>(
// joined together.
loan_live_at.from_join(
&dead_borrow_region_can_reach_dead_1,
&origin_live_on_entry_var,
origin_live_on_entry,
|&(_origin2, point), &loan, _| ((loan, point), ()),
);

// errors(loan, point) :-
// loan_invalidated_at(loan, point),
// loan_live_at(loan, point).
errors.from_join(
&loan_invalidated_at,
&loan_live_at,
loan_invalidated_at,
|&(loan, point), _, _| (loan, point),
);

Expand Down
39 changes: 7 additions & 32 deletions polonius-engine/src/output/naive.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ pub(super) fn compute<T: FactTypes>(

let (errors, subset_errors) = {
// Static inputs
let origin_live_on_entry_rel = &ctx.origin_live_on_entry;
let origin_live_on_entry = &ctx.origin_live_on_entry;
let cfg_edge = &ctx.cfg_edge;
let loan_killed_at = &ctx.loan_killed_at;
let known_placeholder_subset = &ctx.known_placeholder_subset;
Expand Down Expand Up @@ -57,33 +57,6 @@ pub(super) fn compute<T: FactTypes>(
let origin_contains_loan_on_entry_op =
iteration.variable_indistinct("origin_contains_loan_on_entry_op");

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

// output relations: illegal accesses errors, and illegal subset relations errors
let errors = iteration.variable("errors");
let subset_errors = iteration.variable::<(T::Origin, T::Origin, T::Point)>("subset_errors");
Expand Down Expand Up @@ -155,8 +128,8 @@ pub(super) fn compute<T: FactTypes>(
&subset,
(
cfg_edge.extend_with(|&(_origin1, _origin2, point1)| point1),
origin_live_on_entry_rel.extend_with(|&(origin1, _origin2, _point1)| origin1),
origin_live_on_entry_rel.extend_with(|&(_origin1, origin2, _point1)| origin2),
origin_live_on_entry.extend_with(|&(origin1, _origin2, _point1)| origin1),
origin_live_on_entry.extend_with(|&(_origin1, origin2, _point1)| origin2),
),
|&(origin1, origin2, _point1), &point2| (origin1, origin2, point2),
);
Expand Down Expand Up @@ -186,7 +159,7 @@ pub(super) fn compute<T: FactTypes>(
(
loan_killed_at.filter_anti(|&(_origin, loan, point1)| (loan, point1)),
cfg_edge.extend_with(|&(_origin, _loan, point1)| point1),
origin_live_on_entry_rel.extend_with(|&(origin, _loan, _point1)| origin),
origin_live_on_entry.extend_with(|&(origin, _loan, _point1)| origin),
),
|&(origin, loan, _point1), &point2| (origin, loan, point2),
);
Expand All @@ -197,9 +170,11 @@ pub(super) fn compute<T: FactTypes>(
// loan_live_at(Loan, Point) :-
// origin_contains_loan_on_entry(Origin, Loan, Point),
// origin_live_on_entry(Origin, Point).
//
// FIXME: Should be merged with Rule 8 so we can leapjoin.
loan_live_at.from_join(
&origin_contains_loan_on_entry_op,
&origin_live_on_entry_var,
origin_live_on_entry,
|&(_origin, point), &loan, _| ((loan, point), ()),
);

Expand Down