Array Objects and _(dynamic_owns)
I just finally got some of my Mesh object invariants and code to verify!
A few weeks ago while working on this, I decided to take a step back to look carefully at the SafeString and SafeContainer objects in the VCC tutorial document (found here). This helped, but I wound up confusing myself over the syntax and meaning of so-called "array objects."
In SafeContainer's struct definition:
struct SafeString **strings; unsigned len; _(invariant \mine((struct SafeString*[len])strings))
In code initializing a SafeContainer before wrapping it:
_(ghost a->\owns += (SafeString[a->len])a->strings; )
Note that SafeContainer's "strings" field is meant to point to an array of pointers to SafeStrings, not an array of SafeStrings. My Mesh object contains arrays of other objects, not pointers to other objects. While SafeContainer's array of pointers (pointers are not "first class objects" as described in the tutorial) needs to be wrapped into an array object and the array object added to SafeContainer's \owns set explicitly, my Mesh object's arrays are made of first class objects which can be directly added to Mesh's \owns set. No encompassing array object is needed, though I have tried adding the appropriate invariant and \owns+= operations and it does not seem to hurt.
My largest mistake was assuming that if I wrapped and managed ownership of an array object encompassing an array of first class objects, that VCC would take that as a shortcut for wrapping and adding the individual objects within, but this seems not to be the case. I must explicitly add and wrap all individual objects within my arrays (and in fact, the array objects are not even required). The assumption I made has had me running in circles for weeks.
Copied here is a sort of simplified toy version of my Mesh class which I used to figure out what was wrong, but without so much clutter. The PairLists object contains two lists of Pair objects and the invariant specifies that all Pair objects in the first list should point their "pair" member pointers at other Pair objects which point back to the objects in the first list... they should each have a symmetric pair. The initialization function builds a valid PairLists object, storing the pairs for the first list into the second list. Note that I have no invariant on the second list, so it may contain arbitrary elements. See my comments for additional notes.
#include <vcc.h> #include <stdlib.h> //malloc typedef unsigned int uint; typedef struct Pair Pair; typedef struct Pair { Pair* pair; } Pair; typedef _(dynamic_owns) struct PairLists { uint num1; uint num2; Pair* pairarray1; Pair* pairarray2; //OWNERSHIP //THESE DO NOT HELP HERE //_(invariant \mine( (Pair[num1]) pairarray1) ) //_(invariant \mine( (Pair[num2]) pairarray2) ) //These invariants on ownership, when uncommented, help see whether the ownership or pair condition portion of the following invariant is failing when it fails. //_(invariant \forall uint i; // i < num1 // ==> // \mine(&pairarray1[i]) //) //_(invariant \forall uint i; // i < num2 // ==> // \mine(&pairarray2[i]) //) _(invariant \forall uint i; i < num1 ==> \mine(&pairarray1[i]) && \mine(pairarray1[i].pair) && \mine(pairarray1[i].pair->pair) && pairarray1[i].pair->pair == &pairarray1[i] //pair's pair points back to pair ) } PairLists; void PairListInit(PairLists* dis) _(writes \extent(dis)) _(ensures \wrapped(dis)) { _(ghost dis->\owns = {};) dis->num1 = 2; dis->num2 = 2; dis->pairarray1 = malloc(dis->num1*sizeof(Pair)); dis->pairarray2 = malloc(dis->num2*sizeof(Pair)); //Ignore malloc failure for the sake of testing the rest of this stuff concisely _(assume dis->pairarray1 != NULL) _(assume dis->pairarray2 != NULL) //Initialize the pairs //If any of these following few lines are removed, the PairLists's pairing invariant is not satisfied. Comment any of these to test that the invariant is working correctly. dis->pairarray1[0].pair = &dis->pairarray2[0]; dis->pairarray2[0].pair = &dis->pairarray1[0]; dis->pairarray1[1].pair = &dis->pairarray2[1]; dis->pairarray2[1].pair = &dis->pairarray1[1]; //Set \owns //THESE DO NOT HELP HERE //_(ghost dis->\owns += (Pair[dis->num1])dis->pairarray1;) //_(ghost dis->\owns += (Pair[dis->num2])dis->pairarray2;) _(ghost dis->\owns += &dis->pairarray1[0];) _(ghost dis->\owns += &dis->pairarray1[1];) _(ghost dis->\owns += &dis->pairarray2[0];) _(ghost dis->\owns += &dis->pairarray2[1];) //THESE DO NOT HELP HERE //_(wrap (Pair[dis->num1])dis->pairarray1) //_(wrap (Pair[dis->num2])dis->pairarray2) _(wrap &dis->pairarray1[0];) _(wrap &dis->pairarray1[1];) _(wrap &dis->pairarray2[0];) _(wrap &dis->pairarray2[1];) _(wrap dis) }