Clearer separation of real and ghost state

[pieter-bos]

(author: @bobismijnnaam)

VerCors does not discern between ghost state and real state. This means real state can be changed from ghost code, and vice versa. This is not an issue, as in practice it is feasible to maintain this separation manually. But, for future reference, below two solutions are documented which can prevent the two types of state from being mixed.

Frama-C solution

Frama-C prevents mixing ghost and real state by tracking the type of state in the type of variables. An int declared in a ghost block is actually of type int \ghost (with the \ghost qualifier listed after the type, similar to how the const qualifier can be listed after the type). If a pointer is taken from such a ghost int, this yields a value of type int \ghost *. By keeping track of the kind of state in the type, mixing of the two kinds of state is prevented. The code snippet below shows an example of referring to both normal pointers and ghost pointers in Frama-C ghost code.

/*@ requires \valid(a);
  @*/
void testGhost(int *a)
{
  /*@ ghost 
    int x;
    int \ghost *ghostPtr;
    int *realPtr;

    ghostPtr = &x;
    ghostPtr = a; // Not ok! Error

    realPtr = &x; // Not ok! Error
    realPtr = a;
     
    @*/
}  

This solution could also be used by VerCors, and seems the most straightforward to implement and explain. A possible drawback of this approach is that ghost methods defined to work over ghost pointers cannot be used on regular pointers, so this might require users to define ghost functions twice in some cases.

Another drawback is that the type system of the language to be checked needs to be changed/extended. For languages that do not have const-like modifiers like Java, it's not immediately clear how the type system has to be extended. But, for a language like Java, maybe generics can be used.

Permission based solution

Since VerCors supports permissions, they could also possibly be used to discern between real and ghost state. For example, VerCors could support a ghost permission and a real permission. A benefit of this is that the type system of the language to be checked does not have to be modified.

A drawback is that still duplicate function definitions are needed for ghost functions that want to operate over both ghost and regular state. Maybe this can be resolved by having some kind of permission that can be both a ghost or regular permission, which disallows writing, and is therefore safe to use in both regular method and ghost method contracts. But this seems like a non-trivial extension of separation logic, and also difficult to encode in Silver.