Stream: t-compiler/wg-nll

Topic: porting-to-datafrog


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

OK so now that we landed https://github.com/rust-lang-nursery/polonius/pull/36 we gotta port the location-insensitive code to use :frog: — I was saying to @lqd that it would be good for @Santiago Pastorino (or someone besides @lqd and @Frank McSherry , anyway) to do this, so that we can gain more experience

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

I can kinda give you a few tips

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

the basic ideas are the same as before — that is, we're breaking down into join operations etc

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

but in the new system you have to create explicit variables to represent each intermediate point

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

cc @Arjan van Eersel with whom I've been chatting in privmsg :)

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

I'm looking now for that video that @Santiago Pastorino and I recorded :) youtube is kind of hard to navigate...

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

ok, found it. So what I was going to say is that the concepts from this video still apply.

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

let me show an example; I think it's good to start by looking at the naive rules

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

(you could read @**Frank McSherry**'s blog post, too, but you may not need to; it covers how the implementation works (as well as how to use it)

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

anyway the basic idea is that we are going to be iteratively building up the full set of tuples

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

so we first create an iteration:

let mut iteration1 = Iteration::new();
nikomatsakis (May 19 2018 at 18:31, on Zulip):

within the iteration you create variables representing the intermediate points

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

you have to declare these up-front, which is perhaps a bit confusing

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

these variables generally serve one of two purposes:

1. indexing an existing relation for a later join: this basically means mapping into a (K, V) tuple where the K represents the key that will be used in the join
2. collecting the results of joins

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

as an example of an index, consider subset_r1p:

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

it is given a while here, during the while loop:

subset_r1p.from_map(&subset, |&(r1, r2, p)| ((r1, p), r2));
nikomatsakis (May 19 2018 at 18:33, on Zulip):

this from_map means "add the tuples resulting from applying the closure to subset into subset_r1p"

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

so in this case we take as input three tuples like (r1, r2, p) and reorganize them to ((r1, p), r2) — this basically makes (r1, p) a key we can use to do a later join

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

similarly subset_r2p makes the key be (r2, p)

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

(you can sort of see the naming convention that @Frank McSherry adopted here: foo_xy means "the relation foo with x and y selected as the key)

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

those two indices are then joined here in order to achieve this bit of datalog:

subset(R1, R3, P) :-
    subset(R1, R2, P),
    subset(R2, R3, P).
lqd (May 19 2018 at 18:35, on Zulip):

(I'm also available to help @Santiago Pastorino whenever, I also have some notes from converting the programs to :frog: the very mechanical steps I followed; but which were of course conceptually similar to what you and niko went over on the video)

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

the key there is that you look for which variables the two relations have in common:

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

in this case, R2 and P are shared between subset(R1, R2, P) and subset(R2, R3, P)

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

in one case, R2 appears in the second position, and in the other, in the first position, which is why we are joining subset_r1p and subset_r2p

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

(I just realized that it might be a bit confusing that R2 is kind of used in two distinct ways here: it might be clearer if we defined the datalog as:

subset(A, C, P) :-
    subset(A, B, P),
    subset(B, C, P).
nikomatsakis (May 19 2018 at 18:37, on Zulip):

in which case the variables in common are B and P

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

and the index subset_r1p corresponds to B appearing in the first position (subset(B, C, P))

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

whereas subset_r2p corresponds to B appearing in the second position (subset(A, B, P))

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

anyway, I'll stop here — maybe that's enough to get you started :) but yeah feel free to leave questions and somebody can answer

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

it occurs to me I probably should have tried to write this up as actual text in Github and not on Zulip but oh well

Keith Yeung (May 19 2018 at 18:41, on Zulip):

i happen to also be reading through this

Keith Yeung (May 19 2018 at 18:42, on Zulip):

name suggestions for the new algorithm?

Keith Yeung (May 19 2018 at 18:42, on Zulip):

InsensitiveFrog?

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

lol. Sure =) eventually I envision this being merged into the optimized-frog variant in any case

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

the name of the evil frog in the Muppets Most Wanted movie was Constantine

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

not sure how we can make use of that

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

or the name Kermit

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

but we ... probably should

Keith Yeung (May 19 2018 at 18:58, on Zulip):

the only thing that i didn't understand from reading the code is the call to .complete()

Keith Yeung (May 19 2018 at 18:59, on Zulip):

e.g. for the naive datafrog algorithm, it's being called on subset_r1p

Keith Yeung (May 19 2018 at 18:59, on Zulip):

the return value of which is assigned to subset

Keith Yeung (May 19 2018 at 18:59, on Zulip):

this makes me think that the result of subset_r1p is being assigned to subset

Keith Yeung (May 19 2018 at 19:01, on Zulip):

which... doesn't quite make much sense to me, since in the iteration we also defined and calculated subset_r2p, subset_p and subset, and we only used subset_r1p

Keith Yeung (May 19 2018 at 19:01, on Zulip):

doesn't this just throw away all our calculations for nothing?

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

ah, actually that's an inefficiency in the way it's expressed I think

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

that said, it's not wrong

lqd (May 19 2018 at 19:03, on Zulip):

the naive algorithm should only have one iteration (there's an issue on GH about that)

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

in particular, we're going to iterate until a fixed point is reached

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

at that point, both subset and subset_r1p have the same set of tuples,

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

but organized differently

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

it happens to return the version that is indexed by (r1, p), because that is what is needed later for a join

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

indeed I think that the main subset is not needed at all

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

you could just always keep the tuples organized like ((r1, p), r2) instead of (r1, r2, p)

lqd (May 19 2018 at 19:05, on Zulip):

@Keith Yeung complete will turn the Variable storage (made to compute the joins in rounds w/ deltas) into the regular tuples you'd expect out of the computation

Keith Yeung (May 19 2018 at 19:08, on Zulip):

at that point, both subset and subset_r1p have the same set of tuples,

huh, this bit is unintuitive to me, because it means that by calculating subset, you also change the data that's in subset_r1p

Keith Yeung (May 19 2018 at 19:09, on Zulip):

which i didn't quite expect, i thought this was supposed to be functional (i.e. without side effects)

lqd (May 19 2018 at 19:10, on Zulip):

the indexed variables are updated manually and independently from one another

Keith Yeung (May 19 2018 at 19:12, on Zulip):

oh wait, are you saying that subset_r1q is a view on subset?

lqd (May 19 2018 at 19:12, on Zulip):

doing things with subset will not touch subset_* — this part updates them https://github.com/rust-lang-nursery/polonius/blob/master/src/output/naive.rs#L71-L74

lqd (May 19 2018 at 19:13, on Zulip):

semantically yes, physically it will be a copy

Keith Yeung (May 19 2018 at 19:13, on Zulip):

@lqd ok, so why in the end do you only have a subset_r1p.complete()? why do you even bother to calculate subset in the iteration?

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

it is one of the inefficiencies, but it's the same data in fine

lqd (May 19 2018 at 19:15, on Zulip):

the indexing and manual maintenance is the thing that's more useful

lqd (May 19 2018 at 19:15, on Zulip):

to be clear

lqd (May 19 2018 at 19:15, on Zulip):

at first we were computing subset

lqd (May 19 2018 at 19:15, on Zulip):

but the next (useless) iteration used subset indexed differently

lqd (May 19 2018 at 19:16, on Zulip):

and reindexed subset, so we just removed part of the redundancy by returning the indexed that was already done before

Keith Yeung (May 19 2018 at 19:16, on Zulip):

yeah, it seems to me that both subset and requires are only useful for indexing

Keith Yeung (May 19 2018 at 19:17, on Zulip):

and in fact subset isn't being used at all in the final iteration

lqd (May 19 2018 at 19:17, on Zulip):

the pattern though will be exactly the same whether the data is used or not

lqd (May 19 2018 at 19:17, on Zulip):

yeah but they flow into each other tho

Keith Yeung (May 19 2018 at 19:19, on Zulip):

this is still not clear to me what in the world is happening

lqd (May 19 2018 at 19:19, on Zulip):

subset goes to requires which goes to borrow_live_at

Keith Yeung (May 19 2018 at 19:19, on Zulip):

lemme pose a question

lqd (May 19 2018 at 19:20, on Zulip):

I suggest focusing on the mechanical transformations of the datalog rules, "here are the steps I need to do for this rule" from this will flow variables, temporaries, and indices

Keith Yeung (May 19 2018 at 19:20, on Zulip):

oh wait, nvm

Keith Yeung (May 19 2018 at 19:20, on Zulip):

i'm seeing it now

Keith Yeung (May 19 2018 at 19:20, on Zulip):

subset_r1p is being mapped from subset

lqd (May 19 2018 at 19:20, on Zulip):

yes

lqd (May 19 2018 at 19:21, on Zulip):

I sent a link to those manual "view" mainenance lines :)

Keith Yeung (May 19 2018 at 19:21, on Zulip):

that really shouldn't be in the first position, since subset_r1p is a result of the computation

Keith Yeung (May 19 2018 at 19:22, on Zulip):

because what i thought before is that data is being copied from subset to subset_r1p, and then subset_r1p is then used to recompute subset

Keith Yeung (May 19 2018 at 19:23, on Zulip):

and after that, no other data assignments happened to subset_r1p

Keith Yeung (May 19 2018 at 19:23, on Zulip):

and we return subset_r1p

Keith Yeung (May 19 2018 at 19:23, on Zulip):

which made the whole process of recomputing subset look useless

Keith Yeung (May 19 2018 at 19:23, on Zulip):

obviously that's not how datafrog works

lqd (May 19 2018 at 19:24, on Zulip):

keep in mind these are all being iterated to a fixpoint

lqd (May 19 2018 at 19:25, on Zulip):

the datalog rules being the key

lqd (May 19 2018 at 19:26, on Zulip):

that's why they're always in the comments as well

lqd (May 19 2018 at 19:26, on Zulip):

the rest is manual maintenance, and positives and negatives of efficiency :)

Keith Yeung (May 19 2018 at 19:26, on Zulip):

the comments aren't enough, because this is a different programming model

Keith Yeung (May 19 2018 at 19:26, on Zulip):

lemme show you what i was thinking

lqd (May 19 2018 at 19:27, on Zulip):

did you see the differential dataflow analyses ?

Keith Yeung (May 19 2018 at 19:27, on Zulip):

i thought subset_r1p.from_map(&subset, ..) meant subset_r1p = subset.map(..)

Keith Yeung (May 19 2018 at 19:29, on Zulip):

so when i didn't see subset_r1p being "assigned to" anymore after the calculation of subset, i was very confused

lqd (May 19 2018 at 19:29, on Zulip):

I fail to see the difference, after both of those calls, subset_r1p and subset will have the "same" tuples, but ordered differently

lqd (May 19 2018 at 19:29, on Zulip):

ok understood

Keith Yeung (May 19 2018 at 19:30, on Zulip):

the difference is, from_map is only called at the beginning of the iteration

lqd (May 19 2018 at 19:30, on Zulip):

it was being assigned, in the next iteration of the loop :)

Keith Yeung (May 19 2018 at 19:30, on Zulip):

yes, this makes more sense now

lqd (May 19 2018 at 19:30, on Zulip):

:thumbs_up:

lqd (May 19 2018 at 19:31, on Zulip):

those rules are the beginning, in my mind, as they are tangential to the datalog

lqd (May 19 2018 at 19:31, on Zulip):

similar to the .map calls that were more localized in DD

Keith Yeung (May 19 2018 at 19:32, on Zulip):

next question, what's the purpose of variable_indistinct()?

lqd (May 19 2018 at 19:32, on Zulip):

a lot of those would be hidden by DD

lqd (May 19 2018 at 19:32, on Zulip):

also keep in mind this whole thing started like wednesday so we're a little light on "best practices" and rationale for communicating everything :D

lqd (May 19 2018 at 19:33, on Zulip):

variable indistinct is a way to control whether the variable will need to be deduped or not

lqd (May 19 2018 at 19:33, on Zulip):

similar to how DD used distinct to ask for deduplication

lqd (May 19 2018 at 19:34, on Zulip):

in most temporaries, indexes, there's no need for this, and slows things down

lqd (May 19 2018 at 19:34, on Zulip):

it's mostly for performance though

lqd (May 19 2018 at 19:34, on Zulip):

AFAIUI

lqd (May 19 2018 at 19:35, on Zulip):

as to not sort/dedup/copy everything all the time

lqd (May 19 2018 at 19:35, on Zulip):

I don't Frank's article on :frog: mentions these but yeah

Keith Yeung (May 19 2018 at 19:37, on Zulip):

hmm... so the most important part is how it's different from just calling variable, but i guess it just means variable is duplicated by default

lqd (May 19 2018 at 19:38, on Zulip):

by default they are maintained "distinctly"

lqd (May 19 2018 at 19:38, on Zulip):

so deduped

lqd (May 19 2018 at 19:39, on Zulip):

(btw datafrog has some documentation by now)

Keith Yeung (May 19 2018 at 19:39, on Zulip):

ohhh ok, so that's why intermediate vars benefit from indistinct

Keith Yeung (May 19 2018 at 19:39, on Zulip):

am reading the source code rn

lqd (May 19 2018 at 19:40, on Zulip):

here https://github.com/frankmcsherry/datafrog/blob/master/src/lib.rs#L111-L115

lqd (May 19 2018 at 19:40, on Zulip):

yeah

lqd (May 19 2018 at 19:40, on Zulip):

and because they are usually indexed from already deduped relations

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

i thought subset_r1p.from_map(&subset, ..) meant subset_r1p = subset.map(..)

it actually means subset_r1p += subset.map(..)

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

(where subset_r1p is a set)

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

perhaps extend_from_map or something would be a better name

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

(to connect to Rust's extend methods)

Keith Yeung (May 19 2018 at 19:49, on Zulip):

@nikomatsakis the key thing i missed was that we're inside of an iteration, so tuples carried over from previous ones

Keith Yeung (May 19 2018 at 19:49, on Zulip):

i thought it was an "all-at-once" assignment

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

yeah; this is why I say += or extend

Frank McSherry (May 19 2018 at 20:04, on Zulip):

I'm here! But I drank a bunch, and also read HN which !#$!@# is just never smart.

Frank McSherry (May 19 2018 at 20:05, on Zulip):

Trying to avoid telling Google's head of cloud programming languages that I can't take his or her opinion seriously as long as their stream processor remotes all of its state to other machines.

Frank McSherry (May 19 2018 at 20:08, on Zulip):

Also, Vienna is a happier place than Zürich. Totally. :D

Keith Yeung (May 19 2018 at 20:14, on Zulip):

oh shoot, i didn't notice that @Arjan van Eersel has already been working on https://github.com/rust-lang-nursery/polonius/issues/37!

Keith Yeung (May 19 2018 at 20:14, on Zulip):

i already made a PR fixing that issue...

Keith Yeung (May 19 2018 at 20:15, on Zulip):

https://github.com/rust-lang-nursery/polonius/pull/39

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

@Keith Yeung sorry I didn't get a chance to try that out yet btw, hopefully soon

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

@Santiago Pastorino so were you going to hack on that now?

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

yes

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

pulling and stuff now :)

lqd (May 21 2018 at 19:55, on Zulip):

@Santiago Pastorino how many potential_errors did you get on clap btw ? I only remember how long it took

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

@lqd hmm don't remember, unsure if I ran with clap or with another example

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

I don't think there are "invalidates" points in the other dataset, some maybe one of yours

Santiago Pastorino (May 21 2018 at 20:04, on Zulip):

to be honest I don't remember what I did, will try to port this thing and test again

Santiago Pastorino (May 21 2018 at 20:05, on Zulip):

was reading @Frank McSherry blog post now to see how's the deal :)

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

(in any case I built a version of the location insensitive thing so that I can help you with it if you had questions while doing yours — but as I don't know what the correct numbers are, it's stIll buggy :simple_smile:

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

I suggest to base your work on the version of the "naive.rs" that Keith has a PR for, it's a tad bit simpler than the one in master right now

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

:+1:

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

oh but issue-47680 does have invalidates facts in the repo, but not in your PR #34, so you should be good to go (+ clap has some as well) :)

Santiago Pastorino (May 21 2018 at 20:39, on Zulip):

:+1:

lqd (May 21 2018 at 21:58, on Zulip):

@Santiago Pastorino I _think_ PR #34 doesn't find potential errors for the issuedataset — & it feels like the last timely join might be the cause — but does have data for restricts_anywhere and subset_anywhere. Just a heads up if you're also using it as a guide for your port :) (& if that's the case I'd focus on translating the datalog rules, rather than transliterating the timely compute too precisely)

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

ok

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

will check that later

lqd (May 21 2018 at 22:13, on Zulip):

maybe there are no potential errors in those datasets :D

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

have just finished porting LocationInsensitive stuff

nikomatsakis (May 21 2018 at 22:15, on Zulip):

I'd be pretty surprised if the issue-47680 had no error

nikomatsakis (May 21 2018 at 22:15, on Zulip):

when run w/ out loc sensitivity

nikomatsakis (May 21 2018 at 22:15, on Zulip):

in fact more than surprised :)

lqd (May 21 2018 at 22:16, on Zulip):

mine finds 2

lqd (May 21 2018 at 22:17, on Zulip):

@Santiago Pastorino once you get the hang of it, translation is pretty straight-forward right ?

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

in order to test location insensitive, are you using some example?

lqd (May 21 2018 at 22:18, on Zulip):

yes issue-47680

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

yes, it's easy, I may have done something wrong though :P

lqd (May 21 2018 at 22:18, on Zulip):

(tbf I have not tried the new "treefrog leapjoin" but that would definitely help in our more complex cases)

Santiago Pastorino (May 21 2018 at 22:20, on Zulip):

https://github.com/rust-lang-nursery/polonius/pull/41

Santiago Pastorino (May 21 2018 at 22:20, on Zulip):

in fact I'm surprised how better the code and easy to read is

Santiago Pastorino (May 21 2018 at 22:20, on Zulip):

again, I may be missing something important :P

Santiago Pastorino (May 21 2018 at 22:20, on Zulip):

haven't tested the thing yet

lqd (May 21 2018 at 22:21, on Zulip):

yeah I think a couple things are missing, almost done :)

lqd (May 21 2018 at 22:22, on Zulip):

oh maybe you're not porting your PR#34 ? I see no invalidates

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

no no

lqd (May 21 2018 at 22:22, on Zulip):

oh :D

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

I'm not porting that

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

I wanted to just port what's in master

Santiago Pastorino (May 21 2018 at 22:23, on Zulip):

then I can force push that PR

Santiago Pastorino (May 21 2018 at 22:23, on Zulip):

I mean, port that port and force push there

lqd (May 21 2018 at 22:23, on Zulip):

then I retract my previous statements! :D

Santiago Pastorino (May 21 2018 at 22:23, on Zulip):

heheh :+1:

Santiago Pastorino (May 21 2018 at 22:23, on Zulip):

once I get the OK or is it merged I can start porting the other part

Santiago Pastorino (May 21 2018 at 22:24, on Zulip):

anyway I'm not 100% sure how some things in datafrog work

Santiago Pastorino (May 21 2018 at 22:25, on Zulip):

mainly how the iterations work, I may be guessing that correctly but better to be 100% sure

Santiago Pastorino (May 21 2018 at 22:25, on Zulip):

I guess the blog post explains a bit that

lqd (May 21 2018 at 22:25, on Zulip):

probably don't need the clone in all_facts.region_live_at.clone()

Santiago Pastorino (May 21 2018 at 22:27, on Zulip):

right, I've added that after saw an error but yeah doesn't seem to be needed

Santiago Pastorino (May 21 2018 at 22:27, on Zulip):

fixed

lqd (May 21 2018 at 22:31, on Zulip):

I guess it would be cool to be able to test it, but it certainly _looks good_ :)

Santiago Pastorino (May 21 2018 at 22:31, on Zulip):

so iteration is just in case there are a lot of rules that one ends affecting the other one?

Santiago Pastorino (May 21 2018 at 22:32, on Zulip):

facts go outside that because are ... facts

lqd (May 21 2018 at 22:32, on Zulip):

slight nit: the "// redundantly computed index" can be removed since you only have one and it's not an index

lqd (May 21 2018 at 22:32, on Zulip):

yeah the iteration is the thing that will create new tuples from the existing ones by applying the rules — all until no more tuples are created

lqd (May 21 2018 at 22:33, on Zulip):

tuples = facts here as well — the input facts / inputs indeed are outside

lqd (May 21 2018 at 22:34, on Zulip):

I wish I didn't add this "redudantly computed" comment as it's obviously not clear enough what I meant at all

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

slight nit: the "// redundantly computed index" can be removed since you only have one and it's not an index

fixed

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

I wish I didn't add this "redudantly computed" comment as it's obviously not clear enough what I meant at all

don't worry, it was just a copy & paste thing and forgot to remove that

lqd (May 21 2018 at 22:51, on Zulip):

as I'm about to go to sleep, I _think_ this is the potential_errors your PR#34 would find on issue-47680:

# potential_errors
"Mid(bb3[2])"  "bw1"
"Mid(bb10[2])" "bw2"
Santiago Pastorino (May 21 2018 at 22:56, on Zulip):

and is that fine?

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

haven't gone through it yet

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

haven't checked the mir

Santiago Pastorino (May 21 2018 at 22:57, on Zulip):

and I don't even remember what the example is about :P

lqd (May 21 2018 at 22:57, on Zulip):

I don't know :)

Santiago Pastorino (May 21 2018 at 22:57, on Zulip):

ok :)

Santiago Pastorino (May 21 2018 at 22:57, on Zulip):

we would need to figure that out

lqd (May 21 2018 at 22:57, on Zulip):

yeah — I hoped to compare at least to the timely one but it doesn't find any errors

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

@nikomatsakis https://github.com/rust-lang-nursery/polonius/pull/41 and https://github.com/rust-lang-nursery/polonius/pull/34, #34 builds on top of #41 so I'd probably need to rebase #34 after #41 is merged

lqd (May 22 2018 at 08:49, on Zulip):

@Santiago Pastorino nice job on the #34 rewrite :) a couple of things: 1) invalidates_lp is an index over static data, we don't need to remap it as no new facts will be added during the iteration 2) and since it's static data you could also get rid of the invalidates + invalidates_lp copy, one of those 2 is not strictly necessary and one could fill it in the "((loan, point) ())" format directly before the iteration

lqd (May 22 2018 at 11:16, on Zulip):

I guess I should have left those on github, a bit easier to review with all the information in a single place

Santiago Pastorino (May 22 2018 at 11:32, on Zulip):

that makes perfect sense

Santiago Pastorino (May 22 2018 at 11:32, on Zulip):

unsure why I did it the way I did

Santiago Pastorino (May 22 2018 at 11:33, on Zulip):

fixed /cc @nikomatsakis

lqd (May 22 2018 at 11:35, on Zulip):

nice :)

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

@Santiago Pastorino let me know if you have the output from your analysis for issue-47680

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

I can kind of sanity check it

Santiago Pastorino (May 22 2018 at 13:32, on Zulip):

potential_errors is empty

nikomatsakis (May 22 2018 at 13:33, on Zulip):

ok, I think that is almost certainly wrong

Santiago Pastorino (May 22 2018 at 13:33, on Zulip):

because borrow_live_at is empty

nikomatsakis (May 22 2018 at 13:34, on Zulip):

huh, that seems wrong

Santiago Pastorino (May 22 2018 at 13:34, on Zulip):

for both main and maybe_next

Santiago Pastorino (May 22 2018 at 13:34, on Zulip):

sorry, sorry, for main borrow_live_at is not empty

nikomatsakis (May 22 2018 at 13:35, on Zulip):

I think that main is the function of interest

nikomatsakis (May 22 2018 at 13:35, on Zulip):

I guess I could build locally and inspect

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

hmm I'm not dumping invalidates

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

need to see what's that

nikomatsakis (May 22 2018 at 13:35, on Zulip):

probably because that's an input

lqd (May 22 2018 at 13:35, on Zulip):

I have a lead

lqd (May 22 2018 at 13:36, on Zulip):

crate invalidates: Vec<(Loan, Point)> but the data looks like "Start(bb1[0])" "bw1" eg the reverse order ?

lqd (May 22 2018 at 13:38, on Zulip):

@Santiago Pastorino

Santiago Pastorino (May 22 2018 at 13:38, on Zulip):

:)

Santiago Pastorino (May 22 2018 at 13:39, on Zulip):

that was one of the things I needed to check

Santiago Pastorino (May 22 2018 at 13:39, on Zulip):

also ... why are we only filling borrow_live_at for results and then trying to dump everything?

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

shouldn't we fill all the stuff if the thing was run with verbose?

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

so ... my question is about this part https://github.com/rust-lang-nursery/polonius/pull/34/files#diff-2cacc48f0a2b0432151b6f258162f827R96

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

we were only filling borrow_live_at and I've changed to fill potential_errors (and I think what I did is not right)

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

but shouldn't we fill all there?

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

@Santiago Pastorino I don't understand what you're asking :(

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

ok

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

first of all I was doing it wrong

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

the current code is giving

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

# potential_errors

"Mid(bb3[2])" "bw1"
"Mid(bb10[2])" "bw2"

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

then we are filling only 1 part of Output

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

left a comment btw

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

and trying to dump all

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

so

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

let me show you the code

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

which might answer this

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

that doesn't answer exactly

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

this one was another question I have

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

this error "Mid(bb3[2])" "bw1" certainly seems right

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

let me show you two things

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

I have two questions

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

the first is about master

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

not related with my PR

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

https://github.com/rust-lang-nursery/polonius/blob/master/src/output/location_insensitive.rs#L81-L87

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

ok

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

here we fill result

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

right

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

and here https://github.com/rust-lang-nursery/polonius/blob/master/src/output/mod.rs#L66-L95 we dump

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

what I'm saying is that dump_enabled doesn't work

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

because stuff is never filled

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

yeah, seems like that got lost somewhere along the way

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

we used to check if dump_enabled and add in the data in that case

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

exactly

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

will add that

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

and the other question was exactly what you've said

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

the already discussed this

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

don't remember very well

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

but seems like we want potential_errors outside dump_enabled

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

confirm

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

the thing is that is only right for insensitive

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

actually, I think that borrow_live_at should go into dump_enabled — eventually

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

we would have to extend datafrogopt to use invalidates

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

which,...we should do

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

it's more-or-less the same code you already wrote

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

ok

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

so datafrogopt also uses potential_errors

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

?

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

no

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

er

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

what do you mean :)

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

it doesn't now

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

well, I guess it would produce not "potential errors" but "true errors"

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

but I think it's fine to just rename potential_errors to errors for now

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

or to use the same vector anyway

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

if you want I can walk through how to interpret that output

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

so we can decide if it is legit :)

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

:+1:

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

first off you have to run -Zdump-mir=nll, here is that output (gisted)

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

yep

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

we can also use the borrow_region.facts to figure out which borrow index corresponds to what :)

"\'_#2r"    "bw0"   "Mid(bb0[3])"
"\'_#3r"    "bw1"   "Mid(bb3[2])"
"\'_#5r"    "bw2"   "Mid(bb10[2])"
nikomatsakis (May 22 2018 at 14:18, on Zulip):

i.e., bw1 is the loan at bb3[2], and bw2 is the loan at bb10[2]

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

those are the two potential errors we saw:

"Mid(bb3[2])" "bw1"
"Mid(bb10[2])" "bw2"
nikomatsakis (May 22 2018 at 14:19, on Zulip):

interestingly, both of them at the point of borrow. This is actually roughly what I expected.

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

:+1:

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

if you look at the input:

fn main() {
    let mut temp = &mut Thing;

    loop {
        match temp.maybe_next() {
            Some(v) => { temp = v; }
            None => { }
        }
    }
}
nikomatsakis (May 22 2018 at 14:20, on Zulip):

the first is saying that when you invoke temp.maybe_next(), it thinks temp is still borrowed

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

in fact, you need location-sensitivity to understand why that is not the case =)

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

:)

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

if you compare to the current NLL analysis, running on play, you will see we get a similar error:

error[E0499]: cannot borrow `*temp` as mutable more than once at a time
  --> src/main.rs:13:15
   |
13 |         match temp.maybe_next() {
   |               ^^^^
   |               |
   |               mutable borrow starts here in previous iteration of loop
   |               borrow later used here
nikomatsakis (May 22 2018 at 14:21, on Zulip):

the current NLL analysis (that is, what is running on rustc) is also location insensitive

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

yep

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

:+1:

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

anyway the other error I suspect is similar

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

so basically " looks good :crab: "

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

(the second error is occurring at the point of a reborrow)

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

I think that occurs because this analysis is even more location insensitive than what is on master right now

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

I've force pushed

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

I've force pushed

we should be able to add a #[test] for this case I think — basically asserting that your result gets the result it does

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

I guess we can merge this, then I can first make dump_enabled work

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

and then make all use potential_errors or something

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

I've force pushed

we should be able to add a #[test] for this case I think — basically asserting that your result gets the result it does

:+1:

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

@nikomatsakis test added and force pushed again

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

stray println in the test ? :)

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

println in test is harmless

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

though maybe not desired

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

@Santiago Pastorino great! merged.

Santiago Pastorino (May 22 2018 at 15:04, on Zulip):

just copied that from the other test :)

Last update: Nov 21 2019 at 14:15UTC