Type information

Sep 11, 2012 at 12:51 PM

Hi, 

Are there any VCC features for asserting/inferring types?

For instance, if I had 

int a = ...;

void* b = &a;

can I assert anything regarding the type (int) of the data/memory "b" points to ("a") ? 

I am guessing there is no support for this kind of thing, right? 

 

Thanks,
Eduardo 

Developer
Sep 11, 2012 at 2:40 PM
Edited Sep 11, 2012 at 2:46 PM

The answer is yes and no.

The fundamental problem is that there is no such thing as "the" object that b points to, because it points to many objects (of different types, but only at most one of any type). Most of these objects are not valid, but there might even be multiple valid objects with the same address. For example, if b was assigned the address of an int that happened to be the first element of struct, that struct (which could very well be valid) also has the same address. If that struct was the first member of a containing struct, the containing struct would likewise have the same address, and so on. This is just a fact of life in the C memory model.

However, if b is a pointer to a field of primitive type, there is indeed at most one valid object (in any state) of which b is a field. (In your example above, where a is a local variable, this object is an artificial object introduced by VCC, which can be accessed as \embedding(&a).)

In VCC, each pointer carries its type, and (if it is not a pointer to an object) its embedding. In an assertion, == between pointers means that they agree non only on their address but also on their types (and their embeddings, if they are not pointers to objects). So you can assert that b points to an int field of a valid object with the assertion

_(assert \embedding((int *) b)->\valid)

Because fields of valid objects don't alias, the type of pointer (to a primitive) to which b could be cast to make this succeed is unique. So this is perhaps what you mean by "the" type of object to which b points. 

There are also stronger statements that you could make in your example, which imply the typing above without explicitly going through \embedding, and which perhaps correspond more closely to what you need, e.g. 

_(assert \mutable((int *) b))

_(assert \thread_local((int *) b))

Hope this helps; if not, please feel free to follow up. 

cheers, ernie

 

Sep 11, 2012 at 10:39 PM

Thanks a lot ... this seems to suit my purpose. I'll try it. 

Cheers

Eduardo

Sep 12, 2012 at 11:19 PM

Ok I tried it even on arrays and it works. Consider

int a[10];

 void* b = a;
  _(assert \thread_local_array((int*) b, 10)) 

_(assert \thread_local_array((char*) b, 1)) 

_(assert \thread_local_array((char*) b, 40))

 

Only the first assertion holds when executing vcc, so I conclude that the type information is honored, and C "dirty casts" don't get in the way. 

Right? Or maybe this might fail in some other case ... and somehow vcc could conclude that b points at something that has no int type?

Given the "liberty" allowed by C casts "a" could in fact be seen as an array of char of size 40 (in C, but not at the level of VCC as I hope) 

I just want to be sure ...

Thanks,

Eduardo

 

 

 

 

 

Developer
Sep 13, 2012 at 12:00 AM

Note, \thread_local_array((int *) b,10) just means \thread_local((int *) b) && \thread_local(((int *) b) + 1) && .. \thread_local(((int *) b) + 9). So for example, \thread_local_array((int *) b, 2) would also succeed.

 

 

But getting to the char vs int thing, you are right, VCC will not allow you to access an int through a char pointer. We actually should provide a way to verify code that does it by means of an explicit construction (memory reinterpretation without invalidating objects on the heap), but it hasn’t been a high priority.

 

Cheers, ernie