search

rust-lang / polonius

Defines the Rust borrow checker.
Apache License 2.0
1.31k stars 74 forks source link

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

Open ecstatic-morse opened 3 years ago

ecstatic-morse commented 3 years ago

Depends on rust-lang/datafrog#36.

Removes some indexes, which should help memory usage by a small amount and makes things easier to read.

lqd commented 3 years ago

The reason why rules 7 and 8 can't be merged yet is another interesting datafrog limitation that could be of interest to you :) It's about leapjoins' well-formedness and there are details in the comment about why we used to need both relation and variable versions of the liveness facts.

lqd commented 3 years ago

Apart from the above point (which we could keep as a comment for the time being, and fix some day in the future): needless to say this looks good to me once we have a datafrog release with the required PR.

ecstatic-morse commented 3 years ago

The reason why rules 7 and 8 can't be merged yet is another interesting datafrog limitation that could be of interest to you :) It's about leapjoins' well-formedness and there are details in the comment about why we used to need both relation and variable versions of the liveness facts.

Hmm, looking at this again, it seems like it's more of an indexing issue? origin_live_on_entry and loan_invalidated_at are both relations, but they don't have a shared key or something?

In any case, I'll just remove the FIXME from this PR. It was more of a note-to-self.

lqd commented 3 years ago

Merging rules 7 and 8 would be something like

errors(Loan, Point) :-
    loan_invalidated_at(Loan, Point),
    origin_contains_loan_on_entry(Origin, Loan, Point),
    origin_live_on_entry(Origin, Point).

If this were implemented as filter leapers on origin_contains_loan_on_entry it would be a leapjoin that is not well-formed: IIRC what Frank said (and I don't think it's documented anywhere ?), leapjoins' WF-ness currently requires at least one extend leaper.

This criterion manifests as runtime errors rather than compile-time errors: IIRC related to the MIN/MAX sentinel indices in the leapjoins, like an assertion that at least one leaper returned a valid index. I think the errors can be triggered on some of the in-repo input tests, with the two rules merged; at least they used to when we tried this 3y ago. And there are some discussions with Frank about this on Zulip where he mentioned a way to fix it in datafrog (it was some kind of passthrough leaper just for that purpose). I can find these discussions if you want.

ecstatic-morse commented 3 years ago

No need to dig through the chat logs. That's pretty clear to me. I've always been a bit confused by the difference between "extend" and "filter" (though more the "anti" variants). "extend" is for when you have terms in the leaper that are not bound by the Variable, correct? That's not the case here, since origin_contains_loan_on_entry has everything already.

lqd commented 3 years ago

Exactly. There's a bit more info in the leapjoin part of Frank's initial post about datafrog, and maybe we should incorporate more of that into the docs ?

(To clarify what I meant: digging through the logs would be to find the proposed fix :)