Stream: t-compiler/wg-nll

Topic: polonius-consumers


Vytautas Astrauskas (May 28 2018 at 20:35, on Zulip):

@nikomatsakis Have you decided what you would like to do with Polonius naïve implementation? I am asking because for our Viper verifier it would be much easier to consume the output of a less optimized version.

Vytautas Astrauskas (May 28 2018 at 20:39, on Zulip):

On the other hand, if we tried to consume the optimized version, we would need to come up with its (at least informal) soundness proof, which, probably, would be quite useful…

Vytautas Astrauskas (May 28 2018 at 20:43, on Zulip):

JFYI: in both cases, we would need access to subset and borrow_live_at facts.

nikomatsakis (May 28 2018 at 21:08, on Zulip):

@nikomatsakis Have you decided what you would like to do with Polonius naïve implementation? I am asking because for our Viper verifier it would be much easier to consume the output of a less optimized version.

I intend to keep the naive version around permanently as the "canonical" rules — then the optimizer would be intendd to be equal, and any discrepancy is likely a bug

nikomatsakis (May 28 2018 at 21:09, on Zulip):

I'm not sure if that fulfills your requirements or not =)

Jake Goulding (May 28 2018 at 21:13, on Zulip):

I intend to keep the naive version around permanently as the "canonical" rules — then the optimizer would be intendd to be equal, and any discrepancy is likely a bug

Then just hook up quickcheck to test that arbitrary inputs are always equal...

nikomatsakis (May 28 2018 at 21:15, on Zulip):

@Jake Goulding I had that in mind too...

nikomatsakis (May 28 2018 at 21:15, on Zulip):

though I'm not sure how good quicktest would be at finding discrepancies

nikomatsakis (May 28 2018 at 21:15, on Zulip):

maybe

Vytautas Astrauskas (May 29 2018 at 07:51, on Zulip):

I'm not sure if that fulfills your requirements or not =)

Yes, this sounds good. We just need a way to invoke Polonius naïve and obtain computed facts. Would it be acceptable for you to have a query that allows obtaining AllFacts and have a Polonius to expose a function that accepts AllFacts and returns subset with loan_live_at?

Vytautas Astrauskas (May 29 2018 at 08:04, on Zulip):

I intend to keep the naive version around permanently as the "canonical" rules — then the optimizer would be intendd to be equal, and any discrepancy is likely a bug

So, for this, we need to extend the test compare mode to support comparing the optimized Polonius algorithm with the naïve one, right?

Vytautas Astrauskas (May 29 2018 at 08:06, on Zulip):

@Santiago Pastorino Is this something you are already working on? I think that implementing this would be a nice opportunity for me to get familiar with the integration code. :relaxed:

nikomatsakis (May 29 2018 at 08:15, on Zulip):

@Vytautas Astrauskas well, @Santiago Pastorino and I had been discussing the idea of having a way to select the algorithm that rustc uses as an extension to https://github.com/rust-lang/rust/pull/51133; maybe we could add that, and then add an algorithm to polonius that compares naive-to-opt

Vytautas Astrauskas (May 29 2018 at 08:17, on Zulip):

though I'm not sure how good quicktest would be at finding discrepancies

I think we could try to adapt something like this.

nikomatsakis (May 29 2018 at 08:17, on Zulip):

yes

nikomatsakis (May 29 2018 at 08:18, on Zulip):

if things get more advanced, we could also contact them

Vytautas Astrauskas (May 29 2018 at 08:20, on Zulip):

@nikomatsakis

@Vytautas Astrauskas well, @Santiago Pastorino and I had been discussing the idea of having a way to select the algorithm that rustc uses as an extension to https://github.com/rust-lang/rust/pull/51133; maybe we could add that, and then add an algorithm to polonius that compares naive-to-opt

Sounds good. Please let me know if I could help to implement this.

Vytautas Astrauskas (May 29 2018 at 08:25, on Zulip):

if things get more advanced, we could also contact them

JFYI: Zhendong Su is moving to ETH.

Santiago Pastorino (May 29 2018 at 13:29, on Zulip):

hey @Vytautas Astrauskas I've done the basics of this, happy to share with you and letting you continue with the rest if you want

Vytautas Astrauskas (May 29 2018 at 13:35, on Zulip):

@Santiago Pastorino Could you specify more precisely what you mean by this?

Vytautas Astrauskas (May 29 2018 at 13:37, on Zulip):

Do you mean changes on the Rustc side to enable comparing Polonius with NLL?

Santiago Pastorino (May 29 2018 at 13:41, on Zulip):

I was talking about this PR https://github.com/rust-lang/rust/pull/51138

Santiago Pastorino (May 29 2018 at 13:41, on Zulip):

consider the last 3 commits

Santiago Pastorino (May 29 2018 at 13:41, on Zulip):

because it's on top of https://github.com/rust-lang/rust/pull/51133

Santiago Pastorino (May 29 2018 at 13:41, on Zulip):

talking about the compare-mode

Vytautas Astrauskas (May 29 2018 at 13:46, on Zulip):

@Santiago Pastorino Thanks!

Vytautas Astrauskas (May 29 2018 at 13:51, on Zulip):

JFYI: I have added an option to choose the Polonius algorithm with an environment variable (pull request) and now I am working on comparing the reported errors.

Santiago Pastorino (May 29 2018 at 13:57, on Zulip):

will take a look in a bit :)

Santiago Pastorino (May 29 2018 at 14:04, on Zulip):

left some comments take a look to see if makes sense to you :)

Vytautas Astrauskas (May 29 2018 at 14:42, on Zulip):

left some comments take a look to see if makes sense to you :)

@Santiago Pastorino Thanks! Fixed.

Santiago Pastorino (May 29 2018 at 15:30, on Zulip):

@Vytautas Astrauskas have you seen a comment I left (or try to) about match here https://github.com/rust-lang-nursery/polonius/pull/64 ?

Vytautas Astrauskas (May 29 2018 at 17:46, on Zulip):

@Santiago Pastorino I have seen your comment that you tried to leave a comment :relaxed:. I'll try to replace match with if else.

Santiago Pastorino (May 29 2018 at 17:48, on Zulip):

@Vytautas Astrauskas just in case :), take my comments as a suggestion, I'm not the one accepting stuff on rustc :wink:

Vytautas Astrauskas (May 29 2018 at 17:58, on Zulip):

@Vytautas Astrauskas just in case :), take my comments as a suggestion, I'm not the one accepting stuff on rustc :wink:

Your suggestions make a lot of sense to me so far. :relaxed:

Last update: Nov 21 2019 at 23:25UTC