Add a helper function for "passthrough" leapers

[ecstatic-morse]

See rust-lang/polonius#178 (comment) 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]

do you think we need a panic or an assertion here to notify users about that ?

[ecstatic-morse]

An assertion here will almost never trigger, even on programs that violate the rule in the parentheses. This leaper has a count of 1, and we always use the leaper with the lowest count to propose values. We return early (skipping propose and intersect) when the count is 0, so we only enter this function when:
- There's another leaper that proposes exactly one value.
- That leaper appears before us in the Leapers tuple (to break the tie).

Since it's not a hard error, just a small inefficiency, I think omitting it is fine. WDYT?

[lqd]

Agreed. Thanks for the clarifications, I had missed this context. It doesn't look like an assertion would be useful in this situation indeed.

[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.