Story for unsafe Rust?

[Pat-Lafon]

Hello! Very cool work. I was looking around this project(at both your documentation and the arxiv paper https://arxiv.org/pdf/2207.04034.pdf) and was wondering about the story here with unsafe Rust? I understand the array bounds-checking side of things but I was wondering how much further this can/could go?

In particular, I was thinking about trying to encode the specifications of unsafe calls around ffi and then have flux check that my use is safe(or that I safely encapsulate the unsafe ffi call)? I've been trying to draw connections between this work and work from my group which I think would be pretty cool https://www.cs.purdue.edu/homes/bendy/SpecInfer/Elrond.pdf.

(Brought about by my recent ventures into modifying code with a rust-c ffi).

[ranjitjhala]

Hi @Pat-Lafon -- that's a great question and something we're actively thinking about right now, e.g. see this:

https://goto.ucsd.edu/~rjhala/hotos-ffi.pdf

Would be great if you can show us some examples of what you're doing to see how flux might be used there!

[Pat-Lafon]

https://goto.ucsd.edu/~rjhala/hotos-ffi.pdf

Wow! This was basically what I was wondering about. Great to see this kind of work being done.

Would be great if you can show us some examples of what you're doing to see how flux might be used there!

I think my interests are squarely around Section 2.4 "Glue Code". My particular example was that of Rust's Z3 bindings, some of the calls to c are allowed/expected to return a null pointer(which would be a great thing to have represented in the type system) a la For example, we can use the refinement type {ptr: *mut T | not_null(ptr)}. I could imagine other examples around only allowing inputs that are bounded such that they won't trigger an overflow on the c side(wondering about integer arithmetic overflows being undefined in c but not in Rust).

So in terms of this work, I guess one could annotate some of return pointers with ensures non_null(v) and then all the input pointers will have requires non_null(ptr). Is that correct? I think I'm assuming that ensures here is inserting this non_null check.

Thanks! All of this gives me something to think about in terms of inferring these specifications.