Stream: t-compiler/wg-polonius

Topic: Using Soufflé


ecstatic-morse (Jan 04 2021 at 21:36, on Zulip):

I've decided that it's easier for me to experiment with polonius using Soufflé than datafrog. I have a hard time translating between datalog rules and calls to the datafrog API. The comments are quite helpful, and I assume the little things like swapping indexes gets easier with time. However, using a full-featured datalog engine has other benefits (rules can't get out of sync, etc.) and seems better for prototyping. Judging from the initial blog post, Niko switched away from Soufflé pretty early on. This makes me somewhat less confident, but still confident enough to proceed.

ecstatic-morse (Jan 04 2021 at 21:38, on Zulip):

I did this on Sunday using the rules from a HackMD floating out in the ether: https://github.com/ecstatic-morse/polonius/tree/souffle

lqd (Jan 04 2021 at 21:38, on Zulip):

https://github.com/rust-lang/polonius/pull/126

ecstatic-morse (Jan 04 2021 at 21:40, on Zulip):

Ah damn, I wish I would have seen that. I had to choose between writing "literate Prolog" markdown files and extensively commented .dl files. I probably would have gone the other way if I would have known.

lqd (Jan 04 2021 at 21:40, on Zulip):

the automatic conversion is interesting

lqd (Jan 04 2021 at 21:42, on Zulip):

(we probably still have the original .dl from way back when :)

ecstatic-morse (Jan 04 2021 at 21:42, on Zulip):

(I did see your renaming PR. Mine uses the new names.)

lqd (Jan 04 2021 at 21:42, on Zulip):

nice !

lqd (Jan 04 2021 at 21:42, on Zulip):

(so does this PR, I've updated it recently)

lqd (Jan 04 2021 at 21:43, on Zulip):

using your script could be nice as well

ecstatic-morse (Jan 04 2021 at 21:44, on Zulip):

Anyways, I fixed up some typos and some missing rules and it compiles. However, it seems something is still missing, since it's not outputting any errors.

lqd (Jan 04 2021 at 21:44, on Zulip):

what input are you testing ?

ecstatic-morse (Jan 04 2021 at 21:44, on Zulip):

(I tried on the vec-push-ref test cases)

lqd (Jan 04 2021 at 21:44, on Zulip):

ok

ecstatic-morse (Jan 04 2021 at 21:44, on Zulip):

foo1 and foo2

lqd (Jan 04 2021 at 21:44, on Zulip):

the thing with this hackmd is that some of it still uses placeholder loans IIRC

lqd (Jan 04 2021 at 21:45, on Zulip):

it probably shouldn't matter to the errors in vec-push-ref as IIRC they were regular errors

ecstatic-morse (Jan 04 2021 at 21:45, on Zulip):

It does have the placeholder rules.

lqd (Jan 04 2021 at 21:45, on Zulip):

yeah but which ones

lqd (Jan 04 2021 at 21:46, on Zulip):

I've switched away from computing subset errors with placeholder loans in 2/3 variants

ecstatic-morse (Jan 04 2021 at 21:46, on Zulip):
origin_contains_loan_on_entry(origin, loan, targetNode) :-
  origin_contains_loan_on_entry(origin, loan, sourceNode),
  !loan_killed_at(loan, sourceNode),
  cfg_edge(sourceNode, targetNode),
  (origin_live_on_entry(origin, targetNode); placeholder(origin, _)).
lqd (Jan 04 2021 at 21:47, on Zulip):

yeah placeholder loans are something else than this one

ecstatic-morse (Jan 04 2021 at 21:47, on Zulip):

This one? It's whatever was in here https://hackmd.io/CGMNjt1hR_qYtsR9hgdGmw?view

lqd (Jan 04 2021 at 21:47, on Zulip):

I'll look them up

lqd (Jan 04 2021 at 21:47, on Zulip):

I'm not exactly sure whether the rules in the hackmd are up to date for move/init and liveness, I would hope so but I'm not sure :/

lqd (Jan 04 2021 at 21:48, on Zulip):

yes that's the one

ecstatic-morse (Jan 04 2021 at 21:48, on Zulip):

I did a sanity check and all the rules seem fine. I have a few questions about liveness but it all seems reasonable.

ecstatic-morse (Jan 04 2021 at 21:49, on Zulip):

I might just be using the wrong input facts, since I had to rename them.

lqd (Jan 04 2021 at 21:49, on Zulip):

eg the second rule here https://hackmd.io/CGMNjt1hR_qYtsR9hgdGmw?view#Error-reporting is no more

ecstatic-morse (Jan 04 2021 at 21:49, on Zulip):
mv borrow_region.facts loan_issued_at.facts
mv killed.facts loan_killed_at.facts
mv invalidates.facts loan_invalidated_at.facts

mv child_path.facts parent_path.facts

mv known_subset.facts known_placeholder_subset.facts
mv outlives.facts subset_base.facts
lqd (Jan 04 2021 at 21:49, on Zulip):

at least, there's a PR to change it

lqd (Jan 04 2021 at 21:51, on Zulip):

or am I spewing random bs, I have updated the hackmd recently

lqd (Jan 04 2021 at 21:51, on Zulip):

(sorry dylan, I'm a bit tired from work and trying to make progress on const generics defaults during the holidays)

lqd (Jan 04 2021 at 21:52, on Zulip):

another point of difference

lqd (Jan 04 2021 at 21:53, on Zulip):

the rules use soufflé's alternative ; combinator

lqd (Jan 04 2021 at 21:53, on Zulip):

but the code does not, it does a similar thing, by materializing liveness for the universal regions / placeholders at all points in the cfg

ecstatic-morse (Jan 04 2021 at 21:55, on Zulip):

No worries. I was planning to work on my own since you're busy for this month at least and Niko is presumably super busy. Figuring this stuff out means I reach competency faster.

ecstatic-morse (Jan 04 2021 at 21:55, on Zulip):

Although I do wish I had known about the rules documentation PR XD

ecstatic-morse (Jan 04 2021 at 21:56, on Zulip):

Yes. You have a PR that adds the placeholder disjunction to the datafrog rules correct?

lqd (Jan 04 2021 at 21:57, on Zulip):

yeah

lqd (Jan 04 2021 at 21:57, on Zulip):

it's still WIP because of the Opt variant which are the only ones using antijoins on liveness

lqd (Jan 04 2021 at 21:57, on Zulip):

and I wanted to discuss this a bit, but I expect we'd just need to add the implicit antijoins and that it should work

lqd (Jan 04 2021 at 21:58, on Zulip):

it's just ... verbose

lqd (Jan 04 2021 at 21:58, on Zulip):

and maybe something datafrog could/should help with

ecstatic-morse (Jan 04 2021 at 21:58, on Zulip):

(I assumed that none of that would affect vec_push_ref):

fn foo1() {
    let mut x = 22;
    let mut v = vec![];
    let p = &x;

    if something() {
        v.push(p);
        x += 1; //~ ERROR
    } else {
        x += 1;
    }

    drop(v);
}
lqd (Jan 04 2021 at 21:59, on Zulip):

yeah same

lqd (Jan 04 2021 at 22:00, on Zulip):

I'm not sure how to debug that apart from comparing the relations contents first between the 3 phases

lqd (Jan 04 2021 at 22:00, on Zulip):

and if that doesn't help, see the tuples emitted each round as well

ecstatic-morse (Jan 04 2021 at 22:00, on Zulip):

Yep. That was my next step but I ran out of time over the weekend. I'll let you know how it goes when I pick it up again, but I'm also busy.

lqd (Jan 04 2021 at 22:01, on Zulip):

I'll try to look at it if I find the time as well

ecstatic-morse (Jan 04 2021 at 22:01, on Zulip):

I wasn't gonna post at all, but you nerd-sniped me with vEB trees. And anyone who has time to think about vEB trees has too much time.

lqd (Jan 04 2021 at 22:01, on Zulip):

haha :joy:

lqd (Jan 04 2021 at 22:02, on Zulip):

there's always time to read on the toilet, like Muchnick's book :p

lqd (Jan 04 2021 at 22:23, on Zulip):

you've done a great job on commenting the rules in your branch

lqd (Jan 04 2021 at 22:24, on Zulip):

or maybe those are from the hackmd (pretty sure you did add some of your own tho)

lqd (Jan 04 2021 at 22:27, on Zulip):

(it shows that I'm not familiar with the comments on the hackmd's move/init and liveness rules, obviously ... they work in rustc == I'm happy)

ecstatic-morse (Jan 05 2021 at 05:05, on Zulip):

Nah those are all verbatim from the HackMD. Thank Albin. I will add to them eventually though.

ecstatic-morse (Jan 05 2021 at 05:09, on Zulip):

I found the critical differences in my transcribed version. Two relations had their arguments flipped from how they appeared in the fact file, and liveness was manually adding some facts here. Tuple counts now match up for examples without placeholders.

ecstatic-morse (Jan 05 2021 at 05:13, on Zulip):

Naive souffle can run the clap-rs benchmark in 2 minutes without using a crazy amount of RAM, so it's definitely usable. Running on 8 cores helps of course (-j8).

ecstatic-morse (Jan 05 2021 at 05:14, on Zulip):

That's enough for tonight though.

lqd (Jan 05 2021 at 07:53, on Zulip):

ah dang I now remember the different ordering in the loan invalidations relation https://github.com/rust-lang/polonius/blob/f2c0fcafdcd341486f7c2225824b26feb0d6b9ce/polonius-engine/src/output/mod.rs#L222

lqd (Jan 05 2021 at 07:55, on Zulip):

and the liveness one is the one I mentioned above, that should have been taken care of by all the "origin is live ; origin is placeholder" joins in the loan analysis rules though

lqd (Jan 05 2021 at 08:00, on Zulip):

maybe we missed one in the hackmd ?

lqd (Jan 06 2021 at 11:53, on Zulip):

btw RE: https://github.com/ecstatic-morse/polonius/commit/3e00d634ccb1026a6d04a6cebb379541b27a9eed the updated names and facts should already be updated in https://github.com/rust-lang/polonius/pull/155 (with the caveat https://github.com/rust-lang/polonius/pull/156#issuecomment-751460154 where I forgot to rename two internal relations in that PR, but that shouldn't matter to use the repository facts with soufflé)

Last update: Jun 20 2021 at 00:30UTC