Add a helper function for "passthrough" leapers

[ecstatic-morse]

See https://github.com/rust-lang/polonius/pull/178#issuecomment-901315380 for background. This is a simple way to combine rules 7 and 8 of the naive analysis. I haven't audited the other rulesets to see where it could be used.

Frankly, this seems a little too cute to me. The fact that you need this esoteric thing to avoid a runtime panic is not good API design. At the very least, we should try to make the "no proposers" case panic at compile-time, but that's easier said than done.

r? @lqd

[lqd]

Sweet, thanks a bunch! That'll allow to shave off a few percents from the naive and opt variants.

(although now that I think about it, maybe some care will be needed for that: it's likely that consumers of polonius are looking at the resulting origin_contains_loan_on_entry facts in verbose mode. rustc doesn't)

Do you want to add tests to show that this indeed works around the WF-ness issue (we both know it does) ?

Either way, r=me.

For reference, this is how combining rules 7 and 8 would look in polonius with this PR (without depending on the other PR about the empty re-indexing):

// errors(Loan, Point) :-
//    origin_contains_loan_on_entry(Origin, Loan, Point),
//    loan_invalidated_at(Loan, Point),
//    origin_live_on_entry(Origin, Point).
errors.from_leapjoin(
    &origin_contains_loan_on_entry,
    (
        datafrog::passthrough(),
        origin_live_on_entry_rel.filter_with(|&(origin, _loan, point)| (origin, point)),
        loan_invalidated_at.filter_with(|&(_origin, loan, point)| ((loan, point), ())),
    ),
    |&(_origin, loan, point), ()| (loan, point),
  );

[ecstatic-morse]

(although now that I think about it, maybe some care will be needed for that: it's likely that consumers of polonius are looking at the resulting origin_contains_loan_on_entry facts in verbose mode. rustc doesn't)

You mean loan_live_at, right? Yeah, that seems like it might be useful. It's more important to eliminate limitations in datafrog than to actually merge the rules.

I still feel like it would be better to have a leapfilter function for this kind of thing, rather than doing a "fake join" so-to-speak. It's probably fine for now, though. I'll add a test.

[lqd]

@vakaras could tell us which of the two, if any, prusti uses, but we emit the data for both these relations in verbose mode.

Agreed, we could indeed have a different leapjoin function for this case, it would be cleaner API for datafrog users.

[nikomatsakis]

Merging -- looks useful and we can tune later.

[vakaras]

@vakaras could tell us which of the two, if any, prusti uses, but we emit the data for both these relations in verbose mode.

Agreed, we could indeed have a different leapjoin function for this case, it would be cleaner API for datafrog users.

@lqd Thanks for the heads-up! Prusti uses loan_live_at to figure out which loans are alive at which program points. We are not using origin_contains_loan_on_entry.