Stream: t-compiler/wg-nll

Topic: soundness-etc


nikomatsakis (May 23 2018 at 19:28, on Zulip):

@pnkfelix in light of the strategy of "focus on existing impl", we should probably review the soundness and other bugs and make sure they are getting fixed. For example, https://github.com/rust-lang/rust/issues/49354, https://github.com/rust-lang/rust/issues/50716, and https://github.com/rust-lang/rust/issues/47184 ...

nikomatsakis (May 23 2018 at 19:28, on Zulip):

cc @Matthew Jasper you around and interested in taking any of those on?

nikomatsakis (May 23 2018 at 19:28, on Zulip):

I thought there was one about implied bounds and NLL but can't find it now

Matthew Jasper (May 23 2018 at 19:48, on Zulip):

I'm around, I've just been busy enough that trivial bounds was taking up all of the time I had for Rust.

Matthew Jasper (May 23 2018 at 19:50, on Zulip):

Of those three, #49354 looks like the one I would be most interested in.

Matthew Jasper (May 23 2018 at 19:52, on Zulip):

That said I was looking at improving some of the move errors before then, but I'm not that happy with the approach I had for that so there isn't much that would be lost.

nikomatsakis (May 23 2018 at 19:52, on Zulip):

sounds interesting indeed

pnkfelix (May 25 2018 at 12:38, on Zulip):

Seems like rust-lang/rust#47184 was fixed sometime between 1st Jan and 30th March!

pnkfelix (May 25 2018 at 12:39, on Zulip):

with a period in middle (observed from 15th Feb rustc) where we ICE'd with a related error: "unexpected region for local data ReStatic"

pnkfelix (May 25 2018 at 12:40, on Zulip):

I'll go ahead and at least bisect to the particular nightlies where each change occurred, to gain confidence that the bug is actually fixed.

pnkfelix (May 25 2018 at 14:02, on Zulip):

oh, whoops: I was using links as my browser and didn't see the full comment thread, so I didn't realize that this was known (namely rust-lang/rust#48482)

nikomatsakis (May 25 2018 at 14:05, on Zulip):

I'm thinking that I will focus on finishing off that issue next

nikomatsakis (May 25 2018 at 14:05, on Zulip):

seems like something we must fix and it's a major architectural unknown

nikomatsakis (May 25 2018 at 14:05, on Zulip):

well, it doesn't have to be me

nikomatsakis (May 25 2018 at 14:05, on Zulip):

but somebody should :)

nikomatsakis (May 25 2018 at 14:05, on Zulip):

although maybe not a blocker for issuing warnings...?

Jake Goulding (May 25 2018 at 14:18, on Zulip):

I was using links as my browser

People like you do exist...

pnkfelix (May 25 2018 at 14:20, on Zulip):

I was using links as my browser

People like you do exist...

(I had forgotten my AC adapter and so I was in emergency-mode trying to make my laptop as dumb as possible, moving all of my tasks to remote ssh sessions)

pnkfelix (May 25 2018 at 14:21, on Zulip):

I'm looking at the issue now, going over your conversation(s) with @David Wood

pnkfelix (May 25 2018 at 14:21, on Zulip):

@nikomatsakis ^

pnkfelix (May 25 2018 at 14:22, on Zulip):

I did want to ask: You (niko) had said you don't want to deal with trying to deconstruct let (a, b): (T, U);

pnkfelix (May 25 2018 at 14:22, on Zulip):

that leads me to ask: What is the alternative you are thinking of? We certainly should not build up a fake value of type (T, U) from the local variables a/b

pnkfelix (May 28 2018 at 10:21, on Zulip):

Follow-up on this topic: I may have managed to implement deconstruction of let (a, b): (T, U);,

nikomatsakis (May 28 2018 at 10:28, on Zulip):

@pnkfelix I'm not sure I had a complete alternative in mind. I suppose deconstruction is the most straightforward sol'n in that case. We will have to handle other cases (e.g., foo::<...>(...)), and I suppose I thought maybe solving those other cases would help us here?

pnkfelix (May 28 2018 at 11:13, on Zulip):

@nikomatsakis before I move too much further on this, I have a question about the rustc::infer::canonical::Canonical type

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

ok

pnkfelix (May 28 2018 at 11:14, on Zulip):

We have struct Canonical<V> { variables: CanonicalVarInfos, value: V }

nikomatsakis (May 28 2018 at 11:14, on Zulip):

(ask away, but also there is a chapter of the rustc-guide covering canonicalization, though it focuses on the role it plays in trait selection)

pnkfelix (May 28 2018 at 11:14, on Zulip):

it says that the free inference variables have been number starting from 0 in order of first appearance

pnkfelix (May 28 2018 at 11:15, on Zulip):

so my question is

pnkfelix (May 28 2018 at 11:16, on Zulip):

in my code to deconstruct a pattern like (a, b), and in parallel deconstruct the type (T, U)

pnkfelix (May 28 2018 at 11:16, on Zulip):

when I actually hit the base case of a binding, the API for mir::UserAssertTy requires a CanonicalTy

pnkfelix (May 28 2018 at 11:16, on Zulip):

so I need to conjure up a CanonicalVarInfos to plus in for the variables field of Canonical

nikomatsakis (May 28 2018 at 11:17, on Zulip):

(one thing you could do would be to instantiate the variables in the infer ctxt and then recanonicalize)

pnkfelix (May 28 2018 at 11:17, on Zulip):

Is the struct of the Canonical type something where the correspondence between the CanonicalVarInfos is based on the implicit order of the free variables

pnkfelix (May 28 2018 at 11:17, on Zulip):

i.e. as I unzip a type's structure, conceptually I may have to also peel off CanonicalVarInfos ?

nikomatsakis (May 28 2018 at 11:18, on Zulip):

yeah, I would not personally take that approach, it's too delicate

pnkfelix (May 28 2018 at 11:18, on Zulip):

Or can I just clone the original CanonicalVarInfos from the original large type

nikomatsakis (May 28 2018 at 11:18, on Zulip):

you could do that, just skip renumbering, though then the resulting type is not truly canonical

pnkfelix (May 28 2018 at 11:18, on Zulip):

ah I see

pnkfelix (May 28 2018 at 11:18, on Zulip):

so the infos should match up

pnkfelix (May 28 2018 at 11:19, on Zulip):

but it won't be canonicalized

pnkfelix (May 28 2018 at 11:19, on Zulip):

hmm

nikomatsakis (May 28 2018 at 11:19, on Zulip):

e.g., if you had (&'_ u32, &'_ i32), you would wind up with (for the RHS) forall<'0, '1> &'1 i32, which is not truly canonical (where the forall refers to the "info" array)

nikomatsakis (May 28 2018 at 11:19, on Zulip):

this probably doesn't matter here

nikomatsakis (May 28 2018 at 11:19, on Zulip):

but it's generally a violation of the Canonical<..> contract

nikomatsakis (May 28 2018 at 11:19, on Zulip):

e.g., for caching

pnkfelix (May 28 2018 at 11:20, on Zulip):

it might be simplest to recanonicalize

pnkfelix (May 28 2018 at 11:21, on Zulip):

either by instatiating in the infer ctxt, as you mentioned... or perhaps by adding some new code that can take the old CanonicalVarInfos and the unzipped type(s) and then do the renumbering (and throwing out of unused var infos...)

nikomatsakis (May 28 2018 at 11:23, on Zulip):

@pnkfelix personally I'd say not worth writing the new code, but yes conceptually it's possible. Rather than doing that optimization, though, I'd prefer to do https://github.com/rust-lang/rust/issues/48417

nikomatsakis (May 28 2018 at 11:24, on Zulip):

actually, @Vytautas Astrauskas, it'd be sort of something completely different, but maybe you are interested in https://github.com/rust-lang/rust/issues/48417 ? :) would be a nice refactoring

nikomatsakis (May 28 2018 at 11:24, on Zulip):

I'd have to explain what I had in mind

nikomatsakis (May 28 2018 at 11:25, on Zulip):

(it's more in the area of traits)

Vytautas Astrauskas (May 28 2018 at 11:25, on Zulip):

Reading.

Jaime Valdemoros (May 28 2018 at 11:25, on Zulip):

If it involved refactoring I'd be keen to get involved (I'm working in the same group as @Vytautas Astrauskas )

nikomatsakis (May 28 2018 at 11:26, on Zulip):

( though possibly also relevant here — if I'm correct, it could be a general overall speedup )

nikomatsakis (May 28 2018 at 11:26, on Zulip):

I'll also leave a few notes on #50716

pnkfelix (May 28 2018 at 14:46, on Zulip):

@nikomatsakis another Q on rust-lang/rust#47184 : is it actually possible to check things like foo::<'static>() via injecting UserAssertTy ? We cannot feed the 'static as an argument to that statement. I guess we could try to instantiate the generics of the fn signature, plugging in the 'static for its lifetime parameter...

nikomatsakis (May 28 2018 at 14:48, on Zulip):

it is not possible I don't think, I think we need a distinct mechanism

nikomatsakis (May 28 2018 at 14:48, on Zulip):

I'm not 100% sure what I think that mechanism should be

nikomatsakis (May 28 2018 at 14:48, on Zulip):

I had planned to look at the astconv code and see if we could modify it

nikomatsakis (May 28 2018 at 14:48, on Zulip):

so that we capture each time we convert a type from HIR

nikomatsakis (May 28 2018 at 14:48, on Zulip):

and somehow store that result for later reference

nikomatsakis (May 28 2018 at 14:49, on Zulip):

idk, this is a bit tricky. @eddyb and I were talking about it too, he has opinions :)

pnkfelix (May 28 2018 at 14:50, on Zulip):

Is your thinking in part that we may do away with UserAssertTy if we were to add this other mechanism to which you allude?

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

yeah, that's a question mark

Julien Cretin (ia0) (May 29 2018 at 22:24, on Zulip):

When we talk about soundness, do we talk about a proof of soundness (proof of algorithm, not proof of implementation) or about fixing known soundness bugs?
Also, do we talk about the soundness of the existing MIR-borrowck or the upcoming polonius version? Reading the weekly meeting of May 29th, I'm assuming we talk about the existing MIR-borrowck.

pnkfelix (May 29 2018 at 22:28, on Zulip):

The tag NLL-sound is typically used for cases where MIR-borrowck is accepting code it should reject; which usually means that it is accepting code that is unsound.

pnkfelix (May 29 2018 at 22:29, on Zulip):

This particular wg-nll topic, "soundness-etc", may or may not be so focused

Julien Cretin (ia0) (May 29 2018 at 22:29, on Zulip):

Ok, thanks! So it's about fixing known issues in MIR-borrowck.

Julien Cretin (ia0) (May 29 2018 at 22:29, on Zulip):

Ah ok :-)

pnkfelix (May 29 2018 at 22:29, on Zulip):

Ok, thanks! So it's about fixing known issues in MIR-borrowck.

yes

pnkfelix (May 29 2018 at 22:30, on Zulip):

however, if someone wants to try to come up with a soundness proof

pnkfelix (May 29 2018 at 22:30, on Zulip):

they certainly are welcome to do so. Though it may be good to talk to the Rust Belt folks like Ralf Jung about their work in this space

pnkfelix (May 29 2018 at 22:31, on Zulip):

Rust Belt folks: https://plv.mpi-sws.org/rustbelt/

Julien Cretin (ia0) (May 29 2018 at 22:31, on Zulip):

Yes definitely, since they have the only formal description of a subset of the language that I know.

Last update: Nov 21 2019 at 13:30UTC