Stream: t-compiler/wg-polonius

Topic: placeholder loans


lqd (Oct 17 2019 at 18:03, on Zulip):

I’ve been reimplementing illegal subset errors using placeholder loans, and it seems to work in tiny tests. Only in the Naive variant for now but this will work equally with DatafrogOpt (since it’s not using the full subset TC like the previous PR used to). I assumed we wanted to materialize those loans at the root of the cfg, but that’s not an information we currently have, so in the couple tests I was using the lowest point in the sorted cfg edges relation, is that sensible ? (with interning and the existing fact files it might not always work though)

lqd (Oct 17 2019 at 22:34, on Zulip):

(and it kinda throws a wrench into the LocationInsensitive variant as a quick filter pre-pass idea)

lqd (Oct 18 2019 at 18:11, on Zulip):

(I mean illegal subset errors in general — not placeholder loans — aren't taken into account by the LocationInsensitive and thus Hybrid variants, and may always require running the full analysis if we can't approximate their absence quickly ?)

nikomatsakis (Oct 22 2019 at 19:09, on Zulip):

I've been wanting to revisit that blog post for a while now

nikomatsakis (Oct 22 2019 at 19:09, on Zulip):

I'm definitely convinced we want to take the "placeholder loan" approach--

nikomatsakis (Oct 22 2019 at 19:09, on Zulip):

if for no other reason than that I think you should be able to stop at any point and replace all the "origins" with sets of loans

nikomatsakis (Oct 22 2019 at 19:09, on Zulip):

without losing any information

nikomatsakis (Oct 22 2019 at 19:09, on Zulip):

but without placeholder loans, you can't do that

lqd (Oct 22 2019 at 19:11, on Zulip):

yeah it seems like the way to go indeed; wondering about how to pass the cfg root (if I've understood correctly) to "seed" them, and then eventually how to create those placeholder loans in rustc

lqd (Oct 22 2019 at 20:32, on Zulip):

besides the common thought of "all the origins" vs "the ones interacting with potential errors", I wonder if this "stop at any point" thought is related to incr. or the query system, eg if we could avoid borrowck-ing a MIR which hasn't incrementally changed (eg in an IDE context; but outside of that, iirc just changing some comments today would mark everything as needing to be recompiled) or reconsidering our roots in Frank's work and looking at rustc sessions as the source of differential datalog updates

lqd (Nov 12 2019 at 01:30, on Zulip):

as I may still be on the road back from rustfest at the time of the meeting tomorrow, and Niko preferred a WIP PR for placeholder loans here it is so we can discuss more easily https://github.com/rust-lang/polonius/pull/137

nikomatsakis (Nov 18 2019 at 15:10, on Zulip):

I guess we can just continue from here @lqd

nikomatsakis (Nov 18 2019 at 15:10, on Zulip):

Meh, Zulip is ok

lqd (Nov 18 2019 at 15:10, on Zulip):

yeah the topic should be better :)

lqd (Nov 18 2019 at 15:10, on Zulip):

alright

nikomatsakis (Nov 18 2019 at 15:11, on Zulip):

I'm skimming the PR, but I guess we can establish our... "goals" for today

nikomatsakis (Nov 18 2019 at 15:11, on Zulip):

oh and -- we should figure out exactly which other dates we will meet :)

lqd (Nov 18 2019 at 15:11, on Zulip):

agreed

nikomatsakis (Nov 18 2019 at 15:11, on Zulip):

I created one calendar invite, I think I could make another for Wed, not sure if I can do more than that

lqd (Nov 18 2019 at 15:11, on Zulip):

"one invite", for tomorrow that is ?

lqd (Nov 18 2019 at 15:12, on Zulip):

(in addition to today's)

nikomatsakis (Nov 18 2019 at 15:12, on Zulip):

er, yes

lqd (Nov 18 2019 at 15:12, on Zulip):

wrt goals I was thinking:

nikomatsakis (Nov 18 2019 at 15:13, on Zulip):

Yeah

nikomatsakis (Nov 18 2019 at 15:13, on Zulip):

I think ideally we would try to end with the PR merged :)

nikomatsakis (Nov 18 2019 at 15:13, on Zulip):

possibly after tweaks

lqd (Nov 18 2019 at 15:13, on Zulip):
lqd (Nov 18 2019 at 15:13, on Zulip):

right

nikomatsakis (Nov 18 2019 at 15:13, on Zulip):

that reminds me that

nikomatsakis (Nov 18 2019 at 15:13, on Zulip):

since my normal desktop server died

nikomatsakis (Nov 18 2019 at 15:14, on Zulip):

I acutally have to get my laptop to build rustc, I've never tried I don't think

lqd (Nov 18 2019 at 15:14, on Zulip):

oh :)

nikomatsakis (Nov 18 2019 at 15:14, on Zulip):

mostly this means running apt-get I .. hope

nikomatsakis (Nov 18 2019 at 15:14, on Zulip):

but anyway

nikomatsakis (Nov 18 2019 at 15:14, on Zulip):

let's look at the PR

lqd (Nov 18 2019 at 15:14, on Zulip):

let's do it

lqd (Nov 18 2019 at 15:15, on Zulip):

so a lot of the early commits are to the parser itself, for unit tests

lqd (Nov 18 2019 at 15:15, on Zulip):

and other basic to add facts to the inputs and output

lqd (Nov 18 2019 at 15:15, on Zulip):

and the most interesting one is https://github.com/rust-lang/polonius/pull/137/commits/31b79b5efe3e888f247c407171941e61280fc841

nikomatsakis (Nov 18 2019 at 15:16, on Zulip):

only the Naive variant has these errors for now, until we're a bit more sure this is a valid direction, and then I'll apply the technique to the DatafrogOpt variant

nikomatsakis (Nov 18 2019 at 15:16, on Zulip):

we should discuss again whether we can remove DatafrogOpt for now (but not yet)

lqd (Nov 18 2019 at 15:17, on Zulip):

yeah I remember you don't like having many variants for now :)

nikomatsakis (Nov 18 2019 at 15:17, on Zulip):

I assumed the placeholder loans should be seeded into requires (AKA contains) at the root of the CFG, but getting this root uses an heuristic (the first edge in the cfg_edge relation) which probably holds for rustc and unit-tests, but not always for interned .facts files like we have in our input datasets, so maybe the root should be passed to the input with the other relations.

nikomatsakis (Nov 18 2019 at 15:17, on Zulip):

this seems not entirely clear

nikomatsakis (Nov 18 2019 at 15:17, on Zulip):

I sort of remember this now from when I was thinking about it

lqd (Nov 18 2019 at 15:17, on Zulip):

(and datafrogopt is mostly related to performance, which we're trying to put aside for now)

nikomatsakis (Nov 18 2019 at 15:17, on Zulip):

(right, I mostly just don't want to expend mental energy there yet)

lqd (Nov 18 2019 at 15:18, on Zulip):

what is not entirely clear, that the heuristic holds or that the loans need to be seeded at the root ?

nikomatsakis (Nov 18 2019 at 15:18, on Zulip):

well, both

nikomatsakis (Nov 18 2019 at 15:18, on Zulip):

but I meant more the latter

lqd (Nov 18 2019 at 15:18, on Zulip):

:)

nikomatsakis (Nov 18 2019 at 15:18, on Zulip):

in particular,

lqd (Nov 18 2019 at 15:18, on Zulip):

yeah I'm not sure about this either

nikomatsakis (Nov 18 2019 at 15:18, on Zulip):

I'm wondering if it suffices to seed at the root, it seems like you just want this to be true "everywhere"

nikomatsakis (Nov 18 2019 at 15:19, on Zulip):

I guess

nikomatsakis (Nov 18 2019 at 15:19, on Zulip):

so long as the placeholder region is never "dead" (which I think we already require)

nikomatsakis (Nov 18 2019 at 15:19, on Zulip):

then if you inject it at the root, it will flow to all live code at least

lqd (Nov 18 2019 at 15:19, on Zulip):

yeah

lqd (Nov 18 2019 at 15:20, on Zulip):

also I was, maybe wrongly, trying to avoid cases where we materialize something "everywhere" (to try to repeat the OOM-cases)

nikomatsakis (Nov 18 2019 at 15:20, on Zulip):

I'm not sure if it's a problem for it not to reach dead code

nikomatsakis (Nov 18 2019 at 15:20, on Zulip):

this is what I was pondering

nikomatsakis (Nov 18 2019 at 15:20, on Zulip):

but regardless it seems like it'd be "simpler" to just inject everywhere

nikomatsakis (Nov 18 2019 at 15:20, on Zulip):

also I was, maybe wrongly, trying to avoid cases where we materialize something "everywhere"

no, I mean this is not wrong

nikomatsakis (Nov 18 2019 at 15:20, on Zulip):

it surely has a runtime cost,

nikomatsakis (Nov 18 2019 at 15:20, on Zulip):

or else results in multiplied rules

nikomatsakis (Nov 18 2019 at 15:21, on Zulip):

otoh, we're going to have the same effect by injecting it at the root

nikomatsakis (Nov 18 2019 at 15:21, on Zulip):

and letting it propagate

nikomatsakis (Nov 18 2019 at 15:21, on Zulip):

and if we acknowledge it explicitly

nikomatsakis (Nov 18 2019 at 15:21, on Zulip):

we are more able to optimize

lqd (Nov 18 2019 at 15:21, on Zulip):

would you rather be conservative and materialize them at all points first ?

nikomatsakis (Nov 18 2019 at 15:21, on Zulip):

I tend to think we should

nikomatsakis (Nov 18 2019 at 15:21, on Zulip):

it seems simpler

nikomatsakis (Nov 18 2019 at 15:22, on Zulip):

I am also thinking of examples like this

nikomatsakis (Nov 18 2019 at 15:22, on Zulip):

which are "sort of related"

nikomatsakis (Nov 18 2019 at 15:22, on Zulip):
fn foo(x: &'a mut Vec<&'b u32>, y: &'c u32) {
    loop {
        x.push(y);
    }
}
nikomatsakis (Nov 18 2019 at 15:22, on Zulip):

in some variations of NLL, this was accepted, because the function never returned

lqd (Nov 18 2019 at 15:22, on Zulip):

oh interesting

nikomatsakis (Nov 18 2019 at 15:23, on Zulip):

there's a case to be made that this is "ok"

nikomatsakis (Nov 18 2019 at 15:23, on Zulip):

e.g., nobody can ever read the vec again

nikomatsakis (Nov 18 2019 at 15:23, on Zulip):

(I'm ignoring panics here, in any case)

nikomatsakis (Nov 18 2019 at 15:23, on Zulip):

but we decided that it felt wrong, and I think arielb1 had a convincing example why that was which I've forgotten now

nikomatsakis (Nov 18 2019 at 15:24, on Zulip):

in any case this has more to do with the error case

lqd (Nov 18 2019 at 15:24, on Zulip):

ok yeah let's do this then

nikomatsakis (Nov 18 2019 at 15:24, on Zulip):

i.e., it's an error wherever it occurs

nikomatsakis (Nov 18 2019 at 15:24, on Zulip):

we don't just check for errors at "exit nodes"

nikomatsakis (Nov 18 2019 at 15:24, on Zulip):

so here's another question

nikomatsakis (Nov 18 2019 at 15:24, on Zulip):

do we have a canonical write-up of the naive rules in datalog form ?

nikomatsakis (Nov 18 2019 at 15:24, on Zulip):

also, are we actually publishing the book successfully?

nikomatsakis (Nov 18 2019 at 15:25, on Zulip):

I think the answer to both is no :)

nikomatsakis (Nov 18 2019 at 15:25, on Zulip):

but I'd like the answer to both to be yes, and to have that write-up be in the book

lqd (Nov 18 2019 at 15:25, on Zulip):

we are publishing the book

nikomatsakis (Nov 18 2019 at 15:25, on Zulip):

ok, that's good

lqd (Nov 18 2019 at 15:25, on Zulip):

but don't have a canonical version of the rules I don't think, yet

nikomatsakis (Nov 18 2019 at 15:25, on Zulip):

oh I think it was salsa where I screwed that up months ago and have not gotten around to fixing it yet

nikomatsakis (Nov 18 2019 at 15:25, on Zulip):

ok, that should be easy enough to extract from the naive secction I guess

lqd (Nov 18 2019 at 15:25, on Zulip):

chalk also had problems

nikomatsakis (Nov 18 2019 at 15:25, on Zulip):

yes, chalk also has problems

nikomatsakis (Nov 18 2019 at 15:25, on Zulip):

sigh

lqd (Nov 18 2019 at 15:25, on Zulip):

I do have the old ones I think

lqd (Nov 18 2019 at 15:26, on Zulip):

Pietro fixed them btw

nikomatsakis (Nov 18 2019 at 15:26, on Zulip):

:tada:

nikomatsakis (Nov 18 2019 at 15:26, on Zulip):

but ok https://rust-lang.github.io/polonius/ works, yes

nikomatsakis (Nov 18 2019 at 15:26, on Zulip):

maybe we can make a hackmd now

nikomatsakis (Nov 18 2019 at 15:26, on Zulip):

that has the canonical rules

lqd (Nov 18 2019 at 15:26, on Zulip):

I do have the ones I used to test on Soufflé with IIRC, where we had the rules "duplicated" with universal_regions

nikomatsakis (Nov 18 2019 at 15:26, on Zulip):

I can do that

lqd (Nov 18 2019 at 15:27, on Zulip):

I might be able to find a more recent version but otherwise: https://gist.github.com/lqd/355588dd6ab9b852469110edc8f6192f

lqd (Nov 18 2019 at 15:27, on Zulip):

(it also lacks liveness/initialization)

lqd (Nov 18 2019 at 15:27, on Zulip):

(and errors ...)

nikomatsakis (Nov 18 2019 at 15:28, on Zulip):

yes so

nikomatsakis (Nov 18 2019 at 15:28, on Zulip):

one of the reasons I'm talking about this

nikomatsakis (Nov 18 2019 at 15:28, on Zulip):

is that I'd like to have this so we can talk about liveness/init in those terms too

nikomatsakis (Nov 18 2019 at 15:28, on Zulip):

hackmd document

nikomatsakis (Nov 18 2019 at 15:29, on Zulip):

I guess it will also let us tweak names ;)

nikomatsakis (Nov 18 2019 at 15:30, on Zulip):

I'm reconciling this against naive.rs right now

nikomatsakis (Nov 18 2019 at 15:33, on Zulip):

Ok, this looks roughly complete?

nikomatsakis (Nov 18 2019 at 15:33, on Zulip):

I don't think we should go overboard with the .output and so forth

lqd (Nov 18 2019 at 15:33, on Zulip):

yeah

nikomatsakis (Nov 18 2019 at 15:33, on Zulip):

but it doesn't matter really

nikomatsakis (Nov 18 2019 at 15:33, on Zulip):

ok, so, to add placeholder loans is fairly minimal...

nikomatsakis (Nov 18 2019 at 15:33, on Zulip):

(I'm really restraining myself from doing a mass rename here. This is hard.)

lqd (Nov 18 2019 at 15:33, on Zulip):

maybe just note at the point your thoughts about renaming

lqd (Nov 18 2019 at 15:34, on Zulip):

and I'll take care of it soon

nikomatsakis (Nov 18 2019 at 15:35, on Zulip):

what should we call requires... idk. something else though =)

nikomatsakis (Nov 18 2019 at 15:35, on Zulip):

anyway for placeholder loans, I think you added an input, right, that identifies the placeholder regions + loans?

nikomatsakis (Nov 18 2019 at 15:35, on Zulip):

e.g., extend universal_region perhaps to placeholder_region(R, L)?

nikomatsakis (Nov 18 2019 at 15:35, on Zulip):

I should look what you actually did in your PR...

nikomatsakis (Nov 18 2019 at 15:36, on Zulip):

ah, right, and we need known_subset

lqd (Nov 18 2019 at 15:36, on Zulip):

yeah

lqd (Nov 18 2019 at 15:36, on Zulip):

I was thinking of needing to fuse universal_regions with their loans

lqd (Nov 18 2019 at 15:36, on Zulip):

so that it's more "a unit of information" but couljd be done later

lqd (Nov 18 2019 at 15:37, on Zulip):

and I seeded requires with placeholder_loans at the cfg root

lqd (Nov 18 2019 at 15:37, on Zulip):

I'll add that as a WIP

lqd (Nov 18 2019 at 15:38, on Zulip):

(or just requires everywhere)

nikomatsakis (Nov 18 2019 at 15:38, on Zulip):

I think I would just make the input be placeholder_data(region, loan) or something like that

nikomatsakis (Nov 18 2019 at 15:39, on Zulip):

then we can derive placeholder_origins (nee universal_regions) from that

nikomatsakis (Nov 18 2019 at 15:39, on Zulip):

I'm mostly looking here to express the rules in the most elegant form

lqd (Nov 18 2019 at 15:39, on Zulip):

ah interesting yes

nikomatsakis (Nov 18 2019 at 15:39, on Zulip):

to aid in explanation / comprehension

nikomatsakis (Nov 18 2019 at 15:41, on Zulip):

oh I think requires should just be contains

lqd (Nov 18 2019 at 15:41, on Zulip):

true!

nikomatsakis (Nov 18 2019 at 15:41, on Zulip):

("origins" contain "loans")

lqd (Nov 18 2019 at 15:41, on Zulip):

this is one we talked about but didn't get to yet

lqd (Nov 18 2019 at 15:43, on Zulip):

seeding the placeholder loans like this

requires(R, B, P) :-
  cfg_edge(P, _),
  placeholder_data(R, B).

seems a bit weird

nikomatsakis (Nov 18 2019 at 15:43, on Zulip):

heh

lqd (Nov 18 2019 at 15:43, on Zulip):

(maybe also both points should be in there)

nikomatsakis (Nov 18 2019 at 15:43, on Zulip):

we have no node relation

nikomatsakis (Nov 18 2019 at 15:43, on Zulip):

but we should probably make one?

nikomatsakis (Nov 18 2019 at 15:43, on Zulip):

also, the names in this doc (e.g., of atoms)

nikomatsakis (Nov 18 2019 at 15:44, on Zulip):

are pretty out of date

nikomatsakis (Nov 18 2019 at 15:44, on Zulip):

(and hence I think out of sync with repo?)

nikomatsakis (Nov 18 2019 at 15:44, on Zulip):

but we should probably make one?

I am debating if it should be an input, or derived from the others

nikomatsakis (Nov 18 2019 at 15:44, on Zulip):

but it seems like an input

nikomatsakis (Nov 18 2019 at 15:44, on Zulip):

i.e., you can have a node with no adjacent edges...

lqd (Nov 18 2019 at 15:44, on Zulip):

we could make a node / point relation, I'm not sure we need to materialize it for real

nikomatsakis (Nov 18 2019 at 15:45, on Zulip):

yeah I'm debating about it

nikomatsakis (Nov 18 2019 at 15:45, on Zulip):

it's not really a very interesting case

nikomatsakis (Nov 18 2019 at 15:45, on Zulip):

i.e., you can have a node with no adjacent edges...

this one

lqd (Nov 18 2019 at 15:45, on Zulip):

yeah very out of date, I think they must date back to our initial explorations last year

lqd (Nov 18 2019 at 15:46, on Zulip):

(the names are out of sync for sure, but the rules seems likely in sync)

lqd (Nov 18 2019 at 15:46, on Zulip):

(but I will check later)

nikomatsakis (Nov 18 2019 at 15:47, on Zulip):

anyway this looks correct to me

nikomatsakis (Nov 18 2019 at 15:47, on Zulip):

seems simple enough

lqd (Nov 18 2019 at 15:47, on Zulip):

right

nikomatsakis (Nov 18 2019 at 15:47, on Zulip):

modulo the node relation bit

lqd (Nov 18 2019 at 15:48, on Zulip):

albin mentioned they had once this question about the cfg root

lqd (Nov 18 2019 at 15:48, on Zulip):

and moved away from requiring it so at least we shouldn't need for now

nikomatsakis (Nov 18 2019 at 15:48, on Zulip):

hmm so

nikomatsakis (Nov 18 2019 at 15:49, on Zulip):

never mind

nikomatsakis (Nov 18 2019 at 15:49, on Zulip):

and moved away from requiring it so at least we shouldn't need for now

interesting

nikomatsakis (Nov 18 2019 at 15:49, on Zulip):

ok

lqd (Nov 18 2019 at 15:50, on Zulip):

you really do want to move to nodes instead of points

nikomatsakis (Nov 18 2019 at 15:50, on Zulip):

I don't know :)

nikomatsakis (Nov 18 2019 at 15:50, on Zulip):

I realized I am using single letters, too

nikomatsakis (Nov 18 2019 at 15:50, on Zulip):

when we said we'd use Node1 etc

nikomatsakis (Nov 18 2019 at 15:51, on Zulip):

I forget what we said about capitalization, but I found the all-lower-case a bit harder to read...

nikomatsakis (Nov 18 2019 at 15:51, on Zulip):

and the full words a bit long (line wrap)

nikomatsakis (Nov 18 2019 at 15:51, on Zulip):

but I still think it's probably correct to use the full words

nikomatsakis (Nov 18 2019 at 15:51, on Zulip):

anyway, so we've got our version of the rules

nikomatsakis (Nov 18 2019 at 15:51, on Zulip):

we need to clean it up

nikomatsakis (Nov 18 2019 at 15:51, on Zulip):

but about the PR

lqd (Nov 18 2019 at 15:52, on Zulip):

we can capitalize for sure

lqd (Nov 18 2019 at 15:52, on Zulip):

should also help testing with regular datalog engines

nikomatsakis (Nov 18 2019 at 15:52, on Zulip):

right

nikomatsakis (Nov 18 2019 at 15:52, on Zulip):
.decl subset_errors(Origin1, Origin2, Point)
subset_errors(Origin1, Origin2, Point) :-
  placeholder_data(Origin1, Loan1),
  placeholder_origin(Origin2),
  requires(Origin2, Loan1, Point),
  !known_subset(Origin1, Origin2).
nikomatsakis (Nov 18 2019 at 15:54, on Zulip):

hmm so is known_subset transitive?

nikomatsakis (Nov 18 2019 at 15:54, on Zulip):

I think we should do the transitive stuff on the polonius side, probably

nikomatsakis (Nov 18 2019 at 15:54, on Zulip):

so the input is probably known_subset_base?

lqd (Nov 18 2019 at 15:54, on Zulip):

I assumed it was a flat list

nikomatsakis (Nov 18 2019 at 15:54, on Zulip):

I am wondering if it should instead be known_contains_base

lqd (Nov 18 2019 at 15:54, on Zulip):

so yes, we'd need to do the transitivity inside polonius

nikomatsakis (Nov 18 2019 at 15:54, on Zulip):

i.e., known_contains_base(O:origin, L:loan)

nikomatsakis (Nov 18 2019 at 15:54, on Zulip):

well regardless we can compute known_contains

nikomatsakis (Nov 18 2019 at 15:55, on Zulip):

I guess it's not very different

nikomatsakis (Nov 18 2019 at 15:55, on Zulip):

but

nikomatsakis (Nov 18 2019 at 15:55, on Zulip):
.decl subset_errors(Origin1, Origin2, Point)
subset_errors(Origin1, Origin2, Point) :-
  contains(Origin2, Loan1, Point),
  placeholder_origin(Origin2),
  placeholder_data(Origin1, Loan2)
  !known_contains(Origin2, Loan1).
nikomatsakis (Nov 18 2019 at 15:56, on Zulip):

wait, that's wrong

nikomatsakis (Nov 18 2019 at 15:56, on Zulip):
.decl subset_errors(Origin1, Origin2, Point)
subset_errors(Origin1, Origin2, Point) :-
  placeholder_data(Origin1, Loan1)
  placeholder_data(Origin2, _)
  contains(Origin2, Loan1, Point),
  !known_contains(Origin2, Loan1).
nikomatsakis (Nov 18 2019 at 15:56, on Zulip):

anyway, I find that mildly easier to read

nikomatsakis (Nov 18 2019 at 15:56, on Zulip):

(interestingly, I sort of prefer the placeholder_data both times just because it makes those two lines easier for me to parse)

lqd (Nov 18 2019 at 15:57, on Zulip):

same for me :)

nikomatsakis (Nov 18 2019 at 15:57, on Zulip):

(not sure about the name placeholder_data, maybe even just placeholder ?)

lqd (Nov 18 2019 at 15:57, on Zulip):

sounds nice

nikomatsakis (Nov 18 2019 at 15:58, on Zulip):

we can just do placeholder(O, _) instead of placeholder_origin, as well

lqd (Nov 18 2019 at 15:58, on Zulip):

(and also solves the terminology questions I had in the other doc PR)

nikomatsakis (Nov 18 2019 at 16:00, on Zulip):
.decl known_contains(O:origin, L:loan)
known_contains(Origin1, Loan1) :-
  placeholder(Origin1, Loan1)
known_contains(Origin2, Loan1) :-
  known_contains(Origin1, Loan1),
  known_subset(Origin1, Origin2).
nikomatsakis (Nov 18 2019 at 16:00, on Zulip):

?

nikomatsakis (Nov 18 2019 at 16:00, on Zulip):

I think that is correct

lqd (Nov 18 2019 at 16:00, on Zulip):

/me was typing that hehe

lqd (Nov 18 2019 at 16:01, on Zulip):

it looks sensible

nikomatsakis (Nov 18 2019 at 16:02, on Zulip):
contains(Origin, Loan, P) :-
  cfg_edge(P, _),
  placeholder(Origin, Loan).
nikomatsakis (Nov 18 2019 at 16:02, on Zulip):

so I agree that we probably need the targets too, no?

lqd (Nov 18 2019 at 16:03, on Zulip):

yeah, or node

nikomatsakis (Nov 18 2019 at 16:03, on Zulip):

I kind of think we should just make node

lqd (Nov 18 2019 at 16:05, on Zulip):

yeah and in any case all these static rules should be "rust" code, eg Relation::extend and the likes, rather than using iterations and joins

nikomatsakis (Nov 18 2019 at 16:05, on Zulip):

correct

nikomatsakis (Nov 18 2019 at 16:05, on Zulip):

ok, so, what does it take to land the PR now...

nikomatsakis (Nov 18 2019 at 16:05, on Zulip):

it's slightly different than the hackmd

lqd (Nov 18 2019 at 16:06, on Zulip):

oh btw

lqd (Nov 18 2019 at 16:06, on Zulip):

in the PR text I was mentioning a use-case extracted from rust, a dataset in the inputs folder

lqd (Nov 18 2019 at 16:06, on Zulip):

subset-relations, which had 3 fns, and a case was confusing me, but looking more at the mir seems correct

lqd (Nov 18 2019 at 16:07, on Zulip):

(the desugaring, wrt lifetimes here, is still a bit confusing to me)

nikomatsakis (Nov 18 2019 at 16:08, on Zulip):

where is this in the PR text?

lqd (Nov 18 2019 at 16:08, on Zulip):

I wanted to ask, we always have two tuples in universal_regions, '0 and '1, what is this '1 ? I thought it was related to 'static, eg a local version, at some point, but I'm not so sure anymore

nikomatsakis (Nov 18 2019 at 16:08, on Zulip):

ah

nikomatsakis (Nov 18 2019 at 16:08, on Zulip):

'0 is 'static

lqd (Nov 18 2019 at 16:09, on Zulip):

I added simple dataset with 3 examples but it was partially manually constructed as I haven't added support for those facts to rustc yet, and while there is a function where an expected subset error occurs, I'm not sure it's about the correct origins (the .facts being a bit distant from the original rust code, and rustfest-induced lack of sleep, make it hard to be sure right now)

this

nikomatsakis (Nov 18 2019 at 16:09, on Zulip):

I think '1 is representing the "entire fn body" -- I'm not sure this is a concept that makes sense in polonius actually

nikomatsakis (Nov 18 2019 at 16:09, on Zulip):

let me go back and check the source

lqd (Nov 18 2019 at 16:09, on Zulip):

this test is the first I've seen where somewhere flowed into '1

nikomatsakis (Nov 18 2019 at 16:10, on Zulip):

which example did it come from?

lqd (Nov 18 2019 at 16:11, on Zulip):

./inputs/subset-relations/subset-relations.rs

lqd (Nov 18 2019 at 16:11, on Zulip):

missing_subset

lqd (Nov 18 2019 at 16:12, on Zulip):

(the 3 are basically the same wrt subset errors)

lqd (Nov 18 2019 at 16:12, on Zulip):

and I manually added the placeholder loans (and a known subset to make valid_subset work)

lqd (Nov 18 2019 at 16:15, on Zulip):

to land the PR: we'd want to be close to the parts of the hackmd related to subset_errors, placeholder, known_subset and its transitive version, right ? (that is, not to the complete hackmd where we already started renaming relations)

nikomatsakis (Nov 18 2019 at 16:17, on Zulip):

yes

nikomatsakis (Nov 18 2019 at 16:17, on Zulip):

I'm looking at that input now

lqd (Nov 18 2019 at 16:17, on Zulip):

I'll work on that then !

lqd (Nov 18 2019 at 16:18, on Zulip):

btw if you need a rustc version working with polonius master I have branch ready for you (we haven't published nor updated rustc since the FactTypes PR)

nikomatsakis (Nov 18 2019 at 16:19, on Zulip):

OK

lqd (Nov 18 2019 at 16:19, on Zulip):

(https://github.com/lqd/rust/tree/placeholder_loans)

lqd (Nov 18 2019 at 16:19, on Zulip):

it doesn't generate the placeholder/known_subset facts though

nikomatsakis (Nov 18 2019 at 16:20, on Zulip):

so @lqd I think that the fn body region

nikomatsakis (Nov 18 2019 at 16:20, on Zulip):

comes after the others

lqd (Nov 18 2019 at 16:20, on Zulip):

(it doesn't look at subset_errors either :joy:)

nikomatsakis (Nov 18 2019 at 16:20, on Zulip):

i.e., '0 is always static

lqd (Nov 18 2019 at 16:21, on Zulip):

aaaaaaaaaaaah

nikomatsakis (Nov 18 2019 at 16:21, on Zulip):

but '1 and '2 would be 'a and 'b respectively

nikomatsakis (Nov 18 2019 at 16:21, on Zulip):

and '3 is the fn body

lqd (Nov 18 2019 at 16:21, on Zulip):

that makes the result very clear now

lqd (Nov 18 2019 at 16:21, on Zulip):

thank you :)

nikomatsakis (Nov 18 2019 at 16:21, on Zulip):

for the missing_subset example, looking at the output from -Zmir-dump=nll, I get

| Free Region Mapping
| '_#0r | Global | ['_#0r, '_#3r, '_#1r, '_#2r]
| '_#1r | Local | ['_#3r, '_#1r]
| '_#2r | Local | ['_#3r, '_#2r]
| '_#3r | Local | ['_#3r]
nikomatsakis (Nov 18 2019 at 16:22, on Zulip):

which I think makes sense -- everything "outlives" the fn body

lqd (Nov 18 2019 at 16:22, on Zulip):

yeah

nikomatsakis (Nov 18 2019 at 16:22, on Zulip):

I guess that the fn body concept makes no sense in polonius but is also not actively harmful

nikomatsakis (Nov 18 2019 at 16:22, on Zulip):

it's basically the union of all placeholder origins

lqd (Nov 18 2019 at 16:22, on Zulip):

I checked afterwards that the renumbered 'a and 'b matched what I was expecting

lqd (Nov 18 2019 at 16:22, on Zulip):

which it does, so only the numbering was confusing

lqd (Nov 18 2019 at 16:23, on Zulip):

but yeah it's clear now :)

nikomatsakis (Nov 18 2019 at 16:23, on Zulip):

to land the PR: we'd want to be close to the parts of the hackmd related to subset_errors, placeholder, known_subset and its transitive version, right ? (that is, not to the complete hackmd where we already started renaming relations)

I guess I will quickly skim the other commits --

nikomatsakis (Nov 18 2019 at 16:23, on Zulip):

I could also try to make some edits to the polonius book

lqd (Nov 18 2019 at 16:24, on Zulip):

I was wondering how we'd generate the placeholder loans in rustc ?

lqd (Nov 18 2019 at 16:24, on Zulip):

and I assumed we'd need to change https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#method.check_universal_regions to check for subset errors

nikomatsakis (Nov 18 2019 at 16:24, on Zulip):

I think we would iterate over the "universal regions" and make one placeholder tuple for each

nikomatsakis (Nov 18 2019 at 16:24, on Zulip):

that said, I realize I'm a bit confused -- did you implement the rustc side of this on that branch?

lqd (Nov 18 2019 at 16:25, on Zulip):

I did not implement the rustc side no

lqd (Nov 18 2019 at 16:25, on Zulip):

I only have a branch where master compiles using the polonius wip branch, so that I could then implement the rustc side

nikomatsakis (Nov 18 2019 at 16:26, on Zulip):

ah ok

lqd (Nov 18 2019 at 16:26, on Zulip):

here I didn't know how to create a BorrowIndex for the placeholder loans tuples

nikomatsakis (Nov 18 2019 at 16:26, on Zulip):

I could also help with that perhaps

nikomatsakis (Nov 18 2019 at 16:26, on Zulip):

I can start just by jotting down a few notes

lqd (Nov 18 2019 at 16:27, on Zulip):

(and was just expecting to check the polonius output in check_universal_regions but not yet where to thread the polonius output)

lqd (Nov 18 2019 at 16:27, on Zulip):

that would be very helpful :)

lqd (Nov 18 2019 at 16:30, on Zulip):

I'd like to have some tests to land the PR, there are not enough like this. I was thinking I'd implement the rustc side of fact gen and then integrate some of the ui tests into the inputs and check those in the unit tests, just to be on the safe side, in addition to having the ui tests work once the feature is complete and rustc can check the polonius-computed subset_errors

nikomatsakis (Nov 18 2019 at 16:32, on Zulip):

it seems like trying to do some renaming in the code would be dumb, we should wait until end of the week for that, agreed?

lqd (Nov 18 2019 at 16:32, on Zulip):

agreed

lqd (Nov 18 2019 at 16:33, on Zulip):

it'll probably be easier to do so once the different WIP work lands

lqd (Nov 18 2019 at 16:33, on Zulip):

even if it's a bit uglier as it lands ?

nikomatsakis (Nov 18 2019 at 16:34, on Zulip):

that was my thought

nikomatsakis (Nov 18 2019 at 16:34, on Zulip):

but I would like to try to mvoe the docs to the new names

nikomatsakis (Nov 18 2019 at 16:34, on Zulip):

maybe that's confuisng :/ but I think it helps me :)

nikomatsakis (Nov 18 2019 at 16:34, on Zulip):

e.g. it took me some time to figure out requires, but contains reads nicely

nikomatsakis (Nov 18 2019 at 16:35, on Zulip):

also, I'm inclined to just land your book changes

nikomatsakis (Nov 18 2019 at 16:35, on Zulip):

and then try to read over them in place and make edits myself

nikomatsakis (Nov 18 2019 at 16:35, on Zulip):

any objection? I'm talking about rust-lang/polonius#126

lqd (Nov 18 2019 at 16:35, on Zulip):

we could do both also

lqd (Nov 18 2019 at 16:36, on Zulip):

you editing docs doesn't seem like the greatest use of your time, but it can be seen as notes of what to reach in the code :)

nikomatsakis (Nov 18 2019 at 16:36, on Zulip):

yes, that was how I thought of it

lqd (Nov 18 2019 at 16:41, on Zulip):

I think I'd like to rename placeholder_loan to placeholder, and then ultimately remove universal_region since it is used everywhere (including .facts in the repo)

lqd (Nov 18 2019 at 16:42, on Zulip):

and/or compute universal_regions in terms of placeholder instead of doing both at once, since we effectively never use universal_region

lqd (Nov 18 2019 at 16:43, on Zulip):

I guess that is a difference between the hackmd and the real code

nikomatsakis (Nov 18 2019 at 16:43, on Zulip):

yes, I did that in the hackmd

nikomatsakis (Nov 18 2019 at 16:43, on Zulip):

and I approve

nikomatsakis (Nov 18 2019 at 16:43, on Zulip):

also, I reviewed the rest of the PR, which seems fine, I left a few stray comments

lqd (Nov 18 2019 at 16:43, on Zulip):

(as instead of duplicating the rules we materialized all the free regions in the liveness)

lqd (Nov 18 2019 at 16:43, on Zulip):

ok awesome thanks a lot

nikomatsakis (Nov 18 2019 at 16:43, on Zulip):

yeah, we were lazy

nikomatsakis (Nov 18 2019 at 16:44, on Zulip):

your datalog compiler might make a difference here?

nikomatsakis (Nov 18 2019 at 16:44, on Zulip):

i.e., if we could write ; rules...

nikomatsakis (Nov 18 2019 at 16:44, on Zulip):

(or, even better, macros...)

lqd (Nov 18 2019 at 16:44, on Zulip):

interesting thought :)

lqd (Nov 18 2019 at 16:44, on Zulip):

it could yeah

lqd (Nov 18 2019 at 16:45, on Zulip):

(when it supports ; ofc)

lqd (Nov 18 2019 at 16:45, on Zulip):

(Vytautas added a bunch of syntax for rustql when we were at rustfest)

nikomatsakis (Nov 18 2019 at 16:45, on Zulip):

Given OOM concerns I definitely think duplicating the rules is better

nikomatsakis (Nov 18 2019 at 16:45, on Zulip):

Personally i'm ready to port polonius :)

lqd (Nov 18 2019 at 16:45, on Zulip):

yeah, even if they are ultimately about equal regions

nikomatsakis (Nov 18 2019 at 16:45, on Zulip):

but that's a topic for another day I guess

nikomatsakis (Nov 18 2019 at 16:46, on Zulip):

anyway I'm going to leave some notes re: rustc

lqd (Nov 18 2019 at 16:46, on Zulip):

it still not generating a complete computation at the moment :) but we'll get there

lqd (Nov 18 2019 at 16:46, on Zulip):

thanks a lot for the notes, it'll save me a bunch of time

nikomatsakis (Nov 18 2019 at 16:47, on Zulip):

ps, I think I found I like "node"

nikomatsakis (Nov 18 2019 at 16:47, on Zulip):

curious about your opinion :) you seem to disagree

nikomatsakis (Nov 18 2019 at 16:47, on Zulip):

but cfg_node relation pushed me over the edge

lqd (Nov 18 2019 at 16:47, on Zulip):

I'm more used to nodes as being basic blocks which is not our case here but I don't have that strong of an opinion

lqd (Nov 18 2019 at 16:47, on Zulip):

node is fine :)

nikomatsakis (Nov 18 2019 at 16:48, on Zulip):

ugh, building rustc is like killing my computer =)

nikomatsakis (Nov 18 2019 at 16:48, on Zulip):

/me remembers why he prefers to build on server

lqd (Nov 18 2019 at 16:48, on Zulip):

:)

lqd (Nov 18 2019 at 16:48, on Zulip):

I have built rustc on a 7y old macbook air, that was fun, and slow

lqd (Nov 18 2019 at 16:49, on Zulip):

(but it's very helpful for polonius performance work)

lqd (Nov 18 2019 at 16:57, on Zulip):

about known_subset, you mentioned:

this doesn't seem useful in the new formulation, but maybe known_contains?

ah this is about the debugging output, agreed

lqd (Nov 18 2019 at 17:05, on Zulip):

do we eventually also want to move to uppercasing the datalog variables in code comments ?
eg from

/// `known_subset(origin1, origin2)` when the "placeholder" `origin1` is a known subset
/// of placeholder `origin2`.
pub known_subset: Vec<(T::Origin, T::Origin)>,

to

/// `known_subset(Origin1, Origin2)` when the "placeholder" `Origin1` is a known subset
/// of placeholder `Origin2`.
pub known_subset: Vec<(T::Origin, T::Origin)>,

?

nikomatsakis (Nov 18 2019 at 17:09, on Zulip):

@lqd tough call :)

nikomatsakis (Nov 18 2019 at 17:09, on Zulip):

I think I would prefer to do so though

nikomatsakis (Nov 18 2019 at 17:09, on Zulip):

the mapping shouldn't be that hard

lqd (Nov 18 2019 at 17:09, on Zulip):

yeah, and it's valuable to have a close relation to the rules themselves

nikomatsakis (Nov 18 2019 at 17:10, on Zulip):

right

nikomatsakis (Nov 18 2019 at 17:12, on Zulip):

btw @lqd check you check the "compiler notes" section in the hackmd?

nikomatsakis (Nov 18 2019 at 17:12, on Zulip):

it turned out to be a bit thornier than I expected

lqd (Nov 18 2019 at 17:12, on Zulip):

reading it now

lqd (Nov 18 2019 at 17:12, on Zulip):

thornier for checking the errors or generating the input facts ?

nikomatsakis (Nov 18 2019 at 17:13, on Zulip):

well both maybe ?

nikomatsakis (Nov 18 2019 at 17:13, on Zulip):

it's not that bad really

nikomatsakis (Nov 18 2019 at 17:13, on Zulip):

there's a few subtle bits

nikomatsakis (Nov 18 2019 at 17:13, on Zulip):

I'm not sure if you're familiar with the ClosureOutlivesRequirement code?

nikomatsakis (Nov 18 2019 at 17:13, on Zulip):

that is, the way we handle closures

lqd (Nov 18 2019 at 17:14, on Zulip):

no especially familiar unfortunately

nikomatsakis (Nov 18 2019 at 17:14, on Zulip):

it's actually not a big deal

nikomatsakis (Nov 18 2019 at 17:14, on Zulip):

the main thing is

nikomatsakis (Nov 18 2019 at 17:14, on Zulip):

when we type-check closures

lqd (Nov 18 2019 at 17:14, on Zulip):

(I was thinking whether we'd end up having to tangle with closures heh)

nikomatsakis (Nov 18 2019 at 17:14, on Zulip):

we only report some errors immediately

nikomatsakis (Nov 18 2019 at 17:15, on Zulip):

the rest we propagated back to the closure's creator

nikomatsakis (Nov 18 2019 at 17:15, on Zulip):

there are some comments on this somewhere I can find, but the details of how it works don't matter

nikomatsakis (Nov 18 2019 at 17:15, on Zulip):

the main thing is that the "handle error" code sometimes reports the error

lqd (Nov 18 2019 at 17:15, on Zulip):

ah yes the Option in check_universal_regions

nikomatsakis (Nov 18 2019 at 17:15, on Zulip):

and other types pushes it into the ClosureOutlivesRequirement struct

nikomatsakis (Nov 18 2019 at 17:15, on Zulip):

that doesn't affect thsi code path but I thought it might be important context when reading the code and trying to figure out wtf is going on

nikomatsakis (Nov 18 2019 at 17:16, on Zulip):

ah, here is the comment

lqd (Nov 18 2019 at 17:16, on Zulip):

ah yeah thanks for this context, I remembered we push some of these obligations but didn't remember in which cases

nikomatsakis (Nov 18 2019 at 17:17, on Zulip):

doc comment of ClosureRegionRequirements

lqd (Nov 18 2019 at 17:17, on Zulip):

oh nice

nikomatsakis (Nov 18 2019 at 17:17, on Zulip):

hmm, that comment doesn't give as much context as I would hope

nikomatsakis (Nov 18 2019 at 17:17, on Zulip):

though maybe it helps ;)

nikomatsakis (Nov 18 2019 at 17:17, on Zulip):

it's more about the details of how things are encoded, not why

nikomatsakis (Nov 18 2019 at 17:18, on Zulip):

Anyway, so, the fact generation did seem a touch trickier than I thought

lqd (Nov 18 2019 at 17:18, on Zulip):

at the very least it's a good todo item for someone to add to the rustc-guide eventually :)

nikomatsakis (Nov 18 2019 at 17:18, on Zulip):

in that we have to make "placeholder loans" which isn't a concept tha NLL has

nikomatsakis (Nov 18 2019 at 17:18, on Zulip):

but I think we can just hack?

nikomatsakis (Nov 18 2019 at 17:18, on Zulip):

the way I suggested

nikomatsakis (Nov 18 2019 at 17:18, on Zulip):

yeah I should go check what's in rustc guid

nikomatsakis (Nov 18 2019 at 17:19, on Zulip):

for all that I talk about the guide, I feel like the NLL coverage leaves much to be desired :(

lqd (Nov 18 2019 at 17:19, on Zulip):

the hack seems liek it should work

lqd (Nov 18 2019 at 17:19, on Zulip):

your recent work about member constraints and general documentation made it a lot better tho

nikomatsakis (Nov 18 2019 at 17:20, on Zulip):

yeah, I was just skimming

nikomatsakis (Nov 18 2019 at 17:20, on Zulip):

it could be worse

nikomatsakis (Nov 18 2019 at 17:20, on Zulip):

anyway

nikomatsakis (Nov 18 2019 at 17:20, on Zulip):

I know there are some comments somewhere wiht more details but maybe not one individual comment saying all the things

nikomatsakis (Nov 18 2019 at 17:21, on Zulip):

the hack seems liek it should work

I think so too

nikomatsakis (Nov 18 2019 at 17:21, on Zulip):

and it's super easy

nikomatsakis (Nov 18 2019 at 17:21, on Zulip):

anyway the main question mark that I wasn't sure about

nikomatsakis (Nov 18 2019 at 17:21, on Zulip):

was how to handle the placeholder errors

nikomatsakis (Nov 18 2019 at 17:21, on Zulip):

let me go sprinkle some links into the code

lqd (Nov 18 2019 at 17:21, on Zulip):

I'll need to thread the polonius output somehow as well but that should be easier than the rest

nikomatsakis (Nov 18 2019 at 17:21, on Zulip):

then I have to run and get lunch + have family meeting with the partner :)

nikomatsakis (Nov 18 2019 at 17:22, on Zulip):

I'll need to thread the polonius output somehow as well but that should be easier than the rest

yeah, that seems pretty easy, just add parameters to a few fns

lqd (Nov 18 2019 at 17:22, on Zulip):

right

nikomatsakis (Nov 18 2019 at 17:22, on Zulip):

those fns already have like 2 dozen parametrs, what's one more :angel:

lqd (Nov 18 2019 at 17:23, on Zulip):

then I have to run and get lunch + have family meeting with the partner :)

of course :) we're nearing the end of the scheduled time, don't hesitate to go early as well

lqd (Nov 18 2019 at 17:23, on Zulip):

thank you for your time already, it was super super helpful

lqd (Nov 18 2019 at 17:23, on Zulip):

and I have an idea on how to complete the different next steps

nikomatsakis (Nov 18 2019 at 17:25, on Zulip):

@lqd ok I added a few links and things

nikomatsakis (Nov 18 2019 at 17:25, on Zulip):

that hopefully makes it a bit clearer what i'm talking about

lqd (Nov 18 2019 at 17:28, on Zulip):

yeah looking at it as you type :)

nikomatsakis (Nov 18 2019 at 17:28, on Zulip):

ok, g2g, bbl! :)

lqd (Nov 18 2019 at 17:29, on Zulip):

thanks a lot niko :) ttyl

lqd (Nov 19 2019 at 03:16, on Zulip):

I do wonder whether DatafrogOpt is compatible with placeholder loans, or if its TC-avoidance could scare the placeholder loans away ^^ (most likely that I'm missing something trying to make it compute subset errors at 4AM). In any case most of the polonius-side of the work we mentioned earlier seems done

lqd (Nov 19 2019 at 13:21, on Zulip):

hey @pnkfelix :) I was wondering if you could point me to some borrowck code about universal regions: I'm trying to emit the universal regions relations as facts for polonius, but I'm not sure where to look for. I thought I should output UniversalRegionRelations.outlives but I don't see an easy way to do so (and it looks more like a builder even though you can query it)

pnkfelix (Nov 19 2019 at 13:22, on Zulip):

I do not have that info in my mental cache

lqd (Nov 19 2019 at 13:23, on Zulip):

so I'm guessing it's probably not this

lqd (Nov 19 2019 at 13:23, on Zulip):

ah ok, no worries :)

lqd (Nov 19 2019 at 13:24, on Zulip):

(and thanks)

lqd (Nov 19 2019 at 13:24, on Zulip):

I'll check with Niko later, the hackathon should start again real soon

lqd (Nov 19 2019 at 13:40, on Zulip):

ah but maybe it's closer to the ConstraintGraph than this

nikomatsakis (Nov 19 2019 at 14:07, on Zulip):

Hey @lqd

lqd (Nov 19 2019 at 14:07, on Zulip):

hello :)

nikomatsakis (Nov 19 2019 at 14:07, on Zulip):

Do you mean that you are trying to generate the known_subset facts?

lqd (Nov 19 2019 at 14:07, on Zulip):

yes

lqd (Nov 19 2019 at 14:08, on Zulip):

I think I got the placeholder loans done correctly, and was trying to do the known_subsets

nikomatsakis (Nov 19 2019 at 14:08, on Zulip):

OK, one sec, let me point you at the right place

lqd (Nov 19 2019 at 14:09, on Zulip):

yay :) thanks

nikomatsakis (Nov 19 2019 at 14:11, on Zulip):

@lqd so the thing we want is the universal_region_relations

nikomatsakis (Nov 19 2019 at 14:11, on Zulip):

and in particular the outlives field

lqd (Nov 19 2019 at 14:12, on Zulip):

yeah that was I was looking at earlier

nikomatsakis (Nov 19 2019 at 14:12, on Zulip):

it seems like the TransitiveRelation type doesn't have a way to "iterate" over the core relations

lqd (Nov 19 2019 at 14:12, on Zulip):

but it seemed like there was only a way to check if a regionvid pair was a known subset but not iterate over all known ones

nikomatsakis (Nov 19 2019 at 14:13, on Zulip):

yes, that's correct, but we could add one

nikomatsakis (Nov 19 2019 at 14:13, on Zulip):

we basically want to expose the edges field

nikomatsakis (Nov 19 2019 at 14:13, on Zulip):

maybe add a method like this

nikomatsakis (Nov 19 2019 at 14:14, on Zulip):
    pub fn edges(&self) -> impl Iterator<Item=(&T, &T)> {
        self.edges
            .iter()
            .map(|edge| (&self.elements[edge.source], &self.elements[edge.target]))
    }
lqd (Nov 19 2019 at 14:14, on Zulip):

ah yes seems straightforward

nikomatsakis (Nov 19 2019 at 14:14, on Zulip):

(with a suitable comment)

nikomatsakis (Nov 19 2019 at 14:14, on Zulip):

in particular to clarify that this does not give the transitive relation

nikomatsakis (Nov 19 2019 at 14:14, on Zulip):

maybe a name like kernel_edges or something

nikomatsakis (Nov 19 2019 at 14:15, on Zulip):

I guess "edge" is a funny name

nikomatsakis (Nov 19 2019 at 14:15, on Zulip):

takes a very graph-like view

nikomatsakis (Nov 19 2019 at 14:15, on Zulip):

but anyway you get the idea

lqd (Nov 19 2019 at 14:15, on Zulip):

yeah :) thanks !

lqd (Nov 19 2019 at 14:16, on Zulip):

it could be confusing that this method of TransitiveRelation does not give transitive results if the naming/doc is not very clear

nikomatsakis (Nov 19 2019 at 14:16, on Zulip):

exactly, but I think with suitable naming it seems fine

lqd (Nov 19 2019 at 14:18, on Zulip):

yeah :)

lqd (Nov 19 2019 at 15:43, on Zulip):

progress, it seems to generate both placeholders and known_subsets facts

lqd (Nov 19 2019 at 15:48, on Zulip):

ofc it didn't magically fix DatafrogOpt apparently not computing the subset errors (leaning more and more towards your idea of forgetting it for a while Niko ;)

nikomatsakis (Nov 19 2019 at 16:53, on Zulip):

@lqd I'm going crazy renaming things

nikomatsakis (Nov 19 2019 at 16:53, on Zulip):

some of these names I don't like

nikomatsakis (Nov 19 2019 at 16:53, on Zulip):
known_placeholder_subset
nikomatsakis (Nov 19 2019 at 16:54, on Zulip):

e.g. I don't think that's right, but I think it should have the term placeholder in it somehow

lqd (Nov 19 2019 at 16:54, on Zulip):

it's true that it's missing

lqd (Nov 19 2019 at 16:54, on Zulip):

otherwise it's too close to the regular subset relation

nikomatsakis (Nov 19 2019 at 16:54, on Zulip):

if it were me it'd be

nikomatsakis (Nov 19 2019 at 16:54, on Zulip):

nikomatsakis (Nov 19 2019 at 16:54, on Zulip):
placeholder_known_to_contain
nikomatsakis (Nov 19 2019 at 16:55, on Zulip):

but I sometimes get pushback for my wordy names :)

lqd (Nov 19 2019 at 16:55, on Zulip):

it's not that bad !

nikomatsakis (Nov 19 2019 at 16:55, on Zulip):

placeholder_origin_known_to_contain

lqd (Nov 19 2019 at 16:55, on Zulip):

:)

nikomatsakis (Nov 19 2019 at 16:56, on Zulip):

it doesn't quite work for subset

nikomatsakis (Nov 19 2019 at 16:56, on Zulip):

placeholder_known_to_be_subset is awkward even for me

nikomatsakis (Nov 19 2019 at 16:56, on Zulip):

I guess known_placeholder_subset is ok

lqd (Nov 19 2019 at 16:56, on Zulip):

yeah it's still short but conveys the same info

lqd (Nov 19 2019 at 16:58, on Zulip):

I was once toying around with declared as a replacement for known

nikomatsakis (Nov 19 2019 at 16:58, on Zulip):

mm I like that

nikomatsakis (Nov 19 2019 at 16:58, on Zulip):

to really fit our new conventions

nikomatsakis (Nov 19 2019 at 16:58, on Zulip):

subset should probably be subset_on_entry or something

nikomatsakis (Nov 19 2019 at 16:59, on Zulip):

argh, I have to run, I'll try to finish up the ones I'm doing now

nikomatsakis (Nov 19 2019 at 16:59, on Zulip):

the hackmd is basically done modulo naming tweaks I think

nikomatsakis (Nov 19 2019 at 16:59, on Zulip):

it includes the liveness/init rules from @Albin Stjerna's branch

lqd (Nov 19 2019 at 16:59, on Zulip):

nice ! sorry I wasn't able to follow much (if any) of what was going on :/

nikomatsakis (Nov 19 2019 at 16:59, on Zulip):

which I effectively reviewed, I guess

lqd (Nov 19 2019 at 16:59, on Zulip):

I've seen you two have made a lot of concrete progress and that's awesome

lqd (Nov 19 2019 at 17:02, on Zulip):

I'm myself trying to emit subset_errors in check_universal_regions rn

nikomatsakis (Nov 19 2019 at 17:02, on Zulip):

nice

lqd (Nov 19 2019 at 17:03, on Zulip):

I was bit by the variants again (in that the default, Hybrid doesn't compute subset errors) ;)

nikomatsakis (Nov 19 2019 at 17:04, on Zulip):

heh

nikomatsakis (Nov 19 2019 at 17:04, on Zulip):

yeah this is why I wanted to try and pull back to fewer variants

lqd (Nov 19 2019 at 17:06, on Zulip):

and we haven't even landed the equality one yet

lqd (Nov 19 2019 at 17:07, on Zulip):

(or a reworking of the Naive rules towards that model, ofc)

nikomatsakis (Nov 19 2019 at 17:09, on Zulip):

ok, I gotta run for today I think

lqd (Nov 19 2019 at 17:10, on Zulip):

:wave:

lqd (Nov 19 2019 at 17:10, on Zulip):

cheers Niko, thanks for today

lqd (Nov 19 2019 at 18:13, on Zulip):

haha my lone example emits subset errors, we'll see how it fares over the ui tests

nikomatsakis (Nov 19 2019 at 18:49, on Zulip):

nice!

lqd (Nov 19 2019 at 19:15, on Zulip):

tbf it’s all thanks to you, your notes were spot on

lqd (Nov 19 2019 at 19:19, on Zulip):

assuming the ui tests work out, and if we say let’s focus on the naive rules first, we could merge the polonius side tomorrow and publish a new version, to quickly update the rustc branch and open the rustc-side PR for review

nikomatsakis (Nov 19 2019 at 19:21, on Zulip):

awesome!

nikomatsakis (Nov 19 2019 at 19:21, on Zulip):

glad the notes were helpful :)

lqd (Nov 19 2019 at 22:52, on Zulip):

I don't have access to the machine running the ui tests now, but I think the work we mentioned for the polonius side has been done. So I've pushed everything and marked https://github.com/rust-lang/polonius/pull/137 as ready for review: all the new work following the previous review starts at commit 8ecd7ff (so around 12 commits), and with a slight summary in this comment

nikomatsakis (Nov 19 2019 at 23:04, on Zulip):

@lqd :tada:

lqd (Nov 19 2019 at 23:05, on Zulip):

well, we still need to see the results of the ui tests :)

lqd (Nov 19 2019 at 23:06, on Zulip):

but progress yay

lqd (Nov 19 2019 at 23:08, on Zulip):

(bringing at least some of the ui tests as datasets + unit tests in the polonius repo maybe also be a good idea)

Albin Stjerna (Nov 20 2019 at 08:02, on Zulip):

(bringing at least some of the ui tests as datasets + unit tests in the polonius repo maybe also be a good idea)

I think I have some of them already, but I've found it a bit hard to make unit tests out of code examples. I think that's also an important focus for the future; fixing test ergonomics

Albin Stjerna (Nov 20 2019 at 08:03, on Zulip):

I'd like testing to be where I can type cargo test and be pretty sure I didn't break anything if they pass

lqd (Nov 20 2019 at 08:13, on Zulip):

I mean specifically bringing ones testing subset errors

lqd (Nov 20 2019 at 08:16, on Zulip):

I've made a couple tries in this PR at some of the ergonomics I had writing tests (and no tries at reorg but we'll need to do it as well), some of https://github.com/rust-lang/polonius/pull/137/files?file-filters%5B%5D=.rs#diff-c5fc4beef0f03493c2e9a9c876073f0fR589-R615 seem easily extensible to more of our use cases, what do you think ?

Albin Stjerna (Nov 20 2019 at 08:17, on Zulip):

NB the things I have been working on doesn't even have support in polonius-parser yet err

lqd (Nov 20 2019 at 08:17, on Zulip):

(we also need to remove some of the existing inputs, I'm not sure they're all super useful)

Albin Stjerna (Nov 20 2019 at 08:18, on Zulip):

Haha honestly I didn't look at the test changes :)

Albin Stjerna (Nov 20 2019 at 08:20, on Zulip):

But it looks good!

lqd (Nov 20 2019 at 08:21, on Zulip):

the ones testing an ./inputs dataset are a bit tedious to write for sure https://github.com/rust-lang/polonius/pull/137/files?file-filters%5B%5D=.rs#diff-c5fc4beef0f03493c2e9a9c876073f0fR638-R666 so I'm not sure about those, but matches your experience, we'll have to work out a way of making them a bit easier to test I totally agree

Albin Stjerna (Nov 20 2019 at 08:21, on Zulip):

It's even worse with liveness and still worse with move paths

Albin Stjerna (Nov 20 2019 at 08:21, on Zulip):

I'm not even sure how to represent those

lqd (Nov 20 2019 at 08:22, on Zulip):

there's a lot of desugaring and interning layers between what we're expressing in the initial rust test code and the data available to us

lqd (Nov 20 2019 at 08:23, on Zulip):

maybe some mix of using the parser to lower what we mean, and looking for that somehow in the existing data I dunno, but yeah you've mentioned before it's a bit tough, and not just ergonomically

lqd (Nov 20 2019 at 08:24, on Zulip):

it seems like an important topic to tackle as part of the correctness push in any case

Albin Stjerna (Nov 20 2019 at 08:26, on Zulip):

Yes!

lqd (Nov 20 2019 at 08:32, on Zulip):

(maybe we could also use a combination of the nll facts and a -Zdump-mir=polonius which can contain some of the data in the richer form usable in tests, e.g. user-facing origin names; or in some cases, also having some of rustc's machinery for comparing the user-facing compiler output, messages and errors, rather than only polonius output; additionally CI could also try to always run rustc tests as well)

Albin Stjerna (Nov 20 2019 at 08:39, on Zulip):

The rustc CI tests will definitely be easier to run automatically once we have a somewhat stable API against rustc

lqd (Nov 20 2019 at 10:05, on Zulip):

ui tests results: 14 failures, some seem easy, I'll push the blessed tests in a bit

lqd (Nov 20 2019 at 10:10, on Zulip):

there are a 6 cases of "test x has been running for over 60 seconds" (but that's probably just the Naive variant, rather than subset errors per se; and some of cases could also be related to fact generation especially the OOM-happy materializing of subsets at all points in the cfg)

lqd (Nov 20 2019 at 11:14, on Zulip):

to put that in perspective until I upload the blessed output, using the Hybrid variant which doesn't compute subset errors:

lqd (Nov 20 2019 at 11:42, on Zulip):

pushed https://github.com/lqd/rust/tree/placeholder_loans, blessed output for the 14 failures here but better seen as this .stderr to .polonius.stderr diff https://gist.github.com/lqd/7b43ac553f4a27041ca3960e6c5aea70. Some of the lifetime notes are duplicated (10 of the 14 failures), there's of course a special casing for 'static that current polonius errors ignore, etc. Not so bad imo.

nikomatsakis (Nov 20 2019 at 14:04, on Zulip):

Re: testing, I think y'all were saying that the "unit test" premise of polonius doesn't quite seem to be living up to its potential?

nikomatsakis (Nov 20 2019 at 14:04, on Zulip):

If so, I agree

nikomatsakis (Nov 20 2019 at 14:04, on Zulip):

it feels like we should be able to write smaller, targeted tests

nikomatsakis (Nov 20 2019 at 14:10, on Zulip):

@lqd let me take a look

nikomatsakis (Nov 20 2019 at 14:10, on Zulip):

it sounded like it was plausible to remove the datafrog-opt and friends

nikomatsakis (Nov 20 2019 at 14:10, on Zulip):

from what you said

nikomatsakis (Nov 20 2019 at 14:10, on Zulip):

we could for the time being add skip-polonius annotations to the tests that are timing out and try to address them separately

lqd (Nov 20 2019 at 14:10, on Zulip):

yeah, or redirect them all to Naive

nikomatsakis (Nov 20 2019 at 14:11, on Zulip):

I don't understand 'redirect them all..' oh, you mean in polonius

lqd (Nov 20 2019 at 14:11, on Zulip):

yeah

nikomatsakis (Nov 20 2019 at 14:11, on Zulip):

yeah, that would be ok too

lqd (Nov 20 2019 at 14:11, on Zulip):

the big materializing of subset relations is going to be the more annoying part of this all endeavour

lqd (Nov 20 2019 at 14:12, on Zulip):

(which we/I might have referred to as the Location::All hack)

nikomatsakis (Nov 20 2019 at 14:17, on Zulip):

hmm

nikomatsakis (Nov 20 2019 at 14:17, on Zulip):

yes, I want to get rid of Location::All

nikomatsakis (Nov 20 2019 at 14:17, on Zulip):

I totally forget what made that hard

nikomatsakis (Nov 20 2019 at 14:18, on Zulip):

I remember I had a branch that did so but it had a few problems

nikomatsakis (Nov 20 2019 at 14:18, on Zulip):

remind me, @lqd, are we doing that in rustc now?

lqd (Nov 20 2019 at 14:18, on Zulip):

it's this right ?

nikomatsakis (Nov 20 2019 at 14:23, on Zulip):

looks right

nikomatsakis (Nov 20 2019 at 14:23, on Zulip):

@lqd I'm reading your branch now, it looks quite good

lqd (Nov 20 2019 at 14:23, on Zulip):

(and one of the reasons why anything "everywhere in the CFG" scares me a bit ;) even rustc tests, which could generally be seen as small-ish, have hundreds of thousands of outlives constraints, over dozens of thousands of cfg nodes; -- and I'm not even talking about macro heavy code we see in the while but have some stats on)

lqd (Nov 20 2019 at 14:24, on Zulip):

are you reading the rustc branch or the polonius PR ?

nikomatsakis (Nov 20 2019 at 14:29, on Zulip):

rustc branch

nikomatsakis (Nov 20 2019 at 14:29, on Zulip):

@lqd yeah we should maybe take some time to review a beter way to handle "outlives-all"

nikomatsakis (Nov 20 2019 at 14:29, on Zulip):

I mean for one thing

nikomatsakis (Nov 20 2019 at 14:29, on Zulip):

we could incorporate it into the rules readily enough

nikomatsakis (Nov 20 2019 at 14:30, on Zulip):

though with a bit of .. duplication

nikomatsakis (Nov 20 2019 at 14:30, on Zulip):

e.g., it's basically a a; b sort of thing

nikomatsakis (Nov 20 2019 at 14:30, on Zulip):

the same thing we did with placeholder

nikomatsakis (Nov 20 2019 at 14:30, on Zulip):

but I don't love this sol'n

lqd (Nov 20 2019 at 14:30, on Zulip):

I thought about that but was hoping it wouldn't just move the OOM from fact generation in rustc, to polonius

nikomatsakis (Nov 20 2019 at 14:30, on Zulip):

yes, exactly

lqd (Nov 20 2019 at 14:30, on Zulip):

including via equal origins (which most of these are)

nikomatsakis (Nov 20 2019 at 14:31, on Zulip):

the rustc changes look good

nikomatsakis (Nov 20 2019 at 14:31, on Zulip):

I didn't review the "--bless" output

nikomatsakis (Nov 20 2019 at 14:31, on Zulip):

I guess I should look at the specific test you mentioned?

nikomatsakis (Nov 20 2019 at 14:31, on Zulip):

including via equal origins (which most of these are)

yes

nikomatsakis (Nov 20 2019 at 14:31, on Zulip):

I think we sohuld put off discussing this until we talk about equal

nikomatsakis (Nov 20 2019 at 14:32, on Zulip):

which I suspect we won't quite get to today but that's ok

lqd (Nov 20 2019 at 14:32, on Zulip):

a couple tests are interesting yeah

nikomatsakis (Nov 20 2019 at 14:32, on Zulip):

you mentioned some of the higher ranked tests?

lqd (Nov 20 2019 at 14:32, on Zulip):

yeah the hrtb perfect forwarding case

lqd (Nov 20 2019 at 14:32, on Zulip):

which "loses" an error

lqd (Nov 20 2019 at 14:34, on Zulip):

(the others seem either due to the fact that we might push many duplicate subset errors, because they're propagated along the cfg so we have one at all points where the placeholder loan flowed into an unexpected placeholder; or some behaviour tailored to 'static)

nikomatsakis (Nov 20 2019 at 14:34, on Zulip):

looking

lqd (Nov 20 2019 at 14:34, on Zulip):

eg https://gist.github.com/lqd/7b43ac553f4a27041ca3960e6c5aea70#file-hrtb-perfect-forwarding-polonius-diff

lqd (Nov 20 2019 at 14:35, on Zulip):

(if you scroll quickly through the gist you'll see the 10 out of 14 failures being duplicate notes)

nikomatsakis (Nov 20 2019 at 14:35, on Zulip):

hmm

nikomatsakis (Nov 20 2019 at 14:36, on Zulip):

I'm a bit confused

nikomatsakis (Nov 20 2019 at 14:36, on Zulip):

looking at hrtb-perfect-forwarding.rs

nikomatsakis (Nov 20 2019 at 14:36, on Zulip):

I see only one ERROR annotation

nikomatsakis (Nov 20 2019 at 14:36, on Zulip):

and I see one ERROR in the output in your branch

nikomatsakis (Nov 20 2019 at 14:37, on Zulip):

basically the .polonius output looks the same as what I see as .nll output

lqd (Nov 20 2019 at 14:37, on Zulip):

(link is https://github.com/lqd/rust/blob/2fce903fa86d1ca37f155d08367116fd150eb3a8/src/test/ui/hrtb/hrtb-perfect-forwarding.rs if anyone needs it)

nikomatsakis (Nov 20 2019 at 14:37, on Zulip):

oh

nikomatsakis (Nov 20 2019 at 14:37, on Zulip):

ok ok

nikomatsakis (Nov 20 2019 at 14:37, on Zulip):

now I see :)

nikomatsakis (Nov 20 2019 at 14:37, on Zulip):

I should've clicked your link

nikomatsakis (Nov 20 2019 at 14:38, on Zulip):

hmm that is a bit curious

nikomatsakis (Nov 20 2019 at 14:38, on Zulip):

do you know @lqd what the "error tuples" we get out are?

nikomatsakis (Nov 20 2019 at 14:38, on Zulip):

(or the input tuples)

nikomatsakis (Nov 20 2019 at 14:39, on Zulip):

/me thinks

lqd (Nov 20 2019 at 14:39, on Zulip):

no but I can find out

nikomatsakis (Nov 20 2019 at 14:39, on Zulip):

ok so

nikomatsakis (Nov 20 2019 at 14:39, on Zulip):

I think I know why this is

nikomatsakis (Nov 20 2019 at 14:39, on Zulip):

in short, I think it's because we have to fix the "other side"

nikomatsakis (Nov 20 2019 at 14:39, on Zulip):

in other words, I want this setup where chalk ahndles the higher-ranked stuff

nikomatsakis (Nov 20 2019 at 14:39, on Zulip):

but right now, some of that work is being pushed to region solving

nikomatsakis (Nov 20 2019 at 14:39, on Zulip):

and polonius is not able to handle it

lqd (Nov 20 2019 at 14:39, on Zulip):

I was expecting something like this with this case

nikomatsakis (Nov 20 2019 at 14:39, on Zulip):

(and rightly so)

lqd (Nov 20 2019 at 14:42, on Zulip):

maybe it means the time to experiment with this in chalk is sooner than expected :/

nikomatsakis (Nov 20 2019 at 14:42, on Zulip):

yeah, I think the behavior here is expected, and the main question is how to "record it" so we dn't forget about it

nikomatsakis (Nov 20 2019 at 14:42, on Zulip):

I actually started some of that experimentation

nikomatsakis (Nov 20 2019 at 14:42, on Zulip):

but I've not gotten very far

nikomatsakis (Nov 20 2019 at 14:42, on Zulip):

the interesting question is whether I can do some of that in rustc, too

lqd (Nov 20 2019 at 14:43, on Zulip):

in lambda prolog you mean, or chalk ?

nikomatsakis (Nov 20 2019 at 14:43, on Zulip):

no, in chalk, just a bit over the last few mornings

lqd (Nov 20 2019 at 14:43, on Zulip):

nice :)

lqd (Nov 20 2019 at 14:43, on Zulip):

we could ignore this test in the polonius compare mode, maybe get the .facts i the polonius repo

nikomatsakis (Nov 20 2019 at 14:44, on Zulip):

yes, that seems good

lqd (Nov 20 2019 at 14:44, on Zulip):

or just bless the output and have some issues in the polonius repo

nikomatsakis (Nov 20 2019 at 14:44, on Zulip):

well, hmm

nikomatsakis (Nov 20 2019 at 14:44, on Zulip):

in general I do not like "ignoring" tests

nikomatsakis (Nov 20 2019 at 14:44, on Zulip):

I might rather open an issue on the polonius repo or something

nikomatsakis (Nov 20 2019 at 14:44, on Zulip):

or just bless the output and have some issues in the polonius repo

er, yes, that

lqd (Nov 20 2019 at 14:44, on Zulip):

because other blessed output will need to be reviewed by the time we are finished, like we had to do with nlls

nikomatsakis (Nov 20 2019 at 14:44, on Zulip):

"les great rendesvous" or whatever french people say :P

lqd (Nov 20 2019 at 14:44, on Zulip):

(rn it's mostly diagnostics ofc)

lqd (Nov 20 2019 at 14:44, on Zulip):

lol

nikomatsakis (Nov 20 2019 at 14:45, on Zulip):

I forget the phrase, though I've heard it...

lqd (Nov 20 2019 at 14:45, on Zulip):

les grands esprits se rencontrent ?

lqd (Nov 20 2019 at 14:45, on Zulip):

(great minds think alike)

nikomatsakis (Nov 20 2019 at 14:45, on Zulip):

that's the one

lqd (Nov 20 2019 at 14:46, on Zulip):

:)

nikomatsakis (Nov 20 2019 at 14:46, on Zulip):

anyway I like opening issues

lqd (Nov 20 2019 at 14:46, on Zulip):

let's do this for this test

nikomatsakis (Nov 20 2019 at 14:46, on Zulip):

ignoring tests are "... too quiet"

nikomatsakis (Nov 20 2019 at 14:46, on Zulip):

easily forgotten

nikomatsakis (Nov 20 2019 at 14:46, on Zulip):

plus it's good to know if the output changes more

lqd (Nov 20 2019 at 14:46, on Zulip):

and we'll need some for higher ranked subtyping I assume, at the very least to test it....

lqd (Nov 20 2019 at 14:47, on Zulip):

a couple of the other failures are related to 'static, eg the first 2: https://gist.github.com/lqd/7b43ac553f4a27041ca3960e6c5aea70#file-closure-substs-polonius-diff and https://gist.github.com/lqd/7b43ac553f4a27041ca3960e6c5aea70#file-error-handling-polonius-diff

nikomatsakis (Nov 20 2019 at 14:47, on Zulip):

yeah I saw you said you suspected something about 'static

lqd (Nov 20 2019 at 14:48, on Zulip):

yeah, in another context, I added some assertions to rustc checking errors in the polonius output (illegal acess errors, not subset ones)

lqd (Nov 20 2019 at 14:48, on Zulip):

and it seemed like polonius was finding errors, maybe it was about statics/consts

lqd (Nov 20 2019 at 14:49, on Zulip):

but rustc wasn't asking for those in the output so that was weird: no rustc errors, and still polonius computed error tuples

lqd (Nov 20 2019 at 14:49, on Zulip):

so I'll definitely want to revisit this later

lqd (Nov 20 2019 at 14:49, on Zulip):

in today's cases however it seem mostly related to origins which outlive 'static ?

lqd (Nov 20 2019 at 14:50, on Zulip):

(or _are_ 'static)

lqd (Nov 20 2019 at 14:52, on Zulip):

I'm not sure if those should emit a subset error with ReStatic or something ?

nikomatsakis (Nov 20 2019 at 14:54, on Zulip):

those diffs

nikomatsakis (Nov 20 2019 at 14:54, on Zulip):

I'm not 100% sure what to make of them

nikomatsakis (Nov 20 2019 at 14:55, on Zulip):

in the first case, there is an extra error, right?

nikomatsakis (Nov 20 2019 at 14:55, on Zulip):

two extra errors

nikomatsakis (Nov 20 2019 at 14:55, on Zulip):

the first error does not look wrong to me

nikomatsakis (Nov 20 2019 at 14:55, on Zulip):

in other words

nikomatsakis (Nov 20 2019 at 14:55, on Zulip):
--- ./src/test/ui/nll/user-annotations/closure-substs.stderr    2019-04-23 15:38:28.770932800 +0200
+++ ./src/test/ui/nll/user-annotations/closure-substs.polonius.stderr   2019-11-20 12:16:21.782801300 +0100
@@ -16,6 +16,16 @@
    |                ^ returning this value requires that `'1` must outlive `'static`

 error: lifetime may not live long enough
+  --> $DIR/closure-substs.rs:15:16
+   |
+LL |     |x: &i32| -> &'static i32 {
+   |         -        ------------ return type of closure is &'2 i32
+   |         |
+   |         let's call the lifetime of this reference `'1`
+LL |         return x;
+   |                ^ returning this value requires that `'1` must outlive `'2`
+
+error: lifetime may not live long enough
   --> $DIR/closure-substs.rs:22:9
    |
nikomatsakis (Nov 20 2019 at 14:56, on Zulip):

this hunk seems "reasonable"

nikomatsakis (Nov 20 2019 at 14:56, on Zulip):

i.e., the problem is probably more in error reporting or duplicate detection

nikomatsakis (Nov 20 2019 at 14:56, on Zulip):

I guess the same with this one

nikomatsakis (Nov 20 2019 at 14:56, on Zulip):
+error[E0521]: borrowed data escapes outside of closure
+  --> $DIR/closure-substs.rs:29:9
+   |
+LL |     |x: &i32, b: fn(&'static i32)| {
+   |      -        - `b` is declared here, outside of the closure body
+   |      |
+   |      `x` is a reference that is only valid in the closure body
+LL |         b(x);
+   |         ^^^^ `x` escapes the closure body here
+
+error: aborting due to 6 previous errors
nikomatsakis (Nov 20 2019 at 14:56, on Zulip):

like, the error as described is ... wrong, but it's "kind of right"

lqd (Nov 20 2019 at 14:57, on Zulip):

here are the first test original stderrs https://github.com/lqd/rust/blob/2fce903fa86d1ca37f155d08367116fd150eb3a8/src/test/ui/nll/user-annotations/closure-substs.stderr vs https://github.com/lqd/rust/blob/2fce903fa86d1ca37f155d08367116fd150eb3a8/src/test/ui/nll/user-annotations/closure-substs.polonius.stderr

nikomatsakis (Nov 20 2019 at 14:57, on Zulip):

i.e., at that spot, the lifetime of x is being related to 'static, and I suspect polonius is reporting the right thing, but we're reporting it in a bogus way

nikomatsakis (Nov 20 2019 at 14:58, on Zulip):

I'm not totally sure what's up with the error-handling test, that .. hmm. That is going through a complex path for sure.

lqd (Nov 20 2019 at 14:58, on Zulip):

yeah I was thinking that polonius was reporting an error related to the renumbered/freshened region

nikomatsakis (Nov 20 2019 at 14:58, on Zulip):

yeah I was thinking that polonius was reporting an error related to the renumbered/freshened region

in the closure-substs test?

lqd (Nov 20 2019 at 14:58, on Zulip):

but rustc usually wouldn't maybe do that in diagnostics or something

lqd (Nov 20 2019 at 14:58, on Zulip):

yes

nikomatsakis (Nov 20 2019 at 14:59, on Zulip):

but rustc usually wouldn't maybe do that in diagnostics or something

yeah Ithink it's a case of doing a slightly different thing than rustc does

nikomatsakis (Nov 20 2019 at 14:59, on Zulip):

and our diagnostic handling not being tuned for that

nikomatsakis (Nov 20 2019 at 14:59, on Zulip):

but not a wrong thing

lqd (Nov 20 2019 at 14:59, on Zulip):

eg rustc would emit restatic in this case but polonius emits the '2 for the same error

lqd (Nov 20 2019 at 14:59, on Zulip):

yeah agreed

nikomatsakis (Nov 20 2019 at 14:59, on Zulip):

the other test--

nikomatsakis (Nov 20 2019 at 14:59, on Zulip):

let me go look at it

nikomatsakis (Nov 20 2019 at 14:59, on Zulip):

we definitely added some custom logic around impl trait with mutiple, unrelated lifetimes

lqd (Nov 20 2019 at 14:59, on Zulip):

probably more about diagnostics and expectations than bugs in polonius

nikomatsakis (Nov 20 2019 at 15:00, on Zulip):

egads that test :)

nikomatsakis (Nov 20 2019 at 15:00, on Zulip):
fn foo<'a, 'b, 'c>(x: &'static i32, mut y: &'a i32) -> E<'b, 'c> {
    //~^ ERROR lifetime may not live long enough
    let v = CopyIfEq::<*mut _, *mut _>(&mut {x}, &mut y);
    let u = v;
    let _: *mut &'a i32 = u.1;
    unsafe { let _: &'b i32 = *u.0; }
    u.0
}
lqd (Nov 20 2019 at 15:01, on Zulip):

the other test

diff https://gist.github.com/lqd/7b43ac553f4a27041ca3960e6c5aea70#file-error-handling-polonius-diff
nll https://github.com/lqd/rust/blob/2fce903fa86d1ca37f155d08367116fd150eb3a8/src/test/ui/impl-trait/multiple-lifetimes/error-handling.stderr
polonius https://github.com/lqd/rust/blob/2fce903fa86d1ca37f155d08367116fd150eb3a8/src/test/ui/impl-trait/multiple-lifetimes/error-handling.polonius.stderr

nikomatsakis (Nov 20 2019 at 15:01, on Zulip):

I remember this being a very carefully crafted bit of code now :)

nikomatsakis (Nov 20 2019 at 15:01, on Zulip):

probably by @Matthew Jasper

lqd (Nov 20 2019 at 15:02, on Zulip):

probably you :)

lqd (Nov 20 2019 at 15:03, on Zulip):

ah and it's about existential type

nikomatsakis (Nov 20 2019 at 15:04, on Zulip):

yeah so this has tod o with those MemberConstraint things we added

nikomatsakis (Nov 20 2019 at 15:04, on Zulip):

obviously polonius knows nothing about them

nikomatsakis (Nov 20 2019 at 15:04, on Zulip):

I thnk that's prob ok but I'm trying to bring it a bit back in cache ;)

nikomatsakis (Nov 20 2019 at 15:05, on Zulip):

well I suspect this may be something where we want to file an issue and do follow-up

lqd (Nov 20 2019 at 15:05, on Zulip):

alright, that I can do

lqd (Nov 20 2019 at 15:06, on Zulip):

for the other duplicated diagnostics notes, I wonder if we should just emit one subset error, since we're not using the cfg node where it happens rn

nikomatsakis (Nov 20 2019 at 15:07, on Zulip):

ok, I sort of remember now

lqd (Nov 20 2019 at 15:07, on Zulip):

I'll need to look whether check_universal_regions does emit only one such error per unique, not known, free region pair

nikomatsakis (Nov 20 2019 at 15:08, on Zulip):

I definitely think we should leave this for follow-up work

nikomatsakis (Nov 20 2019 at 15:08, on Zulip):

but I do think we may have to do something

lqd (Nov 20 2019 at 15:08, on Zulip):

wrt the member constraints you mean ?

nikomatsakis (Nov 20 2019 at 15:08, on Zulip):

correct

nikomatsakis (Nov 20 2019 at 15:09, on Zulip):

But I also remember thinking that some of the problems here

nikomatsakis (Nov 20 2019 at 15:09, on Zulip):

Got easier in Polonius's model

lqd (Nov 20 2019 at 15:09, on Zulip):

I was sorta hoping we wouldn't have to do anything heh

nikomatsakis (Nov 20 2019 at 15:09, on Zulip):

Though damned if I remember why :)

lqd (Nov 20 2019 at 15:09, on Zulip):

:)

nikomatsakis (Nov 20 2019 at 15:09, on Zulip):

Well it had to do with the way that polonius origins are sets of loans

nikomatsakis (Nov 20 2019 at 15:09, on Zulip):

and the fact that union was a relatively easy concept for us to express

lqd (Nov 20 2019 at 15:09, on Zulip):

that's very true

lqd (Nov 20 2019 at 15:10, on Zulip):

so maybe we have to do something, but it wouldn't be that big

nikomatsakis (Nov 20 2019 at 15:11, on Zulip):

@lqd I had to run but will be back in a bit

nikomatsakis (Nov 20 2019 at 15:11, on Zulip):

so far I think gthis all looks great and we should move forward to landing :)

lqd (Nov 20 2019 at 15:11, on Zulip):

alright :)

lqd (Nov 20 2019 at 15:12, on Zulip):

awesome

lqd (Nov 20 2019 at 15:12, on Zulip):

I'll take care of what's missing in the rustc branch

lqd (Nov 20 2019 at 15:12, on Zulip):

(that'll require checking/landing the polonius PR as well ofc)

lqd (Nov 20 2019 at 15:13, on Zulip):

rn I'm looking at the filtering we mentioned yesterday, and adapting to support placeholder loans, I think I'm close-ish

lqd (Nov 20 2019 at 17:28, on Zulip):

(for subset errors whitelisting all placeholders does the trick, even though I'm sure we could tighten this a bit more to only check some placeholders which are not in known_subset, and their loans, etc. the ui tests pass equally well, and on this 8-core machine, clock in at 20mins even with the 6 slow/alloc-heavy tests (this filtering doesn't change those, since it's likely in fact gen, and the filtering is done in polonius instead of rustc) and that was overall similar to the optimized variant)

lqd (Nov 20 2019 at 17:31, on Zulip):

(in the same vein, and as I said before, I also applied this to liveness (to limit to "interesting vars", the ones whose uses/drops can derefs these interesting origins) and rustc tests also pass, in around 19mins once again)

lqd (Nov 20 2019 at 17:34, on Zulip):

(and if the 2 finished in XXX at the end of the compare mode tests are indeed the run-times of both modes, on this machine the polonius one is around 1.8x)

lqd (Nov 20 2019 at 17:51, on Zulip):

the subtlety of this (much like the propagation of placeholder loans along the CFG wrt dead code) may also not be particularly covered by all our tests, but if that's interesting to you @nikomatsakis well: https://github.com/lqd/borrow-check/commits/thats_interesting

lqd (Nov 20 2019 at 17:56, on Zulip):

and last time I checked this (and now I'd need to regen the placeholder facts) this takes clap from 9-10s to 600ms (which is in the LocationInsensitive territory)

lqd (Nov 20 2019 at 18:25, on Zulip):

ah I see the duplicate regions relations in the rustc branch are only when using#[rustc_regions], so while I can deduplicate the subset errors in the polonius equivalent of check_universal_regions (and indeed I have locally), should I @nikomatsakis ? (or just bless as-is, and create an issue to look at this rustc-internal debug output later)

lqd (Nov 20 2019 at 18:27, on Zulip):

(sorry for pinging you btw -- I'll get dinner and finalize this later then)

lqd (Nov 21 2019 at 09:53, on Zulip):

(I vote "no": bless the stderrs as-is, and will file an issue and fix #[rustc_regions] later)

Albin Stjerna (Nov 21 2019 at 13:30, on Zulip):

I'll take care of what's missing in the rustc branch

I'm not looking forward to how much this will likely clash with my changes to rustc, but I'm ready for a rebase-party

lqd (Nov 21 2019 at 13:38, on Zulip):

these rustc changes are all in all pretty minimal so it shouldn't clash a lot (or at all, hopefully)

Albin Stjerna (Nov 21 2019 at 13:52, on Zulip):

:)

nikomatsakis (Nov 22 2019 at 02:29, on Zulip):

@lqd I don't quite understand what you are asking me I think I'm happy with "just bless and figure it out"

lqd (Nov 22 2019 at 07:14, on Zulip):

it was about the 10 failures which all look like https://gist.github.com/lqd/7b43ac553f4a27041ca3960e6c5aea70#file-escape-upvar-nested-polonius-diff a lot of duplicate notes in the debug output when using #[rustc_regions], but OK :)

lqd (Nov 22 2019 at 07:16, on Zulip):

I'll bless this all with explanations in the commits, and open tracking issues in the polonius repo. We'll just need to land the polonius side, then I can rebase the rustc branch to open a PR

lqd (Nov 23 2019 at 02:27, on Zulip):

(btw, thanks for the review Niko!)

lqd (Nov 23 2019 at 02:47, on Zulip):

I'll update the comments and all, merge+release to open the rustc PR, and then help out Albin where I can

lqd (Nov 23 2019 at 03:02, on Zulip):

(on that note @Albin Stjerna your latest thesis draft is super cool! I've just started reading this one and the improvements you've been doing are great — also thanks for the classy shoutout to the WG — I'll try to have feedback for you)

Albin Stjerna (Nov 23 2019 at 08:21, on Zulip):

@lqd Thank you! Also let me know if you prefer other names than lqd :) I feel a lot better about this version of the thesis than the first one.

lqd (Nov 23 2019 at 09:24, on Zulip):

(up to you re: name, I don't mind — the non-asciiness can be annoying to type hehe, but it's eg here if you want/need it)

Albin Stjerna (Nov 26 2019 at 20:04, on Zulip):

My keyboard handles far worse than that every day :)

Last update: Mar 31 2020 at 02:35UTC