Conflict of "writes" and "wrap" constructs at the beginning of loop

Jan 10, 2013 at 2:20 AM

Hi,
I have found a problem that I cannot solve at all. Consider the following simple structure and init function:

typedef struct {
	unsigned int field;
	_(invariant \this->field > 0)
} Structure;

void init(Structure * str)
	_(requires \mutable(str))
	_(writes str)
	_(ensures \wrapped(str))
{
	str->field = 7;
	_(wrap str)

	for (size_t i = 0; i < 10; ++i)
		_(invariant \wrapped(str))
		_(invariant i <= 10)
		_(decreases 10 - i)
	{}
}

This error is displayed after unsuccessful verification:

init.c(16,2) : error VC8011: writes clause of the loop might not be included writes clause of the function.
I guess the problem is in the confrontation of annotations _(writes \span(str)) and _(wrap str), where the function provides direct access to object fields, but wrap command forbids it. However the error occurs only at the beginning of the first loop. Loops may have their own writes annotations, and this causes inconsistency. Unfortunately I cannot remove the _(writes \span(str)) annotation if I want to edit fields of the object before wrapping. How to annotate such a function that initializes and then wraps an object?

David

Coordinator
Jan 10, 2013 at 5:32 PM

Hi David,

  the key is to add the writes clause _(writes \extent(str)) to the function, which allows you to change the fields of str *and* then wrap str. Then, in the loop, you'd want to add the annotation _(writes str), because the loop keeps str wrapped and you'd like the writability of the pointer str across the loop.

  Hope this helps,

  Mark

Jan 14, 2013 at 8:03 PM
Edited Jan 22, 2013 at 5:24 PM

Hi Mark,

I tried the suggestion you mentioned for this case. If I use _(writes \extent(str)) to replace _(writes str) for function. VCC also complain about "writes clause of the loop....".

However, if I add _(writes str) to the loop, it would be acceptable for vcc, even I use _(writes \span(str)) as write clause of function. Why we have to add write clause for the loop even there's nothing been edited. I also tried the following code.

void init(Structure * str)
    _(writes \extent(str))
    _(ensures \wrapped(str))
{
    unsigned t = 0;

    str->field = 7;
    _(wrap str)

    for(size_t i = 0; i < 10; i++)
        _(writes &t) //this also can be _(writes str)
_(invariant t == i) { t++; } }

It Vcc also accept this. 

Thanks very much,

Shu Cheng

Jan 14, 2013 at 8:39 PM

Hi David,

One thing just confuse me. If your for loop would not edit "str", why you need _(invariant \wrapped(str)) for the loop.

If we can remove this invariant, and move _(wrap str) after the for loop. Vcc would accept the code. Otherwise, you may need a write clause for loop to show that you won't write \span(str), like the cases I shown in previous post.

My understanding for this problem is:

    - loop would inherit the write clause from function.

    - at the beginning, the write clause of function is \span(str), which includes pointers to str and everything inside.

    - "wrap str" remove the pointers to fields of str from function's write clause

    - But loop still have that bit of pointers. So problem occurs.

I'm not sure is this understanding correct. But it seems can be used to explain the problem.

Hope this helps, and please correct me if there's anything incorrect.

Thanks very much,

Shu Cheng

Jan 27, 2013 at 9:57 PM

Thanks Mark, hopefully I have understood. If I put _(writes str) clause explicitly, I ignore all writes clauses specified on the function. So I will avoid conflicts of wrap and writes clauses. Inside the loop, then I can unwrap the object and write its fields.

A comment to Shu's question: _(writes \extent(str)) allows you to write fields of object. By quoting writes clause explicitly on the loop, VCC do not use writes clauses of function, and that is what we want. Otherwise, loop would expect writing to wrapped object. That is wrong. But why the function deals with writes clauses of str, when inside it is not written? I am not sure as you are.

Now I can just explain an example with local variable t. Since you have replaced writes clauses of function with your own, the loop does not care about str and code verifies. Of course, you do not need to write it like this, local variables can always be written.

You are right that _(invariant \wrapped(str)) is useless in the example, but generally it is not useless at all. I could unwrap the object inside the loop. Without the invariant I would not know whether the object is wrapped or not after the loop and it would violates postcondition. I do not expect that body of the loop is empty, but I just did not mention the content. This invariant does not cause the error I originally described.

David

Coordinator
Feb 11, 2013 at 8:03 PM
Hi David,

VCC doesn't inspect the loop body to infer anything about writes clauses. In my first comment, I suggested putting _(writes str) on the loop. Indeed, it would be simpler if the loop does not have a writes clauses at all, or in other words, specify a writes for an empty set. Here's your working original example (I also dropped the redundant invariant on \wrapped(str), which isn't needed anymore if str is not written to):
 #include <vcc.h>

typedef struct {
  unsigned int field;
  _(invariant \this->field > 0)
} Structure;

void init(Structure * str)
  _(writes \extent(str))
  _(ensures \wrapped(str))
{
  str->field = 7;
  _(wrap str)

  for (size_t i = 0; i < 10; ++i)
    _(invariant i <= 10)
    _(decreases 10 - i)
    _(writes {})
  {}
}
Hope this helps, Mark