This project is read-only.

Inconsistent Function Contract - \array_range in writes clause and \wrapped for an array of objects

Jan 8, 2014 at 5:55 AM
Edited Jan 10, 2014 at 2:04 AM
I am confused about what is making the contract of the last example method here inconsistent/contradictory, and I'm not sure how to do it correctly.
They all verify if the _(assert \false) lines are removed; they're just there to demonstrate the inconsistent invariant in the last one without having to run vcc with /smoke.
typedef struct MyObject
{
    int field;
} MyObject;

void WriteIntArray(int* vals, size_t size)
    _(requires size > 0)
    _(writes \array_range(vals,size))
{
    _(assert \false)    //Fails here, like it should
    vals[0] = 3;
}

void WriteSingleStruct(MyObject* obj)
    _(requires \wrapped(obj))
    _(writes obj)
{
    _(assert \false)    //Fails here, like it should
    _(unwrap obj)
    obj->field = 3;
}

void WriteStructArray1(MyObject* objarr, size_t size)
    _(requires size > 0)
    _(requires \forall size_t i; i < size ==> \wrapped(&objarr[i]))
    _(writes &objarr[0])
    //but what if I want all elements to be writable, no matter the size?
{
    _(assert \false)    //Fails here, like it should
    _(unwrap &objarr[0])
    objarr[0].field = 3;
}

void WriteStructArray2(MyObject* objarr, size_t size)
    _(requires size > 0)
    _(requires \forall size_t i; i < size ==> \wrapped(&objarr[i]))
    _(writes \array_range(objarr,size))
    //How can I make all elements writable? Is it even possible?
{
    _(assert \false)    //NO FAILURE... means contract is inconsistent
    _(unwrap &objarr[0])
    objarr[0].field = 3;
}
How does \array_range(obj,size) differ from a simple list of each of the array elements' addresses? What is causing the inconsistency between the array element \wrapped requirement and the \array_range write clause?

Sorry if there's something elementary here that I'm missing -- and thank you for your time!
Jan 8, 2014 at 5:57 PM
Edited Jan 10, 2014 at 2:04 AM
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.
void WriteStructArray2_fixed(MyObject* objarr, size_t size)
    _(requires size > 0)
    _(requires \forall size_t i; i < size ==> \wrapped(&objarr[i]))
    _(writes \array_members(objarr,size))
{
    _(unwrap &objarr[0])
    objarr[0].field = 3;
}
I had searched through the whole website, the tutorial, the manual, the samples, and the test suite to try to figure this out. Only now that I know what to be looking for do I see that testsuite file arrays-12 shows this use of \array_members!!

Here is a post corresponding to this discussion on my project blog, including syntax highlighting and more fleshed-out code samples with malloc and free: http://vc3d.tumblr.com/post/72677614116/fixed-arrays-of-objects

Tags
array object objects arrays structs structures arrayrange arraymembers range members extent full extent array range array members in array array of objects array of structs array of structures malloc free heap
Marked as answer by foxox on 1/9/2014 at 1:38 PM
Jan 8, 2014 at 6:32 PM
Hi foxox,

Thanks for sharing your questions and solutions. You are perfectly right in your last post: array_range contains all objects (even nested ones) whose address is within the array's range, whereas array members only contains the outermost objects whose address is that of an element of the array.

When you run into this kind of issue, you can debug more easily by writing a function that calls the one with the faulty contract on arguments you believe are correct. You will then most likely get a verification error, along with a trace of memory states that you can observe to figure out what is wrong. In this case, you may have seen that some of the objects in \array_range were not writable, which may have made it easier to realize that your intuition of what \array_range meant was wrong.

Keep up the good work!
Francois
Marked as answer by foxox on 1/9/2014 at 1:38 PM
Jan 8, 2014 at 7:13 PM
Hi Francois!
Thank you so much for your confirmation on the difference between and use of \array_range and \array_members !
fdupress wrote:
When you run into this kind of issue, you can debug more easily by writing a function that calls the one with the faulty contract on arguments you believe are correct. You will then most likely get a verification error, along with a trace of memory states that you can observe to figure out what is wrong. In this case, you may have seen that some of the objects in \array_range were not writable, which may have made it easier to realize that your intuition of what \array_range meant was wrong.
I had tried this in another sample of similar code ( http://vc3d.tumblr.com/post/72590187480/arrays-of-objects ) but I was so dumbfounded without knowing that "\array_members" existed that I thought there was some mysterious force blocking the knowledge of writability between my init and disposal function calls, not simply that "_(writes \array_range..." was demanding too much.
Glad to be moving forward again...