Stream: t-compiler/wg-polonius

Topic: move errors


Albin Stjerna (Nov 05 2019 at 14:59, on Zulip):

I have a question. If we have a move error at some MIR statement x, should it happen at Start(x)or Mid(x)? Both make sense to me, if the evaluation happens before the effect (which is the only way I see there being any point to separating start/mid).

Matthew Jasper (Nov 05 2019 at 16:20, on Zulip):

Invalidates error are at the start point, so I would expect move errors to also be at the start point.

Albin Stjerna (Nov 05 2019 at 17:43, on Zulip):

Great thanks :)

lqd (Mar 08 2020 at 21:59, on Zulip):

@Albin Stjerna I've tried to trace the move errors a bit just to see if something obvious jumps at you, there's a false positive in the dataset issue-47680 (it's small-ish, especially compared to clap :) it finds an unexpected move error: "Start(bb8[1])" "mp11" which seems to come all the way up via path_maybe_uninitialized_on_exit (from possibly the beginning of the whole phase 2)

lqd (Mar 08 2020 at 22:00, on Zulip):

here's a trace of the tuples created during both phases of initialization
and the error itself appears in round 41 of phase 2:

 `move_error(Path { index: 2 }, Point { index: 46 })` tuple created, from leapjoining `path_maybe_uninitialized_on_exit(Path { index: 2 }, Point { index: 45 })` with value `Point { index: 46 }`
Albin Stjerna (Mar 09 2020 at 12:19, on Zulip):

Is the path a variable or a function argument?

lqd (Mar 09 2020 at 12:58, on Zulip):

I don't know, it looks like a variable in the code, but mp11 doesn't doesn't appear in https://github.com/rust-lang/polonius/blob/master/inputs/issue-47680/nll-facts/main/path_is_var.facts -- then again I know nothing about these facts and rules

Albin Stjerna (Mar 10 2020 at 19:40, on Zulip):

The relation between move paths and variables is slightly byzantine

Albin Stjerna (Mar 10 2020 at 19:41, on Zulip):

apparently, there's a hierarchy: mp5.mp10.mp11

Albin Stjerna (Mar 10 2020 at 19:41, on Zulip):

And mp5 is _5

Albin Stjerna (Mar 10 2020 at 19:43, on Zulip):

Ok, so it's a regular variable, moved at start, and assigned at Start(bb4[0]), which should also initialise all its children

Albin Stjerna (Mar 10 2020 at 19:44, on Zulip):

This looks a lot like an off-by-one

Albin Stjerna (Mar 10 2020 at 19:44, on Zulip):

Because at Mid(bb8[1]), mp11 is moved

Albin Stjerna (Mar 10 2020 at 19:46, on Zulip):

And the error happens at Start(bb8[1])

Albin Stjerna (Mar 10 2020 at 19:46, on Zulip):

I guess it's caused by the join with the accessed-by relationship, presumably caused by a move expression at bb8[1]

Albin Stjerna (Mar 10 2020 at 19:47, on Zulip):

I was so sure I fixed the problems with overlaps in move statements

Albin Stjerna (Mar 10 2020 at 19:53, on Zulip):

It might also be related to propagation from path transitivity in path_maybe_uninitialized_on_exit, I'll have to check the rules

lqd (Mar 10 2020 at 20:05, on Zulip):

I was wondering whether you expected conditional_init to emit 2 move errors btw ?

Albin Stjerna (Mar 10 2020 at 20:13, on Zulip):

What is conditional_init?

lqd (Mar 10 2020 at 20:18, on Zulip):

one of the move errors test you added

lqd (Mar 10 2020 at 20:18, on Zulip):

in the smoke-test dataset

lqd (Mar 10 2020 at 20:19, on Zulip):

here https://github.com/rust-lang/polonius/blob/master/inputs/smoke-test/polonius-smoke-test.rs#L73-L78

Albin Stjerna (Mar 10 2020 at 20:19, on Zulip):

...

Albin Stjerna (Mar 10 2020 at 20:20, on Zulip):

I guess it should emit one?

lqd (Mar 10 2020 at 20:20, on Zulip):

I'm not really sure how the facts map back to rustc errors

Albin Stjerna (Mar 10 2020 at 20:20, on Zulip):

on line 76, it should say that a may not be initialized

Albin Stjerna (Mar 10 2020 at 20:21, on Zulip):

I'm not sure either

lqd (Mar 10 2020 at 20:21, on Zulip):

but maybe one of those 2 is the same off by one as earlier

Albin Stjerna (Mar 10 2020 at 20:21, on Zulip):

That sounds likely

lqd (Mar 10 2020 at 20:21, on Zulip):

I don't have the MIR handy but those 2 errors are a bit apart from each other so it seemed likely

lqd (Mar 10 2020 at 20:22, on Zulip):

I saw that while encoding it into a unit test https://github.com/rust-lang/polonius/pull/144/commits/a1e97641a09901aea761ffdec744517fa227bc99#diff-c5fc4beef0f03493c2e9a9c876073f0fR716-R741

lqd (Mar 10 2020 at 20:22, on Zulip):

but it may be encoding another false positive at the same time

lqd (Mar 10 2020 at 20:24, on Zulip):

if it is indeed the off by one, at least this function is super simple

lqd (Mar 10 2020 at 20:24, on Zulip):

which should make analysis easier than the earlier one

lqd (Mar 18 2020 at 19:41, on Zulip):

I have a lead on the false positive error from the conditional_init dataset (the earliest of the two errors: Start(bb2[0]), mp3). _3 is interesting because it's a call's return place.

MIR excerpt

The terminator we're looking at is from the _3 = random() call leading to bb2 and rustc generates a fact saying _3 will be initialized on the non-panic path, at the start location of the successor block (Start(bb2[0]), where our error happens).

The rule for move errors is:

move_error(Path, TargetNode) :-
   path_maybe_uninitialized_on_exit(Path, SourceNode),
   cfg_edge(SourceNode, TargetNode),
   path_accessed_at(Path, TargetNode).

so here SourceNode = Mid(bb0[3]), TargetNode = Start(bb2[0]) and there must be a path_access_at the target node. This path access fact at the start node is generated here which I assume because of some uses here.

The rules seem designed specifically to compute a move error on an edge rather than at a point, so I'm not sure whether this path access should have been at the mid point, or if it's the other way around and the rule should look at uninitialized accesses at single points ?
I'll try and emit the fact at the mid point and see if anything breaks.

lqd (Mar 18 2020 at 19:57, on Zulip):

I'll try and emit the fact at the mid point and see if anything breaks.

answer: a lot of things break, this start point is load-bearing

lqd (Mar 18 2020 at 20:00, on Zulip):

maybe this will help you @Albin Stjerna, or maybe you and niko already talked about this

lqd (Mar 18 2020 at 21:17, on Zulip):

or maybe move errors could be ignoring these cases, by allowing access + assignment at the target node ?

move_error(Path, TargetNode) :-
   path_maybe_uninitialized_on_exit(Path, SourceNode),
   cfg_edge(SourceNode, TargetNode),
   path_accessed_at(Path, TargetNode),
   !path_assigned_at(path, TargetNode).
lqd (Mar 18 2020 at 21:20, on Zulip):

(but wouldn't fix some of the other false positives I've seen, so hard to say)

lqd (Mar 18 2020 at 22:31, on Zulip):

(and I think the false positives in clap have the same shape as this one in conditional_init)

lqd (Mar 18 2020 at 22:32, on Zulip):

while some of the other false positives like in issue-47680 were caused by a small typo

lqd (Mar 18 2020 at 22:44, on Zulip):

(I'll re-check the previous path access fact start/mid location tests with the typo fixed)

lqd (Mar 18 2020 at 23:31, on Zulip):

muuuuuch better, yay, and it also fixes the 3 maybe-drop-* tests changes: they go back to their prior behavior and we don't have 2 unexpected passes / 1 unexpected fail

Albin Stjerna (Mar 19 2020 at 08:17, on Zulip):

Yay! Nice job!

lqd (Mar 19 2020 at 08:47, on Zulip):

@Albin Stjerna do you maybe remember a reason why these accesses were initially at the start point while other uses were at the mid point ? if not, it's probably ok to move it there as well :)

lqd (Mar 19 2020 at 08:52, on Zulip):

it doesn't seem to impact the var_maybe_partly_initialized_on_exit part of move/init which impacts liveness and loan analysis so that's that. I guess we'll know more when we finally emit the move errors :clown:

Albin Stjerna (Mar 19 2020 at 09:12, on Zulip):

Err

Albin Stjerna (Mar 19 2020 at 09:12, on Zulip):

I have a memory

Albin Stjerna (Mar 19 2020 at 09:13, on Zulip):

But I think they should happen at mid-point

lqd (Mar 19 2020 at 09:14, on Zulip):

seems sensible to me as well

lqd (Mar 19 2020 at 09:14, on Zulip):

I'll take care of it

lqd (Mar 19 2020 at 09:15, on Zulip):

the sweet dance of updating the 2 repos in lockstep :)

Albin Stjerna (Mar 19 2020 at 10:15, on Zulip):

I'm so happy this wasn't some big thing (probably)

lqd (Mar 19 2020 at 10:18, on Zulip):

more and more I think we'll have to compute them differently, it's not datafrog's strong suit

lqd (Mar 19 2020 at 10:19, on Zulip):

but let's get them correct first and then we can refactor all we want

lqd (Mar 19 2020 at 10:19, on Zulip):

in the mean time it'll just be tough to work on anything downstream from move errors

lqd (Mar 19 2020 at 10:20, on Zulip):

(on the big datasets)

lqd (Mar 19 2020 at 10:22, on Zulip):

but yeah, same, good news :)

lqd (Mar 20 2020 at 15:35, on Zulip):

@Albin Stjerna I've updated https://github.com/rust-lang/polonius/pull/144 to fix the subpaths false positives

lqd (Mar 20 2020 at 15:36, on Zulip):

one PR down, two to go

lqd (Mar 20 2020 at 15:37, on Zulip):

(maybe three, if we count the one to update the version and publish the release needed for the two other PRs)

lqd (Mar 20 2020 at 15:38, on Zulip):

should be rather straightforward to review if you ignore the fact updates commits :)

lqd (Mar 20 2020 at 15:51, on Zulip):

maybe I'll just bump polonius-engine to 0.12.1 in this PR

Albin Stjerna (Mar 20 2020 at 15:59, on Zulip):

Excellent, I'll have a look at it during the weekend!

lqd (Mar 20 2020 at 16:00, on Zulip):

sweet, thank you; I'll get to work on the rustc and fact updates ones then

lqd (Mar 20 2020 at 17:19, on Zulip):

(I also added a few low hanging fruit commits for some move/init cleanups)

Albin Stjerna (Mar 22 2020 at 16:31, on Zulip):

@lqd I think it looks great; I love how reviewing this teaches me how to write better code as well

Albin Stjerna (Mar 22 2020 at 16:37, on Zulip):

Merged it!

Albin Stjerna (Mar 22 2020 at 16:38, on Zulip):

(I just assumed I could)

lqd (Mar 22 2020 at 21:28, on Zulip):

thanks a bunch

lqd (Mar 30 2020 at 00:43, on Zulip):

0.12.1 published, rustc PR to fix the remaining (I hope) move errors false positives + UI test expectations https://github.com/rust-lang/rust/pull/70546

lqd (Mar 30 2020 at 00:43, on Zulip):

when it lands I'll update the polonius repo facts again

lqd (Mar 30 2020 at 01:09, on Zulip):

(but this should all go away if we go with the previous plan I mentioned to fix the OOMs, all those are materialization of the Locations::All subsets)

lqd (Mar 30 2020 at 19:19, on Zulip):

turns out it landed very quickly, so here's the updated facts PR https://github.com/rust-lang/polonius/pull/147, and we should be good on move errors until we actually emit them in rustc

Last update: Apr 03 2020 at 17:40UTC