Stream: t-compiler/wg-nll

Topic: location-insensitive pre-pass (#29)


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

Spinning off from #4, I was thinking that a way to go faster would be to do a "location-insensitive pre-pass". I sketched the idea here https://github.com/rust-lang-nursery/borrow-check/issues/29. Basically we can do a less precise analysis, find out where errors might lie, and then do the more precise version only for those loans etc that are potentially problematic.

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

@Santiago Pastorino one thing to clarify — re: #29 — although we sketched out how to compute the transitive closure for the subset relation, I don't actually think we need to do that in the code

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

I do think we'll want to compute the transitive requires relation

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

or at least somewhere we need transitivity :)

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

in #29, I sketched out the requires relation like so:

requires(R1, L1) :- borrow_region(R1, L1, _P).
requires(R2, L1) :- requires(R1, L1), subset(R1, R2).

This version, notably, doesn't require a transitive subset relation to be correct — the second clause will propagate "along" the subset relation. So e.g. if you have two tuples:

R1 <= R2
R2 <= R3

and you have borrow_region(R1, L0), then the second rule would compute a first pass with just one fact:

requires(R1, L0)

On the second pass, it would use that fact to compute:

requires(R2, L0)

and then in the third round it would add requires(R3, L0).

Santiago Pastorino (May 15 2018 at 17:36, on Zulip):

hey, I'm back, going to start, thanks for the comments

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

@Santiago Pastorino how goes?

lqd (May 15 2018 at 18:30, on Zulip):

(btw I tried earlier these rules with soufflé on clap, and it was indeed fast, a good sign since it should be faster with the Invalidates facts)

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

one thing I am not sure about: today's borrow checker is location-sensitive for the requires relation, but not the subset. We may want that. But since this is only a "pre-filter", we may find we don't need it.

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

@nikomatsakis was interrupted here several times so I'm reading the thing and now focused to do it

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

was reading the issue

Santiago Pastorino (May 15 2018 at 18:46, on Zulip):
// requires(R1, L1) :- borrow_region(R1, L1, _P).
Santiago Pastorino (May 15 2018 at 18:46, on Zulip):

@nikomatsakis for this example borrow_region is declared, right?

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

what do you mean by "declared"?

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

oh, well, borrow_region is an input

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

that is, it comes from AllFacts

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

like outlives

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

yes

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

so it comes with a .decl clause

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

in datalog

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

yeah, and a .input as well, strictly speaking :)

lqd (May 15 2018 at 18:48, on Zulip):

.decl + input yes

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

yep

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

just in case asking :)

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

I was trying to mimic what you were doing like in here ...

Santiago Pastorino (May 15 2018 at 18:51, on Zulip):
                // .decl subset(Ra, Rb) -- `R1 <= R2` holds
                //
                // subset_base(Ra, Rb) :- outlives(Ra, Rb, _P)
Santiago Pastorino (May 15 2018 at 18:51, on Zulip):

but unsure why you use .decl, didn't you mean input?

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

nope

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

I don't think I added comments for the inputs

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

but rather the "derived relations"

lqd (May 15 2018 at 18:52, on Zulip):

@Santiago Pastorino here's how it looks with the naive rules for the soufflé datalog engine https://gist.github.com/lqd/1db97eb478a504314cc47d7d087faefe

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

so in this case there might be something like: // .decl requires(R, L)

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

@nikomatsakis maybe explain what you mean exactly in that comment?

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

I read that as a declaration

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

and then it could come from input or derived

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

if my definition is right, decl by itself unsure what is telling me

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

@Santiago Pastorino that is correct, but subset is not coming from AllFacts

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

outlives is

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

@Santiago Pastorino here's how it looks with the naive rules for the soufflé datalog engine https://gist.github.com/lqd/1db97eb478a504314cc47d7d087faefe

checking ...

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

the inputs come from AllFacts, you can see them being setup here

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

if my definition is right, decl by itself unsure what is telling me

it's just telling you what the "types" of the tuple are

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

ahh so you're adding decl for stuff that is not in AllFacts?

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

right

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

ok

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

the types for AllFacts you can find in the struct itself

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

so I didn't bother to document them

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

ok

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

truth is, it doesn't tell you that much :)

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

also

Santiago Pastorino (May 15 2018 at 18:56, on Zulip):
                    let borrow_region = borrow_region.enter(&requires.scope());
                    let subset = subset.enter(&requires.scope());
                    let killed = killed.enter(&requires.scope());
                    let region_live_at = region_live_at.enter(&requires.scope());
                    let cfg_edge = cfg_edge.enter(&requires.scope());
                    let universal_region = universal_region.enter(&requires.scope());
Santiago Pastorino (May 15 2018 at 18:57, on Zulip):

why did you do all that in the naive part?

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

you need to do that whenever you have an iterate call

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

ahh I remember you mention something about this subtlety in the video

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

yep

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

ok

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

that is how you bring the things from "outside" the iteration into scope

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

within the iteration

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

if you don't do that, you will find you get various compilation errors :)

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

:)

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

@nikomatsakis a couple of questions ...

nikomatsakis (May 15 2018 at 20:02, on Zulip):

ok, ask quick :) I am leaving in 2 minutes

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

1. what am I supposed to do with borrow_live_at?

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

2. I have some stuff unsure if I'm in the right direction :P

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

2 is not a question, it's kind you look at the code and tell me if we are going in good direction :), hehe

nikomatsakis (May 15 2018 at 20:04, on Zulip):

1. what am I supposed to do with borrow_live_at?

I think we can define it like:

borrow_live_at(L, P) :-
  requires(R, L), region_live_at(R, P)
Santiago Pastorino (May 15 2018 at 20:04, on Zulip):

maybe I need to figure out how to test this

nikomatsakis (May 15 2018 at 20:04, on Zulip):

2. I have some stuff unsure if I'm in the right direction :P

send me a link ?

nikomatsakis (May 15 2018 at 20:04, on Zulip):

maybe I need to figure out how to test this

well, this is the problem :) this is why I was saying we need to work on the integration

nikomatsakis (May 15 2018 at 20:04, on Zulip):

I basically don't know how to test

nikomatsakis (May 15 2018 at 20:04, on Zulip):

but I can probably vet it pretty easily for now

nikomatsakis (May 15 2018 at 20:04, on Zulip):

ok, gotta go, I may be reachable on mobile

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

https://gist.github.com/spastorino/2913826a97e56aa5f3470152d3ec4c04

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

mainly check the requires part

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

@Santiago Pastorino the requires is not quite setup right

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

The return value of iterate closure should include the base facts too

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

If you look at the transitive subset relation we setup you will see what I mean

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

Also it occurs to me can can write some unit tests with hard coded facts

lqd (May 15 2018 at 22:05, on Zulip):

should requires also depend on subset rather than subset_base ?

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

The return value of iterate closure should include the base facts too

can you explain why?

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

I may have thought in a wrong way

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

what I thought was exactly that those facts were already included in subsets, why do I need to add that in requires?

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

I'm not quite sure I understand

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

so you have:

                // requires(R, L) :- borrow_region(R, L, _P).
                let requires = borrow_region
                    .map(|(r, l, _p)| (r, l))
                    .distinct_total();

                // requires(R2, L) :- requires(R1, L), subset(R1, R2).
                let requires = requires.iterate(|requires| {
                    let subset_base = subset_base.enter(&requires.scope());

                    requires
                        .join(&subset_base)
                        .map(|(r1, l, r2)| (r2, l))
                        .distinct_total()
                });
nikomatsakis (May 15 2018 at 22:39, on Zulip):

but you need something like:

                // requires(R, L) :- borrow_region(R, L, _P).
                let requires_base = borrow_region
                    .map(|(r, l, _p)| (r, l))
                    .distinct_total();

                // requires(R2, L) :- requires(R1, L), subset(R1, R2).
                let requires = requires_base.iterate(|requires| {
                    let subset_base = subset_base.enter(&requires.scope());
                    let requires_base = requires_base.enter(&requires.scope());

                    let requires1 = requires_base.clone();

                    let requires2 = requires
                        .join(&subset_base)
                        .map(|(r1, l, r2)| (r2, l));

                    requires1.concat(&requires2).distinct_total()
                });
nikomatsakis (May 15 2018 at 22:39, on Zulip):

should requires also depend on subset rather than subset_base ?

well, yes, but really the distinction isnt' needed; that is, we should remove subset (which is just transitive closure of subset_base) and rename subset_base to subset

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

@Santiago Pastorino

can you explain why?

anyway, the reason for that setup:

this return set doesn't have to include the tuples from round N; but in our case, we want it to, because we want the final set to be strictly growing and getting bigger

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

ahhh I see

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

this explaination makes sense

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

will get back to this tomorrow

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

ah yes haha, I had tested the query before and actually forgot we specifically didn't want the subset TC here :sob:

nikomatsakis (May 16 2018 at 12:01, on Zulip):

btw, @Santiago Pastorino, as I was saying in this message I resurrected my branch of rustc that directly uses the borrow-check logic. We could in principle test your analysis by forking this branch and copying-and-pasting it in. It's not very convenient but it would be a kind of "sanity check"

Santiago Pastorino (May 16 2018 at 12:10, on Zulip):

ok

Santiago Pastorino (May 16 2018 at 12:10, on Zulip):

yeah, when I've said test yesterday I didn't mean to do anything fancy, just run the thing and see if it does something :)

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

but anyway, what you say seems to make more sense anyway (?)

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

well it would be nice if we had a cleaner way of integrating the borrow-check execution with rustc

Santiago Pastorino (May 16 2018 at 12:34, on Zulip):

@nikomatsakis in the code you pasted yesterday

Santiago Pastorino (May 16 2018 at 12:34, on Zulip):

do we need to call distinct_total or distinct?

Santiago Pastorino (May 16 2018 at 12:34, on Zulip):

you put distinct_total but in naive analysis for requires distinct is being called

Santiago Pastorino (May 16 2018 at 12:35, on Zulip):

unsure if in this part we have the subtleties you mentioned me on the call

lqd (May 16 2018 at 12:35, on Zulip):

distinct_total (distinct does more stuff we probably don't need here, IIRC)

Santiago Pastorino (May 16 2018 at 12:36, on Zulip):

yep, Niko told me that yesterday

Santiago Pastorino (May 16 2018 at 12:36, on Zulip):

but in naive for the same case distinct was called

Santiago Pastorino (May 16 2018 at 12:36, on Zulip):

so I was unsure if was a case where we need it or not

Santiago Pastorino (May 16 2018 at 12:37, on Zulip):

anyway, it's true that naive requires part is more complex than this one ... so ... unsure

Santiago Pastorino (May 16 2018 at 12:37, on Zulip):

will leave as distinct_total then :)

nikomatsakis (May 16 2018 at 12:37, on Zulip):

@Santiago Pastorino they could both be distinct_total

lqd (May 16 2018 at 12:37, on Zulip):

Naive is older and less optimized yeah

Santiago Pastorino (May 16 2018 at 12:38, on Zulip):

ok

nikomatsakis (May 16 2018 at 12:38, on Zulip):

I left it that way to make timely-opt look faster in comparison :P

Santiago Pastorino (May 16 2018 at 12:38, on Zulip):

hehe

nikomatsakis (May 16 2018 at 12:38, on Zulip):

(and because I didn't want to change it — it is kind of the "most obviously correct" thing the way it is)

Santiago Pastorino (May 16 2018 at 13:24, on Zulip):

@nikomatsakis so ... as we were talking yesterday, in location insensitive we also want borrow_live_at which considers a fixed point P, right?

nikomatsakis (May 16 2018 at 13:24, on Zulip):

yeah, but it would use the results of the requires location which doesn't take P

Santiago Pastorino (May 16 2018 at 13:24, on Zulip):

exactly

nikomatsakis (May 16 2018 at 13:25, on Zulip):

so basically the "location sensitivity" comes from the region_live_at tuples

Santiago Pastorino (May 16 2018 at 13:25, on Zulip):

yes

Santiago Pastorino (May 16 2018 at 13:26, on Zulip):

what about universal regions?

nikomatsakis (May 16 2018 at 13:28, on Zulip):

heh, good timing for that question

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

I'm planning to remove that distinction; see this comment

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

but for now you could transform the universal_regions facts into region_live_at facts the same way that timely_opt does

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

ok

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

(I linked to the code in that comment)

Santiago Pastorino (May 16 2018 at 13:30, on Zulip):

:+1:

Santiago Pastorino (May 16 2018 at 15:29, on Zulip):
                // borrow_live_at(L, P) :-
                //     requires(R, L), region_live_at(R, P)
                let borrow_live_at = requires
                    .semijoin(&region_live_at)
                    .map(|(_r, l, p)| (l, p));
Santiago Pastorino (May 16 2018 at 15:29, on Zulip):

I'm getting this ...

Santiago Pastorino (May 16 2018 at 15:29, on Zulip):
error[E0308]: mismatched types
   --> src/output/location_insensitive.rs:132:31
    |
132 |                     .semijoin(&region_live_at)
    |                               ^^^^^^^^^^^^^^^ expected struct `facts::Region`, found tuple
    |
    = note: expected type `&differential_dataflow::Collection<timely::dataflow::scopes::Child<'_, timely::dataflow::scopes::Root<timely_communication::allocator::generic::Generic>, ()>, facts::Region, _>`
               found type `&differential_dataflow::Collection<timely::dataflow::scopes::Child<'_, timely::dataflow::scopes::Root<timely_communication::allocator::generic::Generic>, ()>, (facts::Region, facts::Point)>`
Santiago Pastorino (May 16 2018 at 15:30, on Zulip):

unsure exactly why is semijoin expecting that

Santiago Pastorino (May 16 2018 at 15:31, on Zulip):

maybe that's affected after the fix for universal regions?

Santiago Pastorino (May 16 2018 at 15:31, on Zulip):

no, it's not

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

can you send me link to the current commit?

Santiago Pastorino (May 16 2018 at 15:33, on Zulip):

sure

Santiago Pastorino (May 16 2018 at 15:33, on Zulip):

gimme a sec

Santiago Pastorino (May 16 2018 at 15:34, on Zulip):

https://github.com/spastorino/borrow-check/commit/b08864f42c14bb69c004215deca6639d4a64668c

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

I think you just want join

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

not semijoin

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

that is, you want to take information from both sides

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

the L from one, the P from the other

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

semijoin is more like "intersect"

Santiago Pastorino (May 16 2018 at 15:36, on Zulip):

can you explain again the difference?

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

it's roughly what I just wrote :0

Santiago Pastorino (May 16 2018 at 15:36, on Zulip):

ok

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

that is, if you do foo.semijoin(bar)

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

that is basically foo - bar

Santiago Pastorino (May 16 2018 at 15:37, on Zulip):

I read something about empty collections for semijoin

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

er

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

sorry

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

foo && bar

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

like, the tuples that are in both

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

but for that to make sense they must have the same types of tuples

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

that's not 100% true, I think it only considers the first half of foo...

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

that is, foo might look like (K, V) but then bar must have type K

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

in this case you have foo with type (R, L) and bar with type (R, P)

Santiago Pastorino (May 16 2018 at 15:42, on Zulip):

:+1:

Santiago Pastorino (May 16 2018 at 15:42, on Zulip):

another thing now

Santiago Pastorino (May 16 2018 at 15:42, on Zulip):

what do you want to do with the dump_enabled part?

Santiago Pastorino (May 16 2018 at 15:43, on Zulip):

should I make that work? remove something or what's the idea?

Santiago Pastorino (May 16 2018 at 15:44, on Zulip):

and case to make it work, Output struct for subset has Point, Region, Region, now there's no Point anymore

Santiago Pastorino (May 16 2018 at 15:44, on Zulip):

we want to create a new Output struct?

Santiago Pastorino (May 16 2018 at 15:45, on Zulip):

or what was your idea?

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

hmm good question =)

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

I guess add more fields .. ?

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

it seems ok to add more fields

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

that is, those are basically meant to be debug data

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

so if we have a subset_anywhere field or something

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

and at most one has data

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

depending on the algorithm

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

that .. would be ok

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

probably a good idea to add that so that we can at least dump the results

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

and get some idea what it is doing :)

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

ok

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

@nikomatsakis what's update_degrees ?

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

that also needs a Point

nikomatsakis (May 16 2018 at 16:20, on Zulip):

oh, you can just delete that

nikomatsakis (May 16 2018 at 16:21, on Zulip):

that was tracking the in-degree and out-degree of each region in the subset graph

nikomatsakis (May 16 2018 at 16:21, on Zulip):

(we could probably just delete that whole set of code...)

nikomatsakis (May 16 2018 at 16:21, on Zulip):

but at least I would delete the call in your branch

nikomatsakis (May 16 2018 at 16:21, on Zulip):

er, your module

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

hey, back ... ok :+1:

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

@nikomatsakis https://github.com/spastorino/borrow-check/commit/18c5b7f63db904c71f61391add1ae50a93a88495

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

it's kind of ready I guess

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

unsure how to follow

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

at least is compiling

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

haven't tried anything with it yet

lqd (May 16 2018 at 17:18, on Zulip):

maybe remove the subset transitive closure ? :)

lqd (May 16 2018 at 17:18, on Zulip):

(the part marked with "remove this")

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

ouch :)

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

hehe

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

I need to code review myself again

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

fixed

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

and maybe even better

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

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

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

@nikomatsakis @lqd :point_up:

lqd (May 16 2018 at 17:23, on Zulip):

@Santiago Pastorino good job :) did you try to run it on clap to see how fast it runs btw ?

Santiago Pastorino (May 16 2018 at 17:24, on Zulip):

haven't done anything yet

Santiago Pastorino (May 16 2018 at 17:24, on Zulip):

just pushed that to start discussing following steps

Santiago Pastorino (May 16 2018 at 19:43, on Zulip):
[santiago@archlinux borrow-check (location_insensitive)]$ cargo run --release -- --skip-tuples inputs/clap-rs/app-parser-\{\{impl\}\}-add_defaults/ | head
    Finished release [optimized] target(s) in 0.07s
     Running `target/release/borrow-check --skip-tuples 'inputs/clap-rs/app-parser-{{impl}}-add_defaults/'`
--------------------------------------------------
Directory: inputs/clap-rs/app-parser-{{impl}}-add_defaults/
Time: 117.131s
[santiago@archlinux borrow-check (location_insensitive)]$ cargo run --release -- --skip-tuples -a LocationInsensitive inputs/clap-rs/app-parser-\{\{impl\}\}-add_defaults/ | head
    Finished release [optimized] target(s) in 0.07s
     Running `target/release/borrow-check --skip-tuples -a LocationInsensitive 'inputs/clap-rs/app-parser-{{impl}}-add_defaults/'`
--------------------------------------------------
Directory: inputs/clap-rs/app-parser-{{impl}}-add_defaults/
Time: 2.058s
Santiago Pastorino (May 16 2018 at 19:44, on Zulip):

it's just a bit faster :P

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

~57x faster for that example

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

unsure how representative it is

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

just for comparison how fast does -a timelyoptrun on your machine btw ?

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

(Naive — the default slow one is mostly here for "historical" purposes :)

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

~8x faster

Santiago Pastorino (May 16 2018 at 19:55, on Zulip):
[santiago@archlinux borrow-check (location_insensitive)]$ cargo run --release -- --skip-tuples -a TimelyOpt inputs/clap-rs/app-parser-\{\{impl\}\}-add_defaults/ | head
    Finished release [optimized] target(s) in 0.10s
     Running `target/release/borrow-check --skip-tuples -a TimelyOpt 'inputs/clap-rs/app-parser-{{impl}}-add_defaults/'`
--------------------------------------------------
Directory: inputs/clap-rs/app-parser-{{impl}}-add_defaults/
Time: 16.729s
lqd (May 16 2018 at 19:56, on Zulip):

awesome, thank you

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

:+1:

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

also added that info to the PR

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

hopefully adding the Invalidates facts allows avoiding even more computation, as this would just be a first quick pass, before timelyopt

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

(I think, at least :)

nikomatsakis (May 16 2018 at 20:36, on Zulip):

@Santiago Pastorino nice! So

nikomatsakis (May 16 2018 at 20:37, on Zulip):

the next part is the interesting part, really :)

Santiago Pastorino (May 16 2018 at 20:38, on Zulip):

:)

Santiago Pastorino (May 16 2018 at 20:38, on Zulip):

shoot

nikomatsakis (May 16 2018 at 20:39, on Zulip):

the one funny thing about zulip :)

nikomatsakis (May 16 2018 at 20:39, on Zulip):

threads are so good at keeping state

nikomatsakis (May 16 2018 at 20:39, on Zulip):

I have to decide what to put in the issue vs here ;)

nikomatsakis (May 16 2018 at 20:40, on Zulip):

luckily we can have good links :)

nikomatsakis (May 16 2018 at 20:40, on Zulip):

anyway, the idea is roughly what @lqd said: that we can use this as a pre-pass to narrow down where we might have errors

nikomatsakis (May 16 2018 at 20:40, on Zulip):

specifically, which (L, P) points may be in error

nikomatsakis (May 16 2018 at 20:41, on Zulip):

to truly figure that out we need the invalidates facts that @Reed Koser has a PR for

nikomatsakis (May 16 2018 at 20:41, on Zulip):

but we can do some of the follow-up work even now

nikomatsakis (May 16 2018 at 20:41, on Zulip):

just "as if" we had them

nikomatsakis (May 16 2018 at 20:41, on Zulip):

the idea then is: if we know which (L, P) pairs are potentially in error,

nikomatsakis (May 16 2018 at 20:42, on Zulip):

we should be able to narrow down and avoid work

nikomatsakis (May 16 2018 at 20:45, on Zulip):

one annoying problem:

nikomatsakis (May 16 2018 at 20:45, on Zulip):

without some integration into rustc

nikomatsakis (May 16 2018 at 20:45, on Zulip):

it's going to be kinda hard to test this

nikomatsakis (May 16 2018 at 20:46, on Zulip):

@Santiago Pastorino let me first check your PR :)

nikomatsakis (May 16 2018 at 20:48, on Zulip):

looks pretty good, found one nit

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

I have to run to a meeting now

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

hey just checked all this, tomorrow morning will try to tackle some of the stuff, did you open an issue?

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

and fixed the PR

nikomatsakis (May 17 2018 at 08:09, on Zulip):

I didn't open a new issue, I think this still falls under the original one

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

hey @nikomatsakis I'm with time now to tackle this

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

but unsure I follow exactly what's next

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

the information of what needs to be done you said is in the issue?

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

yeah, sort of — sorry, in rustc meeting right now, but done soon

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

ok, @Santiago Pastorino, I'm around now, are you?

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

(deleted)

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

@nikomatsakis back

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

ok so @Santiago Pastorino I'm skimming to see if I left any relevant notes anywhere ;)

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

we have to kind of decide where in the pipeline to start from

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

are you clear on the overall flow I have in mind though? (like, how we can use this "prepass" to speed up second half?)

Santiago Pastorino (May 17 2018 at 15:52, on Zulip):

so ... what I got is that you want to run this first because a lot of programs may just be ok with it

Santiago Pastorino (May 17 2018 at 15:52, on Zulip):

and if fails

Santiago Pastorino (May 17 2018 at 15:52, on Zulip):

we need finer grained checks like what other algorithms do

Santiago Pastorino (May 17 2018 at 15:52, on Zulip):

I don't know exactly what timely_opt does

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

right so

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

the idea is also that from this first analysis

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

we can get back a set of (L, P) pairs where there may be errors

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

i.e., this loan L is invalidated at the point P, but it is still required because of some live references

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

in fact, we can actually get (R, L, P) pairs I suppose

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

where R is the region of the live reference

Santiago Pastorino (May 17 2018 at 15:55, on Zulip):
potential_errors(R, L, P) :-
  invalidated(L, P),
  requires(R, L),
  region_live_at(R, P).
Santiago Pastorino (May 17 2018 at 15:56, on Zulip):

well with R added you said

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

so there are two important parts to flesh out (but maybe not in this order):

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

yeah that's the basic idea

Santiago Pastorino (May 17 2018 at 15:58, on Zulip):

what does how do we go from the results you have to those (R, L, P) errors? means?

Santiago Pastorino (May 17 2018 at 15:58, on Zulip):

my question is related to my english disability to understand exactly what do I need to do with that

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

given those (R, L, P) tuples, how can we use that to speed up the second analysis? what's the "second" analysis?

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

my thought was maybe we should play with this, and synthesize some of the tuples oursleves for testing purposes, but I'm not 100% sure not sure what this means

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

so 3 questions :)

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

what does how do we go from the results you have to those (R, L, P) errors? means?

currently your branch computes region_live_at tuples or something like that, right?

nikomatsakis (May 17 2018 at 16:00, on Zulip):

all I was saying is: we could try to implement these rules that you already gave

nikomatsakis (May 17 2018 at 16:00, on Zulip):

given those (R, L, P) tuples, how can we use that to speed up the second analysis? what's the "second" analysis?

the second one is the "precise one" — TimelyOpt. Put another way, your "location insensitive analysis" would get integrated into TimelyOpt, not be a distinct thing.

nikomatsakis (May 17 2018 at 16:01, on Zulip):

my thought was maybe we should play with this, and synthesize some of the tuples oursleves for testing purposes, but I'm not 100% sure not sure what this means

OK, so, the pipeline is this:

nikomatsakis (May 17 2018 at 16:01, on Zulip):
nikomatsakis (May 17 2018 at 16:02, on Zulip):
nikomatsakis (May 17 2018 at 16:02, on Zulip):

internally, TrueError(L, P) is based on the same rules as today, but we only have to compute it for those (L, P) pairs for which there are potential errors

Santiago Pastorino (May 17 2018 at 16:04, on Zulip):

got it

Santiago Pastorino (May 17 2018 at 16:04, on Zulip):

makes perfect sense

Santiago Pastorino (May 17 2018 at 16:04, on Zulip):

that doesn't mean I won't have more questions, though :P

nikomatsakis (May 17 2018 at 16:05, on Zulip):

@Santiago Pastorino so specifically I was thinking we should focus on this very last bit

nikomatsakis (May 17 2018 at 16:06, on Zulip):

how can we speed up timely-opt given that set of potential errors

nikomatsakis (May 17 2018 at 16:06, on Zulip):

I think it is roughly this:

nikomatsakis (May 17 2018 at 16:06, on Zulip):

we can use the subset_anywhere and requires_anywhere relations you've already built

nikomatsakis (May 17 2018 at 16:06, on Zulip):

to find out which regions might be involved

nikomatsakis (May 17 2018 at 16:07, on Zulip):

then we can limit the subset computation to only take place for those regions

nikomatsakis (May 17 2018 at 16:07, on Zulip):

maybe we should rename things, e.g. subset_anywhere and subset_somewhere

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

so you want me to start from this last part?

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

if I got it correctly first part shouldn't be hard

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

I mean, I just need to figure out how to add invalidates

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

and from there should be easy

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

but anyway I can start from that last part

nikomatsakis (May 17 2018 at 16:40, on Zulip):

so you want me to start from this last part?

I think so? but we could look at the first part too, it's just that it needs some Invalidates tuples as inputs

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

that part kind of continues the other PR I had

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

which just added the fields

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

but yeah, I guess we would need a proper invalidates input file

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

you said that I can get that from Reed's PR, right?

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

we can yes

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

if you do a local build

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

we need a test too

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

https://github.com/rust-lang-nursery/polonius/pull/32 done!

nikomatsakis (May 17 2018 at 17:34, on Zulip):

merged

nikomatsakis (May 17 2018 at 17:40, on Zulip):

so do you know what to do next?

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

yes

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

going to start now

nikomatsakis (May 17 2018 at 17:42, on Zulip):

ok. I'm not sure I know what you are going to do but I'm excited to see =)

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

it's a surprise

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

:P

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

that you will figure out right now because I have a question

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

lol

Santiago Pastorino (May 17 2018 at 17:46, on Zulip):
                // potential_errors(R, L, P) :-
                //   invalidated(L, P),
                //   requires(R, L),
                //   region_live_at(R, P).
Santiago Pastorino (May 17 2018 at 17:46, on Zulip):

isn't that equals to ...

Santiago Pastorino (May 17 2018 at 17:46, on Zulip):
                // potential_errors(R, L, P) :-
                //   invalidated(L, P),
                //   borrow_live_at(L, P)
Santiago Pastorino (May 17 2018 at 17:47, on Zulip):

I know it lacks the R

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

now I wonder if we should discard R from borrow_live_at

nikomatsakis (May 17 2018 at 17:50, on Zulip):

that looks equivalent, yes

nikomatsakis (May 17 2018 at 17:50, on Zulip):

I'm not sure if we need the R

nikomatsakis (May 17 2018 at 17:50, on Zulip):

we can start without it

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

ok

nikomatsakis (May 17 2018 at 17:50, on Zulip):

originally I just had in mind to narrow down to a set of (L, P) pairs

nikomatsakis (May 17 2018 at 17:50, on Zulip):

or even just loans

nikomatsakis (May 17 2018 at 17:50, on Zulip):

but both seem useful:

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

e.g., we only need the information for the loan L for those points on the path from the entry to P

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

but maybe we just start by narrowing down to gather facts for a specific loan

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

we could actually test that independently pretty easily

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

invalidated or invalidates?

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

have seen both terms used

nikomatsakis (May 17 2018 at 17:53, on Zulip):

I think invalidates — I feel like we mostly use present tense :)

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

:+1:

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

another question, why borrow_live_at lives outside of if dump_enabled?

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

maybe I added it in the wrong place :smiley:

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

?

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

checking

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

well in naive algorithm happens the same

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

it was just copied and pasted

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

unsure if that's fine or should all be inside of dump_enabled

nikomatsakis (May 17 2018 at 17:57, on Zulip):

another question, why borrow_live_at lives outside of if dump_enabled?

do you mean, if dump_enabled is false, then when do we still compute borrow_live_at ?

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

yes

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

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

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

if so, the reason is because — in the absence of invalidates facts — that was the "final output" from the analysis

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

is outside the if dump_enabled

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

which we then fed to the borrow checker

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

once we add the invalidates though, we should be able to change that

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

so it is just an 'internal detail'

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

and we want to return invalidates?

nikomatsakis (May 17 2018 at 17:59, on Zulip):

and the final output is rather the (L, P) pairs

nikomatsakis (May 17 2018 at 17:59, on Zulip):

no, invalidates is an input

nikomatsakis (May 17 2018 at 17:59, on Zulip):

telling us which loan is invalidated where

nikomatsakis (May 17 2018 at 17:59, on Zulip):

the output is the set of loans which are invalidated but still required

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

yep, I'm not sure how the output of this thing is used

nikomatsakis (May 17 2018 at 17:59, on Zulip):

(borrow_live_at tells us which loans are still required and where)

nikomatsakis (May 17 2018 at 17:59, on Zulip):

so it's basically the intersection of invalidates and borrow_live_at)

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

when I've said and we want to return invalidates? I meant we want to return potential_errors?

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

so that's basically what timely_opt will use

nikomatsakis (May 17 2018 at 18:06, on Zulip):

when I've said and we want to return invalidates? I meant we want to return potential_errors?

right

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

@nikomatsakis https://github.com/rust-lang-nursery/polonius/pull/34

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

to start discussion again

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

need to check this but I like to push soon

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

(in a call just now)

lqd (May 17 2018 at 18:30, on Zulip):

(the potential_errors(L, P) :- invalidates(L, P), borrow_live_at(L, P). is interesting because we can probably use a semijoin there)

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

doh, I forgot to fix that

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

a join is "wrong"

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

it's an intersection what we need there

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

going to check differential-dataflow API to check how to do an intersection

lqd (May 17 2018 at 18:36, on Zulip):

@Santiago Pastorino maybe something like invalidates.semijoin(&borrow_live_at)

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

semijoin is intersection?

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

where is that more or less explained?

lqd (May 17 2018 at 18:37, on Zulip):

it's a bit like filter IIRC (bear in mind I'm a beginner in this too)

lqd (May 17 2018 at 18:37, on Zulip):

https://docs.rs/differential-dataflow/0.5.0/differential_dataflow/operators/join/trait.Join.html#tymethod.semijoin

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

the thing is that uses a K and I have a pair

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

I would need to semijoin against the first element then reverse the pairs to semijoin against the second element and reverse again to return

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

semijoin is intersection?

yes

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

@nikomatsakis but it receives just one key

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

I guess I need to do what I've mentioned then

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

I would need to semijoin against the first element then reverse the pairs to semijoin against the second element and reverse again to return

:point_up:

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

@nikomatsakis but it receives just one key

well, it is sort of filter + intersection :) that is, you start out with a set of of type (K, V) and you semijoin with another set of type K; you get at the end all the (K, V) pairs where the keys appeared in both

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

probably, yes, or we could potentially reorder the arguments :) but as a general rule of thumb, map is pretty cheap

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

ok

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

thought there was a simpler way to do it

Santiago Pastorino (May 17 2018 at 19:06, on Zulip):
                let potential_errors = borrow_live_at
                    .semijoin(&invalidates.map(|(l, _p)| l))
                    .map(|(l, p)| (p, l))
                    .semijoin(&invalidates.map(|(_l, p)| p))
                    .map(|(p, l)| (l, p))
                    .distinct_total();
Santiago Pastorino (May 17 2018 at 19:08, on Zulip):

that's the way I can think of doing it

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

@Santiago Pastorino I'm a bit confused by your Pr

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

well, by that snippet you quoted right there, acutally

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

borrow_live_at has what type? doesn't it have the type (L, P)

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

oh I think I see

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

yah that's not right :P

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

I think we want to compute basically invalidates intersect borrow_live_at

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

you probably want to do:

nikomatsakis (May 17 2018 at 21:57, on Zulip):
borrow_live_at.map(|(l, p)| ((l, p), ()))
  .semijoin(&invalidates)
  .distinct_total()
nikomatsakis (May 17 2018 at 21:58, on Zulip):

the first map is the key :)

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

introducing the dummy () type means that the "key" you are intersecting on is the (l, p) pair

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

there should probably be a helper for that, blame @Frank McSherry :)

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

(or, I don't know, maybe there is...)

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

oh, I've tried something very similar but not that

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

did borrow_live_at.map(|(l, p)| ((l, p)))

nikomatsakis (May 17 2018 at 22:00, on Zulip):

ah

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

but you need a value, now I see :)

nikomatsakis (May 17 2018 at 22:00, on Zulip):

re: testing, it is hard to test the location-insensitive analysis in isolation

nikomatsakis (May 17 2018 at 22:00, on Zulip):

because it produces a different set of tuples from the location-sensitive one

nikomatsakis (May 17 2018 at 22:00, on Zulip):

so we can't compare them against each other

nikomatsakis (May 17 2018 at 22:00, on Zulip):

but if we add the invalidates facts

nikomatsakis (May 17 2018 at 22:00, on Zulip):

that is different

nikomatsakis (May 17 2018 at 22:00, on Zulip):

since now we shoudl be producing just the set of errors

nikomatsakis (May 17 2018 at 22:01, on Zulip):

and that should be a relatively small set we can inspect by hand

nikomatsakis (May 17 2018 at 22:01, on Zulip):

anyway, I gotta run now

nikomatsakis (May 17 2018 at 22:01, on Zulip):

I think what we're going to want to do next is to kind of integrate the location-insensitive and the timely-opt into one, as I was trying to describe earlier

nikomatsakis (May 17 2018 at 22:01, on Zulip):

roughly the idea is this:

nikomatsakis (May 17 2018 at 22:02, on Zulip):

actually, I'll note this part in github

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

never mind, that was a bit trickier than I thought

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

I wrote something but not much

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

@nikomatsakis don't remember what was expected for get_default but the example does not compile

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

anyway generated the facts, have the invalidates.facts in particular

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

@nikomatsakis I'm here

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

so

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

first get_default doesn't compile, I guess that was the expected result

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

anyway I got the invalidates.facts

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

have ran examples

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

we would need to check that everything is correct I guess :)

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

where are those formats explained?

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

and also ... should I use Reed's new example with it's inputs or get_default?

nikomatsakis (May 18 2018 at 13:07, on Zulip):

first get_default doesn't compile, I guess that was the expected result

yes, it is

nikomatsakis (May 18 2018 at 13:08, on Zulip):

and also ... should I use Reed's new example with it's inputs or get_default?

I think we should continue with get_default first

Santiago Pastorino (May 18 2018 at 13:08, on Zulip):
"Mid(bb5[1])"   "bw1"
nikomatsakis (May 18 2018 at 13:08, on Zulip):

the format is just one tuple per line, separated by tabs

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

I'm getting just that for ok function of get_default

nikomatsakis (May 18 2018 at 13:08, on Zulip):

which relation is that?

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

unsure what do you mean

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

where is that output coming from? :)

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

ok function of get_default.rs

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

let me paste the code

Santiago Pastorino (May 18 2018 at 13:10, on Zulip):
fn ok(map: &mut Map) -> &String {
    loop {
        match map.get() {
            Some(v) => {
                return v;
            }
            None => {
                map.set(String::new()); // Just AST errors here
                //~^ ERROR borrowed as immutable (Ast)
            }
        }
    }
}
Santiago Pastorino (May 18 2018 at 13:10, on Zulip):

would be nice to have the mir dump around for when you run the stuff

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

I'm generating it, otherwise I have no idea what bb5 is

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

:)

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

what is bw1?

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

@Santiago Pastorino that is "loan 1"

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

in the compiler, we still call that Borrow

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

and the Debug impl prints bw

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

ok :)

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

so basically you have to look at the -Zmir-dump to correlate

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

yes

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

will do later

nikomatsakis (May 18 2018 at 13:17, on Zulip):

but that is telling you that bb5[1], whatever that is, has bw1 in scope (or maybe it is the error?)

nikomatsakis (May 18 2018 at 13:17, on Zulip):

I'm still not sure what output you are showing me

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

today is a day a bit more complicated than usual

nikomatsakis (May 18 2018 at 13:17, on Zulip):

I gues I have to look at your brancvh

nikomatsakis (May 18 2018 at 13:17, on Zulip):

yeah sorry chatting also with @pnkfelix (as you can probably see :)

nikomatsakis (May 18 2018 at 13:17, on Zulip):

so I'm a bit lagged

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

no worries

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

this output did come from your branch, right?

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

the thing I'm showing is the content of invalidates.facts when ran using Reed's branch for the function ok of the get_default.rs

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

the thing I'm showing is the content of invalidates.facts when ran using Reed's branch for the function ok of the get_default.rs

ah ok

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

so that is saying:

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

sorry for not clarifying that

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

at that point

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

the loan bw1 is invalidated

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

yep

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

what I think would be a good goal now, on your branch,

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

is to combine that with region_live_at

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

er,

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

borrow_live_at

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

basically the intersection of those

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

is the set of errors

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

and we expect some errors in this example

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

yep, all that is already done

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

I need just to check if it's correct by hand

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

given we said that tests are a bit complex to build

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

@nikomatsakis https://github.com/rust-lang-nursery/polonius/pull/34

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

sorry for not giving more context, I assumed you were following the talk we had yesterday

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

which is impossible given the amount of talks you're having at the same time :P

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

how many open threads do you have? :P

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

ah right :) we did that already

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

how many open threads do you have? :P

don't ask

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

ok so yeah that looks right

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

hehehe

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

one thing

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

yeah, it wasn't that much empathetic to go just straight to a very particular part of the code :)

nikomatsakis (May 18 2018 at 13:23, on Zulip):

I think we should alter the output

nikomatsakis (May 18 2018 at 13:23, on Zulip):

that is, the Output struct

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

ok

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

tell me

nikomatsakis (May 18 2018 at 13:23, on Zulip):

so that this new result is the "main" result

nikomatsakis (May 18 2018 at 13:23, on Zulip):

and borrow_live_at etc is only populated when we have the 'verbose' output

nikomatsakis (May 18 2018 at 13:23, on Zulip):

er, hmm, not sure, it depends how we want to go

nikomatsakis (May 18 2018 at 13:23, on Zulip):

anyway we should at least make sure to dump potential_errors

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

I'm already doing that

nikomatsakis (May 18 2018 at 13:23, on Zulip):

ok

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

I couldn't quite tell from a quick glance

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

or I didn't follow you correctly :P

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

anyway however we do it, can you get the results of potential_errors for the get_default example?

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

so ...

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

https://github.com/rust-lang-nursery/polonius/pull/34/files#diff-9ff1367614ea2af6c399ce0c2500c4d4R38

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

that's Output modified

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

here https://github.com/rust-lang-nursery/polonius/pull/34/files#diff-2cacc48f0a2b0432151b6f258162f827R169, I've moved borrow_live_at to when it's verbose

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

and here https://github.com/rust-lang-nursery/polonius/pull/34/files#diff-2cacc48f0a2b0432151b6f258162f827R185 we are returning potential_errors

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

you're right, I need to do something else in output/mod.rs

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

it dumps borrow_live_at

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

I need to dump that for all the algorithms but for insensitive one

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

I wonder if it's really time to merge the insensitive one with timely-opt

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

I can't decide between trying to keep it as its own thing

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

and merging

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

that said

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

@Santiago Pastorino maybe you should make a new branch and just integrate the "errors" into the other algorithsm

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

modify Output then so that this is the "main output" for everything

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

or, maybe not a separate branch

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

but point is, you can do the same thing for all algorithms

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

yeah, makes sense

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

anyway, I wanted to run this real quick, looking how to enabled dump from command line

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

ok, found it

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

in this case potential_errors is empty for both ok and err fns

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

I'd need to check all this properly

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

in this case potential_errors is empty for both ok and err fns

hmm :)

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

yeah it seems like we need to Dump All The tuples then

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

to try and see what's up w/ that

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

yeah I did that, dumped all

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

but yeah, I need to take a look more carefully

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

ok, yeah, it's kind of annoying to process the raw data

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

you sort of have to cross-reference with the mir-dump

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

this is why I wanted to connect it to rustc :)

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

:)

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

in a bit maybe we can look it over together...

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

ok

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

ping me

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

I'm not sure I have time today

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

may have some spare minutes between meetings and stuff but ping me

nikomatsakis (May 18 2018 at 13:40, on Zulip):

k

lqd (May 22 2018 at 15:00, on Zulip):

just checking, we're still not 100% sure on how to best integrate the location-insensitive analysis results into the sensitive analysis right ?

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

well I'm not sure the best way. I can think of a few simple ways.

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

simplest possible way: does clap pass?

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

if so, we can just use it as a binary test :)

lqd (May 22 2018 at 15:01, on Zulip):

that's what I was thinking at first :)

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

next simplest way: take the set of loans where potential errors occur; use that to limit the requires

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

next next simplest way: take the set of regions "linked" to those borrows, limit subset to those regions

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

that was roughly what I had in mind

lqd (May 22 2018 at 15:01, on Zulip):

clap does pass the loc-insensitive quite fast

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

@lqd how fast? :)

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

you'll be pleased I think

lqd (May 22 2018 at 15:05, on Zulip):

I hope at least

lqd (May 22 2018 at 15:05, on Zulip):

datafrog_opt on this machine is around 5.5s on clap, loc-insensitive is 700-800ms

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

awesome!

lqd (May 22 2018 at 15:07, on Zulip):

I should have mentioned this yesterday sorry, I thought we wouldn't only want to check if any potential errors were found before rerunning the sensitive analysis

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

@lqd well, it seems fine, though we still have to account for "universal regions" in the analysis, which we haven't, but that should be easy enough

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

and I think clap would still pass

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

it's also why I/we were wondering with Frank whether clap was a representative worst case

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

probably not

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

I think we're definitely at the point where the right thing to focus on is rustc integration

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

which will add overhead of its own that must be sanded down

lqd (May 22 2018 at 15:09, on Zulip):

account for universal regions in the loc-insensitive analysis ?

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

just in general

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

we're not accounting for them

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

in particular:

lqd (May 22 2018 at 15:10, on Zulip):

(ofc datafrog_opt with leapjoin is <4.4s)

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

in an example like this:

fn foo(x: &'a u32) -> &'b u32 { x }

we would compute a subset('a, 'b) relation, which we can use to report an error. But we have to use this to inform the set of "potential errors". I've not really thought much about how to do this but shouldn't be very hard.

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

(right now all the errors we are reporting have to do with violated loans)

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

(but that's not the only kind of error we have the responsibility to detect)

lqd (May 22 2018 at 15:12, on Zulip):

oh ok, I guess the diagnostics work will have an impact on the analysis, to get the data it needs

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

(that said, it's a fundamentally similar analysis)

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

you .. might even be able to model universal regions as loans? (that never get killed) .. at one point I was doing that, I forget why I stopped. Anyway.

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

that said, datafrog_opt doesn't produce error points yet, so it's still not "realistic" -- want me to do that ?

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

@lqd yes

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

that goes with what @Santiago Pastorino and I were saying about how it would be useful to make "errors" the primary output for all analyses (and borrow_live_at just a "detail" you see with -v)

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

I'm going to do all this if you're fine

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

need to read all that you've said :)

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

need to do some minor things unrelated to Rust before also

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

@Santiago Pastorino "all this" being the switch to "errors" being the primary output you mean ? (I was almost done producing errors in datafrog_opt)

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

@lqd yes, and other things :)

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

but great if you already did :)

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

@nikomatsakis btw producing the errors will slow down clap as we now have to do a big join with borrow_live_at. I'm not too worried because 1) leapjoin should help with these a lot (and I will try it out just after posting the PR in a couple minutes) 2) it's not strictly necessary to maintain this relation, except for the verbose mode where we display it, otherwise we can fold it into errors 3) for the precise clap benchmark, the loc-insensitive pass will make it that this one never runs (or limit its work, as we talked about)

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

@Santiago Pastorino no worries we can work on it together :thumbs_up: I will not modify the dumped output and so on

Jake Goulding (May 22 2018 at 17:15, on Zulip):

can producing errors only be done if there is an error? would that speed anything up?

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

or do "the other things" :)

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

@Jake Goulding there's something planned in that vein if I understand correctly what you mean: a fast pass that tries to find "potential errors" to either bypass the more complete analysis or at least filter the data for which it will run

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

Isn't that the "location-insensitive pre-pass"? I was mostly wondering if the useful error details (the 3 point notes, etc) could be skipped until theres a known error, following the same ideas

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

I hope so :) it's a bit unclear at the moment how the diagnostics work currently being done will impact the analyses in polonius, the data they will require, but it should be hopefully possible to avoid doing extra work

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

@lqd good observations. Seems fine.

Last update: Nov 21 2019 at 14:40UTC