Stream: t-compiler/wg-polonius

Topic: dafny


Andrea Lattuada (Jun 29 2020 at 12:01, on Zulip):

Hi folks, I’m a research intern at VMware (PhD student at ETH Zürich, where I worked with Frank). I’m currently experimenting with “duct-taping” polonius to the dafny programming language (if you’re unfamiliar, it’s a verification+imperative language from MSR; its imperative part is similar to c#). I’m working with some of the authors of the IronClad/IronFleet papers on a new verification project attempting to extend the usability of the tools to large code-bases. As others have realised, we think linear types are an important step forward (as they alleviate some of the compelxity of reasoning); we have basic (experimental) linear type support built to dafny, and my plan is to extend this support to more of the idioms allowed in rust (thanks to borrowing). Because polonius it’s nicely factored out as a datalog engine, it seems like a prime candidate to attempt the integration.
I realise this may be equal parts(?) interesting and terrifying for peeps in the WG :) The good news is that you’d have another “user”, who’s also happy to contribute diagnostic/other fixes; the “bad" news is that we’re somehow misusing the analysis for a different language.

lqd (Jun 29 2020 at 13:07, on Zulip):

interesting :)

lqd (Jun 29 2020 at 13:07, on Zulip):

dafny seemed nice, even though I also had my eye on why3 and whiley

lqd (Jun 29 2020 at 13:14, on Zulip):

but I need to mention that the analyses in polonius are not finalized yet, it's still a work in progress. maybe focusing on reusing the datalog rules and concepts, more so than the complete implementation itself (which can and will change), could be a "less unstable" basis for your own work

Andrea Lattuada (Jun 29 2020 at 15:09, on Zulip):

Yup! We like dafny for a few reasons, one being that we think it’s more natural for engineers who don’t have a verification background (and, for the same reason, we’ve also been looking at Prusti, the Viper-based verifier for Rust developed at ETH). Thanks for the note. I’m aware that Polonius isn’t finalised, and that’s totally fine by me/us; the final language it would target in our project isn’t well defined yet either. If things diverge, that’s totally okay! (although I have a feeling that some of the things that are still WIP in polonius are for features we don’t need yet, like the interaction with traits). I’ll try to keep a divergent branch orderly, so we can still cherry-pick if there’s anything of use to the “real” polonius. Other reasons I’m experimenting with Polonius: (i) I can write some rust and see what the generated rules look like and (ii) datafrog is neat and I’m already a bit familiar.

Andrea Lattuada (Jun 29 2020 at 15:10, on Zulip):

(Also, please let me know if this is out-of-scope for the wg-polonius stream and I’ll move the communication elsewhere.)

Andrea Lattuada (Jun 29 2020 at 15:14, on Zulip):

Ah, and as a result of today’s experiments, I added a rule to emit errors for partial assignments to moved variables: https://github.com/rust-lang/polonius/compare/master...utaal:partial-move-errors
I believe (correct me if I’m wrong) that these are currently handled by a separate rustc pass. As an example, with this branch you get a partial_move_error fact for

struct Lin { v: u64 }

fn main() {
    let mut a: Lin = Lin { v: 3 };
    take(a);
    a.v = 7; // <- this assignment
}

fn take<V>(_v: V) { }
lqd (Jun 29 2020 at 17:07, on Zulip):

yes move errors are still currently computed and emitted by rustc itself. polonius also computes them but they are not emitted by rustc yet instead of its own computation. (that also means we haven't had a chance to fully debug them yet either)

Andrea Lattuada (Jun 30 2020 at 09:18, on Zulip):

From what I can see, polonius currently computes move errors for points where an uninitialized (moved) path is accessed, but not for points where a path is assigned (like in the example above). The new rule introduced by this https://github.com/rust-lang/polonius/compare/master...utaal:partial-move-errors is an attempt to compute errors for partial assignments to uninitialized variables. Shall I make an Issue/PR for this?

Albin Stjerna (Jul 06 2020 at 17:28, on Zulip):

This sounds super cool! I've been looking at doing stuff with Dafny as well; I'm a PhD student for my day job where I work on string solvers for SMT and applying them for verification

Albin Stjerna (Jul 06 2020 at 17:34, on Zulip):

I would also suggest perhaps using something like Soufflé if you can rather than datafrog; as nice as it is, I believe Soufflé is much more mature

Eh2406 (Jul 06 2020 at 18:11, on Zulip):

Off topic, but what is a string solvers?

Eh2406 (Jul 06 2020 at 18:15, on Zulip):

I know some about SAT and have some idea about how SMT is an extension, but don't know that term.

Eh2406 (Jul 06 2020 at 18:33, on Zulip):

Some googling later, it extends the available data types to include string. That makes sense. I'll let myself out.

c-cube (Jul 06 2020 at 20:39, on Zulip):

It's also crazy hard to solve!
(edit: SMT 2020 just finished today and the invited talk by P. Rümmer was exactly about that: string solving)

lqd (Jul 06 2020 at 20:55, on Zulip):

there was also a talk at pldi recently

Eh2406 (Jul 07 2020 at 01:32, on Zulip):

Links?

Albin Stjerna (Jul 07 2020 at 08:01, on Zulip):

c-cube said:

It's also crazy hard to solve!
(edit: SMT 2020 just finished today and the invited talk by P. Rümmer was exactly about that: string solving)

Philipp Rümmer is my supervisor. :)

Last update: Jun 20 2021 at 00:00UTC