Finalise initialisation calculations #110

amandasystems · 2019-08-06T09:54:49Z

This PR will:

finally remove region_live_at
implement enough initialisation tracking to correctly calculate drop-uses for liveness
extend polonius-parser to work in this new universe

Notably, it will not calculate the full move analysis, as that would a) probably take a lot of time and b) require refactoring of the entire Polonius pipeline, or at the very least extensions to handle more types of errors.

This notably excludes syntax extensions for the new facts.

nikomatsakis

Looking good! Thoughts attached. =)

nikomatsakis · 2019-08-28T12:40:43Z

polonius-engine/src/facts.rs

-    /// `var_initialized_on_exit(V, P) when the variable `V` is initialized on
-    /// exit from point `P` in the program flow.
-    pub var_initialized_on_exit: Vec<(V, P)>,
+    /// `child(M1, M2) when the move path `M1` is the child of `M2`.


I think it'd be useful to give an example. For example, I imagine:

child(M1, M2) would be true If M1 represents a.b.c and M2 represents a.b.

That's true. The hand-wavyness was because I was not entirely sure if it was transitive or not. It is, though, which may or may not be what we want.

Interesting. The name strongly suggests non-transitive to me. I would have said something like descendant for a transitive child relationship.

True, I'll make a note of fixing this at some point.

nikomatsakis · 2019-08-28T12:40:59Z

polonius-engine/src/facts.rs

+    pub child: Vec<(M, M)>,
+
+    /// `path_belongs_to_var(M, V) when the move path `M` starts in variable `V`.
+    pub path_belongs_to_var: Vec<(M, V)>,


Why 'belongs to'? I think maybe path_starts_with_var or something.

I called it that originally, but I got confused and was unsure if it held transitively (it doesn't). I'll change it to something better.

Hmm. I'm not sure what "transitive" means in this case?

"Includes descendants"

nikomatsakis · 2019-08-28T12:41:42Z

polonius-engine/src/facts.rs

+    pub path_belongs_to_var: Vec<(M, V)>,
+
+    /// `initialized_at(M, P) when the move path `M` was initialized at point
+    /// `P`.


Again, I think an example would be good --

If we have some Rust code like:

x.y = 3 // point P

where M1 represents x.y, then we would have initialized_at(M1, P).

Reading over the code I had a few questions. Are you assuming that:

a = (22, 44);

would generate:

initialized_at(a); initialized_at(a.0); initialized_at(a.1);

?

I think my preference would NOT to assume that -- that is, I think the compiler should give us just initialized_at(a), and if we care to elaborate the closure with respect to child paths, we do it ourselves.

Yes, I had to investigate what the current fact generation actually does, and it only generates the fact for the path being initialized directly. I'll clarify this in the comments and add an example.

nikomatsakis · 2019-08-28T12:41:47Z

polonius-engine/src/facts.rs

+    /// `P`.
+    pub initialized_at: Vec<(M, P)>,
+
+    /// `moved_out_at(M, P) when the move path `M` was moved at point `P`.


Similarly, are we assuming here that drop(a); would generate moved_out(a.0) and moved_out(a.1) facts?

Same as above -- I think we should do the elaboration ourselves.

polonius-engine/src/facts.rs

nikomatsakis · 2019-08-28T12:43:38Z

polonius-engine/src/output/initialization.rs

+
+use datafrog::{Iteration, Relation, RelationLeaper};
+
+pub(super) fn init_var_maybe_initialized_on_exit<Region, Loan, Point, Variable, MovePath>(


This function definitely wants a comment with some kind of Rust example showing where it's true and not true.

polonius-engine/src/output/initialization.rs

nikomatsakis · 2019-08-28T13:00:06Z

polonius-engine/src/output/initialization.rs

+
+        // path_maybe_initialized_on_exit(Mother, P) :-
+        //     path_maybe_initialized_on_exit(Daughter, P),
+        //     child(Daughter, Mother).


I'm debating the purpose of this rule. It feels sort of incomplete on its own. It also suggests that the name "maybe initialized" could be refined -- in particular I guess it includes partial initialization? That is, this rule says that if a.b is "maybe initialized", then a is "maybe initialized". There is no corresponding rule saying (for example) that a move from a is also a move from a.b, so I have to assume that moved_out facts are the "transitive closure" over children (and that suggests to me that initialization facts should be the same).

Well, I guess the point of this "maybe partially initialized" relation is precisely to inform the region-live-at computation in NLL, which is probably already imprecise in this manner? I guess I better double check, but I remember us making some decisions like that.

Still, if the goal is to ultimately compute this relation, then why do we need the previous rule?

Well, it doesn't seem harmful -- but I guess we can either do the elaboration at the initial point -- i.e., if some path M is initialized at a point P, then we could make the initial value include that all paths which are either parents or children of M are "maybe initialized" at the point P. And then we don't need this rule to be part of the iteration -- rather, we compute this transition closure before hand.

I think this is what Lark did, but I suppose I should go back and try to write up the rules I used there. Maybe a good blog post.

I think this connects with your next comment, so I'll reply to it there.

nikomatsakis · 2019-08-28T13:13:01Z

polonius-engine/src/output/initialization.rs

+        // var_maybe_initialized_on_exit(V, P) :-
+        //     path_belongs_to_var(M, V),
+        //     path_maybe_initialized_at(M, P).
+        var_maybe_initialized_on_exit.from_leapjoin(


Something is tickling me here. If the goal ultimately is to compute which variables are maybe initialized, why do we have to extend to the parents? That is, it feels like we should track initialization precisely.

Something like this:

When you assign to a path M, that also counts as an assignment to each child path Mc (where Mc is a transitive child of M).

When you move from M, that also counts as a move from from child path Mc (as above).

If M is initialized at P, then it is initialized at each successor Q, unless Q moves from M (as above).

then compute var_maybe_init as we are doing here.

I guess the example where this differs is something like:

a.1 = foo; // initializes a.1 in my version, but also initializes a in your version drop(a.1); // moves out from a.1 only // is "a" considered maybe init here? in your version it is, in mine it isn't.

The existing NLL is somewhat approximate here, so maybe this is intentional.

Am I missing something?

I think what you are detecting is that I am computing sort of two different transitive closures. What I want to do is to trace back partial initialisation to a variable for use in the next step to determine if a drop would happen.

Probably, the cleanest design would be to compute the transitive closure over paths downwards, and separately extend the "variable-rootedness" across another transitive closure (tracing all paths back to their variable), and then finally perform the join, but I am also not sure if this is an over-approximation. The more I think about this, the less I feel like I understand it.

I am fairly certain what we did in the original fact generation was this, though: we emitted var_maybe_initialized_at whenever some sub-path of var was (maybe) initialized at that point.

nikomatsakis · 2019-09-03T19:58:06Z

Per our discussion today, we decided to land this as is

nikomatsakis · 2019-09-03T19:58:11Z

And consider any follow-ups for later

amandasystems mentioned this pull request Aug 6, 2019

Extend Polonius fact generation for (some) move tracking rust-lang/rust#62800

Merged

Albin Stjerna added 3 commits August 16, 2019 20:52

Implement calculations of var_maybe_initialzed_on_exit

da84779

This notably excludes syntax extensions for the new facts.

Remove region_live_at from everywhere

54628a3

Implement move path accesses

02f1be6

amandasystems changed the title ~~[WIP] Finalise initialisation calculations~~ Finalise initialisation calculations Aug 19, 2019

nikomatsakis reviewed Aug 28, 2019

View reviewed changes

nikomatsakis mentioned this pull request Aug 30, 2019

replace "fact" type parameters with associated types #111

Closed

Update the facts with new inputs, bump version, fix boring comments

d720ed9

amandasystems mentioned this pull request Sep 3, 2019

document init_var_maybe_initialized_on_exit #116

Closed

nikomatsakis merged commit 235745d into rust-lang:master Sep 3, 2019

amandasystems mentioned this pull request Oct 15, 2019

Move error reporting and initialisation clean-up #135

Merged

2 tasks

amandasystems mentioned this pull request Nov 12, 2019

update polonius-parser to handle facts for liveness #138

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Finalise initialisation calculations #110

Finalise initialisation calculations #110

amandasystems commented Aug 6, 2019

nikomatsakis left a comment

nikomatsakis Aug 28, 2019

amandasystems Aug 28, 2019

nikomatsakis Aug 30, 2019

amandasystems Sep 3, 2019

nikomatsakis Aug 28, 2019

amandasystems Aug 28, 2019

nikomatsakis Aug 30, 2019

amandasystems Sep 3, 2019

nikomatsakis Aug 28, 2019

nikomatsakis Aug 28, 2019

nikomatsakis Aug 28, 2019

amandasystems Aug 28, 2019

nikomatsakis Aug 28, 2019

nikomatsakis Aug 28, 2019

nikomatsakis Aug 28, 2019

nikomatsakis Aug 28, 2019

nikomatsakis Aug 28, 2019

nikomatsakis Aug 28, 2019

amandasystems Aug 28, 2019

nikomatsakis Aug 28, 2019

amandasystems Aug 28, 2019

nikomatsakis commented Sep 3, 2019

nikomatsakis commented Sep 3, 2019


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

		pub(super) fn init_var_maybe_initialized_on_exit<Region, Loan, Point, Variable, MovePath>(

Finalise initialisation calculations #110

Finalise initialisation calculations #110

Conversation

amandasystems commented Aug 6, 2019

nikomatsakis left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nikomatsakis commented Sep 3, 2019

nikomatsakis commented Sep 3, 2019