Stream: t-compiler/wg-nll

Topic: polonius-correctness-bug


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

Privately, @lqd wrote:

for the example I've been looking at, I feel like the difference between Naive and Opt is something tiny. The 2 missing borrows we'd expect to see are from the borrow_region input tuples (making them requires tuples) but are not in the region_live_atinput -- thus making the last rule borrow_live_at(B, P) :- requires(R, B, P), region_live_at(R, P) ignore them

and I'm moving it to a public thread. =)

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

specifically, the Location::All hack winds up adding outlives relationships at each point, even when some of the regions involved are not live

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

I changed this in my PR — removing Locations::All and instead equating the "inner and outer" return types at the RETURN point

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

sorry if that's vague :( it's hard to describe concisely, I have a comment somewhere tho

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

it sounds like it might repair the discrepancy, but it's an interesting meta-point: the Opt variant seems to assume a certain "WF" condition here

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

I rebased my branch and I'm doing a local build

Jake Goulding (May 30 2018 at 14:17, on Zulip):

and I'm moving it to a public thread. =)

much appreciated from us lurkers

nikomatsakis (May 30 2018 at 14:17, on Zulip):

(as it happens @Jake Goulding, this is also related to that behavior we were discussing earlier)

nikomatsakis (May 30 2018 at 14:17, on Zulip):

e.g., this branch kind of doubles down on it :)

nikomatsakis (May 30 2018 at 14:17, on Zulip):

(in polonius)

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

but you definitely convinced me I want to revisit this question and consider some alternate, less permissive variations

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

but I guess it's good to first get things working the "pure" way

nikomatsakis (May 30 2018 at 14:32, on Zulip):

@lqd which was the failing test again?

lqd (May 30 2018 at 14:33, on Zulip):

issue-31567.rs

nikomatsakis (May 30 2018 at 14:33, on Zulip):

hmm, ok. My branch doesn't fix it :)

lqd (May 30 2018 at 14:33, on Zulip):
struct VecWrapper<'a>(&'a mut S);

struct S(Box<u32>);

fn get_dangling<'a>(v: VecWrapper<'a>) -> &'a u32 {
    let s_inner: &'a S = &*v.0; //~ ERROR `*v.0` does not live long enough
    &s_inner.0
}

impl<'a> Drop for VecWrapper<'a> {
    fn drop(&mut self) {
        *self.0 = S(Box::new(0));
    }
}

fn main() {
    let mut s = S(Box::new(11));
    let vw = VecWrapper(&mut s);
    let dangling = get_dangling(vw);
    println!("{}", dangling);
}
nikomatsakis (May 30 2018 at 14:34, on Zulip):

I don't have time to dig further just now though

lqd (May 30 2018 at 14:45, on Zulip):

yeah it seems the Opt variant has slightly different requirements wrt borrow_region and region_live_at, but for this particular example were not linked to outlivesand the Location::All hack

nikomatsakis (May 30 2018 at 14:50, on Zulip):

interesting. I don't know (yet) why else those would be violated.

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

I'll try to look into which rules here make Naive produce that the regions are live at those points, and Opt is not

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

btw I added the use case where Naive and Opt differ https://github.com/rust-lang-nursery/polonius/pull/67 (time for birthday dinner :)

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

:)

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

(looking at CI this reminds me we can remove the histo crate dependency I think)

lqd (Jun 01 2018 at 16:20, on Zulip):

I feel one of the coolest advantages of this representation as facts, is how extremely easy it is to reduce mechanically, à la property-based testing. I think I have reduced one of the differences between Naive and Opt in issue 31567 to just 5 facts :)

Jake Goulding (Jun 01 2018 at 16:59, on Zulip):

à la property-based testing

I reiterate my statement from before that quickcheck or proptest would be good things to cram in and let them run for a weekend

lqd (Jun 01 2018 at 17:43, on Zulip):

yeah :)

lqd (Jun 01 2018 at 17:51, on Zulip):

@nikomatsakis would you want a PR with a #[should_panic] test for this Naive/Opt difference ?

nikomatsakis (Jun 01 2018 at 17:52, on Zulip):

sounds useful :)

lqd (Jun 01 2018 at 18:21, on Zulip):

it's a bit harder to do with the frontend right now until we've implemented def/use/liveness, since all these facts are at the same point, but it's similar in spirit to:

universal_regions {}
block B0 {
    borrow_region_at('a, L0), outlives('a: 'b), outlives('b: 'c), outlives('c: 'd), use('d); // the use here is mostly so that 'd is live for the frontend
}
lqd (Jun 01 2018 at 18:31, on Zulip):

@nikomatsakis ok so if need be all the issue-31567 facts are in PR #67, and this new reduced test is here :)

nikomatsakis (Jun 01 2018 at 18:32, on Zulip):

awesome: I don't know when I'll have time to look, but I will say that being able to do this sort of reduction was one of the primary reasons I wanted to separate borrowck out

nikomatsakis (Jun 01 2018 at 18:32, on Zulip):

so: very cool!

nikomatsakis (Jun 01 2018 at 18:33, on Zulip):

all my engineer dreams are coming true ;)

lqd (Jun 01 2018 at 18:33, on Zulip):

:)

nikomatsakis (Jun 01 2018 at 18:33, on Zulip):

except the one where this sucker is fast (/me ducks)

nikomatsakis (Jun 01 2018 at 18:33, on Zulip):

(though from my current analysis, I think there's still lots of room to make this NLL type-check go faster...)

lqd (Jun 01 2018 at 18:33, on Zulip):

at least having the test could open the possibility for other contributors to look at it

nikomatsakis (Jun 01 2018 at 18:34, on Zulip):

yep

nikomatsakis (Jun 01 2018 at 18:34, on Zulip):

it's not clear to me that it's a bug exactly, this discrepancy

nikomatsakis (Jun 01 2018 at 18:34, on Zulip):

or at least it might be a prblem on rustc side

nikomatsakis (Jun 01 2018 at 18:34, on Zulip):

I'd really like to remove Location::All

nikomatsakis (Jun 01 2018 at 18:34, on Zulip):

though I guess that doesn't fix this bug, as we said

nikomatsakis (Jun 01 2018 at 18:34, on Zulip):

I wonder if the same discrepancy is still present

lqd (Jun 01 2018 at 18:35, on Zulip):

yeah, but since it's also with the outlives, it's also confusing whether Location::All should / why it doesn't have impact here

nikomatsakis (Jun 01 2018 at 18:35, on Zulip):

it's a bit harder to do with the frontend right now until we've implemented def/use/liveness, since all these facts are at the same point, but it's similar in spirit to:

interesting; this actually does strike me as a kind of bug...

nikomatsakis (Jun 01 2018 at 18:35, on Zulip):

I'll try to look more closely

lqd (Jun 01 2018 at 18:36, on Zulip):

frontend bug ? or rustc + facts bug ?

nikomatsakis (Jun 01 2018 at 18:36, on Zulip):

er, sorry, a bug in DatafrogOpt

lqd (Jun 01 2018 at 18:36, on Zulip):

right

lqd (Jun 01 2018 at 18:36, on Zulip):

there are no cfg edges whatsoever

lqd (Jun 01 2018 at 18:37, on Zulip):

and we're trying to limit the TC to regions that are live-to-dead along edges _huge shortcuts in this sentence cough_

lqd (Jun 01 2018 at 20:52, on Zulip):

The other missing loan from the same issue has basically the same structure, except the last of the 3 outlives is at a different point (but the cfg_edges are not significant for this specific missing loan either). I'll try and look at the other -Zpolonius issues next

lqd (Jun 04 2018 at 22:38, on Zulip):

omg I finally got through all the -Zpolonius failures Santiago posted before. I focused on finding the ones failing because of the Naive vs Opt differences, and found 11 of the 50+ failing tests. I reduced those to a smaller number (<5) of vaguely distinct patterns, but it feels like it's only a couple of unique patterns — but since a few seemed very related to the TC at a single point, it's possible it's actually a single bug. (since it hasn't been merged yet I'll repurpose PR #69 to add this small number of patterns, instead of just the one issue)

lqd (Jun 05 2018 at 11:26, on Zulip):

ok I think it really is one single bug: there are 4 unique-ish patterns, with 3 of those being a longer chain of outlives at the same point, and the 4th still having the same scheme but over 2 points instead of one

lqd (Jun 05 2018 at 11:30, on Zulip):

reduced, it looks a bit like this, whenever a region is live at a single point, Opt misses the region(s) it outlives (recursively)

universal_regions {}
block B0 {
    borrow_region_at('a, L0), outlives('a: 'b), use('b); // region_live_at('b)
}
lqd (Jun 05 2018 at 11:32, on Zulip):

and in rustc's tests, there are multiple variations of this, either differing on the length of the outlives chain, or whether it happens at the same point or the next

lqd (Jun 05 2018 at 11:40, on Zulip):

so I'll encode all this as 4 tests, but they are likely to be fixed at the same time

lqd (Jun 05 2018 at 12:27, on Zulip):

@nikomatsakis I've updated https://github.com/rust-lang-nursery/polonius/pull/69 could you validate my comments in the tests are clear enough for you ?

nikomatsakis (Jun 05 2018 at 12:28, on Zulip):

yep

nikomatsakis (Jun 05 2018 at 12:28, on Zulip):

thanks for doing this btw

nikomatsakis (Jun 05 2018 at 12:28, on Zulip):

comment is excellent

nikomatsakis (Jun 05 2018 at 12:29, on Zulip):

I was wondering — why can't we use the 'parser front-end for this'? in particular, does it not support kind of "Explicit form of every fact"?

nikomatsakis (Jun 05 2018 at 12:29, on Zulip):

maybe we should make that a goal :)

lqd (Jun 05 2018 at 12:29, on Zulip):

agreed

lqd (Jun 05 2018 at 12:29, on Zulip):

while the 4th test could work I think

lqd (Jun 05 2018 at 12:29, on Zulip):

the other 3 are at the same point, and so not exactly realistic wrt to the format

lqd (Jun 05 2018 at 12:30, on Zulip):

it could work with "blabla /"

nikomatsakis (Jun 05 2018 at 12:30, on Zulip):

why does being at the same point make it unrealistic?

lqd (Jun 05 2018 at 12:31, on Zulip):

just towards the format, eg I felt we mostly wanted to use the mid point

lqd (Jun 05 2018 at 12:32, on Zulip):

and here we'd have to use the start point

lqd (Jun 05 2018 at 12:34, on Zulip):

but yes I agree the frontend is made exactly for these cases :) I also initially was about to ask if you wanted to try to use it before merging those tests, instead of the facts as-is

nikomatsakis (Jun 05 2018 at 12:35, on Zulip):

question: can you readily dump out the values of the various sets for the send_is_not_static_std_sync test?

nikomatsakis (Jun 05 2018 at 12:35, on Zulip):

I'd be curious to see

lqd (Jun 05 2018 at 12:35, on Zulip):

sure, I'll push them

lqd (Jun 05 2018 at 12:37, on Zulip):

(I also have an ugly function doing the reduction work)

lqd (Jun 05 2018 at 12:40, on Zulip):

@nikomatsakis https://github.com/lqd/borrow-check/commit/914889f98afb44d3bf18c479a2939b15bda4a7ea

lqd (Jun 05 2018 at 12:40, on Zulip):

mutex and rwlock are the failing functions and are reduced in the tests

lqd (Jun 05 2018 at 13:17, on Zulip):

I was wondering — why can't we use the 'parser front-end for this'? in particular, does it not support kind of "Explicit form of every fact"?

yes, this, we can't emit region_live_at manually right now (we kinda talked about it only as byproducts of use and liveness IIRC) but I can add it, we would want to avoid writing region_live_at as they are tedious, but for these exact cases it would have been useful :)

lqd (Jun 05 2018 at 14:02, on Zulip):

@nikomatsakis for these tests, would you rather have the "exactly minimal facts" which were automatically reduced, or something that can be a slight superset but using the frontend ? (since the frontend is focused on statements rather than points, there could be two points and an edge being generated, when sometimes no edges are actually needed to trigger the bug)

lqd (Jun 05 2018 at 21:17, on Zulip):

alright I've added region_live_at to the frontend, and converted the minimal reduced tests to the less-minimal frontend format :) (PR by tomorrow, although I'm not sure whether this would need bumping the polonius-parser or polonius version)

nikomatsakis (Sep 27 2018 at 21:02, on Zulip):

revising this topic, maybe this had the bug?

nikomatsakis (Sep 27 2018 at 21:04, on Zulip):

dang Zulip search is good btw

nikomatsakis (Sep 27 2018 at 21:05, on Zulip):

I have literally never failed to find the thing I was looking for thus far

lqd (Sep 27 2018 at 21:08, on Zulip):

:D (yeah it was this topic)

nikomatsakis (Sep 27 2018 at 21:13, on Zulip):

hmm ok so the test:

        universal_regions { }
        block B0 {
            borrow_region_at('a, L0),
            outlives('a: 'b),
            outlives('b: 'c),
            outlives('c: 'd),
            region_live_at('d);
        }
nikomatsakis (Sep 27 2018 at 21:14, on Zulip):

so ... I think that the problem is that the optimized version assumes that there are two live endpoints

nikomatsakis (Sep 27 2018 at 21:14, on Zulip):

but here there is only one

nikomatsakis (Sep 27 2018 at 21:14, on Zulip):

I am tempted to say that this is an invalid input that we should fix

nikomatsakis (Sep 27 2018 at 21:15, on Zulip):

in particular, I think that one could say that the borrow region is always live at the point where it is introduced

nikomatsakis (Sep 27 2018 at 21:15, on Zulip):

however

nikomatsakis (Sep 27 2018 at 21:15, on Zulip):

let me look at the code a bit to refresh my memory

nikomatsakis (Sep 27 2018 at 21:15, on Zulip):

e.g. this input passes

        universal_regions { }
        block B0 {
            borrow_region_at('a, L0),
            region_live_at('a),
            outlives('a: 'b),
            outlives('b: 'c),
            outlives('c: 'd),
            region_live_at('d);
        }
lqd (Sep 27 2018 at 21:24, on Zulip):

this would be nice, and we could quickly prototype such a fix in the same way we add all points to universal_regions

nikomatsakis (Sep 27 2018 at 21:25, on Zulip):

otoh I remember wanting it to be the case that

nikomatsakis (Sep 27 2018 at 21:25, on Zulip):

you could talk about various regions in the "mid-point" of things

nikomatsakis (Sep 27 2018 at 21:25, on Zulip):

that are never used outside

nikomatsakis (Sep 27 2018 at 21:25, on Zulip):

and only serve to make connections

nikomatsakis (Sep 27 2018 at 21:25, on Zulip):

but this is still true, I suppose

nikomatsakis (Sep 27 2018 at 21:25, on Zulip):

in particular, when you e.g. invoke a fn

nikomatsakis (Sep 27 2018 at 21:26, on Zulip):

that instantiates some higher-ranked regions at the point of call

nikomatsakis (Sep 27 2018 at 21:26, on Zulip):

and those don't appear in any MIR types, they only exist at the "mid point"

nikomatsakis (Sep 27 2018 at 21:26, on Zulip):

but they make connections between the arguments and the return type of the fn

nikomatsakis (Sep 27 2018 at 21:26, on Zulip):

e.g., for<'a> fn(&'a str) -> &'a str

nikomatsakis (Sep 27 2018 at 21:26, on Zulip):

the region that represents 'a for any particular call

nikomatsakis (Sep 27 2018 at 21:26, on Zulip):

so this still preserves the "both end-points are live on entry to the mid point" property

nikomatsakis (Sep 27 2018 at 21:30, on Zulip):

I am trying to bring the "opt code" back into cache now to decide how hard it would be to match behavior though :)

nikomatsakis (Sep 27 2018 at 21:31, on Zulip):

but I'm not sure if it's worth it, feels to me like the borrow region should be live at the (mid-point) of borrow

nikomatsakis (Sep 27 2018 at 21:31, on Zulip):

which I think is the bug here

lqd (Sep 27 2018 at 21:31, on Zulip):

very interesting cases tho, even if they don't appear quite often in the test suite

nikomatsakis (Sep 27 2018 at 21:36, on Zulip):

that's what I'm wondering

nikomatsakis (Sep 27 2018 at 21:36, on Zulip):

why only this test case?

nikomatsakis (Sep 27 2018 at 21:36, on Zulip):

I have to look at the rust test too

lqd (Sep 27 2018 at 21:37, on Zulip):

it's more let's say 10 rustc tests

lqd (Sep 27 2018 at 21:37, on Zulip):

but one pattern, only the length of the outlives chain changing (maybe 2 patterns, at most, but if memory serves, it only looked like there was one)

lqd (Sep 27 2018 at 21:39, on Zulip):

(IIRC I've mentioned in the polonius tests, the rustc tests where we saw these lengths of chains)

nikomatsakis (Sep 27 2018 at 21:40, on Zulip):

hmm

lqd (Sep 28 2018 at 12:00, on Zulip):

I might be Doin It Wrong™ but I tried the quick hack we mentioned yesterday, to declare that each borrow region is always live at the point where it is introduced: it seems to fix the failing tests focusing on the opt/naive difference, but will also make other tests fail (eg our key loop feature of issue-47680)

nikomatsakis (Sep 28 2018 at 15:05, on Zulip):

interesting

nikomatsakis (Sep 28 2018 at 15:06, on Zulip):

I don't have it quite "in cache enough" just yet

lqd (Sep 28 2018 at 15:09, on Zulip):

there's no rush

Last update: Nov 21 2019 at 13:10UTC