#array object

Here is a minimal example of allocation/initialization/disposal/freeing of a container object encapsulating an array of other objects. This was my holy grail for the past couple of weeks and I finally have it. I can apply these same annotation forms to my actual project now.

#include <vcc.h> #include <stdlib.h> //malloc typedef struct MyObject { int field; } MyObject; typedef _(dynamic_owns) struct MyObjectArrayContainer { MyObject* arr; size_t size; _(ghost \object arrob) _(invariant arrob == (MyObject[size])arr) _(invariant \malloc_root(arrob)) _(invariant \mine(arrob)) _(invariant \forall size_t i; i < size ==> \mine(arr+i)) } MyObjectArrayContainer; void InitContainer(MyObjectArrayContainer* container) _(writes \extent(container) ) _(ensures \wrapped(container)) _(ensures \unchanged(container->size)) _(requires container->size > 0) { container->arr = malloc(sizeof(MyObject) * container->size); _(assume container->arr != NULL) _(ghost size_t i) _(ghost for (i=0; i<container->size; i++) _(writes \array_members(container->arr,container->size) ) _(invariant \forall size_t j; j >= i && j < container->size ==> \mutable(container->arr+j)) _(invariant \forall size_t j; j < i ==> \wrapped(container->arr+j)) { _(wrap container->arr+i) } ) _(ghost container->\owns = \array_members(container->arr,container->size)) _(ghost container->arrob = (MyObject[container->size])container->arr) _(wrap container->arrob) _(ghost container->\owns += container->arrob) _(wrap container) } void DisposeContainer(MyObjectArrayContainer* container) _(requires \wrapped(container)) _(writes container) _(ensures \extent_mutable(container) ) _(requires container->size > 0) //Optional: //_(ensures \unchanged(container->size)) //_(ensures container->arr == NULL) //_(ensures container->arrob == NULL) { _(unwrap container) _(assert \forall size_t i; i < container->size ==> \wrapped(container->arr+i)) _(ghost size_t i) _(ghost for (i = 0; i < container->size; i++) _(writes \array_members(container->arr,container->size)) _(invariant \forall size_t j; j >= i && j < container->size ==> \wrapped(container->arr+j)) _(invariant \forall size_t j; j < i ==> \mutable(container->arr+j)) { _(unwrap container->arr+i) } ) _(unwrap container->arrob) free(_(MyObject[container->size])container->arr); //Optional: //container->arr = NULL; //_(ghost container->arrob = NULL) } void ObjectArrayContainerMallocAndFree_Methods() { MyObjectArrayContainer cont; MyObjectArrayContainer* container = &cont; container->size = 7; InitContainer(container); DisposeContainer(container); }

In the home stretch of the process of figuring this out, I encountered this new problem:

Almost as soon as submitting my last post here, I think I determined the correct way to annotate the joint unwrapping and freeing of an array of objects.

The post describing my problem: http://vc3d.tumblr.com/post/72817418657/disposing-arrays-of-objects

Working code:

#include <vcc.h> #include <stdlib.h> //malloc typedef struct MyObject { int field; } MyObject; void ObjectArrayMallocAndFree_UnwrapBlock_OK() { MyObject* arr; size_t size = 3; arr = malloc(sizeof(MyObject) * size); _(assume arr != NULL) _(wrap &arr[0]) _(wrap &arr[1]) _(wrap &arr[2]) _(writes \span((MyObject[size])arr) ) _(writes \array_members(arr,size) ) //for the unwraps _(requires \full_context() ) { _(unwrap &arr[0]) _(unwrap &arr[1]) _(unwrap &arr[2]) free(_(MyObject[size])arr); } }

As explored in my last post, \array_members(arr,size) and \extent( (MyObject[size])arr ) seemed to be overlapping. I changed "writes \extent" to "writes \span", and also included \array_members in the writes clause. This verifies, even with smoke testing, so I think it's actually what I want.

I think the array object actually contains "struct fields" of the array elements, so trying to write the \extent of the array object was bringing in the \extent of the array elements too, which didn't jive with their wrapped state, similar to trying to have _(writes \extent(someObject)) and _(requires \wrapped(someObject)) both in a contract at once. See here for more information on that kind of inconsistency: http://vc3d.tumblr.com/post/72017742298/updated-with-explanation-below-i-am-currently

UPDATE: I think I figured this one out. See here: http://vc3d.tumblr.com/post/72820494021/fixed-disposing-arrays-of-objects

I have been trying to verify an object array disposal method which takes an array of wrapped objects, unwraps them, then frees the memory the array used.

I started with this simple example:

#include <vcc.h> #include <stdlib.h> //malloc typedef struct MyObject { int field; } MyObject;void ObjectArrayMallocAndFree_OK() { MyObject* arr; size_t size = 10; arr = malloc(sizeof(MyObject) * size); _(assume arr != NULL) free(_(MyObject[size])arr); }

Then I added on more structure until I have this.

void ObjectArrayMallocAndFree_StillOK() { MyObject* arr; size_t size = 10; arr = malloc(sizeof(MyObject) * size); _(assume arr != NULL) //I would like to do things to the elements here _(writes \extent((MyObject[size])arr)) _(requires \full_context()) { free(_(MyObject[size])arr); } }

Let's say I want to wrap up the array elements and then unwrap them before freeing the array...

void ObjectArrayMallocAndFree_WrapUnwrap_OK() { MyObject* arr; size_t size = 3; arr = malloc(sizeof(MyObject) * size); _(assume arr != NULL) _(wrap &arr[0]) _(wrap &arr[1]) _(wrap &arr[2]) _(unwrap &arr[0]) _(unwrap &arr[1]) _(unwrap &arr[2]) _(writes \extent((MyObject[size])arr)) _(requires \full_context()) { free(_(MyObject[size])arr); } }

Okay... still verifies. What about bunching the unwraps in with the free()?

void ObjectArrayMallocAndFree_UnwrapBlock_FAIL() { MyObject* arr; size_t size = 3; arr = malloc(sizeof(MyObject) * size); _(assume arr != NULL) _(wrap &arr[0]) _(wrap &arr[1]) _(wrap &arr[2]) _(writes \extent((MyObject[size])arr) ) _(writes (MyObject[size])arr ) _(writes \array_members(arr,size) ) //for the unwraps _(requires \full_context() ) //_(requires \malloc_root((MyObject[size])arr) ) //_(requires \forall size_t i; i < size ==> \wrapped(&arr[i])) { _(unwrap &arr[0]) _(unwrap &arr[1]) _(unwrap &arr[2]) free(_(MyObject[size])arr); } }

That doesn't verify. \array_members(arr,size) need to be writable for the unwraps and \extent((MyObject[size])arr) needs to be writable to call free().

Commenting _(writes \extent((MyObject[size])arr)) produces this error: error VC8510: Assertion '\extent(p) is writable in call to free(_(MyObject[size])arr)' did not verify.

But uncommenting it produces this one: error VC8027: writes clause of the block might not be included writes clause of the function.

Since the previous attempt (function ObjectArrayMallocAndFree_StillOK above) only required _(writes \extent((MyObject[size])arr) ) and it verifies fine, I believe that the _(wrap &arr[0]) lines are affecting what the prover thinks are things (the array elements) within \extent((MyObject[size])arr), and so it thinks that parts of \extent((MyObject[size])arr) may not be writable within the nested block, HOWEVER, the VCC Manual says:

If the base type of the array is an object type, the array object has no fields (other than the implicit ones present in all objects), and so is not very useful.

So I would think that the elements of the array are not fields of the object-base-type array object and so not included in \extent((MyObject[size])arr), so I'm not sure why there is this interference.

\extent() is defined like this in the manual, and clearly deals only with "fields" and the object itself:

\objset \extent(\object o) This returns \span(o), along with \extent of any struct fields of o. \objset \span(\object o) The set consisting of o, along with a pointer to each primitive field of o.