Abstract typedefs

Editor
Oct 11, 2010 at 2:09 PM

Hi all,

There is in C some support for hiding of implementation and abstract interfaces at the source level, in the form of unary typedefs, that basically force the user of the library to use the provided API. From a verification point of view, this kind of feature would be a huge bonus if used properly. However, VCC's parser seems to choke on unary typedefs.

One solution is to replace the unary typedef with a type aliasing to void (i.e. "typedef myAbstractType" becomes "typedef void myAbstractType"), but this causes other issues:
1) the unary typedef tells the compiler to only allow manipulation of pointers to the type (because the size of objects of that type is unknown),
2) something one would expect when verifying the use of a library using such abstractions is that casts to and from abstract types are forbidden.

Number 2 above is the real issue: because the type is abstracted away, the data invariants are also hidden. In particular, if I have an abstract type AT1, and an abstract type AT2, I would like any cast from AT1 to AT2 to be invalid, as AT1's implementation's invariants may be incompatible with those of AT2's implementation, and allowing such a cast is highly unsound. This unsoundness also exists when casting pointers around (which you would have to do in order for it to compile, anyway): if I have a pointer to an object of type AT1 that is wrapped, and I cast it to a pointer to an object of type AT2, I would like VCC to complain loudly at me, which it obviously doesn't do if both types are simply explicit aliases for void...

So I would like to know several things here. Do you have any plans for supporting this, or even any use for it in your current verification effort(s)? If you are not planning on supporting this, but have a use for it already, what kind of side argument do you make to prove the soundness of code that uses your library? And finally, how much trouble do you think it would be to add some support for this into VCC? I can have a stab at it, but I'd rather only do it once I'm aware of *all* the soundness issues, and not just the ones I happened to notice at first glance.

Cheers,
Francois

Coordinator
Oct 11, 2010 at 5:54 PM

It seems like a nice feature to have. If you translate them by leaving invariants and size undefined there should be no soundness issues. You will be able to cast around (as you always are in VCC), but you won’t be able to prove the result is typed let alone wrapped.

While nice, it does not bring any new expressive power: you can get a similar effect by including an uninterpreted function in the invariant, and only giving it definition in the implementation file.

Michal

Editor
Oct 11, 2010 at 6:25 PM

Thanks Michal. I ended up replacing the "void" with a "struct {}" in the typedef. This creates a fresh, anonymous, empty struct for every abstract type declaration and seems to achieve the desired effect (namely, preventing the casting of a wrapped abstract object to one of another type), at least temporarily, until I can make a patch for VCC.

I will also try and think about what kind of soundness statement we can make when dealing with such an abstract interface, especially in the presence of more complex function contracts.

Cheers,
Francois