I also have some more general questions about polonius:
borrow_live_atrelation considered 'bug-free' ? I have some examples that have surprising results.
Loanin the polonius sense always has exactly one owner at any point it is alive? (anything else wouldn't really make sense tbh)
borrow_live_at it's a bit subtle, first of all the relation is not completely, strictly speaking, needed to be materialized. The computation's goal is to find different types of errors, and those don't require computing the full contents of origins at all points of the CFG: as an oversimplified example, illegal access errors can only happen for invalidated loans, therefore, tracking the others is not needed since they can't produce errors.
Similarly, illegal subset errors can only happen on placeholder loans (which are to be phased out anyways, but it's just to illustrate my point) -- and earlier in the pipeline, before doing the full location-sensitive analysis, there's a location-insensitive pre-pass which first checks (and filters out (WIP)) the loans to limit the full pass to those possibly error-producing loans (origins will in the future be similarly filtered at this point, if they don't participate in subset or illegal access errors, there's no need to compute their contents), and in this case, the relation wouldn't be computed at all.
It used to be considered bug-free by itself, but it's not used by itself anymore: it's at the end of the pipeline, after move/init analysis whose correctness and equivalence with rustc has not been validated yet (and there have been false positives before, and there may still be) @Albin Stjerna is working on this specific part and would know more than I do
all these can make for surprising results :)
for the other question I guess it depends on what you mean by "owner": if you mean origin then not really, a loan can flow into placeholder origins (AKA universal region / free region) which are live at all points
By owner I mean a
Variable, though that may not even make sense in the context of polonius.
Thanks for the explanation about
borrow_live_at, though it's also disappointing for my purpose. I guess I'll need to reimplement a version of polonius if I want to get the liveness of borrows at all points in the CFG. Though I'm really only interested in the points loans die at.
In short I'm hoping to use polonius to identify when borrows die, and which variable was holding the borrow when it died. The second part I should be able to calculate by considering moves in the MIR graph, but for the first bit I need polonius to tell me which borrows are alive at each point.
As far as I can tell the information returned from
borrow_live_at works for me, though there are some surprising results, they don't seem lead me to do anything unsound. I hope that access to this relation stays as polonius evolves!
for the foreseeable future (as you can see there's not a lot of activity ATM) you should be able to only use the parts of the pipeline you need: liveness -> move/init analysis (with the caveat I've mentioned earlier) ->
Naive variant (bypassing the LocationInsensitive, and Optimized variants, the latter of which only computes the subset TC and contained loans on some of the origins dying at edges, etc)
yep I currently only use the naive version, I'm definitely not as performance sensitive as rustc is
For a surprising result, I found it surprising that a loan could die in one branch of an if statement but be alive at the end
I believe that access to the relation will be available in some form or another, especially if the datalog computation is used for validation rather than production (for performance reasons, say), especially in the Naive variant; as it's at the very least useful for debugging and testing and so on
effectively that a program execution could follow a path where a loan disappears from the live set and re-enters later
at the end, meaning after the branch ? this sounds like an expected case but maybe I'm misunderstanding
(say, since the points following the branch have to expect either branch could have been taken, and expect the union of results)
yea I guess I expected the loan to be counted as alive in a branch where it wasn't used since it would be used again in the future
again, this behavior doesn't cause problems for me, it's just surprising
since if a loan is dead in any branch it can't actually be used afterwards (if my intuition is correct) all it can do is die after the branches merge
(the datafrog_opt variant could be useful for you to look at dying origins and similar, it should have the points you need)
I actually don't need anything about origins (which are lifetimes / regions, right?)
yea they only matter for meta theory in my case
I guess it depends whether you consider loans to have liveness per se, is what I mean, they're live if they're contained in an origin live at a point
so the points where they die mixes both containment and origin liveness
but yeah, you know better than me what you actually need of course :)
ah hm, ok. I've pretty much ignored the
origin_live_on_entry relation sine
borrow_live_at seemed to be exactly what I needed. I hadn't considered that a loan could be in
borrow_live_at after its origin had died
ahh the theory to implementation gap :P
loans can indeed flow from origin to origin even if they're dead or dying (that's what the opt variant tries to ensure)
ok, printing region liveness in my debug viewer definitely helps understand this
thanks for the help I think I understand how to correctly find where loans die now :P
(and as you've seen origins can surprisingly "resurrect" )
mais, de rien :) :baguette:
the naive version computes strictly larger relations than the opt version, correct? ie im not missing out on tuples by using the naive version?
(to sum up, loans flow from origin to origin along the CFG regardless of liveness, the only thing that can stop a loan from flowing is a kill point)