Invariants for global variables

Nov 30, 2012 at 12:24 PM

Hi,

I'm considering is it possible to state the invariants for global variables? Which may specify the properties for the variables like in structure.

And if I have a field in a struct, is that possible for me to bind it to a field in another struct? For example in following code. I have a struct T and I'd like to specify that the value of s_val[t] is equal to t->val? And also is that possible to say that s_sortedarr[] is sorted with invariant?

typedef struct T{
  unsigned val;
}T;

T *px;

_(ghost struct {
  // other fields of the struct
  unsigned s_val[T*];
  unsigned s_sortedarr[];
};)

Thanks very much!

Shu Cheng

Developer
Dec 5, 2012 at 1:24 PM

Hi Shu,

- If you want to add an invariant constraining the nonvolatile fields of a particular object such as px of some type, you put those invariants in another object that knows that px is closed (typically because it transitively owns px).

- Global variables of primitive types are fields of anonymous global objects (one per variable, obtainable through \embedding()). Thus, if you want to talk about fields of *px, you want to own both \embedding(&px) (the object that owns the variable px) and px (the T that px points to). The natural choice in your example is the global ghost object (lets call it s).

- Before using these globals, they have to be initialized and wrapped up. This requires someone to start out with ownership of them; the only place to "get" this ownership is at program entry.

Here is a solution putting these together:

typedef struct T{
  unsigned val;
}T;

T *px;

_(ghost struct {
  // other fields of the struct
  unsigned s_val[T*];
  unsigned s_sortedarr[];
  _(invariant \mine(\embedding(&px)))
  _(invariant \mine(px))
  _(invariant px->val == s_val[px])
} s;)

void main() 
  _(requires \program_entry_point())
  _(writes &px, \embedding(&px), \extent(&s))
{
	px = malloc(sizeof(T));
	_(assume px)
	px->val = 0;
	_(wrap px)
	_(wrap \embedding(&px))
	_(ghost s.s_val = \lambda T *t; (unsigned) 0)
	_(wrap &s)
	// invariants established - start using s/px
}

Hope this helps,

ernie

 

 

Dec 7, 2012 at 2:33 PM

Hi Ernie,

This is quite helpful for me. Thanks very much!!