Stream: t-compiler/wg-polonius

Topic: equality variant vs polonius-as-is


lqd (Aug 03 2020 at 14:43, on Zulip):

this one is important with respect to users

nikomatsakis (Aug 03 2020 at 14:43, on Zulip):

(side note that it feels like it wants to use union-set in the ultimate impl...)

lqd (Aug 03 2020 at 16:13, on Zulip):

I had this old implementation of the equality rules https://github.com/lqd/borrow-check/tree/variant_prototype2 which was my last look at the rules. I remember I had to add another TC of the equality tuples compared to just propagating them as mentioned on the issue, as they were missing an error in one of our examples. I rambled the analysis and fix, in this other topic starting here which ends with the rustc test cases with unexpected results: 2 cases which shouldn't be compiling but do so with the prototype

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

OK

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

let me try to catch up here, I feel like this is the most interesting unknown at present, right?

nikomatsakis (Aug 03 2020 at 16:17, on Zulip):

(not sure btw if you following along with what @Albin Stjerna and I were saying in #t-compiler/wg-polonius > move error reporting, it looks like we could speed that up somewhat while also getting the error reporting that rustc wants...)

lqd (Aug 03 2020 at 16:19, on Zulip):

(I was not entirely following but that's great to hear !)

lqd (Aug 03 2020 at 16:19, on Zulip):

it feels like a very interesting unknown indeed

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

and one that at least you wouldn't "waste" your precious little time on updating hackmd rules that I can do in the meantime :)

nikomatsakis (Aug 03 2020 at 16:23, on Zulip):

I'm looking at the two test cases you cited in the "ramble"

lqd (Aug 03 2020 at 16:25, on Zulip):

:) rambling-as-a-service

nikomatsakis (Aug 03 2020 at 16:30, on Zulip):

So I want to try and reproduce this case: https://github.com/rust-lang/rust/blob/master/src/test/ui/nll/promoted-bounds.rs

nikomatsakis (Aug 03 2020 at 16:32, on Zulip):

off the top of my head, I can't see why it would not get an error. I expect that we would force c to be {Lb, La} (where those are loans from &l and &5 repsectively)

nikomatsakis (Aug 03 2020 at 16:32, on Zulip):

and hence we should get an error when we leave the scope of {...} that block because of some statement like STORAGE_DEAD(l)

nikomatsakis (Aug 03 2020 at 16:33, on Zulip):

in order for me to do that, @lqd, do I have to build a rustc that links against your branch? Or can I just generate the facts I guess?

lqd (Aug 03 2020 at 16:34, on Zulip):

oh sorry I don't remember if I had pushed it, let me check (I tend not to do so)

lqd (Aug 03 2020 at 16:35, on Zulip):

(since it's an old polonius branch, generating new facts wouldn't work either, after the relations have been renamed and so on)

nikomatsakis (Aug 03 2020 at 16:35, on Zulip):

ok, maybe a worthwhile experiment would be to try and "rebase"

lqd (Aug 03 2020 at 16:36, on Zulip):

but I think your dedicated half day for the sprint is close to ending ?

lqd (Aug 03 2020 at 16:36, on Zulip):

if so, I can prepare both the rustc branch and polonius rebased prototype later today

nikomatsakis (Aug 03 2020 at 16:37, on Zulip):

yeah, I've got to go, I've got a bit more time -- I might pop back in later and do a few more things, not sure yet

nikomatsakis (Aug 03 2020 at 16:37, on Zulip):

if nothing else though I have to attend the lang-team meeting in a few hours :)

lqd (Aug 03 2020 at 16:42, on Zulip):

alright I will start preparing these 2

lqd (Aug 03 2020 at 16:43, on Zulip):

it's more important / useful than the OOM fixes, and we can talk a bit about those later in the sprint

nikomatsakis (Aug 03 2020 at 17:16, on Zulip):

I agree, this is probably the biggest unknown

lqd (Aug 03 2020 at 19:48, on Zulip):

@nikomatsakis alright I've finished rebasing and adding subset errors to the prototype https://github.com/lqd/borrow-check/tree/variant_prototype3

lqd (Aug 03 2020 at 19:50, on Zulip):

did you want to run rustc's tests with it or just the one example from earlier ? if it's the former I can push a rustc branch to make it easier to test

lqd (Aug 03 2020 at 19:50, on Zulip):

otherwise any recent nightly's facts would work

lqd (Aug 03 2020 at 20:07, on Zulip):

here is the rustc branch for easy testing if need be https://github.com/lqd/rust/tree/equality_prototype

nikomatsakis (Aug 03 2020 at 20:21, on Zulip):

ooh, nice

lqd (Aug 03 2020 at 20:26, on Zulip):

most of the variant was generated by datapond so its definitely, absolutely, not at all efficient. For example, equal origins are still present in subsets which will take some deduping at the end of each round, and so on, but that shouldn't matter for our tests at least

lqd (Aug 03 2020 at 20:31, on Zulip):

output on promoted-bounds:

$ cargo run -q -- ./inputs/promoted-bounds/nll-facts/main/ --show-tuples -a naive && cargo run -q -- ./inputs/promoted-bounds/nll-facts/main/ --show-tuples -a prototype
--------------------------------------------------
Directory: ./inputs/promoted-bounds/nll-facts/main/
Time: 0.061s
# errors
errors "Start(bb2[7])" "bw0"
# move_errors
# subset_errors
--------------------------------------------------
Directory: ./inputs/promoted-bounds/nll-facts/main/
Time: 0.064s
# errors
# move_errors
# subset_errors
nikomatsakis (Aug 03 2020 at 22:36, on Zulip):

you didn't check in the promoted-bounds inputs, right?

nikomatsakis (Aug 03 2020 at 22:36, on Zulip):

I don't see them, anyway

lqd (Aug 03 2020 at 22:36, on Zulip):

no but I can do so

lqd (Aug 03 2020 at 22:36, on Zulip):

just a sec

nikomatsakis (Aug 03 2020 at 22:38, on Zulip):

it's ok, I generated them

nikomatsakis (Aug 03 2020 at 22:38, on Zulip):

I see the output now

lqd (Aug 03 2020 at 22:40, on Zulip):

ah ok

lqd (Aug 03 2020 at 22:40, on Zulip):

I was just about to push

nikomatsakis (Aug 03 2020 at 22:59, on Zulip):

I'm trying to remember what kind of debug output there is

nikomatsakis (Aug 03 2020 at 22:59, on Zulip):

e.g., I guess I can't readily get a graphviz of the cfg?

lqd (Aug 03 2020 at 23:00, on Zulip):

you can IIRC

lqd (Aug 03 2020 at 23:01, on Zulip):

probably --graphviz-file somefile.dot

lqd (Aug 03 2020 at 23:01, on Zulip):

it will have some facts so it's not just the cfg

nikomatsakis (Aug 03 2020 at 23:04, on Zulip):

yeah

nikomatsakis (Aug 03 2020 at 23:04, on Zulip):

useful maybe

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

they can easily be removed to just leave the cfg IIRC

lqd (Aug 03 2020 at 23:11, on Zulip):

(last time I rambled while debugging I also had to add the equality tuples to the graphviz output)

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

@lqd I realize I might be a bit confused -- the promoted-boudns test. With naive, at least, it generates an error--- like it's supposed to, right?

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

oh, I have to run with Prototype...

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

right :)

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

that part of the command line was scrolled out on my earlier output

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

ok, so, digging a bit ...

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

at bb0[22]

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

we have _8 = move _9(move _10, move _11) -> [return: bb2, unwind: bb1];

nikomatsakis (Aug 04 2020 at 01:05, on Zulip):
    let _8: &'_#70r i32;
    let mut _9: fn(&'_#71r i32, &'_#72r i32) -> &'_#73r i32 {shorten_lifetime::<'_#71r, '_#72r, '_#73r>}; // in scope 0 at promoted-bounds.rs:20:17: 20:37
    let mut _10: &'_#74r i32;            // in scope 0 at promoted-bounds.rs:20:38: 20:39
    let mut _11: &'_#75r i32;            // in scope 0 at promoted-bounds.rs:20:41: 20:42
nikomatsakis (Aug 04 2020 at 01:05, on Zulip):

but

nikomatsakis (Aug 04 2020 at 01:05, on Zulip):
outlives("\'_#73r", "\'_#70r", _)
outlives("\'_#74r", "\'_#71r", _)
outlives("\'_#75r", "\'_#72r", _)
nikomatsakis (Aug 04 2020 at 01:06, on Zulip):

there seems to be missing a relationship between 71, 72, and 73

nikomatsakis (Aug 04 2020 at 01:06, on Zulip):

that would've been established by the where clauses on _9

nikomatsakis (Aug 04 2020 at 01:06, on Zulip):

i.e., for the type to be well-formed

nikomatsakis (Aug 04 2020 at 01:07, on Zulip):

I'm not 100% sure where that would be checked

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

that's very interesting

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

both that it can show a problem in fact generation, and that the Naive variant is able to overcome it :thinking:

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

ah if you use a direct call, the prototype variant does indeed find the error

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

I think NLLs would work similarly on this relationship, that is 71 <: 73, 72 <: 73 follow via _31 (let mut _31: &'_#104r fn(&'_#105r i32, &'_#106r i32) -> &'_#107r i32 {shorten_lifetime::<'_#105r, '_#106r, '_#107r>}; ) with 71 <: 105 <: 107 <: 73 and 72 <: 106 <: 107 <: 73 (with some intermediate origins removed)

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

it's not as clear in the facts as it is in the MIR :upside_down: where are they ?!

lqd (Aug 04 2020 at 09:30, on Zulip):

these facts are super confusing, it's like the regions have different names

lqd (Aug 04 2020 at 09:36, on Zulip):

going by the subset graph shape, I think we have 71 <: 61 <: 105 showing up as 77 <: 67 <: 115

nikomatsakis (Aug 04 2020 at 09:42, on Zulip):

ok I might be starting to get a hunch for what the problem is

nikomatsakis (Aug 04 2020 at 09:49, on Zulip):

the regions are indeed confusing but my hunch is this

nikomatsakis (Aug 04 2020 at 09:49, on Zulip):

(side note that the proliferation of intermediate regions and so forth is probably kind of painful for polonius, it's exactly what the opt variants were trying to help... i.e., avoid propagating loan regions along every subset edge...)

nikomatsakis (Aug 04 2020 at 09:50, on Zulip):

anyway my hunch is that, somewhere, we are enforcing the relationship between 71, 72, and 73 -- but we're establishing it once and then expecting it to remain true, but the whole idea of this variant was that we don't have to do that

nikomatsakis (Aug 04 2020 at 09:50, on Zulip):

this example seems to suggest that this idea is wrong, that at least sometimes we do need to carry subset relations forward

nikomatsakis (Aug 04 2020 at 09:51, on Zulip):

I'm trying to wrap my head around it :)

nikomatsakis (Aug 04 2020 at 09:51, on Zulip):

I remember having this feeling that the notion of carrying equality constraints forward also kind of felt like a hack

nikomatsakis (Aug 04 2020 at 09:51, on Zulip):

i.e., that there is a deeper distinction between 'momentary' relations and 'permanent' relations

nikomatsakis (Aug 04 2020 at 09:52, on Zulip):

the latter coming about effectively when you create two kind of distinct aliases, and you need to keep a relationship between the parts

nikomatsakis (Aug 04 2020 at 09:58, on Zulip):

or maybe I'm looking at this wrong

nikomatsakis (Aug 04 2020 at 09:59, on Zulip):

maybe the problem is not that the subset relation should've propagated forward, so much as that we are not enforcing that the type is well-formed at the location or something like that

nikomatsakis (Aug 04 2020 at 09:59, on Zulip):

gonna have to go and come back later though :)

nikomatsakis (Aug 04 2020 at 10:09, on Zulip):

the example as given doesn't show it, but something I'm thinking about is this variant:

 let promoted_fn_item_ref: fn(_, _) -> _ = shorten_lifetime;
nikomatsakis (Aug 04 2020 at 10:09, on Zulip):

playground

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

it's interesting because the _ are going to be instantiated to various &'X i32, &'Y i32, and &'Z i32, and there has to be a relationship between X, Y, and Z that persists

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

but that relationship doesn't come from the fn type itself, it comes from the shorten_lifetime type

nikomatsakis (Aug 04 2020 at 10:11, on Zulip):

this makes me think that the equality variant as written is sort of flawed indeed, that there is a concept of "transient" subset relationships that are only enforced at a particular point, but it's more subtle than I was giving credit to

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

it's pretty subtle and kinda hard to wrap my head around in conversation, without focusing hard on the equality propagation rules for each example

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

I think my take-away here is that the equality variant is kind of incorrect

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

it'd be good to write up the examples in a bit more detail but

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

there is probably a different way to formulate the rules to accept the program(s) I initially wanted to accept

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

I think it'd be more like -- can we identify those cases where the subset relation has to hold instantaneously and just enforce them at a single point and not propagate them forward?

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

but I also think maybe the best "immediate step" here is to take some notes and defer this until we've made progress in other areas

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

we expected it to be incorrect :)

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

some notes/summary would be good for later

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

I can focus on it in the future if it's important, with more dedication than the quick hack job that it is

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

lqd said:

we expected it to be incorrect :)

well, I mean that the concept is incorrect

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

you can't just propagate equality

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

I didn't quite expect that at least :)

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

I was thinking maybe it was an impl bug or something else

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

oh :)

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

me neither evidently, it's interesting/scary that such subtlety was only present in one or two tests

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

which reminds me, that maybe the other unexpected case may contain a different cause

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

lqd said:

me neither evidently, it's interesting/scary that such subtlety was only present in one or two tests

yeah, I was thinking about that :)

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

ok well let me post an update to the issue

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

I forget, did we have an example that compiles with NLL but does not compile with polinius?

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

I feel like we did

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

I found this motivating example on Zulip but I also think maybe it's wrong, though it could (maybe) be made correct

 13:42

let mut x: &'x u32;
let mut y: &'y u32;

if something {
  y = x; // creates `'x: 'y` subset relation
}

if something {
  x = &z; // creates {L0} in 'x constraint
  // this point, we have `'x: 'y` and `{L0} in `'x`, so we also have `{L0} in 'y`
  drop(x);
}

z += 1; // polonius flags an (unnecessary) error

drop(y);

wrong in the sense that I think polonius with just subset rules would accept it

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

in particular, I think x = &z should make 'x be dead on entry to that point, so we would drop the 'x: 'y subset relation

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

I don't remember we had an example that compiled with NLLs and was rejected by polonius

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

oh I see that we already found that

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

this was a revised version of the motivating example

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

ah right right

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

although it too could be resolved with a more precise version

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

lqd said:

I don't remember we had an example that compiled with NLLs and was rejected by polonius

I could be wrong, for some reason I thought we did

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

the "polonius imprecision unnecessary error"

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

if we don't, that's good :)

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

I was basically wondering if there was some extension that would be required to make polonius not break any NLL code

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

I feel like NLL also rejected that

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

it appears it does reject it

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

yes, it does

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

at least crater would be our best bet to find such a case if it exists, compared to finding code that doesn't compile today and shouldn't compile with polonius either

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

+1

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

I would be curious to get @Aaron Weiss's take on the promoted-bounds example, though. MAybe I can draft up my even more troublesome variant of it.

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

example

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

(we could publish a "puzzle of the day" of similar examples, like the sudoku cryptic, but for lifetimes :)

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

my writeup: https://github.com/rust-lang/polonius/issues/107#issuecomment-668612953

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

It seems sort of obvious that this is broken now

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

but of course it wasn't before :)

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

not sure if I should just close the issue or what

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

I'll leave it for now, at least we settled that mystery

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

yeah let's keep it, it's food for thought for the future as there seems to be some real insight in there

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

(on the topic of "exactly one example that showed the problem", I am interested in how we could try to prove polonius correct... but one thing at a time, and it seems like @Aaron Weiss and @Andrea Lattuada are kind of doing work paving that route)

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

/me curious about dafny

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

maybe we need an F* to rust extractor like "rusty kremlin" (IIRC oxide is in F*?)

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

(maybe kremlin would work as is heh)

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

I've finished reading the writeup and it's great, super clear, thanks a bunch

Last update: Jun 20 2021 at 00:15UTC