Extend FFI support: passing pointers to and from C

[RalfJung]

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]

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]

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.

[RalfJung]

Turns out we have a very old issue to track native FFI support, so closing in favor of #11.

[nevakrien]

I have found a place where this matters in pure rust code.

if you write pointers onto some buffer then read them as raw u8 miri will not realize you are in fact reading the same pointer

#[test]
fn test_push_pop_valid_pointer() {
    let mut stack = Stack::with_capacity(100);

    // Create some random data on the heap
    let value = Box::new(12345);
    let ptr = Box::into_raw(value);

    stack.push_grow(&Aligned::new(ptr));
    let p :*const usize= unsafe{stack.pop().unwrap().to_inner()};
    assert_eq!(p,ptr); //same pointer

    unsafe{assert_eq!(12345,*ptr)};//miri happy
    unsafe{assert_eq!(12345,*p)};//miri angry
}

[saethlin]

That is off-topic for this issue.

What you have is almost certainly just a bug in that Stack implementation. It's probably using typed copies where the type doesn't carry provenance, and it should be using an untyped copy. You should be able to demonstrate pretty easily that the problem is not reading and writing pointers to memory; putting them in a Vec works just fine.

Pointer equality compares address only, not provenance. So your // same pointer comment is misleading.

[RalfJung]

Reading a pointer as raw u8 loses its provenance so what you describe sounds like expected behavior Ptr-to-int transmutation is not the same as ptr-to-int cast.

Anyway, your example uses a bunch of types that are not defined, so it's completely unclear what happens. If you think there is a Miri bug, please file a new issue and provide a self-contained example.