Stream: t-compiler/wg-polonius

Topic: subset errors rework


lqd (Aug 04 2020 at 11:08, on Zulip):

I'm working on pushing my prototypes computing subset errors:

nikomatsakis (Aug 04 2020 at 13:29, on Zulip):

this is great!

lqd (Aug 04 2020 at 13:31, on Zulip):

I'm close to finishing the 1st part (adding tests as we speak, which reminds me that we'd also need some more testing, refactoring tests, etc :)

lqd (Aug 04 2020 at 13:49, on Zulip):

alright here are the location-insensitive subset errors https://github.com/lqd/borrow-check/tree/subset_errors_are_back_with_a_vengeance

lqd (Aug 04 2020 at 13:52, on Zulip):

(I'll run rustc tests now, but wanted to publish it so you could take a look; there's a kind of hack I disliked but is no big deal: as we can call the location insensitive variant directly, and that normal subset errors are keyed by their location, when debugging I put them at the 0 point)

lqd (Aug 04 2020 at 13:53, on Zulip):

I like that it shows the placeholder loans neatness :) we add the contained loans, and just remove the locations from the rules

lqd (Aug 04 2020 at 13:54, on Zulip):

(in the naive variant, there are too many subsets we don't need to also push subset error computations down to the requires relation, while we don't maintain transitive subsets in the location-insensitive pass; also in the Naive variant placeholder loans come into conflict with our lack of coolness about things that are true at all points of the cfg)

nikomatsakis (Aug 04 2020 at 14:04, on Zulip):

let me take a look

lqd (Aug 04 2020 at 14:05, on Zulip):

it's very simple

nikomatsakis (Aug 04 2020 at 14:13, on Zulip):

so

nikomatsakis (Aug 04 2020 at 14:14, on Zulip):

this is still using the placeholder loan approach, right?

nikomatsakis (Aug 04 2020 at 14:14, on Zulip):

(just to make sure I understand what I'm reading)

nikomatsakis (Aug 04 2020 at 14:15, on Zulip):

I don't see any edits to the "naive" code, right?

nikomatsakis (Aug 04 2020 at 14:15, on Zulip):

I guess that it just kind of "falls out" because we're already saying 'only propagate those loans that might be involved in an error'?

nikomatsakis (Aug 04 2020 at 14:16, on Zulip):

lqd said:

I like that it shows the placeholder loans neatness :) we add the contained loans, and just remove the locations from the rules

to be clear, if you think placeholder loans work out nicer than the subset approach, I'm happy for us to keep using them :)

lqd (Aug 04 2020 at 14:17, on Zulip):

yes this is only part 1 of 3 of the list above, adding them to the location insensitive variant

lqd (Aug 04 2020 at 14:17, on Zulip):

using placeholder loans for now, but we can still change it later :)

lqd (Aug 04 2020 at 14:17, on Zulip):

which we can decide once more of the work is done on the opt and naive variant

nikomatsakis (Aug 04 2020 at 14:18, on Zulip):

yeah

nikomatsakis (Aug 04 2020 at 14:18, on Zulip):

I see the appeal

nikomatsakis (Aug 04 2020 at 14:18, on Zulip):

in particular I can imagine that it might be helpful because all the errors are then based on "loan propagation" only

lqd (Aug 04 2020 at 14:18, on Zulip):

specifically as of course it's a kind of duplication; maybe performance can be a deciding factor but it's currently hard to tell

nikomatsakis (Aug 04 2020 at 14:19, on Zulip):

yeah

nikomatsakis (Aug 04 2020 at 14:19, on Zulip):

I guess I think we should look to what makes the rules "feel" most elegant

nikomatsakis (Aug 04 2020 at 14:19, on Zulip):

because I suspect we may have to do horrible things to them in the name of performance anyway ;)

lqd (Aug 04 2020 at 14:19, on Zulip):

yeah :D

lqd (Aug 04 2020 at 17:33, on Zulip):

alright, part 2/3 is here with the last 5 commits of https://github.com/lqd/borrow-check/commits/subset_errors_are_back_with_a_vengeance

lqd (Aug 04 2020 at 17:34, on Zulip):

this adds the subset errors computation to the Opt variant, and would also show what it'd take to switch the Naive variant to using the subset-based rules

lqd (Aug 04 2020 at 17:35, on Zulip):

I definitely need to run rustc's tests of course but they should pass

lqd (Aug 04 2020 at 17:35, on Zulip):

and with that the Hybrid variant works again, so ♪ the opts are back in toooo-wn ♫

lqd (Aug 04 2020 at 19:34, on Zulip):

no apparent new failures on rustc's tests

lqd (Aug 04 2020 at 19:37, on Zulip):

the test run seemed faster as well, but it's still heavily dominated by move errors

lqd (Aug 04 2020 at 21:27, on Zulip):

and finally, part 3/3 if we decide it's cool, using subset-based rules in the naive variant https://github.com/lqd/borrow-check/commit/33a554ad8a6cead1a132ddb3dd747911247f3690 -- not particularly earth-shattering

lqd (Aug 04 2020 at 21:49, on Zulip):

(all in all it's cool that the location-insensitive variant can now be used again, but I do recall computing potential loan and subset errors on the condensation graph manually was like 20x on clap — that is, in absolute values, from 20ms to 1ms)

lqd (Aug 04 2020 at 23:07, on Zulip):

I forgot I could disable move errors to have an idea of the Hybrid variant duration on tests, looks like 10% if I remove the <10 current failures and tests behaving weirdly and that we have to analyze and fix (could be fact generation, or some of the computations I'm not sure)

lqd (Aug 05 2020 at 09:31, on Zulip):

for this I'll open PRs for the two branches above if you all like the changes

nikomatsakis (Aug 05 2020 at 13:39, on Zulip):

@lqd let me take a look..

lqd (Aug 05 2020 at 13:40, on Zulip):

sweet thank you, it’s not urgent or anything

lqd (Aug 05 2020 at 13:49, on Zulip):

I just wanted to check if polonius' profiling regions would show up inside rustc's profiling regions, they do, the top row is rustc image.png

lqd (Aug 05 2020 at 13:51, on Zulip):

(that being said, nagisa has made a tracy subscriber for tracing, and oli has/is in the process of making rustc use tracing instead of log)

nikomatsakis (Aug 05 2020 at 14:08, on Zulip):

@lqd looking at the naive rules first

nikomatsakis (Aug 05 2020 at 14:08, on Zulip):

it feels like they could get more naive

nikomatsakis (Aug 05 2020 at 14:08, on Zulip):

but maybe you structured it this way because of efficiency

nikomatsakis (Aug 05 2020 at 14:08, on Zulip):

or maybe I'm missing something

nikomatsakis (Aug 05 2020 at 14:08, on Zulip):

i.e., you have

nikomatsakis (Aug 05 2020 at 14:08, on Zulip):
subset_placeholder(O1, O2, N) :-
    subset(O1, O2, N),
    placeholder_region(O1).

and the transitive rule for that

nikomatsakis (Aug 05 2020 at 14:09, on Zulip):

but presumably we could just say that

subset_errors(O1, O2, N) :-
    subset(O1, O2, N),
    placeholder_region(O1),
    placeholder_region(O2),
    !known_subset(O1, O2)
nikomatsakis (Aug 05 2020 at 14:09, on Zulip):

right?

nikomatsakis (Aug 05 2020 at 14:10, on Zulip):

i.e., we don't really need the subset_placeholder rule

lqd (Aug 05 2020 at 14:10, on Zulip):

I think it was indeed one of the options we talked about but you came up with it in the post I think

lqd (Aug 05 2020 at 14:11, on Zulip):

that it was indeed for efficiency and the way to not be impacted by the heavy subset filtering in the Opt variant

nikomatsakis (Aug 05 2020 at 14:11, on Zulip):

the opt rules are a bit more complex

nikomatsakis (Aug 05 2020 at 14:11, on Zulip):

yeah, ok, in the opt rules we don't have the "transitive subset" to intersect with

lqd (Aug 05 2020 at 14:11, on Zulip):

right

lqd (Aug 05 2020 at 14:11, on Zulip):

we surely could use the simpler way for the Naive rules since we do have the subset TC here

lqd (Aug 05 2020 at 14:12, on Zulip):

I can do that

lqd (Aug 05 2020 at 14:13, on Zulip):

it simplifies the variant at the slight expense of having another way to compute erroneous subsets but it's not a big deal and no one will know since we haven't yet documented the Opt rules :)

nikomatsakis (Aug 05 2020 at 14:45, on Zulip):

sorry, got distracted by some other things --

nikomatsakis (Aug 05 2020 at 14:45, on Zulip):

but it seems like keeping the naive rules naive is a good thing

nikomatsakis (Aug 05 2020 at 14:46, on Zulip):

that said, i'm wondering about weaving in the LocationInsensitive stuff here

lqd (Aug 05 2020 at 14:46, on Zulip):

where ?

nikomatsakis (Aug 05 2020 at 14:46, on Zulip):

I think right now we are using that primarily to stop loans from propagating, is that right @lqd ?

nikomatsakis (Aug 05 2020 at 14:46, on Zulip):

oh, you had some more commits I think I maybe didn't read yet

lqd (Aug 05 2020 at 14:46, on Zulip):

this branch has subset errors in the 3 variants yeah

lqd (Aug 05 2020 at 14:47, on Zulip):

location-insensitive is the one we talked about a bit before, using placeholder loans

lqd (Aug 05 2020 at 14:47, on Zulip):

so that we could resurrect the Hybrid variant (variant-alooza)

lqd (Aug 05 2020 at 14:48, on Zulip):

to now finally be able to use the location-insensitive "potential errors" to filter origins and loans in the location sensitive analysis (Opt, in the most common case, but the same applies to the Naive variant if we wanted to)

lqd (Aug 05 2020 at 14:49, on Zulip):

so we'd use that both to stop loans from propagating, but prior to that, also limit which origins they should transitively propagate to

nikomatsakis (Aug 05 2020 at 14:50, on Zulip):

yeah but the main thing is

nikomatsakis (Aug 05 2020 at 14:50, on Zulip):

that if we are computing placeholder errors from the (transitive) subset

nikomatsakis (Aug 05 2020 at 14:51, on Zulip):

we still need to compute the transitive subset :P

nikomatsakis (Aug 05 2020 at 14:51, on Zulip):

sorry, let me phrase that another way

lqd (Aug 05 2020 at 14:51, on Zulip):

:)

nikomatsakis (Aug 05 2020 at 14:51, on Zulip):

I don't thikn we have ever had a variant of the naive analysis that tries to avoid computing parts of the subset relation, is that true?

lqd (Aug 05 2020 at 14:51, on Zulip):

yeah but Naive does that anyway

lqd (Aug 05 2020 at 14:51, on Zulip):

that is my recollection as well

lqd (Aug 05 2020 at 14:51, on Zulip):

apart from:

nikomatsakis (Aug 05 2020 at 14:52, on Zulip):

yeah and for opt we're saying "we compute the full transitive subset, but only starting from those placeholders that may be involved in errors"

nikomatsakis (Aug 05 2020 at 14:52, on Zulip):

(or you could imagine doing that, anyway)

nikomatsakis (Aug 05 2020 at 14:52, on Zulip):

( we could also just keep the naive/opt setup analogous )

lqd (Aug 05 2020 at 14:52, on Zulip):
lqd (Aug 05 2020 at 14:52, on Zulip):
lqd (Aug 05 2020 at 14:53, on Zulip):

for opt we're not really computing the full transitive subset

lqd (Aug 05 2020 at 14:53, on Zulip):

for Naive we do, and the quote would be exactly that

lqd (Aug 05 2020 at 14:54, on Zulip):

I guess I'm a bit lax

lqd (Aug 05 2020 at 14:54, on Zulip):

and handwaving too much which subsets we compute starting from placeholders

lqd (Aug 05 2020 at 14:55, on Zulip):

hopefully the essence of what I meant came through ...

nikomatsakis (Aug 05 2020 at 14:55, on Zulip):

ok. so basically I'm just thinking about a few things

nikomatsakis (Aug 05 2020 at 14:56, on Zulip):
lqd (Aug 05 2020 at 14:56, on Zulip):

having subset_placeholder may allow us to filter differently when we want to compute loan errors and subset errors

nikomatsakis (Aug 05 2020 at 14:56, on Zulip):

(i.e., we are already looking for loans that may be part of errors, and we restrict those from propagating)

nikomatsakis (Aug 05 2020 at 14:56, on Zulip):

essentially I guess I'm trying to think which formulation feels simpler overall

nikomatsakis (Aug 05 2020 at 14:56, on Zulip):

I think the appeal of the subset analysis for me was that, in the naive case at least, it was basically just adding one extra rule

lqd (Aug 05 2020 at 14:57, on Zulip):

what is a bit confusing is that we can still use the potential loan errors (not potential subset errors) from LocIns to filter loans

nikomatsakis (Aug 05 2020 at 14:57, on Zulip):

anyway I think all this code looks good and I am kind of happy with whichever approach ultimately

nikomatsakis (Aug 05 2020 at 14:57, on Zulip):

lqd said:

what is a bit confusing is that we can still use the potential loan errors (not potential subset errors) from LocIns to filter loans

I mean we want to do this, right?

lqd (Aug 05 2020 at 14:57, on Zulip):

sure

nikomatsakis (Aug 05 2020 at 14:57, on Zulip):

we probably want to do this in the opt variant, too

lqd (Aug 05 2020 at 14:57, on Zulip):

right right

nikomatsakis (Aug 05 2020 at 14:58, on Zulip):

I guess overall the opt variant feels like it'd be a bit simpler using a placeholder loans approach

lqd (Aug 05 2020 at 14:58, on Zulip):

yeah but it doesn't work as is there

nikomatsakis (Aug 05 2020 at 14:58, on Zulip):

why not?

lqd (Aug 05 2020 at 14:58, on Zulip):

there are too little subsets

nikomatsakis (Aug 05 2020 at 14:59, on Zulip):

I'm imagining that it would work like this:

nikomatsakis (Aug 05 2020 at 14:59, on Zulip):

this can propagate like any other loan through the subset relations

lqd (Aug 05 2020 at 14:59, on Zulip):

(just a sec let me look at the rules to make sure I'm not saying an incorrect thing on why it didn't work)

nikomatsakis (Aug 05 2020 at 14:59, on Zulip):

and then we have a error rule to say

nikomatsakis (Aug 05 2020 at 15:00, on Zulip):

(and we can filter that first rule down to loans that are potentially involved in errors)

lqd (Aug 05 2020 at 15:00, on Zulip):

what I recall was: we didn't have enough contains (requires) data for the placeholder loans approach

nikomatsakis (Aug 05 2020 at 15:01, on Zulip):

hmm

nikomatsakis (Aug 05 2020 at 15:01, on Zulip):

I have to remember

lqd (Aug 05 2020 at 15:01, on Zulip):

I'm not sure I debugged it to the point of knowing which data was missing and which rule filtered it

nikomatsakis (Aug 05 2020 at 15:01, on Zulip):

do we not compute the transitive contains in the opt variant either?

lqd (Aug 05 2020 at 15:01, on Zulip):

but it's easy enough to try

nikomatsakis (Aug 05 2020 at 15:01, on Zulip):

I thought we did

lqd (Aug 05 2020 at 15:01, on Zulip):

we do but it's heaviliy filtered down

lqd (Aug 05 2020 at 15:02, on Zulip):

we have less subsets, so we have less requires, was my recollection

lqd (Aug 05 2020 at 15:02, on Zulip):

the placeholder loans rules are super easy to copy paste if you want to try it in the opt variant

lqd (Aug 05 2020 at 15:03, on Zulip):

I can whip something up if you want ?

nikomatsakis (Aug 05 2020 at 15:03, on Zulip):

sure, I'm skimming the rules now

lqd (Aug 05 2020 at 15:04, on Zulip):

you do want me to do it you mean ?

lqd (Aug 05 2020 at 15:06, on Zulip):

(I remembered that since placeholders contained their loans at all points, loan propagation along the cfg created duplicates which needed to be deduped, for all rounds, at all cfg points, so it should be less efficient than the subset-based rules -- it's not important to this conversation, I just remembered this looking at it, but it's just our "X at all points are suboptimal")

lqd (Aug 05 2020 at 15:07, on Zulip):

I'm making Opt use placeholder loans rn

nikomatsakis (Aug 05 2020 at 15:12, on Zulip):

yeah, might as well try it

nikomatsakis (Aug 05 2020 at 15:15, on Zulip):

ok wait @lqd

nikomatsakis (Aug 05 2020 at 15:15, on Zulip):

so I think I see

nikomatsakis (Aug 05 2020 at 15:15, on Zulip):

I guess the opt variant is smarter than I remembered :)

lqd (Aug 05 2020 at 15:15, on Zulip):

it's a bit rushed but I have it

lqd (Aug 05 2020 at 15:15, on Zulip):

haha

nikomatsakis (Aug 05 2020 at 15:15, on Zulip):

in particular, it doesn't propagate loans indiscriminantly

nikomatsakis (Aug 05 2020 at 15:15, on Zulip):

i.e., it waits until an origin goes to dead

nikomatsakis (Aug 05 2020 at 15:15, on Zulip):

to propagate the loans from that origin to its successors

lqd (Aug 05 2020 at 15:16, on Zulip):

right !

nikomatsakis (Aug 05 2020 at 15:16, on Zulip):

so I can imagine that just adding the naive rules

nikomatsakis (Aug 05 2020 at 15:16, on Zulip):

is not going to work :)

lqd (Aug 05 2020 at 15:16, on Zulip):

that's what I was handwaving all along (jk)

nikomatsakis (Aug 05 2020 at 15:16, on Zulip):

this works out ok for the borrow rules beacuse

nikomatsakis (Aug 05 2020 at 15:16, on Zulip):

we don't care which origin contains a loan

lqd (Aug 05 2020 at 15:16, on Zulip):

if you want to try for some reason, here's a diff https://gist.github.com/lqd/1358b95bccb5e4c3672a61517bda471b

nikomatsakis (Aug 05 2020 at 15:16, on Zulip):

we only care that some live origin contains the loan

nikomatsakis (Aug 05 2020 at 15:16, on Zulip):

but for the subset errors, that's not true

nikomatsakis (Aug 05 2020 at 15:17, on Zulip):

so... ok... now I'm convinced that placeholder loans the wrong approach

lqd (Aug 05 2020 at 15:17, on Zulip):

:)

nikomatsakis (Aug 05 2020 at 15:17, on Zulip):

basically, the way that we use them is distinct

nikomatsakis (Aug 05 2020 at 15:17, on Zulip):

so it doesn't really help us to leverage the loan mechanism in the opt variant

nikomatsakis (Aug 05 2020 at 15:17, on Zulip):

and the naive variant is even simpler with the subset approach

lqd (Aug 05 2020 at 15:17, on Zulip):

but it looks good for the location-insensitive one

nikomatsakis (Aug 05 2020 at 15:18, on Zulip):

sure, but location insensitive can also be extended to use the origin-relations approach very easily, right?

lqd (Aug 05 2020 at 15:18, on Zulip):

sure

nikomatsakis (Aug 05 2020 at 15:18, on Zulip):

i.e., it computes the transitive subset relation but it just does it without considering the nodes

lqd (Aug 05 2020 at 15:18, on Zulip):

it's easy to do so but we might not want to maintain the subsets if we don't really need to

lqd (Aug 05 2020 at 15:18, on Zulip):

for the purity of rules this argument wouldn't matter of course

nikomatsakis (Aug 05 2020 at 15:19, on Zulip):

does it currently not compute the transitive subset relation at all?

nikomatsakis (Aug 05 2020 at 15:19, on Zulip):

location-insensitive, I mean

nikomatsakis (Aug 05 2020 at 15:19, on Zulip):

it just propagates loans?

nikomatsakis (Aug 05 2020 at 15:19, on Zulip):

I guess that makes sense

lqd (Aug 05 2020 at 15:19, on Zulip):

no

lqd (Aug 05 2020 at 15:19, on Zulip):

yup just loans

nikomatsakis (Aug 05 2020 at 15:19, on Zulip):

ok, so, what you're saying is:

nikomatsakis (Aug 05 2020 at 15:20, on Zulip):

we can keep the concept of placeholder origin with a paired placeholder loan

nikomatsakis (Aug 05 2020 at 15:20, on Zulip):

but only the location insensitive analysis uses the loan for anything

lqd (Aug 05 2020 at 15:20, on Zulip):

(which is why it was really fast and easy to make the location insensitive analyses as reachability queries on the condensation graph)

nikomatsakis (Aug 05 2020 at 15:20, on Zulip):

we could of course also have the insensitive analysis

lqd (Aug 05 2020 at 15:20, on Zulip):

for example yeah, but that's really not a big deal either way

nikomatsakis (Aug 05 2020 at 15:20, on Zulip):

propagate a distinct relation that is just for "outlived placeholder origins"

nikomatsakis (Aug 05 2020 at 15:21, on Zulip):

i.e., we'd have the "transitive loans contained in origin X" and the "transitive placeholder origins contained in origin X"

nikomatsakis (Aug 05 2020 at 15:21, on Zulip):

instead of just one set of tuples

nikomatsakis (Aug 05 2020 at 15:21, on Zulip):

that combines them both

lqd (Aug 05 2020 at 15:21, on Zulip):

both methods work here, I'm not sure if there's that much of an eficiency difference tbh

nikomatsakis (Aug 05 2020 at 15:21, on Zulip):

right, I imagine it's kind of "six in one, half a dozen in the other"

lqd (Aug 05 2020 at 15:21, on Zulip):

sure

lqd (Aug 05 2020 at 15:21, on Zulip):

:)

nikomatsakis (Aug 05 2020 at 15:21, on Zulip):

the only advantage I see is not having "placeholder loans" as a thing at all

nikomatsakis (Aug 05 2020 at 15:21, on Zulip):

at the cost of some duplication in the "location insensitive" rules

lqd (Aug 05 2020 at 15:21, on Zulip):

and the known contains relation that goes with them

nikomatsakis (Aug 05 2020 at 15:22, on Zulip):

well we still need a known_subset relation

lqd (Aug 05 2020 at 15:22, on Zulip):

sure

nikomatsakis (Aug 05 2020 at 15:22, on Zulip):

but yeah

lqd (Aug 05 2020 at 15:22, on Zulip):

as of now we have both

nikomatsakis (Aug 05 2020 at 15:22, on Zulip):

seems a bit better to me to just have "placeholder origins"

lqd (Aug 05 2020 at 15:22, on Zulip):

yesterday we only had known_contains

nikomatsakis (Aug 05 2020 at 15:22, on Zulip):

the location insensitive rules we'd be duplicating are very simple

lqd (Aug 05 2020 at 15:22, on Zulip):

very

nikomatsakis (Aug 05 2020 at 15:22, on Zulip):

and then the output is kind of the "loans involved in errors" and "placeholder origins involved in errors"

nikomatsakis (Aug 05 2020 at 15:23, on Zulip):

and we can filter things in a straightforward way using those

lqd (Aug 05 2020 at 15:23, on Zulip):

I honestly don't mind either way until we have proof that one is obviously better than the other

lqd (Aug 05 2020 at 15:23, on Zulip):

exactly

nikomatsakis (Aug 05 2020 at 15:23, on Zulip):

I'm convinced :)

nikomatsakis (Aug 05 2020 at 15:23, on Zulip):

it's not a major difference, I agree

lqd (Aug 05 2020 at 15:24, on Zulip):

it's not super easy to know how to filter the different relations depending on whether a potential error, or potential subset error, or both, involve a given loan / origin

lqd (Aug 05 2020 at 15:25, on Zulip):

on a slightly unrelated topic, because I'm finding "error" to lack precision, how would you call the loan analysis errors, compared to subset errors. "illegal access errors" ?

nikomatsakis (Aug 05 2020 at 15:29, on Zulip):

lqd said:

it's not super easy to know how to filter the different relations depending on whether a potential error, or potential subset error, or both, involve a given loan / origin

say more?

lqd (Aug 05 2020 at 15:29, on Zulip):

for example, if LocIns finds a single potential illegal access error we can eliminate all other borrow regions

lqd (Aug 05 2020 at 15:30, on Zulip):

we can also look at all origins which the introducing origin flows into

lqd (Aug 05 2020 at 15:30, on Zulip):

and remove the others

lqd (Aug 05 2020 at 15:31, on Zulip):

if now there's also a potential subset error, things are more complicated

lqd (Aug 05 2020 at 15:31, on Zulip):

we need to make sure that filtering the outlives constraints doesn't remove the path between the placeholders

lqd (Aug 05 2020 at 15:33, on Zulip):

maybe, just maybe, having the two different transitive subsets could help here, but I haven't looked into it

lqd (Aug 05 2020 at 15:35, on Zulip):

so I mostly meant that we had to be careful when making use of the results of the LocIns variant in the Naive or Opt variants (as part of the Hybrid context) to optimize possibly differently with these 2 kinds of potential errors

nikomatsakis (Aug 05 2020 at 15:36, on Zulip):

I see

nikomatsakis (Aug 05 2020 at 15:36, on Zulip):

lqd said:

we can also look at all origins which the introducing origin flows into

this is the part that interacts, right?

nikomatsakis (Aug 05 2020 at 15:36, on Zulip):

we can certainly compute two "parallel" subset relationships

lqd (Aug 05 2020 at 15:37, on Zulip):

yeah that's a key part, I'm not sure if it's the only part tho

lqd (Aug 05 2020 at 15:37, on Zulip):

absolutely

nikomatsakis (Aug 05 2020 at 15:37, on Zulip):

I was initially imagining that we would just filter the loans that get "introduced" into the contains (requires?) relationship

nikomatsakis (Aug 05 2020 at 15:37, on Zulip):

that's easy

lqd (Aug 05 2020 at 15:37, on Zulip):

the relations should be heavility filtered anyway so having both relationships if need be wouldn't matter much

nikomatsakis (Aug 05 2020 at 15:37, on Zulip):

I guess I'm imagining that we can have a relation like contains, but call it contains_placeholder(origin1, origin2, node)

nikomatsakis (Aug 05 2020 at 15:38, on Zulip):

this is probably subset_placeholder but I think using a distinct name is maybe less confusing? unclera :)

nikomatsakis (Aug 05 2020 at 15:38, on Zulip):

perhaps more confusing actually, I take it back

nikomatsakis (Aug 05 2020 at 15:38, on Zulip):

anyway the point is that it would be built using subset_base only

lqd (Aug 05 2020 at 15:38, on Zulip):

for potential loan errors we can indeed filter requires that's immediate

lqd (Aug 05 2020 at 15:38, on Zulip):

but we don't have to do the TC on "useless origins"

nikomatsakis (Aug 05 2020 at 15:38, on Zulip):

(does that work...that might require a lot of duplication I guess for the logic that moves it between nodes)

lqd (Aug 05 2020 at 15:39, on Zulip):

and can filter subsets as well via filtering outlives

nikomatsakis (Aug 05 2020 at 15:39, on Zulip):

yeah so at least in the opt variant, I was imagining that we would (a) control which loans we introduce and (b) only compute the subset_placeholder if the placeholder origin is known to be part of a potential error

lqd (Aug 05 2020 at 15:40, on Zulip):

agreed

nikomatsakis (Aug 05 2020 at 15:40, on Zulip):

but if we are going to restrict the subset relation itself

lqd (Aug 05 2020 at 15:40, on Zulip):

it seems elegant and straightforward

nikomatsakis (Aug 05 2020 at 15:40, on Zulip):

I guess I'm not sure that's worth the effort :)

nikomatsakis (Aug 05 2020 at 15:40, on Zulip):

in the naive variant, presumably, it could be

lqd (Aug 05 2020 at 15:40, on Zulip):

we don't have to for opt yeah

lqd (Aug 05 2020 at 15:40, on Zulip):

for naive it's trivial, easy and effective

nikomatsakis (Aug 05 2020 at 15:41, on Zulip):

well, it's easy, but then it potentially eliminates errors,

lqd (Aug 05 2020 at 15:41, on Zulip):

(at least on clap :)

nikomatsakis (Aug 05 2020 at 15:41, on Zulip):

butI guess the answer is that we can include all origins that may be involved in subset errors too?

nikomatsakis (Aug 05 2020 at 15:41, on Zulip):

(can we compute that readily enough?)

lqd (Aug 05 2020 at 15:41, on Zulip):

yup

lqd (Aug 05 2020 at 15:41, on Zulip):

I did that once

lqd (Aug 05 2020 at 15:42, on Zulip):

and turns out it prevents most filtering unfortunately on clap ;)

lqd (Aug 05 2020 at 15:42, on Zulip):

oh well

nikomatsakis (Aug 05 2020 at 15:42, on Zulip):

so basically we have:

nikomatsakis (Aug 05 2020 at 15:42, on Zulip):

lqd said:

and turns out it prevents most filtering unfortunately on clap ;)

wait, what?

lqd (Aug 05 2020 at 15:42, on Zulip):

it's just the shape of the clap dataset I think

nikomatsakis (Aug 05 2020 at 15:43, on Zulip):

that confuses me

lqd (Aug 05 2020 at 15:43, on Zulip):

sorry:

nikomatsakis (Aug 05 2020 at 15:43, on Zulip):

are you saying that, in clap at least, there are a lot of potential errors?

lqd (Aug 05 2020 at 15:43, on Zulip):

though to be fair I hadn't limited it only to placeholder only involved in potential subset errors

nikomatsakis (Aug 05 2020 at 15:43, on Zulip):

and so the filtering isn't that effective

nikomatsakis (Aug 05 2020 at 15:43, on Zulip):

ah

lqd (Aug 05 2020 at 15:43, on Zulip):

sorry I'm confusing you

nikomatsakis (Aug 05 2020 at 15:44, on Zulip):

you were saying you limited it to "anything derived from a placeholder"

lqd (Aug 05 2020 at 15:44, on Zulip):

there are no potential subset errors in clap

lqd (Aug 05 2020 at 15:44, on Zulip):

yes

nikomatsakis (Aug 05 2020 at 15:44, on Zulip):

ok ok

nikomatsakis (Aug 05 2020 at 15:44, on Zulip):

I can understand that

lqd (Aug 05 2020 at 15:44, on Zulip):

sorry I had forgotten that key point

nikomatsakis (Aug 05 2020 at 15:44, on Zulip):

that does seem imp't

lqd (Aug 05 2020 at 15:44, on Zulip):

turns out something in clap flows into a placeholder and limits filtering

lqd (Aug 05 2020 at 15:44, on Zulip):

it has a weird shape actually, like 2 huge SCCs or something

nikomatsakis (Aug 05 2020 at 15:44, on Zulip):

I see, yes, that sounds quite plausible

nikomatsakis (Aug 05 2020 at 15:45, on Zulip):

but I think we can limit to cases that may involve errors

nikomatsakis (Aug 05 2020 at 15:45, on Zulip):

and that is probably a big difference

lqd (Aug 05 2020 at 15:45, on Zulip):

right

lqd (Aug 05 2020 at 15:45, on Zulip):

it absolutely was on illegal access errors so I presume it will on subset errors as well

lqd (Aug 05 2020 at 15:45, on Zulip):

especially since subset errors are, I believe, heavier to compute than the others

lqd (Aug 05 2020 at 15:46, on Zulip):

but maybe clap skewed my view

lqd (Aug 05 2020 at 15:46, on Zulip):

illegal access errors traversals are numerous but shallow in the subset graph, subset errors traversals are few but traverse deeper

lqd (Aug 05 2020 at 15:53, on Zulip):

(or subset multigraph since we don't really link 'static to regular origins -- or hypergraph with outlives as hyperedges between the cfg points, I'm still unsure how to describe it)

lqd (Aug 05 2020 at 15:54, on Zulip):

(that also makes it hard to find papers in the literature to solve our problems for us)

lqd (Aug 05 2020 at 15:59, on Zulip):

transitive closures of dynamic graphs don't really work as is, worst case optimal joins on k^n trees either (though they have a nice data structure I wish I could use because of the naming resemblance: lqdags :)

nikomatsakis (Aug 05 2020 at 16:15, on Zulip):

heh

nikomatsakis (Aug 05 2020 at 16:16, on Zulip):

ok, well, we should try to document some of the plans from this thread into the hackmd

nikomatsakis (Aug 05 2020 at 16:16, on Zulip):

I have to run and grab some lunch but will do

lqd (Aug 05 2020 at 16:20, on Zulip):

great, thank you

lqd (Aug 05 2020 at 16:20, on Zulip):

I’ll turn the naive rules more naive soon-ish

lqd (Aug 05 2020 at 16:21, on Zulip):

and document them in the hackmd, before opening the PR, maybe add them to the book as well now that is think about it

lqd (Aug 05 2020 at 16:21, on Zulip):

enjoy your meal, bon appétit

nikomatsakis (Aug 05 2020 at 19:09, on Zulip):

@lqd took me a while but I'm adding stuff to https://github.com/rust-lang/polonius/issues/153

nikomatsakis (Aug 05 2020 at 19:09, on Zulip):

I may get some of the details wrong, please double check =)

lqd (Aug 05 2020 at 19:43, on Zulip):

Will do :) thanks for doing that

lqd (Aug 05 2020 at 23:21, on Zulip):

that's a great summary

Last update: Jun 20 2021 at 00:00UTC