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
@Tamas Szabo I think you want to ping @nikomatsakis
@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.
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.
It lives at https://github.com/rust-lang/polonius
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.
Super keen to learn about Datafrog! :D
(( Still planning on a Differential explainer, @nikomatsakis, just .. all the things ... >.< ))