#vc3d

Given what I figured out in yesterday's post about hints, I have fixed the memory use problem I had before while checking my Mesh invariant for admissibility.

I think I finally understand where VCC Hints can be used.

Here is some example code. It is like the PairedList code I posted before, but now has internal arrays which are only partially used, and the use of witnesses has been removed. The important parts are the ownership invariants and the in_array invariants.

#include <vcc.h> #include <stdlib.h> //malloc typedef struct Paired Paired; typedef struct Paired { Paired* pair; } Paired; typedef _(dynamic_owns) struct PairedVarLists { //Used size of the arrays size_t num1; size_t num2; //Maximum sizes of the arrays size_t cap1; size_t cap2; //Size invariants _(invariant num1 <= cap1) _(invariant num2 <= cap2) _(invariant cap1 > 0) _(invariant cap2 > 0) //Arrays storing Paired objects Paired* pairarray1; Paired* pairarray2; //Require that the arrays do not overlap _(invariant pairarray1 != pairarray2) _(invariant \arrays_disjoint(pairarray1, cap1, pairarray2, cap2)) //Array objects (needed for free/dispose) _(ghost \object arrayob1) _(ghost \object arrayob2) //Array object invariants _(invariant arrayob1 == (Paired[cap1])pairarray1) _(invariant arrayob2 == (Paired[cap2])pairarray2) _(invariant \malloc_root(arrayob1)) _(invariant \malloc_root(arrayob2)) _(invariant \mine(arrayob1) && \mine(arrayob2)) //Ownership invariants _(invariant \forall \natural i; {&pairarray1[i]} i < cap1 ==> \mine(&pairarray1[i]) ) _(invariant \forall \natural j; {&pairarray2[j]} j < cap2 ==> \mine(&pairarray2[j]) ) //in_array invariants //Note that either the :hints or the \mine()s are needed _(invariant \forall \natural i; {:hint \mine(&pairarray1[i])} i < num1 ==> //\mine(&pairarray1[i]) && \in_array(pairarray1[i].pair, pairarray2, num2) ) _(invariant \forall \natural j; {:hint \mine(&pairarray2[j])} j < num2 ==> //\mine(&pairarray2[j]) && \in_array(pairarray2[j].pair, pairarray1, num1) ) //Pairing invariants (paired structure) //...omitted } PairedVarLists;

Either the "{:hint \mine(&pairarray1[i])}" hints or the "\mine(&pairarray1[i])" parts of the in_array invariants are needed. The hints hearken to the ownership invariants, while the "\mine"s introduce the ownership information again in a redundant way. In this case, the \mine versions let the admissibility check succeed faster. If both are omitted, the admissibility check fails by running out of memory.

I am having a lot of trouble right now keeping the mesh admissibility check from running out of memory. The invariants are all good, but there are some particular ways of organizing them which cause memory issues. I have been trying to separate parts of large invariants into smaller ones (and vice versa) by changing conjunctions, but can't get it all to operate correctly when it comes to using the Mesh structure in actual code. I have to guide the proofs with assertions in the code because if I try to make the invariants more useful to VCC, the admissibility check runs out of memory before it can succeed.

Here is my stepping-stone up to verification of the actual project code. This structure stores two lists of "Paired" objects which each has a pointer and its invariants require that the pointers of items in one list point to items in the other list in corresponding pairs... a simple mesh-like structure.

The last thing I figured out here was the necessity of the \arrays_disjoint invariant and the invariant ensuring that the array object aliases aren't identical.

There remain a couple of assertions in the dispose function and I'm not sure why they are required.

Code:

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:

I posted yesterday, confused about working with arrays of objects. The post can be found here: http://vc3d.tumblr.com/post/72590187480/arrays-of-objects

I posted a discussion thread on the VCC site here: https://vcc.codeplex.com/discussions/484017

I think I may have figured it out. I took a look through the VCC source and see that \array_range corresponds with $array_range which mentions $array_range_no_state which, for non-primitives, branches to a use of $full_extent. So, is it that \array_range (for objects / structs) is like the following?

\objset \array_range(\object o, size_t s) The set of the extents of all objects o+i where size_t i < s.

Also in the source I see \array_members, corresponding with $array_members, which only mentions $in_array and not any extent. When I replace \array_range with \array_members in my last function, it verifies (well, after removing the _(assert \false), and it does trip that now so the contract must be consistent) and seems to behave how I want it to there.

//Dispose a MyObject array with size 2 void MyObjectArrayDispose_2(MyObject** test) _(requires \forall size_t i; i < 2 ==> \wrapped(&(*test)[i]) ) //conflicts with writes arrayrange _(requires \wrapped((MyObject[2])(*test)) ) _(requires \malloc_root((MyObject[2])(*test)) ) _(writes (MyObject[2])(*test) ) _(writes test) //_(writes &(*test)[0]) //_(writes &(*test)[1]) //Use this instead: _(writes \array_members(*test,2)) { _(unwrap *test+0) _(unwrap &(*test)[1]) //Make arrayobject writable. This shows VCC that the free() below is okay _(unwrap (MyObject[2])(*test) ) free((void*) speccast(MyObject[2], (*test))); }

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.

I have been trying to sort through the task of verifying C code (using VCC) which allocates heap memory.

First, I tried naively using objects created via malloc(). I found that you must consider the possibility that malloc returns NULL because of some problem allocating enough room for the structure. This yields errors like "error VC8020: 'dis->verts' is not writable before wrapping it." because of the chance that dis->verts was just set to NULL rather than to a valid writable portion of memory. I temporarily worked around this by _(assume pointer != NULL) following calls to malloc(), but this is not a solution. However, it is enough for the code to verify in most circumstances and reflects my usual lack of concern for program stability when memory is exhausted.

I next found that malloc behaves oddly if you pass it a 0 argument. In this case malloc does not necessarily return NULL, but yet the address it returns may still not be mutable nor writable. It is not enough to _(assume ) that the pointer is not NULL.

error VC8020: 'dis->edges' is not writable before wrapping it. error VC9502: Call 'wrap dis->edges' did not verify. error VC9599: (related information) Precondition: 'the object being wrapped is mutable'.