This project is read-only.

Distinguishing physical and ghost pointers

Aug 6, 2009 at 12:54 PM
Edited Aug 6, 2009 at 12:56 PM

Currently, we do not distinguish between physical and ghost pointers. This leads to soundness problems where spec code could change physical locations (by writing through a ghost pointer to a physical location). Clearly, we cannot disable writing through pointers in spec code entirely, so we need to find a way to deal prevent the write to physical memory only.

Additionally, we need support for arbitrary convertability between 64bit integers and physical pointers, which we currently don't.

Yesterday, we had discussed the idea of using type of the object being pointed to as the indicated for physical or ghost. Pointers to spec types would be ghost pointers and any other pointer would be to physical memory. This leads to a number of problems: we cannot have ghost pointers to primitive types (including other pointers) or untyped ghost pointers. Maybe even more importantly, it is unclear how to deal with direct pointers to physical structures embedded into spec structs. They would point to a non-spec type but to ghost memory - not a good solution.

Alternatively I would prefer the following solution: we annotate each pointer type explicitly to be either physical or ghosts. For physical pointers, we do not need to do anything. For ghost pointers, we use a special syntax:

spec(T ^x;)

This declares a local, parameter, or field x that points to an instance of T that has been allocated on the ghost heap. Dereferencing x is still done using the '*' and '->' operators. When the 'spec' is apparent from the context, e.g., inside of spec functions or types, we do not need to surround the declaration of x with an extra 'spec'.

In terms of convertability, the types T^ and T* are different and assignment between these is suppressed by the compiler; so is casting between ghost and physical pointers. Additionally, we could introduce Boogie predicates $physical and $ghost for pointers and generate the corresponding proof obligations that all assignments are safe.



Aug 6, 2009 at 4:01 PM

For consistency, we will need that applying &p->f on ghost pointer p gives us a ghost pointer. Also it would likely make sense to make T* into T^ automatically, when T is a ghost-only type (like ListManager or record types). This would make the usage of ^ rather scarce, which I guess is a good thing.


Aug 6, 2009 at 6:48 PM

Not only does &p->f for a ghost pointer give a ghost pointer. The same holds for &p->f for a physical pointer p and a spec field f; similarly, &a for a spec local a and &p for a spec parameter p. I think this should be all the cases.

I am not sure if we should infer the '^' when pointing to a spec type -  making this information explicit could make the code actually more readable, even if it means more changes to existing annotations initially.

Aug 7, 2009 at 10:30 AM

I have just come across one complication: obj_t needs to be compatible with both physical and ghost objects; otherwise, we could not put them into an owns-set or define the contracts of a lock to be generic enough. That, of course, means that we cannot purely rely on the type system to enforce the separation of ghost and physical heap. We will have to generate proof obligations at for any cast to a pointer type. Also, we will need to define predicates that allow to talk about physical-ness or ghost-ness of pointers.