search

rust-lang / miri

An interpreter for Rust's mid-level intermediate representation
Apache License 2.0
4.17k stars 320 forks source link

Extend FFI support: passing pointers to and from C #3491

Open RalfJung opened 2 months ago

RalfJung commented 2 months ago

Currently only integers can be passed around; for most real APIs, support for pointers is needed.

Current status: I have a Bachelor student working on this.

pauladam94 commented 1 month ago

Currently only integers can be passed around; for most real APIs, support for pointers is needed.

Current status: I have a Bachelor student working on this.

I am working with Marco Vassena in Utrecht (Netherlands) about formalization of such C Rust FFI. Is there any way to get in touch with this student just to share ideas ?

RalfJung commented 1 month ago

We're very far away from any kind of formalization, so TBH I don't think that would make a lot of sense. I think the formal behavior should be quite different than what we'll have in Miri, but Miri can't implement angelic choice so we have to do some sort of approximation.