Stream: t-compiler/wg-polonius

Topic: planning meeting 2019.11.05


lqd (Nov 05 2019 at 16:09, on Zulip):

hey all :)

IIUC the meeting will be in a couple hours (it's my understanding that DST is now in place in the US as well, so back at the regular time) which is 9PM for us Europeans.

since we were hoping to do some planning (especially around the focus week at the end of the month) tonight I've updated the "state of polonius" list here https://hackmd.io/wGwGGRCKStiWBq9voP4e2A?view, so that we can see what's in-flight etc.

(I'm still kind of away, preparing for rustfest but I'll definitely be at the meeting)

lqd (Nov 05 2019 at 17:58, on Zulip):

(where "9PM" meant "9PM CET", and "a couple hours" meant "4 hours" — should be actually a couple hours from now — ♪ whistles ♫)

Albin Stjerna (Nov 05 2019 at 20:02, on Zulip):

Should be now, right?

lqd (Nov 05 2019 at 20:02, on Zulip):

I think

Albin Stjerna (Nov 05 2019 at 20:02, on Zulip):

The Google Calendar seems to say the same

lqd (Nov 05 2019 at 20:03, on Zulip):

heh I was checking the same thing

nikomatsakis (Nov 05 2019 at 20:04, on Zulip):

Hey all

lqd (Nov 05 2019 at 20:04, on Zulip):

:wave:

nikomatsakis (Nov 05 2019 at 20:04, on Zulip):

How're things

lqd (Nov 05 2019 at 20:05, on Zulip):

fine and you ?

lqd (Nov 05 2019 at 20:05, on Zulip):

there might have been some slight confusion about DST but seems to be fixed worldwide :)

nikomatsakis (Nov 05 2019 at 20:06, on Zulip):

heh yes :)

lqd (Nov 05 2019 at 20:06, on Zulip):

I don't know if you two saw what I wrote earlier, but I (only) managed to update the list of in-flight things (or future things)

lqd (Nov 05 2019 at 20:07, on Zulip):

so that we could have an idea and possibly pre-plan our goals for the work at the end of the month

lqd (Nov 05 2019 at 20:07, on Zulip):

(hopefully I didn't miss anything)

nikomatsakis (Nov 05 2019 at 20:07, on Zulip):

I did not see

nikomatsakis (Nov 05 2019 at 20:08, on Zulip):

I accidentally hit "mark all as read" and all of zulip a few hours back

nikomatsakis (Nov 05 2019 at 20:08, on Zulip):

It was ... very freeing

nikomatsakis (Nov 05 2019 at 20:08, on Zulip):

But I am probably missing some messages

nikomatsakis (Nov 05 2019 at 20:08, on Zulip):

Anyway, I'm opening the hackmd now

lqd (Nov 05 2019 at 20:08, on Zulip):

an easy way to achieve inbox zero :)

nikomatsakis (Nov 05 2019 at 20:09, on Zulip):

s/an easy way/the only way/

nikomatsakis (Nov 05 2019 at 20:09, on Zulip):

ok so

nikomatsakis (Nov 05 2019 at 20:09, on Zulip):

skimming the document

nikomatsakis (Nov 05 2019 at 20:09, on Zulip):

I also saw @Albin Stjerna raised some points about move errors

lqd (Nov 05 2019 at 20:10, on Zulip):

yeah, and a PR

Albin Stjerna (Nov 05 2019 at 20:10, on Zulip):

Yes, one, but Matthew Jasper responded

Albin Stjerna (Nov 05 2019 at 20:10, on Zulip):

And I think I...will do what they said. It's not what I am currently doing though, so there might be an off-by-one on initialisation tracking

Albin Stjerna (Nov 05 2019 at 20:10, on Zulip):

I realised this when I was rewriting that section for my thesis

Albin Stjerna (Nov 05 2019 at 20:10, on Zulip):

(this is totally what I should be doing for my PhD)

lqd (Nov 05 2019 at 20:11, on Zulip):

(the start/mid separation doesn't exist in rustc so maybe the difference would not matter in practice but yeah Start points seem best indeed)

Albin Stjerna (Nov 05 2019 at 20:11, on Zulip):

I think it does, because I think every move becomes a move error otherwise

lqd (Nov 05 2019 at 20:11, on Zulip):

haha

lqd (Nov 05 2019 at 20:11, on Zulip):

that is a practical difference

nikomatsakis (Nov 05 2019 at 20:12, on Zulip):

OK, so there are probably two? main axes of expansion -- well, maybe 3

nikomatsakis (Nov 05 2019 at 20:12, on Zulip):
lqd (Nov 05 2019 at 20:12, on Zulip):

I guess we should focus on completeness and correctness first

nikomatsakis (Nov 05 2019 at 20:13, on Zulip):

and then there is the

nikomatsakis (Nov 05 2019 at 20:13, on Zulip):

right, Im talking about the "completeness and correctness" side of things

nikomatsakis (Nov 05 2019 at 20:13, on Zulip):

so my take on higher-ranked subtyping is

nikomatsakis (Nov 05 2019 at 20:13, on Zulip):

this is not polonius's problem

nikomatsakis (Nov 05 2019 at 20:13, on Zulip):

I've been meaning forever to try and write about the experimentation that I did

lqd (Nov 05 2019 at 20:13, on Zulip):

solely chalk's problem ?

nikomatsakis (Nov 05 2019 at 20:14, on Zulip):

but the tl;dr is that I think chalk should handle all the higher-ranked reasoning and just emit a set of "top-level region constraints" for polonius to solve

lqd (Nov 05 2019 at 20:14, on Zulip):

does that mean that we need to get chalk in rustc for polonius to be useful ?

nikomatsakis (Nov 05 2019 at 20:14, on Zulip):

I guess a question, which I've not through very hard about it, is .. yes, that.

nikomatsakis (Nov 05 2019 at 20:15, on Zulip):

I'm actually sort of unsure what happens with "higher-ranked outlines" now

nikomatsakis (Nov 05 2019 at 20:15, on Zulip):

Regardless, I think a good goal before the coming week would be for me to review your PR and/or document my thoughts there

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

review Albin's move errors PR that is ?

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

I'm still planning on trying to do this "Nov focus week" thing, although I do need to figure out what will have to get canceled to make way for that

nikomatsakis (Nov 05 2019 at 20:17, on Zulip):

review Albin's move errors PR that is ?

actually I meant the "placeholder loans" stuff

nikomatsakis (Nov 05 2019 at 20:17, on Zulip):

well, ok, there are 4 open PRs

nikomatsakis (Nov 05 2019 at 20:17, on Zulip):
nikomatsakis (Nov 05 2019 at 20:17, on Zulip):
nikomatsakis (Nov 05 2019 at 20:17, on Zulip):
lqd (Nov 05 2019 at 20:18, on Zulip):

ah, that's not yet a PR as it depends on a couple open questions and another PR, but yeah at least making sure this is going in the right direction

nikomatsakis (Nov 05 2019 at 20:18, on Zulip):
nikomatsakis (Nov 05 2019 at 20:18, on Zulip):

should we .. just merge this?

Albin Stjerna (Nov 05 2019 at 20:18, on Zulip):

I think my PR should wait until we have a way to err...report move errors

Albin Stjerna (Nov 05 2019 at 20:18, on Zulip):

Otherwise I can't test it

nikomatsakis (Nov 05 2019 at 20:19, on Zulip):

what about this?

Albin Stjerna (Nov 05 2019 at 20:19, on Zulip):

Of course, I will happily take feedback etc before that

lqd (Nov 05 2019 at 20:19, on Zulip):

do you need this one for your work Albin ?

lqd (Nov 05 2019 at 20:19, on Zulip):

(134)

Albin Stjerna (Nov 05 2019 at 20:19, on Zulip):

It would be the easiest way to sneak out move errors, yes

nikomatsakis (Nov 05 2019 at 20:20, on Zulip):

it seems like a step in the right direction to me

lqd (Nov 05 2019 at 20:20, on Zulip):

it seems like a good first step

nikomatsakis (Nov 05 2019 at 20:20, on Zulip):

I think the only thing we were wondering before was

nikomatsakis (Nov 05 2019 at 20:20, on Zulip):

should we give ownership of the facts

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

But I guess we could also decide on some other interface for reporting other errors, and that would work just as well

nikomatsakis (Nov 05 2019 at 20:20, on Zulip):

whereas now we pass it by reference?

nikomatsakis (Nov 05 2019 at 20:20, on Zulip):

but we could handle that ina follow-up PR

nikomatsakis (Nov 05 2019 at 20:20, on Zulip):

I'm inclined to merge stuff

lqd (Nov 05 2019 at 20:20, on Zulip):

yeah I was thinking followup as well

lqd (Nov 05 2019 at 20:21, on Zulip):

as it'd require releasing a version, updating rustc (with T::Factsas well)

nikomatsakis (Nov 05 2019 at 20:21, on Zulip):

merge?

Albin Stjerna (Nov 05 2019 at 20:21, on Zulip):

@Vytautas Astrauskas, if you are here, does your work rely on having access to Polonius' facts after Polonius has executed, from Rust? Would giving ownership of Polonius' facts affect you?

lqd (Nov 05 2019 at 20:21, on Zulip):

maybe the way the variants return their output could be better, esp when adding the illegal subset relation errors next/soon

nikomatsakis (Nov 05 2019 at 20:22, on Zulip):

merged

nikomatsakis (Nov 05 2019 at 20:22, on Zulip):

woohoo, we're on a roll

lqd (Nov 05 2019 at 20:22, on Zulip):

:)

lqd (Nov 05 2019 at 20:22, on Zulip):

do you need a WIP placeholder loans PR or looking at the branch would be enough ?

nikomatsakis (Nov 05 2019 at 20:22, on Zulip):

WIP PR's are helpful

nikomatsakis (Nov 05 2019 at 20:22, on Zulip):

easier to find :)

lqd (Nov 05 2019 at 20:23, on Zulip):

ok I'll try to do one before leaving for rustfest (or there :)

lqd (Nov 05 2019 at 20:24, on Zulip):

@Albin Stjerna you mean prusti itself ?

lqd (Nov 05 2019 at 20:25, on Zulip):

(I do wonder how do they "make use of polonius" though yeah, I can ask them at rustfest)

nikomatsakis (Nov 05 2019 at 20:25, on Zulip):

I was just talking some to them today

Albin Stjerna (Nov 05 2019 at 20:25, on Zulip):

We talked briefly about this at SPLASH

Albin Stjerna (Nov 05 2019 at 20:26, on Zulip):

Ah, good

nikomatsakis (Nov 05 2019 at 20:26, on Zulip):

I think they may be scraping things off the disk, but not sure

Albin Stjerna (Nov 05 2019 at 20:26, on Zulip):

I got that impression as well

lqd (Nov 05 2019 at 20:26, on Zulip):

I'm wondering (the same question about any new polonius feature really) how best to test illegal subset relations errors

Albin Stjerna (Nov 05 2019 at 20:26, on Zulip):

They also had some trouble translating some interned values to something useful

nikomatsakis (Nov 05 2019 at 20:26, on Zulip):

@lqd coming back to the analysis

nikomatsakis (Nov 05 2019 at 20:27, on Zulip):

I'd really like to remove datafrog-opt and (perhaps) the location insensitive variant. I'm not sure why I'm so obsessed with this. I guess it's just that, coming back to polonius, it feels a bit overwhelming to have many variants.

nikomatsakis (Nov 05 2019 at 20:27, on Zulip):

I'd also like to port over to your nifty compilation tool :)

nikomatsakis (Nov 05 2019 at 20:27, on Zulip):

though perhaps that is mildly lower priority

nikomatsakis (Nov 05 2019 at 20:27, on Zulip):

I still don't quite understand what's blocking those moves

Albin Stjerna (Nov 05 2019 at 20:28, on Zulip):

(I do wonder how do they "make use of polonius" though yeah, I can ask them at rustfest)

@lqd It's this, but Polonius is literally just an argument to rustc in a footnote https://2019.splashcon.org/details/splash-2019-oopsla/31/Leveraging-Rust-Types-for-Modular-Specification-and-Verification

nikomatsakis (Nov 05 2019 at 20:28, on Zulip):

it seemed like you had found that some simple optimizations made datafrog-opt far less important?

lqd (Nov 05 2019 at 20:28, on Zulip):

I really need to make sure it works on more inputs than just clap though, first :)

Albin Stjerna (Nov 05 2019 at 20:29, on Zulip):

Once my thesis is done, I really want to do something about the benchmarking situation

lqd (Nov 05 2019 at 20:29, on Zulip):

it did seem the LocationInsensitive/DatafrogOpt variants were useful for rustc tests

lqd (Nov 05 2019 at 20:30, on Zulip):

I'd like to check this again as well, but I was hoping we could fix the remaining issues we have and enable the compare more on CI

lqd (Nov 05 2019 at 20:30, on Zulip):

(but if we're talking about a chalk-timescale, maybe it's not super urgent now ofc)

nikomatsakis (Nov 05 2019 at 20:30, on Zulip):

speaking of the "focus week" -- I need to figure out what it will take to really make that ap ossibility for me -- but I think what is most realistic is that i'd like to schedule some big meetings where we can kind of get on zoom and hack together

nikomatsakis (Nov 05 2019 at 20:31, on Zulip):

e.g. I could imagine saying "let's spend 3-4 hours trying to get placeholder loans going" or something like that

nikomatsakis (Nov 05 2019 at 20:31, on Zulip):

not sure if that's the best structure but it seems plausible ;)

nikomatsakis (Nov 05 2019 at 20:31, on Zulip):

if so, we could try to schedule out some meetings

lqd (Nov 05 2019 at 20:31, on Zulip):

@Albin Stjerna I reran the stats on your csvs btw, it's in the list, to at least have some of the bigger/slower functions/crates in there

lqd (Nov 05 2019 at 20:32, on Zulip):

that could work nicely

lqd (Nov 05 2019 at 20:32, on Zulip):

and placeholder loans seem quick to do / integrate as well

lqd (Nov 05 2019 at 20:32, on Zulip):

(but indeed impact the LocationInsensitive/Hybrid variants you were mentioning)

Albin Stjerna (Nov 05 2019 at 20:34, on Zulip):

if so, we could try to schedule out some meetings

I'm up for it!

Albin Stjerna (Nov 05 2019 at 20:35, on Zulip):

You mean now or some other time?

lqd (Nov 05 2019 at 20:36, on Zulip):

the meetings ? for the "focus week" possibly around the end of november

lqd (Nov 05 2019 at 20:36, on Zulip):

or scheduling now you mean ?

Albin Stjerna (Nov 05 2019 at 20:36, on Zulip):

Precisely

nikomatsakis (Nov 05 2019 at 20:37, on Zulip):

I would prefer to schedule them in advance, doesn't necessarily have to be now

nikomatsakis (Nov 05 2019 at 20:37, on Zulip):

I'm skimming https://github.com/rust-lang/polonius/pull/126/

nikomatsakis (Nov 05 2019 at 20:37, on Zulip):

we could talk about what their topics would be, perhaps :)

nikomatsakis (Nov 05 2019 at 20:37, on Zulip):

@Albin Stjerna regarding move errors --

nikomatsakis (Nov 05 2019 at 20:37, on Zulip):

so right now we're computing move-errors but we have no code in rustc to report them, is that it?

lqd (Nov 05 2019 at 20:38, on Zulip):

I believe so yes

lqd (Nov 05 2019 at 20:38, on Zulip):

but it seemed their location was still in flux

nikomatsakis (Nov 05 2019 at 20:38, on Zulip):

Where are we in the "grand renaming" =) I have to say that the new names felt really good during my rustbeltrust talk, for the most part.

nikomatsakis (Nov 05 2019 at 20:38, on Zulip):

The main exception being "node"

nikomatsakis (Nov 05 2019 at 20:39, on Zulip):

That...feels "ok" but also kind of jargon-y.

nikomatsakis (Nov 05 2019 at 20:39, on Zulip):

Maybe it's ok if Path and Point have the same first letter, if we avoid using individual letters anyway

lqd (Nov 05 2019 at 20:39, on Zulip):

in the Great Renaming of 2019, we are at: CFG items are still points ;)

lqd (Nov 05 2019 at 20:39, on Zulip):

mostly we need to do some more renaming for the relation names I think

nikomatsakis (Nov 05 2019 at 20:39, on Zulip):

yeah, the relation names are on my mind

lqd (Nov 05 2019 at 20:40, on Zulip):

the predicates still refer to the old nomenclature

nikomatsakis (Nov 05 2019 at 20:40, on Zulip):

I should probably try to make a canonical write-up of why we have start/mid nodes in the first place

lqd (Nov 05 2019 at 20:40, on Zulip):

and some which don't refer to it might not have the best names either

lqd (Nov 05 2019 at 20:40, on Zulip):

(requires)

nikomatsakis (Nov 05 2019 at 20:40, on Zulip):

yeah that's terrible :)

Albin Stjerna (Nov 05 2019 at 20:40, on Zulip):

so right now we're computing move-errors but we have no code in rustc to report them, is that it?

Yes, that's it

nikomatsakis (Nov 05 2019 at 20:40, on Zulip):

it seems like such code shouldn't be too hard to add

Albin Stjerna (Nov 05 2019 at 20:40, on Zulip):

we also have no code in Polonius-the-binary to report them, but I could of course add that

lqd (Nov 05 2019 at 20:41, on Zulip):

is it a chicken and egg situation in that you need to update rustc to emit move errors to check if the move errors you compute are correct ?

Albin Stjerna (Nov 05 2019 at 20:42, on Zulip):

Hmm, not really, it's more that I would need to have some sort of interface for Polonius to report more than one kind of error at all

Albin Stjerna (Nov 05 2019 at 20:42, on Zulip):

But yes, I guess we could also have rustc emit the move errors as inputs and then compare those

lqd (Nov 05 2019 at 20:43, on Zulip):

I think adding a new one in the Output struct may be the way to go

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

I think so too

Albin Stjerna (Nov 05 2019 at 20:44, on Zulip):

I need to go fairly soon

nikomatsakis (Nov 05 2019 at 20:44, on Zulip):

Hmm, not really, it's more that I would need to have some sort of interface for Polonius to report more than one kind of error at all

I feel like we should be able to land the PR in a mode where it repors errors through a field

nikomatsakis (Nov 05 2019 at 20:44, on Zulip):

then update rustc

nikomatsakis (Nov 05 2019 at 20:44, on Zulip):

and maybe come back and fix up the code

lqd (Nov 05 2019 at 20:44, on Zulip):

where we have only errors now we'll have subset_errors and move_errors as well

nikomatsakis (Nov 05 2019 at 20:44, on Zulip):

I think adding a new one in the Output struct may be the way to go

I was assuming this is what we would do, yes

lqd (Nov 05 2019 at 20:44, on Zulip):

agreed, and we need to update to the FactTypes anyway

lqd (Nov 05 2019 at 20:45, on Zulip):

(I have a patch for that already)

lqd (Nov 05 2019 at 20:46, on Zulip):

in any case it seems like the PR needs a bit more work before reviewing, but we can get the rest of the work done soon

Albin Stjerna (Nov 05 2019 at 20:46, on Zulip):

Yes, for example during the focus week, if not earlier

lqd (Nov 05 2019 at 20:47, on Zulip):

yeah :)

lqd (Nov 05 2019 at 20:47, on Zulip):

getting these "completeness" PRs done would be a nice goal

Albin Stjerna (Nov 05 2019 at 20:47, on Zulip):

Definitely!

nikomatsakis (Nov 05 2019 at 20:47, on Zulip):

yes

nikomatsakis (Nov 05 2019 at 20:48, on Zulip):

I think our goal should be:

nikomatsakis (Nov 05 2019 at 20:48, on Zulip):

probably in that order?

lqd (Nov 05 2019 at 20:48, on Zulip):

seems like a nice plan

nikomatsakis (Nov 05 2019 at 20:48, on Zulip):

I'm not 100% sure, I think that's the order of "fewest unknowns" to "most unknowns"

nikomatsakis (Nov 05 2019 at 20:48, on Zulip):

so I guess it depends if we want to prioritize getting things done

nikomatsakis (Nov 05 2019 at 20:48, on Zulip):

or tackling complex problems

lqd (Nov 05 2019 at 20:48, on Zulip):

(if higher rank subregions will be solely a chalk problem)

nikomatsakis (Nov 05 2019 at 20:48, on Zulip):

but we may also be able to make some progress on move errors etc before hand

lqd (Nov 05 2019 at 20:49, on Zulip):

seems likely as well, and the same for placeholder loans

nikomatsakis (Nov 05 2019 at 20:49, on Zulip):

I am thinking that maybe I can try to use some of my "5am time" to work on polonius over next few weeks

nikomatsakis (Nov 05 2019 at 20:49, on Zulip):

I've been on a rayon kick lately :)

lqd (Nov 05 2019 at 20:49, on Zulip):

at least it gives us something to shoot for and we can adjust before then if needed

nikomatsakis (Nov 05 2019 at 20:50, on Zulip):

(context: I try to give myself like 30-45 minutes in the morning to do fun stuff I wouldn't otherwise have time to do;)

lqd (Nov 05 2019 at 20:50, on Zulip):

yeah the thread sleeping RFC :thumbs_up:

lqd (Nov 05 2019 at 20:51, on Zulip):

if we can get the focus week you can still use your 5am time to do other enjoyable things though :)

nikomatsakis (Nov 05 2019 at 20:51, on Zulip):

I think our goal should be:

let's use this as the plan

Albin Stjerna (Nov 05 2019 at 20:51, on Zulip):

...like sleeping?

nikomatsakis (Nov 05 2019 at 20:51, on Zulip):

heh I used to try and getup at 4am

nikomatsakis (Nov 05 2019 at 20:51, on Zulip):

but I was becoming a very grouchy person

nikomatsakis (Nov 05 2019 at 20:52, on Zulip):

so I had to take back an hour of sleep :)

lqd (Nov 05 2019 at 20:52, on Zulip):

(I wonder if we should help out with chalk as well, since it'll also help polonius)

nikomatsakis (Nov 05 2019 at 20:52, on Zulip):

heh I'm already planning a "chalk week"

lqd (Nov 05 2019 at 20:53, on Zulip):

nice :)

nikomatsakis (Nov 05 2019 at 20:53, on Zulip):

I think most realistic is to try and create like .. 4 meeting times?

Albin Stjerna (Nov 05 2019 at 20:53, on Zulip):

It's actually close enough to my PhD topic I might be able to argue for it

nikomatsakis (Nov 05 2019 at 20:53, on Zulip):

like I don't think 8h a day all week is really realistic for anyone

Albin Stjerna (Nov 05 2019 at 20:53, on Zulip):

Depending on how close to SAT it is

nikomatsakis (Nov 05 2019 at 20:53, on Zulip):

given time zones, mornings are probably best?

nikomatsakis (Nov 05 2019 at 20:53, on Zulip):

er, my mornings

Albin Stjerna (Nov 05 2019 at 20:53, on Zulip):

Yes, definitely

lqd (Nov 05 2019 at 20:53, on Zulip):

5am mornings ?

lqd (Nov 05 2019 at 20:54, on Zulip):

probably 4PM for us if 9-10am boston time

lqd (Nov 05 2019 at 20:54, on Zulip):

(or so, maybe it's just a 5-hour difference ?)

nikomatsakis (Nov 05 2019 at 20:54, on Zulip):

I think I could do like 9:00-13:00 on most days, which is like 15:00-19:00 CEST?

lqd (Nov 05 2019 at 20:55, on Zulip):

I'll likely take the week off from work, so I'll be available whenever, but that time would work

nikomatsakis (Nov 05 2019 at 20:55, on Zulip):

modulo compiler team meetings :)

lqd (Nov 05 2019 at 20:55, on Zulip):

of course :)

lqd (Nov 05 2019 at 20:55, on Zulip):

(that reminds me I'll write a blurb for this week's wg checkin, as it's us and I'll be travelling to rustfest on thursday)

nikomatsakis (Nov 05 2019 at 20:56, on Zulip):

ok. I gotta run

lqd (Nov 05 2019 at 20:56, on Zulip):

:wave: everyone :)

Vytautas Astrauskas (Nov 06 2019 at 10:43, on Zulip):

@Vytautas Astrauskas, if you are here, does your work rely on having
access to Polonius' facts after Polonius has executed, from Rust?

Simply speaking we need Polonius input facts (currently we are reading the facts from the CSV dump) and a way to run Polonius manually (easy since Polonius is a library :smile:).

Would giving ownership of Polonius' facts affect you?

We are currently reading the facts from the dump, so no. However, it would be nice to have a way to obtain facts without going through the disk so that we can avoid hacky parsing of identifiers (like mapping position facts to statements in MIR). For example, if there was a a public function which computes the Polonius input facts for a given function, I think that would be good enough for us, even if this meant that this function would be called twice while running Prusti (once for the borrow checker and once for Prusti).

I think they may be scraping things off the disk, but not sure

More specifically, we parse nll-facts and rustc.*.-------.renumber.0.mir with regex and then map the obtained information on top of mir_validated.

Albin Stjerna (Nov 06 2019 at 11:28, on Zulip):

@Vytautas Astrauskas Hm, and from where would you call this function?

Vytautas Astrauskas (Nov 06 2019 at 11:33, on Zulip):

Prusti (and MIRAI) use the after analysis callback. So, it should be possible to call the function from that callback.

Last update: Nov 15 2019 at 20:40UTC