Stream: t-compiler/wg-polonius

Topic: polonius questions


Xavier Denis (Oct 28 2020 at 16:39, on Zulip):

I also have some more general questions about polonius:

lqd (Oct 28 2020 at 17:37, on Zulip):

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

lqd (Oct 28 2020 at 17:38, on Zulip):

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.

lqd (Oct 28 2020 at 17:38, on Zulip):

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

lqd (Oct 28 2020 at 17:39, on Zulip):

all these can make for surprising results :)

lqd (Oct 28 2020 at 17:42, on Zulip):

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

Xavier Denis (Oct 28 2020 at 18:16, on Zulip):

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.

Xavier Denis (Oct 28 2020 at 18:22, on Zulip):

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!

lqd (Oct 28 2020 at 18:24, on Zulip):

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)

Xavier Denis (Oct 28 2020 at 18:24, on Zulip):

yep I currently only use the naive version, I'm definitely not as performance sensitive as rustc is

Xavier Denis (Oct 28 2020 at 18:25, on Zulip):

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

lqd (Oct 28 2020 at 18:26, on Zulip):

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

Xavier Denis (Oct 28 2020 at 18:26, on Zulip):

effectively that a program execution could follow a path where a loan disappears from the live set and re-enters later

lqd (Oct 28 2020 at 18:32, on Zulip):

at the end, meaning after the branch ? this sounds like an expected case but maybe I'm misunderstanding

lqd (Oct 28 2020 at 18:33, on Zulip):

(say, since the points following the branch have to expect either branch could have been taken, and expect the union of results)

Xavier Denis (Oct 28 2020 at 18:34, on Zulip):

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

Xavier Denis (Oct 28 2020 at 18:35, on Zulip):

again, this behavior doesn't cause problems for me, it's just surprising

lqd (Oct 28 2020 at 18:35, on Zulip):

sure :)

Xavier Denis (Oct 28 2020 at 18:36, on Zulip):

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

lqd (Oct 28 2020 at 18:36, on Zulip):

(the datafrog_opt variant could be useful for you to look at dying origins and similar, it should have the points you need)

Xavier Denis (Oct 28 2020 at 18:36, on Zulip):

I actually don't need anything about origins (which are lifetimes / regions, right?)

lqd (Oct 28 2020 at 18:37, on Zulip):

yeah

Xavier Denis (Oct 28 2020 at 18:37, on Zulip):

yea they only matter for meta theory in my case

lqd (Oct 28 2020 at 18:37, on Zulip):

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

lqd (Oct 28 2020 at 18:38, on Zulip):

so the points where they die mixes both containment and origin liveness

lqd (Oct 28 2020 at 18:38, on Zulip):

but yeah, you know better than me what you actually need of course :)

Xavier Denis (Oct 28 2020 at 18:41, on Zulip):

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

Xavier Denis (Oct 28 2020 at 18:43, on Zulip):

ahh the theory to implementation gap :P

lqd (Oct 28 2020 at 18:45, on Zulip):

loans can indeed flow from origin to origin even if they're dead or dying (that's what the opt variant tries to ensure)

Xavier Denis (Oct 28 2020 at 18:48, on Zulip):

ok, printing region liveness in my debug viewer definitely helps understand this

Xavier Denis (Oct 28 2020 at 18:48, on Zulip):

thanks for the help I think I understand how to correctly find where loans die now :P

lqd (Oct 28 2020 at 18:48, on Zulip):

(and as you've seen origins can surprisingly "resurrect" )

lqd (Oct 28 2020 at 18:48, on Zulip):

mais, de rien :) :baguette:

Xavier Denis (Oct 28 2020 at 18:48, on Zulip):

yep!

Xavier Denis (Oct 28 2020 at 18:56, on Zulip):

the naive version computes strictly larger relations than the opt version, correct? ie im not missing out on tuples by using the naive version?

lqd (Oct 28 2020 at 18:56, on Zulip):

right

lqd (Oct 28 2020 at 18:57, on Zulip):

(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)

Xavier Denis (Oct 28 2020 at 18:58, on Zulip):

yep, merci!

lqd (Oct 28 2020 at 18:58, on Zulip):

haha

Last update: Jun 19 2021 at 23:45UTC