Stream: t-compiler/wg-polonius

Topic: IncA program analysis


Tamas Szabo (Jun 17 2019 at 13:19, on Zulip):

hey guys! I am one of the developers of the IncA program analysis framework (https://github.com/szabta89/IncA). I met with Niko back in November at OOPSLA, and we had a chat about the Rust borrow checker implementation in Datalog. I was in contact recently with Frank McSherry, and he mentioned that custom lattices with aggregation may be something that is interesting for your use cases. These are not standard features in Datalog, but IncA does support them, and it does that incrementally, so that the analysis result can be kept up to date as the input changes. I am here to find out if this is really interesting to you. Cheers, Tamas

pachi (Jun 17 2019 at 13:37, on Zulip):

@Tamas Szabo I think you want to ping @nikomatsakis

nikomatsakis (Jun 17 2019 at 14:25, on Zulip):

@Tamas Szabo I think he was referring to some extension ideas that we had, which needed to compute an equality relation which we propagate around. We've not thought too much yet about how to do that, but perhaps it is something that custom lattices might help with.

Tamas Szabo (Jun 17 2019 at 15:00, on Zulip):

In any case, I would be interested to see your Datalog implemenation, if this is possible at all. Was that implemented in Souffle? We actually do have an importer in IncA that can import Souffle programs, so it would not be too hard to port your analysis.

nikomatsakis (Jun 17 2019 at 20:35, on Zulip):

It lives at https://github.com/rust-lang/polonius

nikomatsakis (Jun 17 2019 at 20:37, on Zulip):

You may find some of the youtube videos here to be useful, @Tamas Szabo -- otherwise, I'll try to answer questions. =) This talk in particular explains how datafrog works, kind of near the end.

Frank McSherry (Jun 19 2019 at 11:48, on Zulip):

Super keen to learn about Datafrog! :D

(( Still planning on a Differential explainer, @nikomatsakis, just .. all the things ... >.< ))

Last update: Nov 15 2019 at 20:00UTC