This project is read-only.

Hybrid pointers

Sep 21, 2009 at 2:22 PM


last we, we started a discussion about the possibility of calling the same function, once with a physical pointer and once with a specification pointer. While I had been rather positive then, after some more thinking about the problem and discussing it with Michal, I no longer think that this is possible, at least not for functions that write. Here is why:

Assume the function would actually be writing through that pointer, then we either have the situation of spec function writing to physical state, of a physical function being called from spec code, neither of which would be a good idea. Also, the idea of implicitly creating two functions, one for physical and one for spec purposes, does not work properly because we do not know which spec or physical pointers should be effected by such a replacement - a physical function could also require some spec parameters of ghost pointer type and vice versus for a ghost function.

So, it seems that the only proper solution would indeed be two manually create a modified copy of the function in question. Sorry!


Sep 21, 2009 at 2:44 PM

The two-function idea would work under the restriction of not mixing pointer types (i.e., then all pointers would be affected by the replacement), right?


Sep 21, 2009 at 2:51 PM
Edited Sep 21, 2009 at 3:09 PM

Yes it would; we could even do a little bit more: if the function is specified for the spec case, we could derive the physical version by replacing all spec pointers by physical pointers. (Similarly, we could go the other way round and replace all physical pointers with spec pointers). What would not work in this manner is to have both the physical and the spec function take both kinds of parameters.

Yet, such an addition to the language looks to me as a rather arbitrary one, which could also be achieved 'in user space' using a preprocessing script. For this solution to work, we would need to support function overloading in the presence of spec and phyiscal pointers. That would be a general principle that seems to be worth supporting. Maybe that is the way to go.

What do you think?

[Quick update: this kind of overload currently does not work but will be supported soon.]

Sep 22, 2009 at 8:51 AM

Yes, it could work relatively easily with the preprocessor. I still don't know yet if I need any of that., though... Might come back here at a later time :)

Sep 22, 2009 at 3:56 PM

Just to quickly mention that this kind of overloading is now supported.