-
Notifications
You must be signed in to change notification settings - Fork 353
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Adding FFI support to Miri, by emarteca #2365
Comments
Echoing what I said on Zulip:
@maurer replied
|
A new value type would be a Big Deal and is basically not an option. But I also don't think you will need it. We already have different types of memory (data and functions, and we will hopefully have vtables soon). But they are all identified by an The new memory type seems indeed pretty fundamental. I would be interested to see your design there before you spend a lot of effort implementing it. The key challenges I see are:
|
I was thinking we'd extend the
Agreed. So far I haven't touched the rustc internals at all.
Good point -- I'm not sure. I've messed around with this a bit and ran into some problems trying to get it to work. I think it'll depend a lot on how we end up representing the pointers internally (which is currently being discussed on zulip) |
Some suggestions/discussion on pointer representation from zulip: @oli-obk says:
...
|
Looks like the design document moved to https://hackmd.io/eFY7Jyl6QGeGKQlJvBp6pw. (I haven't had the time to look at it yet.) Thanks for putting it on hackmd! |
How will that be enough? Memory kinds only serve to make sure the allocator and deallocator match up. They still all have the same representation in the interpreter, the same
What even is the design space here? Pointers are an absolute address plus a |
Sorry, I should've updated this issue WRT the discussion on zulip. The design doc on hackMD is up-to-date though -- here is the relevant section. The main high-level idea so far (from discussion with @RalfJung,@maurer,@oli-obk, and a few others on zulip, and taken from the design doc): Distinguishing Miri memory from external/foreign memoryIn order to be able to distinguish between foreign memory and Miri memory (i.e., for a given location in memory, determine if it corresponds to C memory or Miri), we propose to reserve a large section of virtual memory for the Miri allocator. This way, we ensure there is no overlap in the memory used by the Miri allocator, and external calls. Using this, we can tell if the memory is Miri internal by looking at its If the return of a C call is a Miri pointer (i.e., if it is contained in the memory range reserved by the Miri allocator), then we will need to handle this case: likely we'll need to create the corresponding Any advice/ideas on this proposed plan are welcome :)
|
I don't understand. When you get data back from C it is an untyped raw bag of bytes. How do you even know whether something in there is a pointer? And when you pass a pointer from Miri to C, how are changes that C is making reflected back on the Miri side? The document says to just pass through the pointer, but that makes no sense to me -- Miri memory carries extra metadata, like which bytes are initialized and pointer provenance. You cannot just give C a pointer to the
What happens when a Miri pointer is written there, what do we do with the provenance metadata? What happens when Miri wants to write uninitialized bytes there? Fundamentally, a 'byte' of memory that we can pass to/from C is just a |
We'll know if a pointer to C memory is directly returned, since the function returning it will have the return type specified as a pointer. You're right though, that we won't know what's in that C memory: the main problem (as I understand it) is that we won't know if that pointer is to memory that contains another pointer to somewhere else in C memory. So a case like:
We've updated the doc with a proposed plan on how to deal with provenance. Thanks for the feedback and for looking at this with us! :) |
We don't know which part of that memory even is a pointer. There could be pointers to other C memory there, or pointers to Miri memory, and we will have no clue. We cannot use the types to guide us because types are allowed to be wrong in C. I plan to remove the
I can't quite figure out what you are even proposing here, sorry. It seems to zoom in on a tiny aspect of the problem when you haven't sketched out the larger architecture of the approach yet.
void print(int *x) { printf("%d\n", *x); }
void print2(int **x) { printf("%d\n", **x); }
void set(int *x, int val) { *x = val; }
void set2(int **x, int val) { **x = val; }
void setptr(int **x, int *val) { *x = val; }
void setptr2(int ***x, int *val) { **x = val; } None of these even involve C creating any new allocations. Let's first solve the "simpler" cases. :) Please start with the first case and describe in detail what exactly happens: given the I don't think you will need a "sync list", and Miri already contains what is basically an implementation of PNVI-ae-udi. I don't quite understand which problem that part of the proposal solves, but it seems too complicated on the one hand while also not talking about the real issue I am seeing on the other hand.^^ Mainly, what exactly does the pointer given to C even point to, and how does Miri prepare that memory so that when C does reads and writes, it all makes sense?
I think wildcard provenance is indeed the key -- it's not just similar to wildcard provenance, it's the same thing! (So indeed, having both FFI support for pointers and strict provenance will just not work.) |
This project isn't moving forward any more, so I will close this issue and open a new one instead to track just having more FFI support: #3491. |
I should also say thanks a lot to @emarteca and @maurer for the initial work here, this was great to get us started. :) Once the initial support via libffi is in place, it's much easier for me to extend that support -- now it's mostly "just" regular Miri programming, as most of the dark FFI magic is done. I hope. ;) |
This issue is specifically tracking the effort by @emarteca and @maurer to add FFI support to Miri. There's a design document here, but it does not go into a ton of the actual implementation details.
The text was updated successfully, but these errors were encountered: