Verified C 3D

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.

This one had me stumped:

Code sample with explanation below:

#include <vcc.h> #include <stdlib.h> typedef struct MyObject { int field; } MyObject; typedef _(dynamic_owns) struct SimpleTestWithArray1 { MyObject* arr; size_t size; //Bad: second invariant cannot be shown to be admissible by default (though it is) //_(invariant \forall size_t i; i < size ==> \mine(&arr[i])) //_(invariant \forall size_t i; i < size ==> arr[i].field == 0) //Alternative: put all such invariants under one \forall //_(invariant \forall size_t i; i < size ==> \mine(arr+i) && arr[i].field == 0) //Optimal solution: //The problem with the first approach is that the first invariant triggers on \mine(arr+i) //It needs to trigger on arr+i in order for it to be available while VCC attempts to //convince itself that the second invariant (which mentions arr+i and not \mine(arr+i) //is admissible _(invariant \forall size_t i; {arr+i} i < size ==> \mine(&arr[i])) _(invariant \forall size_t i; i < size ==> arr[i].field == 0) } SimpleTestWithArray1;

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:

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.

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))); }

FIX HERE: http://vc3d.tumblr.com/post/72677614116/fixed-arrays-of-objects

I am currently confused about why this verifies without complaint. I believe the function should fail to maintain the invariant, though I might not be understanding _(inline) or something else correctly.

#include <vcc.h> typedef struct MyObject { size_t val; } MyObject; typedef struct MyObjectUser { _(inline) MyObject obj; _(invariant obj.val == 15) } MyObjectUser; void TestFunction(MyObjectUser* objuser) _(maintains \wrapped(objuser)) _(writes \extent(objuser)) { //Break the invariant? _(unwrapping objuser) { objuser->obj.val = 10; } }

Will update with an answer...

UPDATE! Okay, it seems this issue is caused by _(writes \extent(objuser)). I think that using \extent or \span when they are not needed in the writes clause, when there is also a _(maintains \wrapped(...)) annotation creates an inconsistency: If the object is \wrapped, its fields are unwritable at function entry, but the writes clause indicates that the object's extent or span is \writable.

The solution in this case is to change _(writes \extent(objuser)) to _(writes objuser).

The way to detect the problem is to ensure that there is some other function calling TestFunction. It will be impossible to satisfy the guarantees of the the function upon invoking it, which will show up in VCC output. In this case, the error looks like this:

Verification of TestFunctionTest failed. [0.14] ...\test4.h(31,3) : error VC8510: Assertion '\extent(objuser) is writable in call to TestFunction(&aoeu)' did not verify. Verification errors in 1 function(s) Exiting with 3 (1 error(s).) === Verification failed. ===

In this way, VCC still ensures that bad executable code will not verify... even if TestFunction violates the object's invariants before wrapping it back up and appears to verify on its own, if the programmer attempts to use TestFunction, the code will not verify.

An alternative way to detect the issue is to run VCC with the /smoke option. It will print a warning like this:

I just added SyntaxHighlighter to this blog to render code snippets in a much nicer manner!

SyntaxHighlighter can be found here: http://alexgorbatchev.com/SyntaxHighlighter/

I added custom keyword and function entries to the C/C++ highlighting scheme ("brush") and added "vcc" as another brush alias. My custom shBrushCpp.js can be found here. I am probably missing many keywords, but anything that ever appears on this blog will be added as I go along and it should be clear enough how to add more yourself.

See http://alexgorbatchev.com/SyntaxHighlighter/manual/installation.html for script installation instructions. I provide further Tumblr-specific guidance below:

To add the required Javascript and CSS files to your blog, go to your blog on the Dashboard, then click the Customize link on the right side of the Dashboard. Then, on the Theme edit/preview page, click "Edit HTML".  Put the script and stylesheet code into the <head> part of the page.

Mine are like these:

<script src="MYWEBSITEURL/syntaxhighlighter/shCore.js"></script> <script src="MYWEBSITEURL/syntaxhighlighter/shBrushCpp.js"></script> <script src="MYWEBSITEURL/syntaxhighlighter/shBrushPlain.js"></script> <script src="MYWEBSITEURL/syntaxhighlighter/shBrushJScript.js"></script> <script src="MYWEBSITEURL/syntaxhighlighter/shBrushXml.js"></script> <link rel="stylesheet" href="MYWEBSITEURL/syntaxhighlighter/shCore.css" type="text/css"> <link rel="stylesheet" href="MYWEBSITEURL/syntaxhighlighter/shThemeDefault.css" type="text/css">

Then, put the scripted call to SyntaxHighlighter.all() toward the bottom of your Tumblr HTML, below the Posts section and above the </body> tag.

Like this:

<script type="text/javascript"> SyntaxHighlighter.all(); </script> </body> </html>

I also put a call to SyntaxHighlighter.all() in the Infinite Scroll feature's code, but I don't have that enabled on my Tumblr settings so I haven't actually tested if it's needed or if it works. I put it here:

if ((_posts_loaded > 0) && (_current_page < _total_pages)) { set_trigger(); //Added for syntax highlighting on infinite scroll SyntaxHighlighter.all(); _is_loading = false; } else { disable_scroll(); }

Finally, When making a Tumblr post with code, it must be marked like this:

<pre class="brush: vcc"> //example code int len = 0; _(invariant len > 0) </pre>

which produces:

//example code int len = 0; _(invariant len > 0)

The code should have all >, <, and & characters converted to > < and & sequences, though it seems that Tumblr is willing to accept code with only the ampersands changed so long as none of the < and > characters form HTML tags like <p> or <br> or even (!) similar <vcc.h>, <stdlib.h>, etc.. An easy way to convert these characters in your code is to copy-paste your code into Tumblr's WYSIWYG editor, then click the <html> button in the text editor's toolbar to go into HTML code mode. It should have converted all of those characters for you, so all you have to do is delete the <br> line breaks and then wrap the resulting code in the <pre> tags as shown above.

Here's one I haven't seen before...

=== VCC started. === Command Line: "C:\Program Files (x86)\Microsoft Research\Vcc\Binaries\vcc.exe" /bvd "mesh.c" /p:/DWIN32 /p:/D_DEBUG /p:/D_CONSOLE /p:/D_UNICODE /p:/DUNICODE /clpath:"C:\PROGRAM FILES (X86)\MICROSOFT VISUAL STUDIO 10.0\VC\bin\cl.exe" Value was either too large or too small for a UInt32. Exiting with 3 (1 error(s).) === Verification failed. ===

Which value?! The code compiles and everything!

EDIT! Here was the culprit:

dis->faces[1].edge = &dis->edges[3]; dis->faces[1].normal = Vec3GenVec3(0,0,-1);

Vec3GenVec3 takes 3 floats, so it's still a little curious, but if I change the -1 to anything positive, it is fine.

If I try to specify that it is a float, like by using "-1.0f", it tells me:

(0,0) : error : invalid type for argument 0 in application of $sub_f4: int (expected: $primitive) attempting to dump BPL to buggy.bpl Access to the path 'c:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\buggy.bpl' is denied. Exiting with 3 (2 error(s).) === Verification failed. ===

However, "1.0f" (positive) is fine. Marking the line with the negative float literal as _(unchecked) doesn't help.

EDIT: The answer to this question was found later and described here: http://vc3d.tumblr.com/post/73339717794/note-on-triggers

One thing puzzling me currently about making an invariant for this object is why this is admissible:

_(invariant \forall uint i; i < numfaces ==> \mine(&faces[i]) && \mine(faces[i].edge) && \mine(faces[i].edge->next) && \mine(faces[i].edge->next->next) && \mine(faces[i].edge->next->next->next) && faces[i].edge->next->next->next == faces[i].edge )

but separating the parts of that invariant like below is not admissible:

_(invariant \forall uint i; i < numfaces ==> \mine(&faces[i]) && \mine(faces[i].edge) && \mine(faces[i].edge->next) && \mine(faces[i].edge->next->next) && \mine(faces[i].edge->next->next->next) ) _(invariant \forall uint i; i < numfaces ==> faces[i].edge->next->next->next == faces[i].edge )

I want to point out one issue I had a long while back because I don't think I've mentioned it yet.

The _(dynamic_owns) examples in the tutorial document do not show how to initialize such an object. Particularly, how to initialize the \owns set. Here is an example:

SafeContainer* a; //...malloc and other such things here...// _(ghost a->\owns = {}; )

The \owns set must be initialized with {} before it can be used and before the object can be wrapped, but it's as simple as that :-)

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.

Verification of Mesh#adm failed. [1.40] mesh.h(92,3) : error VC8012: invariant(\forall uint i; ( i < numfaces ) ==> ( faces[i].edge->face == &(faces[i]) ) ) of Mesh is not admissible.

>:|