Stream: t-compiler/wg-polonius

Topic: initialization


Albin Stjerna (Jul 15 2019 at 09:05, on Zulip):

Hi @WG-polonius! By now Niko should be on vacation (DON'T READ NIKO, VACATE!), but I figured I should give working on initialisation a shot anyway. I have a rough idea of what I should do, and some questions, including one on error reporting that overlaps with @lqd's work on illegal subset relations.

Would anyone be willing to have a quick chat about this at some point? It makes more sense to me to see if anyone has answers to my questions before I start digging the answers out of Rust and/or make assumptions.

lqd (Jul 15 2019 at 09:51, on Zulip):

with Niko and Felix gone, maybe Matthew would be a good person to talk to

lqd (Jul 15 2019 at 09:52, on Zulip):

or ofc eddyb

Albin Stjerna (Jul 15 2019 at 10:18, on Zulip):

Hmh, yes probably

Albin Stjerna (Jul 15 2019 at 10:18, on Zulip):

Thanks

Albin Stjerna (Jul 15 2019 at 10:39, on Zulip):

Ping @Matthew Jasper to begin with, would you have the time to talk a bit about initialisation at some point?

Matthew Jasper (Jul 15 2019 at 11:27, on Zulip):

I should be free and at my computer in 7-8 hours. I could answer any really simple questions now.

nikomatsakis (Jul 15 2019 at 11:35, on Zulip):

/me does not read

Albin Stjerna (Jul 15 2019 at 12:16, on Zulip):

@Matthew Jasper thanks! Poke me when you're available, or preferably slightly before that so I can get to a computer :)

Robert Jacobson (Jul 15 2019 at 16:17, on Zulip):

@Albin Stjerna I haven't forgotten your generous offer to read what I write about Polonius, but I got sidetracked by writing a Pratt parser/Pratt parser generator in Rust, a creature that seems to be conspicuously absent from the Rust ecosystem. Just curious, have there been discussions about strengthening the Rust parser ecosystem? Or is it considered not particularly important considering the existence of other well-known external tools like Ragel that already target Rust? I haven't worked in this space long enough to know.

Albin Stjerna (Jul 15 2019 at 17:00, on Zulip):

@Robert Jacobson I don't know, honestly, I'm rather new here myself.

Matthew Jasper (Jul 15 2019 at 17:18, on Zulip):

@Albin Stjerna I should be able to discuss things in 20-30 minutes

Albin Stjerna (Jul 15 2019 at 17:37, on Zulip):

@Matthew Jasper Yay!

Matthew Jasper (Jul 15 2019 at 17:52, on Zulip):

Ok, I'm here

Matthew Jasper (Jul 15 2019 at 17:53, on Zulip):

So, there were some notes on this here: https://paper.dropbox.com/doc/Polonius-and-initialization--Ag9uxQB9rVuyu~JQ71KkYscwAg-mNvR4jqITCdsJDUMEhFbv

Matthew Jasper (Jul 15 2019 at 17:58, on Zulip):

...which I don't have write access to

Matthew Jasper (Jul 15 2019 at 18:02, on Zulip):

But the last section provides some details on what to do.

simulacrum (Jul 15 2019 at 18:02, on Zulip):

If you have an email for me (feel free to PM) I can invite you

Albin Stjerna (Jul 15 2019 at 18:03, on Zulip):

@Matthew Jasper Yes, I had a look at them earlier

Albin Stjerna (Jul 15 2019 at 18:05, on Zulip):

I think I understand the big picture: so I want to produce the following facts:
- "path x1 is a child of path x2"
- "path x was accessed at point p" facts
- "path x was initialised at point p" facts
- "path x was deinitialised at point p"

Albin Stjerna (Jul 15 2019 at 18:06, on Zulip):

I think it would be fairly straightforward to use that to calculate which paths are inintialised maybe/for sure where, and then from that to errors on invalid access

Albin Stjerna (Jul 15 2019 at 18:07, on Zulip):

However, I think I should start by calculating var_initialized_on_exit(V, P) because I already have those tuples collected

Albin Stjerna (Jul 15 2019 at 18:07, on Zulip):

It should be true if the variable V might be initialised at P

Matthew Jasper (Jul 15 2019 at 18:07, on Zulip):

So step 1 is to implement Atom for MovePathIndex (the one defined here: https://github.com/rust-lang/rust/blob/f3f9d6dfd92dfaeb14df891ad27b2531809dd734/src/librustc_mir/dataflow/move_paths/mod.rs#L16)

Albin Stjerna (Jul 15 2019 at 18:07, on Zulip):

Ok, that was another question I had, what I should use for the input

Albin Stjerna (Jul 15 2019 at 18:08, on Zulip):

But that was my best candidate :)

Matthew Jasper (Jul 15 2019 at 18:08, on Zulip):

However, I think I should start by calculating var_initialized_on_exit(V, P) because I already have those tuples collected

That sounds more sensible than trying to implement the remaining half of the borrow checker

Albin Stjerna (Jul 15 2019 at 18:08, on Zulip):

Arr, How Hard Could It Be™

Matthew Jasper (Jul 15 2019 at 18:08, on Zulip):

Very hard with the time you have.

Albin Stjerna (Jul 15 2019 at 18:09, on Zulip):

True

Matthew Jasper (Jul 15 2019 at 18:09, on Zulip):

Most of the facts can be extracted from this struct https://github.com/rust-lang/rust/blob/f3f9d6dfd92dfaeb14df891ad27b2531809dd734/src/librustc_mir/dataflow/move_paths/mod.rs#L99

Albin Stjerna (Jul 15 2019 at 18:09, on Zulip):

Isn't that sort of cheating?

Albin Stjerna (Jul 15 2019 at 18:09, on Zulip):

Because that struct already kind of has all the initialisation data, right?

Matthew Jasper (Jul 15 2019 at 18:10, on Zulip):

It only has where things are initialized and deinitialized, not the initialization flow data.

Albin Stjerna (Jul 15 2019 at 18:11, on Zulip):

Oh, ok, then it makes sense

Albin Stjerna (Jul 15 2019 at 18:11, on Zulip):

Ok, and that one obviously has the mapping from local <-> move paths

Albin Stjerna (Jul 15 2019 at 18:11, on Zulip):

So that was...all my questions I think

Matthew Jasper (Jul 15 2019 at 18:11, on Zulip):

rev_lookup contains the relations between move paths and locals, and the parent relation.

Matthew Jasper (Jul 15 2019 at 18:12, on Zulip):

and moves and initscontain the initializations and deinitializations

Albin Stjerna (Jul 15 2019 at 18:12, on Zulip):

Yes, I'm already using it to get var_initialized_on_exit (which should probably be renamed to var_may_be_initialized_on_exit)

Matthew Jasper (Jul 15 2019 at 18:13, on Zulip):

Which leaves the "used at" facts, which you fortunately don't need for var_may_be_initialized_on_exit

Albin Stjerna (Jul 15 2019 at 18:13, on Zulip):

no, and I already have them right?

Albin Stjerna (Jul 15 2019 at 18:13, on Zulip):

I needed them for liveness

Albin Stjerna (Jul 15 2019 at 18:14, on Zulip):

Unless I need a used at for a move path and not a variable hmm

Matthew Jasper (Jul 15 2019 at 18:14, on Zulip):

Yes

Matthew Jasper (Jul 15 2019 at 18:14, on Zulip):

So liveness considers x.a a use of x, but for move errors it's only a use of x.a

Albin Stjerna (Jul 15 2019 at 18:15, on Zulip):

ah of course

Albin Stjerna (Jul 15 2019 at 18:15, on Zulip):

so it's higher resolution

Matthew Jasper (Jul 15 2019 at 18:16, on Zulip):

Actually, they shouldn't be too bad to generate

Matthew Jasper (Jul 15 2019 at 18:17, on Zulip):

You can add a visit_place method to the implementation here: https://github.com/rust-lang/rust/blob/099f9e4e8aac3968888636e2126c4b7f8e6bb2d3/src/librustc_mir/borrow_check/nll/invalidation.rs#L57

Matthew Jasper (Jul 15 2019 at 18:19, on Zulip):

Then you generate a uses fact if the context is a non-mutating use, or it's a MutatingUse(Borrow).

Albin Stjerna (Jul 15 2019 at 18:20, on Zulip):

Hm, ok, and how do I go from there to the MovePathIndex of the use?

Matthew Jasper (Jul 15 2019 at 18:22, on Zulip):

move_data.rev_lookup.find(), and then extract the move path from the returned value.

Albin Stjerna (Jul 15 2019 at 18:22, on Zulip):

Ah, ok so I have that in the context

Matthew Jasper (Jul 15 2019 at 18:22, on Zulip):

You can add it.

Albin Stjerna (Jul 15 2019 at 18:23, on Zulip):

Ok, that makes sense

Matthew Jasper (Jul 15 2019 at 18:23, on Zulip):

That's not quite correct for Box de-references and inline asm. But it should be a close approximation.

Matthew Jasper (Jul 15 2019 at 18:23, on Zulip):

and it can be fixed.

Albin Stjerna (Jul 15 2019 at 18:24, on Zulip):

Ah, ok

Matthew Jasper (Jul 15 2019 at 18:24, on Zulip):

and assigning to any dereference....

Albin Stjerna (Jul 15 2019 at 18:24, on Zulip):

Haha

Albin Stjerna (Jul 15 2019 at 18:24, on Zulip):

What I have learned from this project is that it's a miracle that any compiler ever works for anything

Matthew Jasper (Jul 15 2019 at 18:25, on Zulip):

So true

Albin Stjerna (Jul 15 2019 at 18:25, on Zulip):

I currently have a sheet of paper containing a very messy mind-map of which module calls which function where to populate data for which other function, and that's just to have an idea for where Polonius intersects with NLL

Albin Stjerna (Jul 15 2019 at 18:26, on Zulip):

Ok, but I think that's more than enough to get me started. Do you also have a suggestion for where to intercept MoveData and start emitting facts?

Albin Stjerna (Jul 15 2019 at 18:28, on Zulip):

Do you think liveness::generate() would do, or should it be earlier?

Matthew Jasper (Jul 15 2019 at 18:32, on Zulip):

I'd probably do it right when we create the AllFacts

Matthew Jasper (Jul 15 2019 at 18:33, on Zulip):

In the totally accurately named nll/mod.rs:compute_regions

Albin Stjerna (Jul 15 2019 at 18:33, on Zulip):

I did wonder about that one

Albin Stjerna (Jul 15 2019 at 18:34, on Zulip):

But that sounds good

Albin Stjerna (Jul 15 2019 at 18:34, on Zulip):

Thank you so much!

Albin Stjerna (Jul 24 2019 at 13:45, on Zulip):

@Matthew Jasper I ran into a snag of sorts; I'm not sure I understand how MIR Locals translate to their corresponding MovePathIndexes. So what I did was I populated the var_starts_path fact from basically dumping the lookups in MovePathLookup so that I have tuples of (Local, MovePathIndex). In my small sample program, this generates one MovePathIndexper Local, basically, which is weird because many of them map to the same place. Basically, I don't know where to look for the information that somehow shows that a case like _1 = _2 means _1 now is the "same" as _2, for some definition of sameness.

Albin Stjerna (Jul 24 2019 at 13:47, on Zulip):

Or, I guess what is weird is that when I try to populate my parentrelation by iterating over all the MovePaths in MoveData and adding a tuple per entry I get from move_path.parents(), I only get one interesting parent relationship and nothing matching the move paths where things are actually moved out of my tuple

Albin Stjerna (Jul 24 2019 at 13:49, on Zulip):

Specifically, my code looks like this:

fn populate_polonius_move_facts(all_facts: &mut AllFacts, move_data: &MoveData<'_>, _location_table: &LocationTable) {
    all_facts.var_starts_path.extend(move_data.rev_lookup.iter_locals_enumerated().map(|(v, &m)| (v, m)));

    for (idx, move_path) in move_data.move_paths.iter_enumerated() {
        all_facts.parent.extend(move_path.parents(&move_data.move_paths).iter().map(|&parent| (parent, idx)));
    }
}

I would have expected the "interesting" MoveIndexes to also have parents, but they don't? Is this because my program isn't interesting enough (i.e. compiles)?

Albin Stjerna (Jul 24 2019 at 13:56, on Zulip):

Perhaps I should hold off judgement until I have Init events and see where that would get me

Albin Stjerna (Jul 24 2019 at 14:43, on Zulip):

Also, when looking at the Initstruct, the documentation says that "initializations can be from an argument or from a statement". What does it mean for an initialisation to happen in an argument?

Matthew Jasper (Jul 24 2019 at 18:28, on Zulip):

Also, when looking at the Initstruct, the documentation says that "initializations can be from an argument or from a statement". What does it mean for an initialisation to happen in an argument?

given fn f(x: i32) {} x is initialized "before the function starts". That's recorded as an initialization from an assignment

Matthew Jasper (Jul 24 2019 at 18:32, on Zulip):

For the other stuff it would be helpful to see the function that you're testing on and output facts

Albin Stjerna (Jul 24 2019 at 20:32, on Zulip):

I'll do some more thinking tomorrow and see if I can figure out what I would even expect it to do and let you know. There is a chance that it actually works and that I'm just confused. I think I should have most of the logic for calculating var_maybe_initialized_on_exit(which should probably be called var_maybe_partially_initialized_on_exit, but that's just too long)

Albin Stjerna (Jul 25 2019 at 10:28, on Zulip):

@Matthew Jasper Ok, so I put everything together and added some compare functionality similar to what I did for provenance variable liveness. I haven't verified that the parenthood relationship works yet, but I have identified a definite problem with terminators that I don't know how to handle, and would very much appreciate your input on.

Situation: there is a basic block, (N) with a terminator terminator(N) that performs one or more function calls with moves (of m) and one assignment (of a), like a = foo(move m), with terminators going to a block (RETURN) and (UNWIND).
What should happen: it's unclear to me whether m should be considered initialised in terminator(N). Does the move always happen before the call? However, it is clear to me that in RETURN, mshould be deinitialised (definitely), and ashould be initialised (definitely).
What actually happens: the rustc-generated var_maybe_initialized_on_exit has:
- var_maybe_initialized_on_exit(a, terminator(N)) = False.
- var_maybe_initialized_on_exit(a, start(RETURN)) = True.
- var_maybe_initialized_on_exit(a, start(UNWIND)) = False.
- var_maybe_initialized_on_exit(m, start(UNWIND)) = False.

However, as Polonius doesn't see the difference between a terminator and a regular point in the program-flow, in other words it treats both arms the same: both the move and the initialisation happens before the unwind arm.

Suggested fix: Would it be sufficient to just emit initialized_at(a, start(RETURN)) in this case, you think?

Matthew Jasper (Jul 25 2019 at 21:38, on Zulip):

Livened is able to ignore most of this due to how MIR is constructed. Moving the initialization to the start of the return block is the correct fix for now. I should probably go through the handling of calls in MIR again sometime, because it's a bit of a hack that doesn't easily port to polonius.

Albin Stjerna (Jul 26 2019 at 14:15, on Zulip):

Ok, I'll try that and see what else breaks/was already broken. :)

Albin Stjerna (Jul 26 2019 at 14:16, on Zulip):

Thanks!

Albin Stjerna (Aug 01 2019 at 12:41, on Zulip):

@Matthew Jasper Ok, I'm almost there now. I just have two problems left:
- my emitted facts and the ones in Polonius don't always agree on when a move caused by a function call happens. This is a bit confusing, as I just emit facts straight from MoveData. I'll have a look at that later, but:
- I currently don't know how to set function arguments as initialised. I know I can find them in MoveData::inits, but they don't have a Locationof any kind in the case of an InitLocation::Argument. So I guess my question is: how do I find the Locationof the start of the function taking a Localas argument?

Albin Stjerna (Aug 01 2019 at 12:42, on Zulip):

(or, I guess I could just find all functions and mark their arguments as initialised if that's easier)

Matthew Jasper (Aug 01 2019 at 13:04, on Zulip):

InitLocation:: Argument really should be Parameter, it should be fine to use the start point of the CFG for them.

Albin Stjerna (Aug 01 2019 at 13:05, on Zulip):

Hmh, and how would I find that?

Albin Stjerna (Aug 01 2019 at 13:06, on Zulip):

I mean, I do have access to the MIR Body, but how do I even tell which function I am in?

Albin Stjerna (Aug 01 2019 at 13:06, on Zulip):

Or is it one Bodyper function?

Albin Stjerna (Aug 01 2019 at 13:07, on Zulip):

Ah yes, ok

Albin Stjerna (Aug 01 2019 at 16:27, on Zulip):

@Matthew Jasper Ok, now the calculated var_maybe_initialized_on_exit:s actually produce the same region_live_at values for all inputs (yay!), and mostly the same input facts as Rust. I still have a problem with moves in function calls though. For example, I have a function like this:

fn main() {
    let x = 13;
    let y = Foo { data: &x };
    println!("y = {:?}", y);
    println!("x = {:?}", x);
}

It has this MIR, and these Polonius inputs/results. Notably, the only difference to the expected values is the status of the moved variables _25 and _46. The discrepancy happens for _25 after the terminator _23 = const std::fmt::ArgumentV1::<'_>::new::<Foo<'_>>(move _24, move _25). In the facts I generate, _25is immediately moved and so is moved on entry to bb2, and on the entire unwind path. In the inputs from rustc (which may be buggy), it is moved by a StorageDead immediately upon entry to 2, but also magically resurrects at the end of the unwind path (in the resume block); despite both versions agreeing that it's uninitialised in both predecessor blocks (3 and 8).

The same thing (except the magical resurrection) happens to _46.

What is the expected behaviour here? Can a move in a terminator somehow not happen? Why is the first argument moved and not the second one?

Matthew Jasper (Aug 01 2019 at 20:23, on Zulip):

I can't get the polonius inputs pdf to load correctly

Matthew Jasper (Aug 01 2019 at 20:25, on Zulip):

_25 and _46 definitely shouldn't be initialized after the function calls.

Albin Stjerna (Aug 02 2019 at 06:51, on Zulip):

Ok, then I’ll have a closer look at the other reported differences and see if they are identical and if so consider it a bug in the current fact generation

Albin Stjerna (Aug 02 2019 at 13:50, on Zulip):

@Matthew Jasper Ok, I have gone through the cases where my output is different from Rustc's, and in almost all cases it's the same problem (a move in a function call not happening until a later StorageDead). In the other two cases it must also be a bug, because they have variables suddenly being initialised without ever having even been even mentioned in the MIR. In other words, I think the computed var_maybe_initialised_on_exitis now correct, with some degree of confidence.

The question now becomes what to do with the old facts. I would like to remove the old var_initialised_on_exitlogic from rustc, and possibly also the entire input fact from Polonius, because it was always an ugly hack. However, that means I can no longer run the comparison tests (some of which fail spuriously anyway).

That also has a follow-on question, which is: should I also throw away the region_live_at input, which I now also have logic to calculate? Similar problems apply here: that would mean that we lose the infrastructure for verifying it, but on the other hand, we already have.

Finally, I could extend the Polonius grammar to also have support for formulating all the initialisation-related facts. This is probably a prerequisite for testing them at all, but it would also be a lot of work for little gain.

What do you think I should do?

Matthew Jasper (Aug 02 2019 at 13:59, on Zulip):

:+1: to removing the licenses and initialized on exit facts.

Albin Stjerna (Aug 02 2019 at 13:59, on Zulip):

"licenses"?

Matthew Jasper (Aug 02 2019 at 14:24, on Zulip):

Liveness

Albin Stjerna (Aug 02 2019 at 14:58, on Zulip):

ah, ok! And what do I do about the tests?

Matthew Jasper (Aug 02 2019 at 18:39, on Zulip):

Remove them

Albin Stjerna (Aug 02 2019 at 19:33, on Zulip):

This is going to be so satisfying :)

Albin Stjerna (Aug 05 2019 at 14:30, on Zulip):

I'm a bit confused about something that should be basic datafrog, but for some reason doesn't work as I expect it to. So I'm fixing a bug in the liveness calculations by filtering out initial values for var_drop_live_atto only contain variables that are actually initialised when they were dropped. I create a static variable for the var_drop_used
relation for use with leapjoins, and then I proceed like this:

// var_drop_live(V, P) :-
//     var_drop_used(V, P),
//     var_maybe_initialzed_on_exit(V, P).
var_drop_live_var.from_leapjoin(
      &var_drop_used_var,
      var_maybe_initialized_on_exit_rel.extend_with(|&(v, _p)| v),
      |&(v, _), &p| (v, p)
  );

Shouldn't this do a join on V, excluding any V:s not in both var_maybe_initialized_on_exit and var_drop_used? Or have I misunderstood how this works? Also, I don't understand why I get wildly different outputs depending on which tuple I select pfrom?

Albin Stjerna (Aug 05 2019 at 14:30, on Zulip):

(Ping @lqd who maybe knows and perhaps doesn't hang around here)

Albin Stjerna (Aug 05 2019 at 14:56, on Zulip):

As far as I can tell, it behaves like an outer join!?

Albin Stjerna (Aug 05 2019 at 19:49, on Zulip):

Update: it's not that, because the same thing happens if I make the "join" myself, but the facts _are_ correct and there should never be any join. I don't understand!? HOW can var_drop_live_at be true for _2 here? It's very clearly not in var_maybe_initialized_on_exit:
pasted image

Albin Stjerna (Aug 05 2019 at 19:50, on Zulip):

(The name "_on_exit" is also wrong, it should be on_entryI guess?)

lqd (Aug 05 2019 at 20:14, on Zulip):

(sorry I'm on holidays and missed the ping)

lqd (Aug 05 2019 at 20:15, on Zulip):

IIUC you're effectively encoding an outer join

lqd (Aug 05 2019 at 20:15, on Zulip):

but the datalog does not only join on V here

lqd (Aug 05 2019 at 20:16, on Zulip):

P is also present in both relations

lqd (Aug 05 2019 at 20:17, on Zulip):

what you're looking for, IIUC, is to filter the (V, P)s present in both relations only

lqd (Aug 05 2019 at 20:18, on Zulip):

however, this won't be possible/easy (it's a gamble depending on the data) with a leapjoin for now

lqd (Aug 05 2019 at 20:19, on Zulip):

they have a weird under-specified/undocumented criterion wrt well-formedness, that is they expect to have a least one extend_with (I think) and even though that's what you have here the leaper for the join should probably be filter_with — but if you do that the leapjoin won't be well-formed anymore (until at least until we relax this requirement in :frog:)

Albin Stjerna (Aug 05 2019 at 20:19, on Zulip):

Haha, I just spent 20 minutes trying to figure out how this happened and was _so proud_ of myself for figuring it out, only to realise you just replied :)

Albin Stjerna (Aug 05 2019 at 20:20, on Zulip):

That was after literal hours of debugging earlier today

lqd (Aug 05 2019 at 20:20, on Zulip):

so, what you're looking for here is a regular join between variables/relations setup to filter, that is, where the whole tuple is a "key" like ((V,P), ()) — there are examples of that in the naive/datafrogopt variants IIRC

lqd (Aug 05 2019 at 20:21, on Zulip):

sorry :)

Albin Stjerna (Aug 05 2019 at 20:21, on Zulip):

Oh that's by no means your fault :)

lqd (Aug 05 2019 at 20:21, on Zulip):

still good that you were able to figure it out on your own :)

Albin Stjerna (Aug 05 2019 at 20:21, on Zulip):

But great, now I think I know how to proceed yay

lqd (Aug 05 2019 at 20:22, on Zulip):

yeah once you know how to encode this pattern you'll be good I think

lqd (Aug 05 2019 at 20:23, on Zulip):

the borrow_live_at here is a good example

lqd (Aug 05 2019 at 20:24, on Zulip):

the join is here

Albin Stjerna (Aug 05 2019 at 20:24, on Zulip):

It looks like literally the same pattern, but with a 3-tuple

Albin Stjerna (Aug 05 2019 at 20:24, on Zulip):

And I also looked at it earlier today when trying to figure out if I did something wrong

Albin Stjerna (Aug 05 2019 at 20:24, on Zulip):

Oh well, I'll go to sleep first I guess

Albin Stjerna (Aug 05 2019 at 20:24, on Zulip):

Thank you! :)

lqd (Aug 05 2019 at 20:25, on Zulip):

the datalog-to-datafrog encoding is a bit hard to read immediately after writing it :)

lqd (Aug 05 2019 at 20:25, on Zulip):

it's .. a bit unreadable for sure

lqd (Aug 05 2019 at 20:26, on Zulip):

you're very welcome, at least I knew how to help here :)

lqd (Aug 05 2019 at 20:35, on Zulip):

(I updated an earlier message to add another case which is even more similar, encoding errors(B, P) :- invalidates(B, P), borrow_live_at(B, P).)

Albin Stjerna (Aug 06 2019 at 07:42, on Zulip):

Ok so now I think I have a different bug in my actual logic haha

Albin Stjerna (Aug 06 2019 at 07:43, on Zulip):

Because I currently ignore all drops of uninitialised variables, and that's not correct is it? At least, that gives different region liveness from the one supplied by rustc

Albin Stjerna (Aug 06 2019 at 07:50, on Zulip):

Ah, I see the bug now. At a drop(), I only consider a variable actually drop-used if it is initialised, but there's an off-by-one error in this logic: it's a tautology that drop(x) means xis not initialised on exit from that statement. I need to join on the previous statement.

Albin Stjerna (Aug 06 2019 at 07:52, on Zulip):

(which will always be just one statement because the drop always occurs mid-point)

Albin Stjerna (Aug 06 2019 at 08:12, on Zulip):

Wohooo that did it!

Albin Stjerna (Aug 06 2019 at 08:12, on Zulip):

And using only joins on relations no less

Albin Stjerna (Aug 06 2019 at 08:33, on Zulip):

In the process of debugging this, I also made a Python script that takes the input from cargo test and produces readable output in Markdown, should I put that somewhere in case it's useful to anyone else?

Albin Stjerna (Aug 06 2019 at 08:35, on Zulip):

It looks something like this:

$ cargo test implicit_fragment | ./parse-diff-output.py
    Finished dev [unoptimized + debuginfo] target(s) in 0.07s
     Running target/debug/deps/polonius-55bdf7bb7cdabdf9
error: test failed, to rerun pass '--lib'
## `maybe_initialized_drop_implicit_fragment_drop_main::computed_region_live_at_same_as_input`
- `Start(bb3[0])`:  **missing**: _#13r
- `Mid(bb3[0])`:    **missing**: _#13r
- `Start(bb7[5])`:  **missing**: _#16r
- `Mid(bb7[5])`:    **missing**: _#16r
- `Start(bb8[0])`:  **missing**: _#16r
- `Mid(bb8[0])`:    **missing**: _#16r
- `Start(bb9[0])`:  **missing**: _#16r
- `Mid(bb9[0])`:    **missing**: _#16r
- `Start(bb10[0])`: **missing**: _#16r
- `Mid(bb10[0])`:   **missing**: _#16r
- `Start(bb11[0])`: **missing**: _#16r
- `Mid(bb11[0])`:   **missing**: _#16r
- `Start(bb11[1])`: **missing**: _#16r
- `Mid(bb11[1])`:   **missing**: _#16r
- `Start(bb11[2])`: **missing**: _#16r
- `Mid(bb11[2])`:   **missing**: _#16r
- `Start(bb11[3])`: **missing**: _#16r
- `Mid(bb11[3])`:   **missing**: _#16r
- `Start(bb11[4])`: **missing**: _#16r
- `Mid(bb11[4])`:   **missing**: _#16r
Albin Stjerna (Aug 06 2019 at 08:35, on Zulip):

Hmh, maybe it's not useful anymore now that the big region_live_atcomparisons are soon gone

Albin Stjerna (Aug 07 2019 at 15:57, on Zulip):

@Matthew Jasper cc @lqd

Ok, I have finished generating var_maybe_initialized_on_exit and have removed region_live_at. Last time I checked, it passed all tests, but I'm currently having some troubles in the methods comparing the location-insensitive analysis to the full one. I don't understand them yet, but will debug later.

My implementation doesn't do the full move analysis, but I have fact generation for path access, and I have written comments mocking the Datalog I think is needed. I think it's come to the point where there's a point in having someone take a look at it, if you have the time. There's no rush, because I'm leaving for some vacation until August 15th.

I'm thinking that I should not try to finish the full move analysis as part of my thesis work as Matthew suggested. I will also leave the job of updating polonius-parser to work with these gazillion new facts, but I will absolutely try to do that at some point, just not under deadline.

PRs are at polonius#110 and rust#62800, but they don't have the updated facts yet.

lqd (Aug 07 2019 at 19:48, on Zulip):

nicely done :)

lqd (Aug 07 2019 at 19:49, on Zulip):

don't worry about the parser I can take care of that

lqd (Aug 07 2019 at 19:50, on Zulip):

I think Matthew or Niko would be better than me looking at the rustc side but I can look at the polonius for sure

lqd (Aug 07 2019 at 19:51, on Zulip):

(I'll myself be back from vacation around the same time as you)

Albin Stjerna (Aug 16 2019 at 15:46, on Zulip):

Ok, I have done some further hunting of the bug I mentioned. The problem is this: Polonius + rustc with my latest changes reports no errors for smoke-test's return_ref_to_local(). Or rather, my new logic, including the new region_live_at, works fine. However, sometime after I remove region_live_at, the new fact generation (or Polonius) somehow changes behaviour and it stops working. This is very weird because the problem seems to stem from incorrect subset relation propagation, but there are no changes to either that part of the code, nor to any related fact generation code, and as far as I can tell, the inputs are identical.

Last good commit on my branch is https://github.com/albins/polonius/commit/6b0fc8e6cf0cc5019af26a32898ae8c0064592dd, and the last good one on my Rustc branch is https://github.com/albins/rust/commit/c265a4108307ede999049c71650f95bd2d539d5e.

Albin Stjerna (Aug 16 2019 at 15:47, on Zulip):

I'll continue looking at this tomorrow, but I just can't wrap my head around it!

Albin Stjerna (Aug 16 2019 at 19:07, on Zulip):

Ok, this is nuts. I have the following in the correct output (HEAD of my master branch):
pasted image

and then I have this at HEAD of my working branch:
pasted image

Those are...the same facts?! Also, this is my diff of naive.rs:

diff --git a/polonius-engine/src/output/naive.rs b/polonius-engine/src/output/naive.rs
index 1cf252ed16..028fdfd4d3 100644
--- a/polonius-engine/src/output/naive.rs
+++ b/polonius-engine/src/output/naive.rs
@@ -13,26 +13,37 @@
 use std::collections::{BTreeMap, BTreeSet};
 use std::time::Instant;

+use crate::output::initialization;
 use crate::output::liveness;
 use crate::output::Output;
 use facts::{AllFacts, Atom};

 use datafrog::{Iteration, Relation, RelationLeaper};

-pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom, Variable: Atom>(
+pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom, Variable: Atom, MovePath: Atom>(
     dump_enabled: bool,
-    all_facts: AllFacts<Region, Loan, Point, Variable>,
-) -> Output<Region, Loan, Point, Variable> {
+    all_facts: AllFacts<Region, Loan, Point, Variable, MovePath>,
+) -> Output<Region, Loan, Point, Variable, MovePath> {
     let mut result = Output::new(dump_enabled);

+    let var_maybe_initialized_on_exit = initialization::init_var_maybe_initialized_on_exit(
+        all_facts.child,
+        all_facts.path_belongs_to_var,
+        all_facts.initialized_at,
+        all_facts.moved_out_at,
+        all_facts.path_accessed_at,
+        &all_facts.cfg_edge,
+        &mut result,
+    );
+
     let region_live_at = liveness::init_region_live_at(
         all_facts.var_used,
         all_facts.var_drop_used,
         all_facts.var_defined,
         all_facts.var_uses_region,
         all_facts.var_drops_region,
+        var_maybe_initialized_on_exit,
         &all_facts.cfg_edge,
-        all_facts.region_live_at,
         all_facts.universal_region,
         &mut result,
     );
Albin Stjerna (Aug 19 2019 at 10:39, on Zulip):

Update: it's a fact generation bug. The dereferencing of _2never causes a use-fact to be emitted. I think this may be due to the lazy reference generation? I.e. _2 is dereferenced, but only to create a copy, it seems?

What I think should happen if I understand the reasoning correctly is that Polonius should infer through outlives relations that _0 outlives the value it is referring to and return an error, presumably when the value is moved by the StorageDead() just before the terminator, but the propagation of the outlives relation relies on the liveness of _2's provenance variable, r6.

Here is the MIR:

StorageLive(_1)
_1 = const 0i32
FakeRead(ForLet, _1)
StorageLive(_2)
_2 = &_1
_0 = &(*_2)
StorageDead(_1)
StorageDead(_2)

Also, should a used variable be considered used at the start of the expression where it is used, or mid-point?

Albin Stjerna (Aug 19 2019 at 10:42, on Zulip):

As a reminder, I use the following MIR Visitor to extract variable uses:

impl Visitor<'tcx> for UseFactsExtractor<'_> {
    fn visit_local(&mut self, &local: &Local, context: PlaceContext, location: Location) {
        match categorize(context) {
            Some(DefUse::Def) => self.insert_def(local, location),
            Some(DefUse::Use) => self.insert_use(local, location),
            Some(DefUse::Drop) => self.insert_drop_use(local, location),
            _ => (),
        }
    }
}

Clearly there is some type of use I am missing here?

Albin Stjerna (Aug 19 2019 at 10:43, on Zulip):

(I now also use the same Visitor to visit places and emit move-path-uses for future move analysis)

Matthew Jasper (Aug 19 2019 at 11:47, on Zulip):

You're missing a super_place call in your visit_place override.

Albin Stjerna (Aug 19 2019 at 12:14, on Zulip):

What does that do?

Albin Stjerna (Aug 19 2019 at 12:28, on Zulip):

well it...makes the rest work. :)

Albin Stjerna (Aug 19 2019 at 12:28, on Zulip):

Thank you!

Albin Stjerna (Aug 19 2019 at 13:49, on Zulip):

HA, ok @nikomatsakis polonius#110 and rust#62800 are ready for review!

Albin Stjerna (Aug 19 2019 at 13:49, on Zulip):

...presuming it passes the tests

Albin Stjerna (Aug 19 2019 at 13:50, on Zulip):

But it Does On My Machine™

nikomatsakis (Aug 27 2019 at 19:11, on Zulip):

HA, ok nikomatsakis polonius#110 and rust#62800 are ready for review!

just saw this

nikomatsakis (Aug 27 2019 at 19:11, on Zulip):

Great!

Albin Stjerna (Aug 30 2019 at 09:47, on Zulip):

@nikomatsakis Ok, I have been thinking about your comments on var_maybe_initialized_on_exit a lot. I think the case is as follows:

var_drop_live(V, P) :-
     var_drop_used(V, P),
     var_maybe_initialized_on_exit(V, P).
Albin Stjerna (Aug 30 2019 at 09:54, on Zulip):

I also have an idea for how to do move errors:

nikomatsakis (Aug 30 2019 at 11:06, on Zulip):

@Albin Stjerna

That is, whenever a variable had some path initialized, the variable was considered initialized.

Yes, has_any_child_of is saying "if any path that begins with move_path is considered initialized...". That seems to map to the rule for var_maybe_initialized_on_exit for sure.

nikomatsakis (Aug 30 2019 at 11:07, on Zulip):

I'm not sure I fully understand your later comments, let me take a stab

nikomatsakis (Aug 30 2019 at 11:07, on Zulip):

So, just talking about MIR, if you have DROP(x), that is considered a no-op if x has been moved. We don't always know that statically. In a later phase ("elaborate drops"), we will extend the MIR to either eliminate no-op DROP terminators, or to add boolean variables that conditionally execute them if needed.

nikomatsakis (Aug 30 2019 at 11:08, on Zulip):

In some cases they will be transformed into DROP(x.y.z), if only some sub-path is initialized.

nikomatsakis (Aug 30 2019 at 11:09, on Zulip):

(But, in those cases, x and x.y cannot have destructors, due to other NLL rules)

nikomatsakis (Aug 30 2019 at 11:09, on Zulip):

(This all makes sense so far?)

nikomatsakis (Aug 30 2019 at 11:10, on Zulip):

Given how I understand this, though, I don't see why we would care about the initialisation of anything below root-levels of references.

nikomatsakis (Aug 30 2019 at 11:12, on Zulip):

It's true that the current incarnation of NLL is somewhat restrictive about initialized sub-paths. For example you can't compile code like this, iirc:

let x: (_, _);
x.0 = vec![22];
v.1 = vec![44];

but I think we intend to support such things eventually (c.f. https://github.com/rust-lang/rust/issues/54987)

nikomatsakis (Aug 30 2019 at 11:13, on Zulip):

In such a case, you would never have a direct initialization of x

nikomatsakis (Aug 30 2019 at 11:14, on Zulip):

I was imagining then a scenario like this:

let x: (_, _);
x.0 = ...;
std::mem::drop(x.0);
nikomatsakis (Aug 30 2019 at 11:14, on Zulip):

If we only tracked initialization at the level of local variables, we would see that x is initialized after x.0 = ... but we couldn't say for sure that x is not initialized after std::mem::drop, because we only saw a single field moved and not the entire thing.

nikomatsakis (Aug 30 2019 at 11:15, on Zulip):

Anyway, to be clear, I believe that the rules as you wrote them were equivalent to the changes I was suggesting -- but I felt like the setup you had would be a bit less efficient and/or clear.

nikomatsakis (Aug 30 2019 at 11:16, on Zulip):

it seems mildly simpler to say that errors are accessed intersected with maybe_moved?

nikomatsakis (Aug 30 2019 at 11:16, on Zulip):

Ah, I guess you also want an error if it is uninitialized, is your point

nikomatsakis (Aug 30 2019 at 11:16, on Zulip):

Except that uninitialized things are considered moved to start

nikomatsakis (Aug 30 2019 at 11:26, on Zulip):

I see I already wrote a summary of how Lark handled things -- it was doing a different sort of analysis than the one you are doing. In particular, it was just doing the "move errors" part. That is, detecting access to uninitialized or moved paths.

nikomatsakis (Aug 30 2019 at 11:26, on Zulip):

But some parts are relevant.

nikomatsakis (Aug 30 2019 at 11:35, on Zulip):

Re-reading that code, I feel like it too is does more transitive closures than are really necessary

Albin Stjerna (Aug 30 2019 at 11:57, on Zulip):

Anyway, to be clear, I believe that the rules as you wrote them were equivalent to the changes I was suggesting -- but I felt like the setup you had would be a bit less efficient and/or clear.

I guess the key question here is: would that lead to correct calculations of region_live_at?

Albin Stjerna (Aug 30 2019 at 11:58, on Zulip):

Except that uninitialized things are considered moved to start

Avoiding a notion of "to start" is specifically why I went about the acrobatics I described; I don't have any concept of "to start" in Datafrog, right?

Albin Stjerna (Aug 30 2019 at 11:58, on Zulip):

There is no first_node_of_cfg, and I'd rather not just guess it's index 0

nikomatsakis (Sep 03 2019 at 19:58, on Zulip):

so I landed https://github.com/rust-lang/polonius/pull/110

nikomatsakis (Sep 03 2019 at 19:58, on Zulip):

now we need a new polonius release, right?

nikomatsakis (Sep 03 2019 at 19:58, on Zulip):

(am I the only one with such privileges?)

Albin Stjerna (Sep 03 2019 at 19:58, on Zulip):

Yes please

Albin Stjerna (Sep 03 2019 at 19:58, on Zulip):

and yes, I think so

Albin Stjerna (Sep 03 2019 at 19:59, on Zulip):

/me has no idea

nikomatsakis (Sep 03 2019 at 20:01, on Zulip):

hmm no it should be more folks

nikomatsakis (Sep 03 2019 at 20:01, on Zulip):

I think @lqd can do it, for example

lqd (Sep 03 2019 at 20:01, on Zulip):

can I ?!

lqd (Sep 03 2019 at 20:02, on Zulip):

I didn't know that

nikomatsakis (Sep 03 2019 at 20:02, on Zulip):

maybe :)

nikomatsakis (Sep 03 2019 at 20:03, on Zulip):

the wg-compiler-nll github team has access, which I might actually want to revoke, along with the compiler team

nikomatsakis (Sep 03 2019 at 20:03, on Zulip):

but I think I should add the compiler-contributors team

nikomatsakis (Sep 03 2019 at 20:03, on Zulip):

which includes you

nikomatsakis (Sep 03 2019 at 20:03, on Zulip):

you're probably also a member of wg-compiler-nll ...

lqd (Sep 03 2019 at 20:04, on Zulip):

yes

nikomatsakis (Sep 03 2019 at 20:04, on Zulip):

anyway I'll publish v0.10.0

nikomatsakis (Sep 03 2019 at 20:07, on Zulip):

done -- @Albin Stjerna do you want to modify rust#62800 to use it?

lqd (Sep 03 2019 at 20:09, on Zulip):

(thanks for the release, I'll learn how to do it in the future so we don't have to bother you :)

nikomatsakis (Sep 03 2019 at 20:16, on Zulip):

no worries, I just don't like things to be bottlenecked on me

Albin Stjerna (Sep 03 2019 at 21:06, on Zulip):

I'll do it tomorrow!

Albin Stjerna (Sep 03 2019 at 21:06, on Zulip):

Signed, going to bed

Albin Stjerna (Sep 04 2019 at 07:53, on Zulip):

@nikomatsakis rust#62800 should be ready to merge once CI passes!

lqd (Sep 04 2019 at 08:33, on Zulip):

@Albin Stjerna ah I see some tidy checks failed, CI didn't get to run yet

Albin Stjerna (Sep 04 2019 at 08:35, on Zulip):

sigh of course

Albin Stjerna (Sep 04 2019 at 08:35, on Zulip):

Guess it must be due to the rebase or something, I’ll have a look

Albin Stjerna (Sep 04 2019 at 08:52, on Zulip):

Ah, it was the file where the try blocks cause rustfmt to error out, that explains things

Albin Stjerna (Sep 04 2019 at 08:53, on Zulip):

Anyway, it passes now

Albin Stjerna (Sep 17 2019 at 08:00, on Zulip):

@lqd By the way, I plan on eventually following Niko's suggestions and perform a precise analysis on move paths. You mentioned that I could use the rustc unit tests. Do you...err...know how to run those with Polonius? Also, that should probably go in the book at some point, I guess

lqd (Sep 17 2019 at 08:23, on Zulip):

yeah it's the --compare-mode polonius flag to add to your x.py test invocation

lqd (Sep 17 2019 at 08:25, on Zulip):

note that right now there are 2 OOMS, and 4-5 benign failures tho

lqd (Sep 17 2019 at 08:26, on Zulip):

since they're in the run pass maybe --pass check could be helpful in avoiding the OOMs, but I didn't try that (as I had them deleted locally to try to compare durations)

Albin Stjerna (Sep 17 2019 at 12:58, on Zulip):

@lqd Thanks, I guess I can just ignore those. Do you know how comprehensive those tests are, otherwise? I.e. how likely are they to catch a subtle mistake?

lqd (Sep 17 2019 at 13:00, on Zulip):

I guess subtlety can be easily missed and it can depend on the specific domain you're testing

lqd (Sep 17 2019 at 13:00, on Zulip):

different areas are more or less well covered

lqd (Sep 17 2019 at 13:01, on Zulip):

say, it'll be better to pass those 10K tests than none at all :)

lqd (Sep 17 2019 at 13:02, on Zulip):

and if the area isn't covered well enough, we can always, and should, add more tests

lqd (Sep 17 2019 at 13:03, on Zulip):

in general there are some tests in many areas

Albin Stjerna (Oct 14 2019 at 15:18, on Zulip):

@lqd You mentioned a problem with leapjoins that only filtered, does this happen when you have an expression like:

path_definitely_initialized_at(Path, Point) :-
        path_maybe_initialized_on_exit(Path, Point),
        !path_maybe_moved_at(Path, Point).

Where all components are actually Relations?

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

if you're talking about Relation::from_leapjoin or similar I don't know; I only used them with variables

lqd (Oct 14 2019 at 15:20, on Zulip):

I assume it could apply

Albin Stjerna (Oct 14 2019 at 15:20, on Zulip):

Ah, ok. But is it a compilation error or a runtime error?

lqd (Oct 14 2019 at 15:20, on Zulip):

the WF-ness rule is : "there needs to be an extend_with" (IIRC, surely Frank would know better, but I think it's this)

Albin Stjerna (Oct 14 2019 at 15:20, on Zulip):

Ah, ok

lqd (Oct 14 2019 at 15:20, on Zulip):

runtime error, sometimes

lqd (Oct 14 2019 at 15:20, on Zulip):

it depends on the data IIRC

Albin Stjerna (Oct 14 2019 at 15:20, on Zulip):

Is there an easy work-around?

lqd (Oct 14 2019 at 15:21, on Zulip):

for variables yes, use a regular join hehe

lqd (Oct 14 2019 at 15:21, on Zulip):

for relations I don't know sorry, niko added that API but I've never had the opportunity to use it yet

Albin Stjerna (Oct 14 2019 at 15:21, on Zulip):

I'll try it and see what happens

Albin Stjerna (Oct 14 2019 at 15:22, on Zulip):

My original problem was that I wanted to antijoin on a variable, which you cannot do (I guess because it might lead to future tuples needing to be retracted)

Albin Stjerna (Oct 14 2019 at 15:22, on Zulip):

So I had to stage my computation

Albin Stjerna (Oct 14 2019 at 15:22, on Zulip):

Which means that in the end, all I really have are Relations

lqd (Oct 14 2019 at 15:23, on Zulip):

not even one variable ?

Albin Stjerna (Oct 14 2019 at 15:23, on Zulip):

Nope

lqd (Oct 14 2019 at 15:23, on Zulip):

maybe you can then artificially make one variable

Albin Stjerna (Oct 14 2019 at 15:23, on Zulip):

I guess I can

Albin Stjerna (Oct 14 2019 at 15:24, on Zulip):

It works as a quick work-around :)

lqd (Oct 14 2019 at 15:24, on Zulip):

what relation are you producing ?

Albin Stjerna (Oct 14 2019 at 15:25, on Zulip):

So it's a four-stage process: first I compute transitive closure of path accesses, then I use those to compute paths that may be moved or not moved, then I calculate the definitely-moved ones and I use those to generate move errors

Albin Stjerna (Oct 14 2019 at 15:25, on Zulip):

Basically, move errors = path access - known initialised paths

lqd (Oct 14 2019 at 15:25, on Zulip):

seems like move errors are an intensional predicate

Albin Stjerna (Oct 14 2019 at 15:26, on Zulip):

known initialised paths = maybe initialised paths - maybe moved paths

Albin Stjerna (Oct 14 2019 at 15:26, on Zulip):

err maybe?

Albin Stjerna (Oct 14 2019 at 15:26, on Zulip):

(what does that mean?)

lqd (Oct 14 2019 at 15:27, on Zulip):

it's producing tuples, not input data; those are usually variables, except for your stratification problem as you mentioned, there you had no choice

Albin Stjerna (Oct 14 2019 at 15:27, on Zulip):

Ah, ok, yes

lqd (Oct 14 2019 at 15:29, on Zulip):

but yeah if stratification is turning every join into a separate iteration, that's unfortunate

lqd (Oct 14 2019 at 15:29, on Zulip):

but yeah a couple variables at the last step should unblock you

Albin Stjerna (Oct 14 2019 at 15:31, on Zulip):

Yes, thanks!

Albin Stjerna (Oct 14 2019 at 16:07, on Zulip):

Ok, revamped initialisation logic compiling now :)

Albin Stjerna (Oct 14 2019 at 16:07, on Zulip):

Let's see if it messed up any ui-tests first, and then worry about how to verify move errors

Albin Stjerna (Oct 14 2019 at 19:11, on Zulip):

This looks...slightly promising? I can't see how these failures would be due to initialisation:

failures:
    [ui] ui/abi/cross-crate/anon-extern-mod-cross-crate-2.rs
    [ui] ui/abi/duplicated-external-mods.rs
    [ui] ui/abi/extern/extern-crosscrate.rs
    [ui] ui/abi/foreign/foreign-dupe.rs
    [ui] ui/abi/invoke-external-foreign.rs
Albin Stjerna (Oct 14 2019 at 19:12, on Zulip):

All the errors are from ld

Albin Stjerna (Oct 15 2019 at 11:17, on Zulip):

Hmm, difficult to say if I changed anything: literally stopping all generation of child in Rust gives me no additional errors, so either I'm doing something wrong or it doesn't cover move paths x drop-liveness very much

lqd (Oct 15 2019 at 11:35, on Zulip):

what kind of errors are you expecting and where ?

Albin Stjerna (Oct 15 2019 at 12:42, on Zulip):

That is a good question. So what I did was I stopped emitting child at all, which would mean that nothing would be drop-live, so I would expect Polonius to under-report some errors with structs implementing their own drop if they hold a loan that is violated.

Albin Stjerna (Oct 15 2019 at 12:43, on Zulip):

I know I lifted some examples from the compiletests into Polonius inputs, and those should at least cause problems

Albin Stjerna (Oct 15 2019 at 12:44, on Zulip):

...ok no I get it it shouldn't cause a problem

Albin Stjerna (Oct 15 2019 at 12:44, on Zulip):

...because initialisation is always precise enough I think, or at least it is in this case

Albin Stjerna (Oct 15 2019 at 12:56, on Zulip):

Anyway, the shared context stuff would have been nice now, because then I could use it to report errors from the initialisation step :)

Albin Stjerna (Nov 19 2019 at 10:19, on Zulip):

Err, is it possible to use a borrowed Relation in leapjoins?

Albin Stjerna (Nov 19 2019 at 10:19, on Zulip):

Signed, still Datafrog-challenged

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

Ok, so the move error code is...not correct

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

Precisely how, I don't know yet

Albin Stjerna (Nov 19 2019 at 12:28, on Zulip):

It is also INCREDIBLY slow on clap

Albin Stjerna (Nov 19 2019 at 12:33, on Zulip):

Ah, it's at least one fact generation bug, I generate path_accessed_at() events at midpoint, should be start-point

Albin Stjerna (Nov 19 2019 at 13:54, on Zulip):

Update: I think it's...working after fixing that. I mean, I'm sure there might be edge cases, but it's working for the simple cases I have tried so far.

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

Hey all, be here soon

Albin Stjerna (Nov 19 2019 at 14:00, on Zulip):

Me too, I'm getting some tea

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

OK

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

So @Albin Stjerna where we at here :)

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

PS I prob have to go in ~3hr, at least for a bit

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

@Albin Stjerna one thing I wanted to do is to update the "canonical polonius rules" to include the rules for initialization and liveness

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

PS I prob have to go in ~3hr, at least for a bit

Fine by me, I'd like to go home around then

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

That means we have to argue about the names of everything :)

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

lol

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

well let's start with whatever names :)

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

first off, I guess, I should start by looking at your PR?

Albin Stjerna (Nov 19 2019 at 14:17, on Zulip):

I guess!

Albin Stjerna (Nov 19 2019 at 14:17, on Zulip):

I have restructured the code a bit so that the passes are clearer

Albin Stjerna (Nov 19 2019 at 14:17, on Zulip):

I also think the passes are probably a bad idea and we should think about a better way to do them

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

But it's not a gigantonormous function anymore

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

I'll update the hackmd while you are looking :)

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

@Albin Stjerna maybe we can do that a bit together?

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

I'm reading now

Albin Stjerna (Nov 19 2019 at 14:24, on Zulip):

Sure!

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

to start, what are the fresh inputs

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

I guess some of that is already present in the cod

Albin Stjerna (Nov 19 2019 at 14:25, on Zulip):

Well, there are no new inputs since my last PR

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

right so we should look at the facts.rs

Albin Stjerna (Nov 19 2019 at 14:26, on Zulip):

I can do better pasted image

Albin Stjerna (Nov 19 2019 at 14:27, on Zulip):

pasted image

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

dramatis personae

:thumbs_up: :)

Albin Stjerna (Nov 19 2019 at 14:28, on Zulip):

If you liked that, you should see my Hamlet quotes at the start of every chapter

Albin Stjerna (Nov 19 2019 at 14:28, on Zulip):

I mean, I spent a lot of time rewriting that thing, I might as well get to be a bit silly

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

I'll be looking forward to your updated manuscript :)

Albin Stjerna (Nov 19 2019 at 14:29, on Zulip):

here's a spoiler: pasted image

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

nice

Albin Stjerna (Nov 19 2019 at 14:29, on Zulip):

I also have examples for every slightly complex rule

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

nice :)

Albin Stjerna (Nov 19 2019 at 14:29, on Zulip):

I wrote those specifically with the idea of porting them to The Book

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

beautiful

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

ok, so, I am copying some of that over

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

I added a section 'liveness-related inputs'

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

(I let everyone know you were re-working your draft btw https://rust-lang.github.io/compiler-team/minutes/triage-meeting/2019-11-14/ :) (Working group sync a bit down)

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

can you say a bit about var_initialized_on_entry

Albin Stjerna (Nov 19 2019 at 14:31, on Zulip):

Ok, so it solves an off-by-one problem

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

is that initialized_at from the code?

Albin Stjerna (Nov 19 2019 at 14:31, on Zulip):

Not really

Albin Stjerna (Nov 19 2019 at 14:31, on Zulip):

initialized_at says that something becomes initialised at mid-point of somewhere

Albin Stjerna (Nov 19 2019 at 14:32, on Zulip):

var_initialized_on_exit is the "propagated" version of that; it moves across the CFG as you would expect

Albin Stjerna (Nov 19 2019 at 14:32, on Zulip):

but it stops at a move

Albin Stjerna (Nov 19 2019 at 14:32, on Zulip):

Which means that every move would have a move error (I think)

Albin Stjerna (Nov 19 2019 at 14:33, on Zulip):

So what it says intuitively is that if we know that a move is initialized on exit from somewhere, we also know that it's initialized when arriving at the successor (but not necessarily when leaving it)

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

var_initialized_on_exit is the "propagated" version of that; it moves across the CFG as you would expect

two questions

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

first, the image above says var_initialized_on_*entry*

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

second, it says it's a "fact"

Albin Stjerna (Nov 19 2019 at 14:34, on Zulip):

There's two of them, and they are facts from the perspective of liveness

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

I see

Albin Stjerna (Nov 19 2019 at 14:35, on Zulip):

I'm kind of fudging it in the table

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

I hadn't thought about the question of distinct "phases"

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

I guess it makes sense to start with the move stuff? (that is kind of the first phase?)

Albin Stjerna (Nov 19 2019 at 14:36, on Zulip):

I guess, yes

Albin Stjerna (Nov 19 2019 at 14:36, on Zulip):

I mean, the move analysis forks

Albin Stjerna (Nov 19 2019 at 14:36, on Zulip):

One part goes into liveness, and the other continues to become move errors

Albin Stjerna (Nov 19 2019 at 14:37, on Zulip):

But computationally the move analysis happens first :)

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

I really should just down your thesis right now, shouldn't I

Albin Stjerna (Nov 19 2019 at 14:38, on Zulip):

It might be the fastest way to understand what I'm doing yes

Albin Stjerna (Nov 19 2019 at 14:38, on Zulip):

But don't read the old one

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

send me the correct link

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

let's dial back a bit

Albin Stjerna (Nov 19 2019 at 14:38, on Zulip):

here's the newest draft

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

I'm thinking that a flat hackmd with "all the rules" is probably not best

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

let's start by writing out the overall flow

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

I'm guessing that's in the thesis

Albin Stjerna (Nov 19 2019 at 14:40, on Zulip):

I have these, which are less accurate now:
Very high Slightly lower

Albin Stjerna (Nov 19 2019 at 14:40, on Zulip):

(move errors are kind of a happy bonus)

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

heh, just found those

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

(this is really quite beautifully done)

Albin Stjerna (Nov 19 2019 at 14:41, on Zulip):

Thank you!

Albin Stjerna (Nov 19 2019 at 14:42, on Zulip):

I really needed to hear that, given that I had literally no input for months, then got "ok but this is incomprehensible" as feedback from my subject reviewer, then spent almost two months' of evenings and weekends rewriting it into this

Albin Stjerna (Nov 19 2019 at 14:43, on Zulip):

It wasn't all bad though because I didn't like the first version, and I do like this one

Albin Stjerna (Nov 19 2019 at 14:43, on Zulip):

And as I said, it should be straightforward to cannibalise it into the book

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

sorry for not giving you more feedback earlier :)

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

anyway, I think the "big picture" is this:

Albin Stjerna (Nov 19 2019 at 14:45, on Zulip):

It's all right, I'm blaming Tobias more than you :)

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

me too :P

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

(I have to find a better phrasing for the last part, since it doesn't account for 'killed' loans, but anyway)

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

oh and I forgot to add that liveness uses initialization to make its results more precise

Albin Stjerna (Nov 19 2019 at 14:47, on Zulip):

I think it would be incorrect without it, but yes

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

so in terms of your PR btw

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

it's useful for me to pull this stuff together, but what do you see as the actual bits of coding needed before it can land?

Albin Stjerna (Nov 19 2019 at 14:49, on Zulip):

It took me a long time to realise that conceptually it's not that a drop of something moved is a no-op, it's not even the responsibility of that drop, given that the object has been moved to somewhere else (which should drop it).

Albin Stjerna (Nov 19 2019 at 14:49, on Zulip):

Hmm, I would need to change some things in rustc

Albin Stjerna (Nov 19 2019 at 14:49, on Zulip):

Notably, I need to emit accessed_at() at start and not mid-point

Albin Stjerna (Nov 19 2019 at 14:49, on Zulip):

Also make child() non-transitive

Albin Stjerna (Nov 19 2019 at 14:50, on Zulip):

(not required, but reasonable)

Albin Stjerna (Nov 19 2019 at 14:50, on Zulip):

And perhaps rename path_belongs_to_var to something like path_starts_in_var

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

(I'm skimming the code in the PR itself, which so far seems very good)

Albin Stjerna (Nov 19 2019 at 14:51, on Zulip):

Also, I do we want to use Hungarian notation and have _var pre- and suffixes?

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

I think we should rename child to parent

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

for consistency with ancestor

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

(side note)

Albin Stjerna (Nov 19 2019 at 14:52, on Zulip):

Hm, yes, I have both, but I need to index it from the left

Albin Stjerna (Nov 19 2019 at 14:52, on Zulip):

Or at some point I had both anyway

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

Also, I do we want to use Hungarian notation and have _var pre- and suffixes?

I don't quite follow this

Albin Stjerna (Nov 19 2019 at 14:52, on Zulip):

Ok so many but not all relations follow a convention where they record what they are relations between

Albin Stjerna (Nov 19 2019 at 14:53, on Zulip):

For example var_uses_region

Albin Stjerna (Nov 19 2019 at 14:53, on Zulip):

(Which I guess is now called something else)

Albin Stjerna (Nov 19 2019 at 14:53, on Zulip):

Given that we typically know the type of the relations, var and region are sort of redundant, right?

Albin Stjerna (Nov 19 2019 at 14:53, on Zulip):

Also, we are inconsistent with this

Albin Stjerna (Nov 19 2019 at 14:54, on Zulip):

We are also inconsistent with the _at suffix

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

good video on the topic (which kinda disagrees with the premise that knowing the types of the arguments is always redundant to the relation name) https://www.youtube.com/watch?v=Uska9DgJEoo

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

I agree we are somewhat inconsistent :)

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

I don't feel the need to record 100% of the types

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

in the name

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

and I definitely don't want to go full-on pn_moved_out or something

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

but I do find that having some redundancy helps me when reading

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

I view the types in the declarations as being for the compiler

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

and the types in the names as being for the reader

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

but e.g. moved_out_at(Path, Node) .. hmm .. path_moved_out_at(Path, Node) feels like an improvement, likely

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

path_moved_out_at_node, not sure :)

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

I definitely like the ordering of the arguments to "match" the name somehow

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

maybe just writing everything out would feel better?

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

I'm thinking about e.g. contains -- something like origin_contains_loan... probably clearer ..

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

on the other hand I was pretty happy with placeholder(Origin, Loan)

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

and I cannot imagine that "hungarian style notation" would improve that

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

(it's not a verb, I guess)

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

the other thing we sometimes have to record if foo_base vs foo (transitive)

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

@Albin Stjerna some other inconsistencies, which seem perhaps more imporant:

Albin Stjerna (Nov 19 2019 at 15:05, on Zulip):

Hmm

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

seems related to transitive vs direct

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

maybe best answered by just not using the term "moved" for both

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

I guess that is path_maybe_uninitialized_on_entry?

Albin Stjerna (Nov 19 2019 at 15:06, on Zulip):

Hm, yes, I guess so

Albin Stjerna (Nov 19 2019 at 15:06, on Zulip):

These include/exclude things are really tricky

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

@Albin Stjerna so var_maybe_initialized_on_exit

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

this is specifically concluding: is there any subpath of the variable that is initialized

Albin Stjerna (Nov 19 2019 at 15:11, on Zulip):

It used to be that

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

hmm

Albin Stjerna (Nov 19 2019 at 15:11, on Zulip):

It's not anymore

Albin Stjerna (Nov 19 2019 at 15:11, on Zulip):

It's the opposite

Albin Stjerna (Nov 19 2019 at 15:11, on Zulip):

It specifically tracks if the root path of x was moved

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

I guess the question is what this input means

nikomatsakis (Nov 19 2019 at 15:12, on Zulip):
path_belongs_to_var
Albin Stjerna (Nov 19 2019 at 15:12, on Zulip):

You asked when I introduced it and you were right

Albin Stjerna (Nov 19 2019 at 15:12, on Zulip):

I want to change it to path_is_root_of_var or something like that

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

I think is should just be

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

path_is_var

Albin Stjerna (Nov 19 2019 at 15:13, on Zulip):

...yes, that works better

Albin Stjerna (Nov 19 2019 at 15:13, on Zulip):

It's what we want for drop-liveness anyway, right?

Albin Stjerna (Nov 19 2019 at 15:13, on Zulip):

Because we only care about full moves

Albin Stjerna (Nov 19 2019 at 15:13, on Zulip):

Given that the drop() override is attached to whatever was rooted at that variable

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

well that was the next question

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

I mean if the variable is partly initialized

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

we still have to drop those parts that remain

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

I guess I'll check it out when I get that far

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

ps I've been editing the hackmd

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

I see that

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

not sure if you're following along at all

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

ok

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

I am!

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

...sort of

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

I'm doing some on the fly renaming :P

Albin Stjerna (Nov 19 2019 at 15:15, on Zulip):

...ok not sufficiently

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

I think we should start documenting conventions at the top maybe

Albin Stjerna (Nov 19 2019 at 15:15, on Zulip):

YES

Albin Stjerna (Nov 19 2019 at 15:16, on Zulip):

hmm, wait

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

I'm taking a stab at some, feel free to tell me that they are bad :)

Albin Stjerna (Nov 19 2019 at 15:16, on Zulip):

There was a reason why paty_maybe_moved_... was called that

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

(I think we're not consistently following them yet)

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

There was a reason why paty_maybe_moved_... was called that

what was that

Albin Stjerna (Nov 19 2019 at 15:16, on Zulip):

Uninitialised should be deinitialised

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

ah, interesting

Albin Stjerna (Nov 19 2019 at 15:16, on Zulip):

Because this relation does not capture a variable that has never been initialised

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

Ok, +1 to deinitialized

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

that said

Albin Stjerna (Nov 19 2019 at 15:17, on Zulip):

That would have required starting at the root of the CFG, which I did not have

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

I just proposed the convention of on_entry vs at to distinguish "instantaneous" things from "over path" things

Albin Stjerna (Nov 19 2019 at 15:17, on Zulip):

Ok, sounds reasonable

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

so we could maybe just use moved

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

though I sort of like the idea of also trying to separate out the property

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

e.g., initialized_at vs initialized_on_entry

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

we would need a different name for the former otherwise, which is maybe ok ("assigned"?)

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

ok so at would be my on exit?

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

well I mean we have initialized_at which is an input fact, right?

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

Aah ok you meant like that

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

that just says "there is an initialization at this point"

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

Ok that makes sense

Albin Stjerna (Nov 19 2019 at 15:19, on Zulip):

So any input fact would be _at, and the computed relations would be _on_entry or on_exit

Albin Stjerna (Nov 19 2019 at 15:19, on Zulip):

Makes sense!

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

but shall we also try to have distinct "relation names"?

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

I just updated to assigned_at for example and I think it's useful

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

redundancy ftw

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

You mean from facts? I guess it makes sense too

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

yeah, I am doing that

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

which suggests "deinitialized"

Albin Stjerna (Nov 19 2019 at 15:21, on Zulip):

that's ok I think?

Albin Stjerna (Nov 19 2019 at 15:21, on Zulip):

Or moved?

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

I think "deinitialized" is good

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

"move" is the action

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

"deinitialized" is the state

Albin Stjerna (Nov 19 2019 at 15:22, on Zulip):

That tracks, because I can imagine other types of deinitialisation perhaps maybe I don't know

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

right

Albin Stjerna (Nov 19 2019 at 15:22, on Zulip):

In some future version of Rust

Albin Stjerna (Nov 19 2019 at 15:23, on Zulip):

Or maybe if there's weirdness involved, like I don't know inline assembly or something

Albin Stjerna (Nov 19 2019 at 15:23, on Zulip):

Matthew said there were edge cases with inline assembly that wouldn't work with what I'm doing

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

heh oh dear

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

ok well I'm just reading through the code and transcribing

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

so far so good

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

I've updated the names, hopefully consistently

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

me and @lqd said yesterday that we'd probably try to go over the code at the end

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

to try and make it match the names in the hackmd

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

which introduces some "mapping confusion" for the time being but hopefully we can handle it

Albin Stjerna (Nov 19 2019 at 15:25, on Zulip):

Hmm, this looks wrong though:

path_maybe_deinitialized_on_entry(Path, Node) :-
    path_moved_at(Path, Node).
nikomatsakis (Nov 19 2019 at 15:25, on Zulip):

should probably record the names from the code

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

yes, it does

Albin Stjerna (Nov 19 2019 at 15:25, on Zulip):

I'm with deinitialized on exit, but not on entry

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

yes, though your comment suggests otherwise

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

score on for naming conventions

Albin Stjerna (Nov 19 2019 at 15:26, on Zulip):

Yes, definitely

nikomatsakis (Nov 19 2019 at 15:26, on Zulip):
    // path_maybe_moved_at(Path, Point): There exists at least one path through
    // the CFG to Point such that `Path` has been moved out by the time we
    // arrive at `Point` without it being re-initialized for sure.
Albin Stjerna (Nov 19 2019 at 15:26, on Zulip):

Makes that much clearer and might have been a bug

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

"we arrive at"

Albin Stjerna (Nov 19 2019 at 15:27, on Zulip):

The tell-tale sign is that it has the same shape as initialized_on_exitbut not the same suffix :)

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

I'm trying to remember

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

is there a reason to distinguish "definitely initialized" from "maybe deinitialized"?

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

ah well I guess it's exactly

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

the fact that uninitialized things are distinct?

Albin Stjerna (Nov 19 2019 at 15:30, on Zulip):

maybe deinitialized doesn't capture "never initialized"

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

right

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

in some versions of the compiler at least

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

we generated a "move" for a let x that does not initialize x

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

but anyway

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

I'm definitely finding this naming convention helpful

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

e.g.

nikomatsakis (Nov 19 2019 at 15:30, on Zulip):
path_definitely_initialized_on_exit(Path, Node) :-
    path_maybe_initialized_on_exit(Path, Node),
    !path_maybe_deinitialized_on_exit(Path, Node).
nikomatsakis (Nov 19 2019 at 15:31, on Zulip):

vs path_definitely_initialized_at

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

I would have guessed that the latter meant "on entry"

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

but it must be on exit...

Albin Stjerna (Nov 19 2019 at 15:31, on Zulip):

Yes, it's much clearer

Albin Stjerna (Nov 19 2019 at 15:31, on Zulip):

I feel like I need to draw this actually

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

I'm not.. entirely convinced this is true

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

e.g.

Albin Stjerna (Nov 19 2019 at 15:32, on Zulip):

No, set subtraction is weird

nikomatsakis (Nov 19 2019 at 15:32, on Zulip):
let a;
if something() { a = 44; }
print(a);
nikomatsakis (Nov 19 2019 at 15:32, on Zulip):

here a is "maybe initialized"

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

but it is not "maybe deinitialized"

Albin Stjerna (Nov 19 2019 at 15:32, on Zulip):

hmmmm

Albin Stjerna (Nov 19 2019 at 15:33, on Zulip):

Ok so maybe I didn't solve the problem I thought I solved

Albin Stjerna (Nov 19 2019 at 15:34, on Zulip):

Or well, it did solve the problem I was trying to solve, which was just

let a;
print(a);
nikomatsakis (Nov 19 2019 at 15:35, on Zulip):

it seems like we need some sort of action for "uninitialized variable"

Albin Stjerna (Nov 19 2019 at 15:35, on Zulip):

Yes, I guess we do

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

e.g. maybe some facts that indicate the root

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

this could take many forms

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

well wait

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

er ok I guess that we can't readily do "intersection" of many flows

Albin Stjerna (Nov 19 2019 at 15:37, on Zulip):

No, I ran into that problem many times trying to design this solution

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

I imagine this might take the form then of a start_node fact and perhaps initialized_at(Path, Node) facts for the parameters

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

No, I ran into that problem many times trying to design this solution

yes I think this is (well, partly) why we have traditionally propagated "moves"

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

(I think the other reason was that it's better for errors)

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

I'm not wild about start_node fact -- have to think -- well I guess it's ok. I'm just thinking about what to do for unreachable code blocks

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

I don't honestly know what the current borrow checker does

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

(answer: you don't get errors from dead code (playground))

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

that's what I thought, though I couldn't quite remember where we landed

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

I imagine this might take the form then of a start_node fact and perhaps initialized_at(Path, Node) facts for the parameters

actually I guess this doesn't work

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

you really need something to enumerate the set of "uninitialized" variables

Albin Stjerna (Nov 19 2019 at 15:42, on Zulip):

Hm, yes I guess

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

I'm going quickly to check how borrow checker handles error reporting btw

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

The hard part is formulating this without saying something about all edges going into a node

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

Which we cannot capture

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

tracking "uninitialized" things seems easy enough

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

You mean, as in never initialised?

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

yeah

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

like if we had local_variable(Var) facts and start_node(Node)

Albin Stjerna (Nov 19 2019 at 15:44, on Zulip):

What would local_variable do?

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

you could do

path_maybe_uninitialized_on_exit(Path, Node) :-
    local_variable(Var),
    path_is_var(Path, Var),
    start_node(Node)
nikomatsakis (Nov 19 2019 at 15:45, on Zulip):

or alternatively the compiler could generate path_moved_at facts for all local variables at the start node

Albin Stjerna (Nov 19 2019 at 15:45, on Zulip):

And local_variable() would essentially mean "not an argument"?

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

correct

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

we probably also want to record the arguments as initialzied -- but I guess we must already generate path_initialized_at facts for those

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

now that I think about it

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

or else we'd get errors all over the place

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

(seems worth noting)

Albin Stjerna (Nov 19 2019 at 15:46, on Zulip):

Yes, I guess we must

Albin Stjerna (Nov 19 2019 at 15:46, on Zulip):

Hmm, no I'm not sure come to think about it

Albin Stjerna (Nov 19 2019 at 15:47, on Zulip):

No wait, that works, for some reason

Albin Stjerna (Nov 19 2019 at 15:47, on Zulip):

...yes because the arguments get initialized at the start of the block

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

ok, so, from skimming the code it appears to me that

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

the current borrow checker is also tracking "uninitialized paths"

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

which seems good

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

I know at some point we tracked instead "in-scope moves", in a sense

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

but I think we now compute those lazilly at the point of error instead

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

this suggests to me @Albin Stjerna that the most consistent thing would be to add path_moved_at actions at the start block for local variables

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

(or some other name that winds up "unioned together")

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

but I think we now compute those lazilly at the point of error instead

specifically, in the get_moved_indices method, which I vaguely recall now

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

In that case, I thnk we can rename to path_maybe_uninitialized_on_exit and remove the "known initialized" computation altogether

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

(which I have done in the doc, along with noting the assumption that path_moved_at includes tuples for all local variables at the start point)

Albin Stjerna (Nov 19 2019 at 15:56, on Zulip):

Ok, sounds good!

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

I will note though that it should be possible to compute intersection too, as the cfg-edge is a fact

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

There are extensions to datalog that include cerain operators

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

If we wanted, one could imagine coding that up

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

But let's not go there for now

Albin Stjerna (Nov 19 2019 at 15:57, on Zulip):

Nah

Albin Stjerna (Nov 19 2019 at 15:57, on Zulip):

Ok good, then I can just fix that in my report as well and it will be...probably correct

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

lol

Albin Stjerna (Nov 19 2019 at 15:59, on Zulip):

I'll have a look at emitting the facts in Rust

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

if I'm not mistaken

nikomatsakis (Nov 19 2019 at 15:59, on Zulip):
        // move_error(path, point) :-
        //     path_accessed_at(path, point),
        //     !path_definitely_initialized_at(path, point).
nikomatsakis (Nov 19 2019 at 15:59, on Zulip):

is wrong

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

precisely because of the on-entry vs on-exit confusion

Albin Stjerna (Nov 19 2019 at 16:00, on Zulip):

a-ha!

nikomatsakis (Nov 19 2019 at 16:01, on Zulip):
move_error(Path, TargetNode) :-
    cfg_edge(SourceNode, TargetNode),
    path_accessed_at(Path, TargetNode),
    path_maybe_uninitialized_on_exit(SourceNode).
Albin Stjerna (Nov 19 2019 at 16:01, on Zulip):

So the join we want is path_definitely_initialized_on_entry?

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

that seems more correct, right?

nikomatsakis (Nov 19 2019 at 16:01, on Zulip):
move_error(Path, TargetNode) :-
    path_maybe_uninitialized_on_exit(Path, SourceNode),
    cfg_edge(SourceNode, TargetNode),
    path_accessed_at(Path, TargetNode).
nikomatsakis (Nov 19 2019 at 16:02, on Zulip):

reordered and minor nits fixed

Albin Stjerna (Nov 19 2019 at 16:02, on Zulip):

Hm yes that looks correct to me

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

The fact that this is no longer an antijoin might speed things up dramatically

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

ok, so the only remaining bit of confusion here

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

Also, eliminate most of the pipeline

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

is precisely what var_maybe_initialized_on_exit should be

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

I think it probably wants to be "any subpart of this variable is initialized"

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

however, I'm trying to remember just what we do in the existing borrow check

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

I know it's a bit.. more complex than that

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

or maybe it's not

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

(in particular, the role of this variable is to suppress drops where the value is dropped but not, in fact, initialized, right?)

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

but let me start looking at liveness now, I guess

Albin Stjerna (Nov 19 2019 at 16:06, on Zulip):

(in particular, the role of this variable is to suppress drops where the value is dropped but not, in fact, initialized, right?)

It's only used when a variable implements its own deallocator

Albin Stjerna (Nov 19 2019 at 16:07, on Zulip):

We use it when a drop of a variable may happen, and that variable overrides drop() in order to force any origin inside of that variable (which may be a compex struct) to be live

Albin Stjerna (Nov 19 2019 at 16:07, on Zulip):

That's all

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

Yeah, I think that the more complex part comes when computing the invalidates facts

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

ps, that would be better renamed to loan_invalidated_at...

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

OK, bikeshed time

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

or

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

or something like that

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

the latter is probably too long

Albin Stjerna (Nov 19 2019 at 16:17, on Zulip):

It's a bit long yes

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

(note that the term provenance doesn't (I don't think) read any better here)

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

No, and I don't like "uses" either

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

It's too abstract; what is happening here is...more concrete than that

Albin Stjerna (Nov 19 2019 at 16:19, on Zulip):

var_may_come_from_origin?

Albin Stjerna (Nov 19 2019 at 16:19, on Zulip):

var_may_refer_to_origin?

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

var_refers_to_origin is ok

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

but what about var_drops_origin

Albin Stjerna (Nov 19 2019 at 16:22, on Zulip):

Yes that's very opaque

Albin Stjerna (Nov 19 2019 at 16:22, on Zulip):

Also, the relation is really indirect

Albin Stjerna (Nov 19 2019 at 16:22, on Zulip):

the origin is...used in a drop of var

Albin Stjerna (Nov 19 2019 at 16:25, on Zulip):

Haha, I just found this code, which I apparently wrote:

// Arguments are initialized on function entry
            InitLocation::Argument(local) => {
                assert!(body.local_kind(local) == LocalKind::Arg);
                let fn_entry = Location {block: BasicBlock::from_u32(0u32), statement_index: 0 };
                all_facts.initialized_at.push((init.path, location_table.start_index(fn_entry)));

            }
Albin Stjerna (Nov 19 2019 at 16:25, on Zulip):

So ok, that was me

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

I like my descritpion

nikomatsakis (Nov 19 2019 at 16:26, on Zulip):
// References with the given origin may be
// dereferenced when the variable is used
.decl var_uses_origin(Variable, Origin)

// References with the given origin may be
// dereferenced when the variable is dropped
.decl var_drops_origin(Variable, Origin)
nikomatsakis (Nov 19 2019 at 16:26, on Zulip):

but I don't know how to turn those comments into concise relation names :)

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

use_of_var_derefs_origin(Var, Origin)

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

drop_of_var_derefs_origin(Var, Origin)

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

maybe?

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

var_use_derefs_origin / var_drop_derefs_origin ?

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

also plausible

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

ps @Albin Stjerna I am pretty sure that we want to compute (what I am calling) var_maybe_partly_initialized_on_exit -- i.e., it's true if any sub-path of the variable is initialized.

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

I'll have to check the code but I feel like that must be what it is using

Albin Stjerna (Nov 19 2019 at 16:31, on Zulip):

Hmm, that's what I was computing before

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

(that said, I could imagine us trying to make this more precise in the future)

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

e.g. if you have

Albin Stjerna (Nov 19 2019 at 16:31, on Zulip):

I think I got the same liveness output if I made it simpler

nikomatsakis (Nov 19 2019 at 16:32, on Zulip):
let x = (vec![], vec![]);
drop(x.1);
nikomatsakis (Nov 19 2019 at 16:32, on Zulip):

the drop of x is still going to drop x.0, and is hence still relevant

Albin Stjerna (Nov 19 2019 at 16:32, on Zulip):

(working on initial moves for non-arguments)

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

ok, well, we should work this out

Albin Stjerna (Nov 19 2019 at 16:33, on Zulip):

Yes, we should

Albin Stjerna (Nov 19 2019 at 16:33, on Zulip):

The question I guess becomes what MIR that will translate to

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

the MIR will have a drop of X in that case

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

there is a later pass that converts it to drop(x.0), but it hasn't executed yet

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

I will check the code in a bit

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

I'm still going over the liveness rules

Albin Stjerna (Nov 19 2019 at 16:35, on Zulip):

I think what would happen is that the MIR would have an extraction of x.1 into a variable, and then drop that variable

Albin Stjerna (Nov 19 2019 at 16:35, on Zulip):

And then that variable would be initialized

Albin Stjerna (Nov 19 2019 at 16:35, on Zulip):

according to Polonius

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

I gotta find some place to drop other notes

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

e.g., there is an efficiency thing

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

in particular in the borrow checker, we stop computing "drop-use" ranges when we see that something is "use live"

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

because we know that a full use always uses all the origins that a drop-use would use

Albin Stjerna (Nov 19 2019 at 16:37, on Zulip):

That's smart

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

this might dramatically reduce the number of tuples

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

in certain cases, at least

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

well... up to 2x I guess :)

Albin Stjerna (Nov 19 2019 at 16:37, on Zulip):

Drop-liveness is incredibly uncommon

Albin Stjerna (Nov 19 2019 at 16:38, on Zulip):

Remember, I think we only compute this for structs that implement drop()

Albin Stjerna (Nov 19 2019 at 16:38, on Zulip):

Maybe not all the precursors perhaps

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

Yes, I know

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

It's ok as is for now

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

I noted it as an "opt opportunity"

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

var_use_derefs_origin / var_drop_derefs_origin ?

I think this one is probably best from our bikeshed? or else use_of_var...

Albin Stjerna (Nov 19 2019 at 16:40, on Zulip):

Yes, I agree!

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

I personally find the use_of_var_derefs_origin a bit clearer, if verbose

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

mostly because my brain keeps trying to read "use" as a verb

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

and not a noun

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

but I would go with whichever

Albin Stjerna (Nov 19 2019 at 16:46, on Zulip):

Me too

Albin Stjerna (Nov 19 2019 at 16:46, on Zulip):

I don't have a strong preference either way

Albin Stjerna (Nov 19 2019 at 16:46, on Zulip):

I'm going to head home soon by the way, and have dinner

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

It seems the test cases I wrote all work, and so does Niko's, when I add moves at the start of the function!

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

woohoo

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

not sure if you saw but I've basically finished writing up the rules in hackmd

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

they diverge slightly from your branch in the ways we discussed

Albin Stjerna (Nov 19 2019 at 17:00, on Zulip):

That's good; I'll fix the branch to follow your suggestions

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

I ... think they are correct :)

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

let me know if you see any discrepancies

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

(sorry I wasn't able to follow much (if any) of what was going on :/ but I see you two have made a lot of concrete progress on naming, rules, reviewing most of the pipeline, etc thank you @Albin Stjerna and @nikomatsakis for your time y'all are awesome)

Albin Stjerna (Nov 19 2019 at 17:01, on Zulip):

My gut feeling says the rules you have will run significantly faster than the ones I had before

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

They seem to require less fighting with Datafrog

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

when we're all done with this, we need to write up a "sprint report" for Inside Rust blog

Albin Stjerna (Nov 19 2019 at 17:05, on Zulip):

Note that one of the todos in my PR is precisely what you were arguing against, @nikomatsakis, that is that we can get away with not computing partial initialization for drop-liveness :)

Albin Stjerna (Nov 19 2019 at 17:05, on Zulip):

I'm still not convinced

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

I should come up with a good test

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

the new renaming, analyses descriptions, etc, in the hackmd, are super cool, great job

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

My plan is to add them to the book in my PR as well

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

Ok, I have spent most of the day implementing most of the rules Niko described, including renamings

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

of...virtually all liveness-and-initialization-touching facts

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

Which I just finished, coming soon in the PR I hope

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

@Albin Stjerna nice <3

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

You say NOW, wait until you see the diff

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

Just imagine the fact regeneration mess

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

The PR is now completely unreadable

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

@nikomatsakis If it turns out you can convince me that we need to worry about partial initialization for drops, I propose that we just join path_is_var through ancestor and use that rather than extra facts.

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

I gave up already and implemented that :)

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

This means that the initialization thing just needs a book entry

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

And then it's ready for reveiw

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

It made the initialization pipeline super clean

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

Because now there's two steps where the first one consumes all inputs and elaborates, and the other one starts from the first one's conclusions

nikomatsakis (Nov 22 2019 at 01:49, on Zulip):

I gave up already and implemented that :)

@Albin Stjerna so I thought about the question of whether you need to track partial initialization. I think the example I was imagining was one like this:

let mut x, y;
let v = (vec![&x], vec![&y]);
drop(v.1);
// here, because `v` will be dropped, I think both x and y are *both* considered borrowed still

OK, actually, that example doesn't error -- but that's because we know that Vec doesn't refernce its data. This version does error, when we use a random type with a dtor.

nikomatsakis (Nov 22 2019 at 01:49, on Zulip):

I realized as I was writing it up though that the way the rules are written, I think

nikomatsakis (Nov 22 2019 at 01:50, on Zulip):

you will have here 2 initialized paths -- v and v.0 -- and one uninitialized path -- v.1

nikomatsakis (Nov 22 2019 at 01:50, on Zulip):

it may well therefore be true that we only need to consider the local variable pathv

nikomatsakis (Nov 22 2019 at 01:50, on Zulip):

however

nikomatsakis (Nov 22 2019 at 01:50, on Zulip):

well it still feels "more right" to me to consider all the paths :)

nikomatsakis (Nov 22 2019 at 01:51, on Zulip):

but I guess the point is that initialized_on_entry(Path, Point) (or whatever we called it) really means that the path is (at least) partially initialized on entry

nikomatsakis (Nov 22 2019 at 01:51, on Zulip):

and, at least sometimes, we will have subpaths -- so for it to be fully initialized, all subpaths must also be present

nikomatsakis (Nov 22 2019 at 01:51, on Zulip):

sorry if this is a conversation we already had

nikomatsakis (Nov 22 2019 at 01:52, on Zulip):

I guess I would say, with that understanding, and if we document the relation in that way, I am comfortable with the version that just checks for the path that is equal to the variable -- but I also think they are both equivalent

nikomatsakis (Nov 22 2019 at 01:52, on Zulip):

anyway so what branches here are ready for merge :)

Albin Stjerna (Nov 22 2019 at 10:18, on Zulip):

We could merge my PR I think, and I could send a later PR documenting it in the book

Albin Stjerna (Nov 22 2019 at 10:19, on Zulip):

"My PR" = polonius#135

Albin Stjerna (Nov 22 2019 at 10:22, on Zulip):

I don't know why cargo fmt errors on CI; my cargo fmt doesn't suggest any changes???

lqd (Nov 22 2019 at 10:50, on Zulip):

a couple notes, 1) I think you don't need to into_iter/iter.collect, you could extend(x.iter()) (or sometimes it's also possible to just move the relation from your context into the variables) 2) Vec::new isn't an expensive operation, so no real need to avoid one creation with the or_insert_with(Vec::new), that being said, it's probably easier/best to use or_default instead

lqd (Nov 22 2019 at 13:33, on Zulip):

3) how much of these new/updated .facts datasets do we need ? I think a lot of those were added as unit tests back in the first liveness PRs, but then were removed from the tests, but the ./inputs/ datasets were kept IIRC. They might have already served their purpose, or are you often rerunning polonius with all these liveness and initialization datasets ? if they're less useful now than they were before, maybe we can delete the ones we don't re-run often and are not automatically checked by the unit tests, what do you think ?

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

a couple notes, 1) I think you don't need to into_iter/iter.collect, you could extend(x.iter()) (or sometimes it's also possible to just move the relation from your context into the variables) 2) Vec::new isn't an expensive operation, so no real need to avoid one creation with the or_insert_with(Vec::new), that being said, it's probably easier/best to use or_default instead

Thanks! I did that because it was suggested by Clippy, I could of course change that back :)

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

3) how much of these new/updated .facts datasets do we need ? I think a lot of those were added as unit tests back in the first liveness PRs, but then were removed from the tests, but the ./inputs/ datasets were kept IIRC. They might have already served their purpose, or are you often rerunning polonius with all these liveness and initialization datasets ? if they're less useful now than they were before, maybe we can delete the ones we don't re-run often and are not automatically checked by the unit tests, what do you think ?

Very few of them, and I think it makes sense to aim for using polonius-parser etc instead

lqd (Nov 26 2019 at 20:09, on Zulip):

ok then we can clean this up later, after move errors land

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

Sounds good! I'd like to write something in the book and look at extending the parser as well, but I'm not sure how much time I have this week

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

I've been procrastinating the actual research I'm supposed to do a bit too much :(

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

I was about to ask/look for what you'd need in the parser ?

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

Basically none of the facts I added exist there yet

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

And I'm not sure how to handle variables in general, to be honest

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

Because explicitly declaring both path parent/child relations and variables seems a bit redundant

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

indeed

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

the liveness facts would need to be added as well, right ? not just the initialization ones ?

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

ah no, some are already there

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

Yes, but I think they are incomplete

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

I'd have to do an inventory :)

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

But I think I know enough to write the rules without any greater problems

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

I just don't have time right now

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

to write the initialization/move errors rules you mean ?

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

or something related to the parser and unit tests

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

Both :)

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

But yes, the parser, and the unit tests

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

As in "the last bits of work to do on initialisation"

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

if you already have in mind how they're supposed to work, and have the time to leave a couple notes somewhere, I can look at it if it would help

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

Sure! I'll see if I can describe it in the PR sometime tomorrow

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

No wait, no time like the present

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

alright :)

lqd (Nov 26 2019 at 20:25, on Zulip):

I'll have a little unexpected time since what I was planning on doing apparently needs to wait for niko to be back, so I can look at this parser yhing for the initialization facts earlier than I thought

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

Ah!

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

Ok, it's here: https://github.com/rust-lang/polonius/pull/135#issuecomment-558809090

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

I wrote some discussion of what I think should be done as well

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

Because I'm not clear how "bare bones" the input should be, and I think it makes a lot of sense to do some abstracting

lqd (Nov 26 2019 at 20:49, on Zulip):

sweet, thank you :)

Albin Stjerna (Nov 26 2019 at 21:01, on Zulip):

Hey, you're the one who just volunteered to do my work for me :heart:

lqd (Nov 26 2019 at 21:55, on Zulip):

ofc whatever we do here will be less validating than rustc's tests, so integrating init/move errors will be the most important :)

Last update: Mar 31 2020 at 02:05UTC