out_param() versus weak_out_param()

Coordinator
Aug 27, 2009 at 2:26 PM
Edited Aug 31, 2009 at 7:43 PM

Currently vccp.h defines

#define out_param(p) \
  writes(p) \
  maintains(mutable(p) && is_object_root(p))

#define weak_out_param(p) \
  writes(p) \
  ensures(mutable(p) && unchanged(emb(p)))

 

which are both meant to be used to mark call-by-reference parameters. According to my experience, specifying function contracts with out_param() is not advisable because some day some client code walks in that can only guarantee weak_out_param(), which will require to revisit already verified code.

So, to me it would make sense to define

 

#define strong_out_param(p) \
  writes(p) \
  maintains(mutable(p) && is_object_root(p))

#define out_param(p) \
  writes(p) \
  ensures(mutable(p) && unchanged(emb(p)))

 

or even delete the first variant altogether.

Does somebody have any good cases / examples where (according to the current definitions) out_param() is required over weak_out_param()? Is it a performance issue?

Another, unrelated question / comment is that both definitions are currently not suitable for pointers to pointers to non-primitive type (i.e. int* versus struct S *). To support that we need extent_mutable() in contrast to just mutable(). However, since extent_mutable() doesn't currently work for primitive types (a) a second set of definitions would be required or (b) we should also provide extent_mutable() for primitive (cf. similar to extent_zero(), which we also need for primitive types). I would prefer (b) but don't know whether this might have performance implications.

Thoughts? Comments?

[Update: only pointers are involved, corrected "int** versus struct S **" above to "int* versus struct S *"]

 

Coordinator
Aug 31, 2009 at 6:47 PM

Replying to myself: the unrelated question is actually bogus, please ignore that (we are talking about a mutability of a T** here, not mutability of a T*).

Coordinator
Aug 31, 2009 at 7:45 PM

So, the second comment was bogus. The suggestion for the non-primitive types (with arbitrary nesting) would be

#define out_param(p) \
  writes(extent(p)) \
  ensures(extent_mutable(p) && unchanged(emb(p)))
and we would need extent() and extent_mutable() work for primitives.

Coordinator
Sep 1, 2009 at 9:11 AM

I think we should change that, unless it introduces some severe problems.