Stream: t-compiler/wg-nll

Topic: borrow-check issue #4


Reed Koser (May 09 2018 at 20:28, on Zulip):

Was there a discussion about how to integrate two-phase borrows into the alias analysis? It's not entirely obvious to me how we should generate invalidate statements without livenss information for them. Right now, that's computed as part of the overall borrow liveness computation, and depends on our existing region inference if I'm remembering that code correctly... which is exactly what the new analysis rips out :sweat_smile:

Reed Koser (May 09 2018 at 20:30, on Zulip):

@nikomatsakis @Santiago Pastorino ^

nikomatsakis (May 09 2018 at 20:31, on Zulip):

the invalidation information should be independent I think

nikomatsakis (May 09 2018 at 20:31, on Zulip):

just based on which paths overlap

nikomatsakis (May 09 2018 at 20:31, on Zulip):

not based on the location at all

nikomatsakis (May 09 2018 at 20:31, on Zulip):

but I gotta run, I'll be back in 15-30 mins

Reed Koser (May 09 2018 at 21:02, on Zulip):

I think it still matters? If we have something like

LOC0: _3 = &'3 mut _1 // this borrow is two phase
LOC1:  _4 = &'4 _1
// do something with _4
// ... _4 dies here
LOC2: call(move _3, ... ) // borrow activates here

Borrowing _1 immutably using _4 needs to still work; but if I'm blindly generating invalidate rules I /think/ we would incorrectly generate an error since we would generate at least 2 invalidates facts:
- i0: invalidates('4, LOC0) because single-phase mutable borrows require all borrows of the same path (or any parent path) to be dead
- i1: invalidates('3, LOC1) because creating this borrow is going to invalidate a single-phase mutable borrow
We also have a region R3 R3 representing the liveness of '3, which has to be live at LOC0, LOC1, and LOC2. Thus we would error at LOC1 since '3 R3 \in R3 but '3 is invalidated by i1. R3 R3 has to contain every point between LOC0 and LOC2 since otherwise bad things might happen to _1 when we aren't looking (e.g. overwriting it, which is illegal today since any write access to _1 or its children would force the activation of '3). All this is assuming I know my borrow checker rules which might not be true :upside_down_face:.

nikomatsakis (May 09 2018 at 21:11, on Zulip):

@Reed Koser I see, yeah good point.

nikomatsakis (May 09 2018 at 21:12, on Zulip):

still, we know whether we are in the "active" region or not

nikomatsakis (May 09 2018 at 21:12, on Zulip):

based solely on the dominator information

nikomatsakis (May 09 2018 at 21:12, on Zulip):

so you could take that into account when considering what "invalidates" perhaps

nikomatsakis (May 09 2018 at 21:12, on Zulip):

/me thinks

nikomatsakis (May 09 2018 at 21:12, on Zulip):

I think that would be true -- the idea would be that the &mut a.b.c would be in error in the first place

nikomatsakis (May 09 2018 at 21:13, on Zulip):

i.e., the initial borrow still invalidates itself, but -- until activation -- only writes to a.b.c violate the loan

nikomatsakis (May 09 2018 at 21:36, on Zulip):

@Reed Koser btw however far you get post your branch if you run out of time. I'll be able to talk more about this tomorrow, I gotta run for tonight.

Reed Koser (May 09 2018 at 21:37, on Zulip):

Sounds good. Using the dominator information should work out I think? I'll definitely push a branch

nikomatsakis (May 10 2018 at 02:27, on Zulip):

This is the branch that removes position information and thus (I believe) speeds up "NLL" while sacrificing precision: https://github.com/rust-lang/rust/pull/50593

Reed Koser (May 10 2018 at 10:08, on Zulip):

Here's what I was able to get done: https://github.com/bobtwinkles/rust/tree/nll_facts_invalidate
It's not complete, probably doesn't compile, and definitely doesn't work but I'm way past out of time today and I'll be spending tomorrow traveling. I think I got most of the boring stuff out of the way for you @Santiago Pastorino, if you want to pick this up and run with it :smile: . You'll need to review check_access_for_conflict in invalidation.rs and add a call to generate_invalidates in nll/mod.rs. Reviewing everything else in there probably wouldn't be the worst idea. As a "nice to have thing", we can probably do better than just iterating over every single borrow every single time we need to check for conflicts. Something like a FxHashMap<Place, Vec<BorrowIndex>> mapping from the root place to a list of the borrows involving that place and its children would probably work well

Reed Koser (May 10 2018 at 10:11, on Zulip):

also the code duplication with the current borrow check hurts me a little, and there should be a way to reduce it

Reed Koser (May 10 2018 at 10:13, on Zulip):

it might be possible to just roll this generation into the existing borrow checking by switching out the implementation of each_borrow_involving_path actually, that might be worth looking into

Reed Koser (May 10 2018 at 10:13, on Zulip):

I was expecting the changes to be more drastic but it appears that won't be the case

Santiago Pastorino (May 10 2018 at 11:48, on Zulip):

@Reed Koser cool, thanks. I told Niko that I wasn't finding time for this, I should be able today or tomorrow

nikomatsakis (May 10 2018 at 11:50, on Zulip):

I haven't had a chance to check out @Reed Koser's branch yet

nikomatsakis (May 11 2018 at 12:56, on Zulip):

it seems like it'd be great to continue on this, @Santiago Pastorino, if you have time today—

nikomatsakis (May 11 2018 at 12:57, on Zulip):

specifically, I was thinking that it'd be really nice to get the borrow-check repo to the point where we can run it on actual files

nikomatsakis (May 11 2018 at 12:57, on Zulip):

and see the errors that result

nikomatsakis (May 11 2018 at 12:57, on Zulip):

i.e., in order to try out examples

nikomatsakis (May 11 2018 at 12:57, on Zulip):

(not to mention the optimization potential)

nikomatsakis (May 11 2018 at 12:57, on Zulip):

my vision was roughly that you give a .rs file

Santiago Pastorino (May 11 2018 at 12:57, on Zulip):

(deleted)

nikomatsakis (May 11 2018 at 12:57, on Zulip):

and we run rustc -Znll-facts, load the facts,

Santiago Pastorino (May 11 2018 at 12:57, on Zulip):

(deleted)

nikomatsakis (May 11 2018 at 12:57, on Zulip):

run our analysis and print errors

nikomatsakis (May 11 2018 at 12:57, on Zulip):

though you could integrate in different ways

nikomatsakis (May 11 2018 at 12:58, on Zulip):

(e.g., rustc could invoke us, instead, or we could be a custom driver)

Santiago Pastorino (May 11 2018 at 12:58, on Zulip):

sorry for those two yes, using with Zulip :P

Santiago Pastorino (May 11 2018 at 12:58, on Zulip):

it seems like it'd be great to continue on this, @Santiago Pastorino, if you have time today—

yes

nikomatsakis (May 11 2018 at 12:58, on Zulip):

but it seems like getting the info from #4 is the first step

Santiago Pastorino (May 11 2018 at 13:00, on Zulip):

:+1:

Reed Koser (May 11 2018 at 19:43, on Zulip):

I'll be around to chat, it's unlikely that I'll have a chance to write code until Monday or Tuesday at the earliest though. So don't worry about duplicate work for now =)

nikomatsakis (May 14 2018 at 13:56, on Zulip):

I think neither @Santiago Pastorino nor I had a chance to even look at the branch yet

nikomatsakis (May 14 2018 at 13:57, on Zulip):

but I was hoping to look at it quickly now

nikomatsakis (May 14 2018 at 13:57, on Zulip):

I guess this is the main commit

Santiago Pastorino (May 14 2018 at 14:02, on Zulip):

:+1:

Santiago Pastorino (May 14 2018 at 14:03, on Zulip):

I'm doing all this right now :)

nikomatsakis (May 14 2018 at 14:13, on Zulip):

@Santiago Pastorino so I agree with @Reed Koser that we ought to be able to refactor the borrow-check to share more core

nikomatsakis (May 14 2018 at 14:13, on Zulip):

I'm not sure how much to worry about that -- maybe worth landing something first? -- but ...

nikomatsakis (May 14 2018 at 14:14, on Zulip):

I guess the idea would be to have a function that , for a given Location, returns a list of invalidated loans (and why)

nikomatsakis (May 14 2018 at 14:14, on Zulip):

which the borrow checker could then call

Santiago Pastorino (May 14 2018 at 14:18, on Zulip):

:+1:

nikomatsakis (May 14 2018 at 19:13, on Zulip):

@Santiago Pastorino so -- in terms of what code goes where —

nikomatsakis (May 14 2018 at 19:13, on Zulip):

the first step is modifying rustc so that it generates the Invalidates tuples at the right locations

nikomatsakis (May 14 2018 at 19:13, on Zulip):

it looks like @Reed Koser got pretty far there, the main problem is that there is a lot of code duplication

Santiago Pastorino (May 14 2018 at 19:14, on Zulip):

I'm trying to take a shortcut :P

nikomatsakis (May 14 2018 at 19:14, on Zulip):

that is, the existing borrow check code in librustc_mir and this "fact dumper" kind of encode the same info

nikomatsakis (May 14 2018 at 19:14, on Zulip):

right now, the borrow checker works sort of like this:

nikomatsakis (May 14 2018 at 19:14, on Zulip):

it walks the MIR

nikomatsakis (May 14 2018 at 19:15, on Zulip):

and, for each statement, determines what loans it invalidates -- then it checks if those loans are "in scope" at that point -- if both are true it reports an error

nikomatsakis (May 14 2018 at 19:15, on Zulip):

but these concepts are not "explicitly materialized" as facts per se

nikomatsakis (May 14 2018 at 19:15, on Zulip):

more like, the borrow check invokes some helper fn whose name I forgot — check_access_for_conflict, I think? — for each of the loans that would be invalidated

nikomatsakis (May 14 2018 at 19:15, on Zulip):

or "borrows", as we call them there

Santiago Pastorino (May 14 2018 at 19:16, on Zulip):

that is, the existing borrow check code in librustc_mir and this "fact dumper" kind of encode the same info

when you say fact dumper, what are you referring to?

nikomatsakis (May 14 2018 at 19:17, on Zulip):

I'm referring to @Reed Koser's branch

nikomatsakis (May 14 2018 at 19:17, on Zulip):

but it builds on some code I landed in rustc a bit back

nikomatsakis (May 14 2018 at 19:17, on Zulip):

that lets you pass -Znll-facts to rustc

nikomatsakis (May 14 2018 at 19:17, on Zulip):

which causes it to dump facts into a subdirectory

Santiago Pastorino (May 14 2018 at 19:18, on Zulip):

got it

nikomatsakis (May 14 2018 at 19:18, on Zulip):

anyway I actually think the code duplication is ok for now

nikomatsakis (May 14 2018 at 19:19, on Zulip):

so we could land it as is — potentially — and then resolve that

nikomatsakis (May 14 2018 at 19:19, on Zulip):

but it would be nice if the borrow checker itself

Santiago Pastorino (May 14 2018 at 19:19, on Zulip):

ok

nikomatsakis (May 14 2018 at 19:19, on Zulip):

used these facts to drive itself

nikomatsakis (May 14 2018 at 19:19, on Zulip):

so that our tests would check that they are a complete set

nikomatsakis (May 14 2018 at 19:19, on Zulip):

(because, if they weren't, we'd be missing errors)

nikomatsakis (May 14 2018 at 19:19, on Zulip):

anyway, this is all just the 1st step — once we have the facts available, there is work to do on the borrow-check repository side

Santiago Pastorino (May 14 2018 at 19:20, on Zulip):

haven't checked @Reed Koser code yet, but seems like we need to make that compile and work

Santiago Pastorino (May 14 2018 at 19:20, on Zulip):

I mean, it seems that it doesn't miss more stuff

nikomatsakis (May 14 2018 at 19:22, on Zulip):

yeah

nikomatsakis (May 14 2018 at 19:23, on Zulip):

the code is pretty straight forward (nice job @Reed Koser =)

nikomatsakis (May 14 2018 at 19:23, on Zulip):

you can view it in this commit

Santiago Pastorino (May 14 2018 at 19:23, on Zulip):

:+1:

nikomatsakis (May 14 2018 at 19:24, on Zulip):

in particular this file

nikomatsakis (May 14 2018 at 19:24, on Zulip):

it walks over the MIR and figures out which paths are manipulated and how

nikomatsakis (May 14 2018 at 19:24, on Zulip):

so e.g. an assign statement is here

nikomatsakis (May 14 2018 at 19:25, on Zulip):

these ultimately boil down to calls to this function

nikomatsakis (May 14 2018 at 19:25, on Zulip):

I guess it doesn't build though

nikomatsakis (May 14 2018 at 19:25, on Zulip):

or at least I don't see impls of things like report_conflicting_borrow

nikomatsakis (May 14 2018 at 19:26, on Zulip):

but I think the idea would be that you would add an Invalidated fact for each such call

nikomatsakis (May 14 2018 at 19:26, on Zulip):

(this code looks like it's kind of cut-and-paste out from the rest of the borrow checker, which makes total sense)

Reed Koser (May 14 2018 at 19:32, on Zulip):

Your analysis there is correct, is mostly copy paste =P.
The general strategy was to copy over most of the core, rip out the real error reporting, and replace it with fact generation

Reed Koser (May 14 2018 at 19:32, on Zulip):

I got about halfway though ripping out the error reporting and didn't get to the last step there at all really

Reed Koser (May 14 2018 at 19:34, on Zulip):

Though I think it should be reasonably trivial (just append to the fact list probably)

Reed Koser (May 14 2018 at 19:35, on Zulip):

I'll have some time to hack on something borrow-check related later today too, possibly the nicer front end if @Santiago Pastorino is going to finish this up

Reed Koser (May 14 2018 at 19:36, on Zulip):

I can also finish up this patch, I feel kinda bad about dropping the ball

Santiago Pastorino (May 14 2018 at 19:36, on Zulip):

I'm ok with taking it over and also ok with leaving it to you

Santiago Pastorino (May 14 2018 at 19:36, on Zulip):

can't promise that I will finish it all today

Santiago Pastorino (May 14 2018 at 19:37, on Zulip):

but I can promise to work on it a bit today and tomorrow and finish this ASAP

nikomatsakis (May 14 2018 at 19:37, on Zulip):

I'm trying to think: it seems like it woudl make the most sense for @Reed Koser to finish what they started, but is there follow-up work we can productively do on the borrow-check side now

nikomatsakis (May 14 2018 at 19:38, on Zulip):

I also opened up this https://github.com/rust-lang-nursery/borrow-check/issues/26 which seems like it might interest you @Santiago Pastorino , as an aside

nikomatsakis (May 14 2018 at 19:38, on Zulip):

(we could flesh it out and make it more concrete)

nikomatsakis (May 14 2018 at 19:38, on Zulip):

(basically I'd like some other way to use borrow-check that lets us test and develop examples without having to run rustc)

nikomatsakis (May 14 2018 at 19:39, on Zulip):

I'm trying to think: it seems like it woudl make the most sense for @Reed Koser to finish what they started, but is there follow-up work we can productively do on the borrow-check side now

well

nikomatsakis (May 14 2018 at 19:39, on Zulip):

one thing we could obviously do

nikomatsakis (May 14 2018 at 19:39, on Zulip):

we could add a kind of filter on the differential-dataflow rules

Reed Koser (May 14 2018 at 19:40, on Zulip):

That works for me. I can finish this up then if that's alright @Santiago Pastorino. I know you claimed it earlier and I kinda stole it

nikomatsakis (May 14 2018 at 19:40, on Zulip):

that cause it to ignore loans that arent' relevant anywhere

nikomatsakis (May 14 2018 at 19:40, on Zulip):

not that interesting but maybe relevant

nikomatsakis (May 14 2018 at 19:40, on Zulip):

anyway it'd be mostly an exercise in learning how stuff work

nikomatsakis (May 14 2018 at 19:40, on Zulip):

@Santiago Pastorino I culd write-up some instructions on that if you have time now

nikomatsakis (May 14 2018 at 19:40, on Zulip):

well let me try to add a few notes into #4 anyway

Santiago Pastorino (May 14 2018 at 19:42, on Zulip):

@Reed Koser go ahead :)

Santiago Pastorino (May 14 2018 at 19:42, on Zulip):

all yours

Santiago Pastorino (May 14 2018 at 19:44, on Zulip):

@nikomatsakis yep, let me know what to do :)

Reed Koser (May 14 2018 at 19:44, on Zulip):

Sounds good, thanks

Santiago Pastorino (May 14 2018 at 19:45, on Zulip):

I have time to do some rustc stuff again since today, besides from going to the doctor with the baby :)

nikomatsakis (May 14 2018 at 19:50, on Zulip):

@Santiago Pastorino I wrote up this

nikomatsakis (May 14 2018 at 19:50, on Zulip):

very simple first step, but I imagine it'll take a bit to get acquainted with borrow-check codebase anyhow

Santiago Pastorino (May 14 2018 at 19:50, on Zulip):

:+1:

Santiago Pastorino (May 14 2018 at 19:51, on Zulip):

so it's two things? https://github.com/rust-lang-nursery/borrow-check/issues/26 and https://github.com/rust-lang-nursery/borrow-check/issues/4#issuecomment-388940330 ?

nikomatsakis (May 14 2018 at 19:53, on Zulip):

those are distinct things

nikomatsakis (May 14 2018 at 19:53, on Zulip):

either one seems fine

nikomatsakis (May 14 2018 at 19:54, on Zulip):

but the latter is much more concrete

nikomatsakis (May 14 2018 at 19:54, on Zulip):

the former is kind of a big task

Reed Koser (May 14 2018 at 19:55, on Zulip):

I think my branch includes step 1 there

Santiago Pastorino (May 14 2018 at 19:55, on Zulip):

ok

Santiago Pastorino (May 14 2018 at 19:55, on Zulip):

gonna try to help with the latter thing

Reed Koser (May 14 2018 at 19:56, on Zulip):

Oh wait that's in borrow-check nvm

Reed Koser (May 14 2018 at 19:56, on Zulip):

I added that to all facts in rustc

nikomatsakis (May 14 2018 at 19:56, on Zulip):

right, those are separate

lqd (May 14 2018 at 20:21, on Zulip):

wrt a friendlier frontend, maybe the one at nll-soufflé could be reused @nikomatsakis ?

Santiago Pastorino (May 14 2018 at 21:06, on Zulip):

@nikomatsakis I'm going to the doctor now with the little baby :), but was reading what you wrote

Santiago Pastorino (May 14 2018 at 21:07, on Zulip):

in particular then we would need to make that compile loading facts from invalidated.facts.

Santiago Pastorino (May 14 2018 at 21:07, on Zulip):

what does it means to compile loading a file?

Santiago Pastorino (May 14 2018 at 21:07, on Zulip):

you mean that you want the thing to run with invalidated.facts?

Santiago Pastorino (May 14 2018 at 21:08, on Zulip):

and also

Santiago Pastorino (May 14 2018 at 21:08, on Zulip):

where is invalidated.facts?

Santiago Pastorino (May 14 2018 at 21:09, on Zulip):

it's not under inputs dir

Santiago Pastorino (May 14 2018 at 21:09, on Zulip):

should I generate that somehow?

Santiago Pastorino (May 14 2018 at 21:09, on Zulip):

sorry, I'm very late to the party, I guess you explained all this several times

Santiago Pastorino (May 14 2018 at 21:10, on Zulip):

I will do this when I'm back

nikomatsakis (May 14 2018 at 21:55, on Zulip):

should I generate that somehow?

sorry, should have been clearer: yes, I figured you'd just make an empty file to start

nikomatsakis (May 14 2018 at 21:55, on Zulip):

since we are not actually using this data for anything yet

Santiago Pastorino (May 14 2018 at 22:51, on Zulip):

@nikomatsakis I'm back and this thing is done

Santiago Pastorino (May 14 2018 at 22:51, on Zulip):

the part 1

nikomatsakis (May 14 2018 at 22:51, on Zulip):

Nice

Santiago Pastorino (May 14 2018 at 22:52, on Zulip):

hehe, I had to do nothing

Santiago Pastorino (May 14 2018 at 22:52, on Zulip):

we need to talk about part 2

nikomatsakis (May 14 2018 at 22:55, on Zulip):

ok so

nikomatsakis (May 14 2018 at 22:55, on Zulip):

I was thinking about this on the bike ride home just now

nikomatsakis (May 14 2018 at 22:55, on Zulip):

I've only got a few minutes but maybe I can sketch something on the issue

Santiago Pastorino (May 14 2018 at 22:56, on Zulip):

ok

Santiago Pastorino (May 14 2018 at 22:56, on Zulip):

yes

Santiago Pastorino (May 14 2018 at 22:56, on Zulip):

I'm around with some time to code, so :+1:

Santiago Pastorino (May 14 2018 at 22:56, on Zulip):

meanwhile I'm going to read borrow-check code

nikomatsakis (May 14 2018 at 23:04, on Zulip):

ok so I left some notes, but they're probably too vague to be of much use

nikomatsakis (May 14 2018 at 23:04, on Zulip):

gotta run now in any case

nikomatsakis (May 14 2018 at 23:04, on Zulip):

@Santiago Pastorino can you open a PR ?

Santiago Pastorino (May 14 2018 at 23:16, on Zulip):

yes

Santiago Pastorino (May 14 2018 at 23:17, on Zulip):

it's a shame the PR

Santiago Pastorino (May 14 2018 at 23:17, on Zulip):

but yes

Santiago Pastorino (May 14 2018 at 23:18, on Zulip):

https://github.com/rust-lang-nursery/borrow-check/pull/28

nikomatsakis (May 15 2018 at 00:26, on Zulip):

heh; I think there's a few more things that could be added.

nikomatsakis (May 15 2018 at 00:26, on Zulip):

I'll leave comments :)

Santiago Pastorino (May 15 2018 at 13:27, on Zulip):

unsure what happened yesterday with this

nikomatsakis (May 15 2018 at 13:27, on Zulip):

nothing yet :)

Santiago Pastorino (May 15 2018 at 13:27, on Zulip):

hehe committed two lines of codes and one was missing

Santiago Pastorino (May 15 2018 at 13:28, on Zulip):

nothing yet :)

well, talking about the last part I had assigned

Santiago Pastorino (May 15 2018 at 13:29, on Zulip):

need to tackle step 2

nikomatsakis (May 15 2018 at 13:29, on Zulip):

right so I also broke out a new issue that described my thoughts there in a bit more detail

nikomatsakis (May 15 2018 at 13:30, on Zulip):

but this intersects what @pnkfelix and I are talking about @Santiago Pastorino so maybe jump in there :)

Santiago Pastorino (May 15 2018 at 13:35, on Zulip):

in #making-plans?

nikomatsakis (May 15 2018 at 13:39, on Zulip):

@Santiago Pastorino yeah, particularly towards the end -- e.g. in this comment I sketched out what I see as the major pieces atm

Santiago Pastorino (May 15 2018 at 13:40, on Zulip):

:+1:, I'm reading :)

Santiago Pastorino (May 15 2018 at 13:40, on Zulip):

70 messages left :P

Reed Koser (May 15 2018 at 13:44, on Zulip):

Sorry I meant to write up my progress on this but ran out of time last night. I cleaned up the work I did Thursday and then stopped because I 1) ran in to a doozy of a borrowck error and 2) had to get some sleep. Hopefully I'll have enough time to actually finish this up tonight, but it turns out moving across the country results in some time-consuming tasks =)

Reed Koser (May 15 2018 at 13:52, on Zulip):

So reading through other threads, seems like this is blocking a lot of other work. I won't have time to poke at this until 12+ hours from now, so if someone else has spare cycles between now and then (@pnkfelix?) feel free to pick this up

pnkfelix (May 15 2018 at 13:52, on Zulip):

my evenings are often filled with child care stuff

pnkfelix (May 15 2018 at 13:53, on Zulip):

so don't be too confident that I'll be poking at too many new things in the next 12+ hours

Reed Koser (May 15 2018 at 13:53, on Zulip):

:+1: No worries. Your children are probably more important than working on this stuff :smile:

Reed Koser (May 16 2018 at 14:09, on Zulip):

Just a heads up, I pushed https://github.com/rust-lang/rust/pull/50798
There's some more cleanup I think I should do but it's ready for review.

nikomatsakis (May 16 2018 at 14:10, on Zulip):

nice

Reed Koser (May 16 2018 at 14:10, on Zulip):

I /think/ I picked up all the important cases for invalidations but it's definitely possible I missed something =)

nikomatsakis (May 16 2018 at 14:10, on Zulip):

cool

nikomatsakis (May 16 2018 at 14:10, on Zulip):

I'll check :)

Reed Koser (May 16 2018 at 14:11, on Zulip):

sounds good, thanks

nikomatsakis (May 16 2018 at 15:55, on Zulip):

@Reed Koser I left a review fyi

nikomatsakis (May 16 2018 at 15:55, on Zulip):

in particular, I answered some of your FIXME questions

nikomatsakis (May 16 2018 at 15:56, on Zulip):

but it basically looked right to me, though I could easily be missing something too :)

Reed Koser (May 16 2018 at 16:12, on Zulip):

Cool, I'll take a look after work

Reed Koser (May 16 2018 at 16:12, on Zulip):

Probably like 7:30 PST

Reed Koser (May 17 2018 at 07:51, on Zulip):

@nikomatsakis https://github.com/rust-lang/rust/pull/50798 is back in your wheelhouse

nikomatsakis (May 17 2018 at 15:44, on Zulip):

ok, I r+'d it

nikomatsakis (May 17 2018 at 15:44, on Zulip):

I was chatting a bit with @David Wood about the next steps here

nikomatsakis (May 17 2018 at 15:44, on Zulip):

basically we don't have to wait for the PR to land to start trying it out

nikomatsakis (May 17 2018 at 15:46, on Zulip):

@David Wood probably step 1 is to get a build going of rust-lang/rust#50798

davidtwco (May 17 2018 at 15:46, on Zulip):

Alright, I'll get that kicked off.

nikomatsakis (May 17 2018 at 15:46, on Zulip):

the blog post actually spelled out the datalog rules we're going to need already

Reed Koser (May 17 2018 at 15:46, on Zulip):

:crab:

Reed Koser (May 17 2018 at 15:46, on Zulip):

Good luck and God speed

nikomatsakis (May 17 2018 at 15:46, on Zulip):

not sure what's the best way to "come up to speed"

davidtwco (May 17 2018 at 15:47, on Zulip):

What was the video you mentioned?

csmoe (May 17 2018 at 15:47, on Zulip):

https://www.youtube.com/watch?v=oTnbtGuSpWQ&feature=youtu.be

csmoe (May 17 2018 at 15:47, on Zulip):

this one?

csmoe (May 17 2018 at 15:48, on Zulip):

I finished it just now.

nikomatsakis (May 17 2018 at 15:48, on Zulip):

that looks like it

davidtwco (May 17 2018 at 15:50, on Zulip):

Alright, I'll give that a watch, read the blog post and get that PR built.

nikomatsakis (May 17 2018 at 15:51, on Zulip):

@David Wood feel free to ping me with any questions of course

davidtwco (May 17 2018 at 15:51, on Zulip):

Will do!

Santiago Pastorino (May 17 2018 at 20:26, on Zulip):

so ... how can I generate input data from @Reed Koser PR?

Santiago Pastorino (May 17 2018 at 20:26, on Zulip):

taking a look but any pointer is appreciated

nikomatsakis (May 17 2018 at 20:26, on Zulip):

well, you have to build it first

nikomatsakis (May 17 2018 at 20:27, on Zulip):

then you have to run -Znll-facts on some input

nikomatsakis (May 17 2018 at 20:27, on Zulip):

so we should pick some inputs that have errors :)

Santiago Pastorino (May 17 2018 at 20:27, on Zulip):

yeah saw about -Znll-facts

Santiago Pastorino (May 17 2018 at 20:28, on Zulip):

but what were you using on polonius repo?

Santiago Pastorino (May 17 2018 at 20:28, on Zulip):

are there some inputs you were already using?

Santiago Pastorino (May 17 2018 at 20:28, on Zulip):

do I need to build some example?

Santiago Pastorino (May 17 2018 at 20:30, on Zulip):

hmm in the video there's an example if I'm not wrong

nikomatsakis (May 17 2018 at 20:31, on Zulip):

there are some inputs I used on the repo, however,

nikomatsakis (May 17 2018 at 20:31, on Zulip):

none of those examples actually are expected to give an error

nikomatsakis (May 17 2018 at 20:31, on Zulip):

doesn't mean we can't try them, actually :)

nikomatsakis (May 17 2018 at 20:33, on Zulip):

so basically you would do rustc -Znll-facts foo.rs

nikomatsakis (May 17 2018 at 20:33, on Zulip):

I think the README.md maybe talks about that?

nikomatsakis (May 17 2018 at 20:33, on Zulip):

yes, there is a section here

Santiago Pastorino (May 17 2018 at 20:48, on Zulip):

:+1:

Santiago Pastorino (May 17 2018 at 20:48, on Zulip):

maybe some example like ...

Santiago Pastorino (May 17 2018 at 20:48, on Zulip):
fn location_sensitive(vec: &mut Vec<u32>) -> &mut u32 {
    let p = &mut vec[3];

    if *p == 4 {
        return p;
    }

    vec.push(5);

    &mut vec[4]
}
Santiago Pastorino (May 17 2018 at 20:49, on Zulip):

it's the idea you mentioned on the video

nikomatsakis (May 17 2018 at 20:51, on Zulip):

I see. Yes, that's good.

nikomatsakis (May 17 2018 at 20:51, on Zulip):

there is an example in the repo you could use

Santiago Pastorino (May 17 2018 at 20:54, on Zulip):

issue-47680.rs ?

Santiago Pastorino (May 17 2018 at 20:55, on Zulip):

but does this fail in the insensitive analysis?

Santiago Pastorino (May 17 2018 at 20:56, on Zulip):

it depends on what we try to do, just dumping invalidates would be good to test this out

Santiago Pastorino (May 17 2018 at 20:56, on Zulip):

but at the same time we would need one that fails

nikomatsakis (May 17 2018 at 20:56, on Zulip):

no, not that one

nikomatsakis (May 17 2018 at 20:56, on Zulip):

it will however definitely fail in the insensitive analysis

nikomatsakis (May 17 2018 at 20:56, on Zulip):

it's not the one I meant tho

nikomatsakis (May 17 2018 at 20:56, on Zulip):

one sec

Santiago Pastorino (May 17 2018 at 20:56, on Zulip):

well probably the one that fails would be more useful when I do the second part which is tying timely_opt with insensitive stuff

Santiago Pastorino (May 17 2018 at 20:57, on Zulip):

yeah for the first part I think anything is good

nikomatsakis (May 17 2018 at 20:58, on Zulip):

I meant src/test/ui/nll/get_default.rs

nikomatsakis (May 17 2018 at 20:58, on Zulip):

it's basically the same test as the one from our discussion tho

nikomatsakis (May 17 2018 at 21:36, on Zulip):

@Santiago Pastorino were you able to run anything?

Santiago Pastorino (May 17 2018 at 21:40, on Zulip):

hey, I'm back

Santiago Pastorino (May 17 2018 at 21:41, on Zulip):

not yet, wasn't with the computer

Santiago Pastorino (May 17 2018 at 21:41, on Zulip):

let me try

Reed Koser (May 18 2018 at 07:48, on Zulip):

I created https://github.com/rust-lang-nursery/polonius/pull/35 to "properly" close out #4. It just adds some example facts to the repo so people don't necessarily have to build their own rustc to play with invalidates. CC @nikomatsakis @Santiago Pastorino and @lqd

nikomatsakis (May 18 2018 at 09:34, on Zulip):

I guess that closes out #4; should probably open another issue to change the official output from the borrow_live_at results to just the points where errors occur

Santiago Pastorino (May 18 2018 at 11:04, on Zulip):

@Reed Koser cool, I had done the same in another PR will check with @nikomatsakis how to finish my stuff

nikomatsakis (May 18 2018 at 12:36, on Zulip):

hey @Santiago Pastorino, I'm around now

Reed Koser (May 18 2018 at 14:47, on Zulip):

Don't we want both? The invalidates facts for input and errors as output validation

Reed Koser (May 18 2018 at 14:47, on Zulip):

Oh you mean in the prototype

Reed Koser (May 18 2018 at 14:48, on Zulip):

Brain isn't working at full speed quite yet

nikomatsakis (May 18 2018 at 14:59, on Zulip):

Don't we want both? The invalidates facts for input and errors as output validation

not sure I understood you here :)

nikomatsakis (May 18 2018 at 15:00, on Zulip):

but I think the next logical step after adding invalidates relation is rejiggering the analyses to output errors instead of the raw borrow_live_at (though this impacts also the integration that @pnkfelix was proposing, but we can tweak this — e.g., have an option to emit borrow_live_at too)

nikomatsakis (May 18 2018 at 15:01, on Zulip):

I'm not sure just how far @Santiago Pastorino got on this but in their PR they have the basic setup for the location insensitive case, anyway

Last update: Nov 21 2019 at 13:15UTC